Metamath Proof Explorer

Theorem resqrex

Description: Existence of a square root for positive reals. (Contributed by Mario Carneiro, 9-Jul-2013)

Ref Expression
Assertion resqrex 
|- ( ( A e. RR /\ 0 <_ A ) -> E. x e. RR ( 0 <_ x /\ ( x ^ 2 ) = A ) )

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 elrp 
 |-  ( A e. RR+ <-> ( A e. RR /\ 0 < A ) )
5 01sqrex 
 |-  ( ( A e. RR+ /\ A <_ 1 ) -> E. x e. RR+ ( x <_ 1 /\ ( x ^ 2 ) = A ) )
6 rprege0 
 |-  ( x e. RR+ -> ( x e. RR /\ 0 <_ x ) )
7 6 anim1i 
 |-  ( ( x e. RR+ /\ ( x ^ 2 ) = A ) -> ( ( x e. RR /\ 0 <_ x ) /\ ( x ^ 2 ) = A ) )
8 anass 
 |-  ( ( ( x e. RR /\ 0 <_ x ) /\ ( x ^ 2 ) = A ) <-> ( x e. RR /\ ( 0 <_ x /\ ( x ^ 2 ) = A ) ) )
9 7 8 sylib 
 |-  ( ( x e. RR+ /\ ( x ^ 2 ) = A ) -> ( x e. RR /\ ( 0 <_ x /\ ( x ^ 2 ) = A ) ) )
10 9 adantrl 
 |-  ( ( x e. RR+ /\ ( x <_ 1 /\ ( x ^ 2 ) = A ) ) -> ( x e. RR /\ ( 0 <_ x /\ ( x ^ 2 ) = A ) ) )
11 10 reximi2 
 |-  ( E. x e. RR+ ( x <_ 1 /\ ( x ^ 2 ) = A ) -> E. x e. RR ( 0 <_ x /\ ( x ^ 2 ) = A ) )
12 5 11 syl 
 |-  ( ( A e. RR+ /\ A <_ 1 ) -> E. x e. RR ( 0 <_ x /\ ( x ^ 2 ) = A ) )
13 4 12 sylanbr 
 |-  ( ( ( A e. RR /\ 0 < A ) /\ A <_ 1 ) -> E. x e. RR ( 0 <_ x /\ ( x ^ 2 ) = A ) )
14 13 exp31 
 |-  ( A e. RR -> ( 0 < A -> ( A <_ 1 -> E. x e. RR ( 0 <_ x /\ ( x ^ 2 ) = A ) ) ) )
15 sq0 
 |-  ( 0 ^ 2 ) = 0
16 id 
 |-  ( 0 = A -> 0 = A )
17 15 16 eqtrid 
 |-  ( 0 = A -> ( 0 ^ 2 ) = A )
18 0le0 
 |-  0 <_ 0
19 17 18 jctil 
 |-  ( 0 = A -> ( 0 <_ 0 /\ ( 0 ^ 2 ) = A ) )
20 breq2 
 |-  ( x = 0 -> ( 0 <_ x <-> 0 <_ 0 ) )
21 oveq1 
 |-  ( x = 0 -> ( x ^ 2 ) = ( 0 ^ 2 ) )
22 21 eqeq1d 
 |-  ( x = 0 -> ( ( x ^ 2 ) = A <-> ( 0 ^ 2 ) = A ) )
23 20 22 anbi12d 
 |-  ( x = 0 -> ( ( 0 <_ x /\ ( x ^ 2 ) = A ) <-> ( 0 <_ 0 /\ ( 0 ^ 2 ) = A ) ) )
24 23 rspcev 
 |-  ( ( 0 e. RR /\ ( 0 <_ 0 /\ ( 0 ^ 2 ) = A ) ) -> E. x e. RR ( 0 <_ x /\ ( x ^ 2 ) = A ) )
25 1 19 24 sylancr 
 |-  ( 0 = A -> E. x e. RR ( 0 <_ x /\ ( x ^ 2 ) = A ) )
26 25 a1i13 
 |-  ( A e. RR -> ( 0 = A -> ( A <_ 1 -> E. x e. RR ( 0 <_ x /\ ( x ^ 2 ) = A ) ) ) )
27 14 26 jaod 
 |-  ( A e. RR -> ( ( 0 < A \/ 0 = A ) -> ( A <_ 1 -> E. x e. RR ( 0 <_ x /\ ( x ^ 2 ) = A ) ) ) )
28 3 27 sylbid 
 |-  ( A e. RR -> ( 0 <_ A -> ( A <_ 1 -> E. x e. RR ( 0 <_ x /\ ( x ^ 2 ) = A ) ) ) )
29 28 imp 
 |-  ( ( A e. RR /\ 0 <_ A ) -> ( A <_ 1 -> E. x e. RR ( 0 <_ x /\ ( x ^ 2 ) = A ) ) )
30 0lt1 
 |-  0 < 1
31 1re 
 |-  1 e. RR
