Advertisement
Not a member of Pastebin yet?
Sign Up,
it unlocks many cool features!
- Theorem “≤-Isotonicity of ·”:
- 0 < d ⇒ (a ≤ b ≡ a · d ≤ b · d)
- Proof:
- Assuming `0 < d`:
- (a ≤ b ≡ a · d ≤ b · d)
- ≡⟨ “Definition of ≤” ⟩
- ((a < b ∨ a = b) ≡ (a · d < b · d) ∨ (a · d = b · d))
- ≡⟨ “<-Isotonicity of ·” with Assumption `0 < d` ⟩
- ((a < b ∨ a = b) ≡ ( a < b ) ∨ (a · d = b · d))
- ≡⟨ “Cancellation of ·” with “Definition of ≠” with “Irreflexivity of <” with Assumption `0 < d` ⟩
- ((a < b ∨ a = b) ≡ ( a < b ) ∨ (a = b))
- ≡⟨ “Reflexivity of ≡” ⟩
- true
Advertisement
Add Comment
Please, Sign In to add comment
Advertisement