Step | Hyp | Ref
| Expression |
1 | | carsggect.1 |
. . 3
|
2 | | 0ex 4790 |
. . . 4
|
3 | 2 | a1i 11 |
. . 3
|
4 | | carsggect.0 |
. . 3
|
5 | | padct 29497 |
. . 3
|
6 | 1, 3, 4, 5 | syl3anc 1326 |
. 2
|
7 | | nfv 1843 |
. . . . 5
|
8 | | simpr1 1067 |
. . . . . . 7
|
9 | 8 | feqmptd 6249 |
. . . . . 6
|
10 | 9 | rneqd 5353 |
. . . . 5
|
11 | 7, 10 | esumeq1d 30097 |
. . . 4
Σ* Σ* |
12 | | fvex 6201 |
. . . . . . . . . 10
toCaraSiga |
13 | 12 | a1i 11 |
. . . . . . . . 9
toCaraSiga |
14 | | carsggect.2 |
. . . . . . . . . . 11
toCaraSiga |
15 | 14 | adantr 481 |
. . . . . . . . . 10
toCaraSiga |
16 | | carsgval.1 |
. . . . . . . . . . . . 13
|
17 | 16 | adantr 481 |
. . . . . . . . . . . 12
|
18 | | carsgval.2 |
. . . . . . . . . . . . 13
|
19 | 18 | adantr 481 |
. . . . . . . . . . . 12
|
20 | | carsgsiga.1 |
. . . . . . . . . . . . 13
|
21 | 20 | adantr 481 |
. . . . . . . . . . . 12
|
22 | 17, 19, 21 | 0elcarsg 30369 |
. . . . . . . . . . 11
toCaraSiga |
23 | 22 | snssd 4340 |
. . . . . . . . . 10
toCaraSiga |
24 | 15, 23 | unssd 3789 |
. . . . . . . . 9
toCaraSiga |
25 | 13, 24 | ssexd 4805 |
. . . . . . . 8
|
26 | 19 | adantr 481 |
. . . . . . . . 9
|
27 | 16, 18 | carsgcl 30366 |
. . . . . . . . . . . . 13
toCaraSiga |
28 | 14, 27 | sstrd 3613 |
. . . . . . . . . . . 12
|
29 | 28 | adantr 481 |
. . . . . . . . . . 11
|
30 | | 0elpw 4834 |
. . . . . . . . . . . . 13
|
31 | 30 | a1i 11 |
. . . . . . . . . . . 12
|
32 | 31 | snssd 4340 |
. . . . . . . . . . 11
|
33 | 29, 32 | unssd 3789 |
. . . . . . . . . 10
|
34 | 33 | sselda 3603 |
. . . . . . . . 9
|
35 | 26, 34 | ffvelrnd 6360 |
. . . . . . . 8
|
36 | | frn 6053 |
. . . . . . . . 9
|
37 | 8, 36 | syl 17 |
. . . . . . . 8
|
38 | 7, 25, 35, 37 | esummono 30116 |
. . . . . . 7
Σ*
Σ* |
39 | | ctex 7970 |
. . . . . . . . . 10
|
40 | 1, 39 | syl 17 |
. . . . . . . . 9
|
41 | 40 | adantr 481 |
. . . . . . . 8
|
42 | 13, 23 | ssexd 4805 |
. . . . . . . 8
|
43 | 19 | adantr 481 |
. . . . . . . . 9
|
44 | 29 | sselda 3603 |
. . . . . . . . 9
|
45 | 43, 44 | ffvelrnd 6360 |
. . . . . . . 8
|
46 | | elsni 4194 |
. . . . . . . . . . 11
|
47 | 46 | adantl 482 |
. . . . . . . . . 10
|
48 | 47 | fveq2d 6195 |
. . . . . . . . 9
|
49 | 21 | adantr 481 |
. . . . . . . . 9
|
50 | 48, 49 | eqtrd 2656 |
. . . . . . . 8
|
51 | 41, 42, 45, 50 | esumpad 30117 |
. . . . . . 7
Σ* Σ* |
52 | 38, 51 | breqtrd 4679 |
. . . . . 6
Σ*
Σ* |
53 | 37, 24 | sstrd 3613 |
. . . . . . . 8
toCaraSiga |
54 | | ssexg 4804 |
. . . . . . . 8
toCaraSiga toCaraSiga
|
55 | 53, 12, 54 | sylancl 694 |
. . . . . . 7
|
56 | 19 | adantr 481 |
. . . . . . . 8
|
57 | 37, 33 | sstrd 3613 |
. . . . . . . . 9
|
58 | 57 | sselda 3603 |
. . . . . . . 8
|
59 | 56, 58 | ffvelrnd 6360 |
. . . . . . 7
|
60 | | simpr2 1068 |
. . . . . . 7
|
61 | 7, 55, 59, 60 | esummono 30116 |
. . . . . 6
Σ*
Σ* |
62 | 52, 61 | jca 554 |
. . . . 5
Σ* Σ*
Σ*
Σ* |
63 | | iccssxr 12256 |
. . . . . . 7
|
64 | 59 | ralrimiva 2966 |
. . . . . . . 8
|
65 | | nfcv 2764 |
. . . . . . . . 9
|
66 | 65 | esumcl 30092 |
. . . . . . . 8
Σ* |
67 | 55, 64, 66 | syl2anc 693 |
. . . . . . 7
Σ* |
68 | 63, 67 | sseldi 3601 |
. . . . . 6
Σ* |
69 | 45 | ralrimiva 2966 |
. . . . . . . 8
|
70 | | nfcv 2764 |
. . . . . . . . 9
|
71 | 70 | esumcl 30092 |
. . . . . . . 8
Σ* |
72 | 41, 69, 71 | syl2anc 693 |
. . . . . . 7
Σ* |
73 | 63, 72 | sseldi 3601 |
. . . . . 6
Σ* |
74 | | xrletri3 11985 |
. . . . . 6
Σ*
Σ* Σ*
Σ* Σ*
Σ*
Σ*
Σ* |
75 | 68, 73, 74 | syl2anc 693 |
. . . . 5
Σ* Σ*
Σ* Σ*
Σ*
Σ* |
76 | 62, 75 | mpbird 247 |
. . . 4
Σ* Σ* |
77 | | fveq2 6191 |
. . . . 5
|
78 | | nnex 11026 |
. . . . . 6
|
79 | 78 | a1i 11 |
. . . . 5
|
80 | 19 | adantr 481 |
. . . . . 6
|
81 | 33 | adantr 481 |
. . . . . . 7
|
82 | 8 | adantr 481 |
. . . . . . . 8
|
83 | | simpr 477 |
. . . . . . . 8
|
84 | 82, 83 | ffvelrnd 6360 |
. . . . . . 7
|
85 | 81, 84 | sseldd 3604 |
. . . . . 6
|
86 | 80, 85 | ffvelrnd 6360 |
. . . . 5
|
87 | | simpr 477 |
. . . . . . 7
|
88 | 87 | fveq2d 6195 |
. . . . . 6
|
89 | 21 | ad2antrr 762 |
. . . . . 6
|
90 | 88, 89 | eqtrd 2656 |
. . . . 5
|
91 | | cnvimass 5485 |
. . . . . . . 8
|
92 | 91 | a1i 11 |
. . . . . . 7
|
93 | | fdm 6051 |
. . . . . . . 8
|
94 | 8, 93 | syl 17 |
. . . . . . 7
|
95 | 92, 94 | sseqtrd 3641 |
. . . . . 6
|
96 | | ffun 6048 |
. . . . . . . . . . 11
|
97 | 8, 96 | syl 17 |
. . . . . . . . . 10
|
98 | 97 | adantr 481 |
. . . . . . . . 9
|
99 | | difpreima 6343 |
. . . . . . . . . . . . 13
|
100 | 8, 96, 99 | 3syl 18 |
. . . . . . . . . . . 12
|
101 | | fimacnv 6347 |
. . . . . . . . . . . . . 14
|
102 | 8, 101 | syl 17 |
. . . . . . . . . . . . 13
|
103 | 102 | difeq1d 3727 |
. . . . . . . . . . . 12
|
104 | 100, 103 | eqtrd 2656 |
. . . . . . . . . . 11
|
105 | | uncom 3757 |
. . . . . . . . . . . . . . . 16
|
106 | 105 | difeq1i 3724 |
. . . . . . . . . . . . . . 15
|
107 | | difun2 4048 |
. . . . . . . . . . . . . . 15
|
108 | 106, 107 | eqtr3i 2646 |
. . . . . . . . . . . . . 14
|
109 | | difss 3737 |
. . . . . . . . . . . . . 14
|
110 | 108, 109 | eqsstri 3635 |
. . . . . . . . . . . . 13
|
111 | 110 | a1i 11 |
. . . . . . . . . . . 12
|
112 | | sspreima 29447 |
. . . . . . . . . . . 12
|
113 | 97, 111, 112 | syl2anc 693 |
. . . . . . . . . . 11
|
114 | 104, 113 | eqsstr3d 3640 |
. . . . . . . . . 10
|
115 | 114 | sselda 3603 |
. . . . . . . . 9
|
116 | | fvimacnvi 6331 |
. . . . . . . . 9
|
117 | 98, 115, 116 | syl2anc 693 |
. . . . . . . 8
|
118 | | elsni 4194 |
. . . . . . . 8
|
119 | 117, 118 | syl 17 |
. . . . . . 7
|
120 | 119 | ralrimiva 2966 |
. . . . . 6
|
121 | | carsggect.3 |
. . . . . . . 8
Disj
|
122 | 121 | adantr 481 |
. . . . . . 7
Disj |
123 | | simpr3 1069 |
. . . . . . . . . 10
|
124 | | fresf1o 29433 |
. . . . . . . . . 10
|
125 | 97, 60, 123, 124 | syl3anc 1326 |
. . . . . . . . 9
|
126 | | simpr 477 |
. . . . . . . . 9
|
127 | 125, 126 | disjrdx 29404 |
. . . . . . . 8
Disj Disj |
128 | | fvres 6207 |
. . . . . . . . . 10
|
129 | 128 | adantl 482 |
. . . . . . . . 9
|
130 | 129 | disjeq2dv 4625 |
. . . . . . . 8
Disj Disj |
131 | 127, 130 | bitr3d 270 |
. . . . . . 7
Disj
Disj |
132 | 122, 131 | mpbid 222 |
. . . . . 6
Disj |
133 | | disjss3 4652 |
. . . . . . 7
Disj
Disj |
134 | 133 | biimpa 501 |
. . . . . 6
Disj Disj |
135 | 95, 120, 132, 134 | syl21anc 1325 |
. . . . 5
Disj |
136 | 77, 79, 86, 85, 90, 135 | esumrnmpt2 30130 |
. . . 4
Σ* Σ* |
137 | 11, 76, 136 | 3eqtr3rd 2665 |
. . 3
Σ* Σ* |
138 | | uniiun 4573 |
. . . . . . 7
|
139 | 28 | sselda 3603 |
. . . . . . . 8
|
140 | 40, 139 | elpwiuncl 29359 |
. . . . . . 7
|
141 | 138, 140 | syl5eqel 2705 |
. . . . . 6
|
142 | 141 | adantr 481 |
. . . . 5
|
143 | 19, 142 | ffvelrnd 6360 |
. . . 4
|
144 | | carsgsiga.2 |
. . . . . . . . . 10
Σ* |
145 | 144 | 3adant1r 1319 |
. . . . . . . . 9
Σ* |
146 | | fveq2 6191 |
. . . . . . . . . 10
|
147 | | nfcv 2764 |
. . . . . . . . . 10
|
148 | | nfcv 2764 |
. . . . . . . . . 10
|
149 | | nfcv 2764 |
. . . . . . . . . 10
|
150 | | nfcv 2764 |
. . . . . . . . . 10
|
151 | 146, 147,
148, 149, 150 | cbvesum 30104 |
. . . . . . . . 9
Σ*
Σ* |
152 | 145, 151 | syl6breq 4694 |
. . . . . . . 8
Σ* |
153 | | ffn 6045 |
. . . . . . . . . 10
|
154 | | fz1ssnn 12372 |
. . . . . . . . . . 11
|
155 | | fnssres 6004 |
. . . . . . . . . . 11
|
156 | 154, 155 | mpan2 707 |
. . . . . . . . . 10
|
157 | 8, 153, 156 | 3syl 18 |
. . . . . . . . 9
|
158 | | fzfi 12771 |
. . . . . . . . . 10
|
159 | | fnfi 8238 |
. . . . . . . . . 10
|
160 | 158, 159 | mpan2 707 |
. . . . . . . . 9
|
161 | | rnfi 8249 |
. . . . . . . . 9
|
162 | 157, 160,
161 | 3syl 18 |
. . . . . . . 8
|
163 | | resss 5422 |
. . . . . . . . . . 11
|
164 | | rnss 5354 |
. . . . . . . . . . 11
|
165 | 163, 164 | ax-mp 5 |
. . . . . . . . . 10
|
166 | 165 | a1i 11 |
. . . . . . . . 9
|
167 | 166, 53 | sstrd 3613 |
. . . . . . . 8
toCaraSiga |
168 | 166, 37 | sstrd 3613 |
. . . . . . . . 9
|
169 | | nfcv 2764 |
. . . . . . . . . . . . 13
|
170 | | nfcv 2764 |
. . . . . . . . . . . . 13
|
171 | | id 22 |
. . . . . . . . . . . . 13
|
172 | 169, 170,
171 | cbvdisj 4630 |
. . . . . . . . . . . 12
Disj
Disj |
173 | | disjun0 29408 |
. . . . . . . . . . . 12
Disj
Disj |
174 | 172, 173 | sylbi 207 |
. . . . . . . . . . 11
Disj
Disj |
175 | 121, 174 | syl 17 |
. . . . . . . . . 10
Disj
|
176 | 175 | adantr 481 |
. . . . . . . . 9
Disj |
177 | | disjss1 4626 |
. . . . . . . . 9
Disj Disj |
178 | 168, 176,
177 | sylc 65 |
. . . . . . . 8
Disj |
179 | | pwidg 4173 |
. . . . . . . . 9
|
180 | 17, 179 | syl 17 |
. . . . . . . 8
|
181 | 17, 19, 21, 152, 162, 167, 178, 180 | carsgclctunlem1 30379 |
. . . . . . 7
Σ* |
182 | 181 | adantr 481 |
. . . . . 6
Σ* |
183 | 168 | unissd 4462 |
. . . . . . . . . . 11
|
184 | | uniun 4456 |
. . . . . . . . . . . 12
|
185 | 2 | unisn 4451 |
. . . . . . . . . . . . 13
|
186 | 185 | uneq2i 3764 |
. . . . . . . . . . . 12
|
187 | | un0 3967 |
. . . . . . . . . . . 12
|
188 | 184, 186,
187 | 3eqtri 2648 |
. . . . . . . . . . 11
|
189 | 183, 188 | syl6sseq 3651 |
. . . . . . . . . 10
|
190 | 189 | adantr 481 |
. . . . . . . . 9
|
191 | | uniss 4458 |
. . . . . . . . . . . 12
|
192 | | unipw 4918 |
. . . . . . . . . . . 12
|
193 | 191, 192 | syl6sseq 3651 |
. . . . . . . . . . 11
|
194 | 28, 193 | syl 17 |
. . . . . . . . . 10
|
195 | 194 | ad2antrr 762 |
. . . . . . . . 9
|
196 | 190, 195 | sstrd 3613 |
. . . . . . . 8
|
197 | | sseqin2 3817 |
. . . . . . . 8
|
198 | 196, 197 | sylib 208 |
. . . . . . 7
|
199 | 198 | fveq2d 6195 |
. . . . . 6
|
200 | | nfv 1843 |
. . . . . . . 8
|
201 | 168 | adantr 481 |
. . . . . . . . . . . . . 14
|
202 | 28 | ad2antrr 762 |
. . . . . . . . . . . . . . 15
|
203 | 30 | a1i 11 |
. . . . . . . . . . . . . . . 16
|
204 | 203 | snssd 4340 |
. . . . . . . . . . . . . . 15
|
205 | 202, 204 | unssd 3789 |
. . . . . . . . . . . . . 14
|
206 | 201, 205 | sstrd 3613 |
. . . . . . . . . . . . 13
|
207 | 206 | sselda 3603 |
. . . . . . . . . . . 12
|
208 | 207 | elpwid 4170 |
. . . . . . . . . . 11
|
209 | | sseqin2 3817 |
. . . . . . . . . . 11
|
210 | 208, 209 | sylib 208 |
. . . . . . . . . 10
|
211 | 210 | fveq2d 6195 |
. . . . . . . . 9
|
212 | 211 | ralrimiva 2966 |
. . . . . . . 8
|
213 | 200, 212 | esumeq2d 30099 |
. . . . . . 7
Σ* Σ* |
214 | 9 | reseq1d 5395 |
. . . . . . . . . . . 12
|
215 | 214 | adantr 481 |
. . . . . . . . . . 11
|
216 | | resmpt 5449 |
. . . . . . . . . . . 12
|
217 | 154, 216 | ax-mp 5 |
. . . . . . . . . . 11
|
218 | 215, 217 | syl6eq 2672 |
. . . . . . . . . 10
|
219 | 218 | eqcomd 2628 |
. . . . . . . . 9
|
220 | 219 | rneqd 5353 |
. . . . . . . 8
|
221 | 200, 220 | esumeq1d 30097 |
. . . . . . 7
Σ* Σ* |
222 | 158 | a1i 11 |
. . . . . . . 8
|
223 | 19 | ad2antrr 762 |
. . . . . . . . 9
|
224 | 154 | a1i 11 |
. . . . . . . . . . 11
|
225 | 224 | sselda 3603 |
. . . . . . . . . 10
|
226 | 85 | adantlr 751 |
. . . . . . . . . 10
|
227 | 225, 226 | syldan 487 |
. . . . . . . . 9
|
228 | 223, 227 | ffvelrnd 6360 |
. . . . . . . 8
|
229 | | simpr 477 |
. . . . . . . . . 10
|
230 | 229 | fveq2d 6195 |
. . . . . . . . 9
|
231 | 21 | ad3antrrr 766 |
. . . . . . . . 9
|
232 | 230, 231 | eqtrd 2656 |
. . . . . . . 8
|
233 | | disjss1 4626 |
. . . . . . . . . . 11
Disj Disj |
234 | 154, 233 | ax-mp 5 |
. . . . . . . . . 10
Disj Disj |
235 | 135, 234 | syl 17 |
. . . . . . . . 9
Disj |
236 | 235 | adantr 481 |
. . . . . . . 8
Disj |
237 | 77, 222, 228, 227, 232, 236 | esumrnmpt2 30130 |
. . . . . . 7
Σ* Σ* |
238 | 213, 221,
237 | 3eqtr2d 2662 |
. . . . . 6
Σ* Σ* |
239 | 182, 199,
238 | 3eqtr3d 2664 |
. . . . 5
Σ* |
240 | | carsggect.4 |
. . . . . . . 8
|
241 | 240 | 3adant1r 1319 |
. . . . . . 7
|
242 | 17, 19, 189, 142, 241 | carsgmon 30376 |
. . . . . 6
|
243 | 242 | adantr 481 |
. . . . 5
|
244 | 239, 243 | eqbrtrrd 4677 |
. . . 4
Σ*
|
245 | 143, 86, 244 | esumgect 30152 |
. . 3
Σ* |
246 | 137, 245 | eqbrtrrd 4677 |
. 2
Σ*
|
247 | 6, 246 | exlimddv 1863 |
1
Σ* |