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	$⊢ (A \in ℝ \land B \in ℝ) \to ((0 <_{ℝ} A \land 0 <_{ℝ} B) \to 0 <_{ℝ} A B)$

Proof

Step	Hyp	Ref	Expression
1		elreal	$⊢ A \in ℝ \leftrightarrow \exists x \in 𝑹 ⟨x, 0_{𝑹}⟩ = A$
2		elreal	$⊢ B \in ℝ \leftrightarrow \exists y \in 𝑹 ⟨y, 0_{𝑹}⟩ = B$
3		breq2	$⊢ ⟨x, 0_{𝑹}⟩ = A \to (0 <_{ℝ} ⟨x, 0_{𝑹}⟩ \leftrightarrow 0 <_{ℝ} A)$
4	3	anbi1d	$⊢ ⟨x, 0_{𝑹}⟩ = A \to ((0 <_{ℝ} ⟨x, 0_{𝑹}⟩ \land 0 <_{ℝ} ⟨y, 0_{𝑹}⟩) \leftrightarrow (0 <_{ℝ} A \land 0 <_{ℝ} ⟨y, 0_{𝑹}⟩))$
5		oveq1	$⊢ ⟨x, 0_{𝑹}⟩ = A \to ⟨x, 0_{𝑹}⟩ ⟨y, 0_{𝑹}⟩ = A ⟨y, 0_{𝑹}⟩$
6	5	breq2d	$⊢ ⟨x, 0_{𝑹}⟩ = A \to (0 <_{ℝ} ⟨x, 0_{𝑹}⟩ ⟨y, 0_{𝑹}⟩ \leftrightarrow 0 <_{ℝ} A ⟨y, 0_{𝑹}⟩)$
7	4 6	imbi12d	$⊢ ⟨x, 0_{𝑹}⟩ = A \to (((0 <_{ℝ} ⟨x, 0_{𝑹}⟩ \land 0 <_{ℝ} ⟨y, 0_{𝑹}⟩) \to 0 <_{ℝ} ⟨x, 0_{𝑹}⟩ ⟨y, 0_{𝑹}⟩) \leftrightarrow ((0 <_{ℝ} A \land 0 <_{ℝ} ⟨y, 0_{𝑹}⟩) \to 0 <_{ℝ} A ⟨y, 0_{𝑹}⟩))$
8		breq2	$⊢ ⟨y, 0_{𝑹}⟩ = B \to (0 <_{ℝ} ⟨y, 0_{𝑹}⟩ \leftrightarrow 0 <_{ℝ} B)$
9	8	anbi2d	$⊢ ⟨y, 0_{𝑹}⟩ = B \to ((0 <_{ℝ} A \land 0 <_{ℝ} ⟨y, 0_{𝑹}⟩) \leftrightarrow (0 <_{ℝ} A \land 0 <_{ℝ} B))$
10		oveq2	$⊢ ⟨y, 0_{𝑹}⟩ = B \to A ⟨y, 0_{𝑹}⟩ = A B$
11	10	breq2d	$⊢ ⟨y, 0_{𝑹}⟩ = B \to (0 <_{ℝ} A ⟨y, 0_{𝑹}⟩ \leftrightarrow 0 <_{ℝ} A B)$
12	9 11	imbi12d	$⊢ ⟨y, 0_{𝑹}⟩ = B \to (((0 <_{ℝ} A \land 0 <_{ℝ} ⟨y, 0_{𝑹}⟩) \to 0 <_{ℝ} A ⟨y, 0_{𝑹}⟩) \leftrightarrow ((0 <_{ℝ} A \land 0 <_{ℝ} B) \to 0 <_{ℝ} A B))$
13		df-0	$⊢ 0 = ⟨0_{𝑹}, 0_{𝑹}⟩$
14	13	breq1i	$⊢ 0 <_{ℝ} ⟨x, 0_{𝑹}⟩ \leftrightarrow ⟨0_{𝑹}, 0_{𝑹}⟩ <_{ℝ} ⟨x, 0_{𝑹}⟩$
15		ltresr	$⊢ ⟨0_{𝑹}, 0_{𝑹}⟩ <_{ℝ} ⟨x, 0_{𝑹}⟩ \leftrightarrow 0_{𝑹} <_{𝑹} x$
16	14 15	bitri	$⊢ 0 <_{ℝ} ⟨x, 0_{𝑹}⟩ \leftrightarrow 0_{𝑹} <_{𝑹} x$
17	13	breq1i	$⊢ 0 <_{ℝ} ⟨y, 0_{𝑹}⟩ \leftrightarrow ⟨0_{𝑹}, 0_{𝑹}⟩ <_{ℝ} ⟨y, 0_{𝑹}⟩$
18		ltresr	$⊢ ⟨0_{𝑹}, 0_{𝑹}⟩ <_{ℝ} ⟨y, 0_{𝑹}⟩ \leftrightarrow 0_{𝑹} <_{𝑹} y$
19	17 18	bitri	$⊢ 0 <_{ℝ} ⟨y, 0_{𝑹}⟩ \leftrightarrow 0_{𝑹} <_{𝑹} y$
20		mulgt0sr	$⊢ (0_{𝑹} <_{𝑹} x \land 0_{𝑹} <_{𝑹} y) \to 0_{𝑹} <_{𝑹} (x \cdot_{𝑹} y)$
21	16 19 20	syl2anb	$⊢ (0 <_{ℝ} ⟨x, 0_{𝑹}⟩ \land 0 <_{ℝ} ⟨y, 0_{𝑹}⟩) \to 0_{𝑹} <_{𝑹} (x \cdot_{𝑹} y)$
22	13	a1i	$⊢ (x \in 𝑹 \land y \in 𝑹) \to 0 = ⟨0_{𝑹}, 0_{𝑹}⟩$
23		mulresr	$⊢ (x \in 𝑹 \land y \in 𝑹) \to ⟨x, 0_{𝑹}⟩ ⟨y, 0_{𝑹}⟩ = ⟨x \cdot_{𝑹} y, 0_{𝑹}⟩$
24	22 23	breq12d	$⊢ (x \in 𝑹 \land y \in 𝑹) \to (0 <_{ℝ} ⟨x, 0_{𝑹}⟩ ⟨y, 0_{𝑹}⟩ \leftrightarrow ⟨0_{𝑹}, 0_{𝑹}⟩ <_{ℝ} ⟨x \cdot_{𝑹} y, 0_{𝑹}⟩)$
25		ltresr	$⊢ ⟨0_{𝑹}, 0_{𝑹}⟩ <_{ℝ} ⟨x \cdot_{𝑹} y, 0_{𝑹}⟩ \leftrightarrow 0_{𝑹} <_{𝑹} (x \cdot_{𝑹} y)$
26	24 25	bitrdi	$⊢ (x \in 𝑹 \land y \in 𝑹) \to (0 <_{ℝ} ⟨x, 0_{𝑹}⟩ ⟨y, 0_{𝑹}⟩ \leftrightarrow 0_{𝑹} <_{𝑹} (x \cdot_{𝑹} y))$
27	21 26	imbitrrid	$⊢ (x \in 𝑹 \land y \in 𝑹) \to ((0 <_{ℝ} ⟨x, 0_{𝑹}⟩ \land 0 <_{ℝ} ⟨y, 0_{𝑹}⟩) \to 0 <_{ℝ} ⟨x, 0_{𝑹}⟩ ⟨y, 0_{𝑹}⟩)$
28	1 2 7 12 27	2gencl	$⊢ (A \in ℝ \land B \in ℝ) \to ((0 <_{ℝ} A \land 0 <_{ℝ} B) \to 0 <_{ℝ} A B)$

Metamath Proof Explorer

Theorem axpre-mulgt0

Proof