Step | Hyp | Ref
| Expression |
1 | | id 22 |
. 2
   |
2 | | dvnmul.n |
. . 3
   |
3 | | nn0uz 11190 |
. . . . 5
     |
4 | 2, 3 | syl6eleq 2538 |
. . . 4
       |
5 | | eluzfz2 11804 |
. . . 4
    
      |
6 | 4, 5 | syl 17 |
. . 3
       |
7 | | eleq1 2516 |
. . . . 5
     
       |
8 | | fveq2 5863 |
. . . . . . 7
                           |
9 | | oveq2 6296 |
. . . . . . . . . 10
           |
10 | 9 | sumeq1d 13760 |
. . . . . . . . 9
                               
                     
         |
11 | | oveq1 6295 |
. . . . . . . . . . 11
       |
12 | | oveq1 6295 |
. . . . . . . . . . . . . 14
       |
13 | 12 | fveq2d 5867 |
. . . . . . . . . . . . 13
          
    |
14 | 13 | fveq1d 5865 |
. . . . . . . . . . . 12
                       |
15 | 14 | oveq2d 6304 |
. . . . . . . . . . 11
                                  
        |
16 | 11, 15 | oveq12d 6306 |
. . . . . . . . . 10
                 
                                 |
17 | 16 | sumeq2ad 37638 |
. . . . . . . . 9
                               
                     
         |
18 | 10, 17 | eqtrd 2484 |
. . . . . . . 8
                               
                     
         |
19 | 18 | mpteq2dv 4489 |
. . . . . . 7
                        
                                          |
20 | 8, 19 | eqeq12d 2465 |
. . . . . 6
                                             
                                               |
21 | 20 | imbi2d 318 |
. . . . 5
  
                                             
                                   
            |
22 | 7, 21 | imbi12d 322 |
. . . 4
                                           
         
    
                                                  |
23 | | fveq2 5863 |
. . . . . . 7
                           |
24 | | simpl 459 |
. . . . . . . . . 10
     |
25 | 24 | oveq2d 6304 |
. . . . . . . . 9
             |
26 | | simpll 759 |
. . . . . . . . . . 11
   
       |
27 | 26 | oveq1d 6303 |
. . . . . . . . . 10
   
           |
28 | 26 | oveq1d 6303 |
. . . . . . . . . . . . 13
   
           |
29 | 28 | fveq2d 5867 |
. . . . . . . . . . . 12
   
                   |
30 | 29 | fveq1d 5865 |
. . . . . . . . . . 11
   
                           |
31 | 30 | oveq2d 6304 |
. . . . . . . . . 10
   
                                               |
32 | 27, 31 | oveq12d 6306 |
. . . . . . . . 9
   
                     
                                 |
33 | 25, 32 | sumeq12rdv 13766 |
. . . . . . . 8
                                                                 |
34 | 33 | mpteq2dva 4488 |
. . . . . . 7
                        
                                          |
35 | 23, 34 | eqeq12d 2465 |
. . . . . 6
                                             
                                               |
36 | 35 | imbi2d 318 |
. . . . 5
  
                                             
                                                |
37 | | fveq2 5863 |
. . . . . . 7
                           |
38 | | simpl 459 |
. . . . . . . . . 10
 
   |
39 | 38 | oveq2d 6304 |
. . . . . . . . 9
 
           |
40 | | simpll 759 |
. . . . . . . . . . 11
   
       |
41 | 40 | oveq1d 6303 |
. . . . . . . . . 10
   
           |
42 | 40 | oveq1d 6303 |
. . . . . . . . . . . . 13
   
           |
43 | 42 | fveq2d 5867 |
. . . . . . . . . . . 12
   
                   |
44 | 43 | fveq1d 5865 |
. . . . . . . . . . 11
   
                           |
45 | 44 | oveq2d 6304 |
. . . . . . . . . 10
   
                                               |
46 | 41, 45 | oveq12d 6306 |
. . . . . . . . 9
   
                     
                                 |
47 | 39, 46 | sumeq12rdv 13766 |
. . . . . . . 8
 
                                                               |
48 | 47 | mpteq2dva 4488 |
. . . . . . 7
                        
                                          |
49 | 37, 48 | eqeq12d 2465 |
. . . . . 6
                                             
                                               |
50 | 49 | imbi2d 318 |
. . . . 5
  
                                             
                                                |
51 | | fveq2 5863 |
. . . . . . 7
                               |
52 | | simpl 459 |
. . . . . . . . . 10
   
     |
53 | 52 | oveq2d 6304 |
. . . . . . . . 9
   
             |
54 | | simpll 759 |
. . . . . . . . . . 11
     
           |
55 | 54 | oveq1d 6303 |
. . . . . . . . . 10
     
               |
56 | 54 | oveq1d 6303 |
. . . . . . . . . . . . 13
     
               |
57 | 56 | fveq2d 5867 |
. . . . . . . . . . . 12
     
                       |
