sqlecan

Description: Cancel one factor of a square in a <_ comparison. Unlike lemul1 , the common factor A may be zero. (Contributed by NM, 17-Jan-2008)

		Ref	Expression
	Assertion	sqlecan	$⊢ ((A \in ℝ \land 0 \leq A) \land (B \in ℝ \land 0 \leq B)) \to (A^{2} \leq B A \leftrightarrow A \leq B)$

Proof

Step	Hyp	Ref	Expression
1		0re	$⊢ 0 \in ℝ$
2		leloe	$⊢ (0 \in ℝ \land A \in ℝ) \to (0 \leq A \leftrightarrow (0 < A \lor 0 = A))$
3	1 2	mpan	$⊢ A \in ℝ \to (0 \leq A \leftrightarrow (0 < A \lor 0 = A))$
4		recn	$⊢ A \in ℝ \to A \in ℂ$
5		sqval	$⊢ A \in ℂ \to A^{2} = A A$
6	4 5	syl	$⊢ A \in ℝ \to A^{2} = A A$
7	6	breq1d	$⊢ A \in ℝ \to (A^{2} \leq B A \leftrightarrow A A \leq B A)$
8	7	3ad2ant1	$⊢ (A \in ℝ \land B \in ℝ \land (A \in ℝ \land 0 < A)) \to (A^{2} \leq B A \leftrightarrow A A \leq B A)$
9		lemul1	$⊢ (A \in ℝ \land B \in ℝ \land (A \in ℝ \land 0 < A)) \to (A \leq B \leftrightarrow A A \leq B A)$
10	8 9	bitr4d	$⊢ (A \in ℝ \land B \in ℝ \land (A \in ℝ \land 0 < A)) \to (A^{2} \leq B A \leftrightarrow A \leq B)$
11	10	3exp	$⊢ A \in ℝ \to (B \in ℝ \to ((A \in ℝ \land 0 < A) \to (A^{2} \leq B A \leftrightarrow A \leq B)))$
12	11	exp4a	$⊢ A \in ℝ \to (B \in ℝ \to (A \in ℝ \to (0 < A \to (A^{2} \leq B A \leftrightarrow A \leq B))))$
13	12	pm2.43a	$⊢ A \in ℝ \to (B \in ℝ \to (0 < A \to (A^{2} \leq B A \leftrightarrow A \leq B)))$
14	13	adantrd	$⊢ A \in ℝ \to ((B \in ℝ \land 0 \leq B) \to (0 < A \to (A^{2} \leq B A \leftrightarrow A \leq B)))$
15	14	com23	$⊢ A \in ℝ \to (0 < A \to ((B \in ℝ \land 0 \leq B) \to (A^{2} \leq B A \leftrightarrow A \leq B)))$
16		sq0	$⊢ 0^{2} = 0$
17		0le0	$⊢ 0 \leq 0$
18	16 17	eqbrtri	$⊢ 0^{2} \leq 0$
19		recn	$⊢ B \in ℝ \to B \in ℂ$
20	19	mul01d	$⊢ B \in ℝ \to B \cdot 0 = 0$
21	18 20	breqtrrid	$⊢ B \in ℝ \to 0^{2} \leq B \cdot 0$
22	21	adantl	$⊢ (0 = A \land B \in ℝ) \to 0^{2} \leq B \cdot 0$
23		oveq1	$⊢ 0 = A \to 0^{2} = A^{2}$
24		oveq2	$⊢ 0 = A \to B \cdot 0 = B A$
25	23 24	breq12d	$⊢ 0 = A \to (0^{2} \leq B \cdot 0 \leftrightarrow A^{2} \leq B A)$
26	25	adantr	$⊢ (0 = A \land B \in ℝ) \to (0^{2} \leq B \cdot 0 \leftrightarrow A^{2} \leq B A)$
27	22 26	mpbid	$⊢ (0 = A \land B \in ℝ) \to A^{2} \leq B A$
28	27	adantrr	$⊢ (0 = A \land (B \in ℝ \land 0 \leq B)) \to A^{2} \leq B A$
29		breq1	$⊢ 0 = A \to (0 \leq B \leftrightarrow A \leq B)$
30	29	biimpa	$⊢ (0 = A \land 0 \leq B) \to A \leq B$
31	30	adantrl	$⊢ (0 = A \land (B \in ℝ \land 0 \leq B)) \to A \leq B$
32	28 31	2thd	$⊢ (0 = A \land (B \in ℝ \land 0 \leq B)) \to (A^{2} \leq B A \leftrightarrow A \leq B)$
33	32	ex	$⊢ 0 = A \to ((B \in ℝ \land 0 \leq B) \to (A^{2} \leq B A \leftrightarrow A \leq B))$
34	33	a1i	$⊢ A \in ℝ \to (0 = A \to ((B \in ℝ \land 0 \leq B) \to (A^{2} \leq B A \leftrightarrow A \leq B)))$
35	15 34	jaod	$⊢ A \in ℝ \to ((0 < A \lor 0 = A) \to ((B \in ℝ \land 0 \leq B) \to (A^{2} \leq B A \leftrightarrow A \leq B)))$
36	3 35	sylbid	$⊢ A \in ℝ \to (0 \leq A \to ((B \in ℝ \land 0 \leq B) \to (A^{2} \leq B A \leftrightarrow A \leq B)))$
37	36	imp31	$⊢ ((A \in ℝ \land 0 \leq A) \land (B \in ℝ \land 0 \leq B)) \to (A^{2} \leq B A \leftrightarrow A \leq B)$

Metamath Proof Explorer

Theorem sqlecan

Proof