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 ⊢A∈ℝ∧0≤A∧B∈ℝ∧0≤B→A2≤B⁢A↔A≤B

Proof

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