PROOF 18

Prove.

Transposition is justified

On the reals ℝ.

A way to read this proof

First separate what is assumed from what is to be proved. At each step, ask which definition or earlier result permits the move. If it is unclear, return to that premise rather than skipping to the conclusion.

Definition D1

The solution set of an equation is the set of all x that make it true.

Proof.

(1)The solution set of a + x = b is { x : a + x = b }.convention

(2)If two equations have the same solution set, they are the same question.convention

∎

Definition D2

b − a denotes b + (−a).

Proof.

The existence of −a is guaranteed by A4.A4

∎

Lemma L1

If a + x = b, then x = b − a

Proof.

(1)Suppose a + x = b.assumption

(2)(a + x) + (−a) = b + (−a)(1), A4, E

(3)(a + x) + (−a) = (x + a) + (−a)A2

(4)　　　　　　 = x + (a + (−a))A1

(5)　　　　　　 = x + 0 = xA4, A3

(6)x = b + (−a) = b − a(2), (5), D2

∎

Lemma L2

If x = b − a, then a + x = b

Proof.

(1)Suppose x = b − a = b + (−a).assumption, D2

(2)a + x = a + (b + (−a))(1), E

(3)　　 = a + ((−a) + b)A2

(4)　　 = (a + (−a)) + bA1

(5)　　 = 0 + b = bA4, A2, A3

(6)a + x = b(2), (5)

∎

Theorem T1

The solution set of a + x = b and the solution set of x = b − a are equal.

Proof.

(1)Every solution of the first equation is a solution of the second.L1, D1

(2)Every solution of the second equation is a solution of the first.L2, D1

(3)The two solution sets contain each other.(1), (2)

(4)Therefore the two solution sets are equal.(3), S

∎

Theorem T2

Multiplying both sides by 0 enlarges the solution set.

Proof.

(1)The solution set of x = d is { d }.D1

(2)Multiplying both sides by 0 gives 0 × x = 0 × d.E

(3)For every x, 0 × x = 0, and 0 × d = 0.A5

(4)Therefore the solution set of 0 × x = 0 × d is all of the reals.(3), D1

(5)Since 0 ≠ 1, there is a real number different from d.A6

(6)The solution set has grown. The two equations are not the same question.(1), (4), (5)

∎

Remark

Can A4 be removed from this proof?

Check whether transposition is a rule, or the result of a reversible operation.