Proof of Theorem mcubic
Step | Hyp | Ref
| Expression |
1 | | mcubic.m |
. . . . . 6
           |
2 | | mcubic.b |
. . . . . . . 8
   |
3 | 2 | sqcld 12411 |
. . . . . . 7
       |
4 | | 3cn 10681 |
. . . . . . . 8
 |
5 | | mcubic.c |
. . . . . . . 8
   |
6 | | mulcl 9620 |
. . . . . . . 8
 
     |
7 | 4, 5, 6 | sylancr 668 |
. . . . . . 7
     |
8 | 3, 7 | subcld 9983 |
. . . . . 6
           |
9 | 1, 8 | eqeltrd 2528 |
. . . . 5
   |
10 | 4 | a1i 11 |
. . . . 5
   |
11 | | 3ne0 10701 |
. . . . . 6
 |
12 | 11 | a1i 11 |
. . . . 5
   |
13 | 9, 10, 12 | divcld 10380 |
. . . 4
     |
14 | 13 | negcld 9970 |
. . 3
      |
15 | | mcubic.n |
. . . . 5
              ;     |
16 | | 2cn 10677 |
. . . . . . . 8
 |
17 | | 3nn0 10884 |
. . . . . . . . 9
 |
18 | | expcl 12287 |
. . . . . . . . 9
 
       |
19 | 2, 17, 18 | sylancl 667 |
. . . . . . . 8
       |
20 | | mulcl 9620 |
. . . . . . . 8
               |
21 | 16, 19, 20 | sylancr 668 |
. . . . . . 7
         |
22 | | 9cn 10694 |
. . . . . . . 8
 |
23 | 2, 5 | mulcld 9660 |
. . . . . . . 8
     |
24 | | mulcl 9620 |
. . . . . . . 8
  
        |
25 | 22, 23, 24 | sylancr 668 |
. . . . . . 7
  
    |
26 | 21, 25 | subcld 9983 |
. . . . . 6
               |
27 | | 2nn0 10883 |
. . . . . . . . 9
 |
28 | | 7nn 10769 |
. . . . . . . . 9
 |
29 | 27, 28 | decnncl 11061 |
. . . . . . . 8
;  |
30 | 29 | nncni 10616 |
. . . . . . 7
;  |
31 | | mcubic.d |
. . . . . . 7
   |
32 | | mulcl 9620 |
. . . . . . 7
 ;
 ;    |
33 | 30, 31, 32 | sylancr 668 |
. . . . . 6
 ;    |
34 | 26, 33 | addcld 9659 |
. . . . 5
          
   ;     |
35 | 15, 34 | eqeltrd 2528 |
. . . 4
   |
36 | 30 | a1i 11 |
. . . 4
 ;   |
37 | 29 | nnne0i 10641 |
. . . . 5
;  |
38 | 37 | a1i 11 |
. . . 4
 ;   |
39 | 35, 36, 38 | divcld 10380 |
. . 3
  ;    |
40 | | mcubic.x |
. . . 4
   |
41 | 2, 10, 12 | divcld 10380 |
. . . 4
     |
42 | 40, 41 | addcld 9659 |
. . 3
       |
43 | | mcubic.t |
. . . . 5
   |
44 | 43, 10, 12 | divcld 10380 |
. . . 4
     |
45 | 44 | negcld 9970 |
. . 3
      |
46 | | 3nn 10765 |
. . . . . 6
 |
47 | 46 | a1i 11 |
. . . . 5
   |
48 | | 2nn 10764 |
. . . . . . 7
 |
49 | | 1nn0 10882 |
. . . . . . 7
 |
50 | | 1nn 10617 |
. . . . . . 7
 |
51 | | 2t1e2 10755 |
. . . . . . . . 9
   |
52 | 51 | oveq1i 6298 |
. . . . . . . 8
       |
53 | | 2p1e3 10730 |
. . . . . . . 8
   |
54 | 52, 53 | eqtri 2472 |
. . . . . . 7
     |
55 | | 1lt2 10773 |
. . . . . . 7
 |
56 | 48, 49, 50, 54, 55 | ndvdsi 14384 |
. . . . . 6
 |
57 | 56 | a1i 11 |
. . . . 5
   |
58 | | oexpneg 14361 |
. . . . 5
   
                 |
59 | 44, 47, 57, 58 | syl3anc 1267 |
. . . 4
                 |
