Proof of Theorem sqreulem
Step | Hyp | Ref
| Expression |
1 | | sqrteulem.1 |
. . . . 5
                             |
2 | 1 | oveq1i 6318 |
. . . 4
                                     |
3 | | abscl 13418 |
. . . . . . . 8
       |
4 | | absge0 13427 |
. . . . . . . 8
       |
5 | | resqrtcl 13394 |
. . . . . . . 8
                     |
6 | 3, 4, 5 | syl2anc 673 |
. . . . . . 7
           |
7 | 6 | recnd 9687 |
. . . . . 6
           |
8 | 7 | adantr 472 |
. . . . 5
                   |
9 | 3 | recnd 9687 |
. . . . . . . 8
       |
10 | | addcl 9639 |
. . . . . . . 8
     
         |
11 | 9, 10 | mpancom 682 |
. . . . . . 7
         |
12 | 11 | adantr 472 |
. . . . . 6
                 |
13 | | abscl 13418 |
. . . . . . . . 9
                   |
14 | 11, 13 | syl 17 |
. . . . . . . 8
             |
15 | 14 | recnd 9687 |
. . . . . . 7
             |
16 | 15 | adantr 472 |
. . . . . 6
                     |
17 | 11 | abs00ad 13430 |
. . . . . . . 8
                     |
18 | 17 | necon3bid 2687 |
. . . . . . 7
                     |
19 | 18 | biimpar 493 |
. . . . . 6
                     |
20 | 12, 16, 19 | divcld 10405 |
. . . . 5
                             |
21 | 8, 20 | sqmuld 12466 |
. . . 4
                                                                               |
22 | 2, 21 | syl5eq 2517 |
. . 3
                                                   |
23 | 3 | adantr 472 |
. . . . 5
               |
24 | 4 | adantr 472 |
. . . . 5
        
      |
25 | | resqrtth 13396 |
. . . . 5
                             |
26 | 23, 24, 25 | syl2anc 673 |
. . . 4
                           |
27 | 12, 16, 19 | sqdivd 12467 |
. . . . 5
                                                           |
28 | | absvalsq 13420 |
. . . . . . . . . . 11
                 |
29 | | 2cn 10702 |
. . . . . . . . . . . . . 14
 |
30 | | mulass 9645 |
. . . . . . . . . . . . . 14
                         |
31 | 29, 30 | mp3an1 1377 |
. . . . . . . . . . . . 13
     
                   |
32 | 9, 31 | mpancom 682 |
. . . . . . . . . . . 12
                   |
33 | | mulcl 9641 |
. . . . . . . . . . . . . 14
               |
34 | 29, 9, 33 | sylancr 676 |
. . . . . . . . . . . . 13
         |
35 | | mulcom 9643 |
. . . . . . . . . . . . 13
                           |
36 | 34, 35 | mpancom 682 |
. . . . . . . . . . . 12
                   |
37 | 32, 36 | eqtr3d 2507 |
. . . . . . . . . . 11
                   |
38 | 28, 37 | oveq12d 6326 |
. . . . . . . . . 10
                                     |
39 | | cjcl 13245 |
. . . . . . . . . . 11
       |
40 | | adddi 9646 |
. . . . . . . . . . 11
                                             |
41 | 39, 34, 40 | mpd3an23 1392 |
. . . . . . . . . 10
 
                               |
42 | 38, 41 | eqtr4d 2508 |
. . . . . . . . 9
                                   |
43 | | sqval 12372 |
. . . . . . . . 9
         |
44 | 42, 43 | oveq12d 6326 |
. . . . . . . 8
                                             |
45 | | binom2 12427 |
. . . . . . . . 9
     
                                     |
46 | 9, 45 | mpancom 682 |
. . . . . . . 8
                                     |
47 | | id 22 |
. . . . . . . . 9
   |
48 | 39, 34 | addcld 9680 |
. . . . . . . . 9
               |
