Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  axpre-ltadd GIF version

 Description: Ordering property of addition on reals. Axiom for real and complex numbers, derived from set theory. This construction-dependent theorem should not be referenced directly; instead, use ax-pre-ltadd 6799. (Contributed by NM, 11-May-1996.) (New usage is discouraged.)
Assertion
Ref Expression
axpre-ltadd ((A B 𝐶 ℝ) → (A < B → (𝐶 + A) < (𝐶 + B)))

Dummy variables x y z are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 elreal 6727 . . 3 (A ℝ ↔ x Rx, 0R⟩ = A)
2 elreal 6727 . . 3 (B ℝ ↔ y Ry, 0R⟩ = B)
3 elreal 6727 . . 3 (𝐶 ℝ ↔ z Rz, 0R⟩ = 𝐶)
4 breq1 3758 . . . 4 (⟨x, 0R⟩ = A → (⟨x, 0R⟩ <y, 0R⟩ ↔ A <y, 0R⟩))
5 oveq2 5463 . . . . 5 (⟨x, 0R⟩ = A → (⟨z, 0R⟩ + ⟨x, 0R⟩) = (⟨z, 0R⟩ + A))
65breq1d 3765 . . . 4 (⟨x, 0R⟩ = A → ((⟨z, 0R⟩ + ⟨x, 0R⟩) < (⟨z, 0R⟩ + ⟨y, 0R⟩) ↔ (⟨z, 0R⟩ + A) < (⟨z, 0R⟩ + ⟨y, 0R⟩)))
74, 6bibi12d 224 . . 3 (⟨x, 0R⟩ = A → ((⟨x, 0R⟩ <y, 0R⟩ ↔ (⟨z, 0R⟩ + ⟨x, 0R⟩) < (⟨z, 0R⟩ + ⟨y, 0R⟩)) ↔ (A <y, 0R⟩ ↔ (⟨z, 0R⟩ + A) < (⟨z, 0R⟩ + ⟨y, 0R⟩))))
8 breq2 3759 . . . 4 (⟨y, 0R⟩ = B → (A <y, 0R⟩ ↔ A < B))
9 oveq2 5463 . . . . 5 (⟨y, 0R⟩ = B → (⟨z, 0R⟩ + ⟨y, 0R⟩) = (⟨z, 0R⟩ + B))
109breq2d 3767 . . . 4 (⟨y, 0R⟩ = B → ((⟨z, 0R⟩ + A) < (⟨z, 0R⟩ + ⟨y, 0R⟩) ↔ (⟨z, 0R⟩ + A) < (⟨z, 0R⟩ + B)))
118, 10bibi12d 224 . . 3 (⟨y, 0R⟩ = B → ((A <y, 0R⟩ ↔ (⟨z, 0R⟩ + A) < (⟨z, 0R⟩ + ⟨y, 0R⟩)) ↔ (A < B ↔ (⟨z, 0R⟩ + A) < (⟨z, 0R⟩ + B))))
12 oveq1 5462 . . . . 5 (⟨z, 0R⟩ = 𝐶 → (⟨z, 0R⟩ + A) = (𝐶 + A))
13 oveq1 5462 . . . . 5 (⟨z, 0R⟩ = 𝐶 → (⟨z, 0R⟩ + B) = (𝐶 + B))
1412, 13breq12d 3768 . . . 4 (⟨z, 0R⟩ = 𝐶 → ((⟨z, 0R⟩ + A) < (⟨z, 0R⟩ + B) ↔ (𝐶 + A) < (𝐶 + B)))
1514bibi2d 221 . . 3 (⟨z, 0R⟩ = 𝐶 → ((A < B ↔ (⟨z, 0R⟩ + A) < (⟨z, 0R⟩ + B)) ↔ (A < B ↔ (𝐶 + A) < (𝐶 + B))))
16 ltasrg 6698 . . . 4 ((x R y R z R) → (x <R y ↔ (z +R x) <R (z +R y)))
17 ltresr 6736 . . . . 5 (⟨x, 0R⟩ <y, 0R⟩ ↔ x <R y)
1817a1i 9 . . . 4 ((x R y R z R) → (⟨x, 0R⟩ <y, 0R⟩ ↔ x <R y))
19 simp3 905 . . . . . 6 ((x R y R z R) → z R)
20 simp1 903 . . . . . 6 ((x R y R z R) → x R)
21 simp2 904 . . . . . 6 ((x R y R z R) → y R)
22 addresr 6734 . . . . . . 7 ((z R x R) → (⟨z, 0R⟩ + ⟨x, 0R⟩) = ⟨(z +R x), 0R⟩)
23 addresr 6734 . . . . . . 7 ((z R y R) → (⟨z, 0R⟩ + ⟨y, 0R⟩) = ⟨(z +R y), 0R⟩)
2422, 23breqan12d 3770 . . . . . 6 (((z R x R) (z R y R)) → ((⟨z, 0R⟩ + ⟨x, 0R⟩) < (⟨z, 0R⟩ + ⟨y, 0R⟩) ↔ ⟨(z +R x), 0R⟩ < ⟨(z +R y), 0R⟩))
2519, 20, 19, 21, 24syl22anc 1135 . . . . 5 ((x R y R z R) → ((⟨z, 0R⟩ + ⟨x, 0R⟩) < (⟨z, 0R⟩ + ⟨y, 0R⟩) ↔ ⟨(z +R x), 0R⟩ < ⟨(z +R y), 0R⟩))
26 ltresr 6736 . . . . 5 (⟨(z +R x), 0R⟩ < ⟨(z +R y), 0R⟩ ↔ (z +R x) <R (z +R y))
2725, 26syl6bb 185 . . . 4 ((x R y R z R) → ((⟨z, 0R⟩ + ⟨x, 0R⟩) < (⟨z, 0R⟩ + ⟨y, 0R⟩) ↔ (z +R x) <R (z +R y)))
2816, 18, 273bitr4d 209 . . 3 ((x R y R z R) → (⟨x, 0R⟩ <y, 0R⟩ ↔ (⟨z, 0R⟩ + ⟨x, 0R⟩) < (⟨z, 0R⟩ + ⟨y, 0R⟩)))
291, 2, 3, 7, 11, 15, 283gencl 2582 . 2 ((A B 𝐶 ℝ) → (A < B ↔ (𝐶 + A) < (𝐶 + B)))
3029biimpd 132 1 ((A B 𝐶 ℝ) → (A < B → (𝐶 + A) < (𝐶 + B)))
 Colors of variables: wff set class Syntax hints:   → wi 4   ∧ wa 97   ↔ wb 98   ∧ w3a 884   = wceq 1242   ∈ wcel 1390  ⟨cop 3370   class class class wbr 3755  (class class class)co 5455  Rcnr 6281  0Rc0r 6282   +R cplr 6285
 Copyright terms: Public domain W3C validator