60 | 17 | a1i 11 |
. . . . . . 7
   |
61 | 43, 10, 12, 60 | expdivd 12427 |
. . . . . 6
                   |
62 | | mcubic.3 |
. . . . . . 7
           |
63 | | 3exp3 15055 |
. . . . . . . 8
    ;  |
64 | 63 | a1i 11 |
. . . . . . 7
     ;   |
65 | 62, 64 | oveq12d 6306 |
. . . . . 6
                ;    |
66 | | mcubic.g |
. . . . . . . . 9
   |
67 | 35, 66 | addcld 9659 |
. . . . . . . 8
     |
68 | | 2cnd 10679 |
. . . . . . . 8
   |
69 | | 2ne0 10699 |
. . . . . . . . 9
 |
70 | 69 | a1i 11 |
. . . . . . . 8
   |
71 | 67, 68, 36, 70, 38 | divdiv32d 10405 |
. . . . . . 7
      ;      ;     |
72 | 35, 66 | addcomd 9832 |
. . . . . . . . . 10
       |
73 | 72 | oveq1d 6303 |
. . . . . . . . 9
    ;     ;    |
74 | 66, 35, 36, 38 | divdird 10418 |
. . . . . . . . 9
    ;    ;   ;     |
75 | 73, 74 | eqtrd 2484 |
. . . . . . . 8
    ;    ;   ;     |
76 | 75 | oveq1d 6303 |
. . . . . . 7
     ;      ;   ;      |
77 | 66, 36, 38 | divcld 10380 |
. . . . . . . 8
  ;    |
78 | 77, 39, 68, 70 | divdird 10418 |
. . . . . . 7
    ;   ;       ;     ;      |
79 | 71, 76, 78 | 3eqtrd 2488 |
. . . . . 6
      ;     ;     ;      |
80 | 61, 65, 79 | 3eqtrd 2488 |
. . . . 5
          ;     ;      |
81 | 80 | negeqd 9866 |
. . . 4
            ;     ;      |
82 | 77 | halfcld 10854 |
. . . . 5
   ;     |
83 | 39 | halfcld 10854 |
. . . . 5
   ;     |
84 | 82, 83 | negdi2d 9997 |
. . . 4
     ;     ;        ;     ;      |
85 | 59, 81, 84 | 3eqtrd 2488 |
. . 3
            ;     ;      |
86 | 82 | negcld 9970 |
. . 3
    ;     |
87 | | sqneg 12332 |
. . . . 5
   ;       ;         ;        |
88 | 82, 87 | syl 17 |
. . . 4
     ;         ;        |
89 | 77, 68, 70 | sqdivd 12426 |
. . . 4
    ;         ;            |
90 | 39, 68, 70 | sqdivd 12426 |
. . . . . . . 8
    ;         ;            |
91 | 35, 36, 38 | sqdivd 12426 |
. . . . . . . . 9
   ;          ;       |
92 | 91 | oveq1d 6303 |
. . . . . . . 8
    ;                ;            |
93 | 90, 92 | eqtr2d 2485 |
. . . . . . 7
       ;             ;        |
94 | | 4cn 10684 |
. . . . . . . . . . . 12
 |
95 | 94 | a1i 11 |
. . . . . . . . . . 11
   |
96 | | expcl 12287 |
. . . . . . . . . . . 12
 
       |
97 | 9, 17, 96 | sylancl 667 |
. . . . . . . . . . 11
       |
98 | 30 | sqcli 12352 |
. . . . . . . . . . . 12
;     |
99 | 98 | a1i 11 |
. . . . . . . . . . 11
 ;      |
100 | | sqne0 12338 |
. . . . . . . . . . . . 13
;  ;    ;    |
101 | 36, 100 | syl 17 |
. . . . . . . . . . . 12
  ;    ;    |
102 | 38, 101 | mpbird 236 |
. . . . . . . . . . 11
 ;      |
103 | 95, 97, 99, 102 | divassd 10415 |
. . . . . . . . . 10
        ;           ;        |
104 | 22 | a1i 11 |
. . . . . . . . . . . . 13
   |
105 | | 9nn 10771 |
. . . . . . . . . . . . . . 15
 |
106 | 105 | nnne0i 10641 |
. . . . . . . . . . . . . 14
 |
107 | 106 | a1i 11 |
. . . . . . . . . . . . 13
   |