58 | 57 | fveq1d 5865 |
. . . . . . . . . . 11
     
                               |
59 | 58 | oveq2d 6304 |
. . . . . . . . . 10
     
                                                   |
60 | 55, 59 | oveq12d 6306 |
. . . . . . . . 9
     
                       
                                     |
61 | 53, 60 | sumeq12rdv 13766 |
. . . . . . . 8
   
                                                                     |
62 | 61 | mpteq2dva 4488 |
. . . . . . 7
                          
                                                |
63 | 51, 62 | eqeq12d 2465 |
. . . . . 6
                                               
                                                       |
64 | 63 | imbi2d 318 |
. . . . 5
    
                                             
                                                        |
65 | | fveq2 5863 |
. . . . . . 7
                           |
66 | | simpl 459 |
. . . . . . . . . 10
 
   |
67 | 66 | oveq2d 6304 |
. . . . . . . . 9
 
           |
68 | | simpll 759 |
. . . . . . . . . . 11
   
       |
69 | 68 | oveq1d 6303 |
. . . . . . . . . 10
   
           |
70 | 68 | oveq1d 6303 |
. . . . . . . . . . . . 13
   
           |
71 | 70 | fveq2d 5867 |
. . . . . . . . . . . 12
   
              
    |
72 | 71 | fveq1d 5865 |
. . . . . . . . . . 11
   
                           |
73 | 72 | oveq2d 6304 |
. . . . . . . . . 10
   
                                      
        |
74 | 69, 73 | oveq12d 6306 |
. . . . . . . . 9
   
                     
                                 |
75 | 67, 74 | sumeq12rdv 13766 |
. . . . . . . 8
 
                                                               |
76 | 75 | mpteq2dva 4488 |
. . . . . . 7
                        
                                          |
77 | 65, 76 | eqeq12d 2465 |
. . . . . 6
                                             
                                               |
78 | 77 | imbi2d 318 |
. . . . 5
  
                                             
                                                |
79 | | dvnmul.s |
. . . . . . . . 9
      |
80 | | recnprss 22852 |
. . . . . . . . 9
   
  |
81 | 79, 80 | syl 17 |
. . . . . . . 8

  |
82 | | dvnmul.a |
. . . . . . . . . 10
 
   |
83 | | dvnmul.cc |
. . . . . . . . . 10
 
   |
84 | 82, 83 | mulcld 9660 |
. . . . . . . . 9
 
 
   |
85 | | restsspw 15323 |
. . . . . . . . . . 11
   ℂfld ↾t    |
86 | | dvnmul.x |
. . . . . . . . . . 11
    ℂfld ↾t    |
87 | 85, 86 | sseldi 3429 |
. . . . . . . . . 10
    |
88 | | elpwi 3959 |
. . . . . . . . . 10
    |
89 | 87, 88 | syl 17 |
. . . . . . . . 9

  |
90 | | cnex 9617 |
. . . . . . . . . 10
 |
91 | 90 | a1i 11 |
. . . . . . . . 9
   |
92 | 84, 89, 91, 79 | mptelpm 37435 |
. . . . . . . 8
     
   |
93 | | dvn0 22871 |
. . . . . . . 8
 
                         |
94 | 81, 92, 93 | syl2anc 666 |
. . . . . . 7
                   |
95 | | 0z 10945 |
. . . . . . . . . . . 12
 |
96 | | fzsn 11837 |
. . . . . . . . . . . 12
         |
97 | 95, 96 | ax-mp 5 |
. . . . . . . . . . 11
       |
98 | 97 | sumeq1i 13757 |
. . . . . . . . . 10
                              
                           |
99 | 98 | a1i 11 |
. . . . . . . . 9
 
                               
                            |
100 | | nfcvd 2592 |
. . . . . . . . . 10
 
       |
101 | | nfv 1760 |
. . . . . . . . . 10
     |
102 | | oveq2 6296 |
. . . . . . . . . . . . . 14
       |
103 | | 0nn0 10881 |
. . . . . . . . . . . . . . . 16
 |
104 | | bcn0 12492 |
. . . . . . . . . . . . . . . 16

    |
105 | 103, 104 | ax-mp 5 |
. . . . . . . . . . . . . . 15
   |
106 | 105 | a1i 11 |
. . . . . . . . . . . . . 14
     |
107 | 102, 106 | eqtrd 2484 |
. . . . . . . . . . . . 13
     |
108 | 107 | adantl 468 |
. . . . . . . . . . . 12
         |
109 | | fveq2 5863 |
. . . . . . . . . . . . . . . . . . 19
           |
110 | 109 | adantl 468 |
. . . . . . . . . . . . . . . . . 18
 
           |
111 | | dvnmul.c |
. . . . . . . . . . . . . . . . . . . . . 22
               |
112 | | fveq2 5863 |
. . . . . . . . . . . . . . . . . . . . . . 23
                   |