32 ltletr 
 |-  ( ( 0 e. RR /\ 1 e. RR /\ A e. RR ) -> ( ( 0 < 1 /\ 1 <_ A ) -> 0 < A ) )
33 1 31 32 mp3an12 
 |-  ( A e. RR -> ( ( 0 < 1 /\ 1 <_ A ) -> 0 < A ) )
34 30 33 mpani 
 |-  ( A e. RR -> ( 1 <_ A -> 0 < A ) )
35 34 imp 
 |-  ( ( A e. RR /\ 1 <_ A ) -> 0 < A )
36 4 biimpri 
 |-  ( ( A e. RR /\ 0 < A ) -> A e. RR+ )
37 35 36 syldan 
 |-  ( ( A e. RR /\ 1 <_ A ) -> A e. RR+ )
38 37 rpreccld 
 |-  ( ( A e. RR /\ 1 <_ A ) -> ( 1 / A ) e. RR+ )
39 simpr 
 |-  ( ( A e. RR /\ 1 <_ A ) -> 1 <_ A )
40 lerec 
 |-  ( ( ( 1 e. RR /\ 0 < 1 ) /\ ( A e. RR /\ 0 < A ) ) -> ( 1 <_ A <-> ( 1 / A ) <_ ( 1 / 1 ) ) )
41 31 30 40 mpanl12 
 |-  ( ( A e. RR /\ 0 < A ) -> ( 1 <_ A <-> ( 1 / A ) <_ ( 1 / 1 ) ) )
42 35 41 syldan 
 |-  ( ( A e. RR /\ 1 <_ A ) -> ( 1 <_ A <-> ( 1 / A ) <_ ( 1 / 1 ) ) )
43 39 42 mpbid 
 |-  ( ( A e. RR /\ 1 <_ A ) -> ( 1 / A ) <_ ( 1 / 1 ) )
44 1div1e1 
 |-  ( 1 / 1 ) = 1
45 43 44 breqtrdi 
 |-  ( ( A e. RR /\ 1 <_ A ) -> ( 1 / A ) <_ 1 )
46 01sqrex 
 |-  ( ( ( 1 / A ) e. RR+ /\ ( 1 / A ) <_ 1 ) -> E. y e. RR+ ( y <_ 1 /\ ( y ^ 2 ) = ( 1 / A ) ) )
47 38 45 46 syl2anc 
 |-  ( ( A e. RR /\ 1 <_ A ) -> E. y e. RR+ ( y <_ 1 /\ ( y ^ 2 ) = ( 1 / A ) ) )
48 rpre 
 |-  ( y e. RR+ -> y e. RR )
49 48 3ad2ant2 
 |-  ( ( ( A e. RR /\ 1 <_ A ) /\ y e. RR+ /\ ( y <_ 1 /\ ( y ^ 2 ) = ( 1 / A ) ) ) -> y e. RR )
50 rpgt0 
 |-  ( y e. RR+ -> 0 < y )
51 50 3ad2ant2 
 |-  ( ( ( A e. RR /\ 1 <_ A ) /\ y e. RR+ /\ ( y <_ 1 /\ ( y ^ 2 ) = ( 1 / A ) ) ) -> 0 < y )
52 gt0ne0 
 |-  ( ( y e. RR /\ 0 < y ) -> y =/= 0 )
53 rereccl 
 |-  ( ( y e. RR /\ y =/= 0 ) -> ( 1 / y ) e. RR )
54 52 53 syldan 
 |-  ( ( y e. RR /\ 0 < y ) -> ( 1 / y ) e. RR )
55 49 51 54 syl2anc 
 |-  ( ( ( A e. RR /\ 1 <_ A ) /\ y e. RR+ /\ ( y <_ 1 /\ ( y ^ 2 ) = ( 1 / A ) ) ) -> ( 1 / y ) e. RR )
56 recgt0 
 |-  ( ( y e. RR /\ 0 < y ) -> 0 < ( 1 / y ) )
57 ltle 
 |-  ( ( 0 e. RR /\ ( 1 / y ) e. RR ) -> ( 0 < ( 1 / y ) -> 0 <_ ( 1 / y ) ) )
58 1 57 mpan 
 |-  ( ( 1 / y ) e. RR -> ( 0 < ( 1 / y ) -> 0 <_ ( 1 / y ) ) )
59 54 56 58 sylc 
 |-  ( ( y e. RR /\ 0 < y ) -> 0 <_ ( 1 / y ) )
60 49 51 59 syl2anc 
 |-  ( ( ( A e. RR /\ 1 <_ A ) /\ y e. RR+ /\ ( y <_ 1 /\ ( y ^ 2 ) = ( 1 / A ) ) ) -> 0 <_ ( 1 / y ) )
61 recn 
 |-  ( y e. RR -> y e. CC )
62 61 adantr 
 |-  ( ( y e. RR /\ 0 < y ) -> y e. CC )
63 62 52 sqrecd 
 |-  ( ( y e. RR /\ 0 < y ) -> ( ( 1 / y ) ^ 2 ) = ( 1 / ( y ^ 2 ) ) )
