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 <ℝ ( 𝐴 · 𝐵 ) ) )