113 | 112 | cbvmptv 4494 |
. . . . . . . . . . . . . . . . . . . . . 22
                             |
114 | 111, 113 | eqtri 2472 |
. . . . . . . . . . . . . . . . . . . . 21
               |
115 | 114 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
                 |
116 | | fveq2 5863 |
. . . . . . . . . . . . . . . . . . . . 21
                   |
117 | 116 | adantl 468 |
. . . . . . . . . . . . . . . . . . . 20
 
                   |
118 | | eluzfz1 11803 |
. . . . . . . . . . . . . . . . . . . . 21
    
      |
119 | 4, 118 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
       |
120 | | fvex 5873 |
. . . . . . . . . . . . . . . . . . . . 21
         |
121 | 120 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
           |
122 | 115, 117,
119, 121 | fvmptd 5952 |
. . . . . . . . . . . . . . . . . . 19
               |
123 | 122 | adantr 467 |
. . . . . . . . . . . . . . . . . 18
 
               |
124 | 110, 123 | eqtrd 2484 |
. . . . . . . . . . . . . . . . 17
 
               |
125 | | dvnmulf |
. . . . . . . . . . . . . . . . . . . 20
   |
126 | 82, 89, 91, 79 | mptelpm 37435 |
. . . . . . . . . . . . . . . . . . . 20
   
   |
127 | 125, 126 | syl5eqel 2532 |
. . . . . . . . . . . . . . . . . . 19
     |
128 | | dvn0 22871 |
. . . . . . . . . . . . . . . . . . 19
 
             |
129 | 81, 127, 128 | syl2anc 666 |
. . . . . . . . . . . . . . . . . 18
           |
130 | 129 | adantr 467 |
. . . . . . . . . . . . . . . . 17
 
           |
131 | 124, 130 | eqtrd 2484 |
. . . . . . . . . . . . . . . 16
 
       |
132 | 131 | fveq1d 5865 |
. . . . . . . . . . . . . . 15
 
               |
133 | 132 | adantlr 720 |
. . . . . . . . . . . . . 14
                   |
134 | | simpr 463 |
. . . . . . . . . . . . . . . 16
 
   |
135 | 125 | fvmpt2 5955 |
. . . . . . . . . . . . . . . 16
 
       |
136 | 134, 82, 135 | syl2anc 666 |
. . . . . . . . . . . . . . 15
 
       |
137 | 136 | adantr 467 |
. . . . . . . . . . . . . 14
           |
138 | 133, 137 | eqtrd 2484 |
. . . . . . . . . . . . 13
               |
139 | | oveq2 6296 |
. . . . . . . . . . . . . . . . . . 19
       |
140 | | 0m0e0 10716 |
. . . . . . . . . . . . . . . . . . . 20
   |
141 | 140 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
     |
142 | 139, 141 | eqtrd 2484 |
. . . . . . . . . . . . . . . . . 18
     |
143 | 142 | fveq2d 5867 |
. . . . . . . . . . . . . . . . 17
             |
144 | 143 | fveq1d 5865 |
. . . . . . . . . . . . . . . 16
                     |
145 | 144 | adantl 468 |
. . . . . . . . . . . . . . 15
 
                     |
146 | 145 | adantlr 720 |
. . . . . . . . . . . . . 14
                         |
147 | | dvnmul.d |
. . . . . . . . . . . . . . . . . . . 20
               |
148 | | fveq2 5863 |
. . . . . . . . . . . . . . . . . . . . 21
                   |
149 | 148 | cbvmptv 4494 |
. . . . . . . . . . . . . . . . . . . 20
                             |
150 | 147, 149 | eqtri 2472 |
. . . . . . . . . . . . . . . . . . 19
               |
151 | 150 | fveq1i 5864 |
. . . . . . . . . . . . . . . . . 18
                       |
152 | 151 | a1i 11 |
. . . . . . . . . . . . . . . . 17
                         |
153 | | eqidd 2451 |
. . . . . . . . . . . . . . . . . 18
                               |
154 | | fveq2 5863 |
. . . . . . . . . . . . . . . . . . . 20
                   |
155 | 154 | adantl 468 |
. . . . . . . . . . . . . . . . . . 19
 
                   |
156 | | dvnmul.f |
. . . . . . . . . . . . . . . . . . . . . 22
   |
157 | 83, 89, 91, 79 | mptelpm 37435 |
. . . . . . . . . . . . . . . . . . . . . 22
   
   |
158 | 156, 157 | syl5eqel 2532 |
. . . . . . . . . . . . . . . . . . . . 21
     |
159 | | dvn0 22871 |
. . . . . . . . . . . . . . . . . . . . 21
 
             |
160 | 81, 158, 159 | syl2anc 666 |
. . . . . . . . . . . . . . . . . . . 20
           |
161 | 160 | adantr 467 |
. . . . . . . . . . . . . . . . . . 19
 
           |
162 | 155, 161 | eqtrd 2484 |
. . . . . . . . . . . . . . . . . 18
 
           |
