xmulgt0

Description: Extended real version of mulgt0 . (Contributed by Mario Carneiro, 20-Aug-2015)

		Ref	Expression
	Assertion	xmulgt0	$⊢ ((A \in ℝ^{} \land 0 < A) \land (B \in ℝ^{} \land 0 < B)) \to 0 < A \cdot_{𝑒} B$

Proof

Step	Hyp	Ref	Expression
1		simpr	$⊢ (A \in ℝ^{*} \land 0 < A) \to 0 < A$
2		simpr	$⊢ (B \in ℝ^{*} \land 0 < B) \to 0 < B$
3	1 2	anim12i	$⊢ ((A \in ℝ^{} \land 0 < A) \land (B \in ℝ^{} \land 0 < B)) \to (0 < A \land 0 < B)$
4		mulgt0	$⊢ ((A \in ℝ \land 0 < A) \land (B \in ℝ \land 0 < B)) \to 0 < A B$
5	4	an4s	$⊢ ((A \in ℝ \land B \in ℝ) \land (0 < A \land 0 < B)) \to 0 < A B$
6	5	ancoms	$⊢ ((0 < A \land 0 < B) \land (A \in ℝ \land B \in ℝ)) \to 0 < A B$
7		rexmul	$⊢ (A \in ℝ \land B \in ℝ) \to A \cdot_{𝑒} B = A B$
8	7	adantl	$⊢ ((0 < A \land 0 < B) \land (A \in ℝ \land B \in ℝ)) \to A \cdot_{𝑒} B = A B$
9	6 8	breqtrrd	$⊢ ((0 < A \land 0 < B) \land (A \in ℝ \land B \in ℝ)) \to 0 < A \cdot_{𝑒} B$
10	3 9	sylan	$⊢ (((A \in ℝ^{} \land 0 < A) \land (B \in ℝ^{} \land 0 < B)) \land (A \in ℝ \land B \in ℝ)) \to 0 < A \cdot_{𝑒} B$
11	10	anassrs	$⊢ ((((A \in ℝ^{} \land 0 < A) \land (B \in ℝ^{} \land 0 < B)) \land A \in ℝ) \land B \in ℝ) \to 0 < A \cdot_{𝑒} B$
12		0ltpnf	$⊢ 0 < +∞$
13		oveq2	$⊢ B = +∞ \to A \cdot_{𝑒} B = A \cdot_{𝑒} +∞$
14		xmulpnf1	$⊢ (A \in ℝ^{*} \land 0 < A) \to A \cdot_{𝑒} +∞ = +∞$
15	14	adantr	$⊢ ((A \in ℝ^{} \land 0 < A) \land (B \in ℝ^{} \land 0 < B)) \to A \cdot_{𝑒} +∞ = +∞$
16	13 15	sylan9eqr	$⊢ (((A \in ℝ^{} \land 0 < A) \land (B \in ℝ^{} \land 0 < B)) \land B = +∞) \to A \cdot_{𝑒} B = +∞$
17	12 16	breqtrrid	$⊢ (((A \in ℝ^{} \land 0 < A) \land (B \in ℝ^{} \land 0 < B)) \land B = +∞) \to 0 < A \cdot_{𝑒} B$
18	17	adantlr	$⊢ ((((A \in ℝ^{} \land 0 < A) \land (B \in ℝ^{} \land 0 < B)) \land A \in ℝ) \land B = +∞) \to 0 < A \cdot_{𝑒} B$
19		simplrr	$⊢ (((A \in ℝ^{} \land 0 < A) \land (B \in ℝ^{} \land 0 < B)) \land A \in ℝ) \to 0 < B$
20		xmulasslem2	$⊢ (0 < B \land B = −∞) \to 0 < A \cdot_{𝑒} B$
21	19 20	sylan	$⊢ ((((A \in ℝ^{} \land 0 < A) \land (B \in ℝ^{} \land 0 < B)) \land A \in ℝ) \land B = −∞) \to 0 < A \cdot_{𝑒} B$
22		simprl	$⊢ ((A \in ℝ^{} \land 0 < A) \land (B \in ℝ^{} \land 0 < B)) \to B \in ℝ^{*}$
23		elxr	$⊢ B \in ℝ^{*} \leftrightarrow (B \in ℝ \lor B = +∞ \lor B = −∞)$
24	22 23	sylib	$⊢ ((A \in ℝ^{} \land 0 < A) \land (B \in ℝ^{} \land 0 < B)) \to (B \in ℝ \lor B = +∞ \lor B = −∞)$
25	24	adantr	$⊢ (((A \in ℝ^{} \land 0 < A) \land (B \in ℝ^{} \land 0 < B)) \land A \in ℝ) \to (B \in ℝ \lor B = +∞ \lor B = −∞)$
26	11 18 21 25	mpjao3dan	$⊢ (((A \in ℝ^{} \land 0 < A) \land (B \in ℝ^{} \land 0 < B)) \land A \in ℝ) \to 0 < A \cdot_{𝑒} B$
27		oveq1	$⊢ A = +∞ \to A \cdot_{𝑒} B = +∞ \cdot_{𝑒} B$
28		xmulpnf2	$⊢ (B \in ℝ^{*} \land 0 < B) \to +∞ \cdot_{𝑒} B = +∞$
29	28	adantl	$⊢ ((A \in ℝ^{} \land 0 < A) \land (B \in ℝ^{} \land 0 < B)) \to +∞ \cdot_{𝑒} B = +∞$
30	27 29	sylan9eqr	$⊢ (((A \in ℝ^{} \land 0 < A) \land (B \in ℝ^{} \land 0 < B)) \land A = +∞) \to A \cdot_{𝑒} B = +∞$
31	12 30	breqtrrid	$⊢ (((A \in ℝ^{} \land 0 < A) \land (B \in ℝ^{} \land 0 < B)) \land A = +∞) \to 0 < A \cdot_{𝑒} B$
32		xmulasslem2	$⊢ (0 < A \land A = −∞) \to 0 < A \cdot_{𝑒} B$
33	32	ad4ant24	$⊢ (((A \in ℝ^{} \land 0 < A) \land (B \in ℝ^{} \land 0 < B)) \land A = −∞) \to 0 < A \cdot_{𝑒} B$
34		simpll	$⊢ ((A \in ℝ^{} \land 0 < A) \land (B \in ℝ^{} \land 0 < B)) \to A \in ℝ^{*}$
35		elxr	$⊢ A \in ℝ^{*} \leftrightarrow (A \in ℝ \lor A = +∞ \lor A = −∞)$
36	34 35	sylib	$⊢ ((A \in ℝ^{} \land 0 < A) \land (B \in ℝ^{} \land 0 < B)) \to (A \in ℝ \lor A = +∞ \lor A = −∞)$
37	26 31 33 36	mpjao3dan	$⊢ ((A \in ℝ^{} \land 0 < A) \land (B \in ℝ^{} \land 0 < B)) \to 0 < A \cdot_{𝑒} B$

Metamath Proof Explorer

Theorem xmulgt0

Proof