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