163 | 156 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
     |
164 | | mptexg 6133 |
. . . . . . . . . . . . . . . . . . . 20
      |
165 | 87, 164 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
     |
166 | 163, 165 | eqeltrd 2528 |
. . . . . . . . . . . . . . . . . 18
   |
167 | 153, 162,
119, 166 | fvmptd 5952 |
. . . . . . . . . . . . . . . . 17
                     |
168 | 152, 167 | eqtrd 2484 |
. . . . . . . . . . . . . . . 16
       |
169 | 168 | fveq1d 5865 |
. . . . . . . . . . . . . . 15
               |
170 | 169 | ad2antrr 731 |
. . . . . . . . . . . . . 14
                   |
171 | 163, 83 | fvmpt2d 5957 |
. . . . . . . . . . . . . . 15
 
       |
172 | 171 | adantr 467 |
. . . . . . . . . . . . . 14
           |
173 | 146, 170,
172 | 3eqtrd 2488 |
. . . . . . . . . . . . 13
                 |
174 | 138, 173 | oveq12d 6306 |
. . . . . . . . . . . 12
                             |
175 | 108, 174 | oveq12d 6306 |
. . . . . . . . . . 11
                                   |
176 | 84 | mulid2d 9658 |
. . . . . . . . . . . 12
 
         |
177 | 176 | adantr 467 |
. . . . . . . . . . 11
      
      |
178 | 175, 177 | eqtrd 2484 |
. . . . . . . . . 10
                                 |
179 | | 0re 9640 |
. . . . . . . . . . 11
 |
180 | 179 | a1i 11 |
. . . . . . . . . 10
 
   |
181 | 100, 101,
178, 180, 84 | sumsnd 37341 |
. . . . . . . . 9
 
                                |
182 | 99, 181 | eqtr2d 2485 |
. . . . . . . 8
 
 
                                 |
183 | 182 | mpteq2dva 4488 |
. . . . . . 7
                                       |
184 | 94, 183 | eqtrd 2484 |
. . . . . 6
                                               |
185 | 184 | a1i 11 |
. . . . 5
    
                                                |
186 | | simp3 1009 |
. . . . . . 7
   ..^                                               
  |
187 | | simp1 1007 |
. . . . . . 7
   ..^                                               
 ..^   |
188 | | simp2 1008 |
. . . . . . . 8
   ..^                                               
                                                |
189 | | pm3.35 590 |
. . . . . . . 8
 
                                                                                             |
190 | 186, 188,
189 | syl2anc 666 |
. . . . . . 7
   ..^                                               
                                              |
191 | 81 | adantr 467 |
. . . . . . . . . 10
 
 ..^    |
192 | 92 | adantr 467 |
. . . . . . . . . 10
 
 ..^          |
193 | | elfzonn0 11957 |
. . . . . . . . . . 11
  ..^
  |
194 | 193 | adantl 468 |
. . . . . . . . . 10
 
 ..^    |
195 | | dvnp1 22872 |
. . . . . . . . . 10
 
     
                               |
196 | 191, 192,
194, 195 | syl3anc 1267 |
. . . . . . . . 9
 
 ..^                                |
197 | 196 | adantr 467 |
. . . . . . . 8
    ..^                                                                             |
198 | | simpr 463 |
. . . . . . . . 9
    ..^                                                                                             |
199 | 198 | oveq2d 6304 |
. . . . . . . 8
    ..^                                                              
                                  |
200 | | eqid 2450 |
. . . . . . . . . . 11
   ℂfld ↾t     ℂfld
↾t   |
201 | | eqid 2450 |
. . . . . . . . . . 11
  ℂfld   ℂfld |
202 | 79 | adantr 467 |
. . . . . . . . . . 11
 
 ..^   
   |
203 | 86 | adantr 467 |
. . . . . . . . . . 11
 
 ..^     ℂfld
↾t    |
204 | | fzfid 12183 |
. . . . . . . . . . 11
 
 ..^        |
205 | 193 | adantr 467 |
. . . . . . . . . . . . . . . 16
   ..^        |
206 | | elfzelz 11797 |
. . . . . . . . . . . . . . . . 17
       |
207 | 206 | adantl 468 |
. . . . . . . . . . . . . . . 16
   ..^        |
208 | 205, 207 | bccld 37531 |
. . . . . . . . . . . . . . 15
   ..^          |
209 | 208 | nn0cnd 10924 |
. . . . . . . . . . . . . 14
   ..^          |
210 | 209 | adantll 719 |
. . . . . . . . . . . . 13
    ..^           |
211 | 210 | 3adant3 1027 |
. . . . . . . . . . . 12
    ..^     
     |
212 | | simpll 759 |
. . . . . . . . . . . . . . . 16
    ..^         |
213 | | 0zd 10946 |
. . . . . . . . . . . . . . . . . . . 20
   ..^        |
