This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( 𝐴 <ℝ 𝐵 → ( 𝐶 + 𝐴 ) <ℝ ( 𝐶 + 𝐵 ) ) )