Advertisement
Guest User

Untitled

a guest
Oct 19th, 2018
81
0
Never
Not a member of Pastebin yet? Sign Up, it unlocks many cool features!
text 0.62 KB | None | 0 0
  1. Theorem “≤-Isotonicity of ·”:
  2. 0 < d ⇒ (a ≤ b ≡ a · d ≤ b · d)
  3. Proof:
  4. Assuming `0 < d`:
  5. (a ≤ b ≡ a · d ≤ b · d)
  6. ≡⟨ “Definition of ≤” ⟩
  7. ((a < b ∨ a = b) ≡ (a · d < b · d) ∨ (a · d = b · d))
  8. ≡⟨ “<-Isotonicity of ·” with Assumption `0 < d` ⟩
  9. ((a < b ∨ a = b) ≡ ( a < b ) ∨ (a · d = b · d))
  10. ≡⟨ “Cancellation of ·” with “Definition of ≠” with “Irreflexivity of <” with Assumption `0 < d` ⟩
  11. ((a < b ∨ a = b) ≡ ( a < b ) ∨ (a = b))
  12. ≡⟨ “Reflexivity of ≡” ⟩
  13. true
Advertisement
Add Comment
Please, Sign In to add comment
Advertisement