108 | 9, 104, 107, 60 | expdivd 12427 |
. . . . . . . . . . . 12
                   |
109 | 16, 4 | mulcomi 9646 |
. . . . . . . . . . . . . . . 16
     |
110 | 109 | oveq2i 6299 |
. . . . . . . . . . . . . . 15
             |
111 | | expmul 12314 |
. . . . . . . . . . . . . . . 16
 
                 |
112 | 4, 27, 17, 111 | mp3an 1363 |
. . . . . . . . . . . . . . 15
               |
113 | | expmul 12314 |
. . . . . . . . . . . . . . . 16
 
                 |
114 | 4, 17, 27, 113 | mp3an 1363 |
. . . . . . . . . . . . . . 15
               |
115 | 110, 112,
114 | 3eqtr3i 2480 |
. . . . . . . . . . . . . 14
                 |
116 | | sq3 12369 |
. . . . . . . . . . . . . . 15
     |
117 | 116 | oveq1i 6298 |
. . . . . . . . . . . . . 14
             |
118 | 63 | oveq1i 6298 |
. . . . . . . . . . . . . 14
        ;     |
119 | 115, 117,
118 | 3eqtr3i 2480 |
. . . . . . . . . . . . 13
    ;     |
120 | 119 | oveq2i 6299 |
. . . . . . . . . . . 12
               ;      |
121 | 108, 120 | syl6eq 2500 |
. . . . . . . . . . 11
            ;       |
122 | 121 | oveq2d 6304 |
. . . . . . . . . 10
               ;        |
123 | 103, 122 | eqtr4d 2487 |
. . . . . . . . 9
        ;               |
124 | 123 | oveq1d 6303 |
. . . . . . . 8
         ;                          |
125 | | sq2 12368 |
. . . . . . . . . 10
     |
126 | 125 | oveq2i 6299 |
. . . . . . . . 9
                         |
127 | 9, 104, 107 | divcld 10380 |
. . . . . . . . . . 11
     |
128 | | expcl 12287 |
. . . . . . . . . . 11
   
         |
129 | 127, 17, 128 | sylancl 667 |
. . . . . . . . . 10
         |
130 | | 4ne0 10703 |
. . . . . . . . . . 11
 |
131 | 130 | a1i 11 |
. . . . . . . . . 10
   |
132 | 129, 95, 131 | divcan3d 10385 |
. . . . . . . . 9
                   |
133 | 126, 132 | syl5eq 2496 |
. . . . . . . 8
                       |
134 | 124, 133 | eqtrd 2484 |
. . . . . . 7
         ;                  |
135 | 93, 134 | oveq12d 6306 |
. . . . . 6
        ;                  ;               ;               |
136 | 35 | sqcld 12411 |
. . . . . . . 8
       |
137 | 136, 99, 102 | divcld 10380 |
. . . . . . 7
      ;       |
138 | | mulcl 9620 |
. . . . . . . . 9
               |
139 | 94, 97, 138 | sylancr 668 |
. . . . . . . 8
         |
140 | 139, 99, 102 | divcld 10380 |
. . . . . . 7
        ;       |
141 | 16 | sqcli 12352 |
. . . . . . . 8
     |
142 | 141 | a1i 11 |
. . . . . . 7
       |
143 | 125, 130 | eqnetri 2693 |
. . . . . . . 8
     |
144 | 143 | a1i 11 |
. . . . . . 7
       |
145 | 137, 140,
142, 144 | divsubdird 10419 |
. . . . . 6
        ;            ;                  ;                  ;             |
146 | 83 | sqcld 12411 |
. . . . . . 7
    ;        |
147 | 146, 129 | negsubd 9989 |
. . . . . 6
     ;                  ;               |
148 | 135, 145,
147 | 3eqtr4d 2494 |
. . . . 5
        ;            ;               ;                |
149 | 66, 36, 38 | sqdivd 12426 |
. . . . . . 7
   ;          ;       |
150 | | mcubic.2 |
. . . . . . . 8
                   |
151 | 150 | oveq1d 6303 |
. . . . . . 7
      ;                  ;       |
152 | 136, 139,
99, 102 | divsubdird 10419 |
. . . . . . 7
              ;           ;            ;        |
153 | 149, 151,
152 | 3eqtrd 2488 |
. . . . . 6
   ;           ;            ;        |
