Theorem 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	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 0 ≤ 𝐵 ) ) → ( ( 𝐴 ↑ 2 ) ≤ ( 𝐵 · 𝐴 ) ↔ 𝐴 ≤ 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		0re	⊢ 0 ∈ ℝ
2		leloe	⊢ ( ( 0 ∈ ℝ ∧ 𝐴 ∈ ℝ ) → ( 0 ≤ 𝐴 ↔ ( 0 < 𝐴 ∨ 0 = 𝐴 ) ) )
3	1 2	mpan	⊢ ( 𝐴 ∈ ℝ → ( 0 ≤ 𝐴 ↔ ( 0 < 𝐴 ∨ 0 = 𝐴 ) ) )
4		recn	⊢ ( 𝐴 ∈ ℝ → 𝐴 ∈ ℂ )
5		sqval	⊢ ( 𝐴 ∈ ℂ → ( 𝐴 ↑ 2 ) = ( 𝐴 · 𝐴 ) )
6	4 5	syl	⊢ ( 𝐴 ∈ ℝ → ( 𝐴 ↑ 2 ) = ( 𝐴 · 𝐴 ) )
7	6	breq1d	⊢ ( 𝐴 ∈ ℝ → ( ( 𝐴 ↑ 2 ) ≤ ( 𝐵 · 𝐴 ) ↔ ( 𝐴 · 𝐴 ) ≤ ( 𝐵 · 𝐴 ) ) )
8	7	3ad2ant1	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ ( 𝐴 ∈ ℝ ∧ 0 < 𝐴 ) ) → ( ( 𝐴 ↑ 2 ) ≤ ( 𝐵 · 𝐴 ) ↔ ( 𝐴 · 𝐴 ) ≤ ( 𝐵 · 𝐴 ) ) )
9		lemul1	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ ( 𝐴 ∈ ℝ ∧ 0 < 𝐴 ) ) → ( 𝐴 ≤ 𝐵 ↔ ( 𝐴 · 𝐴 ) ≤ ( 𝐵 · 𝐴 ) ) )
10	8 9	bitr4d	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ ( 𝐴 ∈ ℝ ∧ 0 < 𝐴 ) ) → ( ( 𝐴 ↑ 2 ) ≤ ( 𝐵 · 𝐴 ) ↔ 𝐴 ≤ 𝐵 ) )
11	10	3exp	⊢ ( 𝐴 ∈ ℝ → ( 𝐵 ∈ ℝ → ( ( 𝐴 ∈ ℝ ∧ 0 < 𝐴 ) → ( ( 𝐴 ↑ 2 ) ≤ ( 𝐵 · 𝐴 ) ↔ 𝐴 ≤ 𝐵 ) ) ) )
12	11	exp4a	⊢ ( 𝐴 ∈ ℝ → ( 𝐵 ∈ ℝ → ( 𝐴 ∈ ℝ → ( 0 < 𝐴 → ( ( 𝐴 ↑ 2 ) ≤ ( 𝐵 · 𝐴 ) ↔ 𝐴 ≤ 𝐵 ) ) ) ) )
13	12	pm2.43a	⊢ ( 𝐴 ∈ ℝ → ( 𝐵 ∈ ℝ → ( 0 < 𝐴 → ( ( 𝐴 ↑ 2 ) ≤ ( 𝐵 · 𝐴 ) ↔ 𝐴 ≤ 𝐵 ) ) ) )
14	13	adantrd	⊢ ( 𝐴 ∈ ℝ → ( ( 𝐵 ∈ ℝ ∧ 0 ≤ 𝐵 ) → ( 0 < 𝐴 → ( ( 𝐴 ↑ 2 ) ≤ ( 𝐵 · 𝐴 ) ↔ 𝐴 ≤ 𝐵 ) ) ) )
15	14	com23	⊢ ( 𝐴 ∈ ℝ → ( 0 < 𝐴 → ( ( 𝐵 ∈ ℝ ∧ 0 ≤ 𝐵 ) → ( ( 𝐴 ↑ 2 ) ≤ ( 𝐵 · 𝐴 ) ↔ 𝐴 ≤ 𝐵 ) ) ) )
16		sq0	⊢ ( 0 ↑ 2 ) = 0
17		0le0	⊢ 0 ≤ 0
18	16 17	eqbrtri	⊢ ( 0 ↑ 2 ) ≤ 0
19		recn	⊢ ( 𝐵 ∈ ℝ → 𝐵 ∈ ℂ )
20	19	mul01d	⊢ ( 𝐵 ∈ ℝ → ( 𝐵 · 0 ) = 0 )
21	18 20	breqtrrid	⊢ ( 𝐵 ∈ ℝ → ( 0 ↑ 2 ) ≤ ( 𝐵 · 0 ) )
22	21	adantl	⊢ ( ( 0 = 𝐴 ∧ 𝐵 ∈ ℝ ) → ( 0 ↑ 2 ) ≤ ( 𝐵 · 0 ) )
23		oveq1	⊢ ( 0 = 𝐴 → ( 0 ↑ 2 ) = ( 𝐴 ↑ 2 ) )
24		oveq2	⊢ ( 0 = 𝐴 → ( 𝐵 · 0 ) = ( 𝐵 · 𝐴 ) )
25	23 24	breq12d	⊢ ( 0 = 𝐴 → ( ( 0 ↑ 2 ) ≤ ( 𝐵 · 0 ) ↔ ( 𝐴 ↑ 2 ) ≤ ( 𝐵 · 𝐴 ) ) )
26	25	adantr	⊢ ( ( 0 = 𝐴 ∧ 𝐵 ∈ ℝ ) → ( ( 0 ↑ 2 ) ≤ ( 𝐵 · 0 ) ↔ ( 𝐴 ↑ 2 ) ≤ ( 𝐵 · 𝐴 ) ) )
27	22 26	mpbid	⊢ ( ( 0 = 𝐴 ∧ 𝐵 ∈ ℝ ) → ( 𝐴 ↑ 2 ) ≤ ( 𝐵 · 𝐴 ) )
28	27	adantrr	⊢ ( ( 0 = 𝐴 ∧ ( 𝐵 ∈ ℝ ∧ 0 ≤ 𝐵 ) ) → ( 𝐴 ↑ 2 ) ≤ ( 𝐵 · 𝐴 ) )
29		breq1	⊢ ( 0 = 𝐴 → ( 0 ≤ 𝐵 ↔ 𝐴 ≤ 𝐵 ) )
30	29	biimpa	⊢ ( ( 0 = 𝐴 ∧ 0 ≤ 𝐵 ) → 𝐴 ≤ 𝐵 )
31	30	adantrl	⊢ ( ( 0 = 𝐴 ∧ ( 𝐵 ∈ ℝ ∧ 0 ≤ 𝐵 ) ) → 𝐴 ≤ 𝐵 )
32	28 31	2thd	⊢ ( ( 0 = 𝐴 ∧ ( 𝐵 ∈ ℝ ∧ 0 ≤ 𝐵 ) ) → ( ( 𝐴 ↑ 2 ) ≤ ( 𝐵 · 𝐴 ) ↔ 𝐴 ≤ 𝐵 ) )
33	32	ex	⊢ ( 0 = 𝐴 → ( ( 𝐵 ∈ ℝ ∧ 0 ≤ 𝐵 ) → ( ( 𝐴 ↑ 2 ) ≤ ( 𝐵 · 𝐴 ) ↔ 𝐴 ≤ 𝐵 ) ) )
34	33	a1i	⊢ ( 𝐴 ∈ ℝ → ( 0 = 𝐴 → ( ( 𝐵 ∈ ℝ ∧ 0 ≤ 𝐵 ) → ( ( 𝐴 ↑ 2 ) ≤ ( 𝐵 · 𝐴 ) ↔ 𝐴 ≤ 𝐵 ) ) ) )
35	15 34	jaod	⊢ ( 𝐴 ∈ ℝ → ( ( 0 < 𝐴 ∨ 0 = 𝐴 ) → ( ( 𝐵 ∈ ℝ ∧ 0 ≤ 𝐵 ) → ( ( 𝐴 ↑ 2 ) ≤ ( 𝐵 · 𝐴 ) ↔ 𝐴 ≤ 𝐵 ) ) ) )
36	3 35	sylbid	⊢ ( 𝐴 ∈ ℝ → ( 0 ≤ 𝐴 → ( ( 𝐵 ∈ ℝ ∧ 0 ≤ 𝐵 ) → ( ( 𝐴 ↑ 2 ) ≤ ( 𝐵 · 𝐴 ) ↔ 𝐴 ≤ 𝐵 ) ) ) )
37	36	imp31	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 0 ≤ 𝐵 ) ) → ( ( 𝐴 ↑ 2 ) ≤ ( 𝐵 · 𝐴 ) ↔ 𝐴 ≤ 𝐵 ) )