Proof of Theorem sqreulem
Step | Hyp | Ref
| Expression |
1 | | sqrteulem.1 |
. . . . 5
|
2 | 1 | oveq1i 6660 |
. . . 4
|
3 | | abscl 14018 |
. . . . . . . 8
|
4 | | absge0 14027 |
. . . . . . . 8
|
5 | | resqrtcl 13994 |
. . . . . . . 8
|
6 | 3, 4, 5 | syl2anc 693 |
. . . . . . 7
|
7 | 6 | recnd 10068 |
. . . . . 6
|
8 | 7 | adantr 481 |
. . . . 5
|
9 | 3 | recnd 10068 |
. . . . . . . 8
|
10 | | addcl 10018 |
. . . . . . . 8
|
11 | 9, 10 | mpancom 703 |
. . . . . . 7
|
12 | 11 | adantr 481 |
. . . . . 6
|
13 | | abscl 14018 |
. . . . . . . . 9
|
14 | 11, 13 | syl 17 |
. . . . . . . 8
|
15 | 14 | recnd 10068 |
. . . . . . 7
|
16 | 15 | adantr 481 |
. . . . . 6
|
17 | 11 | abs00ad 14030 |
. . . . . . . 8
|
18 | 17 | necon3bid 2838 |
. . . . . . 7
|
19 | 18 | biimpar 502 |
. . . . . 6
|
20 | 12, 16, 19 | divcld 10801 |
. . . . 5
|
21 | 8, 20 | sqmuld 13020 |
. . . 4
|
22 | 2, 21 | syl5eq 2668 |
. . 3
|
23 | 3 | adantr 481 |
. . . . 5
|
24 | 4 | adantr 481 |
. . . . 5
|
25 | | resqrtth 13996 |
. . . . 5
|
26 | 23, 24, 25 | syl2anc 693 |
. . . 4
|
27 | 12, 16, 19 | sqdivd 13021 |
. . . . 5
|
28 | | absvalsq 14020 |
. . . . . . . . . . 11
|
29 | | 2cn 11091 |
. . . . . . . . . . . . . 14
|
30 | | mulass 10024 |
. . . . . . . . . . . . . 14
|
31 | 29, 30 | mp3an1 1411 |
. . . . . . . . . . . . 13
|
32 | 9, 31 | mpancom 703 |
. . . . . . . . . . . 12
|
33 | | mulcl 10020 |
. . . . . . . . . . . . . 14
|
34 | 29, 9, 33 | sylancr 695 |
. . . . . . . . . . . . 13
|
35 | | mulcom 10022 |
. . . . . . . . . . . . 13
|
36 | 34, 35 | mpancom 703 |
. . . . . . . . . . . 12
|
37 | 32, 36 | eqtr3d 2658 |
. . . . . . . . . . 11
|
38 | 28, 37 | oveq12d 6668 |
. . . . . . . . . 10
|
39 | | cjcl 13845 |
. . . . . . . . . . 11
|
40 | | adddi 10025 |
. . . . . . . . . . 11
|
41 | 39, 34, 40 | mpd3an23 1426 |
. . . . . . . . . 10
|
42 | 38, 41 | eqtr4d 2659 |
. . . . . . . . 9
|
43 | | sqval 12922 |
. . . . . . . . 9
|
44 | 42, 43 | oveq12d 6668 |
. . . . . . . 8
|
45 | | binom2 12979 |
. . . . . . . . 9
|
46 | 9, 45 | mpancom 703 |
. . . . . . . 8
|
47 | | id 22 |
. . . . . . . . 9
|
48 | 39, 34 | addcld 10059 |
. . . . . . . . 9
|
49 | 47, 48, 47 | adddid 10064 |
. . . . . . . 8
|
50 | 44, 46, 49 | 3eqtr4d 2666 |
. . . . . . 7
|
51 | 9, 34 | mulcld 10060 |
. . . . . . . . . . 11
|
52 | 9, 39 | mulcld 10060 |
. . . . . . . . . . 11
|
53 | 51, 52 | addcomd 10238 |
. . . . . . . . . 10
|
54 | 9, 9 | mulcld 10060 |
. . . . . . . . . . . . 13
|
55 | 54 | 2timesd 11275 |
. . . . . . . . . . . 12
|
56 | | mul12 10202 |
. . . . . . . . . . . . . 14
|
57 | 29, 56 | mp3an1 1411 |
. . . . . . . . . . . . 13
|
58 | 9, 9, 57 | syl2anc 693 |
. . . . . . . . . . . 12
|
59 | 9 | sqvald 13005 |
. . . . . . . . . . . . . 14
|
60 | | mulcom 10022 |
. . . . . . . . . . . . . . 15
|
61 | 39, 60 | mpdan 702 |
. . . . . . . . . . . . . 14
|
62 | 28, 59, 61 | 3eqtr3d 2664 |
. . . . . . . . . . . . 13
|
63 | 62 | oveq2d 6666 |
. . . . . . . . . . . 12
|
64 | 55, 58, 63 | 3eqtr3rd 2665 |
. . . . . . . . . . 11
|
65 | 64 | oveq1d 6665 |
. . . . . . . . . 10
|
66 | 9, 39, 34 | adddid 10064 |
. . . . . . . . . 10
|
67 | 53, 65, 66 | 3eqtr4d 2666 |
. . . . . . . . 9
|
68 | 67 | oveq1d 6665 |
. . . . . . . 8
|
69 | | cjadd 13881 |
. . . . . . . . . . . . 13
|
70 | 9, 69 | mpancom 703 |
. . . . . . . . . . . 12
|
71 | 3 | cjred 13966 |
. . . . . . . . . . . . 13
|
72 | 71 | oveq1d 6665 |
. . . . . . . . . . . 12
|
73 | 70, 72 | eqtrd 2656 |
. . . . . . . . . . 11
|
74 | 73 | oveq2d 6666 |
. . . . . . . . . 10
|
75 | 9, 47, 9, 39 | muladdd 10489 |
. . . . . . . . . 10
|
76 | 74, 75 | eqtrd 2656 |
. . . . . . . . 9
|
77 | | absvalsq 14020 |
. . . . . . . . . 10
|
78 | 11, 77 | syl 17 |
. . . . . . . . 9
|
79 | | mulcl 10020 |
. . . . . . . . . . . 12
|
80 | 39, 79 | mpancom 703 |
. . . . . . . . . . 11
|
81 | 54, 80 | addcld 10059 |
. . . . . . . . . 10
|
82 | | mulcl 10020 |
. . . . . . . . . . 11
|
83 | 9, 82 | mpancom 703 |
. . . . . . . . . 10
|
84 | 81, 52, 83 | addassd 10062 |
. . . . . . . . 9
|
85 | 76, 78, 84 | 3eqtr4d 2666 |
. . . . . . . 8
|
86 | 9, 48, 47 | adddid 10064 |
. . . . . . . 8
|
87 | 68, 85, 86 | 3eqtr4d 2666 |
. . . . . . 7
|
88 | 50, 87 | oveq12d 6668 |
. . . . . 6
|
89 | 88 | adantr 481 |
. . . . 5
|
90 | 27, 89 | eqtrd 2656 |
. . . 4
|
91 | 26, 90 | oveq12d 6668 |
. . 3
|
92 | | addcl 10018 |
. . . . . . . 8
|
93 | 48, 92 | mpancom 703 |
. . . . . . 7
|
94 | 9, 47, 93 | mul12d 10245 |
. . . . . 6
|
95 | 94 | oveq1d 6665 |
. . . . 5
|
96 | 95 | adantr 481 |
. . . 4
|
97 | 9 | adantr 481 |
. . . . 5
|
98 | | mulcl 10020 |
. . . . . . 7
|
99 | 93, 98 | mpdan 702 |
. . . . . 6
|
100 | 99 | adantr 481 |
. . . . 5
|
101 | 9, 93 | mulcld 10060 |
. . . . . 6
|
102 | 101 | adantr 481 |
. . . . 5
|
103 | | sqeq0 12927 |
. . . . . . . . 9
|
104 | 15, 103 | syl 17 |
. . . . . . . 8
|
105 | 87 | eqeq1d 2624 |
. . . . . . . 8
|
106 | 104, 105,
17 | 3bitr3rd 299 |
. . . . . . 7
|
107 | 106 | necon3bid 2838 |
. . . . . 6
|
108 | 107 | biimpa 501 |
. . . . 5
|
109 | 97, 100, 102, 108 | divassd 10836 |
. . . 4
|
110 | | simpl 473 |
. . . . 5
|
111 | 110, 102,
108 | divcan4d 10807 |
. . . 4
|
112 | 96, 109, 111 | 3eqtr3d 2664 |
. . 3
|
113 | 22, 91, 112 | 3eqtrd 2660 |
. 2
|
114 | 6 | adantr 481 |
. . . . 5
|
115 | 11 | addcjd 13952 |
. . . . . . . 8
|
116 | | 2re 11090 |
. . . . . . . . 9
|
117 | 11 | recld 13934 |
. . . . . . . . 9
|
118 | | remulcl 10021 |
. . . . . . . . 9
|
119 | 116, 117,
118 | sylancr 695 |
. . . . . . . 8
|
120 | 115, 119 | eqeltrd 2701 |
. . . . . . 7
|
121 | 120 | adantr 481 |
. . . . . 6
|
122 | 14 | adantr 481 |
. . . . . 6
|
123 | 121, 122,
19 | redivcld 10853 |
. . . . 5
|
124 | 114, 123 | remulcld 10070 |
. . . 4
|
125 | | sqrtge0 13998 |
. . . . . . 7
|
126 | 3, 4, 125 | syl2anc 693 |
. . . . . 6
|
127 | 126 | adantr 481 |
. . . . 5
|
128 | | negcl 10281 |
. . . . . . . . . . . 12
|
129 | | releabs 14061 |
. . . . . . . . . . . 12
|
130 | 128, 129 | syl 17 |
. . . . . . . . . . 11
|
131 | | abscl 14018 |
. . . . . . . . . . . . 13
|
132 | 128, 131 | syl 17 |
. . . . . . . . . . . 12
|
133 | 128 | recld 13934 |
. . . . . . . . . . . 12
|
134 | 132, 133 | subge0d 10617 |
. . . . . . . . . . 11
|
135 | 130, 134 | mpbird 247 |
. . . . . . . . . 10
|
136 | | readd 13866 |
. . . . . . . . . . . 12
|
137 | 9, 136 | mpancom 703 |
. . . . . . . . . . 11
|
138 | 3 | rered 13964 |
. . . . . . . . . . . . 13
|
139 | | absneg 14017 |
. . . . . . . . . . . . 13
|
140 | 138, 139 | eqtr4d 2659 |
. . . . . . . . . . . 12
|
141 | | negneg 10331 |
. . . . . . . . . . . . . 14
|
142 | 141 | fveq2d 6195 |
. . . . . . . . . . . . 13
|
143 | 128 | renegd 13949 |
. . . . . . . . . . . . 13
|
144 | 142, 143 | eqtr3d 2658 |
. . . . . . . . . . . 12
|
145 | 140, 144 | oveq12d 6668 |
. . . . . . . . . . 11
|
146 | 132 | recnd 10068 |
. . . . . . . . . . . 12
|
147 | 133 | recnd 10068 |
. . . . . . . . . . . 12
|
148 | 146, 147 | negsubd 10398 |
. . . . . . . . . . 11
|
149 | 137, 145,
148 | 3eqtrd 2660 |
. . . . . . . . . 10
|
150 | 135, 149 | breqtrrd 4681 |
. . . . . . . . 9
|
151 | | 0le2 11111 |
. . . . . . . . . 10
|
152 | | mulge0 10546 |
. . . . . . . . . 10
|
153 | 116, 151,
152 | mpanl12 718 |
. . . . . . . . 9
|
154 | 117, 150,
153 | syl2anc 693 |
. . . . . . . 8
|
155 | 154, 115 | breqtrrd 4681 |
. . . . . . 7
|
156 | 155 | adantr 481 |
. . . . . 6
|
157 | | absge0 14027 |
. . . . . . . 8
|
158 | 12, 157 | syl 17 |
. . . . . . 7
|
159 | 122, 158,
19 | ne0gt0d 10174 |
. . . . . 6
|
160 | | divge0 10892 |
. . . . . 6
|
161 | 121, 156,
122, 159, 160 | syl22anc 1327 |
. . . . 5
|
162 | 114, 123,
127, 161 | mulge0d 10604 |
. . . 4
|
163 | | 2pos 11112 |
. . . . 5
|
164 | | divge0 10892 |
. . . . 5
|
165 | 116, 163,
164 | mpanr12 721 |
. . . 4
|
166 | 124, 162,
165 | syl2anc 693 |
. . 3
|
167 | 8, 20 | mulcld 10060 |
. . . . . 6
|
168 | 1, 167 | syl5eqel 2705 |
. . . . 5
|
169 | | reval 13846 |
. . . . 5
|
170 | 168, 169 | syl 17 |
. . . 4
|
171 | 1 | oveq1i 6660 |
. . . . . . 7
|
172 | 1 | fveq2i 6194 |
. . . . . . . . . 10
|
173 | 8, 20 | cjmuld 13961 |
. . . . . . . . . 10
|
174 | 172, 173 | syl5eq 2668 |
. . . . . . . . 9
|
175 | 6 | cjred 13966 |
. . . . . . . . . . 11
|
176 | 175 | adantr 481 |
. . . . . . . . . 10
|
177 | 12, 16, 19 | cjdivd 13963 |
. . . . . . . . . . 11
|
178 | 122 | cjred 13966 |
. . . . . . . . . . . 12
|
179 | 178 | oveq2d 6666 |
. . . . . . . . . . 11
|
180 | 177, 179 | eqtrd 2656 |
. . . . . . . . . 10
|
181 | 176, 180 | oveq12d 6668 |
. . . . . . . . 9
|
182 | 174, 181 | eqtrd 2656 |
. . . . . . . 8
|
183 | 182 | oveq2d 6666 |
. . . . . . 7
|
184 | 12 | cjcld 13936 |
. . . . . . . . 9
|
185 | 184, 16, 19 | divcld 10801 |
. . . . . . . 8
|
186 | 8, 20, 185 | adddid 10064 |
. . . . . . 7
|
187 | 171, 183,
186 | 3eqtr4a 2682 |
. . . . . 6
|
188 | 12, 184, 16, 19 | divdird 10839 |
. . . . . . 7
|
189 | 188 | oveq2d 6666 |
. . . . . 6
|
190 | 187, 189 | eqtr4d 2659 |
. . . . 5
|
191 | 190 | oveq1d 6665 |
. . . 4
|
192 | 170, 191 | eqtrd 2656 |
. . 3
|
193 | 166, 192 | breqtrrd 4681 |
. 2
|
194 | | subneg 10330 |
. . . . . . . . . 10
|
195 | 9, 194 | mpancom 703 |
. . . . . . . . 9
|
196 | 195 | eqeq1d 2624 |
. . . . . . . 8
|
197 | 9, 128 | subeq0ad 10402 |
. . . . . . . 8
|
198 | 196, 197 | bitr3d 270 |
. . . . . . 7
|
199 | 198 | necon3bid 2838 |
. . . . . 6
|
200 | 199 | biimpa 501 |
. . . . 5
|
201 | | resqcl 12931 |
. . . . . . . . . 10
|
202 | | ax-icn 9995 |
. . . . . . . . . . . . 13
|
203 | | sqmul 12926 |
. . . . . . . . . . . . 13
|
204 | 202, 168,
203 | sylancr 695 |
. . . . . . . . . . . 12
|
205 | | i2 12965 |
. . . . . . . . . . . . . 14
|
206 | 205 | a1i 11 |
. . . . . . . . . . . . 13
|
207 | 206, 113 | oveq12d 6668 |
. . . . . . . . . . . 12
|
208 | | mulm1 10471 |
. . . . . . . . . . . . 13
|
209 | 208 | adantr 481 |
. . . . . . . . . . . 12
|
210 | 204, 207,
209 | 3eqtrd 2660 |
. . . . . . . . . . 11
|
211 | 210 | eleq1d 2686 |
. . . . . . . . . 10
|
212 | 201, 211 | syl5ib 234 |
. . . . . . . . 9
|
213 | | renegcl 10344 |
. . . . . . . . . 10
|
214 | 141 | eleq1d 2686 |
. . . . . . . . . 10
|
215 | 213, 214 | syl5ib 234 |
. . . . . . . . 9
|
216 | 110, 212,
215 | sylsyld 61 |
. . . . . . . 8
|
217 | | sqge0 12940 |
. . . . . . . . . 10
|
218 | 210 | breq2d 4665 |
. . . . . . . . . 10
|
219 | 217, 218 | syl5ib 234 |
. . . . . . . . 9
|
220 | | le0neg1 10536 |
. . . . . . . . . 10
|
221 | 220 | biimprcd 240 |
. . . . . . . . 9
|
222 | 219, 216,
221 | syl6c 70 |
. . . . . . . 8
|
223 | 216, 222 | jcad 555 |
. . . . . . 7
|
224 | | absnid 14038 |
. . . . . . 7
|
225 | 223, 224 | syl6 35 |
. . . . . 6
|
226 | 225 | necon3ad 2807 |
. . . . 5
|
227 | 200, 226 | mpd 15 |
. . . 4
|
228 | | rpre 11839 |
. . . 4
|
229 | 227, 228 | nsyl 135 |
. . 3
|
230 | | df-nel 2898 |
. . 3
|
231 | 229, 230 | sylibr 224 |
. 2
|
232 | 113, 193,
231 | 3jca 1242 |
1
|