49 | 47, 48, 47 | adddid 9685 |
. . . . . . . 8
 
                                   |
50 | 44, 46, 49 | 3eqtr4d 2515 |
. . . . . . 7
                             |
51 | 9, 34 | mulcld 9681 |
. . . . . . . . . . 11
               |
52 | 9, 39 | mulcld 9681 |
. . . . . . . . . . 11
             |
53 | 51, 52 | addcomd 9853 |
. . . . . . . . . 10
                                                   |
54 | 9, 9 | mulcld 9681 |
. . . . . . . . . . . . 13
             |
55 | 54 | 2timesd 10878 |
. . . . . . . . . . . 12
                                     |
56 | | mul12 9817 |
. . . . . . . . . . . . . 14
                                     |
57 | 29, 56 | mp3an1 1377 |
. . . . . . . . . . . . 13
                                     |
58 | 9, 9, 57 | syl2anc 673 |
. . . . . . . . . . . 12
                           |
59 | 9 | sqvald 12451 |
. . . . . . . . . . . . . 14
                     |
60 | | mulcom 9643 |
. . . . . . . . . . . . . . 15
                     |
61 | 39, 60 | mpdan 681 |
. . . . . . . . . . . . . 14
 
             |
62 | 28, 59, 61 | 3eqtr3d 2513 |
. . . . . . . . . . . . 13
                   |
63 | 62 | oveq2d 6324 |
. . . . . . . . . . . 12
                                           |
64 | 55, 58, 63 | 3eqtr3rd 2514 |
. . . . . . . . . . 11
                                 |
65 | 64 | oveq1d 6323 |
. . . . . . . . . 10
                                                         |
66 | 9, 39, 34 | adddid 9685 |
. . . . . . . . . 10
                                             |
67 | 53, 65, 66 | 3eqtr4d 2515 |
. . . . . . . . 9
                                                   |
68 | 67 | oveq1d 6323 |
. . . . . . . 8
                                                                   |
69 | | cjadd 13281 |
. . . . . . . . . . . . 13
     
                           |
70 | 9, 69 | mpancom 682 |
. . . . . . . . . . . 12
                           |
71 | 3 | cjred 13366 |
. . . . . . . . . . . . 13
               |
72 | 71 | oveq1d 6323 |
. . . . . . . . . . . 12
                           |
73 | 70, 72 | eqtrd 2505 |
. . . . . . . . . . 11
                       |
74 | 73 | oveq2d 6324 |
. . . . . . . . . 10
                                       |
75 | 9, 47, 9, 39 | muladdd 10097 |
. . . . . . . . . 10
                                                           |
76 | 74, 75 | eqtrd 2505 |
. . . . . . . . 9
                                                           |
77 | | absvalsq 13420 |
. . . . . . . . . 10
                                         |
78 | 11, 77 | syl 17 |
. . . . . . . . 9
                                   |
79 | | mulcl 9641 |
. . . . . . . . . . . 12
     
         |
80 | 39, 79 | mpancom 682 |
. . . . . . . . . . 11
         |
81 | 54, 80 | addcld 9680 |
. . . . . . . . . 10
                     |
82 | | mulcl 9641 |
. . . . . . . . . . 11
     
         |
83 | 9, 82 | mpancom 682 |
. . . . . . . . . 10
         |
84 | 81, 52, 83 | addassd 9683 |
. . . . . . . . 9
                                                                               |
85 | 76, 78, 84 | 3eqtr4d 2515 |
. . . . . . . 8
                                                       |
86 | 9, 48, 47 | adddid 9685 |
. . . . . . . 8
                                                 |
87 | 68, 85, 86 | 3eqtr4d 2515 |
. . . . . . 7
                                     |
88 | 50, 87 | oveq12d 6326 |
. . . . . 6
                                                                   |
89 | 88 | adantr 472 |
. . . . 5
                                                                           |
90 | 27, 89 | eqtrd 2505 |
. . . 4
                                                                       |