154 | 153 | oveq1d 6303 |
. . . . 5
    ;                 ;            ;             |
155 | | oexpneg 14361 |
. . . . . . 7
   
                 |
156 | 127, 47, 57, 155 | syl3anc 1267 |
. . . . . 6
                 |
157 | 156 | oveq2d 6304 |
. . . . 5
     ;        
         ;                |
158 | 148, 154,
157 | 3eqtr4d 2494 |
. . . 4
    ;              ;                |
159 | 88, 89, 158 | 3eqtrd 2488 |
. . 3
     ;          ;                |
160 | 9, 10, 10, 12, 12 | divdiv1d 10411 |
. . . . . 6
           |
161 | | 3t3e9 10759 |
. . . . . . 7
   |
162 | 161 | oveq2i 6299 |
. . . . . 6
       |
163 | 160, 162 | syl6eq 2500 |
. . . . 5
         |
164 | 163 | negeqd 9866 |
. . . 4
       
   |
165 | 13, 10, 12 | divnegd 10393 |
. . . 4
             |
166 | 164, 165 | eqtr3d 2486 |
. . 3
           |
167 | | eqidd 2451 |
. . 3
   ;     ;     |
168 | | mcubic.0 |
. . . . 5
   |
169 | 43, 10, 168, 12 | divne0d 10396 |
. . . 4
     |
170 | 44, 169 | negne0d 9981 |
. . 3
      |
171 | 14, 39, 42, 45, 85, 86, 159, 166, 167, 170 | dcubic 23765 |
. 2
                      ;    
                              |
172 | | binom3 12390 |
. . . . . . 7
  
                                                |
173 | 40, 41, 172 | syl2anc 666 |
. . . . . 6
   
                                           |
174 | 40 | sqcld 12411 |
. . . . . . . . . 10
       |
175 | 10, 174, 41 | mul12d 9839 |
. . . . . . . . 9
                       |
176 | 2, 10, 12 | divcan2d 10382 |
. . . . . . . . . 10
       |
177 | 176 | oveq2d 6304 |
. . . . . . . . 9
                   |
178 | 174, 2 | mulcomd 9661 |
. . . . . . . . 9
               |
179 | 175, 177,
178 | 3eqtrd 2488 |
. . . . . . . 8
                   |
180 | 179 | oveq2d 6304 |
. . . . . . 7
                               |
181 | 180 | oveq1d 6303 |
. . . . . 6
                    
                               
                  |
182 | 173, 181 | eqtrd 2484 |
. . . . 5
   
                                       |
183 | 182 | oveq1d 6303 |
. . . 4
                     ;                                        
       ;      |
184 | | expcl 12287 |
. . . . . . 7
 
       |
185 | 40, 17, 184 | sylancl 667 |
. . . . . 6
       |
186 | 2, 174 | mulcld 9660 |
. . . . . 6
         |
187 | 185, 186 | addcld 9659 |
. . . . 5
               |
188 | 41 | sqcld 12411 |
. . . . . . . 8
         |
189 | 40, 188 | mulcld 9660 |
. . . . . . 7
           |
190 | 10, 189 | mulcld 9660 |
. . . . . 6
  
          |
191 | | expcl 12287 |
. . . . . . 7
   
         |
192 | 41, 17, 191 | sylancl 667 |
. . . . . 6
         |
193 | 190, 192 | addcld 9659 |
. . . . 5
                     |
194 | 14, 42 | mulcld 9660 |
. . . . . 6
            |
195 | 194, 39 | addcld 9659 |
. . . . 5
            ;     |
196 | 187, 193,
195 | addassd 9662 |
. . . 4
                 
                   
       ;                    
                          ;       |
197 | 14, 40, 41 | adddid 9664 |
. . . . . . . . . 10
                          |
198 | 197 | oveq1d 6303 |
. . . . . . . . 9
            ;            
      ;     |
199 | 14, 40 | mulcld 9660 |
. . . . . . . . . 10
        |
200 | 14, 41 | mulcld 9660 |
. . . . . . . . . 10
          |
201 | 199, 200,
39 | addassd 9662 |
. . . . . . . . 9
     
           ;      
     
     ;      |
202 | 1 | oveq1d 6303 |
. . . . . . . . . . . . . . 15
               |
203 | 3, 7, 10, 12 | divsubdird 10419 |
. . . . . . . . . . . . . . 15
                         |
