Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  axpre-ltadd Structured version   Visualization version   GIF version

 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 10055. This construction-dependent theorem should not be referenced directly; instead, use ax-pre-ltadd 9956. (Contributed by NM, 11-May-1996.) (New usage is discouraged.)
Assertion
Ref Expression
axpre-ltadd ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐴 < 𝐵 → (𝐶 + 𝐴) < (𝐶 + 𝐵)))

Dummy variables 𝑥 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 elreal 9896 . . 3 (𝐴 ∈ ℝ ↔ ∃𝑥R𝑥, 0R⟩ = 𝐴)
2 elreal 9896 . . 3 (𝐵 ∈ ℝ ↔ ∃𝑦R𝑦, 0R⟩ = 𝐵)
3 elreal 9896 . . 3 (𝐶 ∈ ℝ ↔ ∃𝑧R𝑧, 0R⟩ = 𝐶)
4 breq1 4616 . . . 4 (⟨𝑥, 0R⟩ = 𝐴 → (⟨𝑥, 0R⟩ <𝑦, 0R⟩ ↔ 𝐴 <𝑦, 0R⟩))
5 oveq2 6612 . . . . 5 (⟨𝑥, 0R⟩ = 𝐴 → (⟨𝑧, 0R⟩ + ⟨𝑥, 0R⟩) = (⟨𝑧, 0R⟩ + 𝐴))
65breq1d 4623 . . . 4 (⟨𝑥, 0R⟩ = 𝐴 → ((⟨𝑧, 0R⟩ + ⟨𝑥, 0R⟩) < (⟨𝑧, 0R⟩ + ⟨𝑦, 0R⟩) ↔ (⟨𝑧, 0R⟩ + 𝐴) < (⟨𝑧, 0R⟩ + ⟨𝑦, 0R⟩)))
74, 6bibi12d 335 . . 3 (⟨𝑥, 0R⟩ = 𝐴 → ((⟨𝑥, 0R⟩ <𝑦, 0R⟩ ↔ (⟨𝑧, 0R⟩ + ⟨𝑥, 0R⟩) < (⟨𝑧, 0R⟩ + ⟨𝑦, 0R⟩)) ↔ (𝐴 <𝑦, 0R⟩ ↔ (⟨𝑧, 0R⟩ + 𝐴) < (⟨𝑧, 0R⟩ + ⟨𝑦, 0R⟩))))
8 breq2 4617 . . . 4 (⟨𝑦, 0R⟩ = 𝐵 → (𝐴 <𝑦, 0R⟩ ↔ 𝐴 < 𝐵))
9 oveq2 6612 . . . . 5 (⟨𝑦, 0R⟩ = 𝐵 → (⟨𝑧, 0R⟩ + ⟨𝑦, 0R⟩) = (⟨𝑧, 0R⟩ + 𝐵))
109breq2d 4625 . . . 4 (⟨𝑦, 0R⟩ = 𝐵 → ((⟨𝑧, 0R⟩ + 𝐴) < (⟨𝑧, 0R⟩ + ⟨𝑦, 0R⟩) ↔ (⟨𝑧, 0R⟩ + 𝐴) < (⟨𝑧, 0R⟩ + 𝐵)))
118, 10bibi12d 335 . . 3 (⟨𝑦, 0R⟩ = 𝐵 → ((𝐴 <𝑦, 0R⟩ ↔ (⟨𝑧, 0R⟩ + 𝐴) < (⟨𝑧, 0R⟩ + ⟨𝑦, 0R⟩)) ↔ (𝐴 < 𝐵 ↔ (⟨𝑧, 0R⟩ + 𝐴) < (⟨𝑧, 0R⟩ + 𝐵))))
12 oveq1 6611 . . . . 5 (⟨𝑧, 0R⟩ = 𝐶 → (⟨𝑧, 0R⟩ + 𝐴) = (𝐶 + 𝐴))
13 oveq1 6611 . . . . 5 (⟨𝑧, 0R⟩ = 𝐶 → (⟨𝑧, 0R⟩ + 𝐵) = (𝐶 + 𝐵))
1412, 13breq12d 4626 . . . 4 (⟨𝑧, 0R⟩ = 𝐶 → ((⟨𝑧, 0R⟩ + 𝐴) < (⟨𝑧, 0R⟩ + 𝐵) ↔ (𝐶 + 𝐴) < (𝐶 + 𝐵)))
1514bibi2d 332 . . 3 (⟨𝑧, 0R⟩ = 𝐶 → ((𝐴 < 𝐵 ↔ (⟨𝑧, 0R⟩ + 𝐴) < (⟨𝑧, 0R⟩ + 𝐵)) ↔ (𝐴 < 𝐵 ↔ (𝐶 + 𝐴) < (𝐶 + 𝐵))))
16 ltasr 9865 . . . . . . 7 (𝑧R → (𝑥 <R 𝑦 ↔ (𝑧 +R 𝑥) <R (𝑧 +R 𝑦)))
1716adantr 481 . . . . . 6 ((𝑧R ∧ (𝑥R𝑦R)) → (𝑥 <R 𝑦 ↔ (𝑧 +R 𝑥) <R (𝑧 +R 𝑦)))
18 ltresr 9905 . . . . . . 7 (⟨𝑥, 0R⟩ <𝑦, 0R⟩ ↔ 𝑥 <R 𝑦)
1918a1i 11 . . . . . 6 ((𝑧R ∧ (𝑥R𝑦R)) → (⟨𝑥, 0R⟩ <𝑦, 0R⟩ ↔ 𝑥 <R 𝑦))
20 addresr 9903 . . . . . . . . 9 ((𝑧R𝑥R) → (⟨𝑧, 0R⟩ + ⟨𝑥, 0R⟩) = ⟨(𝑧 +R 𝑥), 0R⟩)
21 addresr 9903 . . . . . . . . 9 ((𝑧R𝑦R) → (⟨𝑧, 0R⟩ + ⟨𝑦, 0R⟩) = ⟨(𝑧 +R 𝑦), 0R⟩)
2220, 21breqan12d 4629 . . . . . . . 8 (((𝑧R𝑥R) ∧ (𝑧R𝑦R)) → ((⟨𝑧, 0R⟩ + ⟨𝑥, 0R⟩) < (⟨𝑧, 0R⟩ + ⟨𝑦, 0R⟩) ↔ ⟨(𝑧 +R 𝑥), 0R⟩ < ⟨(𝑧 +R 𝑦), 0R⟩))
2322anandis 872 . . . . . . 7 ((𝑧R ∧ (𝑥R𝑦R)) → ((⟨𝑧, 0R⟩ + ⟨𝑥, 0R⟩) < (⟨𝑧, 0R⟩ + ⟨𝑦, 0R⟩) ↔ ⟨(𝑧 +R 𝑥), 0R⟩ < ⟨(𝑧 +R 𝑦), 0R⟩))
24 ltresr 9905 . . . . . . 7 (⟨(𝑧 +R 𝑥), 0R⟩ < ⟨(𝑧 +R 𝑦), 0R⟩ ↔ (𝑧 +R 𝑥) <R (𝑧 +R 𝑦))
2523, 24syl6bb 276 . . . . . 6 ((𝑧R ∧ (𝑥R𝑦R)) → ((⟨𝑧, 0R⟩ + ⟨𝑥, 0R⟩) < (⟨𝑧, 0R⟩ + ⟨𝑦, 0R⟩) ↔ (𝑧 +R 𝑥) <R (𝑧 +R 𝑦)))
2617, 19, 253bitr4d 300 . . . . 5 ((𝑧R ∧ (𝑥R𝑦R)) → (⟨𝑥, 0R⟩ <𝑦, 0R⟩ ↔ (⟨𝑧, 0R⟩ + ⟨𝑥, 0R⟩) < (⟨𝑧, 0R⟩ + ⟨𝑦, 0R⟩)))
2726ancoms 469 . . . 4 (((𝑥R𝑦R) ∧ 𝑧R) → (⟨𝑥, 0R⟩ <𝑦, 0R⟩ ↔ (⟨𝑧, 0R⟩ + ⟨𝑥, 0R⟩) < (⟨𝑧, 0R⟩ + ⟨𝑦, 0R⟩)))
28273impa 1256 . . 3 ((𝑥R𝑦R𝑧R) → (⟨𝑥, 0R⟩ <𝑦, 0R⟩ ↔ (⟨𝑧, 0R⟩ + ⟨𝑥, 0R⟩) < (⟨𝑧, 0R⟩ + ⟨𝑦, 0R⟩)))
291, 2, 3, 7, 11, 15, 283gencl 3223 . 2 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐴 < 𝐵 ↔ (𝐶 + 𝐴) < (𝐶 + 𝐵)))
3029biimpd 219 1 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐴 < 𝐵 → (𝐶 + 𝐴) < (𝐶 + 𝐵)))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 196   ∧ wa 384   ∧ w3a 1036   = wceq 1480   ∈ wcel 1987  ⟨cop 4154   class class class wbr 4613  (class class class)co 6604  Rcnr 9631  0Rc0r 9632   +R cplr 9635
 Copyright terms: Public domain W3C validator