214 | | elfzoel2 11916 |
. . . . . . . . . . . . . . . . . . . . 21
  ..^
  |
215 | 214 | adantr 467 |
. . . . . . . . . . . . . . . . . . . 20
   ..^        |
216 | 213, 215,
207 | 3jca 1187 |
. . . . . . . . . . . . . . . . . . 19
   ..^      
   |
217 | | elfzle1 11799 |
. . . . . . . . . . . . . . . . . . . 20
       |
218 | 217 | adantl 468 |
. . . . . . . . . . . . . . . . . . 19
   ..^        |
219 | 207 | zred 11037 |
. . . . . . . . . . . . . . . . . . . 20
   ..^        |
220 | 214 | zred 11037 |
. . . . . . . . . . . . . . . . . . . . 21
  ..^
  |
221 | 220 | adantr 467 |
. . . . . . . . . . . . . . . . . . . 20
   ..^        |
222 | 193 | nn0red 10923 |
. . . . . . . . . . . . . . . . . . . . . 22
  ..^
  |
223 | 222 | adantr 467 |
. . . . . . . . . . . . . . . . . . . . 21
   ..^        |
224 | | elfzle2 11800 |
. . . . . . . . . . . . . . . . . . . . . 22
       |
225 | 224 | adantl 468 |
. . . . . . . . . . . . . . . . . . . . 21
   ..^        |
226 | | elfzolt2 11926 |
. . . . . . . . . . . . . . . . . . . . . 22
  ..^
  |
227 | 226 | adantr 467 |
. . . . . . . . . . . . . . . . . . . . 21
   ..^        |
228 | 219, 223,
221, 225, 227 | lelttrd 9790 |
. . . . . . . . . . . . . . . . . . . 20
   ..^        |
229 | 219, 221,
228 | ltled 9780 |
. . . . . . . . . . . . . . . . . . 19
   ..^        |
230 | 216, 218,
229 | jca32 538 |
. . . . . . . . . . . . . . . . . 18
   ..^       
 
    |
231 | | elfz2 11788 |
. . . . . . . . . . . . . . . . . 18
    
 
 
    |
232 | 230, 231 | sylibr 216 |
. . . . . . . . . . . . . . . . 17
   ..^            |
233 | 232 | adantll 719 |
. . . . . . . . . . . . . . . 16
    ..^             |
234 | | dvnmul.dvnf |
. . . . . . . . . . . . . . . . 17
 
                   |
235 | 111 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
                 |
236 | | fvex 5873 |
. . . . . . . . . . . . . . . . . . . 20
         |
237 | 236 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
 
               |
238 | 235, 237 | fvmpt2d 5957 |
. . . . . . . . . . . . . . . . . 18
 
                   |
239 | 238 | feq1d 5712 |
. . . . . . . . . . . . . . . . 17
 
             
               |
240 | 234, 239 | mpbird 236 |
. . . . . . . . . . . . . . . 16
 
               |
241 | 212, 233,
240 | syl2anc 666 |
. . . . . . . . . . . . . . 15
    ..^                 |
242 | 241 | 3adant3 1027 |
. . . . . . . . . . . . . 14
    ..^     
           |
243 | | simp3 1009 |
. . . . . . . . . . . . . 14
    ..^     
   |
244 | 242, 243 | ffvelrnd 6021 |
. . . . . . . . . . . . 13
    ..^     
           |
245 | 193 | nn0zd 11035 |
. . . . . . . . . . . . . . . . . . . . . . 23
  ..^
  |
246 | 245 | adantr 467 |
. . . . . . . . . . . . . . . . . . . . . 22
   ..^        |
247 | 246, 207 | zsubcld 11042 |
. . . . . . . . . . . . . . . . . . . . 21
   ..^          |
248 | 213, 215,
247 | 3jca 1187 |
. . . . . . . . . . . . . . . . . . . 20
   ..^      
     |
249 | | elfzel2 11795 |
. . . . . . . . . . . . . . . . . . . . . . . 24
       |
250 | 249 | zred 11037 |
. . . . . . . . . . . . . . . . . . . . . . 23
       |
251 | 206 | zred 11037 |
. . . . . . . . . . . . . . . . . . . . . . 23
       |
252 | 250, 251 | subge0d 10200 |
. . . . . . . . . . . . . . . . . . . . . 22
     
 
   |
253 | 224, 252 | mpbird 236 |
. . . . . . . . . . . . . . . . . . . . 21
         |
254 | 253 | adantl 468 |
. . . . . . . . . . . . . . . . . . . 20
   ..^          |
255 | 223, 219 | resubcld 10044 |
. . . . . . . . . . . . . . . . . . . . 21
   ..^          |
256 | 221, 219 | resubcld 10044 |
. . . . . . . . . . . . . . . . . . . . . . 23
   ..^      
   |
257 | 179 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
   ..^        |
258 | 221, 257 | jca 535 |
. . . . . . . . . . . . . . . . . . . . . . . 24
   ..^      
   |
