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

Theorem axpre-mulgt0 6771
 Description: The product of two positive reals is positive. Axiom for real and complex numbers, derived from set theory. This construction-dependent theorem should not be referenced directly; instead, use ax-pre-mulgt0 6800. (Contributed by NM, 13-May-1996.) (New usage is discouraged.)
Assertion
Ref Expression
axpre-mulgt0 ((A B ℝ) → ((0 < A 0 < B) → 0 < (A · B)))

Proof of Theorem axpre-mulgt0
Dummy variables x y 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 breq2 3759 . . . 4 (⟨x, 0R⟩ = A → (0 <x, 0R⟩ ↔ 0 < A))
43anbi1d 438 . . 3 (⟨x, 0R⟩ = A → ((0 <x, 0R 0 <y, 0R⟩) ↔ (0 < A 0 <y, 0R⟩)))
5 oveq1 5462 . . . 4 (⟨x, 0R⟩ = A → (⟨x, 0R⟩ · ⟨y, 0R⟩) = (A · ⟨y, 0R⟩))
65breq2d 3767 . . 3 (⟨x, 0R⟩ = A → (0 < (⟨x, 0R⟩ · ⟨y, 0R⟩) ↔ 0 < (A · ⟨y, 0R⟩)))
74, 6imbi12d 223 . 2 (⟨x, 0R⟩ = A → (((0 <x, 0R 0 <y, 0R⟩) → 0 < (⟨x, 0R⟩ · ⟨y, 0R⟩)) ↔ ((0 < A 0 <y, 0R⟩) → 0 < (A · ⟨y, 0R⟩))))
8 breq2 3759 . . . 4 (⟨y, 0R⟩ = B → (0 <y, 0R⟩ ↔ 0 < B))
98anbi2d 437 . . 3 (⟨y, 0R⟩ = B → ((0 < A 0 <y, 0R⟩) ↔ (0 < A 0 < B)))
10 oveq2 5463 . . . 4 (⟨y, 0R⟩ = B → (A · ⟨y, 0R⟩) = (A · B))
1110breq2d 3767 . . 3 (⟨y, 0R⟩ = B → (0 < (A · ⟨y, 0R⟩) ↔ 0 < (A · B)))
129, 11imbi12d 223 . 2 (⟨y, 0R⟩ = B → (((0 < A 0 <y, 0R⟩) → 0 < (A · ⟨y, 0R⟩)) ↔ ((0 < A 0 < B) → 0 < (A · B))))
13 df-0 6718 . . . . . 6 0 = ⟨0R, 0R
1413breq1i 3762 . . . . 5 (0 <x, 0R⟩ ↔ ⟨0R, 0R⟩ <x, 0R⟩)
15 ltresr 6736 . . . . 5 (⟨0R, 0R⟩ <x, 0R⟩ ↔ 0R <R x)
1614, 15bitri 173 . . . 4 (0 <x, 0R⟩ ↔ 0R <R x)
1713breq1i 3762 . . . . 5 (0 <y, 0R⟩ ↔ ⟨0R, 0R⟩ <y, 0R⟩)
18 ltresr 6736 . . . . 5 (⟨0R, 0R⟩ <y, 0R⟩ ↔ 0R <R y)
1917, 18bitri 173 . . . 4 (0 <y, 0R⟩ ↔ 0R <R y)
20 mulgt0sr 6704 . . . 4 ((0R <R x 0R <R y) → 0R <R (x ·R y))
2116, 19, 20syl2anb 275 . . 3 ((0 <x, 0R 0 <y, 0R⟩) → 0R <R (x ·R y))
2213a1i 9 . . . . 5 ((x R y R) → 0 = ⟨0R, 0R⟩)
23 mulresr 6735 . . . . 5 ((x R y R) → (⟨x, 0R⟩ · ⟨y, 0R⟩) = ⟨(x ·R y), 0R⟩)
2422, 23breq12d 3768 . . . 4 ((x R y R) → (0 < (⟨x, 0R⟩ · ⟨y, 0R⟩) ↔ ⟨0R, 0R⟩ < ⟨(x ·R y), 0R⟩))
25 ltresr 6736 . . . 4 (⟨0R, 0R⟩ < ⟨(x ·R y), 0R⟩ ↔ 0R <R (x ·R y))
2624, 25syl6bb 185 . . 3 ((x R y R) → (0 < (⟨x, 0R⟩ · ⟨y, 0R⟩) ↔ 0R <R (x ·R y)))
2721, 26syl5ibr 145 . 2 ((x R y R) → ((0 <x, 0R 0 <y, 0R⟩) → 0 < (⟨x, 0R⟩ · ⟨y, 0R⟩)))
281, 2, 7, 12, 272gencl 2581 1 ((A B ℝ) → ((0 < A 0 < B) → 0 < (A · B)))
 Colors of variables: wff set class Syntax hints:   → wi 4   ∧ wa 97   = 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