204 | 5, 10, 12 | divcan3d 10385 |
. . . . . . . . . . . . . . . 16
       |
205 | 204 | oveq2d 6304 |
. . . . . . . . . . . . . . 15
                       |
206 | 202, 203,
205 | 3eqtrd 2488 |
. . . . . . . . . . . . . 14
             |
207 | 206 | negeqd 9866 |
. . . . . . . . . . . . 13
               |
208 | 3, 10, 12 | divcld 10380 |
. . . . . . . . . . . . . 14
         |
209 | 208, 5 | negsubdi2d 9999 |
. . . . . . . . . . . . 13
                    |
210 | 207, 209 | eqtrd 2484 |
. . . . . . . . . . . 12
              |
211 | 210 | oveq1d 6303 |
. . . . . . . . . . 11
                  |
212 | 5, 208, 40 | subdird 10072 |
. . . . . . . . . . 11
                         |
213 | 208, 40 | mulcomd 9661 |
. . . . . . . . . . . . 13
                   |
214 | 4 | sqvali 12351 |
. . . . . . . . . . . . . . . . . 18
       |
215 | 214 | oveq2i 6299 |
. . . . . . . . . . . . . . . . 17
                   |
216 | 2, 10, 12 | sqdivd 12426 |
. . . . . . . . . . . . . . . . 17
                   |
217 | 3, 10, 10, 12, 12 | divdiv1d 10411 |
. . . . . . . . . . . . . . . . 17
                   |
218 | 215, 216,
217 | 3eqtr4a 2510 |
. . . . . . . . . . . . . . . 16
                 |
219 | 218 | oveq2d 6304 |
. . . . . . . . . . . . . . 15
                     |
220 | 208, 10, 12 | divcan2d 10382 |
. . . . . . . . . . . . . . 15
                   |
221 | 219, 220 | eqtrd 2484 |
. . . . . . . . . . . . . 14
                 |
222 | 221 | oveq2d 6304 |
. . . . . . . . . . . . 13
                     |
223 | 40, 10, 188 | mul12d 9839 |
. . . . . . . . . . . . 13
                       |
224 | 213, 222,
223 | 3eqtr2d 2490 |
. . . . . . . . . . . 12
                     |
225 | 224 | oveq2d 6304 |
. . . . . . . . . . 11
                             |
226 | 211, 212,
225 | 3eqtrd 2488 |
. . . . . . . . . 10
                      |
227 | 210 | oveq1d 6303 |
. . . . . . . . . . . . 13
                      |
228 | 5, 208, 41 | subdird 10072 |
. . . . . . . . . . . . 13
                               |
229 | 5, 2, 10, 12 | divassd 10415 |
. . . . . . . . . . . . . . 15
           |
230 | 5, 2 | mulcomd 9661 |
. . . . . . . . . . . . . . . 16
       |
231 | 230 | oveq1d 6303 |
. . . . . . . . . . . . . . 15
           |
232 | 229, 231 | eqtr3d 2486 |
. . . . . . . . . . . . . 14
           |
233 | 3, 10, 2, 10, 12, 12 | divmuldivd 10421 |
. . . . . . . . . . . . . . 15
                       |
234 | | df-3 10666 |
. . . . . . . . . . . . . . . . . 18
   |
235 | 234 | oveq2i 6299 |
. . . . . . . . . . . . . . . . 17
           |
236 | | expp1 12276 |
. . . . . . . . . . . . . . . . . 18
 
               |
237 | 2, 27, 236 | sylancl 667 |
. . . . . . . . . . . . . . . . 17
               |
238 | 235, 237 | syl5req 2497 |
. . . . . . . . . . . . . . . 16
             |
239 | 161 | a1i 11 |
. . . . . . . . . . . . . . . 16
     |
240 | 238, 239 | oveq12d 6306 |
. . . . . . . . . . . . . . 15
                   |
241 | 233, 240 | eqtrd 2484 |
. . . . . . . . . . . . . 14
                   |
242 | 232, 241 | oveq12d 6306 |
. . . . . . . . . . . . 13
   
                           |
243 | 227, 228,
242 | 3eqtrd 2488 |
. . . . . . . . . . . 12
                      |
244 | 15 | oveq1d 6303 |
. . . . . . . . . . . . 13
  ;                ;   ;    |
