Step Hyp Ref
Expression 1 cvgcmpce.1 . 2
2 cvgcmpce.2 . . . . . 6
3 2 , 1 syl6eleq 2555 . . . . 5
4 eluzel2 11115 . . . . 5
5 3 , 4 syl 16 . . . 4
6 cvgcmpce.4 . . . 4
7 1 , 5 , 6 serf 12135 . . 3
8 7 ffvelrnda 6031 . 2
9 fveq2 5871 . . . . . . . . 9
10 9 oveq2d 6312 . . . . . . . 8
11 eqid 2457 . . . . . . . 8
12 ovex 6324 . . . . . . . 8
13 10 , 11 , 12 fvmpt 5956 . . . . . . 7
14 13 adantl 466 . . . . . 6
15 cvgcmpce.6 . . . . . . . 8
16 15 adantr 465 . . . . . . 7
17 cvgcmpce.3 . . . . . . 7
18 16 , 17 remulcld 9645 . . . . . 6
19 14 , 18 eqeltrd 2545 . . . . 5
20 fveq2 5871 . . . . . . . . 9
21 20 fveq2d 5875 . . . . . . . 8
22 eqid 2457 . . . . . . . 8
23 fvex 5881 . . . . . . . 8
24 21 , 22 , 23 fvmpt 5956 . . . . . . 7
25 24 adantl 466 . . . . . 6
26 6 abscld 13267 . . . . . 6
27 25 , 26 eqeltrd 2545 . . . . 5
28 15 recnd 9643 . . . . . . 7
29 cvgcmpce.5 . . . . . . . 8
30 climdm 13377 . . . . . . . 8
31 29 , 30 sylib 196 . . . . . . 7
32 17 recnd 9643 . . . . . . 7
33 1 , 5 , 28 , 31 , 32 , 14 isermulc2 13480 . . . . . 6
34 climrel 13315 . . . . . . 7
35 34 releldmi 5244 . . . . . 6
36 33 , 35 syl 16 . . . . 5
37 1 uztrn2 11127 . . . . . . 7
38 2 , 37 sylan 471 . . . . . 6
39 6 absge0d 13275 . . . . . . 7
40 39 , 25 breqtrrd 4478 . . . . . 6
41 38 , 40 syldan 470 . . . . 5
42 cvgcmpce.7 . . . . . 6
43 38 , 24 syl 16 . . . . . 6
44 38 , 13 syl 16 . . . . . 6
45 42 , 43 , 44 3brtr4d 4482 . . . . 5
46 1 , 2 , 19 , 27 , 36 , 41 , 45 cvgcmp 13630 . . . 4
47 1 climcau 13493 . . . 4
48 5 , 46 , 47 syl2anc 661 . . 3
49 1 , 5 , 27 serfre 12136 . . . . . . . . . . . . 13
50 49 ad2antrr 725 . . . . . . . . . . . 12
51 1 uztrn2 11127 . . . . . . . . . . . . 13
52 51 adantl 466 . . . . . . . . . . . 12
53 50 , 52 ffvelrnd 6032 . . . . . . . . . . 11
54 simprl 756 . . . . . . . . . . . 12
55 50 , 54 ffvelrnd 6032 . . . . . . . . . . 11
56 53 , 55 resubcld 10012 . . . . . . . . . 10
57 0red 9618 . . . . . . . . . . 11
58 7 ad2antrr 725 . . . . . . . . . . . . . 14
59 58 , 52 ffvelrnd 6032 . . . . . . . . . . . . 13
60 58 , 54 ffvelrnd 6032 . . . . . . . . . . . . 13
61 59 , 60 subcld 9954 . . . . . . . . . . . 12
62 61 abscld 13267 . . . . . . . . . . 11
63 61 absge0d 13275 . . . . . . . . . . 11
64 fzfid 12083 . . . . . . . . . . . . . 14
65 difss 3630 . . . . . . . . . . . . . 14
66 ssfi 7760 . . . . . . . . . . . . . 14
67 64 , 65 , 66 sylancl 662 . . . . . . . . . . . . 13
68 eldifi 3625 . . . . . . . . . . . . . 14
69 simpll 753 . . . . . . . . . . . . . . 15
70 elfzuz 11713 . . . . . . . . . . . . . . . 16
71 70 , 1 syl6eleqr 2556 . . . . . . . . . . . . . . 15
72 69 , 71 , 6 syl2an 477 . . . . . . . . . . . . . 14
73 68 , 72 sylan2 474 . . . . . . . . . . . . 13
74 67 , 73 fsumabs 13615 . . . . . . . . . . . 12
75 eqidd 2458 . . . . . . . . . . . . . . . 16
76 52 , 1 syl6eleq 2555 . . . . . . . . . . . . . . . 16
77 75 , 76 , 72 fsumser 13552 . . . . . . . . . . . . . . 15
78 eqidd 2458 . . . . . . . . . . . . . . . 16
79 54 , 1 syl6eleq 2555 . . . . . . . . . . . . . . . 16
80 elfzuz 11713 . . . . . . . . . . . . . . . . . 18
81 80 , 1 syl6eleqr 2556 . . . . . . . . . . . . . . . . 17
82 69 , 81 , 6 syl2an 477 . . . . . . . . . . . . . . . 16
83 78 , 79 , 82 fsumser 13552 . . . . . . . . . . . . . . 15
84 77 , 83 oveq12d 6314 . . . . . . . . . . . . . 14
85 disjdif 3900 . . . . . . . . . . . . . . . . . 18
86 85 a1i 11 . . . . . . . . . . . . . . . . 17
87 undif2 3904 . . . . . . . . . . . . . . . . . 18
88 fzss2 11752 . . . . . . . . . . . . . . . . . . . 20
89 88 ad2antll 728 . . . . . . . . . . . . . . . . . . 19
90 ssequn1 3673 . . . . . . . . . . . . . . . . . . 19
91 89 , 90 sylib 196 . . . . . . . . . . . . . . . . . 18
92 87 , 91 syl5req 2511 . . . . . . . . . . . . . . . . 17
93 86 , 92 , 64 , 72 fsumsplit 13562 . . . . . . . . . . . . . . . 16
94 93 eqcomd 2465 . . . . . . . . . . . . . . 15
95 64 , 72 fsumcl 13555 . . . . . . . . . . . . . . . 16
96 fzfid 12083 . . . . . . . . . . . . . . . . 17
97 96 , 82 fsumcl 13555 . . . . . . . . . . . . . . . 16
98 67 , 73 fsumcl 13555 . . . . . . . . . . . . . . . 16
99 95 , 97 , 98 subaddd 9972 . . . . . . . . . . . . . . 15
100 94 , 99 mpbird 232 . . . . . . . . . . . . . 14
101 84 , 100 eqtr3d 2500 . . . . . . . . . . . . 13
102 101 fveq2d 5875 . . . . . . . . . . . 12
103 71 adantl 466 . . . . . . . . . . . . . . . 16
104 103 , 24 syl 16 . . . . . . . . . . . . . . 15
105 abscl 13111 . . . . . . . . . . . . . . . . 17
106 105 recnd 9643 . . . . . . . . . . . . . . . 16
107 72 , 106 syl 16 . . . . . . . . . . . . . . 15
108 104 , 76 , 107 fsumser 13552 . . . . . . . . . . . . . 14
109 81 adantl 466 . . . . . . . . . . . . . . . 16
110 109 , 24 syl 16 . . . . . . . . . . . . . . 15
111 82 , 106 syl 16 . . . . . . . . . . . . . . 15
112 110 , 79 , 111 fsumser 13552 . . . . . . . . . . . . . 14
113 108 , 112 oveq12d 6314 . . . . . . . . . . . . 13
114 86 , 92 , 64 , 107 fsumsplit 13562 . . . . . . . . . . . . . . 15
115 114 eqcomd 2465 . . . . . . . . . . . . . 14
116 64 , 107 fsumcl 13555 . . . . . . . . . . . . . . 15
117 96 , 111 fsumcl 13555 . . . . . . . . . . . . . . 15
118 73 , 106 syl 16 . . . . . . . . . . . . . . . 16
119 67 , 118 fsumcl 13555 . . . . . . . . . . . . . . 15
120 116 , 117 ,
119 subaddd 9972 . . . . . . . . . . . . . 14
121 115 , 120 mpbird 232 . . . . . . . . . . . . 13
122 113 , 121 eqtr3d 2500 . . . . . . . . . . . 12
123 74 , 102 , 122 3brtr4d 4482 . . . . . . . . . . 11
124 57 , 62 , 56 , 63 , 123 letrd 9760 . . . . . . . . . 10
125 56 , 124 absidd 13254 . . . . . . . . 9
126 125 breq1d 4462 . . . . . . . 8
127 rpre 11255 . . . . . . . . . . 11
128 127 ad2antlr 726 . . . . . . . . . 10
129 lelttr 9696 . . . . . . . . . 10
130 62 , 56 , 128 , 129 syl3anc 1228 . . . . . . . . 9
131 123 , 130 mpand 675 . . . . . . . 8
132 126 , 131 sylbid 215 . . . . . . 7
133 132 anassrs 648 . . . . . 6
134 133 ralimdva 2865 . . . . 5
135 134 reximdva 2932 . . . 4
136 135 ralimdva 2865 . . 3
137 48 , 136 mpd 15 . 2
138 seqex 12109 . . 3
139 138 a1i 11 . 2
140 1 , 8 , 137 , 139 caucvg 13501 1
