prodgt0

Description: Infer that a multiplicand is positive from a nonnegative multiplier and positive product. (Contributed by NM, 24-Apr-2005) (Revised by Mario Carneiro, 27-May-2016)

		Ref	Expression
	Assertion	prodgt0	$⊢ ((A \in ℝ \land B \in ℝ) \land (0 \leq A \land 0 < A B)) \to 0 < B$

Proof

Step	Hyp	Ref	Expression
1		0red	$⊢ (A \in ℝ \land B \in ℝ) \to 0 \in ℝ$
2		simpl	$⊢ (A \in ℝ \land B \in ℝ) \to A \in ℝ$
3	1 2	leloed	$⊢ (A \in ℝ \land B \in ℝ) \to (0 \leq A \leftrightarrow (0 < A \lor 0 = A))$
4		simpll	$⊢ ((A \in ℝ \land B \in ℝ) \land (0 < A \land 0 < A B)) \to A \in ℝ$
5		simplr	$⊢ ((A \in ℝ \land B \in ℝ) \land (0 < A \land 0 < A B)) \to B \in ℝ$
6	4 5	remulcld	$⊢ ((A \in ℝ \land B \in ℝ) \land (0 < A \land 0 < A B)) \to A B \in ℝ$
7		simprl	$⊢ ((A \in ℝ \land B \in ℝ) \land (0 < A \land 0 < A B)) \to 0 < A$
8	7	gt0ne0d	$⊢ ((A \in ℝ \land B \in ℝ) \land (0 < A \land 0 < A B)) \to A \neq 0$
9	4 8	rereccld	$⊢ ((A \in ℝ \land B \in ℝ) \land (0 < A \land 0 < A B)) \to \frac{1}{A} \in ℝ$
10		simprr	$⊢ ((A \in ℝ \land B \in ℝ) \land (0 < A \land 0 < A B)) \to 0 < A B$
11		recgt0	$⊢ (A \in ℝ \land 0 < A) \to 0 < \frac{1}{A}$
12	11	ad2ant2r	$⊢ ((A \in ℝ \land B \in ℝ) \land (0 < A \land 0 < A B)) \to 0 < \frac{1}{A}$
13	6 9 10 12	mulgt0d	$⊢ ((A \in ℝ \land B \in ℝ) \land (0 < A \land 0 < A B)) \to 0 < A B (\frac{1}{A})$
14	6	recnd	$⊢ ((A \in ℝ \land B \in ℝ) \land (0 < A \land 0 < A B)) \to A B \in ℂ$
15	4	recnd	$⊢ ((A \in ℝ \land B \in ℝ) \land (0 < A \land 0 < A B)) \to A \in ℂ$
16	14 15 8	divrecd	$⊢ ((A \in ℝ \land B \in ℝ) \land (0 < A \land 0 < A B)) \to \frac{A B}{A} = A B (\frac{1}{A})$
17		simpr	$⊢ (A \in ℝ \land B \in ℝ) \to B \in ℝ$
18	17	recnd	$⊢ (A \in ℝ \land B \in ℝ) \to B \in ℂ$
19	18	adantr	$⊢ ((A \in ℝ \land B \in ℝ) \land (0 < A \land 0 < A B)) \to B \in ℂ$
20	19 15 8	divcan3d	$⊢ ((A \in ℝ \land B \in ℝ) \land (0 < A \land 0 < A B)) \to \frac{A B}{A} = B$
21	16 20	eqtr3d	$⊢ ((A \in ℝ \land B \in ℝ) \land (0 < A \land 0 < A B)) \to A B (\frac{1}{A}) = B$
22	13 21	breqtrd	$⊢ ((A \in ℝ \land B \in ℝ) \land (0 < A \land 0 < A B)) \to 0 < B$
23	22	exp32	$⊢ (A \in ℝ \land B \in ℝ) \to (0 < A \to (0 < A B \to 0 < B))$
24		0re	$⊢ 0 \in ℝ$
25	24	ltnri	$⊢ \neg 0 < 0$
26	18	mul02d	$⊢ (A \in ℝ \land B \in ℝ) \to 0 \cdot B = 0$
27	26	breq2d	$⊢ (A \in ℝ \land B \in ℝ) \to (0 < 0 \cdot B \leftrightarrow 0 < 0)$
28	25 27	mtbiri	$⊢ (A \in ℝ \land B \in ℝ) \to \neg 0 < 0 \cdot B$
29	28	pm2.21d	$⊢ (A \in ℝ \land B \in ℝ) \to (0 < 0 \cdot B \to 0 < B)$
30		oveq1	$⊢ 0 = A \to 0 \cdot B = A B$
31	30	breq2d	$⊢ 0 = A \to (0 < 0 \cdot B \leftrightarrow 0 < A B)$
32	31	imbi1d	$⊢ 0 = A \to ((0 < 0 \cdot B \to 0 < B) \leftrightarrow (0 < A B \to 0 < B))$
33	29 32	syl5ibcom	$⊢ (A \in ℝ \land B \in ℝ) \to (0 = A \to (0 < A B \to 0 < B))$
34	23 33	jaod	$⊢ (A \in ℝ \land B \in ℝ) \to ((0 < A \lor 0 = A) \to (0 < A B \to 0 < B))$
35	3 34	sylbid	$⊢ (A \in ℝ \land B \in ℝ) \to (0 \leq A \to (0 < A B \to 0 < B))$
36	35	imp32	$⊢ ((A \in ℝ \land B \in ℝ) \land (0 \leq A \land 0 < A B)) \to 0 < B$

Metamath Proof Explorer

Theorem prodgt0

Proof