245 | 26, 33, 36, 38 | divdird 10418 |
. . . . . . . . . . . . 13
               ;   ;                ;   ;  ;     |
246 | 21, 25, 36, 38 | divsubdird 10419 |
. . . . . . . . . . . . . . 15
          
   ;          ;       ;     |
247 | | 9t3e27 11144 |
. . . . . . . . . . . . . . . . . 18
  ;  |
248 | 247 | oveq2i 6299 |
. . . . . . . . . . . . . . . . 17
             ;   |
249 | 23, 10, 104, 12, 107 | divcan5d 10406 |
. . . . . . . . . . . . . . . . 17
               |
250 | 248, 249 | syl5eqr 2498 |
. . . . . . . . . . . . . . . 16
      ;        |
251 | 250 | oveq2d 6304 |
. . . . . . . . . . . . . . 15
         ;       ;           ;         |
252 | 246, 251 | eqtrd 2484 |
. . . . . . . . . . . . . 14
          
   ;          ;         |
253 | 31, 36, 38 | divcan3d 10385 |
. . . . . . . . . . . . . 14
  ; 
;    |
254 | 252, 253 | oveq12d 6306 |
. . . . . . . . . . . . 13
               ;   ;  ;            ;          |
255 | 244, 245,
254 | 3eqtrd 2488 |
. . . . . . . . . . . 12
  ;           ;          |
256 | 243, 255 | oveq12d 6306 |
. . . . . . . . . . 11
          ;                         ;           |
257 | 19, 104, 107 | divcld 10380 |
. . . . . . . . . . . . . . 15
         |
258 | 21, 36, 38 | divcld 10380 |
. . . . . . . . . . . . . . 15
        ;    |
259 | 257, 258 | negsubdi2d 9999 |
. . . . . . . . . . . . . 14
                ;           ;           |
260 | 2, 10, 12, 60 | expdivd 12427 |
. . . . . . . . . . . . . . . 16
                   |
261 | 63 | oveq2i 6299 |
. . . . . . . . . . . . . . . . 17
               ;   |
262 | | ax-1cn 9594 |
. . . . . . . . . . . . . . . . . . . . . . 23
 |
263 | 4, 16, 262, 53 | subaddrii 9961 |
. . . . . . . . . . . . . . . . . . . . . 22
   |
264 | 263 | oveq1i 6298 |
. . . . . . . . . . . . . . . . . . . . 21
               |
265 | 19 | mulid2d 9658 |
. . . . . . . . . . . . . . . . . . . . 21
             |
266 | 264, 265 | syl5eq 2496 |
. . . . . . . . . . . . . . . . . . . 20
               |
267 | 10, 68, 19 | subdird 10072 |
. . . . . . . . . . . . . . . . . . . 20
                         |
268 | 266, 267 | eqtr3d 2486 |
. . . . . . . . . . . . . . . . . . 19
                     |
269 | 268 | oveq1d 6303 |
. . . . . . . . . . . . . . . . . 18
      ;                 ;    |
270 | | mulcl 9620 |
. . . . . . . . . . . . . . . . . . . 20
               |
271 | 4, 19, 270 | sylancr 668 |
. . . . . . . . . . . . . . . . . . 19
         |
272 | 271, 21, 36, 38 | divsubdird 10419 |
. . . . . . . . . . . . . . . . . 18
                ;          ;         ;     |
273 | 269, 272 | eqtrd 2484 |
. . . . . . . . . . . . . . . . 17
      ;          ;         ;     |
274 | 261, 273 | syl5eq 2496 |
. . . . . . . . . . . . . . . 16
                   ;         ;     |
275 | 22, 4, 247 | mulcomli 9647 |
. . . . . . . . . . . . . . . . . . 19
  ;  |
276 | 275 | oveq2i 6299 |
. . . . . . . . . . . . . . . . . 18
                 ;   |
277 | 19, 104, 10, 107, 12 | divcan5d 10406 |
. . . . . . . . . . . . . . . . . 18
                   |
278 | 276, 277 | syl5eqr 2498 |
. . . . . . . . . . . . . . . . 17
        ;          |
279 | 278 | oveq1d 6303 |
. . . . . . . . . . . . . . . 16
         ;         ;                 ;     |
280 | 260, 274,
279 | 3eqtrd 2488 |
. . . . . . . . . . . . . . 15
                     ;     |
