Metamath Proof Explorer

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 ) ≤ ( 𝐵 · 𝐴 ) ↔ 𝐴 ≤ 𝐵 ) )