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

Theorem axpre-mulext 6772
 Description: Strong extensionality of multiplication (expressed in terms of <ℝ). Axiom for real and complex numbers, derived from set theory. This construction-dependent theorem should not be referenced directly; instead, use ax-pre-mulext 6801. (Contributed by Jim Kingdon, 18-Feb-2020.) (New usage is discouraged.)
Assertion
Ref Expression
axpre-mulext ((A B 𝐶 ℝ) → ((A · 𝐶) < (B · 𝐶) → (A < B B < A)))

Proof of Theorem axpre-mulext
Dummy variables x y z are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 elreal 6727 . 2 (A ℝ ↔ x Rx, 0R⟩ = A)
2 elreal 6727 . 2 (B ℝ ↔ y Ry, 0R⟩ = B)
3 elreal 6727 . 2 (𝐶 ℝ ↔ z Rz, 0R⟩ = 𝐶)
4 oveq1 5462 . . . 4 (⟨x, 0R⟩ = A → (⟨x, 0R⟩ · ⟨z, 0R⟩) = (A · ⟨z, 0R⟩))
54breq1d 3765 . . 3 (⟨x, 0R⟩ = A → ((⟨x, 0R⟩ · ⟨z, 0R⟩) < (⟨y, 0R⟩ · ⟨z, 0R⟩) ↔ (A · ⟨z, 0R⟩) < (⟨y, 0R⟩ · ⟨z, 0R⟩)))
6 breq1 3758 . . . 4 (⟨x, 0R⟩ = A → (⟨x, 0R⟩ <y, 0R⟩ ↔ A <y, 0R⟩))
7 breq2 3759 . . . 4 (⟨x, 0R⟩ = A → (⟨y, 0R⟩ <x, 0R⟩ ↔ ⟨y, 0R⟩ < A))
86, 7orbi12d 706 . . 3 (⟨x, 0R⟩ = A → ((⟨x, 0R⟩ <y, 0Ry, 0R⟩ <x, 0R⟩) ↔ (A <y, 0Ry, 0R⟩ < A)))
95, 8imbi12d 223 . 2 (⟨x, 0R⟩ = A → (((⟨x, 0R⟩ · ⟨z, 0R⟩) < (⟨y, 0R⟩ · ⟨z, 0R⟩) → (⟨x, 0R⟩ <y, 0Ry, 0R⟩ <x, 0R⟩)) ↔ ((A · ⟨z, 0R⟩) < (⟨y, 0R⟩ · ⟨z, 0R⟩) → (A <y, 0Ry, 0R⟩ < A))))
10 oveq1 5462 . . . 4 (⟨y, 0R⟩ = B → (⟨y, 0R⟩ · ⟨z, 0R⟩) = (B · ⟨z, 0R⟩))
1110breq2d 3767 . . 3 (⟨y, 0R⟩ = B → ((A · ⟨z, 0R⟩) < (⟨y, 0R⟩ · ⟨z, 0R⟩) ↔ (A · ⟨z, 0R⟩) < (B · ⟨z, 0R⟩)))
12 breq2 3759 . . . 4 (⟨y, 0R⟩ = B → (A <y, 0R⟩ ↔ A < B))
13 breq1 3758 . . . 4 (⟨y, 0R⟩ = B → (⟨y, 0R⟩ < AB < A))
1412, 13orbi12d 706 . . 3 (⟨y, 0R⟩ = B → ((A <y, 0Ry, 0R⟩ < A) ↔ (A < B B < A)))
1511, 14imbi12d 223 . 2 (⟨y, 0R⟩ = B → (((A · ⟨z, 0R⟩) < (⟨y, 0R⟩ · ⟨z, 0R⟩) → (A <y, 0Ry, 0R⟩ < A)) ↔ ((A · ⟨z, 0R⟩) < (B · ⟨z, 0R⟩) → (A < B B < A))))
16 oveq2 5463 . . . 4 (⟨z, 0R⟩ = 𝐶 → (A · ⟨z, 0R⟩) = (A · 𝐶))
17 oveq2 5463 . . . 4 (⟨z, 0R⟩ = 𝐶 → (B · ⟨z, 0R⟩) = (B · 𝐶))
1816, 17breq12d 3768 . . 3 (⟨z, 0R⟩ = 𝐶 → ((A · ⟨z, 0R⟩) < (B · ⟨z, 0R⟩) ↔ (A · 𝐶) < (B · 𝐶)))
1918imbi1d 220 . 2 (⟨z, 0R⟩ = 𝐶 → (((A · ⟨z, 0R⟩) < (B · ⟨z, 0R⟩) → (A < B B < A)) ↔ ((A · 𝐶) < (B · 𝐶) → (A < B B < A))))
20 mulextsr1 6707 . . 3 ((x R y R z R) → ((x ·R z) <R (y ·R z) → (x <R y y <R x)))
21 mulresr 6735 . . . . . 6 ((x R z R) → (⟨x, 0R⟩ · ⟨z, 0R⟩) = ⟨(x ·R z), 0R⟩)
22213adant2 922 . . . . 5 ((x R y R z R) → (⟨x, 0R⟩ · ⟨z, 0R⟩) = ⟨(x ·R z), 0R⟩)
23 mulresr 6735 . . . . . 6 ((y R z R) → (⟨y, 0R⟩ · ⟨z, 0R⟩) = ⟨(y ·R z), 0R⟩)
24233adant1 921 . . . . 5 ((x R y R z R) → (⟨y, 0R⟩ · ⟨z, 0R⟩) = ⟨(y ·R z), 0R⟩)
2522, 24breq12d 3768 . . . 4 ((x R y R z R) → ((⟨x, 0R⟩ · ⟨z, 0R⟩) < (⟨y, 0R⟩ · ⟨z, 0R⟩) ↔ ⟨(x ·R z), 0R⟩ < ⟨(y ·R z), 0R⟩))
26 ltresr 6736 . . . 4 (⟨(x ·R z), 0R⟩ < ⟨(y ·R z), 0R⟩ ↔ (x ·R z) <R (y ·R z))
2725, 26syl6bb 185 . . 3 ((x R y R z R) → ((⟨x, 0R⟩ · ⟨z, 0R⟩) < (⟨y, 0R⟩ · ⟨z, 0R⟩) ↔ (x ·R z) <R (y ·R z)))
28 ltresr 6736 . . . . 5 (⟨x, 0R⟩ <y, 0R⟩ ↔ x <R y)
29 ltresr 6736 . . . . 5 (⟨y, 0R⟩ <x, 0R⟩ ↔ y <R x)
3028, 29orbi12i 680 . . . 4 ((⟨x, 0R⟩ <y, 0Ry, 0R⟩ <x, 0R⟩) ↔ (x <R y y <R x))
3130a1i 9 . . 3 ((x R y R z R) → ((⟨x, 0R⟩ <y, 0Ry, 0R⟩ <x, 0R⟩) ↔ (x <R y y <R x)))
3220, 27, 313imtr4d 192 . 2 ((x R y R z R) → ((⟨x, 0R⟩ · ⟨z, 0R⟩) < (⟨y, 0R⟩ · ⟨z, 0R⟩) → (⟨x, 0R⟩ <y, 0Ry, 0R⟩ <x, 0R⟩)))
331, 2, 3, 9, 15, 19, 323gencl 2582 1 ((A B 𝐶 ℝ) → ((A · 𝐶) < (B · 𝐶) → (A < B B < A)))
 Colors of variables: wff set class Syntax hints:   → wi 4   ↔ wb 98   ∨ wo 628   ∧ w3a 884   = wceq 1242   ∈ wcel 1390  ⟨cop 3370   class class class wbr 3755  (class class class)co 5455  Rcnr 6281  0Rc0r 6282   ·R cmr 6286
 Copyright terms: Public domain W3C validator