281 | 280 | negeqd 9866 |
. . . . . . . . . . . . . 14
                       ;     |
282 | 23, 10, 12 | divcld 10380 |
. . . . . . . . . . . . . . 15
       |
283 | 282, 257,
258 | npncan3d 10019 |
. . . . . . . . . . . . . 14
                      ;                ;           |
284 | 259, 281,
283 | 3eqtr4d 2494 |
. . . . . . . . . . . . 13
                             ;          |
285 | 284 | oveq1d 6303 |
. . . . . . . . . . . 12
                                ;           |
286 | 192 | negcld 9970 |
. . . . . . . . . . . . 13
          |
287 | 286, 31 | addcomd 9832 |
. . . . . . . . . . . 12
                     |
288 | 243, 200 | eqeltrrd 2529 |
. . . . . . . . . . . . 13
               |
289 | 258, 282 | subcld 9983 |
. . . . . . . . . . . . 13
         ;         |
290 | 288, 289,
31 | addassd 9662 |
. . . . . . . . . . . 12
                       ;                               ;           |
291 | 285, 287,
290 | 3eqtr3d 2492 |
. . . . . . . . . . 11
                                ;           |
292 | 31, 192 | negsubd 9989 |
. . . . . . . . . . 11
                    |
293 | 256, 291,
292 | 3eqtr2d 2490 |
. . . . . . . . . 10
          ;             |
294 | 226, 293 | oveq12d 6306 |
. . . . . . . . 9
                ;                              |
295 | 198, 201,
294 | 3eqtrd 2488 |
. . . . . . . 8
            ;                             |
296 | 5, 40 | mulcld 9660 |
. . . . . . . . 9
     |
297 | 296, 31, 190, 192 | addsub4d 10030 |
. . . . . . . 8
        
                                          |
298 | 295, 297 | eqtr4d 2487 |
. . . . . . 7
            ;                             |
299 | 298 | oveq2d 6304 |
. . . . . 6
                               ;       
                      
                   |
300 | 296, 31 | addcld 9659 |
. . . . . . 7
       |
301 | 193, 300 | pncan3d 9986 |
. . . . . 6
                                                   |
302 | 299, 301 | eqtrd 2484 |
. . . . 5
                               ;          |
303 | 302 | oveq2d 6304 |
. . . 4
                 
                          ;                         |
304 | 183, 196,
303 | 3eqtrd 2488 |
. . 3
                     ;                        |
305 | 304 | eqeq1d 2452 |
. 2
                      ;                         |
306 | | oveq1 6295 |
. . . . . . . 8
           |
307 | | 0exp 12304 |
. . . . . . . . 9
       |
308 | 46, 307 | ax-mp 5 |
. . . . . . . 8
     |
309 | 306, 308 | syl6eq 2500 |
. . . . . . 7
       |
310 | | 0ne1 10674 |
. . . . . . . 8
 |
311 | 310 | a1i 11 |
. . . . . . 7
   |
312 | 309, 311 | eqnetrd 2690 |
. . . . . 6
       |
313 | 312 | necon2i 2657 |
. . . . 5
       |
314 | | eqcom 2457 |
. . . . . . . 8
             
               |
315 | 2 | adantr 467 |
. . . . . . . . . . . . 13
 
  
  |
316 | | simprl 763 |
. . . . . . . . . . . . . . 15
 
     |
317 | 43 | adantr 467 |
. . . . . . . . . . . . . . 15
 
  
  |
318 | 316, 317 | mulcld 9660 |
. . . . . . . . . . . . . 14
 
       |
319 | 9 | adantr 467 |
. . . . . . . . . . . . . . 15
 
  
  |
320 | | simprr 765 |
. . . . . . . . . . . . . . . 16
 
     |
321 | 168 | adantr 467 |
. . . . . . . . . . . . . . . 16
 
     |
322 | 316, 317,
320, 321 | mulne0d 10261 |
. . . . . . . . . . . . . . 15
 
       |
323 | 319, 318,
322 | divcld 10380 |
. . . . . . . . . . . . . 14
 
         |
324 | 318, 323 | addcld 9659 |
. . . . . . . . . . . . 13
 
             |
325 | 4 | a1i 11 |
. . . . . . . . . . . . 13
 
     |
326 | 11 | a1i 11 |
. . . . . . . . . . . . 13
 
     |
