Metamath Proof Explorer

Theorem sqrlearg

Description: The square compared with its argument. (Contributed by Glauco Siliprandi, 26-Jun-2021)

Ref Expression
Hypothesis sqrlearg.1 
|- ( ph -> A e. RR )
Assertion sqrlearg 
|- ( ph -> ( ( A ^ 2 ) <_ A <-> A e. ( 0 [,] 1 ) ) )

Proof

Step Hyp Ref Expression
1 sqrlearg.1 
 |-  ( ph -> A e. RR )
2 0re 
 |-  0 e. RR
3 2 a1i 
 |-  ( ( ph /\ ( A ^ 2 ) <_ A ) -> 0 e. RR )
4 simpr 
 |-  ( ( ph /\ -. A <_ 1 ) -> -. A <_ 1 )
5 1red 
 |-  ( ( ph /\ -. A <_ 1 ) -> 1 e. RR )
6 1 adantr 
 |-  ( ( ph /\ -. A <_ 1 ) -> A e. RR )
7 5 6 ltnled 
 |-  ( ( ph /\ -. A <_ 1 ) -> ( 1 < A <-> -. A <_ 1 ) )
8 4 7 mpbird 
 |-  ( ( ph /\ -. A <_ 1 ) -> 1 < A )
9 1red 
 |-  ( ( ph /\ 1 < A ) -> 1 e. RR )
10 1 adantr 
 |-  ( ( ph /\ 1 < A ) -> A e. RR )
11 2 a1i 
 |-  ( ( ph /\ 1 < A ) -> 0 e. RR )
12 0lt1 
 |-  0 < 1
13 12 a1i 
 |-  ( ( ph /\ 1 < A ) -> 0 < 1 )
14 simpr 
 |-  ( ( ph /\ 1 < A ) -> 1 < A )
15 11 9 10 13 14 lttrd 
 |-  ( ( ph /\ 1 < A ) -> 0 < A )
16 10 15 elrpd 
 |-  ( ( ph /\ 1 < A ) -> A e. RR+ )
17 9 10 16 14 ltmul2dd 
 |-  ( ( ph /\ 1 < A ) -> ( A x. 1 ) < ( A x. A ) )
18 1 recnd 
 |-  ( ph -> A e. CC )
19 18 mulid1d 
 |-  ( ph -> ( A x. 1 ) = A )
20 19 adantr 
 |-  ( ( ph /\ 1 < A ) -> ( A x. 1 ) = A )
21 18 sqvald 
 |-  ( ph -> ( A ^ 2 ) = ( A x. A ) )
22 21 eqcomd 
 |-  ( ph -> ( A x. A ) = ( A ^ 2 ) )
23 22 adantr 
 |-  ( ( ph /\ 1 < A ) -> ( A x. A ) = ( A ^ 2 ) )
24 20 23 breq12d 
 |-  ( ( ph /\ 1 < A ) -> ( ( A x. 1 ) < ( A x. A ) <-> A < ( A ^ 2 ) ) )
25 17 24 mpbid 
 |-  ( ( ph /\ 1 < A ) -> A < ( A ^ 2 ) )
26 8 25 syldan 
 |-  ( ( ph /\ -. A <_ 1 ) -> A < ( A ^ 2 ) )
27 26 adantlr 
 |-  ( ( ( ph /\ ( A ^ 2 ) <_ A ) /\ -. A <_ 1 ) -> A < ( A ^ 2 ) )
28 simpr 
 |-  ( ( ph /\ ( A ^ 2 ) <_ A ) -> ( A ^ 2 ) <_ A )
29 1 resqcld 
 |-  ( ph -> ( A ^ 2 ) e. RR )
30 29 adantr 
 |-  ( ( ph /\ ( A ^ 2 ) <_ A ) -> ( A ^ 2 ) e. RR )
31 1 adantr 
 |-  ( ( ph /\ ( A ^ 2 ) <_ A ) -> A e. RR )
32 30 31 lenltd 
 |-  ( ( ph /\ ( A ^ 2 ) <_ A ) -> ( ( A ^ 2 ) <_ A <-> -. A < ( A ^ 2 ) ) )
33 28 32 mpbid 
 |-  ( ( ph /\ ( A ^ 2 ) <_ A ) -> -. A < ( A ^ 2 ) )
34 33 adantr 
 |-  ( ( ( ph /\ ( A ^ 2 ) <_ A ) /\ -. A <_ 1 ) -> -. A < ( A ^ 2 ) )
35 27 34 condan 
 |-  ( ( ph /\ ( A ^ 2 ) <_ A ) -> A <_ 1 )
36 1red 
 |-  ( ( ph /\ A <_ 1 ) -> 1 e. RR )
37 35 36 syldan 
 |-  ( ( ph /\ ( A ^ 2 ) <_ A ) -> 1 e. RR )
38 31 sqge0d 
 |-  ( ( ph /\ ( A ^ 2 ) <_ A ) -> 0 <_ ( A ^ 2 ) )
39 3 30 31 38 28 letrd 
 |-  ( ( ph /\ ( A ^ 2 ) <_ A ) -> 0 <_ A )
40 3 37 31 39 35 eliccd 
 |-  ( ( ph /\ ( A ^ 2 ) <_ A ) -> A e. ( 0 [,] 1 ) )
41 40 ex 
 |-  ( ph -> ( ( A ^ 2 ) <_ A -> A e. ( 0 [,] 1 ) ) )
42 unitssre 
 |-  ( 0 [,] 1 ) C_ RR
43 42 sseli 
 |-  ( A e. ( 0 [,] 1 ) -> A e. RR )
44 1red 
 |-  ( A e. ( 0 [,] 1 ) -> 1 e. RR )
45 0xr 
 |-  0 e. RR*
46 45 a1i 
 |-  ( A e. ( 0 [,] 1 ) -> 0 e. RR* )
47 44 rexrd 
 |-  ( A e. ( 0 [,] 1 ) -> 1 e. RR* )
48 id 
 |-  ( A e. ( 0 [,] 1 ) -> A e. ( 0 [,] 1 ) )
49 46 47 48 iccgelbd 
 |-  ( A e. ( 0 [,] 1 ) -> 0 <_ A )
50 46 47 48 iccleubd 
 |-  ( A e. ( 0 [,] 1 ) -> A <_ 1 )
51 43 44 43 49 50 lemul2ad 
 |-  ( A e. ( 0 [,] 1 ) -> ( A x. A ) <_ ( A x. 1 ) )
52 51 adantl 
 |-  ( ( ph /\ A e. ( 0 [,] 1 ) ) -> ( A x. A ) <_ ( A x. 1 ) )
53 22 adantr 
 |-  ( ( ph /\ A e. ( 0 [,] 1 ) ) -> ( A x. A ) = ( A ^ 2 ) )
54 19 adantr 
 |-  ( ( ph /\ A e. ( 0 [,] 1 ) ) -> ( A x. 1 ) = A )
55 53 54 breq12d 
 |-  ( ( ph /\ A e. ( 0 [,] 1 ) ) -> ( ( A x. A ) <_ ( A x. 1 ) <-> ( A ^ 2 ) <_ A ) )
56 52 55 mpbid 
 |-  ( ( ph /\ A e. ( 0 [,] 1 ) ) -> ( A ^ 2 ) <_ A )
57 56 ex 
 |-  ( ph -> ( A e. ( 0 [,] 1 ) -> ( A ^ 2 ) <_ A ) )
58 41 57 impbid 
 |-  ( ph -> ( ( A ^ 2 ) <_ A <-> A e. ( 0 [,] 1 ) ) )