91 | 26, 90 | oveq12d 6326 |
. . 3
                                                                                           |
92 | | addcl 9639 |
. . . . . . . 8
                               |
93 | 48, 92 | mpancom 682 |
. . . . . . 7
                 |
94 | 9, 47, 93 | mul12d 9860 |
. . . . . 6
                                               |
95 | 94 | oveq1d 6323 |
. . . . 5
                                                                                           |
96 | 95 | adantr 472 |
. . . 4
               
                                                                                   |
97 | 9 | adantr 472 |
. . . . 5
               |
98 | | mulcl 9641 |
. . . . . . 7
                                   |
99 | 93, 98 | mpdan 681 |
. . . . . 6
 
                 |
100 | 99 | adantr 472 |
. . . . 5
                           |
101 | 9, 93 | mulcld 9681 |
. . . . . 6
                       |
102 | 101 | adantr 472 |
. . . . 5
                               |
103 | | sqeq0 12377 |
. . . . . . . . 9
                         
             |
104 | 15, 103 | syl 17 |
. . . . . . . 8
               
             |
105 | 87 | eqeq1d 2473 |
. . . . . . . 8
               
                       |
106 | 104, 105,
17 | 3bitr3rd 292 |
. . . . . . 7
       
                       |
107 | 106 | necon3bid 2687 |
. . . . . 6
       
                       |
108 | 107 | biimpa 492 |
. . . . 5
                               |
109 | 97, 100, 102, 108 | divassd 10440 |
. . . 4
               
                                                                                   |
110 | | simpl 464 |
. . . . 5
        
  |
111 | 110, 102,
108 | divcan4d 10411 |
. . . 4
                                                       |
112 | 96, 109, 111 | 3eqtr3d 2513 |
. . 3
                                                       |
113 | 22, 91, 112 | 3eqtrd 2509 |
. 2
               |
114 | 6 | adantr 472 |
. . . . 5
                   |
115 | 11 | addcjd 13352 |
. . . . . . . 8
                                 |
116 | | 2re 10701 |
. . . . . . . . 9
 |
117 | 11 | recld 13334 |
. . . . . . . . 9
             |
118 | | remulcl 9642 |
. . . . . . . . 9
                           |
119 | 116, 117,
118 | sylancr 676 |
. . . . . . . 8
               |
120 | 115, 119 | eqeltrd 2549 |
. . . . . . 7
                     |
121 | 120 | adantr 472 |
. . . . . 6
                             |
122 | 14 | adantr 472 |
. . . . . 6
                     |
123 | 121, 122,
19 | redivcld 10457 |
. . . . 5
                                         |
124 | 114, 123 | remulcld 9689 |
. . . 4
                                                   |
125 | | sqrtge0 13398 |
. . . . . . 7
                     |
126 | 3, 4, 125 | syl2anc 673 |
. . . . . 6
           |
127 | 126 | adantr 472 |
. . . . 5
        
          |
128 | | negcl 9895 |
. . . . . . . . . . . 12
    |
129 | | releabs 13461 |
. . . . . . . . . . . 12
 
    
       |
130 | 128, 129 | syl 17 |
. . . . . . . . . . 11
             |
131 | | abscl 13418 |
. . . . . . . . . . . . 13
 
       |
132 | 128, 131 | syl 17 |
. . . . . . . . . . . 12
        |
133 | 128 | recld 13334 |
. . . . . . . . . . . 12
        |
134 | 132, 133 | subge0d 10224 |
. . . . . . . . . . 11
 
           
             |
135 | 130, 134 | mpbird 240 |
. . . . . . . . . 10
               |
136 | | readd 13266 |
. . . . . . . . . . . 12
     
                           |
137 | 9, 136 | mpancom 682 |
. . . . . . . . . . 11
                           |
138 | 3 | rered 13364 |
. . . . . . . . . . . . 13
               |
139 | | absneg 13417 |
. . . . . . . . . . . . 13
            |
