Step | Hyp | Ref
| Expression |
1 | | fzofi 12773 |
. . . 4
..^ |
2 | 1 | a1i 11 |
. . 3
..^ |
3 | | dvfsumle.x |
. . 3
..^ |
4 | | dvfsumle.m |
. . . . . . . . . . 11
|
5 | | eluzel2 11692 |
. . . . . . . . . . 11
|
6 | 4, 5 | syl 17 |
. . . . . . . . . 10
|
7 | | eluzelz 11697 |
. . . . . . . . . . 11
|
8 | 4, 7 | syl 17 |
. . . . . . . . . 10
|
9 | | fzval2 12329 |
. . . . . . . . . 10
|
10 | 6, 8, 9 | syl2anc 693 |
. . . . . . . . 9
|
11 | | inss1 3833 |
. . . . . . . . 9
|
12 | 10, 11 | syl6eqss 3655 |
. . . . . . . 8
|
13 | 12 | sselda 3603 |
. . . . . . 7
|
14 | | dvfsumle.a |
. . . . . . . . . 10
|
15 | | cncff 22696 |
. . . . . . . . . 10
|
16 | 14, 15 | syl 17 |
. . . . . . . . 9
|
17 | | eqid 2622 |
. . . . . . . . . 10
|
18 | 17 | fmpt 6381 |
. . . . . . . . 9
|
19 | 16, 18 | sylibr 224 |
. . . . . . . 8
|
20 | | nfcsb1v 3549 |
. . . . . . . . . 10
|
21 | 20 | nfel1 2779 |
. . . . . . . . 9
|
22 | | csbeq1a 3542 |
. . . . . . . . . 10
|
23 | 22 | eleq1d 2686 |
. . . . . . . . 9
|
24 | 21, 23 | rspc 3303 |
. . . . . . . 8
|
25 | 19, 24 | mpan9 486 |
. . . . . . 7
|
26 | 13, 25 | syldan 487 |
. . . . . 6
|
27 | 26 | ralrimiva 2966 |
. . . . 5
|
28 | | fzofzp1 12565 |
. . . . 5
..^
|
29 | | csbeq1 3536 |
. . . . . . 7
|
30 | 29 | eleq1d 2686 |
. . . . . 6
|
31 | 30 | rspccva 3308 |
. . . . 5
|
32 | 27, 28, 31 | syl2an 494 |
. . . 4
..^
|
33 | | elfzofz 12485 |
. . . . 5
..^
|
34 | | csbeq1 3536 |
. . . . . . 7
|
35 | 34 | eleq1d 2686 |
. . . . . 6
|
36 | 35 | rspccva 3308 |
. . . . 5
|
37 | 27, 33, 36 | syl2an 494 |
. . . 4
..^
|
38 | 32, 37 | resubcld 10458 |
. . 3
..^ |
39 | | elfzoelz 12470 |
. . . . . . . . . 10
..^
|
40 | 39 | adantl 482 |
. . . . . . . . 9
..^ |
41 | 40 | zred 11482 |
. . . . . . . 8
..^ |
42 | 41 | recnd 10068 |
. . . . . . 7
..^ |
43 | | ax-1cn 9994 |
. . . . . . 7
|
44 | | pncan2 10288 |
. . . . . . 7
|
45 | 42, 43, 44 | sylancl 694 |
. . . . . 6
..^ |
46 | 45 | oveq2d 6666 |
. . . . 5
..^ |
47 | 3 | recnd 10068 |
. . . . . 6
..^ |
48 | | peano2re 10209 |
. . . . . . . 8
|
49 | 41, 48 | syl 17 |
. . . . . . 7
..^ |
50 | 49 | recnd 10068 |
. . . . . 6
..^ |
51 | 47, 50, 42 | subdid 10486 |
. . . . 5
..^ |
52 | 47 | mulid1d 10057 |
. . . . 5
..^ |
53 | 46, 51, 52 | 3eqtr3d 2664 |
. . . 4
..^
|
54 | | eqid 2622 |
. . . . . 6
ℂfld ℂfld |
55 | 54 | mulcn 22670 |
. . . . . 6
ℂfld ℂfld ℂfld |
56 | 6 | zred 11482 |
. . . . . . . . . . 11
|
57 | 56 | adantr 481 |
. . . . . . . . . 10
..^ |
58 | 8 | zred 11482 |
. . . . . . . . . . 11
|
59 | 58 | adantr 481 |
. . . . . . . . . 10
..^ |
60 | | elfzole1 12478 |
. . . . . . . . . . 11
..^
|
61 | 60 | adantl 482 |
. . . . . . . . . 10
..^ |
62 | 28 | adantl 482 |
. . . . . . . . . . 11
..^ |
63 | | elfzle2 12345 |
. . . . . . . . . . 11
|
64 | 62, 63 | syl 17 |
. . . . . . . . . 10
..^ |
65 | | iccss 12241 |
. . . . . . . . . 10
|
66 | 57, 59, 61, 64, 65 | syl22anc 1327 |
. . . . . . . . 9
..^ |
67 | | iccssre 12255 |
. . . . . . . . . . 11
|
68 | 56, 58, 67 | syl2anc 693 |
. . . . . . . . . 10
|
69 | 68 | adantr 481 |
. . . . . . . . 9
..^ |
70 | 66, 69 | sstrd 3613 |
. . . . . . . 8
..^ |
71 | | ax-resscn 9993 |
. . . . . . . 8
|
72 | 70, 71 | syl6ss 3615 |
. . . . . . 7
..^ |
73 | 71 | a1i 11 |
. . . . . . 7
..^ |
74 | | cncfmptc 22714 |
. . . . . . 7
|
75 | 3, 72, 73, 74 | syl3anc 1326 |
. . . . . 6
..^ |
76 | | cncfmptid 22715 |
. . . . . . 7
|
77 | 70, 71, 76 | sylancl 694 |
. . . . . 6
..^ |
78 | | remulcl 10021 |
. . . . . 6
|
79 | 54, 55, 75, 77, 71, 78 | cncfmpt2ss 22718 |
. . . . 5
..^ |
80 | | reelprrecn 10028 |
. . . . . . . 8
|
81 | 80 | a1i 11 |
. . . . . . 7
..^
|
82 | 57 | rexrd 10089 |
. . . . . . . . . . 11
..^ |
83 | | iooss1 12210 |
. . . . . . . . . . 11
|
84 | 82, 61, 83 | syl2anc 693 |
. . . . . . . . . 10
..^ |
85 | 59 | rexrd 10089 |
. . . . . . . . . . 11
..^ |
86 | | iooss2 12211 |
. . . . . . . . . . 11
|
87 | 85, 64, 86 | syl2anc 693 |
. . . . . . . . . 10
..^ |
88 | 84, 87 | sstrd 3613 |
. . . . . . . . 9
..^ |
89 | | ioossicc 12259 |
. . . . . . . . . 10
|
90 | 69, 71 | syl6ss 3615 |
. . . . . . . . . 10
..^ |
91 | 89, 90 | syl5ss 3614 |
. . . . . . . . 9
..^ |
92 | 88, 91 | sstrd 3613 |
. . . . . . . 8
..^ |
93 | 92 | sselda 3603 |
. . . . . . 7
..^ |
94 | | 1cnd 10056 |
. . . . . . 7
..^ |
95 | 73 | sselda 3603 |
. . . . . . . 8
..^ |
96 | | 1cnd 10056 |
. . . . . . . 8
..^ |
97 | 81 | dvmptid 23720 |
. . . . . . . 8
..^ |
98 | | ioossre 12235 |
. . . . . . . . 9
|
99 | 98 | a1i 11 |
. . . . . . . 8
..^ |
100 | 54 | tgioo2 22606 |
. . . . . . . 8
ℂfld
↾t |
101 | | iooretop 22569 |
. . . . . . . . 9
|
102 | 101 | a1i 11 |
. . . . . . . 8
..^ |
103 | 81, 95, 96, 97, 99, 100, 54, 102 | dvmptres 23726 |
. . . . . . 7
..^ |
104 | 81, 93, 94, 103, 47 | dvmptcmul 23727 |
. . . . . 6
..^ |
105 | 52 | mpteq2dv 4745 |
. . . . . 6
..^ |
106 | 104, 105 | eqtrd 2656 |
. . . . 5
..^ |
107 | | nfcv 2764 |
. . . . . . 7
|
108 | 107, 20, 22 | cbvmpt 4749 |
. . . . . 6
|
109 | 66 | resmptd 5452 |
. . . . . . 7
..^ |
110 | 14 | adantr 481 |
. . . . . . . 8
..^ |
111 | | rescncf 22700 |
. . . . . . . 8
|
112 | 66, 110, 111 | sylc 65 |
. . . . . . 7
..^ |
113 | 109, 112 | eqeltrrd 2702 |
. . . . . 6
..^ |
114 | 108, 113 | syl5eqelr 2706 |
. . . . 5
..^ |
115 | 16 | adantr 481 |
. . . . . . . . 9
..^ |
116 | 115, 18 | sylibr 224 |
. . . . . . . 8
..^ |
117 | 89 | sseli 3599 |
. . . . . . . 8
|
118 | 24 | impcom 446 |
. . . . . . . 8
|
119 | 116, 117,
118 | syl2an 494 |
. . . . . . 7
..^ |
120 | 119 | recnd 10068 |
. . . . . 6
..^ |
121 | 89 | sseli 3599 |
. . . . . . . . . . . 12
|
122 | 19 | r19.21bi 2932 |
. . . . . . . . . . . . 13
|
123 | 122 | adantlr 751 |
. . . . . . . . . . . 12
..^ |
124 | 121, 123 | sylan2 491 |
. . . . . . . . . . 11
..^ |
125 | | eqid 2622 |
. . . . . . . . . . 11
|
126 | 124, 125 | fmptd 6385 |
. . . . . . . . . 10
..^ |
127 | | ioossre 12235 |
. . . . . . . . . 10
|
128 | | dvfre 23714 |
. . . . . . . . . 10
|
129 | 126, 127,
128 | sylancl 694 |
. . . . . . . . 9
..^
|
130 | | dvfsumle.b |
. . . . . . . . . . 11
|
131 | 130 | adantr 481 |
. . . . . . . . . 10
..^
|
132 | 131 | dmeqd 5326 |
. . . . . . . . . . 11
..^
|
133 | | dvfsumle.v |
. . . . . . . . . . . . . 14
|
134 | 133 | adantlr 751 |
. . . . . . . . . . . . 13
..^ |
135 | 134 | ralrimiva 2966 |
. . . . . . . . . . . 12
..^ |
136 | | dmmptg 5632 |
. . . . . . . . . . . 12
|
137 | 135, 136 | syl 17 |
. . . . . . . . . . 11
..^
|
138 | 132, 137 | eqtrd 2656 |
. . . . . . . . . 10
..^
|
139 | 131, 138 | feq12d 6033 |
. . . . . . . . 9
..^ |
140 | 129, 139 | mpbid 222 |
. . . . . . . 8
..^ |
141 | | eqid 2622 |
. . . . . . . . 9
|
142 | 141 | fmpt 6381 |
. . . . . . . 8
|
143 | 140, 142 | sylibr 224 |
. . . . . . 7
..^ |
144 | | nfcsb1v 3549 |
. . . . . . . . 9
|
145 | 144 | nfel1 2779 |
. . . . . . . 8
|
146 | | csbeq1a 3542 |
. . . . . . . . 9
|
147 | 146 | eleq1d 2686 |
. . . . . . . 8
|
148 | 145, 147 | rspc 3303 |
. . . . . . 7
|
149 | 143, 148 | mpan9 486 |
. . . . . 6
..^ |
150 | 107, 20, 22 | cbvmpt 4749 |
. . . . . . . 8
|
151 | 150 | oveq2i 6661 |
. . . . . . 7
|
152 | | nfcv 2764 |
. . . . . . . 8
|
153 | 152, 144,
146 | cbvmpt 4749 |
. . . . . . 7
|
154 | 131, 151,
153 | 3eqtr3g 2679 |
. . . . . 6
..^ |
155 | 81, 120, 149, 154, 88, 100, 54, 102 | dvmptres 23726 |
. . . . 5
..^ |
156 | | dvfsumle.l |
. . . . . . . 8
..^ |
157 | 156 | anassrs 680 |
. . . . . . 7
..^ |
158 | 157 | ralrimiva 2966 |
. . . . . 6
..^
|
159 | | nfcv 2764 |
. . . . . . . 8
|
160 | | nfcv 2764 |
. . . . . . . 8
|
161 | 159, 160,
144 | nfbr 4699 |
. . . . . . 7
|
162 | 146 | breq2d 4665 |
. . . . . . 7
|
163 | 161, 162 | rspc 3303 |
. . . . . 6
|
164 | 158, 163 | mpan9 486 |
. . . . 5
..^ |
165 | 41 | rexrd 10089 |
. . . . . 6
..^ |
166 | 49 | rexrd 10089 |
. . . . . 6
..^ |
167 | 41 | lep1d 10955 |
. . . . . 6
..^ |
168 | | lbicc2 12288 |
. . . . . 6
|
169 | 165, 166,
167, 168 | syl3anc 1326 |
. . . . 5
..^ |
170 | | ubicc2 12289 |
. . . . . 6
|
171 | 165, 166,
167, 170 | syl3anc 1326 |
. . . . 5
..^ |
172 | | oveq2 6658 |
. . . . 5
|
173 | | oveq2 6658 |
. . . . 5
|
174 | 41, 49, 79, 106, 114, 155, 164, 169, 171, 167, 172, 34, 173, 29 | dvle 23770 |
. . . 4
..^
|
175 | 53, 174 | eqbrtrrd 4677 |
. . 3
..^
|
176 | 2, 3, 38, 175 | fsumle 14531 |
. 2
..^ ..^
|
177 | | vex 3203 |
. . . . 5
|
178 | 177 | a1i 11 |
. . . 4
|
179 | | eqeq2 2633 |
. . . . . 6
|
180 | 179 | biimpa 501 |
. . . . 5
|
181 | | dvfsumle.c |
. . . . 5
|
182 | 180, 181 | syl 17 |
. . . 4
|
183 | 178, 182 | csbied 3560 |
. . 3
|
184 | 177 | a1i 11 |
. . . 4
|
185 | | eqeq2 2633 |
. . . . . 6
|
186 | 185 | biimpa 501 |
. . . . 5
|
187 | | dvfsumle.d |
. . . . 5
|
188 | 186, 187 | syl 17 |
. . . 4
|
189 | 184, 188 | csbied 3560 |
. . 3
|
190 | 26 | recnd 10068 |
. . 3
|
191 | 34, 29, 183, 189, 4, 190 | telfsumo2 14535 |
. 2
..^
|
192 | 176, 191 | breqtrd 4679 |
1
..^ |