64 49 51 63 syl2anc 
 |-  ( ( ( A e. RR /\ 1 <_ A ) /\ y e. RR+ /\ ( y <_ 1 /\ ( y ^ 2 ) = ( 1 / A ) ) ) -> ( ( 1 / y ) ^ 2 ) = ( 1 / ( y ^ 2 ) ) )
65 simp3r 
 |-  ( ( ( A e. RR /\ 1 <_ A ) /\ y e. RR+ /\ ( y <_ 1 /\ ( y ^ 2 ) = ( 1 / A ) ) ) -> ( y ^ 2 ) = ( 1 / A ) )
66 65 oveq2d 
 |-  ( ( ( A e. RR /\ 1 <_ A ) /\ y e. RR+ /\ ( y <_ 1 /\ ( y ^ 2 ) = ( 1 / A ) ) ) -> ( 1 / ( y ^ 2 ) ) = ( 1 / ( 1 / A ) ) )
67 recn 
 |-  ( A e. RR -> A e. CC )
68 gt0ne0 
 |-  ( ( A e. RR /\ 0 < A ) -> A =/= 0 )
69 35 68 syldan 
 |-  ( ( A e. RR /\ 1 <_ A ) -> A =/= 0 )
70 recrec 
 |-  ( ( A e. CC /\ A =/= 0 ) -> ( 1 / ( 1 / A ) ) = A )
71 67 69 70 syl2an2r 
 |-  ( ( A e. RR /\ 1 <_ A ) -> ( 1 / ( 1 / A ) ) = A )
72 71 3ad2ant1 
 |-  ( ( ( A e. RR /\ 1 <_ A ) /\ y e. RR+ /\ ( y <_ 1 /\ ( y ^ 2 ) = ( 1 / A ) ) ) -> ( 1 / ( 1 / A ) ) = A )
73 64 66 72 3eqtrd 
 |-  ( ( ( A e. RR /\ 1 <_ A ) /\ y e. RR+ /\ ( y <_ 1 /\ ( y ^ 2 ) = ( 1 / A ) ) ) -> ( ( 1 / y ) ^ 2 ) = A )
74 breq2 
 |-  ( x = ( 1 / y ) -> ( 0 <_ x <-> 0 <_ ( 1 / y ) ) )
75 oveq1 
 |-  ( x = ( 1 / y ) -> ( x ^ 2 ) = ( ( 1 / y ) ^ 2 ) )
76 75 eqeq1d 
 |-  ( x = ( 1 / y ) -> ( ( x ^ 2 ) = A <-> ( ( 1 / y ) ^ 2 ) = A ) )
77 74 76 anbi12d 
 |-  ( x = ( 1 / y ) -> ( ( 0 <_ x /\ ( x ^ 2 ) = A ) <-> ( 0 <_ ( 1 / y ) /\ ( ( 1 / y ) ^ 2 ) = A ) ) )
78 77 rspcev 
 |-  ( ( ( 1 / y ) e. RR /\ ( 0 <_ ( 1 / y ) /\ ( ( 1 / y ) ^ 2 ) = A ) ) -> E. x e. RR ( 0 <_ x /\ ( x ^ 2 ) = A ) )
79 55 60 73 78 syl12anc 
 |-  ( ( ( A e. RR /\ 1 <_ A ) /\ y e. RR+ /\ ( y <_ 1 /\ ( y ^ 2 ) = ( 1 / A ) ) ) -> E. x e. RR ( 0 <_ x /\ ( x ^ 2 ) = A ) )
80 79 rexlimdv3a 
 |-  ( ( A e. RR /\ 1 <_ A ) -> ( E. y e. RR+ ( y <_ 1 /\ ( y ^ 2 ) = ( 1 / A ) ) -> E. x e. RR ( 0 <_ x /\ ( x ^ 2 ) = A ) ) )
81 47 80 mpd 
 |-  ( ( A e. RR /\ 1 <_ A ) -> E. x e. RR ( 0 <_ x /\ ( x ^ 2 ) = A ) )
82 81 ex 
 |-  ( A e. RR -> ( 1 <_ A -> E. x e. RR ( 0 <_ x /\ ( x ^ 2 ) = A ) ) )
83 82 adantr 
 |-  ( ( A e. RR /\ 0 <_ A ) -> ( 1 <_ A -> E. x e. RR ( 0 <_ x /\ ( x ^ 2 ) = A ) ) )
84 simpl 
 |-  ( ( A e. RR /\ 0 <_ A ) -> A e. RR )
85 letric 
 |-  ( ( A e. RR /\ 1 e. RR ) -> ( A <_ 1 \/ 1 <_ A ) )
86 84 31 85 sylancl 
 |-  ( ( A e. RR /\ 0 <_ A ) -> ( A <_ 1 \/ 1 <_ A ) )
87 29 83 86 mpjaod 
 |-  ( ( A e. RR /\ 0 <_ A ) -> E. x e. RR ( 0 <_ x /\ ( x ^ 2 ) = A ) )