327 | 315, 324,
325, 326 | divdird 10418 |
. . . . . . . . . . . 12
 
                               |
328 | 315, 318,
323 | addassd 9662 |
. . . . . . . . . . . . 13
 
                         |
329 | 328 | oveq1d 6303 |
. . . . . . . . . . . 12
 
                             |
330 | 41 | adantr 467 |
. . . . . . . . . . . . 13
 
       |
331 | 324, 325,
326 | divcld 10380 |
. . . . . . . . . . . . 13
 
               |
332 | 330, 331 | subnegd 9990 |
. . . . . . . . . . . 12
 
                                  |
333 | 327, 329,
332 | 3eqtr4d 2494 |
. . . . . . . . . . 11
 
                                |
334 | 333 | negeqd 9866 |
. . . . . . . . . 10
 
                                  |
335 | 331 | negcld 9970 |
. . . . . . . . . . 11
 
                |
336 | 330, 335 | negsubdi2d 9999 |
. . . . . . . . . 10
 
                                    |
337 | 334, 336 | eqtrd 2484 |
. . . . . . . . 9
 
                                 |
338 | 337 | eqeq1d 2452 |
. . . . . . . 8
 
                                   |
339 | 314, 338 | syl5bb 261 |
. . . . . . 7
 
                                   |
340 | 40 | adantr 467 |
. . . . . . . 8
 
  
  |
341 | 335, 330,
340 | subadd2d 10002 |
. . . . . . 7
 
                    
                |
342 | 318, 323,
325, 326 | divdird 10418 |
. . . . . . . . . 10
 
                           |
343 | 342 | negeqd 9866 |
. . . . . . . . 9
 
                             |
344 | 318, 325,
326 | divcld 10380 |
. . . . . . . . . 10
 
         |
345 | 323, 325,
326 | divcld 10380 |
. . . . . . . . . 10
 
           |
346 | 344, 345 | negdi2d 9997 |
. . . . . . . . 9
 
                               |
347 | 316, 317,
325, 326 | divassd 10415 |
. . . . . . . . . . . 12
 
             |
348 | 347 | negeqd 9866 |
. . . . . . . . . . 11
 
               |
349 | 44 | adantr 467 |
. . . . . . . . . . . 12
 
       |
350 | 316, 349 | mulneg2d 10069 |
. . . . . . . . . . 11
 
               |
351 | 348, 350 | eqtr4d 2487 |
. . . . . . . . . 10
 
               |
352 | 319, 318,
325, 322, 326 | divdiv32d 10405 |
. . . . . . . . . . . 12
 
                 |
353 | 13 | adantr 467 |
. . . . . . . . . . . . 13
 
       |
354 | 353, 318,
325, 322, 326 | divcan7d 10408 |
. . . . . . . . . . . 12
 
                     |
355 | 163 | oveq1d 6303 |
. . . . . . . . . . . . 13
                     |
356 | 355 | adantr 467 |
. . . . . . . . . . . 12
 
                       |
357 | 352, 354,
356 | 3eqtr2d 2490 |
. . . . . . . . . . 11
 
                   |
358 | 127 | adantr 467 |
. . . . . . . . . . . 12
 
       |
359 | 318, 325,
322, 326 | divne0d 10396 |
. . . . . . . . . . . 12
 
         |
360 | 358, 344,
359 | div2negd 10395 |
. . . . . . . . . . 11
 
                       |
361 | 351 | oveq2d 6304 |
. . . . . . . . . . 11
 
               
         |
362 | 357, 360,
361 | 3eqtr2d 2490 |
. . . . . . . . . 10
 
           
         |
363 | 351, 362 | oveq12d 6306 |
. . . . . . . . 9
 
                                   |
364 | 343, 346,
363 | 3eqtrd 2488 |
. . . . . . . 8
 
                                 |
365 | 364 | eqeq2d 2460 |
. . . . . . 7
 
     
              
                      |
366 | 339, 341,
365 | 3bitrrd 284 |
. . . . . 6
 
     
                  
                |
367 | 366 | anassrs 653 |
. . . . 5
                          
                |
368 | 313, 367 | sylan2 477 |
. . . 4
           
                  
                |
369 | 368 | pm5.32da 646 |
. . 3
 

                           
                      |
370 | 369 | rexbidva 2897 |
. 2
                             
                       |
371 | 171, 305,
370 | 3bitr3d 287 |
1
                    
                      |