Step | Hyp | Ref
| Expression |
1 | | reprval.a |
. . 3
|
2 | | reprval.m |
. . 3
|
3 | | reprval.s |
. . . 4
|
4 | | 1nn0 11308 |
. . . . 5
|
5 | 4 | a1i 11 |
. . . 4
|
6 | 3, 5 | nn0addcld 11355 |
. . 3
|
7 | 1, 2, 6 | reprval 30688 |
. 2
repr
..^ ..^ |
8 | | simplr 792 |
. . . . . . . . . 10
..^ ..^ ..^ |
9 | | elmapi 7879 |
. . . . . . . . . 10
..^ ..^ |
10 | 8, 9 | syl 17 |
. . . . . . . . 9
..^ ..^ ..^ |
11 | 3 | ad2antrr 762 |
. . . . . . . . . 10
..^ ..^ |
12 | | fzonn0p1 12544 |
. . . . . . . . . 10
..^ |
13 | 11, 12 | syl 17 |
. . . . . . . . 9
..^ ..^ ..^ |
14 | 10, 13 | ffvelrnd 6360 |
. . . . . . . 8
..^ ..^ |
15 | | simpr 477 |
. . . . . . . . . . 11
..^
..^ |
16 | 15 | oveq2d 6666 |
. . . . . . . . . 10
..^
..^ |
17 | 16 | oveq2d 6666 |
. . . . . . . . 9
..^
..^ repr repr |
18 | | opeq2 4403 |
. . . . . . . . . . . . 13
|
19 | 18 | sneqd 4189 |
. . . . . . . . . . . 12
|
20 | 19 | uneq2d 3767 |
. . . . . . . . . . 11
|
21 | 20 | eqeq2d 2632 |
. . . . . . . . . 10
|
22 | 21 | adantl 482 |
. . . . . . . . 9
..^
..^ |
23 | 17, 22 | rexeqbidv 3153 |
. . . . . . . 8
..^
..^ repr
repr |
24 | 9 | adantl 482 |
. . . . . . . . . . . . . . 15
..^
..^ |
25 | 3 | adantr 481 |
. . . . . . . . . . . . . . . 16
..^
|
26 | | fzossfzop1 12545 |
. . . . . . . . . . . . . . . 16
..^ ..^ |
27 | 25, 26 | syl 17 |
. . . . . . . . . . . . . . 15
..^
..^ ..^ |
28 | 24, 27 | fssresd 6071 |
. . . . . . . . . . . . . 14
..^
..^..^ |
29 | 28 | adantr 481 |
. . . . . . . . . . . . 13
..^ ..^ ..^..^ |
30 | | nnex 11026 |
. . . . . . . . . . . . . . . . 17
|
31 | 30 | a1i 11 |
. . . . . . . . . . . . . . . 16
|
32 | 31, 1 | ssexd 4805 |
. . . . . . . . . . . . . . 15
|
33 | | fzofi 12773 |
. . . . . . . . . . . . . . . 16
..^ |
34 | 33 | elexi 3213 |
. . . . . . . . . . . . . . 15
..^ |
35 | | elmapg 7870 |
. . . . . . . . . . . . . . 15
..^ ..^ ..^ ..^..^ |
36 | 32, 34, 35 | sylancl 694 |
. . . . . . . . . . . . . 14
..^ ..^ ..^..^ |
37 | 36 | ad2antrr 762 |
. . . . . . . . . . . . 13
..^ ..^ ..^ ..^
..^..^ |
38 | 29, 37 | mpbird 247 |
. . . . . . . . . . . 12
..^ ..^ ..^ ..^ |
39 | 33 | a1i 11 |
. . . . . . . . . . . . . . . 16
..^
..^ |
40 | | nnsscn 11025 |
. . . . . . . . . . . . . . . . . . . 20
|
41 | 40 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
|
42 | 1, 41 | sstrd 3613 |
. . . . . . . . . . . . . . . . . 18
|
43 | 42 | ad2antrr 762 |
. . . . . . . . . . . . . . . . 17
..^ ..^
|
44 | 28 | ffvelrnda 6359 |
. . . . . . . . . . . . . . . . 17
..^ ..^
..^ |
45 | 43, 44 | sseldd 3604 |
. . . . . . . . . . . . . . . 16
..^ ..^
..^ |
46 | 39, 45 | fsumcl 14464 |
. . . . . . . . . . . . . . 15
..^
..^ ..^ |
47 | 46 | adantr 481 |
. . . . . . . . . . . . . 14
..^ ..^ ..^ ..^ |
48 | 42 | adantr 481 |
. . . . . . . . . . . . . . . 16
..^
|
49 | 25, 12 | syl 17 |
. . . . . . . . . . . . . . . . 17
..^
..^ |
50 | 24, 49 | ffvelrnd 6360 |
. . . . . . . . . . . . . . . 16
..^
|
51 | 48, 50 | sseldd 3604 |
. . . . . . . . . . . . . . 15
..^
|
52 | 51 | adantr 481 |
. . . . . . . . . . . . . 14
..^ ..^ |
53 | 47, 52 | pncand 10393 |
. . . . . . . . . . . . 13
..^ ..^
..^
..^ ..^ ..^ |
54 | | nfv 1843 |
. . . . . . . . . . . . . . . . . 18
..^ |
55 | | nfcv 2764 |
. . . . . . . . . . . . . . . . . 18
|
56 | | fzonel 12483 |
. . . . . . . . . . . . . . . . . . 19
..^ |
57 | 56 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
..^
..^ |
58 | 24 | adantr 481 |
. . . . . . . . . . . . . . . . . . . 20
..^ ..^
..^ |
59 | 27 | sselda 3603 |
. . . . . . . . . . . . . . . . . . . 20
..^ ..^
..^ |
60 | 58, 59 | ffvelrnd 6360 |
. . . . . . . . . . . . . . . . . . 19
..^ ..^
|
61 | 43, 60 | sseldd 3604 |
. . . . . . . . . . . . . . . . . 18
..^ ..^
|
62 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . 18
|
63 | 54, 55, 39, 25, 57, 61, 62, 51 | fsumsplitsn 14474 |
. . . . . . . . . . . . . . . . 17
..^
..^ ..^ |
64 | | fzosplitsn 12576 |
. . . . . . . . . . . . . . . . . . . 20
..^ ..^ |
65 | | nn0uz 11722 |
. . . . . . . . . . . . . . . . . . . 20
|
66 | 64, 65 | eleq2s 2719 |
. . . . . . . . . . . . . . . . . . 19
..^ ..^ |
67 | 25, 66 | syl 17 |
. . . . . . . . . . . . . . . . . 18
..^
..^ ..^ |
68 | 67 | sumeq1d 14431 |
. . . . . . . . . . . . . . . . 17
..^
..^ ..^ |
69 | | simpr 477 |
. . . . . . . . . . . . . . . . . . . 20
..^ ..^
..^ |
70 | 69 | fvresd 6208 |
. . . . . . . . . . . . . . . . . . 19
..^ ..^
..^ |
71 | 70 | sumeq2dv 14433 |
. . . . . . . . . . . . . . . . . 18
..^
..^ ..^ ..^ |
72 | 71 | oveq1d 6665 |
. . . . . . . . . . . . . . . . 17
..^
..^
..^
..^ |
73 | 63, 68, 72 | 3eqtr4d 2666 |
. . . . . . . . . . . . . . . 16
..^
..^
..^
..^ |
74 | 73 | adantr 481 |
. . . . . . . . . . . . . . 15
..^ ..^ ..^ ..^ ..^ |
75 | | simpr 477 |
. . . . . . . . . . . . . . 15
..^ ..^ ..^ |
76 | 74, 75 | eqtr3d 2658 |
. . . . . . . . . . . . . 14
..^ ..^ ..^ ..^ |
77 | 76 | oveq1d 6665 |
. . . . . . . . . . . . 13
..^ ..^
..^
..^ |
78 | 53, 77 | eqtr3d 2658 |
. . . . . . . . . . . 12
..^ ..^ ..^ ..^ |
79 | 38, 78 | jca 554 |
. . . . . . . . . . 11
..^ ..^ ..^ ..^
..^
..^ |
80 | | fveq1 6190 |
. . . . . . . . . . . . . 14
..^ ..^ |
81 | 80 | sumeq2sdv 14435 |
. . . . . . . . . . . . 13
..^ ..^ ..^ ..^ |
82 | 81 | eqeq1d 2624 |
. . . . . . . . . . . 12
..^ ..^
..^ ..^ |
83 | 82 | elrab 3363 |
. . . . . . . . . . 11
..^ ..^ ..^
..^ ..^ ..^
..^ |
84 | 79, 83 | sylibr 224 |
. . . . . . . . . 10
..^ ..^ ..^ ..^ ..^ |
85 | 1 | ad2antrr 762 |
. . . . . . . . . . 11
..^ ..^ |
86 | 2 | ad2antrr 762 |
. . . . . . . . . . . 12
..^ ..^ |
87 | | nnssz 11397 |
. . . . . . . . . . . . . . 15
|
88 | 1, 87 | syl6ss 3615 |
. . . . . . . . . . . . . 14
|
89 | 88 | ad2antrr 762 |
. . . . . . . . . . . . 13
..^ ..^ |
90 | 89, 14 | sseldd 3604 |
. . . . . . . . . . . 12
..^ ..^ |
91 | 86, 90 | zsubcld 11487 |
. . . . . . . . . . 11
..^ ..^ |
92 | 85, 91, 11 | reprval 30688 |
. . . . . . . . . 10
..^ ..^ repr ..^ ..^ |
93 | 84, 92 | eleqtrrd 2704 |
. . . . . . . . 9
..^ ..^ ..^ repr |
94 | | simpr 477 |
. . . . . . . . . . 11
..^
..^ ..^
..^ |
95 | 94 | uneq1d 3766 |
. . . . . . . . . 10
..^
..^ ..^
..^ |
96 | 95 | eqeq2d 2632 |
. . . . . . . . 9
..^
..^ ..^
..^ |
97 | 10 | ffnd 6046 |
. . . . . . . . . . 11
..^ ..^ ..^ |
98 | | fnsnsplit 6450 |
. . . . . . . . . . 11
..^ ..^
..^ |
99 | 97, 13, 98 | syl2anc 693 |
. . . . . . . . . 10
..^ ..^ ..^ |
100 | 11, 65 | syl6eleq 2711 |
. . . . . . . . . . . . 13
..^ ..^ |
101 | | fzodif2 29552 |
. . . . . . . . . . . . 13
..^ ..^ |
102 | 100, 101 | syl 17 |
. . . . . . . . . . . 12
..^ ..^ ..^ ..^ |
103 | 102 | reseq2d 5396 |
. . . . . . . . . . 11
..^ ..^ ..^ ..^ |
104 | 103 | uneq1d 3766 |
. . . . . . . . . 10
..^ ..^ ..^ ..^ |
105 | 99, 104 | eqtrd 2656 |
. . . . . . . . 9
..^ ..^ ..^ |
106 | 93, 96, 105 | rspcedvd 3317 |
. . . . . . . 8
..^ ..^ repr |
107 | 14, 23, 106 | rspcedvd 3317 |
. . . . . . 7
..^ ..^
repr |
108 | 107 | anasss 679 |
. . . . . 6
..^ ..^
repr |
109 | | simpr 477 |
. . . . . . . . 9
repr
|
110 | 1 | adantr 481 |
. . . . . . . . . . . . . . 15
|
111 | 110 | adantr 481 |
. . . . . . . . . . . . . 14
repr
|
112 | 2 | adantr 481 |
. . . . . . . . . . . . . . . 16
|
113 | 88 | sselda 3603 |
. . . . . . . . . . . . . . . 16
|
114 | 112, 113 | zsubcld 11487 |
. . . . . . . . . . . . . . 15
|
115 | 114 | adantr 481 |
. . . . . . . . . . . . . 14
repr
|
116 | 3 | adantr 481 |
. . . . . . . . . . . . . . 15
|
117 | 116 | adantr 481 |
. . . . . . . . . . . . . 14
repr
|
118 | | simpr 477 |
. . . . . . . . . . . . . 14
repr
repr |
119 | 111, 115,
117, 118 | reprf 30690 |
. . . . . . . . . . . . 13
repr
..^ |
120 | | simplr 792 |
. . . . . . . . . . . . . 14
repr
|
121 | 117, 120 | fsnd 6179 |
. . . . . . . . . . . . 13
repr
|
122 | | fzodisjsn 12505 |
. . . . . . . . . . . . . 14
..^ |
123 | 122 | a1i 11 |
. . . . . . . . . . . . 13
repr
..^ |
124 | 119, 121,
123 | fun2d 6068 |
. . . . . . . . . . . 12
repr
..^ |
125 | 117, 66 | syl 17 |
. . . . . . . . . . . . 13
repr
..^ ..^ |
126 | 125 | feq2d 6031 |
. . . . . . . . . . . 12
repr
..^
..^ |
127 | 124, 126 | mpbird 247 |
. . . . . . . . . . 11
repr
..^ |
128 | | ovex 6678 |
. . . . . . . . . . . . 13
..^ |
129 | | elmapg 7870 |
. . . . . . . . . . . . 13
..^ ..^
..^ |
130 | 32, 128, 129 | sylancl 694 |
. . . . . . . . . . . 12
..^
..^ |
131 | 130 | ad2antrr 762 |
. . . . . . . . . . 11
repr
..^ ..^ |
132 | 127, 131 | mpbird 247 |
. . . . . . . . . 10
repr
..^ |
133 | 132 | adantr 481 |
. . . . . . . . 9
repr
..^ |
134 | 109, 133 | eqeltrd 2701 |
. . . . . . . 8
repr
..^ |
135 | 125 | adantr 481 |
. . . . . . . . . 10
repr
..^ ..^ |
136 | 135 | sumeq1d 14431 |
. . . . . . . . 9
repr
..^ ..^ |
137 | | nfv 1843 |
. . . . . . . . . 10
repr |
138 | 33 | a1i 11 |
. . . . . . . . . 10
repr
..^ |
139 | 117 | adantr 481 |
. . . . . . . . . 10
repr
|
140 | 56 | a1i 11 |
. . . . . . . . . 10
repr
..^ |
141 | 42 | ad4antr 768 |
. . . . . . . . . . 11
repr ..^
|
142 | 127 | adantr 481 |
. . . . . . . . . . . . . 14
repr
..^ |
143 | 109 | feq1d 6030 |
. . . . . . . . . . . . . 14
repr
..^ ..^ |
144 | 142, 143 | mpbird 247 |
. . . . . . . . . . . . 13
repr
..^ |
145 | 144 | adantr 481 |
. . . . . . . . . . . 12
repr ..^
..^ |
146 | | simpr 477 |
. . . . . . . . . . . . . 14
repr ..^
..^ |
147 | | elun1 3780 |
. . . . . . . . . . . . . 14
..^
..^ |
148 | 146, 147 | syl 17 |
. . . . . . . . . . . . 13
repr ..^
..^ |
149 | 125 | ad2antrr 762 |
. . . . . . . . . . . . 13
repr ..^
..^ ..^ |
150 | 148, 149 | eleqtrrd 2704 |
. . . . . . . . . . . 12
repr ..^
..^ |
151 | 145, 150 | ffvelrnd 6360 |
. . . . . . . . . . 11
repr ..^
|
152 | 141, 151 | sseldd 3604 |
. . . . . . . . . 10
repr ..^
|
153 | 42 | ad3antrrr 766 |
. . . . . . . . . . 11
repr
|
154 | 139, 12 | syl 17 |
. . . . . . . . . . . 12
repr
..^ |
155 | 144, 154 | ffvelrnd 6360 |
. . . . . . . . . . 11
repr
|
156 | 153, 155 | sseldd 3604 |
. . . . . . . . . 10
repr
|
157 | 137, 55, 138, 139, 140, 152, 62, 156 | fsumsplitsn 14474 |
. . . . . . . . 9
repr
..^
..^ |
158 | | simplr 792 |
. . . . . . . . . . . . . . . 16
repr ..^
|
159 | 158 | fveq1d 6193 |
. . . . . . . . . . . . . . 15
repr ..^
|
160 | 119 | ffnd 6046 |
. . . . . . . . . . . . . . . . 17
repr
..^ |
161 | 160 | ad2antrr 762 |
. . . . . . . . . . . . . . . 16
repr ..^
..^ |
162 | 121 | ffnd 6046 |
. . . . . . . . . . . . . . . . 17
repr
|
163 | 162 | ad2antrr 762 |
. . . . . . . . . . . . . . . 16
repr ..^
|
164 | 122 | a1i 11 |
. . . . . . . . . . . . . . . 16
repr ..^
..^ |
165 | | fvun1 6269 |
. . . . . . . . . . . . . . . 16
..^
..^
..^ |
166 | 161, 163,
164, 146, 165 | syl112anc 1330 |
. . . . . . . . . . . . . . 15
repr ..^
|
167 | 159, 166 | eqtrd 2656 |
. . . . . . . . . . . . . 14
repr ..^
|
168 | 167 | ralrimiva 2966 |
. . . . . . . . . . . . 13
repr
..^ |
169 | 168 | sumeq2d 14432 |
. . . . . . . . . . . 12
repr
..^ ..^ |
170 | 111 | adantr 481 |
. . . . . . . . . . . . 13
repr
|
171 | 115 | adantr 481 |
. . . . . . . . . . . . 13
repr
|
172 | 118 | adantr 481 |
. . . . . . . . . . . . 13
repr
repr |
173 | 170, 171,
139, 172 | reprsum 30691 |
. . . . . . . . . . . 12
repr
..^ |
174 | 169, 173 | eqtrd 2656 |
. . . . . . . . . . 11
repr
..^ |
175 | 109 | fveq1d 6193 |
. . . . . . . . . . . 12
repr
|
176 | 160 | adantr 481 |
. . . . . . . . . . . . 13
repr
..^ |
177 | 162 | adantr 481 |
. . . . . . . . . . . . 13
repr
|
178 | 122 | a1i 11 |
. . . . . . . . . . . . 13
repr
..^ |
179 | | snidg 4206 |
. . . . . . . . . . . . . 14
|
180 | 139, 179 | syl 17 |
. . . . . . . . . . . . 13
repr
|
181 | | fvun2 6270 |
. . . . . . . . . . . . 13
..^
..^
|
182 | 176, 177,
178, 180, 181 | syl112anc 1330 |
. . . . . . . . . . . 12
repr
|
183 | 120 | adantr 481 |
. . . . . . . . . . . . 13
repr
|
184 | | fvsng 6447 |
. . . . . . . . . . . . 13
|
185 | 139, 183,
184 | syl2anc 693 |
. . . . . . . . . . . 12
repr
|
186 | 175, 182,
185 | 3eqtrd 2660 |
. . . . . . . . . . 11
repr
|
187 | 174, 186 | oveq12d 6668 |
. . . . . . . . . 10
repr
..^ |
188 | | zsscn 11385 |
. . . . . . . . . . . 12
|
189 | 112 | ad2antrr 762 |
. . . . . . . . . . . 12
repr
|
190 | 188, 189 | sseldi 3601 |
. . . . . . . . . . 11
repr
|
191 | 186, 156 | eqeltrrd 2702 |
. . . . . . . . . . 11
repr
|
192 | 190, 191 | npcand 10396 |
. . . . . . . . . 10
repr
|
193 | 187, 192 | eqtrd 2656 |
. . . . . . . . 9
repr
..^ |
194 | 136, 157,
193 | 3eqtrd 2660 |
. . . . . . . 8
repr
..^ |
195 | 134, 194 | jca 554 |
. . . . . . 7
repr
..^ ..^ |
196 | 195 | r19.29ffa 29320 |
. . . . . 6
repr ..^ ..^ |
197 | 108, 196 | impbida 877 |
. . . . 5
..^ ..^
repr |
198 | | reprsuc.f |
. . . . . . 7
repr |
199 | | vex 3203 |
. . . . . . . 8
|
200 | | snex 4908 |
. . . . . . . 8
|
201 | 199, 200 | unex 6956 |
. . . . . . 7
|
202 | 198, 201 | elrnmpti 5376 |
. . . . . 6
repr |
203 | 202 | rexbii 3041 |
. . . . 5
repr |
204 | 197, 203 | syl6bbr 278 |
. . . 4
..^ ..^
|
205 | | fveq1 6190 |
. . . . . . . 8
|
206 | 205 | sumeq2sdv 14435 |
. . . . . . 7
..^ ..^ |
207 | 206 | eqeq1d 2624 |
. . . . . 6
..^ ..^ |
208 | 207 | cbvrabv 3199 |
. . . . 5
..^ ..^ ..^ ..^ |
209 | 208 | rabeq2i 3197 |
. . . 4
..^ ..^
..^ ..^ |
210 | | eliun 4524 |
. . . 4
|
211 | 204, 209,
210 | 3bitr4g 303 |
. . 3
..^
..^
|
212 | 211 | eqrdv 2620 |
. 2
..^ ..^ |
213 | 7, 212 | eqtrd 2656 |
1
repr
|