Proof of Theorem fsumparts
Step | Hyp | Ref
| Expression |
1 | | sum0 14452 |
. . . 4
|
2 | | 0m0e0 11130 |
. . . 4
|
3 | 1, 2 | eqtr4i 2647 |
. . 3
|
4 | | simpr 477 |
. . . . . 6
|
5 | 4 | oveq2d 6666 |
. . . . 5
..^ ..^ |
6 | | fzo0 12492 |
. . . . 5
..^ |
7 | 5, 6 | syl6eq 2672 |
. . . 4
..^ |
8 | 7 | sumeq1d 14431 |
. . 3
..^
|
9 | | fsumparts.1 |
. . . . . . . 8
|
10 | | eluzfz1 12348 |
. . . . . . . 8
|
11 | 9, 10 | syl 17 |
. . . . . . 7
|
12 | | eqtr3 2643 |
. . . . . . . . . . . 12
|
13 | | fsumparts.e |
. . . . . . . . . . . 12
|
14 | | oveq12 6659 |
. . . . . . . . . . . 12
|
15 | 12, 13, 14 | 3syl 18 |
. . . . . . . . . . 11
|
16 | | fsumparts.d |
. . . . . . . . . . . . 13
|
17 | | oveq12 6659 |
. . . . . . . . . . . . 13
|
18 | 16, 17 | syl 17 |
. . . . . . . . . . . 12
|
19 | 18 | adantr 481 |
. . . . . . . . . . 11
|
20 | 15, 19 | eqeq12d 2637 |
. . . . . . . . . 10
|
21 | 20 | pm5.74da 723 |
. . . . . . . . 9
|
22 | | eqidd 2623 |
. . . . . . . . 9
|
23 | 21, 22 | vtoclg 3266 |
. . . . . . . 8
|
24 | 23 | imp 445 |
. . . . . . 7
|
25 | 11, 24 | sylan 488 |
. . . . . 6
|
26 | 25 | oveq1d 6665 |
. . . . 5
|
27 | | fsumparts.2 |
. . . . . . . . . 10
|
28 | 27 | ralrimiva 2966 |
. . . . . . . . 9
|
29 | 16 | simpld 475 |
. . . . . . . . . . 11
|
30 | 29 | eleq1d 2686 |
. . . . . . . . . 10
|
31 | 30 | rspcv 3305 |
. . . . . . . . 9
|
32 | 11, 28, 31 | sylc 65 |
. . . . . . . 8
|
33 | | fsumparts.3 |
. . . . . . . . . 10
|
34 | 33 | ralrimiva 2966 |
. . . . . . . . 9
|
35 | 16 | simprd 479 |
. . . . . . . . . . 11
|
36 | 35 | eleq1d 2686 |
. . . . . . . . . 10
|
37 | 36 | rspcv 3305 |
. . . . . . . . 9
|
38 | 11, 34, 37 | sylc 65 |
. . . . . . . 8
|
39 | 32, 38 | mulcld 10060 |
. . . . . . 7
|
40 | 39 | subidd 10380 |
. . . . . 6
|
41 | 40 | adantr 481 |
. . . . 5
|
42 | 26, 41 | eqtrd 2656 |
. . . 4
|
43 | 7 | sumeq1d 14431 |
. . . . 5
..^ |
44 | | sum0 14452 |
. . . . 5
|
45 | 43, 44 | syl6eq 2672 |
. . . 4
..^ |
46 | 42, 45 | oveq12d 6668 |
. . 3
..^ |
47 | 3, 8, 46 | 3eqtr4a 2682 |
. 2
..^
..^ |
48 | | simpr 477 |
. . . . . . . . 9
|
49 | | eluzel2 11692 |
. . . . . . . . . . . . . 14
|
50 | 9, 49 | syl 17 |
. . . . . . . . . . . . 13
|
51 | 50 | adantr 481 |
. . . . . . . . . . . 12
|
52 | | fzp1ss 12392 |
. . . . . . . . . . . 12
|
53 | 51, 52 | syl 17 |
. . . . . . . . . . 11
|
54 | 53 | sselda 3603 |
. . . . . . . . . 10
|
55 | 27, 33 | mulcld 10060 |
. . . . . . . . . . 11
|
56 | 55 | adantlr 751 |
. . . . . . . . . 10
|
57 | 54, 56 | syldan 487 |
. . . . . . . . 9
|
58 | 13, 14 | syl 17 |
. . . . . . . . 9
|
59 | 48, 57, 58 | fsumm1 14480 |
. . . . . . . 8
|
60 | | eluzelz 11697 |
. . . . . . . . . . . . . 14
|
61 | 9, 60 | syl 17 |
. . . . . . . . . . . . 13
|
62 | 61 | adantr 481 |
. . . . . . . . . . . 12
|
63 | | fzoval 12471 |
. . . . . . . . . . . 12
..^ |
64 | 62, 63 | syl 17 |
. . . . . . . . . . 11
..^ |
65 | 51 | zcnd 11483 |
. . . . . . . . . . . . 13
|
66 | | ax-1cn 9994 |
. . . . . . . . . . . . 13
|
67 | | pncan 10287 |
. . . . . . . . . . . . 13
|
68 | 65, 66, 67 | sylancl 694 |
. . . . . . . . . . . 12
|
69 | 68 | oveq1d 6665 |
. . . . . . . . . . 11
|
70 | 64, 69 | eqtr4d 2659 |
. . . . . . . . . 10
..^ |
71 | 70 | sumeq1d 14431 |
. . . . . . . . 9
..^
|
72 | | 1zzd 11408 |
. . . . . . . . . 10
|
73 | 51 | peano2zd 11485 |
. . . . . . . . . 10
|
74 | | fsumparts.c |
. . . . . . . . . . 11
|
75 | | oveq12 6659 |
. . . . . . . . . . 11
|
76 | 74, 75 | syl 17 |
. . . . . . . . . 10
|
77 | 72, 73, 62, 57, 76 | fsumshftm 14513 |
. . . . . . . . 9
|
78 | 71, 77 | eqtr4d 2659 |
. . . . . . . 8
..^ |
79 | | fzoval 12471 |
. . . . . . . . . . 11
..^
|
80 | 62, 79 | syl 17 |
. . . . . . . . . 10
..^ |
81 | 80 | sumeq1d 14431 |
. . . . . . . . 9
..^
|
82 | 81 | oveq1d 6665 |
. . . . . . . 8
..^ |
83 | 59, 78, 82 | 3eqtr4d 2666 |
. . . . . . 7
..^
..^ |
84 | | fzofi 12773 |
. . . . . . . . . 10
..^ |
85 | 84 | a1i 11 |
. . . . . . . . 9
..^ |
86 | | uzid 11702 |
. . . . . . . . . . . 12
|
87 | | peano2uz 11741 |
. . . . . . . . . . . 12
|
88 | | fzoss1 12495 |
. . . . . . . . . . . 12
..^ ..^ |
89 | 51, 86, 87, 88 | 4syl 19 |
. . . . . . . . . . 11
..^ ..^ |
90 | 89 | sselda 3603 |
. . . . . . . . . 10
..^
..^ |
91 | | elfzofz 12485 |
. . . . . . . . . . . 12
..^
|
92 | 91, 55 | sylan2 491 |
. . . . . . . . . . 11
..^ |
93 | 92 | adantlr 751 |
. . . . . . . . . 10
..^
|
94 | 90, 93 | syldan 487 |
. . . . . . . . 9
..^
|
95 | 85, 94 | fsumcl 14464 |
. . . . . . . 8
..^ |
96 | | eluzfz2 12349 |
. . . . . . . . . . . 12
|
97 | 9, 96 | syl 17 |
. . . . . . . . . . 11
|
98 | 13 | simpld 475 |
. . . . . . . . . . . . 13
|
99 | 98 | eleq1d 2686 |
. . . . . . . . . . . 12
|
100 | 99 | rspcv 3305 |
. . . . . . . . . . 11
|
101 | 97, 28, 100 | sylc 65 |
. . . . . . . . . 10
|
102 | 13 | simprd 479 |
. . . . . . . . . . . . 13
|
103 | 102 | eleq1d 2686 |
. . . . . . . . . . . 12
|
104 | 103 | rspcv 3305 |
. . . . . . . . . . 11
|
105 | 97, 34, 104 | sylc 65 |
. . . . . . . . . 10
|
106 | 101, 105 | mulcld 10060 |
. . . . . . . . 9
|
107 | 106 | adantr 481 |
. . . . . . . 8
|
108 | 95, 107 | addcomd 10238 |
. . . . . . 7
..^ ..^ |
109 | 83, 108 | eqtrd 2656 |
. . . . . 6
..^ ..^ |
110 | 109 | oveq1d 6665 |
. . . . 5
..^ ..^ ..^ ..^ |
111 | | fzofzp1 12565 |
. . . . . . . . . 10
..^
|
112 | 74 | simpld 475 |
. . . . . . . . . . . 12
|
113 | 112 | eleq1d 2686 |
. . . . . . . . . . 11
|
114 | 113 | rspccva 3308 |
. . . . . . . . . 10
|
115 | 28, 111, 114 | syl2an 494 |
. . . . . . . . 9
..^ |
116 | | elfzofz 12485 |
. . . . . . . . . 10
..^
|
117 | | fsumparts.b |
. . . . . . . . . . . . 13
|
118 | 117 | simpld 475 |
. . . . . . . . . . . 12
|
119 | 118 | eleq1d 2686 |
. . . . . . . . . . 11
|
120 | 119 | rspccva 3308 |
. . . . . . . . . 10
|
121 | 28, 116, 120 | syl2an 494 |
. . . . . . . . 9
..^ |
122 | 74 | simprd 479 |
. . . . . . . . . . . 12
|
123 | 122 | eleq1d 2686 |
. . . . . . . . . . 11
|
124 | 123 | rspccva 3308 |
. . . . . . . . . 10
|
125 | 34, 111, 124 | syl2an 494 |
. . . . . . . . 9
..^ |
126 | 115, 121,
125 | subdird 10487 |
. . . . . . . 8
..^ |
127 | 126 | sumeq2dv 14433 |
. . . . . . 7
..^ ..^ |
128 | | fzofi 12773 |
. . . . . . . . 9
..^ |
129 | 128 | a1i 11 |
. . . . . . . 8
..^ |
130 | 115, 125 | mulcld 10060 |
. . . . . . . 8
..^ |
131 | 121, 125 | mulcld 10060 |
. . . . . . . 8
..^ |
132 | 129, 130,
131 | fsumsub 14520 |
. . . . . . 7
..^ ..^ ..^ |
133 | 127, 132 | eqtrd 2656 |
. . . . . 6
..^ ..^ ..^ |
134 | 133 | adantr 481 |
. . . . 5
..^
..^ ..^ |
135 | 129, 131 | fsumcl 14464 |
. . . . . . 7
..^ |
136 | 135 | adantr 481 |
. . . . . 6
..^ |
137 | 107, 136,
95 | subsub3d 10422 |
. . . . 5
..^ ..^ ..^ ..^ |
138 | 110, 134,
137 | 3eqtr4d 2666 |
. . . 4
..^ ..^ ..^ |
139 | 138 | oveq2d 6666 |
. . 3
..^ ..^ ..^ |
140 | 39 | adantr 481 |
. . . 4
|
141 | 136, 95 | subcld 10392 |
. . . 4
..^ ..^ |
142 | 107, 140,
141 | nnncan1d 10426 |
. . 3
..^ ..^ ..^ ..^
|
143 | 95, 140 | addcomd 10238 |
. . . . . . 7
..^ ..^ |
144 | | eluzp1m1 11711 |
. . . . . . . . . 10
|
145 | 50, 144 | sylan 488 |
. . . . . . . . 9
|
146 | 64 | eleq2d 2687 |
. . . . . . . . . . 11
..^ |
147 | 146 | biimpar 502 |
. . . . . . . . . 10
..^ |
148 | 147, 93 | syldan 487 |
. . . . . . . . 9
|
149 | 145, 148,
18 | fsum1p 14482 |
. . . . . . . 8
|
150 | 64 | sumeq1d 14431 |
. . . . . . . 8
..^
|
151 | 81 | oveq2d 6666 |
. . . . . . . 8
..^ |
152 | 149, 150,
151 | 3eqtr4d 2666 |
. . . . . . 7
..^ ..^ |
153 | 143, 152 | eqtr4d 2659 |
. . . . . 6
..^
..^ |
154 | | oveq12 6659 |
. . . . . . . 8
|
155 | 117, 154 | syl 17 |
. . . . . . 7
|
156 | 155 | cbvsumv 14426 |
. . . . . 6
..^ ..^ |
157 | 153, 156 | syl6eq 2672 |
. . . . 5
..^
..^ |
158 | 157 | oveq2d 6666 |
. . . 4
..^ ..^ ..^ ..^ |
159 | 136, 95, 140 | subsub4d 10423 |
. . . 4
..^ ..^ ..^ ..^ |
160 | 117 | simprd 479 |
. . . . . . . . . . 11
|
161 | 160 | eleq1d 2686 |
. . . . . . . . . 10
|
162 | 161 | rspccva 3308 |
. . . . . . . . 9
|
163 | 34, 116, 162 | syl2an 494 |
. . . . . . . 8
..^ |
164 | 121, 125,
163 | subdid 10486 |
. . . . . . 7
..^
|
165 | 164 | sumeq2dv 14433 |
. . . . . 6
..^ ..^ |
166 | 121, 163 | mulcld 10060 |
. . . . . . 7
..^ |
167 | 129, 131,
166 | fsumsub 14520 |
. . . . . 6
..^ ..^ ..^ |
168 | 165, 167 | eqtrd 2656 |
. . . . 5
..^ ..^ ..^ |
169 | 168 | adantr 481 |
. . . 4
..^
..^ ..^ |
170 | 158, 159,
169 | 3eqtr4d 2666 |
. . 3
..^ ..^ ..^ |
171 | 139, 142,
170 | 3eqtrrd 2661 |
. 2
..^
..^ |
172 | | uzp1 11721 |
. . 3
|
173 | 9, 172 | syl 17 |
. 2
|
174 | 47, 171, 173 | mpjaodan 827 |
1
..^ ..^ |