This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 imbitrrid ⊢ ( ( 𝑥 ∈ R ∧ 𝑦 ∈ R ) → ( ( 0 <ℝ ⟨ 𝑥 , 0R ⟩ ∧ 0 <ℝ ⟨ 𝑦 , 0R ⟩ ) → 0 <ℝ ( ⟨ 𝑥 , 0R ⟩ · ⟨ 𝑦 , 0R ⟩ ) ) )
28 1 2 7 12 27 2gencl ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( ( 0 <ℝ 𝐴 ∧ 0 <ℝ 𝐵 ) → 0 <ℝ ( 𝐴 · 𝐵 ) ) )