Step | Hyp | Ref
| Expression |
1 | | fzofi 12187 |
. . . 4
 ..^  |
2 | 1 | a1i 11 |
. . 3
  ..^   |
3 | | dvfsumle.x |
. . 3
 
 ..^    |
4 | | dvfsumle.m |
. . . . . . . . . . 11
       |
5 | | eluzel2 11164 |
. . . . . . . . . . 11
    
  |
6 | 4, 5 | syl 17 |
. . . . . . . . . 10
   |
7 | | eluzelz 11168 |
. . . . . . . . . . 11
    
  |
8 | 4, 7 | syl 17 |
. . . . . . . . . 10
   |
9 | | fzval2 11787 |
. . . . . . . . . 10
 
        ![[,] [,]](_icc.gif)     |
10 | 6, 8, 9 | syl2anc 667 |
. . . . . . . . 9
        ![[,] [,]](_icc.gif)     |
11 | | inss1 3652 |
. . . . . . . . 9
   ![[,] [,]](_icc.gif)     ![[,] [,]](_icc.gif)   |
12 | 10, 11 | syl6eqss 3482 |
. . . . . . . 8
    
  ![[,] [,]](_icc.gif)    |
13 | 12 | sselda 3432 |
. . . . . . 7
 
    
  ![[,] [,]](_icc.gif)    |
14 | | dvfsumle.a |
. . . . . . . . . 10
    ![[,] [,]](_icc.gif)      ![[,] [,]](_icc.gif)       |
15 | | cncff 21925 |
. . . . . . . . . 10
    ![[,] [,]](_icc.gif)      ![[,] [,]](_icc.gif)        ![[,] [,]](_icc.gif)       ![[,] [,]](_icc.gif)      |
16 | 14, 15 | syl 17 |
. . . . . . . . 9
    ![[,] [,]](_icc.gif)       ![[,] [,]](_icc.gif)      |
17 | | eqid 2451 |
. . . . . . . . . 10
   ![[,] [,]](_icc.gif)      ![[,] [,]](_icc.gif)    |
18 | 17 | fmpt 6043 |
. . . . . . . . 9
 
  ![[,] [,]](_icc.gif)      ![[,] [,]](_icc.gif)       ![[,] [,]](_icc.gif)      |
19 | 16, 18 | sylibr 216 |
. . . . . . . 8
    ![[,] [,]](_icc.gif)     |
20 | | nfcsb1v 3379 |
. . . . . . . . . 10
  
 ![]_ ]_](_urbrack.gif)  |
21 | 20 | nfel1 2606 |
. . . . . . . . 9
  
 ![]_ ]_](_urbrack.gif)
 |
22 | | csbeq1a 3372 |
. . . . . . . . . 10
   ![]_ ]_](_urbrack.gif)   |
23 | 22 | eleq1d 2513 |
. . . . . . . . 9
 
  ![]_ ]_](_urbrack.gif)    |
24 | 21, 23 | rspc 3144 |
. . . . . . . 8
   ![[,] [,]](_icc.gif)   
  ![[,] [,]](_icc.gif)     ![]_ ]_](_urbrack.gif)    |
25 | 19, 24 | mpan9 472 |
. . . . . . 7
 
  ![[,] [,]](_icc.gif)  
  ![]_ ]_](_urbrack.gif)   |
26 | 13, 25 | syldan 473 |
. . . . . 6
 
    
  ![]_ ]_](_urbrack.gif)   |
27 | 26 | ralrimiva 2802 |
. . . . 5
         ![]_ ]_](_urbrack.gif)
  |
28 | | fzofzp1 12008 |
. . . . 5
  ..^
        |
29 | | csbeq1 3366 |
. . . . . . 7
     ![]_ ]_](_urbrack.gif)     ![]_ ]_](_urbrack.gif)   |
30 | 29 | eleq1d 2513 |
. . . . . 6
    
 ![]_ ]_](_urbrack.gif)
    ![]_ ]_](_urbrack.gif)
   |
31 | 30 | rspccva 3149 |
. . . . 5
          ![]_ ]_](_urbrack.gif)
           ![]_ ]_](_urbrack.gif)
  |
32 | 27, 28, 31 | syl2an 480 |
. . . 4
 
 ..^      ![]_ ]_](_urbrack.gif)
  |
33 | | elfzofz 11935 |
. . . . 5
  ..^
      |
34 | | csbeq1 3366 |
. . . . . . 7
   ![]_ ]_](_urbrack.gif)   ![]_ ]_](_urbrack.gif)   |
