Step | Hyp | Ref
| Expression |
1 | | fsummulc2.2 |
. . . 4
|
2 | 1 | mul01d 8123 |
. . 3
|
3 | | sumeq1 11079 |
. . . . . 6
|
4 | | sum0 11112 |
. . . . . 6
|
5 | 3, 4 | syl6eq 2166 |
. . . . 5
|
6 | 5 | oveq2d 5758 |
. . . 4
|
7 | | sumeq1 11079 |
. . . . 5
|
8 | | sum0 11112 |
. . . . 5
|
9 | 7, 8 | syl6eq 2166 |
. . . 4
|
10 | 6, 9 | eqeq12d 2132 |
. . 3
|
11 | 2, 10 | syl5ibrcom 156 |
. 2
|
12 | | addcl 7713 |
. . . . . . . . 9
|
13 | 12 | adantl 275 |
. . . . . . . 8
♯ ♯ |
14 | 1 | ad2antrr 479 |
. . . . . . . . 9
♯ ♯
|
15 | | simprl 505 |
. . . . . . . . 9
♯ ♯
|
16 | | simprr 506 |
. . . . . . . . 9
♯ ♯ |
17 | 14, 15, 16 | adddid 7758 |
. . . . . . . 8
♯ ♯ |
18 | | simprl 505 |
. . . . . . . . 9
♯ ♯ ♯ |
19 | | nnuz 9317 |
. . . . . . . . 9
|
20 | 18, 19 | eleqtrdi 2210 |
. . . . . . . 8
♯ ♯ ♯ |
21 | | elnnuz 9318 |
. . . . . . . . . . . 12
|
22 | 21 | biimpri 132 |
. . . . . . . . . . 11
|
23 | 22 | adantl 275 |
. . . . . . . . . 10
♯ ♯
|
24 | | f1of 5335 |
. . . . . . . . . . . . . . 15
♯ ♯ |
25 | 24 | ad2antll 482 |
. . . . . . . . . . . . . 14
♯ ♯ ♯ |
26 | 25 | ad2antrr 479 |
. . . . . . . . . . . . 13
♯ ♯
♯ ♯ |
27 | | 1zzd 9039 |
. . . . . . . . . . . . . . 15
♯ ♯
♯ |
28 | 18 | ad2antrr 479 |
. . . . . . . . . . . . . . . 16
♯ ♯
♯ ♯ |
29 | 28 | nnzd 9130 |
. . . . . . . . . . . . . . 15
♯ ♯
♯ ♯ |
30 | | eluzelz 9291 |
. . . . . . . . . . . . . . . 16
|
31 | 30 | ad2antlr 480 |
. . . . . . . . . . . . . . 15
♯ ♯
♯
|
32 | 27, 29, 31 | 3jca 1146 |
. . . . . . . . . . . . . 14
♯ ♯
♯ ♯ |
33 | | eluzle 9294 |
. . . . . . . . . . . . . . . 16
|
34 | 33 | ad2antlr 480 |
. . . . . . . . . . . . . . 15
♯ ♯
♯
|
35 | | simpr 109 |
. . . . . . . . . . . . . . 15
♯ ♯
♯ ♯ |
36 | 34, 35 | jca 304 |
. . . . . . . . . . . . . 14
♯ ♯
♯
♯ |
37 | | elfz2 9752 |
. . . . . . . . . . . . . 14
♯ ♯ ♯ |
38 | 32, 36, 37 | sylanbrc 413 |
. . . . . . . . . . . . 13
♯ ♯
♯
♯ |
39 | | fvco3 5460 |
. . . . . . . . . . . . 13
♯
♯ |
40 | 26, 38, 39 | syl2anc 408 |
. . . . . . . . . . . 12
♯ ♯
♯ |
41 | 26, 38 | ffvelrnd 5524 |
. . . . . . . . . . . . . 14
♯ ♯
♯ |
42 | | fsummulc2.3 |
. . . . . . . . . . . . . . . . 17
|
43 | 42 | ralrimiva 2482 |
. . . . . . . . . . . . . . . 16
|
44 | 43 | ad3antrrr 483 |
. . . . . . . . . . . . . . 15
♯ ♯
♯
|
45 | | nfcsb1v 3005 |
. . . . . . . . . . . . . . . . 17
|
46 | 45 | nfel1 2269 |
. . . . . . . . . . . . . . . 16
|
47 | | csbeq1a 2983 |
. . . . . . . . . . . . . . . . 17
|
48 | 47 | eleq1d 2186 |
. . . . . . . . . . . . . . . 16
|
49 | 46, 48 | rspc 2757 |
. . . . . . . . . . . . . . 15
|
50 | 41, 44, 49 | sylc 62 |
. . . . . . . . . . . . . 14
♯ ♯
♯
|
51 | | eqid 2117 |
. . . . . . . . . . . . . . 15
|
52 | 51 | fvmpts 5467 |
. . . . . . . . . . . . . 14
|
53 | 41, 50, 52 | syl2anc 408 |
. . . . . . . . . . . . 13
♯ ♯
♯ |
54 | 53, 50 | eqeltrd 2194 |
. . . . . . . . . . . 12
♯ ♯
♯ |
55 | 40, 54 | eqeltrd 2194 |
. . . . . . . . . . 11
♯ ♯
♯ |
56 | | 0cnd 7727 |
. . . . . . . . . . 11
♯ ♯
♯
|
57 | 23 | nnzd 9130 |
. . . . . . . . . . . 12
♯ ♯
|
58 | 18 | adantr 274 |
. . . . . . . . . . . . 13
♯ ♯
♯ |
59 | 58 | nnzd 9130 |
. . . . . . . . . . . 12
♯ ♯
♯ |
60 | | zdcle 9085 |
. . . . . . . . . . . 12
♯
DECID
♯ |
61 | 57, 59, 60 | syl2anc 408 |
. . . . . . . . . . 11
♯ ♯
DECID
♯ |
62 | 55, 56, 61 | ifcldadc 3471 |
. . . . . . . . . 10
♯ ♯
♯ |
63 | | breq1 3902 |
. . . . . . . . . . . 12
♯
♯ |
64 | | fveq2 5389 |
. . . . . . . . . . . 12
|
65 | 63, 64 | ifbieq1d 3464 |
. . . . . . . . . . 11
♯ ♯ |
66 | | eqid 2117 |
. . . . . . . . . . 11
♯ ♯ |
67 | 65, 66 | fvmptg 5465 |
. . . . . . . . . 10
♯ ♯ ♯ |
68 | 23, 62, 67 | syl2anc 408 |
. . . . . . . . 9
♯ ♯
♯ ♯ |
69 | 68, 62 | eqeltrd 2194 |
. . . . . . . 8
♯ ♯
♯ |
70 | | csbov2g 5780 |
. . . . . . . . . . . 12
|
71 | 41, 70 | syl 14 |
. . . . . . . . . . 11
♯ ♯
♯
|
72 | 35 | iftrued 3451 |
. . . . . . . . . . . 12
♯ ♯
♯ ♯ |
73 | | fvco3 5460 |
. . . . . . . . . . . . 13
♯
♯ |
74 | 26, 38, 73 | syl2anc 408 |
. . . . . . . . . . . 12
♯ ♯
♯ |
75 | 1 | ad3antrrr 483 |
. . . . . . . . . . . . . . 15
♯ ♯
♯
|
76 | 75, 50 | mulcld 7754 |
. . . . . . . . . . . . . 14
♯ ♯
♯ |
77 | 71, 76 | eqeltrd 2194 |
. . . . . . . . . . . . 13
♯ ♯
♯
|
78 | | eqid 2117 |
. . . . . . . . . . . . . 14
|
79 | 78 | fvmpts 5467 |
. . . . . . . . . . . . 13
|
80 | 41, 77, 79 | syl2anc 408 |
. . . . . . . . . . . 12
♯ ♯
♯
|
81 | 72, 74, 80 | 3eqtrd 2154 |
. . . . . . . . . . 11
♯ ♯
♯ ♯ |
82 | 35 | iftrued 3451 |
. . . . . . . . . . . . 13
♯ ♯
♯ ♯ |
83 | 82, 40, 53 | 3eqtrd 2154 |
. . . . . . . . . . . 12
♯ ♯
♯ ♯ |
84 | 83 | oveq2d 5758 |
. . . . . . . . . . 11
♯ ♯
♯
♯ |
85 | 71, 81, 84 | 3eqtr4d 2160 |
. . . . . . . . . 10
♯ ♯
♯ ♯ ♯ |
86 | 1 | ad3antrrr 483 |
. . . . . . . . . . . 12
♯ ♯
♯
|
87 | 86 | mul01d 8123 |
. . . . . . . . . . 11
♯ ♯
♯
|
88 | | simpr 109 |
. . . . . . . . . . . . 13
♯ ♯
♯
♯ |
89 | 88 | iffalsed 3454 |
. . . . . . . . . . . 12
♯ ♯
♯
♯ |
90 | 89 | oveq2d 5758 |
. . . . . . . . . . 11
♯ ♯
♯
♯ |
91 | 88 | iffalsed 3454 |
. . . . . . . . . . 11
♯ ♯
♯
♯ |
92 | 87, 90, 91 | 3eqtr4rd 2161 |
. . . . . . . . . 10
♯ ♯
♯
♯
♯ |
93 | | exmiddc 806 |
. . . . . . . . . . 11
DECID ♯ ♯ ♯ |
94 | 61, 93 | syl 14 |
. . . . . . . . . 10
♯ ♯
♯ ♯ |
95 | 85, 92, 94 | mpjaodan 772 |
. . . . . . . . 9
♯ ♯
♯
♯ |
96 | 80, 77 | eqeltrd 2194 |
. . . . . . . . . . . 12
♯ ♯
♯ |
97 | 74, 96 | eqeltrd 2194 |
. . . . . . . . . . 11
♯ ♯
♯ |
98 | 97, 56, 61 | ifcldadc 3471 |
. . . . . . . . . 10
♯ ♯
♯ |
99 | | fveq2 5389 |
. . . . . . . . . . . 12
|
100 | 63, 99 | ifbieq1d 3464 |
. . . . . . . . . . 11
♯ ♯ |
101 | | eqid 2117 |
. . . . . . . . . . 11
♯ ♯ |
102 | 100, 101 | fvmptg 5465 |
. . . . . . . . . 10
♯ ♯ ♯ |
103 | 23, 98, 102 | syl2anc 408 |
. . . . . . . . 9
♯ ♯
♯ ♯ |
104 | 68 | oveq2d 5758 |
. . . . . . . . 9
♯ ♯
♯
♯ |
105 | 95, 103, 104 | 3eqtr4d 2160 |
. . . . . . . 8
♯ ♯
♯ ♯ |
106 | | mulcl 7715 |
. . . . . . . . 9
|
107 | 106 | adantl 275 |
. . . . . . . 8
♯ ♯ |
108 | 1 | adantr 274 |
. . . . . . . 8
♯ ♯
|
109 | 13, 17, 20, 69, 105, 107, 108 | seq3distr 10241 |
. . . . . . 7
♯ ♯ ♯ ♯ ♯ ♯ |
110 | | fveq2 5389 |
. . . . . . . 8
|
111 | | simprr 506 |
. . . . . . . 8
♯ ♯ ♯ |
112 | 1 | adantr 274 |
. . . . . . . . . . . 12
|
113 | 112, 42 | mulcld 7754 |
. . . . . . . . . . 11
|
114 | 113 | fmpttd 5543 |
. . . . . . . . . 10
|
115 | 114 | adantr 274 |
. . . . . . . . 9
♯ ♯ |
116 | 115 | ffvelrnda 5523 |
. . . . . . . 8
♯ ♯ |
117 | | fvco3 5460 |
. . . . . . . . 9
♯
♯ |
118 | 25, 117 | sylan 281 |
. . . . . . . 8
♯ ♯ ♯ |
119 | 110, 18, 111, 116, 118 | fsum3 11111 |
. . . . . . 7
♯ ♯ ♯ ♯ |
120 | | fveq2 5389 |
. . . . . . . . 9
|
121 | 42 | fmpttd 5543 |
. . . . . . . . . . 11
|
122 | 121 | adantr 274 |
. . . . . . . . . 10
♯ ♯ |
123 | 122 | ffvelrnda 5523 |
. . . . . . . . 9
♯ ♯ |
124 | | fvco3 5460 |
. . . . . . . . . 10
♯
♯ |
125 | 25, 124 | sylan 281 |
. . . . . . . . 9
♯ ♯ ♯ |
126 | 120, 18, 111, 123, 125 | fsum3 11111 |
. . . . . . . 8
♯ ♯ ♯ ♯ |
127 | 126 | oveq2d 5758 |
. . . . . . 7
♯ ♯ ♯ ♯ |
128 | 109, 119,
127 | 3eqtr4rd 2161 |
. . . . . 6
♯ ♯
|
129 | | sumfct 11098 |
. . . . . . . . 9
|
130 | 43, 129 | syl 14 |
. . . . . . . 8
|
131 | 130 | oveq2d 5758 |
. . . . . . 7
|
132 | 131 | adantr 274 |
. . . . . 6
♯ ♯ |
133 | 113 | ralrimiva 2482 |
. . . . . . . 8
|
134 | | sumfct 11098 |
. . . . . . . 8
|
135 | 133, 134 | syl 14 |
. . . . . . 7
|
136 | 135 | adantr 274 |
. . . . . 6
♯ ♯
|
137 | 128, 132,
136 | 3eqtr3d 2158 |
. . . . 5
♯ ♯
|
138 | 137 | expr 372 |
. . . 4
♯ ♯
|
139 | 138 | exlimdv 1775 |
. . 3
♯ ♯
|
140 | 139 | expimpd 360 |
. 2
♯ ♯
|
141 | | fsummulc2.1 |
. . 3
|
142 | | fz1f1o 11099 |
. . 3
♯ ♯ |
143 | 141, 142 | syl 14 |
. 2
♯ ♯ |
144 | 11, 140, 143 | mpjaod 692 |
1
|