259 | | resubcl 9935 |
. . . . . . . . . . . . . . . . . . . . . . . 24
 
     |
260 | 258, 259 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
   ..^      
   |
261 | 223, 221,
219, 227 | ltsub1dd 10222 |
. . . . . . . . . . . . . . . . . . . . . . 23
   ..^            |
262 | 257, 219,
221, 218 | lesub2dd 10227 |
. . . . . . . . . . . . . . . . . . . . . . 23
   ..^      
     |
263 | 255, 256,
260, 261, 262 | ltletrd 9792 |
. . . . . . . . . . . . . . . . . . . . . 22
   ..^            |
264 | 220 | recnd 9666 |
. . . . . . . . . . . . . . . . . . . . . . . 24
  ..^
  |
265 | 264 | subid1d 9972 |
. . . . . . . . . . . . . . . . . . . . . . 23
  ..^
    |
266 | 265 | adantr 467 |
. . . . . . . . . . . . . . . . . . . . . 22
   ..^      
   |
267 | 263, 266 | breqtrd 4426 |
. . . . . . . . . . . . . . . . . . . . 21
   ..^          |
268 | 255, 221,
267 | ltled 9780 |
. . . . . . . . . . . . . . . . . . . 20
   ..^          |
269 | 248, 254,
268 | jca32 538 |
. . . . . . . . . . . . . . . . . . 19
   ..^             
      |
270 | | elfz2 11788 |
. . . . . . . . . . . . . . . . . . 19
      
 
            |
271 | 269, 270 | sylibr 216 |
. . . . . . . . . . . . . . . . . 18
   ..^              |
272 | 271 | adantll 719 |
. . . . . . . . . . . . . . . . 17
    ..^               |
273 | | ovex 6316 |
. . . . . . . . . . . . . . . . . 18
   |
274 | | eleq1 2516 |
. . . . . . . . . . . . . . . . . . . 20
       
         |
275 | 274 | anbi2d 709 |
. . . . . . . . . . . . . . . . . . 19
    
    
           |
276 | | fveq2 5863 |
. . . . . . . . . . . . . . . . . . . 20
                       |
277 | 276 | feq1d 5712 |
. . . . . . . . . . . . . . . . . . 19
                                 |
278 | 275, 277 | imbi12d 322 |
. . . . . . . . . . . . . . . . . 18
     
                 
        
                  |
279 | | nfv 1760 |
. . . . . . . . . . . . . . . . . . 19
   
                   |
280 | | eleq1 2516 |
. . . . . . . . . . . . . . . . . . . . 21
     
       |
281 | 280 | anbi2d 709 |
. . . . . . . . . . . . . . . . . . . 20
  
    
         |
282 | | fveq2 5863 |
. . . . . . . . . . . . . . . . . . . . 21
                   |
283 | 282 | feq1d 5712 |
. . . . . . . . . . . . . . . . . . . 20
                             |
284 | 281, 283 | imbi12d 322 |
. . . . . . . . . . . . . . . . . . 19
   
                 
      
                |
285 | | dvnmul.dvng |
. . . . . . . . . . . . . . . . . . 19
 
                   |
286 | 279, 284,
285 | chvar 2105 |
. . . . . . . . . . . . . . . . . 18
 
                   |
287 | 273, 278,
286 | vtocl 3099 |
. . . . . . . . . . . . . . . . 17
 
                       |
288 | 212, 272,
287 | syl2anc 666 |
. . . . . . . . . . . . . . . 16
    ..^                       |
289 | 150 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
   ..^                      |
290 | | fveq2 5863 |
. . . . . . . . . . . . . . . . . . . 20
                       |
291 | 290 | adantl 468 |
. . . . . . . . . . . . . . . . . . 19
    ..^
       
                    |
292 | | fvex 5873 |
. . . . . . . . . . . . . . . . . . . 20
           |
293 | 292 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
   ..^                  |
294 | 289, 291,
271, 293 | fvmptd 5952 |
. . . . . . . . . . . . . . . . . 18
   ..^                        |
295 | 294 | adantll 719 |
. . . . . . . . . . . . . . . . 17
    ..^                         |
296 | 295 | feq1d 5712 |
. . . . . . . . . . . . . . . 16
    ..^                 
                 |
297 | 288, 296 | mpbird 236 |
. . . . . . . . . . . . . . 15
    ..^                   |
298 | 297 | 3adant3 1027 |
. . . . . . . . . . . . . 14
    ..^     
             |
299 | 298, 243 | ffvelrnd 6021 |
. . . . . . . . . . . . 13
    ..^     
             |
300 | 244, 299 | mulcld 9660 |
. . . . . . . . . . . 12
    ..^     
                       |
301 | 211, 300 | mulcld 9660 |
. . . . . . . . . . 11
    ..^     
                           |
302 | 211 | 3expa 1207 |
. . . . . . . . . . . . 13
   
 ..^ 
     
    |