35 | 34 | eleq1d 2513 |
. . . . . 6
  
 ![]_ ]_](_urbrack.gif)
  ![]_ ]_](_urbrack.gif)
   |
36 | 35 | rspccva 3149 |
. . . . 5
          ![]_ ]_](_urbrack.gif)
       ![]_ ]_](_urbrack.gif)
  |
37 | 27, 33, 36 | syl2an 480 |
. . . 4
 
 ..^    ![]_ ]_](_urbrack.gif)
  |
38 | 32, 37 | resubcld 10047 |
. . 3
 
 ..^       ![]_ ]_](_urbrack.gif)   ![]_ ]_](_urbrack.gif)    |
39 | | elfzoelz 11920 |
. . . . . . . . . 10
  ..^
  |
40 | 39 | adantl 468 |
. . . . . . . . 9
 
 ..^    |
41 | 40 | zred 11040 |
. . . . . . . 8
 
 ..^    |
42 | 41 | recnd 9669 |
. . . . . . 7
 
 ..^    |
43 | | ax-1cn 9597 |
. . . . . . 7
 |
44 | | pncan2 9882 |
. . . . . . 7
 
       |
45 | 42, 43, 44 | sylancl 668 |
. . . . . 6
 
 ..^        |
46 | 45 | oveq2d 6306 |
. . . . 5
 
 ..^            |
47 | 3 | recnd 9669 |
. . . . . 6
 
 ..^    |
48 | | peano2re 9806 |
. . . . . . . 8
     |
49 | 41, 48 | syl 17 |
. . . . . . 7
 
 ..^      |
50 | 49 | recnd 9669 |
. . . . . 6
 
 ..^      |
51 | 47, 50, 42 | subdid 10074 |
. . . . 5
 
 ..^                  |
52 | 47 | mulid1d 9660 |
. . . . 5
 
 ..^      |
53 | 46, 51, 52 | 3eqtr3d 2493 |
. . . 4
 
 ..^       
    |
54 | | eqid 2451 |
. . . . . 6
  ℂfld   ℂfld |
55 | 54 | mulcn 21899 |
. . . . . 6
    ℂfld   ℂfld   ℂfld  |
56 | 6 | zred 11040 |
. . . . . . . . . . 11
   |
57 | 56 | adantr 467 |
. . . . . . . . . 10
 
 ..^    |
58 | 8 | zred 11040 |
. . . . . . . . . . 11
   |
59 | 58 | adantr 467 |
. . . . . . . . . 10
 
 ..^    |
60 | | elfzole1 11928 |
. . . . . . . . . . 11
  ..^
  |
61 | 60 | adantl 468 |
. . . . . . . . . 10
 
 ..^    |
62 | 28 | adantl 468 |
. . . . . . . . . . 11
 
 ..^          |
63 | | elfzle2 11803 |
. . . . . . . . . . 11
           |
64 | 62, 63 | syl 17 |
. . . . . . . . . 10
 
 ..^      |
65 | | iccss 11702 |
. . . . . . . . . 10
    
      ![[,] [,]](_icc.gif)   
  ![[,] [,]](_icc.gif)    |
66 | 57, 59, 61, 64, 65 | syl22anc 1269 |
. . . . . . . . 9
 
 ..^    ![[,] [,]](_icc.gif)      ![[,] [,]](_icc.gif)    |
67 | | iccssre 11716 |
. . . . . . . . . . 11
 
   ![[,] [,]](_icc.gif) 
  |
68 | 56, 58, 67 | syl2anc 667 |
. . . . . . . . . 10
   ![[,] [,]](_icc.gif) 
  |
69 | 68 | adantr 467 |
. . . . . . . . 9
 
 ..^    ![[,] [,]](_icc.gif)    |
70 | 66, 69 | sstrd 3442 |
. . . . . . . 8
 
 ..^    ![[,] [,]](_icc.gif)      |
71 | | ax-resscn 9596 |
. . . . . . . 8
 |
72 | 70, 71 | syl6ss 3444 |
. . . . . . 7
 
 ..^    ![[,] [,]](_icc.gif)      |
73 | 71 | a1i 11 |
. . . . . . 7
 
 ..^    |
74 | | cncfmptc 21943 |
. . . . . . 7
    ![[,] [,]](_icc.gif)   
    ![[,] [,]](_icc.gif)        ![[,] [,]](_icc.gif)         |
75 | 3, 72, 73, 74 | syl3anc 1268 |
. . . . . 6
 
 ..^     ![[,] [,]](_icc.gif)        ![[,] [,]](_icc.gif)         |
