Step | Hyp | Ref
| Expression |
1 | | iunin2 4584 |
. . . . 5
|
2 | 1 | fveq2i 6194 |
. . . 4
|
3 | | iccssxr 12256 |
. . . . 5
|
4 | | carsgval.2 |
. . . . . 6
|
5 | | nnex 11026 |
. . . . . . . 8
|
6 | 5 | a1i 11 |
. . . . . . 7
|
7 | | carsgclctunlem2.3 |
. . . . . . . . 9
|
8 | 7 | adantr 481 |
. . . . . . . 8
|
9 | 8 | elpwincl1 29357 |
. . . . . . 7
|
10 | 6, 9 | elpwiuncl 29359 |
. . . . . 6
|
11 | 4, 10 | ffvelrnd 6360 |
. . . . 5
|
12 | 3, 11 | sseldi 3601 |
. . . 4
|
13 | 2, 12 | syl5eqelr 2706 |
. . 3
|
14 | 4, 7 | ffvelrnd 6360 |
. . . . 5
|
15 | 3, 14 | sseldi 3601 |
. . . 4
|
16 | 7 | elpwdifcl 29358 |
. . . . . . 7
|
17 | 4, 16 | ffvelrnd 6360 |
. . . . . 6
|
18 | 3, 17 | sseldi 3601 |
. . . . 5
|
19 | 18 | xnegcld 12130 |
. . . 4
|
20 | 15, 19 | xaddcld 12131 |
. . 3
|
21 | 4 | adantr 481 |
. . . . . . . . 9
|
22 | 21, 9 | ffvelrnd 6360 |
. . . . . . . 8
|
23 | 22 | ralrimiva 2966 |
. . . . . . 7
|
24 | | nfcv 2764 |
. . . . . . . 8
|
25 | 24 | esumcl 30092 |
. . . . . . 7
Σ* |
26 | 6, 23, 25 | syl2anc 693 |
. . . . . 6
Σ* |
27 | 3, 26 | sseldi 3601 |
. . . . 5
Σ* |
28 | 9 | ralrimiva 2966 |
. . . . . . . . 9
|
29 | | dfiun3g 5378 |
. . . . . . . . 9
|
30 | 28, 29 | syl 17 |
. . . . . . . 8
|
31 | 30 | fveq2d 6195 |
. . . . . . 7
|
32 | | nnct 12780 |
. . . . . . . . . 10
|
33 | | mptct 9360 |
. . . . . . . . . 10
|
34 | | rnct 9347 |
. . . . . . . . . 10
|
35 | 32, 33, 34 | mp2b 10 |
. . . . . . . . 9
|
36 | 35 | a1i 11 |
. . . . . . . 8
|
37 | | eqid 2622 |
. . . . . . . . . 10
|
38 | 37 | rnmptss 6392 |
. . . . . . . . 9
|
39 | 28, 38 | syl 17 |
. . . . . . . 8
|
40 | | mptexg 6484 |
. . . . . . . . . 10
|
41 | | rnexg 7098 |
. . . . . . . . . 10
|
42 | 5, 40, 41 | mp2b 10 |
. . . . . . . . 9
|
43 | | breq1 4656 |
. . . . . . . . . . . 12
|
44 | | sseq1 3626 |
. . . . . . . . . . . 12
|
45 | 43, 44 | 3anbi23d 1402 |
. . . . . . . . . . 11
|
46 | | unieq 4444 |
. . . . . . . . . . . . 13
|
47 | 46 | fveq2d 6195 |
. . . . . . . . . . . 12
|
48 | | esumeq1 30096 |
. . . . . . . . . . . 12
Σ* Σ* |
49 | 47, 48 | breq12d 4666 |
. . . . . . . . . . 11
Σ*
Σ*
|
50 | 45, 49 | imbi12d 334 |
. . . . . . . . . 10
Σ*
Σ*
|
51 | | carsgsiga.2 |
. . . . . . . . . 10
Σ* |
52 | 50, 51 | vtoclg 3266 |
. . . . . . . . 9
Σ*
|
53 | 42, 52 | ax-mp 5 |
. . . . . . . 8
Σ*
|
54 | 36, 39, 53 | mpd3an23 1426 |
. . . . . . 7
Σ*
|
55 | 31, 54 | eqbrtrd 4675 |
. . . . . 6
Σ*
|
56 | | fveq2 6191 |
. . . . . . 7
|
57 | | simpr 477 |
. . . . . . . . 9
|
58 | 57 | fveq2d 6195 |
. . . . . . . 8
|
59 | | carsgsiga.1 |
. . . . . . . . 9
|
60 | 59 | ad2antrr 762 |
. . . . . . . 8
|
61 | 58, 60 | eqtrd 2656 |
. . . . . . 7
|
62 | | carsgclctunlem2.1 |
. . . . . . . . 9
Disj
|
63 | | disjin 29399 |
. . . . . . . . 9
Disj Disj |
64 | 62, 63 | syl 17 |
. . . . . . . 8
Disj
|
65 | | incom 3805 |
. . . . . . . . . 10
|
66 | 65 | rgenw 2924 |
. . . . . . . . 9
|
67 | | disjeq2 4624 |
. . . . . . . . 9
Disj Disj |
68 | 66, 67 | ax-mp 5 |
. . . . . . . 8
Disj Disj |
69 | 64, 68 | sylib 208 |
. . . . . . 7
Disj
|
70 | 56, 6, 22, 9, 61, 69 | esumrnmpt2 30130 |
. . . . . 6
Σ*
Σ* |
71 | 55, 70 | breqtrd 4679 |
. . . . 5
Σ* |
72 | | carsgval.1 |
. . . . . . . 8
|
73 | | difssd 3738 |
. . . . . . . 8
|
74 | | carsgsiga.3 |
. . . . . . . 8
|
75 | 72, 4, 73, 7, 74 | carsgmon 30376 |
. . . . . . 7
|
76 | 14, 17, 75 | xrge0subcld 29528 |
. . . . . 6
|
77 | 4 | adantr 481 |
. . . . . . . . . . . 12
|
78 | 7 | adantr 481 |
. . . . . . . . . . . . 13
|
79 | 78 | elpwincl1 29357 |
. . . . . . . . . . . 12
|
80 | 77, 79 | ffvelrnd 6360 |
. . . . . . . . . . 11
|
81 | 3, 80 | sseldi 3601 |
. . . . . . . . . 10
|
82 | | xrge0neqmnf 12276 |
. . . . . . . . . . 11
|
83 | 80, 82 | syl 17 |
. . . . . . . . . 10
|
84 | 78 | elpwdifcl 29358 |
. . . . . . . . . . . 12
|
85 | 77, 84 | ffvelrnd 6360 |
. . . . . . . . . . 11
|
86 | 3, 85 | sseldi 3601 |
. . . . . . . . . 10
|
87 | | xrge0neqmnf 12276 |
. . . . . . . . . . 11
|
88 | 85, 87 | syl 17 |
. . . . . . . . . 10
|
89 | 86 | xnegcld 12130 |
. . . . . . . . . 10
|
90 | | xnegneg 12045 |
. . . . . . . . . . . . . . . . 17
|
91 | 86, 90 | syl 17 |
. . . . . . . . . . . . . . . 16
|
92 | 91 | adantr 481 |
. . . . . . . . . . . . . . 15
|
93 | | xnegeq 12038 |
. . . . . . . . . . . . . . . . 17
|
94 | 93 | adantl 482 |
. . . . . . . . . . . . . . . 16
|
95 | | xnegmnf 12041 |
. . . . . . . . . . . . . . . 16
|
96 | 94, 95 | syl6eq 2672 |
. . . . . . . . . . . . . . 15
|
97 | 92, 96 | eqtr3d 2658 |
. . . . . . . . . . . . . 14
|
98 | 97 | oveq2d 6666 |
. . . . . . . . . . . . 13
|
99 | | simpll 790 |
. . . . . . . . . . . . . . . . . . . . 21
|
100 | | fz1ssnn 12372 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
101 | 100 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . 22
|
102 | 101 | sselda 3603 |
. . . . . . . . . . . . . . . . . . . . 21
|
103 | | carsgclctunlem2.2 |
. . . . . . . . . . . . . . . . . . . . 21
toCaraSiga |
104 | 99, 102, 103 | syl2anc 693 |
. . . . . . . . . . . . . . . . . . . 20
toCaraSiga |
105 | 104 | ralrimiva 2966 |
. . . . . . . . . . . . . . . . . . 19
toCaraSiga |
106 | | dfiun3g 5378 |
. . . . . . . . . . . . . . . . . . 19
toCaraSiga
|
107 | 105, 106 | syl 17 |
. . . . . . . . . . . . . . . . . 18
|
108 | 72 | adantr 481 |
. . . . . . . . . . . . . . . . . . 19
|
109 | 59 | adantr 481 |
. . . . . . . . . . . . . . . . . . 19
|
110 | 51 | 3adant1r 1319 |
. . . . . . . . . . . . . . . . . . 19
Σ* |
111 | | fzfi 12771 |
. . . . . . . . . . . . . . . . . . . . 21
|
112 | | mptfi 8265 |
. . . . . . . . . . . . . . . . . . . . 21
|
113 | | rnfi 8249 |
. . . . . . . . . . . . . . . . . . . . 21
|
114 | 111, 112,
113 | mp2b 10 |
. . . . . . . . . . . . . . . . . . . 20
|
115 | 114 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
|
116 | | eqid 2622 |
. . . . . . . . . . . . . . . . . . . . 21
|
117 | 116 | rnmptss 6392 |
. . . . . . . . . . . . . . . . . . . 20
toCaraSiga toCaraSiga |
118 | 105, 117 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
toCaraSiga |
119 | 108, 77, 109, 110, 115, 118 | fiunelcarsg 30378 |
. . . . . . . . . . . . . . . . . 18
toCaraSiga |
120 | 107, 119 | eqeltrd 2701 |
. . . . . . . . . . . . . . . . 17
toCaraSiga |
121 | 108, 77 | elcarsg 30367 |
. . . . . . . . . . . . . . . . 17
toCaraSiga
|
122 | 120, 121 | mpbid 222 |
. . . . . . . . . . . . . . . 16
|
123 | 122 | simprd 479 |
. . . . . . . . . . . . . . 15
|
124 | | ineq1 3807 |
. . . . . . . . . . . . . . . . . . 19
|
125 | 124 | fveq2d 6195 |
. . . . . . . . . . . . . . . . . 18
|
126 | | difeq1 3721 |
. . . . . . . . . . . . . . . . . . 19
|
127 | 126 | fveq2d 6195 |
. . . . . . . . . . . . . . . . . 18
|
128 | 125, 127 | oveq12d 6668 |
. . . . . . . . . . . . . . . . 17
|
129 | | fveq2 6191 |
. . . . . . . . . . . . . . . . 17
|
130 | 128, 129 | eqeq12d 2637 |
. . . . . . . . . . . . . . . 16
|
131 | 130 | rspcv 3305 |
. . . . . . . . . . . . . . 15
|
132 | 78, 123, 131 | sylc 65 |
. . . . . . . . . . . . . 14
|
133 | 132 | adantr 481 |
. . . . . . . . . . . . 13
|
134 | | xaddpnf1 12057 |
. . . . . . . . . . . . . . 15
|
135 | 81, 83, 134 | syl2anc 693 |
. . . . . . . . . . . . . 14
|
136 | 135 | adantr 481 |
. . . . . . . . . . . . 13
|
137 | 98, 133, 136 | 3eqtr3d 2664 |
. . . . . . . . . . . 12
|
138 | | carsgclctunlem2.4 |
. . . . . . . . . . . . . 14
|
139 | 138 | ad2antrr 762 |
. . . . . . . . . . . . 13
|
140 | 139 | neneqd 2799 |
. . . . . . . . . . . 12
|
141 | 137, 140 | pm2.65da 600 |
. . . . . . . . . . 11
|
142 | 141 | neqned 2801 |
. . . . . . . . . 10
|
143 | | xaddass 12079 |
. . . . . . . . . 10
|
144 | 81, 83, 86, 88, 89, 142, 143 | syl222anc 1342 |
. . . . . . . . 9
|
145 | | xnegid 12069 |
. . . . . . . . . . 11
|
146 | 86, 145 | syl 17 |
. . . . . . . . . 10
|
147 | 146 | oveq2d 6666 |
. . . . . . . . 9
|
148 | | xaddid1 12072 |
. . . . . . . . . 10
|
149 | 81, 148 | syl 17 |
. . . . . . . . 9
|
150 | 144, 147,
149 | 3eqtrd 2660 |
. . . . . . . 8
|
151 | 132 | oveq1d 6665 |
. . . . . . . 8
|
152 | 107 | ineq2d 3814 |
. . . . . . . . . 10
|
153 | 152 | fveq2d 6195 |
. . . . . . . . 9
|
154 | | mptss 5454 |
. . . . . . . . . . . . 13
|
155 | | rnss 5354 |
. . . . . . . . . . . . 13
|
156 | 100, 154,
155 | mp2b 10 |
. . . . . . . . . . . 12
|
157 | 156 | a1i 11 |
. . . . . . . . . . 11
|
158 | | disjrnmpt 29398 |
. . . . . . . . . . . . 13
Disj Disj |
159 | 62, 158 | syl 17 |
. . . . . . . . . . . 12
Disj
|
160 | 159 | adantr 481 |
. . . . . . . . . . 11
Disj
|
161 | | disjss1 4626 |
. . . . . . . . . . 11
Disj
Disj |
162 | 157, 160,
161 | sylc 65 |
. . . . . . . . . 10
Disj
|
163 | 108, 77, 109, 110, 115, 118, 162, 78 | carsgclctunlem1 30379 |
. . . . . . . . 9
Σ* |
164 | | ineq2 3808 |
. . . . . . . . . . 11
|
165 | 164 | fveq2d 6195 |
. . . . . . . . . 10
|
166 | 111 | elexi 3213 |
. . . . . . . . . . 11
|
167 | 166 | a1i 11 |
. . . . . . . . . 10
|
168 | 99, 102, 22 | syl2anc 693 |
. . . . . . . . . 10
|
169 | | inss2 3834 |
. . . . . . . . . . . . . . 15
|
170 | | sseq2 3627 |
. . . . . . . . . . . . . . 15
|
171 | 169, 170 | mpbii 223 |
. . . . . . . . . . . . . 14
|
172 | | ss0 3974 |
. . . . . . . . . . . . . 14
|
173 | 171, 172 | syl 17 |
. . . . . . . . . . . . 13
|
174 | 173 | adantl 482 |
. . . . . . . . . . . 12
|
175 | 174 | fveq2d 6195 |
. . . . . . . . . . 11
|
176 | 109 | ad2antrr 762 |
. . . . . . . . . . 11
|
177 | 175, 176 | eqtrd 2656 |
. . . . . . . . . 10
|
178 | 62 | adantr 481 |
. . . . . . . . . . 11
Disj
|
179 | | disjss1 4626 |
. . . . . . . . . . 11
Disj Disj |
180 | 101, 178,
179 | sylc 65 |
. . . . . . . . . 10
Disj
|
181 | 165, 167,
168, 104, 177, 180 | esumrnmpt2 30130 |
. . . . . . . . 9
Σ* Σ* |
182 | 153, 163,
181 | 3eqtrd 2660 |
. . . . . . . 8
Σ*
|
183 | 150, 151,
182 | 3eqtr3rd 2665 |
. . . . . . 7
Σ* |
184 | 17 | adantr 481 |
. . . . . . . . . 10
|
185 | 3, 184 | sseldi 3601 |
. . . . . . . . 9
|
186 | 185 | xnegcld 12130 |
. . . . . . . 8
|
187 | 15 | adantr 481 |
. . . . . . . 8
|
188 | | iunss1 4532 |
. . . . . . . . . . . 12
|
189 | 100, 188 | mp1i 13 |
. . . . . . . . . . 11
|
190 | 189 | sscond 3747 |
. . . . . . . . . 10
|
191 | 74 | 3adant1r 1319 |
. . . . . . . . . 10
|
192 | 108, 77, 190, 84, 191 | carsgmon 30376 |
. . . . . . . . 9
|
193 | | xleneg 12049 |
. . . . . . . . . 10
|
194 | 193 | biimpa 501 |
. . . . . . . . 9
|
195 | 185, 86, 192, 194 | syl21anc 1325 |
. . . . . . . 8
|
196 | | xleadd2a 12084 |
. . . . . . . 8
|
197 | 89, 186, 187, 195, 196 | syl31anc 1329 |
. . . . . . 7
|
198 | 183, 197 | eqbrtrd 4675 |
. . . . . 6
Σ* |
199 | 76, 22, 198 | esumgect 30152 |
. . . . 5
Σ*
|
200 | 12, 27, 20, 71, 199 | xrletrd 11993 |
. . . 4
|
201 | 2, 200 | syl5eqbrr 4689 |
. . 3
|
202 | | xleadd1a 12083 |
. . 3
|
203 | 13, 20, 18, 201, 202 | syl31anc 1329 |
. 2
|
204 | | xrge0npcan 29694 |
. . 3
|
205 | 14, 17, 75, 204 | syl3anc 1326 |
. 2
|
206 | 203, 205 | breqtrd 4679 |
1
|