Theorem axpre-ltadd

Description: Ordering property of addition on reals. Axiom 20 of 22 for real and complex numbers, derived from ZF set theory. Note: The more general version for extended reals is axltadd . This construction-dependent theorem should not be referenced directly; instead, use ax-pre-ltadd . (Contributed by NM, 11-May-1996) (New usage is discouraged.)

	Ref	Expression
Assertion	axpre-ltadd	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( 𝐴 <ℝ 𝐵 → ( 𝐶 + 𝐴 ) <ℝ ( 𝐶 + 𝐵 ) ) )

Proof

Step	Hyp	Ref	Expression
1		elreal	⊢ ( 𝐴 ∈ ℝ ↔ ∃ 𝑥 ∈ R ⟨ 𝑥 , 0R ⟩ = 𝐴 )
2		elreal	⊢ ( 𝐵 ∈ ℝ ↔ ∃ 𝑦 ∈ R ⟨ 𝑦 , 0R ⟩ = 𝐵 )
3		elreal	⊢ ( 𝐶 ∈ ℝ ↔ ∃ 𝑧 ∈ R ⟨ 𝑧 , 0R ⟩ = 𝐶 )
4		breq1	⊢ ( ⟨ 𝑥 , 0R ⟩ = 𝐴 → ( ⟨ 𝑥 , 0R ⟩ <ℝ ⟨ 𝑦 , 0R ⟩ ↔ 𝐴 <ℝ ⟨ 𝑦 , 0R ⟩ ) )
5		oveq2	⊢ ( ⟨ 𝑥 , 0R ⟩ = 𝐴 → ( ⟨ 𝑧 , 0R ⟩ + ⟨ 𝑥 , 0R ⟩ ) = ( ⟨ 𝑧 , 0R ⟩ + 𝐴 ) )
6	5	breq1d	⊢ ( ⟨ 𝑥 , 0R ⟩ = 𝐴 → ( ( ⟨ 𝑧 , 0R ⟩ + ⟨ 𝑥 , 0R ⟩ ) <ℝ ( ⟨ 𝑧 , 0R ⟩ + ⟨ 𝑦 , 0R ⟩ ) ↔ ( ⟨ 𝑧 , 0R ⟩ + 𝐴 ) <ℝ ( ⟨ 𝑧 , 0R ⟩ + ⟨ 𝑦 , 0R ⟩ ) ) )
7	4 6	bibi12d	⊢ ( ⟨ 𝑥 , 0R ⟩ = 𝐴 → ( ( ⟨ 𝑥 , 0R ⟩ <ℝ ⟨ 𝑦 , 0R ⟩ ↔ ( ⟨ 𝑧 , 0R ⟩ + ⟨ 𝑥 , 0R ⟩ ) <ℝ ( ⟨ 𝑧 , 0R ⟩ + ⟨ 𝑦 , 0R ⟩ ) ) ↔ ( 𝐴 <ℝ ⟨ 𝑦 , 0R ⟩ ↔ ( ⟨ 𝑧 , 0R ⟩ + 𝐴 ) <ℝ ( ⟨ 𝑧 , 0R ⟩ + ⟨ 𝑦 , 0R ⟩ ) ) ) )
8		breq2	⊢ ( ⟨ 𝑦 , 0R ⟩ = 𝐵 → ( 𝐴 <ℝ ⟨ 𝑦 , 0R ⟩ ↔ 𝐴 <ℝ 𝐵 ) )
9		oveq2	⊢ ( ⟨ 𝑦 , 0R ⟩ = 𝐵 → ( ⟨ 𝑧 , 0R ⟩ + ⟨ 𝑦 , 0R ⟩ ) = ( ⟨ 𝑧 , 0R ⟩ + 𝐵 ) )
10	9	breq2d	⊢ ( ⟨ 𝑦 , 0R ⟩ = 𝐵 → ( ( ⟨ 𝑧 , 0R ⟩ + 𝐴 ) <ℝ ( ⟨ 𝑧 , 0R ⟩ + ⟨ 𝑦 , 0R ⟩ ) ↔ ( ⟨ 𝑧 , 0R ⟩ + 𝐴 ) <ℝ ( ⟨ 𝑧 , 0R ⟩ + 𝐵 ) ) )
11	8 10	bibi12d	⊢ ( ⟨ 𝑦 , 0R ⟩ = 𝐵 → ( ( 𝐴 <ℝ ⟨ 𝑦 , 0R ⟩ ↔ ( ⟨ 𝑧 , 0R ⟩ + 𝐴 ) <ℝ ( ⟨ 𝑧 , 0R ⟩ + ⟨ 𝑦 , 0R ⟩ ) ) ↔ ( 𝐴 <ℝ 𝐵 ↔ ( ⟨ 𝑧 , 0R ⟩ + 𝐴 ) <ℝ ( ⟨ 𝑧 , 0R ⟩ + 𝐵 ) ) ) )
12		oveq1	⊢ ( ⟨ 𝑧 , 0R ⟩ = 𝐶 → ( ⟨ 𝑧 , 0R ⟩ + 𝐴 ) = ( 𝐶 + 𝐴 ) )
13		oveq1	⊢ ( ⟨ 𝑧 , 0R ⟩ = 𝐶 → ( ⟨ 𝑧 , 0R ⟩ + 𝐵 ) = ( 𝐶 + 𝐵 ) )
14	12 13	breq12d	⊢ ( ⟨ 𝑧 , 0R ⟩ = 𝐶 → ( ( ⟨ 𝑧 , 0R ⟩ + 𝐴 ) <ℝ ( ⟨ 𝑧 , 0R ⟩ + 𝐵 ) ↔ ( 𝐶 + 𝐴 ) <ℝ ( 𝐶 + 𝐵 ) ) )
15	14	bibi2d	⊢ ( ⟨ 𝑧 , 0R ⟩ = 𝐶 → ( ( 𝐴 <ℝ 𝐵 ↔ ( ⟨ 𝑧 , 0R ⟩ + 𝐴 ) <ℝ ( ⟨ 𝑧 , 0R ⟩ + 𝐵 ) ) ↔ ( 𝐴 <ℝ 𝐵 ↔ ( 𝐶 + 𝐴 ) <ℝ ( 𝐶 + 𝐵 ) ) ) )
16		ltasr	⊢ ( 𝑧 ∈ R → ( 𝑥 <R 𝑦 ↔ ( 𝑧 +R 𝑥 ) <R ( 𝑧 +R 𝑦 ) ) )
17	16	adantr	⊢ ( ( 𝑧 ∈ R ∧ ( 𝑥 ∈ R ∧ 𝑦 ∈ R ) ) → ( 𝑥 <R 𝑦 ↔ ( 𝑧 +R 𝑥 ) <R ( 𝑧 +R 𝑦 ) ) )
18		ltresr	⊢ ( ⟨ 𝑥 , 0R ⟩ <ℝ ⟨ 𝑦 , 0R ⟩ ↔ 𝑥 <R 𝑦 )
19	18	a1i	⊢ ( ( 𝑧 ∈ R ∧ ( 𝑥 ∈ R ∧ 𝑦 ∈ R ) ) → ( ⟨ 𝑥 , 0R ⟩ <ℝ ⟨ 𝑦 , 0R ⟩ ↔ 𝑥 <R 𝑦 ) )
20		addresr	⊢ ( ( 𝑧 ∈ R ∧ 𝑥 ∈ R ) → ( ⟨ 𝑧 , 0R ⟩ + ⟨ 𝑥 , 0R ⟩ ) = ⟨ ( 𝑧 +R 𝑥 ) , 0R ⟩ )
21		addresr	⊢ ( ( 𝑧 ∈ R ∧ 𝑦 ∈ R ) → ( ⟨ 𝑧 , 0R ⟩ + ⟨ 𝑦 , 0R ⟩ ) = ⟨ ( 𝑧 +R 𝑦 ) , 0R ⟩ )
22	20 21	breqan12d	⊢ ( ( ( 𝑧 ∈ R ∧ 𝑥 ∈ R ) ∧ ( 𝑧 ∈ R ∧ 𝑦 ∈ R ) ) → ( ( ⟨ 𝑧 , 0R ⟩ + ⟨ 𝑥 , 0R ⟩ ) <ℝ ( ⟨ 𝑧 , 0R ⟩ + ⟨ 𝑦 , 0R ⟩ ) ↔ ⟨ ( 𝑧 +R 𝑥 ) , 0R ⟩ <ℝ ⟨ ( 𝑧 +R 𝑦 ) , 0R ⟩ ) )
23	22	anandis	⊢ ( ( 𝑧 ∈ R ∧ ( 𝑥 ∈ R ∧ 𝑦 ∈ R ) ) → ( ( ⟨ 𝑧 , 0R ⟩ + ⟨ 𝑥 , 0R ⟩ ) <ℝ ( ⟨ 𝑧 , 0R ⟩ + ⟨ 𝑦 , 0R ⟩ ) ↔ ⟨ ( 𝑧 +R 𝑥 ) , 0R ⟩ <ℝ ⟨ ( 𝑧 +R 𝑦 ) , 0R ⟩ ) )
24		ltresr	⊢ ( ⟨ ( 𝑧 +R 𝑥 ) , 0R ⟩ <ℝ ⟨ ( 𝑧 +R 𝑦 ) , 0R ⟩ ↔ ( 𝑧 +R 𝑥 ) <R ( 𝑧 +R 𝑦 ) )
25	23 24	bitrdi	⊢ ( ( 𝑧 ∈ R ∧ ( 𝑥 ∈ R ∧ 𝑦 ∈ R ) ) → ( ( ⟨ 𝑧 , 0R ⟩ + ⟨ 𝑥 , 0R ⟩ ) <ℝ ( ⟨ 𝑧 , 0R ⟩ + ⟨ 𝑦 , 0R ⟩ ) ↔ ( 𝑧 +R 𝑥 ) <R ( 𝑧 +R 𝑦 ) ) )
26	17 19 25	3bitr4d	⊢ ( ( 𝑧 ∈ R ∧ ( 𝑥 ∈ R ∧ 𝑦 ∈ R ) ) → ( ⟨ 𝑥 , 0R ⟩ <ℝ ⟨ 𝑦 , 0R ⟩ ↔ ( ⟨ 𝑧 , 0R ⟩ + ⟨ 𝑥 , 0R ⟩ ) <ℝ ( ⟨ 𝑧 , 0R ⟩ + ⟨ 𝑦 , 0R ⟩ ) ) )
27	26	ancoms	⊢ ( ( ( 𝑥 ∈ R ∧ 𝑦 ∈ R ) ∧ 𝑧 ∈ R ) → ( ⟨ 𝑥 , 0R ⟩ <ℝ ⟨ 𝑦 , 0R ⟩ ↔ ( ⟨ 𝑧 , 0R ⟩ + ⟨ 𝑥 , 0R ⟩ ) <ℝ ( ⟨ 𝑧 , 0R ⟩ + ⟨ 𝑦 , 0R ⟩ ) ) )
28	27	3impa	⊢ ( ( 𝑥 ∈ R ∧ 𝑦 ∈ R ∧ 𝑧 ∈ R ) → ( ⟨ 𝑥 , 0R ⟩ <ℝ ⟨ 𝑦 , 0R ⟩ ↔ ( ⟨ 𝑧 , 0R ⟩ + ⟨ 𝑥 , 0R ⟩ ) <ℝ ( ⟨ 𝑧 , 0R ⟩ + ⟨ 𝑦 , 0R ⟩ ) ) )
29	1 2 3 7 11 15 28	3gencl	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( 𝐴 <ℝ 𝐵 ↔ ( 𝐶 + 𝐴 ) <ℝ ( 𝐶 + 𝐵 ) ) )
30	29	biimpd	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( 𝐴 <ℝ 𝐵 → ( 𝐶 + 𝐴 ) <ℝ ( 𝐶 + 𝐵 ) ) )