76 | | cncfmptid 21944 |
. . . . . . 7
    ![[,] [,]](_icc.gif)   
    ![[,] [,]](_icc.gif)        ![[,] [,]](_icc.gif)         |
77 | 70, 71, 76 | sylancl 668 |
. . . . . 6
 
 ..^     ![[,] [,]](_icc.gif)        ![[,] [,]](_icc.gif)         |
78 | | remulcl 9624 |
. . . . . 6
 
     |
79 | 54, 55, 75, 77, 71, 78 | cncfmpt2ss 21947 |
. . . . 5
 
 ..^     ![[,] [,]](_icc.gif)          ![[,] [,]](_icc.gif)         |
80 | | reelprrecn 9631 |
. . . . . . . 8
    |
81 | 80 | a1i 11 |
. . . . . . 7
 
 ..^   
   |
82 | 57 | rexrd 9690 |
. . . . . . . . . . 11
 
 ..^    |
83 | | iooss1 11671 |
. . . . . . . . . . 11
                 |
84 | 82, 61, 83 | syl2anc 667 |
. . . . . . . . . 10
 
 ..^                |
85 | 59 | rexrd 9690 |
. . . . . . . . . . 11
 
 ..^    |
86 | | iooss2 11672 |
. . . . . . . . . . 11
          
      |
87 | 85, 64, 86 | syl2anc 667 |
. . . . . . . . . 10
 
 ..^              |
88 | 84, 87 | sstrd 3442 |
. . . . . . . . 9
 
 ..^              |
89 | | ioossicc 11720 |
. . . . . . . . . 10
      ![[,] [,]](_icc.gif)   |
90 | 69, 71 | syl6ss 3444 |
. . . . . . . . . 10
 
 ..^    ![[,] [,]](_icc.gif)    |
91 | 89, 90 | syl5ss 3443 |
. . . . . . . . 9
 
 ..^        |
92 | 88, 91 | sstrd 3442 |
. . . . . . . 8
 
 ..^          |
93 | 92 | sselda 3432 |
. . . . . . 7
    ..^           |
94 | | 1cnd 9659 |
. . . . . . 7
    ..^           |
95 | 73 | sselda 3432 |
. . . . . . . 8
    ..^     |
96 | | 1cnd 9659 |
. . . . . . . 8
    ..^     |
97 | 81 | dvmptid 22911 |
. . . . . . . 8
 
 ..^          |
98 | | ioossre 11696 |
. . . . . . . . 9
       |
99 | 98 | a1i 11 |
. . . . . . . 8
 
 ..^          |
100 | 54 | tgioo2 21821 |
. . . . . . . 8
       ℂfld
↾t   |
101 | | iooretop 21786 |
. . . . . . . . 9
           |
102 | 101 | a1i 11 |
. . . . . . . 8
 
 ..^              |
103 | 81, 95, 96, 97, 99, 100, 54, 102 | dvmptres 22917 |
. . . . . . 7
 
 ..^                      |
104 | 81, 93, 94, 103, 47 | dvmptcmul 22918 |
. . . . . 6
 
 ..^                          |
105 | 52 | mpteq2dv 4490 |
. . . . . 6
 
 ..^                      |
106 | 104, 105 | eqtrd 2485 |
. . . . 5
 
 ..^                        |
107 | | nfcv 2592 |
. . . . . . 7
   |
108 | 107, 20, 22 | cbvmpt 4494 |
. . . . . 6
   ![[,] [,]](_icc.gif)        ![[,] [,]](_icc.gif)      ![]_ ]_](_urbrack.gif)   |
109 | 66 | resmptd 5156 |
. . . . . . 7
 
 ..^      ![[,] [,]](_icc.gif)     ![[,] [,]](_icc.gif)        ![[,] [,]](_icc.gif)       |
110 | 14 | adantr 467 |
. . . . . . . 8
 
 ..^     ![[,] [,]](_icc.gif)      ![[,] [,]](_icc.gif)       |
111 | | rescncf 21929 |
. . . . . . . 8
   ![[,] [,]](_icc.gif)      ![[,] [,]](_icc.gif)      ![[,] [,]](_icc.gif)      ![[,] [,]](_icc.gif)         ![[,] [,]](_icc.gif)     ![[,] [,]](_icc.gif)        ![[,] [,]](_icc.gif)          |
112 | 66, 110, 111 | sylc 62 |
. . . . . . 7
 
 ..^      ![[,] [,]](_icc.gif)     ![[,] [,]](_icc.gif)        ![[,] [,]](_icc.gif)         |
