Step | Hyp | Ref
| Expression |
1 | | fprodefsum.2 |
. . . 4
|
2 | | fprodefsum.1 |
. . . 4
|
3 | 1, 2 | syl6eleq 2711 |
. . 3
|
4 | | oveq2 6658 |
. . . . . . 7
|
5 | 4 | prodeq1d 14651 |
. . . . . 6
|
6 | 4 | sumeq1d 14431 |
. . . . . . 7
|
7 | 6 | fveq2d 6195 |
. . . . . 6
|
8 | 5, 7 | eqeq12d 2637 |
. . . . 5
|
9 | 8 | imbi2d 330 |
. . . 4
|
10 | | oveq2 6658 |
. . . . . . 7
|
11 | 10 | prodeq1d 14651 |
. . . . . 6
|
12 | 10 | sumeq1d 14431 |
. . . . . . 7
|
13 | 12 | fveq2d 6195 |
. . . . . 6
|
14 | 11, 13 | eqeq12d 2637 |
. . . . 5
|
15 | 14 | imbi2d 330 |
. . . 4
|
16 | | oveq2 6658 |
. . . . . . 7
|
17 | 16 | prodeq1d 14651 |
. . . . . 6
|
18 | 16 | sumeq1d 14431 |
. . . . . . 7
|
19 | 18 | fveq2d 6195 |
. . . . . 6
|
20 | 17, 19 | eqeq12d 2637 |
. . . . 5
|
21 | 20 | imbi2d 330 |
. . . 4
|
22 | | oveq2 6658 |
. . . . . . 7
|
23 | 22 | prodeq1d 14651 |
. . . . . 6
|
24 | 22 | sumeq1d 14431 |
. . . . . . 7
|
25 | 24 | fveq2d 6195 |
. . . . . 6
|
26 | 23, 25 | eqeq12d 2637 |
. . . . 5
|
27 | 26 | imbi2d 330 |
. . . 4
|
28 | | fzsn 12383 |
. . . . . . . . 9
|
29 | 28 | adantl 482 |
. . . . . . . 8
|
30 | 29 | prodeq1d 14651 |
. . . . . . 7
|
31 | | simpr 477 |
. . . . . . . 8
|
32 | | uzid 11702 |
. . . . . . . . . 10
|
33 | 32, 2 | syl6eleqr 2712 |
. . . . . . . . 9
|
34 | | fprodefsum.3 |
. . . . . . . . . . . 12
|
35 | | efcl 14813 |
. . . . . . . . . . . 12
|
36 | 34, 35 | syl 17 |
. . . . . . . . . . 11
|
37 | | eqid 2622 |
. . . . . . . . . . 11
|
38 | 36, 37 | fmptd 6385 |
. . . . . . . . . 10
|
39 | 38 | ffvelrnda 6359 |
. . . . . . . . 9
|
40 | 33, 39 | sylan2 491 |
. . . . . . . 8
|
41 | | fveq2 6191 |
. . . . . . . . 9
|
42 | 41 | prodsn 14692 |
. . . . . . . 8
|
43 | 31, 40, 42 | syl2anc 693 |
. . . . . . 7
|
44 | 33 | adantl 482 |
. . . . . . . 8
|
45 | | fvex 6201 |
. . . . . . . 8
|
46 | | nfcv 2764 |
. . . . . . . . 9
|
47 | | nfcv 2764 |
. . . . . . . . . 10
|
48 | | nfcsb1v 3549 |
. . . . . . . . . 10
|
49 | 47, 48 | nffv 6198 |
. . . . . . . . 9
|
50 | | csbeq1a 3542 |
. . . . . . . . . 10
|
51 | 50 | fveq2d 6195 |
. . . . . . . . 9
|
52 | 46, 49, 51, 37 | fvmptf 6301 |
. . . . . . . 8
|
53 | 44, 45, 52 | sylancl 694 |
. . . . . . 7
|
54 | 30, 43, 53 | 3eqtrd 2660 |
. . . . . 6
|
55 | 29 | sumeq1d 14431 |
. . . . . . . 8
|
56 | | eqid 2622 |
. . . . . . . . . . . 12
|
57 | 34, 56 | fmptd 6385 |
. . . . . . . . . . 11
|
58 | 57 | ffvelrnda 6359 |
. . . . . . . . . 10
|
59 | 33, 58 | sylan2 491 |
. . . . . . . . 9
|
60 | | fveq2 6191 |
. . . . . . . . . 10
|
61 | 60 | sumsn 14475 |
. . . . . . . . 9
|
62 | 31, 59, 61 | syl2anc 693 |
. . . . . . . 8
|
63 | 34 | ralrimiva 2966 |
. . . . . . . . . 10
|
64 | 48 | nfel1 2779 |
. . . . . . . . . . . 12
|
65 | 50 | eleq1d 2686 |
. . . . . . . . . . . 12
|
66 | 64, 65 | rspc 3303 |
. . . . . . . . . . 11
|
67 | 66 | impcom 446 |
. . . . . . . . . 10
|
68 | 63, 33, 67 | syl2an 494 |
. . . . . . . . 9
|
69 | 56 | fvmpts 6285 |
. . . . . . . . 9
|
70 | 44, 68, 69 | syl2anc 693 |
. . . . . . . 8
|
71 | 55, 62, 70 | 3eqtrd 2660 |
. . . . . . 7
|
72 | 71 | fveq2d 6195 |
. . . . . 6
|
73 | 54, 72 | eqtr4d 2659 |
. . . . 5
|
74 | 73 | expcom 451 |
. . . 4
|
75 | | simp3 1063 |
. . . . . . . . . 10
|
76 | 2 | peano2uzs 11742 |
. . . . . . . . . . . 12
|
77 | | simpr 477 |
. . . . . . . . . . . . . 14
|
78 | | nfcsb1v 3549 |
. . . . . . . . . . . . . . . . . 18
|
79 | 78 | nfel1 2779 |
. . . . . . . . . . . . . . . . 17
|
80 | | csbeq1a 3542 |
. . . . . . . . . . . . . . . . . 18
|
81 | 80 | eleq1d 2686 |
. . . . . . . . . . . . . . . . 17
|
82 | 79, 81 | rspc 3303 |
. . . . . . . . . . . . . . . 16
|
83 | 63, 82 | mpan9 486 |
. . . . . . . . . . . . . . 15
|
84 | | efcl 14813 |
. . . . . . . . . . . . . . 15
|
85 | 83, 84 | syl 17 |
. . . . . . . . . . . . . 14
|
86 | | nfcv 2764 |
. . . . . . . . . . . . . . 15
|
87 | 47, 78 | nffv 6198 |
. . . . . . . . . . . . . . 15
|
88 | 80 | fveq2d 6195 |
. . . . . . . . . . . . . . 15
|
89 | 86, 87, 88, 37 | fvmptf 6301 |
. . . . . . . . . . . . . 14
|
90 | 77, 85, 89 | syl2anc 693 |
. . . . . . . . . . . . 13
|
91 | 56 | fvmpts 6285 |
. . . . . . . . . . . . . . 15
|
92 | 77, 83, 91 | syl2anc 693 |
. . . . . . . . . . . . . 14
|
93 | 92 | fveq2d 6195 |
. . . . . . . . . . . . 13
|
94 | 90, 93 | eqtr4d 2659 |
. . . . . . . . . . . 12
|
95 | 76, 94 | sylan2 491 |
. . . . . . . . . . 11
|
96 | 95 | 3adant3 1081 |
. . . . . . . . . 10
|
97 | 75, 96 | oveq12d 6668 |
. . . . . . . . 9
|
98 | | simpr 477 |
. . . . . . . . . . . 12
|
99 | 98, 2 | syl6eleq 2711 |
. . . . . . . . . . 11
|
100 | | elfzuz 12338 |
. . . . . . . . . . . . . 14
|
101 | 100, 2 | syl6eleqr 2712 |
. . . . . . . . . . . . 13
|
102 | 38 | ffvelrnda 6359 |
. . . . . . . . . . . . 13
|
103 | 101, 102 | sylan2 491 |
. . . . . . . . . . . 12
|
104 | 103 | adantlr 751 |
. . . . . . . . . . 11
|
105 | | fveq2 6191 |
. . . . . . . . . . 11
|
106 | 99, 104, 105 | fprodp1 14699 |
. . . . . . . . . 10
|
107 | 106 | 3adant3 1081 |
. . . . . . . . 9
|
108 | 57 | ffvelrnda 6359 |
. . . . . . . . . . . . . . 15
|
109 | 101, 108 | sylan2 491 |
. . . . . . . . . . . . . 14
|
110 | 109 | adantlr 751 |
. . . . . . . . . . . . 13
|
111 | | fveq2 6191 |
. . . . . . . . . . . . 13
|
112 | 99, 110, 111 | fsump1 14487 |
. . . . . . . . . . . 12
|
113 | 112 | fveq2d 6195 |
. . . . . . . . . . 11
|
114 | | fzfid 12772 |
. . . . . . . . . . . . 13
|
115 | | elfzuz 12338 |
. . . . . . . . . . . . . . . 16
|
116 | 115, 2 | syl6eleqr 2712 |
. . . . . . . . . . . . . . 15
|
117 | 116, 108 | sylan2 491 |
. . . . . . . . . . . . . 14
|
118 | 117 | adantlr 751 |
. . . . . . . . . . . . 13
|
119 | 114, 118 | fsumcl 14464 |
. . . . . . . . . . . 12
|
120 | 57 | ffvelrnda 6359 |
. . . . . . . . . . . . 13
|
121 | 76, 120 | sylan2 491 |
. . . . . . . . . . . 12
|
122 | | efadd 14824 |
. . . . . . . . . . . 12
|
123 | 119, 121,
122 | syl2anc 693 |
. . . . . . . . . . 11
|
124 | 113, 123 | eqtrd 2656 |
. . . . . . . . . 10
|
125 | 124 | 3adant3 1081 |
. . . . . . . . 9
|
126 | 97, 107, 125 | 3eqtr4d 2666 |
. . . . . . . 8
|
127 | 126 | 3exp 1264 |
. . . . . . 7
|
128 | 127 | com12 32 |
. . . . . 6
|
129 | 128 | a2d 29 |
. . . . 5
|
130 | 2 | eqcomi 2631 |
. . . . 5
|
131 | 129, 130 | eleq2s 2719 |
. . . 4
|
132 | 9, 15, 21, 27, 74, 131 | uzind4 11746 |
. . 3
|
133 | 3, 132 | mpcom 38 |
. 2
|
134 | | fzssuz 12382 |
. . . . . . . 8
|
135 | 134, 2 | sseqtr4i 3638 |
. . . . . . 7
|
136 | | resmpt 5449 |
. . . . . . 7
|
137 | 135, 136 | ax-mp 5 |
. . . . . 6
|
138 | 137 | fveq1i 6192 |
. . . . 5
|
139 | | fvres 6207 |
. . . . 5
|
140 | 138, 139 | syl5reqr 2671 |
. . . 4
|
141 | 140 | prodeq2i 14649 |
. . 3
|
142 | | prodfc 14675 |
. . 3
|
143 | 141, 142 | eqtri 2644 |
. 2
|
144 | | resmpt 5449 |
. . . . . . . 8
|
145 | 135, 144 | ax-mp 5 |
. . . . . . 7
|
146 | 145 | fveq1i 6192 |
. . . . . 6
|
147 | | fvres 6207 |
. . . . . 6
|
148 | 146, 147 | syl5reqr 2671 |
. . . . 5
|
149 | 148 | sumeq2i 14429 |
. . . 4
|
150 | | sumfc 14440 |
. . . 4
|
151 | 149, 150 | eqtri 2644 |
. . 3
|
152 | 151 | fveq2i 6194 |
. 2
|
153 | 133, 143,
152 | 3eqtr3g 2679 |
1
|