Proof: Remove Common Term
Let's prove the following theorem:
if the following are true:
- a ⋅ x = a ⋅ y
- not (a = 0)
then x = y
Proof:
Given
| 1 | a ⋅ x = a ⋅ y |
|---|---|
| 2 | not (a = 0) |
| # | Claim | Reason |
|---|---|---|
| 1 | (1 / a) ⋅ (a ⋅ x) = (1 / a) ⋅ (a ⋅ y) | if a ⋅ x = a ⋅ y, then (1 / a) ⋅ (a ⋅ x) = (1 / a) ⋅ (a ⋅ y) |
| 2 | (1 / a) ⋅ (a ⋅ x) = x | if not (a = 0), then (1 / a) ⋅ (a ⋅ x) = x |
| 3 | (1 / a) ⋅ (a ⋅ y) = y | if not (a = 0), then (1 / a) ⋅ (a ⋅ y) = y |
| 4 | x = y | if (1 / a) ⋅ (a ⋅ x) = (1 / a) ⋅ (a ⋅ y) and (1 / a) ⋅ (a ⋅ x) = x and (1 / a) ⋅ (a ⋅ y) = y, then x = y |
Comments
Please log in to add comments