Metamath Proof Explorer


Theorem axpre-mulgt0

Description: The product of two positive reals is positive. Axiom 21 of 22 for real and complex numbers, derived from ZF set theory. Note: The more general version for extended reals is axmulgt0 . This construction-dependent theorem should not be referenced directly; instead, use ax-pre-mulgt0 . (Contributed by NM, 13-May-1996) (New usage is discouraged.)

Ref Expression
Assertion axpre-mulgt0 ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( ( 0 < 𝐴 ∧ 0 < 𝐵 ) → 0 < ( 𝐴 · 𝐵 ) ) )

Proof

Step Hyp Ref Expression
1 elreal ( 𝐴 ∈ ℝ ↔ ∃ 𝑥R𝑥 , 0R ⟩ = 𝐴 )
2 elreal ( 𝐵 ∈ ℝ ↔ ∃ 𝑦R𝑦 , 0R ⟩ = 𝐵 )
3 breq2 ( ⟨ 𝑥 , 0R ⟩ = 𝐴 → ( 0 <𝑥 , 0R ⟩ ↔ 0 < 𝐴 ) )
4 3 anbi1d ( ⟨ 𝑥 , 0R ⟩ = 𝐴 → ( ( 0 <𝑥 , 0R ⟩ ∧ 0 <𝑦 , 0R ⟩ ) ↔ ( 0 < 𝐴 ∧ 0 <𝑦 , 0R ⟩ ) ) )
5 oveq1 ( ⟨ 𝑥 , 0R ⟩ = 𝐴 → ( ⟨ 𝑥 , 0R ⟩ · ⟨ 𝑦 , 0R ⟩ ) = ( 𝐴 · ⟨ 𝑦 , 0R ⟩ ) )
6 5 breq2d ( ⟨ 𝑥 , 0R ⟩ = 𝐴 → ( 0 < ( ⟨ 𝑥 , 0R ⟩ · ⟨ 𝑦 , 0R ⟩ ) ↔ 0 < ( 𝐴 · ⟨ 𝑦 , 0R ⟩ ) ) )
7 4 6 imbi12d ( ⟨ 𝑥 , 0R ⟩ = 𝐴 → ( ( ( 0 <𝑥 , 0R ⟩ ∧ 0 <𝑦 , 0R ⟩ ) → 0 < ( ⟨ 𝑥 , 0R ⟩ · ⟨ 𝑦 , 0R ⟩ ) ) ↔ ( ( 0 < 𝐴 ∧ 0 <𝑦 , 0R ⟩ ) → 0 < ( 𝐴 · ⟨ 𝑦 , 0R ⟩ ) ) ) )
8 breq2 ( ⟨ 𝑦 , 0R ⟩ = 𝐵 → ( 0 <𝑦 , 0R ⟩ ↔ 0 < 𝐵 ) )
9 8 anbi2d ( ⟨ 𝑦 , 0R ⟩ = 𝐵 → ( ( 0 < 𝐴 ∧ 0 <𝑦 , 0R ⟩ ) ↔ ( 0 < 𝐴 ∧ 0 < 𝐵 ) ) )
10 oveq2 ( ⟨ 𝑦 , 0R ⟩ = 𝐵 → ( 𝐴 · ⟨ 𝑦 , 0R ⟩ ) = ( 𝐴 · 𝐵 ) )
11 10 breq2d ( ⟨ 𝑦 , 0R ⟩ = 𝐵 → ( 0 < ( 𝐴 · ⟨ 𝑦 , 0R ⟩ ) ↔ 0 < ( 𝐴 · 𝐵 ) ) )
12 9 11 imbi12d ( ⟨ 𝑦 , 0R ⟩ = 𝐵 → ( ( ( 0 < 𝐴 ∧ 0 <𝑦 , 0R ⟩ ) → 0 < ( 𝐴 · ⟨ 𝑦 , 0R ⟩ ) ) ↔ ( ( 0 < 𝐴 ∧ 0 < 𝐵 ) → 0 < ( 𝐴 · 𝐵 ) ) ) )
13 df-0 0 = ⟨ 0R , 0R
14 13 breq1i ( 0 <𝑥 , 0R ⟩ ↔ ⟨ 0R , 0R ⟩ <𝑥 , 0R ⟩ )
15 ltresr ( ⟨ 0R , 0R ⟩ <𝑥 , 0R ⟩ ↔ 0R <R 𝑥 )
16 14 15 bitri ( 0 <𝑥 , 0R ⟩ ↔ 0R <R 𝑥 )
17 13 breq1i ( 0 <𝑦 , 0R ⟩ ↔ ⟨ 0R , 0R ⟩ <𝑦 , 0R ⟩ )
18 ltresr ( ⟨ 0R , 0R ⟩ <𝑦 , 0R ⟩ ↔ 0R <R 𝑦 )
19 17 18 bitri ( 0 <𝑦 , 0R ⟩ ↔ 0R <R 𝑦 )
20 mulgt0sr ( ( 0R <R 𝑥 ∧ 0R <R 𝑦 ) → 0R <R ( 𝑥 ·R 𝑦 ) )
21 16 19 20 syl2anb ( ( 0 <𝑥 , 0R ⟩ ∧ 0 <𝑦 , 0R ⟩ ) → 0R <R ( 𝑥 ·R 𝑦 ) )
22 13 a1i ( ( 𝑥R𝑦R ) → 0 = ⟨ 0R , 0R ⟩ )
23 mulresr ( ( 𝑥R𝑦R ) → ( ⟨ 𝑥 , 0R ⟩ · ⟨ 𝑦 , 0R ⟩ ) = ⟨ ( 𝑥 ·R 𝑦 ) , 0R ⟩ )
24 22 23 breq12d ( ( 𝑥R𝑦R ) → ( 0 < ( ⟨ 𝑥 , 0R ⟩ · ⟨ 𝑦 , 0R ⟩ ) ↔ ⟨ 0R , 0R ⟩ < ⟨ ( 𝑥 ·R 𝑦 ) , 0R ⟩ ) )
25 ltresr ( ⟨ 0R , 0R ⟩ < ⟨ ( 𝑥 ·R 𝑦 ) , 0R ⟩ ↔ 0R <R ( 𝑥 ·R 𝑦 ) )
26 24 25 bitrdi ( ( 𝑥R𝑦R ) → ( 0 < ( ⟨ 𝑥 , 0R ⟩ · ⟨ 𝑦 , 0R ⟩ ) ↔ 0R <R ( 𝑥 ·R 𝑦 ) ) )
27 21 26 syl5ibr ( ( 𝑥R𝑦R ) → ( ( 0 <𝑥 , 0R ⟩ ∧ 0 <𝑦 , 0R ⟩ ) → 0 < ( ⟨ 𝑥 , 0R ⟩ · ⟨ 𝑦 , 0R ⟩ ) ) )
28 1 2 7 12 27 2gencl ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( ( 0 < 𝐴 ∧ 0 < 𝐵 ) → 0 < ( 𝐴 · 𝐵 ) ) )