xmulge0

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

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

Proof

Step	Hyp	Ref	Expression
1		xmulgt0	$⊢ ((A \in ℝ^{} \land 0 < A) \land (B \in ℝ^{} \land 0 < B)) \to 0 < A \cdot_{𝑒} B$
2	1	an4s	$⊢ ((A \in ℝ^{} \land B \in ℝ^{}) \land (0 < A \land 0 < B)) \to 0 < A \cdot_{𝑒} B$
3		0xr	$⊢ 0 \in ℝ^{*}$
4		xmulcl	$⊢ (A \in ℝ^{} \land B \in ℝ^{}) \to A \cdot_{𝑒} B \in ℝ^{*}$
5	4	adantr	$⊢ ((A \in ℝ^{} \land B \in ℝ^{}) \land (0 < A \land 0 < B)) \to A \cdot_{𝑒} B \in ℝ^{*}$
6		xrltle	$⊢ (0 \in ℝ^{} \land A \cdot_{𝑒} B \in ℝ^{}) \to (0 < A \cdot_{𝑒} B \to 0 \leq A \cdot_{𝑒} B)$
7	3 5 6	sylancr	$⊢ ((A \in ℝ^{} \land B \in ℝ^{}) \land (0 < A \land 0 < B)) \to (0 < A \cdot_{𝑒} B \to 0 \leq A \cdot_{𝑒} B)$
8	2 7	mpd	$⊢ ((A \in ℝ^{} \land B \in ℝ^{}) \land (0 < A \land 0 < B)) \to 0 \leq A \cdot_{𝑒} B$
9	8	ex	$⊢ (A \in ℝ^{} \land B \in ℝ^{}) \to ((0 < A \land 0 < B) \to 0 \leq A \cdot_{𝑒} B)$
10	9	ad2ant2r	$⊢ ((A \in ℝ^{} \land 0 \leq A) \land (B \in ℝ^{} \land 0 \leq B)) \to ((0 < A \land 0 < B) \to 0 \leq A \cdot_{𝑒} B)$
11	10	impl	$⊢ ((((A \in ℝ^{} \land 0 \leq A) \land (B \in ℝ^{} \land 0 \leq B)) \land 0 < A) \land 0 < B) \to 0 \leq A \cdot_{𝑒} B$
12		0le0	$⊢ 0 \leq 0$
13		oveq2	$⊢ 0 = B \to A \cdot_{𝑒} 0 = A \cdot_{𝑒} B$
14	13	eqcomd	$⊢ 0 = B \to A \cdot_{𝑒} B = A \cdot_{𝑒} 0$
15		xmul01	$⊢ A \in ℝ^{*} \to A \cdot_{𝑒} 0 = 0$
16	15	ad2antrr	$⊢ ((A \in ℝ^{} \land 0 \leq A) \land (B \in ℝ^{} \land 0 \leq B)) \to A \cdot_{𝑒} 0 = 0$
17	14 16	sylan9eqr	$⊢ (((A \in ℝ^{} \land 0 \leq A) \land (B \in ℝ^{} \land 0 \leq B)) \land 0 = B) \to A \cdot_{𝑒} B = 0$
18	12 17	breqtrrid	$⊢ (((A \in ℝ^{} \land 0 \leq A) \land (B \in ℝ^{} \land 0 \leq B)) \land 0 = B) \to 0 \leq A \cdot_{𝑒} B$
19	18	adantlr	$⊢ ((((A \in ℝ^{} \land 0 \leq A) \land (B \in ℝ^{} \land 0 \leq B)) \land 0 < A) \land 0 = B) \to 0 \leq A \cdot_{𝑒} B$
20		xrleloe	$⊢ (0 \in ℝ^{} \land B \in ℝ^{}) \to (0 \leq B \leftrightarrow (0 < B \lor 0 = B))$
21	3 20	mpan	$⊢ B \in ℝ^{*} \to (0 \leq B \leftrightarrow (0 < B \lor 0 = B))$
22	21	biimpa	$⊢ (B \in ℝ^{*} \land 0 \leq B) \to (0 < B \lor 0 = B)$
23	22	ad2antlr	$⊢ (((A \in ℝ^{} \land 0 \leq A) \land (B \in ℝ^{} \land 0 \leq B)) \land 0 < A) \to (0 < B \lor 0 = B)$
24	11 19 23	mpjaodan	$⊢ (((A \in ℝ^{} \land 0 \leq A) \land (B \in ℝ^{} \land 0 \leq B)) \land 0 < A) \to 0 \leq A \cdot_{𝑒} B$
25		oveq1	$⊢ 0 = A \to 0 \cdot_{𝑒} B = A \cdot_{𝑒} B$
26	25	eqcomd	$⊢ 0 = A \to A \cdot_{𝑒} B = 0 \cdot_{𝑒} B$
27		xmul02	$⊢ B \in ℝ^{*} \to 0 \cdot_{𝑒} B = 0$
28	27	ad2antrl	$⊢ ((A \in ℝ^{} \land 0 \leq A) \land (B \in ℝ^{} \land 0 \leq B)) \to 0 \cdot_{𝑒} B = 0$
29	26 28	sylan9eqr	$⊢ (((A \in ℝ^{} \land 0 \leq A) \land (B \in ℝ^{} \land 0 \leq B)) \land 0 = A) \to A \cdot_{𝑒} B = 0$
30	12 29	breqtrrid	$⊢ (((A \in ℝ^{} \land 0 \leq A) \land (B \in ℝ^{} \land 0 \leq B)) \land 0 = A) \to 0 \leq A \cdot_{𝑒} B$
31		xrleloe	$⊢ (0 \in ℝ^{} \land A \in ℝ^{}) \to (0 \leq A \leftrightarrow (0 < A \lor 0 = A))$
32	3 31	mpan	$⊢ A \in ℝ^{*} \to (0 \leq A \leftrightarrow (0 < A \lor 0 = A))$
33	32	biimpa	$⊢ (A \in ℝ^{*} \land 0 \leq A) \to (0 < A \lor 0 = A)$
34	33	adantr	$⊢ ((A \in ℝ^{} \land 0 \leq A) \land (B \in ℝ^{} \land 0 \leq B)) \to (0 < A \lor 0 = A)$
35	24 30 34	mpjaodan	$⊢ ((A \in ℝ^{} \land 0 \leq A) \land (B \in ℝ^{} \land 0 \leq B)) \to 0 \leq A \cdot_{𝑒} B$

Metamath Proof Explorer

Theorem xmulge0

Proof