Proof of Theorem fsum2dsub
Step | Hyp | Ref
| Expression |
1 | | fzssz 12343 |
. . . . . 6
|
2 | | simpr 477 |
. . . . . 6
|
3 | 1, 2 | sseldi 3601 |
. . . . 5
|
4 | | 0zd 11389 |
. . . . 5
|
5 | | fzsum2sub.m |
. . . . . . 7
|
6 | 5 | nn0zd 11480 |
. . . . . 6
|
7 | 6 | adantr 481 |
. . . . 5
|
8 | | simpll 790 |
. . . . . 6
|
9 | | fz1ssnn 12372 |
. . . . . . . . . . . 12
|
10 | | nnssnn0 11295 |
. . . . . . . . . . . 12
|
11 | 9, 10 | sstri 3612 |
. . . . . . . . . . 11
|
12 | 11, 2 | sseldi 3601 |
. . . . . . . . . 10
|
13 | | nn0uz 11722 |
. . . . . . . . . 10
|
14 | 12, 13 | syl6eleq 2711 |
. . . . . . . . 9
|
15 | | neg0 10327 |
. . . . . . . . . 10
|
16 | | uzneg 11706 |
. . . . . . . . . 10
|
17 | 15, 16 | syl5eqelr 2706 |
. . . . . . . . 9
|
18 | | fzss1 12380 |
. . . . . . . . 9
|
19 | 14, 17, 18 | 3syl 18 |
. . . . . . . 8
|
20 | | fzssuz 12382 |
. . . . . . . 8
|
21 | 19, 20 | syl6ss 3615 |
. . . . . . 7
|
22 | 21 | sselda 3603 |
. . . . . 6
|
23 | 2 | adantr 481 |
. . . . . 6
|
24 | | fzsum2sub.2 |
. . . . . 6
|
25 | 8, 22, 23, 24 | syl3anc 1326 |
. . . . 5
|
26 | | fzsum2sub.1 |
. . . . 5
|
27 | 3, 4, 7, 25, 26 | fsumshft 14512 |
. . . 4
|
28 | 5 | adantr 481 |
. . . . . . . . . . 11
|
29 | 9, 2 | sseldi 3601 |
. . . . . . . . . . . 12
|
30 | 29 | nnnn0d 11351 |
. . . . . . . . . . 11
|
31 | 28, 30 | nn0addcld 11355 |
. . . . . . . . . 10
|
32 | 31 | nn0red 11352 |
. . . . . . . . 9
|
33 | 32 | ltp1d 10954 |
. . . . . . . 8
|
34 | | fzdisj 12368 |
. . . . . . . 8
|
35 | 33, 34 | syl 17 |
. . . . . . 7
|
36 | | fzsum2sub.n |
. . . . . . . . . . . 12
|
37 | 36 | nn0zd 11480 |
. . . . . . . . . . 11
|
38 | 6, 37 | zaddcld 11486 |
. . . . . . . . . 10
|
39 | 38 | adantr 481 |
. . . . . . . . 9
|
40 | 31 | nn0zd 11480 |
. . . . . . . . 9
|
41 | 29 | nnred 11035 |
. . . . . . . . . 10
|
42 | | nn0addge2 11340 |
. . . . . . . . . 10
|
43 | 41, 28, 42 | syl2anc 693 |
. . . . . . . . 9
|
44 | 36 | nn0red 11352 |
. . . . . . . . . . 11
|
45 | 44 | adantr 481 |
. . . . . . . . . 10
|
46 | 28 | nn0red 11352 |
. . . . . . . . . 10
|
47 | | elfzle2 12345 |
. . . . . . . . . . 11
|
48 | 47 | adantl 482 |
. . . . . . . . . 10
|
49 | 41, 45, 46, 48 | leadd2dd 10642 |
. . . . . . . . 9
|
50 | | elfz4 12335 |
. . . . . . . . 9
|
51 | 3, 39, 40, 43, 49, 50 | syl32anc 1334 |
. . . . . . . 8
|
52 | | fzsplit 12367 |
. . . . . . . 8
|
53 | 51, 52 | syl 17 |
. . . . . . 7
|
54 | | fzfid 12772 |
. . . . . . 7
|
55 | | simpll 790 |
. . . . . . . 8
|
56 | 2 | adantr 481 |
. . . . . . . 8
|
57 | 11, 56 | sseldi 3601 |
. . . . . . . . . 10
|
58 | | fz2ssnn0 29547 |
. . . . . . . . . 10
|
59 | 57, 58 | syl 17 |
. . . . . . . . 9
|
60 | | simpr 477 |
. . . . . . . . 9
|
61 | 59, 60 | sseldd 3604 |
. . . . . . . 8
|
62 | 26 | eleq1d 2686 |
. . . . . . . . 9
|
63 | | simpll 790 |
. . . . . . . . . . . . 13
|
64 | | simplr 792 |
. . . . . . . . . . . . 13
|
65 | | simpr 477 |
. . . . . . . . . . . . 13
|
66 | 63, 64, 65, 24 | syl3anc 1326 |
. . . . . . . . . . . 12
|
67 | 66 | an32s 846 |
. . . . . . . . . . 11
|
68 | 67 | ralrimiva 2966 |
. . . . . . . . . 10
|
69 | 68 | adantr 481 |
. . . . . . . . 9
|
70 | | nnsscn 11025 |
. . . . . . . . . . . . 13
|
71 | 9, 70 | sstri 3612 |
. . . . . . . . . . . 12
|
72 | | simplr 792 |
. . . . . . . . . . . 12
|
73 | 71, 72 | sseldi 3601 |
. . . . . . . . . . 11
|
74 | | simpr 477 |
. . . . . . . . . . . 12
|
75 | 74 | nn0cnd 11353 |
. . . . . . . . . . 11
|
76 | 73, 75 | negsubdi2d 10408 |
. . . . . . . . . 10
|
77 | 1, 72 | sseldi 3601 |
. . . . . . . . . . . 12
|
78 | | eluzmn 11694 |
. . . . . . . . . . . 12
|
79 | 77, 74, 78 | syl2anc 693 |
. . . . . . . . . . 11
|
80 | | uzneg 11706 |
. . . . . . . . . . 11
|
81 | 79, 80 | syl 17 |
. . . . . . . . . 10
|
82 | 76, 81 | eqeltrrd 2702 |
. . . . . . . . 9
|
83 | 62, 69, 82 | rspcdva 3316 |
. . . . . . . 8
|
84 | 55, 56, 61, 83 | syl21anc 1325 |
. . . . . . 7
|
85 | 35, 53, 54, 84 | fsumsplit 14471 |
. . . . . 6
|
86 | 3 | zcnd 11483 |
. . . . . . . . . . 11
|
87 | 86 | addid2d 10237 |
. . . . . . . . . 10
|
88 | 87 | oveq1d 6665 |
. . . . . . . . 9
|
89 | 88 | eqcomd 2628 |
. . . . . . . 8
|
90 | 89 | sumeq1d 14431 |
. . . . . . 7
|
91 | | fzsum2sub.3 |
. . . . . . . . 9
|
92 | 91 | sumeq2dv 14433 |
. . . . . . . 8
|
93 | | fzfi 12771 |
. . . . . . . . 9
|
94 | | sumz 14453 |
. . . . . . . . . 10
|
95 | 94 | olcs 410 |
. . . . . . . . 9
|
96 | 93, 95 | ax-mp 5 |
. . . . . . . 8
|
97 | 92, 96 | syl6eq 2672 |
. . . . . . 7
|
98 | 90, 97 | oveq12d 6668 |
. . . . . 6
|
99 | | fzfid 12772 |
. . . . . . . 8
|
100 | | simpll 790 |
. . . . . . . . 9
|
101 | 2 | adantr 481 |
. . . . . . . . 9
|
102 | | elfzuz3 12339 |
. . . . . . . . . . . . . . . 16
|
103 | 102 | adantl 482 |
. . . . . . . . . . . . . . 15
|
104 | | eluzadd 11716 |
. . . . . . . . . . . . . . 15
|
105 | 103, 7, 104 | syl2anc 693 |
. . . . . . . . . . . . . 14
|
106 | 36 | nn0cnd 11353 |
. . . . . . . . . . . . . . . 16
|
107 | 106 | adantr 481 |
. . . . . . . . . . . . . . 15
|
108 | | zsscn 11385 |
. . . . . . . . . . . . . . . 16
|
109 | 108, 7 | sseldi 3601 |
. . . . . . . . . . . . . . 15
|
110 | 107, 109 | addcomd 10238 |
. . . . . . . . . . . . . 14
|
111 | 86, 109 | addcomd 10238 |
. . . . . . . . . . . . . . 15
|
112 | 111 | fveq2d 6195 |
. . . . . . . . . . . . . 14
|
113 | 105, 110,
112 | 3eltr3d 2715 |
. . . . . . . . . . . . 13
|
114 | 113 | adantr 481 |
. . . . . . . . . . . 12
|
115 | | fzss2 12381 |
. . . . . . . . . . . 12
|
116 | 114, 115 | syl 17 |
. . . . . . . . . . 11
|
117 | | simpr 477 |
. . . . . . . . . . . 12
|
118 | 88 | adantr 481 |
. . . . . . . . . . . 12
|
119 | 117, 118 | eleqtrd 2703 |
. . . . . . . . . . 11
|
120 | 116, 119 | sseldd 3604 |
. . . . . . . . . 10
|
121 | 100, 101,
120, 61 | syl21anc 1325 |
. . . . . . . . 9
|
122 | 100, 101,
121, 83 | syl21anc 1325 |
. . . . . . . 8
|
123 | 99, 122 | fsumcl 14464 |
. . . . . . 7
|
124 | 123 | addid1d 10236 |
. . . . . 6
|
125 | 85, 98, 124 | 3eqtrrd 2661 |
. . . . 5
|
126 | | fzval3 12536 |
. . . . . . . . . 10
..^ |
127 | 39, 126 | syl 17 |
. . . . . . . . 9
..^ |
128 | 127 | ineq2d 3814 |
. . . . . . . 8
..^ ..^ ..^ |
129 | | fzodisj 12502 |
. . . . . . . 8
..^ ..^ |
130 | 128, 129 | syl6eq 2672 |
. . . . . . 7
..^ |
131 | 39 | peano2zd 11485 |
. . . . . . . . . 10
|
132 | 30 | nn0ge0d 11354 |
. . . . . . . . . 10
|
133 | 131 | zred 11482 |
. . . . . . . . . . 11
|
134 | 39 | zred 11482 |
. . . . . . . . . . . 12
|
135 | | nn0addge2 11340 |
. . . . . . . . . . . . . 14
|
136 | 44, 5, 135 | syl2anc 693 |
. . . . . . . . . . . . 13
|
137 | 136 | adantr 481 |
. . . . . . . . . . . 12
|
138 | 134 | lep1d 10955 |
. . . . . . . . . . . 12
|
139 | 45, 134, 133, 137, 138 | letrd 10194 |
. . . . . . . . . . 11
|
140 | 41, 45, 133, 48, 139 | letrd 10194 |
. . . . . . . . . 10
|
141 | | elfz4 12335 |
. . . . . . . . . 10
|
142 | 4, 131, 3, 132, 140, 141 | syl32anc 1334 |
. . . . . . . . 9
|
143 | | fzosplit 12501 |
. . . . . . . . 9
..^ ..^ ..^ |
144 | 142, 143 | syl 17 |
. . . . . . . 8
..^ ..^ ..^ |
145 | | fzval3 12536 |
. . . . . . . . 9
..^ |
146 | 39, 145 | syl 17 |
. . . . . . . 8
..^ |
147 | 127 | uneq2d 3767 |
. . . . . . . 8
..^ ..^ ..^ |
148 | 144, 146,
147 | 3eqtr4d 2666 |
. . . . . . 7
..^ |
149 | | fzfid 12772 |
. . . . . . . 8
|
150 | 149 | adantr 481 |
. . . . . . 7
|
151 | | simpl 473 |
. . . . . . . . 9
|
152 | 2 | adantrl 752 |
. . . . . . . . 9
|
153 | | fz0ssnn0 12435 |
. . . . . . . . . 10
|
154 | | simprl 794 |
. . . . . . . . . 10
|
155 | 153, 154 | sseldi 3601 |
. . . . . . . . 9
|
156 | 151, 152,
155, 83 | syl21anc 1325 |
. . . . . . . 8
|
157 | 156 | anass1rs 849 |
. . . . . . 7
|
158 | 130, 148,
150, 157 | fsumsplit 14471 |
. . . . . 6
..^ |
159 | | fzsum2sub.4 |
. . . . . . . . 9
..^
|
160 | 159 | sumeq2dv 14433 |
. . . . . . . 8
..^ ..^ |
161 | | fzofi 12773 |
. . . . . . . . 9
..^ |
162 | | sumz 14453 |
. . . . . . . . . 10
..^ ..^ ..^ |
163 | 162 | olcs 410 |
. . . . . . . . 9
..^ ..^ |
164 | 161, 163 | ax-mp 5 |
. . . . . . . 8
..^ |
165 | 160, 164 | syl6eq 2672 |
. . . . . . 7
..^ |
166 | 165 | oveq1d 6665 |
. . . . . 6
..^ |
167 | 54, 84 | fsumcl 14464 |
. . . . . . 7
|
168 | 167 | addid2d 10237 |
. . . . . 6
|
169 | 158, 166,
168 | 3eqtrrd 2661 |
. . . . 5
|
170 | 125, 169 | eqtrd 2656 |
. . . 4
|
171 | 27, 170 | eqtrd 2656 |
. . 3
|
172 | 171 | sumeq2dv 14433 |
. 2
|
173 | | fzfid 12772 |
. . 3
|
174 | | fzfid 12772 |
. . 3
|
175 | 25 | anasss 679 |
. . . 4
|
176 | 175 | ancom2s 844 |
. . 3
|
177 | 173, 174,
176 | fsumcom 14507 |
. 2
|
178 | 149, 174,
156 | fsumcom 14507 |
. 2
|
179 | 172, 177,
178 | 3eqtr4d 2666 |
1
|