113 | 109, 112 | eqeltrrd 2530 |
. . . . . 6
 
 ..^     ![[,] [,]](_icc.gif)        ![[,] [,]](_icc.gif)         |
114 | 108, 113 | syl5eqelr 2534 |
. . . . 5
 
 ..^     ![[,] [,]](_icc.gif)      ![]_ ]_](_urbrack.gif)     ![[,] [,]](_icc.gif)         |
115 | 16 | adantr 467 |
. . . . . . . . 9
 
 ..^     ![[,] [,]](_icc.gif)       ![[,] [,]](_icc.gif)      |
116 | 115, 18 | sylibr 216 |
. . . . . . . 8
 
 ..^     ![[,] [,]](_icc.gif)     |
117 | 89 | sseli 3428 |
. . . . . . . 8
       ![[,] [,]](_icc.gif)    |
118 | 24 | impcom 432 |
. . . . . . . 8
     ![[,] [,]](_icc.gif)  
  ![[,] [,]](_icc.gif)   
 ![]_ ]_](_urbrack.gif)
  |
119 | 116, 117,
118 | syl2an 480 |
. . . . . . 7
    ..^         ![]_ ]_](_urbrack.gif)   |
120 | 119 | recnd 9669 |
. . . . . 6
    ..^         ![]_ ]_](_urbrack.gif)   |
121 | 89 | sseli 3428 |
. . . . . . . . . . . 12
       ![[,] [,]](_icc.gif)    |
122 | 19 | r19.21bi 2757 |
. . . . . . . . . . . . 13
 
  ![[,] [,]](_icc.gif)  
  |
123 | 122 | adantlr 721 |
. . . . . . . . . . . 12
    ..^    ![[,] [,]](_icc.gif)     |
124 | 121, 123 | sylan2 477 |
. . . . . . . . . . 11
    ..^         |
125 | | eqid 2451 |
. . . . . . . . . . 11
             |
126 | 124, 125 | fmptd 6046 |
. . . . . . . . . 10
 
 ..^                  |
127 | | ioossre 11696 |
. . . . . . . . . 10
     |
128 | | dvfre 22905 |
. . . . . . . . . 10
                    
                      |
129 | 126, 127,
128 | sylancl 668 |
. . . . . . . . 9
 
 ..^   
        
           |
130 | | dvfsumle.b |
. . . . . . . . . . 11
                 |
131 | 130 | adantr 467 |
. . . . . . . . . 10
 
 ..^   
              |
132 | 131 | dmeqd 5037 |
. . . . . . . . . . 11
 
 ..^ 
                |
133 | | dvfsumle.v |
. . . . . . . . . . . . . 14
 
    
  |
134 | 133 | adantlr 721 |
. . . . . . . . . . . . 13
    ..^         |
135 | 134 | ralrimiva 2802 |
. . . . . . . . . . . 12
 
 ..^          |
136 | | dmmptg 5332 |
. . . . . . . . . . . 12
 
    
            |
137 | 135, 136 | syl 17 |
. . . . . . . . . . 11
 
 ..^ 
            |
138 | 132, 137 | eqtrd 2485 |
. . . . . . . . . 10
 
 ..^ 
              |
139 | 131, 138 | feq12d 5717 |
. . . . . . . . 9
 
 ..^                                        |
140 | 129, 139 | mpbid 214 |
. . . . . . . 8
 
 ..^                  |
141 | | eqid 2451 |
. . . . . . . . 9
             |
142 | 141 | fmpt 6043 |
. . . . . . . 8
 
                     |
143 | 140, 142 | sylibr 216 |
. . . . . . 7
 
 ..^          |
144 | | nfcsb1v 3379 |
. . . . . . . . 9
  
 ![]_ ]_](_urbrack.gif)  |
145 | 144 | nfel1 2606 |
. . . . . . . 8
  
 ![]_ ]_](_urbrack.gif)
 |
146 | | csbeq1a 3372 |
. . . . . . . . 9
   ![]_ ]_](_urbrack.gif)   |
147 | 146 | eleq1d 2513 |
. . . . . . . 8
 
  ![]_ ]_](_urbrack.gif)    |
148 | 145, 147 | rspc 3144 |
. . . . . . 7
      
       ![]_ ]_](_urbrack.gif)    |
149 | 143, 148 | mpan9 472 |
. . . . . 6
    ..^         ![]_ ]_](_urbrack.gif)   |
150 | 107, 20, 22 | cbvmpt 4494 |
. . . . . . . 8
             ![]_ ]_](_urbrack.gif)   |
151 | 150 | oveq2i 6301 |
. . . . . . 7
                ![]_ ]_](_urbrack.gif)    |
