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 e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 <_ B ) ) -> ( ( A ^ 2 ) <_ ( B x. A ) <-> A <_ B ) )

Proof

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