140 | 138, 139 | eqtr4d 2508 |
. . . . . . . . . . . 12
                |
141 | | negneg 9944 |
. . . . . . . . . . . . . 14
     |
142 | 141 | fveq2d 5883 |
. . . . . . . . . . . . 13
             |
143 | 128 | renegd 13349 |
. . . . . . . . . . . . 13
               |
144 | 142, 143 | eqtr3d 2507 |
. . . . . . . . . . . 12
             |
145 | 140, 144 | oveq12d 6326 |
. . . . . . . . . . 11
                              |
146 | 132 | recnd 9687 |
. . . . . . . . . . . 12
        |
147 | 133 | recnd 9687 |
. . . . . . . . . . . 12
        |
148 | 146, 147 | negsubd 10011 |
. . . . . . . . . . 11
                            |
149 | 137, 145,
148 | 3eqtrd 2509 |
. . . . . . . . . 10
                         |
150 | 135, 149 | breqtrrd 4422 |
. . . . . . . . 9
             |
151 | | 0le2 10722 |
. . . . . . . . . 10
 |
152 | | mulge0 10153 |
. . . . . . . . . 10
  
           
           
              |
153 | 116, 151,
152 | mpanl12 696 |
. . . . . . . . 9
                                     |
154 | 117, 150,
153 | syl2anc 673 |
. . . . . . . 8
               |
155 | 154, 115 | breqtrrd 4422 |
. . . . . . 7
                     |
156 | 155 | adantr 472 |
. . . . . 6
        
                    |
157 | | absge0 13427 |
. . . . . . . 8
                   |
158 | 12, 157 | syl 17 |
. . . . . . 7
        
            |
159 | 122, 158,
19 | ne0gt0d 9789 |
. . . . . 6
        
            |
160 | | divge0 10496 |
. . . . . 6
                    
                                         
                                |
161 | 121, 156,
122, 159, 160 | syl22anc 1293 |
. . . . 5
        
                                |
162 | 114, 123,
127, 161 | mulge0d 10211 |
. . . 4
        
                                          |
163 | | 2pos 10723 |
. . . . 5
 |
164 | | divge0 10496 |
. . . . 5
                                                                                      
                                            |
165 | 116, 163,
164 | mpanr12 699 |
. . . 4
                                                                                  
                                            |
166 | 124, 162,
165 | syl2anc 673 |
. . 3
        
                                            |
167 | 8, 20 | mulcld 9681 |
. . . . . 6
                                       |
168 | 1, 167 | syl5eqel 2553 |
. . . . 5
        
  |
169 | | reval 13246 |
. . . . 5
               |
170 | 168, 169 | syl 17 |
. . . 4
                       |
171 | 1 | oveq1i 6318 |
. . . . . . 7
                                                                                                 |
172 | 1 | fveq2i 5882 |
. . . . . . . . . 10
                                     |
173 | 8, 20 | cjmuld 13361 |
. . . . . . . . . 10
                                                                               |
174 | 172, 173 | syl5eq 2517 |
. . . . . . . . 9
                                                   |
175 | 6 | cjred 13366 |
. . . . . . . . . . 11
                       |
176 | 175 | adantr 472 |
. . . . . . . . . 10
                               |
177 | 12, 16, 19 | cjdivd 13363 |
. . . . . . . . . . 11
                                                           |
178 | 122 | cjred 13366 |
. . . . . . . . . . . 12
                                   |
179 | 178 | oveq2d 6324 |
. . . . . . . . . . 11
                                                           |
180 | 177, 179 | eqtrd 2505 |
. . . . . . . . . 10
                                                       |
181 | 176, 180 | oveq12d 6326 |
. . . . . . . . 9
                                                                               |
182 | 174, 181 | eqtrd 2505 |
. . . . . . . 8
                                               |
183 | 182 | oveq2d 6324 |
. . . . . . 7
                                                   |
184 | 12 | cjcld 13336 |
. . . . . . . . 9
                     |
