Theorem ltadd2

Description: Addition to both sides of 'less than'. (Contributed by NM, 12-Nov-1999) (Revised by Mario Carneiro, 27-May-2016)

	Ref	Expression
Assertion	ltadd2	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( 𝐴 < 𝐵 ↔ ( 𝐶 + 𝐴 ) < ( 𝐶 + 𝐵 ) ) )

Proof

Step	Hyp	Ref	Expression
1		axltadd	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( 𝐴 < 𝐵 → ( 𝐶 + 𝐴 ) < ( 𝐶 + 𝐵 ) ) )
2		oveq2	⊢ ( 𝐴 = 𝐵 → ( 𝐶 + 𝐴 ) = ( 𝐶 + 𝐵 ) )
3	2	a1i	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( 𝐴 = 𝐵 → ( 𝐶 + 𝐴 ) = ( 𝐶 + 𝐵 ) ) )
4		axltadd	⊢ ( ( 𝐵 ∈ ℝ ∧ 𝐴 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( 𝐵 < 𝐴 → ( 𝐶 + 𝐵 ) < ( 𝐶 + 𝐴 ) ) )
5	4	3com12	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( 𝐵 < 𝐴 → ( 𝐶 + 𝐵 ) < ( 𝐶 + 𝐴 ) ) )
6	3 5	orim12d	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( ( 𝐴 = 𝐵 ∨ 𝐵 < 𝐴 ) → ( ( 𝐶 + 𝐴 ) = ( 𝐶 + 𝐵 ) ∨ ( 𝐶 + 𝐵 ) < ( 𝐶 + 𝐴 ) ) ) )
7	6	con3d	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( ¬ ( ( 𝐶 + 𝐴 ) = ( 𝐶 + 𝐵 ) ∨ ( 𝐶 + 𝐵 ) < ( 𝐶 + 𝐴 ) ) → ¬ ( 𝐴 = 𝐵 ∨ 𝐵 < 𝐴 ) ) )
8		simp3	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → 𝐶 ∈ ℝ )
9		simp1	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → 𝐴 ∈ ℝ )
10	8 9	readdcld	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( 𝐶 + 𝐴 ) ∈ ℝ )
11		simp2	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → 𝐵 ∈ ℝ )
12	8 11	readdcld	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( 𝐶 + 𝐵 ) ∈ ℝ )
13		axlttri	⊢ ( ( ( 𝐶 + 𝐴 ) ∈ ℝ ∧ ( 𝐶 + 𝐵 ) ∈ ℝ ) → ( ( 𝐶 + 𝐴 ) < ( 𝐶 + 𝐵 ) ↔ ¬ ( ( 𝐶 + 𝐴 ) = ( 𝐶 + 𝐵 ) ∨ ( 𝐶 + 𝐵 ) < ( 𝐶 + 𝐴 ) ) ) )
14	10 12 13	syl2anc	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( ( 𝐶 + 𝐴 ) < ( 𝐶 + 𝐵 ) ↔ ¬ ( ( 𝐶 + 𝐴 ) = ( 𝐶 + 𝐵 ) ∨ ( 𝐶 + 𝐵 ) < ( 𝐶 + 𝐴 ) ) ) )
15		axlttri	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 < 𝐵 ↔ ¬ ( 𝐴 = 𝐵 ∨ 𝐵 < 𝐴 ) ) )
16	9 11 15	syl2anc	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( 𝐴 < 𝐵 ↔ ¬ ( 𝐴 = 𝐵 ∨ 𝐵 < 𝐴 ) ) )
17	7 14 16	3imtr4d	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( ( 𝐶 + 𝐴 ) < ( 𝐶 + 𝐵 ) → 𝐴 < 𝐵 ) )
18	1 17	impbid	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( 𝐴 < 𝐵 ↔ ( 𝐶 + 𝐴 ) < ( 𝐶 + 𝐵 ) ) )