Step | Hyp | Ref
| Expression |
1 | | fsumss.1 |
. . . . . 6
|
2 | | sseq0 3455 |
. . . . . 6
|
3 | 1, 2 | sylan 281 |
. . . . 5
|
4 | 3 | sumeq1d 11316 |
. . . 4
|
5 | | simpr 109 |
. . . . 5
|
6 | 5 | sumeq1d 11316 |
. . . 4
|
7 | 4, 6 | eqtr4d 2206 |
. . 3
|
8 | 7 | ex 114 |
. 2
|
9 | | cnvimass 4972 |
. . . . . . . . 9
|
10 | | simprr 527 |
. . . . . . . . . 10
♯ ♯ ♯ |
11 | | f1of 5440 |
. . . . . . . . . 10
♯ ♯ |
12 | 10, 11 | syl 14 |
. . . . . . . . 9
♯ ♯ ♯ |
13 | 9, 12 | fssdm 5360 |
. . . . . . . 8
♯ ♯ ♯ |
14 | 12 | ffnd 5346 |
. . . . . . . . . . . 12
♯ ♯ ♯ |
15 | | elpreima 5612 |
. . . . . . . . . . . 12
♯
♯ |
16 | 14, 15 | syl 14 |
. . . . . . . . . . 11
♯ ♯ ♯ |
17 | 12 | ffvelrnda 5628 |
. . . . . . . . . . . . 13
♯ ♯ ♯ |
18 | 17 | ex 114 |
. . . . . . . . . . . 12
♯ ♯ ♯ |
19 | 18 | adantrd 277 |
. . . . . . . . . . 11
♯ ♯ ♯ |
20 | 16, 19 | sylbid 149 |
. . . . . . . . . 10
♯ ♯
|
21 | 20 | imp 123 |
. . . . . . . . 9
♯ ♯ |
22 | | fsumss.2 |
. . . . . . . . . . . . . . 15
|
23 | 22 | ex 114 |
. . . . . . . . . . . . . 14
|
24 | 23 | adantr 274 |
. . . . . . . . . . . . 13
|
25 | | eldif 3130 |
. . . . . . . . . . . . . . 15
|
26 | | fsumss.3 |
. . . . . . . . . . . . . . . 16
|
27 | | 0cn 7899 |
. . . . . . . . . . . . . . . 16
|
28 | 26, 27 | eqeltrdi 2261 |
. . . . . . . . . . . . . . 15
|
29 | 25, 28 | sylan2br 286 |
. . . . . . . . . . . . . 14
|
30 | 29 | expr 373 |
. . . . . . . . . . . . 13
|
31 | | eleq1w 2231 |
. . . . . . . . . . . . . . . 16
|
32 | 31 | dcbid 833 |
. . . . . . . . . . . . . . 15
DECID
DECID
|
33 | | fisumss.adc |
. . . . . . . . . . . . . . . 16
DECID |
34 | 33 | adantr 274 |
. . . . . . . . . . . . . . 15
DECID
|
35 | | simpr 109 |
. . . . . . . . . . . . . . 15
|
36 | 32, 34, 35 | rspcdva 2839 |
. . . . . . . . . . . . . 14
DECID
|
37 | | exmiddc 831 |
. . . . . . . . . . . . . 14
DECID
|
38 | 36, 37 | syl 14 |
. . . . . . . . . . . . 13
|
39 | 24, 30, 38 | mpjaod 713 |
. . . . . . . . . . . 12
|
40 | 39 | fmpttd 5648 |
. . . . . . . . . . 11
|
41 | 40 | adantr 274 |
. . . . . . . . . 10
♯ ♯ |
42 | 41 | ffvelrnda 5628 |
. . . . . . . . 9
♯ ♯ |
43 | 21, 42 | syldan 280 |
. . . . . . . 8
♯ ♯ |
44 | | eldifi 3249 |
. . . . . . . . . . . 12
♯ ♯ |
45 | 44, 17 | sylan2 284 |
. . . . . . . . . . 11
♯ ♯ ♯
|
46 | | eldifn 3250 |
. . . . . . . . . . . . 13
♯
|
47 | 46 | adantl 275 |
. . . . . . . . . . . 12
♯ ♯ ♯
|
48 | 16 | adantr 274 |
. . . . . . . . . . . . 13
♯ ♯ ♯
♯ |
49 | 44 | adantl 275 |
. . . . . . . . . . . . . 14
♯ ♯ ♯
♯ |
50 | 49 | biantrurd 303 |
. . . . . . . . . . . . 13
♯ ♯ ♯
♯ |
51 | 48, 50 | bitr4d 190 |
. . . . . . . . . . . 12
♯ ♯ ♯
|
52 | 47, 51 | mtbid 667 |
. . . . . . . . . . 11
♯ ♯ ♯
|
53 | 45, 52 | eldifd 3131 |
. . . . . . . . . 10
♯ ♯ ♯
|
54 | | difss 3253 |
. . . . . . . . . . . . 13
|
55 | | resmpt 4937 |
. . . . . . . . . . . . 13
|
56 | 54, 55 | ax-mp 5 |
. . . . . . . . . . . 12
|
57 | 56 | fveq1i 5495 |
. . . . . . . . . . 11
|
58 | | fvres 5518 |
. . . . . . . . . . 11
|
59 | 57, 58 | eqtr3id 2217 |
. . . . . . . . . 10
|
60 | 53, 59 | syl 14 |
. . . . . . . . 9
♯ ♯ ♯
|
61 | | c0ex 7901 |
. . . . . . . . . . . . . . 15
|
62 | 61 | elsn2 3615 |
. . . . . . . . . . . . . 14
|
63 | 26, 62 | sylibr 133 |
. . . . . . . . . . . . 13
|
64 | 63 | fmpttd 5648 |
. . . . . . . . . . . 12
|
65 | 64 | ad2antrr 485 |
. . . . . . . . . . 11
♯ ♯ ♯
|
66 | 65, 53 | ffvelrnd 5629 |
. . . . . . . . . 10
♯ ♯ ♯
|
67 | | elsni 3599 |
. . . . . . . . . 10
|
68 | 66, 67 | syl 14 |
. . . . . . . . 9
♯ ♯ ♯
|
69 | 60, 68 | eqtr3d 2205 |
. . . . . . . 8
♯ ♯ ♯
|
70 | | eleq1 2233 |
. . . . . . . . . . . . 13
|
71 | 70 | dcbid 833 |
. . . . . . . . . . . 12
DECID
DECID |
72 | 33 | ad3antrrr 489 |
. . . . . . . . . . . 12
♯ ♯
♯ DECID |
73 | 12 | ad2antrr 485 |
. . . . . . . . . . . . 13
♯ ♯
♯ ♯ |
74 | | simpr 109 |
. . . . . . . . . . . . 13
♯ ♯
♯ ♯ |
75 | 73, 74 | ffvelrnd 5629 |
. . . . . . . . . . . 12
♯ ♯
♯ |
76 | 71, 72, 75 | rspcdva 2839 |
. . . . . . . . . . 11
♯ ♯
♯ DECID |
77 | 10 | ad2antrr 485 |
. . . . . . . . . . . . . 14
♯ ♯
♯ ♯ |
78 | | f1ofun 5442 |
. . . . . . . . . . . . . 14
♯
|
79 | 77, 78 | syl 14 |
. . . . . . . . . . . . 13
♯ ♯
♯
|
80 | | f1odm 5444 |
. . . . . . . . . . . . . . 15
♯
♯ |
81 | 77, 80 | syl 14 |
. . . . . . . . . . . . . 14
♯ ♯
♯
♯ |
82 | 74, 81 | eleqtrrd 2250 |
. . . . . . . . . . . . 13
♯ ♯
♯ |
83 | | fvimacnv 5608 |
. . . . . . . . . . . . 13
|
84 | 79, 82, 83 | syl2anc 409 |
. . . . . . . . . . . 12
♯ ♯
♯
|
85 | 84 | dcbid 833 |
. . . . . . . . . . 11
♯ ♯
♯ DECID
DECID
|
86 | 76, 85 | mpbid 146 |
. . . . . . . . . 10
♯ ♯
♯ DECID |
87 | | elpreima 5612 |
. . . . . . . . . . . . . . . . 17
♯
♯ |
88 | | simpl 108 |
. . . . . . . . . . . . . . . . 17
♯ ♯ |
89 | 87, 88 | syl6bi 162 |
. . . . . . . . . . . . . . . 16
♯
♯ |
90 | 89 | con3d 626 |
. . . . . . . . . . . . . . 15
♯
♯
|
91 | 14, 90 | syl 14 |
. . . . . . . . . . . . . 14
♯ ♯ ♯
|
92 | 91 | adantr 274 |
. . . . . . . . . . . . 13
♯ ♯
♯
|
93 | 92 | imp 123 |
. . . . . . . . . . . 12
♯ ♯
♯
|
94 | 93 | olcd 729 |
. . . . . . . . . . 11
♯ ♯
♯
|
95 | | df-dc 830 |
. . . . . . . . . . 11
DECID
|
96 | 94, 95 | sylibr 133 |
. . . . . . . . . 10
♯ ♯
♯ DECID |
97 | | eluzelz 9483 |
. . . . . . . . . . . . 13
|
98 | 97 | adantl 275 |
. . . . . . . . . . . 12
♯ ♯
|
99 | | 1zzd 9226 |
. . . . . . . . . . . 12
♯ ♯
|
100 | | simplrl 530 |
. . . . . . . . . . . . 13
♯ ♯
♯ |
101 | 100 | nnzd 9320 |
. . . . . . . . . . . 12
♯ ♯
♯ |
102 | | fzdcel 9983 |
. . . . . . . . . . . 12
♯ DECID ♯ |
103 | 98, 99, 101, 102 | syl3anc 1233 |
. . . . . . . . . . 11
♯ ♯
DECID
♯ |
104 | | exmiddc 831 |
. . . . . . . . . . 11
DECID ♯ ♯
♯ |
105 | 103, 104 | syl 14 |
. . . . . . . . . 10
♯ ♯
♯ ♯ |
106 | 86, 96, 105 | mpjaodan 793 |
. . . . . . . . 9
♯ ♯
DECID
|
107 | 106 | ralrimiva 2543 |
. . . . . . . 8
♯ ♯
DECID |
108 | | 1zzd 9226 |
. . . . . . . 8
♯ ♯ |
109 | | fzssuz 10008 |
. . . . . . . . 9
♯ |
110 | 109 | a1i 9 |
. . . . . . . 8
♯ ♯ ♯ |
111 | 103 | ralrimiva 2543 |
. . . . . . . 8
♯ ♯
DECID ♯ |
112 | 13, 43, 69, 107, 108, 110, 111 | isumss 11341 |
. . . . . . 7
♯ ♯ ♯ |
113 | 1 | ad2antrr 485 |
. . . . . . . . . . . 12
♯ ♯ |
114 | 113 | resmptd 4940 |
. . . . . . . . . . 11
♯ ♯ |
115 | 114 | fveq1d 5496 |
. . . . . . . . . 10
♯ ♯ |
116 | | fvres 5518 |
. . . . . . . . . . 11
|
117 | 116 | adantl 275 |
. . . . . . . . . 10
♯ ♯ |
118 | 115, 117 | eqtr3d 2205 |
. . . . . . . . 9
♯ ♯ |
119 | 118 | sumeq2dv 11318 |
. . . . . . . 8
♯ ♯
|
120 | | fveq2 5494 |
. . . . . . . . 9
|
121 | 1 | adantr 274 |
. . . . . . . . . 10
♯ ♯ |
122 | | fsumss.4 |
. . . . . . . . . . . 12
|
123 | | ssfidc 6908 |
. . . . . . . . . . . 12
DECID
|
124 | 122, 1, 33, 123 | syl3anc 1233 |
. . . . . . . . . . 11
|
125 | 124 | adantr 274 |
. . . . . . . . . 10
♯ ♯
|
126 | 121, 10, 125 | preimaf1ofi 6924 |
. . . . . . . . 9
♯ ♯ |
127 | | f1of1 5439 |
. . . . . . . . . . . 12
♯ ♯ |
128 | 10, 127 | syl 14 |
. . . . . . . . . . 11
♯ ♯ ♯ |
129 | | f1ores 5455 |
. . . . . . . . . . 11
♯
♯ |
130 | 128, 13, 129 | syl2anc 409 |
. . . . . . . . . 10
♯ ♯ |
131 | | f1ofo 5447 |
. . . . . . . . . . . . 13
♯ ♯ |
132 | 10, 131 | syl 14 |
. . . . . . . . . . . 12
♯ ♯ ♯ |
133 | | foimacnv 5458 |
. . . . . . . . . . . 12
♯ |
134 | 132, 121,
133 | syl2anc 409 |
. . . . . . . . . . 11
♯ ♯ |
135 | | f1oeq3 5431 |
. . . . . . . . . . 11
|
136 | 134, 135 | syl 14 |
. . . . . . . . . 10
♯ ♯
|
137 | 130, 136 | mpbid 146 |
. . . . . . . . 9
♯ ♯ |
138 | | fvres 5518 |
. . . . . . . . . 10
|
139 | 138 | adantl 275 |
. . . . . . . . 9
♯ ♯ |
140 | 121 | sselda 3147 |
. . . . . . . . . 10
♯ ♯ |
141 | 41 | ffvelrnda 5628 |
. . . . . . . . . 10
♯ ♯ |
142 | 140, 141 | syldan 280 |
. . . . . . . . 9
♯ ♯ |
143 | 120, 126,
137, 139, 142 | fsumf1o 11340 |
. . . . . . . 8
♯ ♯ |
144 | 119, 143 | eqtrd 2203 |
. . . . . . 7
♯ ♯ |
145 | | simprl 526 |
. . . . . . . . . 10
♯ ♯ ♯ |
146 | 145 | nnzd 9320 |
. . . . . . . . 9
♯ ♯ ♯ |
147 | 108, 146 | fzfigd 10374 |
. . . . . . . 8
♯ ♯ ♯ |
148 | | eqidd 2171 |
. . . . . . . 8
♯ ♯ ♯ |
149 | 120, 147,
10, 148, 141 | fsumf1o 11340 |
. . . . . . 7
♯ ♯ ♯ |
150 | 112, 144,
149 | 3eqtr4d 2213 |
. . . . . 6
♯ ♯
|
151 | 22 | ralrimiva 2543 |
. . . . . . . 8
|
152 | | sumfct 11324 |
. . . . . . . 8
|
153 | 151, 152 | syl 14 |
. . . . . . 7
|
154 | 153 | adantr 274 |
. . . . . 6
♯ ♯
|
155 | 22 | adantlr 474 |
. . . . . . . . . 10
|
156 | | simpll 524 |
. . . . . . . . . . . 12
|
157 | | simplr 525 |
. . . . . . . . . . . . 13
|
158 | | simpr 109 |
. . . . . . . . . . . . 13
|
159 | 157, 158 | eldifd 3131 |
. . . . . . . . . . . 12
|
160 | 156, 159,
26 | syl2anc 409 |
. . . . . . . . . . 11
|
161 | | 0cnd 7900 |
. . . . . . . . . . 11
|
162 | 160, 161 | eqeltrd 2247 |
. . . . . . . . . 10
|
163 | 155, 162,
38 | mpjaodan 793 |
. . . . . . . . 9
|
164 | 163 | ralrimiva 2543 |
. . . . . . . 8
|
165 | | sumfct 11324 |
. . . . . . . 8
|
166 | 164, 165 | syl 14 |
. . . . . . 7
|
167 | 166 | adantr 274 |
. . . . . 6
♯ ♯
|
168 | 150, 154,
167 | 3eqtr3d 2211 |
. . . . 5
♯ ♯ |
169 | 168 | expr 373 |
. . . 4
♯ ♯ |
170 | 169 | exlimdv 1812 |
. . 3
♯ ♯
|
171 | 170 | expimpd 361 |
. 2
♯ ♯
|
172 | | fz1f1o 11325 |
. . 3
♯ ♯ |
173 | 122, 172 | syl 14 |
. 2
♯ ♯ |
174 | 8, 171, 173 | mpjaod 713 |
1
|