152 | | nfcv 2592 |
. . . . . . . 8
   |
153 | 152, 144,
146 | cbvmpt 4494 |
. . . . . . 7
             ![]_ ]_](_urbrack.gif)   |
154 | 131, 151,
153 | 3eqtr3g 2508 |
. . . . . 6
 
 ..^          ![]_ ]_](_urbrack.gif)          ![]_ ]_](_urbrack.gif)    |
155 | 81, 120, 149, 154, 88, 100, 54, 102 | dvmptres 22917 |
. . . . 5
 
 ..^            ![]_ ]_](_urbrack.gif)            ![]_ ]_](_urbrack.gif)    |
156 | | dvfsumle.l |
. . . . . . . 8
 
  ..^           |
157 | 156 | anassrs 654 |
. . . . . . 7
    ..^           |
158 | 157 | ralrimiva 2802 |
. . . . . 6
 
 ..^         
  |
159 | | nfcv 2592 |
. . . . . . . 8
   |
160 | | nfcv 2592 |
. . . . . . . 8
  |
161 | 159, 160,
144 | nfbr 4447 |
. . . . . . 7
   ![]_ ]_](_urbrack.gif)  |
162 | 146 | breq2d 4414 |
. . . . . . 7
 
  ![]_ ]_](_urbrack.gif)    |
163 | 161, 162 | rspc 3144 |
. . . . . 6
        
      
  ![]_ ]_](_urbrack.gif)    |
164 | 158, 163 | mpan9 472 |
. . . . 5
    ..^           ![]_ ]_](_urbrack.gif)   |
165 | 41 | rexrd 9690 |
. . . . . 6
 
 ..^    |
166 | 49 | rexrd 9690 |
. . . . . 6
 
 ..^      |
167 | 41 | lep1d 10538 |
. . . . . 6
 
 ..^      |
168 | | lbicc2 11748 |
. . . . . 6
   
     ![[,] [,]](_icc.gif)      |
169 | 165, 166,
167, 168 | syl3anc 1268 |
. . . . 5
 
 ..^    ![[,] [,]](_icc.gif)      |
170 | | ubicc2 11749 |
. . . . . 6
   
       ![[,] [,]](_icc.gif)      |
171 | 165, 166,
167, 170 | syl3anc 1268 |
. . . . 5
 
 ..^      ![[,] [,]](_icc.gif)      |
172 | | oveq2 6298 |
. . . . 5
 
     |
173 | | oveq2 6298 |
. . . . 5
   
       |
174 | 41, 49, 79, 106, 114, 155, 164, 169, 171, 167, 172, 34, 173, 29 | dvle 22959 |
. . . 4
 
 ..^       
       ![]_ ]_](_urbrack.gif)
  ![]_ ]_](_urbrack.gif)    |
175 | 53, 174 | eqbrtrrd 4425 |
. . 3
 
 ..^       ![]_ ]_](_urbrack.gif)
  ![]_ ]_](_urbrack.gif)    |
176 | 2, 3, 38, 175 | fsumle 13859 |
. 2
   ..^    ..^       ![]_ ]_](_urbrack.gif)
  ![]_ ]_](_urbrack.gif)    |
177 | | vex 3048 |
. . . . 5
 |
178 | 177 | a1i 11 |
. . . 4
   |
179 | | eqeq2 2462 |
. . . . . 6
 
   |
180 | 179 | biimpa 487 |
. . . . 5
 
   |
181 | | dvfsumle.c |
. . . . 5
   |
182 | 180, 181 | syl 17 |
. . . 4
 
   |
183 | 178, 182 | csbied 3390 |
. . 3
   ![]_ ]_](_urbrack.gif)   |
184 | 177 | a1i 11 |
. . . 4
   |
185 | | eqeq2 2462 |
. . . . . 6
 
   |
186 | 185 | biimpa 487 |
. . . . 5
 
   |
187 | | dvfsumle.d |
. . . . 5
   |
188 | 186, 187 | syl 17 |
. . . 4
 
   |
189 | 184, 188 | csbied 3390 |
. . 3
   ![]_ ]_](_urbrack.gif)   |
190 | 26 | recnd 9669 |
. . 3
 
    
  ![]_ ]_](_urbrack.gif)   |
191 | 34, 29, 183, 189, 4, 190 | telfsumo2 13863 |
. 2
   ..^       ![]_ ]_](_urbrack.gif)
  ![]_ ]_](_urbrack.gif)      |
192 | 176, 191 | breqtrd 4427 |
1
   ..^      |