303 | 246 | peano2zd 11040 |
. . . . . . . . . . . . . . . . . . . . . . . 24
   ..^          |
304 | 303, 207 | zsubcld 11042 |
. . . . . . . . . . . . . . . . . . . . . . 23
   ..^            |
305 | 213, 215,
304 | 3jca 1187 |
. . . . . . . . . . . . . . . . . . . . . 22
   ..^      
       |
306 | | peano2re 9803 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
     |
307 | 250, 306 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
         |
308 | | peano2re 9803 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
     |
309 | 251, 308 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
         |
310 | 251 | ltp1d 10534 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
         |
311 | | 1red 9655 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
       |
312 | 251, 250,
311, 224 | leadd1dd 10224 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
           |
313 | 251, 309,
307, 310, 312 | ltletrd 9792 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
         |
314 | 251, 307,
313 | ltled 9780 |
. . . . . . . . . . . . . . . . . . . . . . . 24
         |
315 | 314 | adantl 468 |
. . . . . . . . . . . . . . . . . . . . . . 23
   ..^          |
316 | 223, 306 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . 24
   ..^          |
317 | 316, 219 | subge0d 10200 |
. . . . . . . . . . . . . . . . . . . . . . 23
   ..^      
   
     |
318 | 315, 317 | mpbird 236 |
. . . . . . . . . . . . . . . . . . . . . 22
   ..^            |
319 | 316, 219 | resubcld 10044 |
. . . . . . . . . . . . . . . . . . . . . . 23
   ..^            |
320 | | elfzop1le2 37497 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
  ..^
    |
321 | 320 | adantr 467 |
. . . . . . . . . . . . . . . . . . . . . . . 24
   ..^          |
322 | 316, 221,
219, 321 | lesub1dd 10226 |
. . . . . . . . . . . . . . . . . . . . . . 23
   ..^              |
323 | 262, 266 | breqtrd 4426 |
. . . . . . . . . . . . . . . . . . . . . . 23
   ..^      
   |
324 | 319, 256,
221, 322, 323 | letrd 9789 |
. . . . . . . . . . . . . . . . . . . . . 22
   ..^            |
325 | 305, 318,
324 | jca32 538 |
. . . . . . . . . . . . . . . . . . . . 21
   ..^                 
        |
326 | | elfz2 11788 |
. . . . . . . . . . . . . . . . . . . . 21
        
 
                  |
327 | 325, 326 | sylibr 216 |
. . . . . . . . . . . . . . . . . . . 20
   ..^                |
328 | 327 | adantll 719 |
. . . . . . . . . . . . . . . . . . 19
    ..^                 |
329 | | ovex 6316 |
. . . . . . . . . . . . . . . . . . . 20
     |
330 | | eleq1 2516 |
. . . . . . . . . . . . . . . . . . . . . 22
         
           |
331 | 330 | anbi2d 709 |
. . . . . . . . . . . . . . . . . . . . 21
      
    
             |
332 | | fveq2 5863 |
. . . . . . . . . . . . . . . . . . . . . 22
                           |
333 | 332 | feq1d 5712 |
. . . . . . . . . . . . . . . . . . . . 21
                                     |
334 | 331, 333 | imbi12d 322 |
. . . . . . . . . . . . . . . . . . . 20
       
                 
          
                    |
335 | 329, 334,
286 | vtocl 3099 |
. . . . . . . . . . . . . . . . . . 19
 
                           |
336 | 212, 328,
335 | syl2anc 666 |
. . . . . . . . . . . . . . . . . 18
    ..^                         |
337 | 150 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
    ..^                       |
338 | | simpr 463 |
. . . . . . . . . . . . . . . . . . . . 21
   
 ..^ 
         
      |
339 | 338 | fveq2d 5867 |
. . . . . . . . . . . . . . . . . . . 20
   
 ..^ 
         
                      |
340 | | fvex 5873 |
. . . . . . . . . . . . . . . . . . . . 21
             |
341 | 340 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
    ..^                     |
342 | 337, 339,
328, 341 | fvmptd 5952 |
. . . . . . . . . . . . . . . . . . 19
    ..^                             |
343 | 342 | feq1d 5712 |
. . . . . . . . . . . . . . . . . 18
    ..^                   
                   |
344 | 336, 343 | mpbird 236 |
. . . . . . . . . . . . . . . . 17
    ..^                     |
345 | 344 | ffvelrnda 6020 |
. . . . . . . . . . . . . . . 16
   
 ..^ 
     
              |
346 | 244 | 3expa 1207 |
. . . . . . . . . . . . . . . 16
   
 ..^ 
     
          |
347 | 345, 346 | mulcomd 9661 |
. . . . . . . . . . . . . . 15
   
 ..^ 
     
                                              |
348 | 347 | oveq2d 6304 |
. . . . . . . . . . . . . 14
   
 ..^ 
     
                                                                                              |
349 | 207 | peano2zd 11040 |
. . . . . . . . . . . . . . . . . . . . . 22
   ..^          |