185 | 184, 16, 19 | divcld 10405 |
. . . . . . . 8
                                 |
186 | 8, 20, 185 | adddid 9685 |
. . . . . . 7
                                                                                                                             |
187 | 171, 183,
186 | 3eqtr4a 2531 |
. . . . . 6
                                                                     |
188 | 12, 184, 16, 19 | divdird 10443 |
. . . . . . 7
                                                                                   |
189 | 188 | oveq2d 6324 |
. . . . . 6
                                                                                                       |
190 | 187, 189 | eqtr4d 2508 |
. . . . 5
                                                         |
191 | 190 | oveq1d 6323 |
. . . 4
                                                             |
192 | 170, 191 | eqtrd 2505 |
. . 3
                                                         |
193 | 166, 192 | breqtrrd 4422 |
. 2
        
      |
194 | | subneg 9943 |
. . . . . . . . . 10
     
                |
195 | 9, 194 | mpancom 682 |
. . . . . . . . 9
                |
196 | 195 | eqeq1d 2473 |
. . . . . . . 8
                  |
197 | 9, 128 | subeq0ad 10015 |
. . . . . . . 8
                 |
198 | 196, 197 | bitr3d 263 |
. . . . . . 7
       
        |
199 | 198 | necon3bid 2687 |
. . . . . 6
       
        |
200 | 199 | biimpa 492 |
. . . . 5
                |
201 | | resqcl 12380 |
. . . . . . . . . 10
           |
202 | | ax-icn 9616 |
. . . . . . . . . . . . 13
 |
203 | | sqmul 12376 |
. . . . . . . . . . . . 13
 
                   |
204 | 202, 168,
203 | sylancr 676 |
. . . . . . . . . . . 12
                           |
205 | | i2 12413 |
. . . . . . . . . . . . . 14
      |
206 | 205 | a1i 11 |
. . . . . . . . . . . . 13
                |
207 | 206, 113 | oveq12d 6326 |
. . . . . . . . . . . 12
                        |
208 | | mulm1 10081 |
. . . . . . . . . . . . 13
       |
209 | 208 | adantr 472 |
. . . . . . . . . . . 12
               |
210 | 204, 207,
209 | 3eqtrd 2509 |
. . . . . . . . . . 11
                  |
211 | 210 | eleq1d 2533 |
. . . . . . . . . 10
                    |
212 | 201, 211 | syl5ib 227 |
. . . . . . . . 9
                |
213 | | renegcl 9957 |
. . . . . . . . . 10
 
    |
214 | 141 | eleq1d 2533 |
. . . . . . . . . 10
   
   |
215 | 213, 214 | syl5ib 227 |
. . . . . . . . 9
      |
216 | 110, 212,
215 | sylsyld 57 |
. . . . . . . 8
               |
217 | | sqge0 12389 |
. . . . . . . . . 10
           |
218 | 210 | breq2d 4407 |
. . . . . . . . . 10
               
    |
219 | 217, 218 | syl5ib 227 |
. . . . . . . . 9
           
    |
220 | | le0neg1 10143 |
. . . . . . . . . 10
 
    |
221 | 220 | biimprcd 233 |
. . . . . . . . 9
  
   |
222 | 219, 216,
221 | syl6c 65 |
. . . . . . . 8
           
   |
223 | 216, 222 | jcad 542 |
. . . . . . 7
            
    |
224 | | absnid 13438 |
. . . . . . 7
          |
225 | 223, 224 | syl6 33 |
. . . . . 6
                    |
226 | 225 | necon3ad 2656 |
. . . . 5
                    |
227 | 200, 226 | mpd 15 |
. . . 4
             |
228 | | rpre 11331 |
. . . 4
  
    |
229 | 227, 228 | nsyl 125 |
. . 3
             |
230 | | df-nel 2644 |
. . 3
  
    |
231 | 229, 230 | sylibr 217 |
. 2
          
  |
232 | 113, 193,
231 | 3jca 1210 |
1
                   
   |