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∈ℝ∧0≤A→∃x∈ℝ0≤x∧x2=A

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