350 | 213, 215,
349 | 3jca 1187 |
. . . . . . . . . . . . . . . . . . . . 21
   ..^      
     |
351 | 179 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . 23
       |
352 | 351, 251,
309, 217, 310 | lelttrd 9790 |
. . . . . . . . . . . . . . . . . . . . . . 23
         |
353 | 351, 309,
352 | ltled 9780 |
. . . . . . . . . . . . . . . . . . . . . 22
         |
354 | 353 | adantl 468 |
. . . . . . . . . . . . . . . . . . . . 21
   ..^          |
355 | 219, 308 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
   ..^          |
356 | 312 | adantl 468 |
. . . . . . . . . . . . . . . . . . . . . 22
   ..^            |
357 | 355, 316,
221, 356, 321 | letrd 9789 |
. . . . . . . . . . . . . . . . . . . . 21
   ..^          |
358 | 350, 354,
357 | jca32 538 |
. . . . . . . . . . . . . . . . . . . 20
   ..^                    |
359 | | elfz2 11788 |
. . . . . . . . . . . . . . . . . . . 20
      
 
            |
360 | 358, 359 | sylibr 216 |
. . . . . . . . . . . . . . . . . . 19
   ..^              |
361 | 360 | adantll 719 |
. . . . . . . . . . . . . . . . . 18
    ..^               |
362 | | ovex 6316 |
. . . . . . . . . . . . . . . . . . 19
   |
363 | | eleq1 2516 |
. . . . . . . . . . . . . . . . . . . . 21
       
         |
364 | 363 | anbi2d 709 |
. . . . . . . . . . . . . . . . . . . 20
    
    
           |
365 | | fveq2 5863 |
. . . . . . . . . . . . . . . . . . . . 21
               |
366 | 365 | feq1d 5712 |
. . . . . . . . . . . . . . . . . . . 20
           
             |
367 | 364, 366 | imbi12d 322 |
. . . . . . . . . . . . . . . . . . 19
     
             
                       |
368 | | nfv 1760 |
. . . . . . . . . . . . . . . . . . . . 21
         |
369 | | nfmpt1 4491 |
. . . . . . . . . . . . . . . . . . . . . . . 24
                 |
370 | 111, 369 | nfcxfr 2589 |
. . . . . . . . . . . . . . . . . . . . . . 23
   |
371 | | nfcv 2591 |
. . . . . . . . . . . . . . . . . . . . . . 23
   |
372 | 370, 371 | nffv 5870 |
. . . . . . . . . . . . . . . . . . . . . 22
       |
373 | | nfcv 2591 |
. . . . . . . . . . . . . . . . . . . . . 22
   |
374 | | nfcv 2591 |
. . . . . . . . . . . . . . . . . . . . . 22
   |
375 | 372, 373,
374 | nff 5722 |
. . . . . . . . . . . . . . . . . . . . 21
           |
376 | 368, 375 | nfim 2002 |
. . . . . . . . . . . . . . . . . . . 20
   
               |
377 | | fveq2 5863 |
. . . . . . . . . . . . . . . . . . . . . 22
           |
378 | 377 | feq1d 5712 |
. . . . . . . . . . . . . . . . . . . . 21
         
           |
379 | 281, 378 | imbi12d 322 |
. . . . . . . . . . . . . . . . . . . 20
   
             
                   |
380 | 376, 379,
240 | chvar 2105 |
. . . . . . . . . . . . . . . . . . 19
 
               |
381 | 362, 367,
380 | vtocl 3099 |
. . . . . . . . . . . . . . . . . 18
 
                   |
382 | 212, 361,
381 | syl2anc 666 |
. . . . . . . . . . . . . . . . 17
    ..^                   |
383 | 382 | ffvelrnda 6020 |
. . . . . . . . . . . . . . . 16
   
 ..^ 
     
            |
384 | 299 | 3expa 1207 |
. . . . . . . . . . . . . . . 16
   
 ..^ 
     
            |
385 | 383, 384 | mulcld 9660 |
. . . . . . . . . . . . . . 15
   
 ..^ 
     
                        |
386 | 345, 346 | mulcld 9660 |
. . . . . . . . . . . . . . 15
   
 ..^ 
     
                        |
387 | 385, 386 | addcld 9659 |
. . . . . . . . . . . . . 14
   
 ..^ 
     
                                                |
388 | 348, 387 | eqeltrrd 2529 |
. . . . . . . . . . . . 13
   
 ..^ 
     
                                                |
389 | 302, 388 | mulcld 9660 |
. . . . . . . . . . . 12
   
 ..^ 
     
                                                    |
390 | 389 | 3impa 1202 |
. . . . . . . . . . 11
    ..^     
                                                     |
391 | 212, 79 | syl 17 |
. . . . . . . . . . . . 13
    ..^            |
392 | 179 | a1i 11 |
. . . . . . . . . . . . 13
 |