Metamath Proof Explorer


Theorem carsgclctunlem2

Description: Lemma for carsgclctun . (Contributed by Thierry Arnoux, 25-May-2020)

Ref Expression
Hypotheses carsgval.1 φ O V
carsgval.2 φ M : 𝒫 O 0 +∞
carsgsiga.1 φ M = 0
carsgsiga.2 φ x ω x 𝒫 O M x * y x M y
carsgsiga.3 φ x y y 𝒫 O M x M y
carsgclctunlem2.1 φ Disj k A
carsgclctunlem2.2 φ k A toCaraSiga M
carsgclctunlem2.3 φ E 𝒫 O
carsgclctunlem2.4 φ M E +∞
Assertion carsgclctunlem2 φ M E k A + 𝑒 M E k A M E

Proof

Step Hyp Ref Expression
1 carsgval.1 φ O V
2 carsgval.2 φ M : 𝒫 O 0 +∞
3 carsgsiga.1 φ M = 0
4 carsgsiga.2 φ x ω x 𝒫 O M x * y x M y
5 carsgsiga.3 φ x y y 𝒫 O M x M y
6 carsgclctunlem2.1 φ Disj k A
7 carsgclctunlem2.2 φ k A toCaraSiga M
8 carsgclctunlem2.3 φ E 𝒫 O
9 carsgclctunlem2.4 φ M E +∞
10 iunin2 k E A = E k A
11 10 fveq2i M k E A = M E k A
12 iccssxr 0 +∞ *
13 nnex V
14 13 a1i φ V
15 8 adantr φ k E 𝒫 O
16 15 elpwincl1 φ k E A 𝒫 O
17 14 16 elpwiuncl φ k E A 𝒫 O
18 2 17 ffvelrnd φ M k E A 0 +∞
19 12 18 sseldi φ M k E A *
20 11 19 eqeltrrid φ M E k A *
21 2 8 ffvelrnd φ M E 0 +∞
22 12 21 sseldi φ M E *
23 8 elpwdifcl φ E k A 𝒫 O
24 2 23 ffvelrnd φ M E k A 0 +∞
25 12 24 sseldi φ M E k A *
26 25 xnegcld φ M E k A *
27 22 26 xaddcld φ M E + 𝑒 M E k A *
28 2 adantr φ k M : 𝒫 O 0 +∞
29 28 16 ffvelrnd φ k M E A 0 +∞
30 29 ralrimiva φ k M E A 0 +∞
31 nfcv _ k
32 31 esumcl V k M E A 0 +∞ * k M E A 0 +∞
33 14 30 32 syl2anc φ * k M E A 0 +∞
34 12 33 sseldi φ * k M E A *
35 16 ralrimiva φ k E A 𝒫 O
36 dfiun3g k E A 𝒫 O k E A = ran k E A
37 35 36 syl φ k E A = ran k E A
38 37 fveq2d φ M k E A = M ran k E A
39 nnct ω
40 mptct ω k E A ω
41 rnct k E A ω ran k E A ω
42 39 40 41 mp2b ran k E A ω
43 42 a1i φ ran k E A ω
44 eqid k E A = k E A
45 44 rnmptss k E A 𝒫 O ran k E A 𝒫 O
46 35 45 syl φ ran k E A 𝒫 O
47 mptexg V k E A V
48 rnexg k E A V ran k E A V
49 13 47 48 mp2b ran k E A V
50 breq1 x = ran k E A x ω ran k E A ω
51 sseq1 x = ran k E A x 𝒫 O ran k E A 𝒫 O
52 50 51 3anbi23d x = ran k E A φ x ω x 𝒫 O φ ran k E A ω ran k E A 𝒫 O
53 unieq x = ran k E A x = ran k E A
54 53 fveq2d x = ran k E A M x = M ran k E A
55 esumeq1 x = ran k E A * y x M y = * y ran k E A M y
56 54 55 breq12d x = ran k E A M x * y x M y M ran k E A * y ran k E A M y
57 52 56 imbi12d x = ran k E A φ x ω x 𝒫 O M x * y x M y φ ran k E A ω ran k E A 𝒫 O M ran k E A * y ran k E A M y
58 57 4 vtoclg ran k E A V φ ran k E A ω ran k E A 𝒫 O M ran k E A * y ran k E A M y
59 49 58 ax-mp φ ran k E A ω ran k E A 𝒫 O M ran k E A * y ran k E A M y
60 43 46 59 mpd3an23 φ M ran k E A * y ran k E A M y
61 38 60 eqbrtrd φ M k E A * y ran k E A M y
62 fveq2 y = E A M y = M E A
63 simpr φ k E A = E A =
64 63 fveq2d φ k E A = M E A = M
65 3 ad2antrr φ k E A = M = 0
66 64 65 eqtrd φ k E A = M E A = 0
67 disjin Disj k A Disj k A E
68 6 67 syl φ Disj k A E
69 incom A E = E A
70 69 rgenw k A E = E A
71 disjeq2 k A E = E A Disj k A E Disj k E A
72 70 71 ax-mp Disj k A E Disj k E A
73 68 72 sylib φ Disj k E A
74 62 14 29 16 66 73 esumrnmpt2 φ * y ran k E A M y = * k M E A
75 61 74 breqtrd φ M k E A * k M E A
76 difssd φ E k A E
77 1 2 76 8 5 carsgmon φ M E k A M E
78 21 24 77 xrge0subcld φ M E + 𝑒 M E k A 0 +∞
79 2 adantr φ n M : 𝒫 O 0 +∞
80 8 adantr φ n E 𝒫 O
81 80 elpwincl1 φ n E k = 1 n A 𝒫 O
82 79 81 ffvelrnd φ n M E k = 1 n A 0 +∞
83 12 82 sseldi φ n M E k = 1 n A *
84 xrge0neqmnf M E k = 1 n A 0 +∞ M E k = 1 n A −∞
85 82 84 syl φ n M E k = 1 n A −∞
86 80 elpwdifcl φ n E k = 1 n A 𝒫 O
87 79 86 ffvelrnd φ n M E k = 1 n A 0 +∞
88 12 87 sseldi φ n M E k = 1 n A *
89 xrge0neqmnf M E k = 1 n A 0 +∞ M E k = 1 n A −∞
90 87 89 syl φ n M E k = 1 n A −∞
91 88 xnegcld φ n M E k = 1 n A *
92 xnegneg M E k = 1 n A * M E k = 1 n A = M E k = 1 n A
93 88 92 syl φ n M E k = 1 n A = M E k = 1 n A
94 93 adantr φ n M E k = 1 n A = −∞ M E k = 1 n A = M E k = 1 n A
95 xnegeq M E k = 1 n A = −∞ M E k = 1 n A = −∞
96 95 adantl φ n M E k = 1 n A = −∞ M E k = 1 n A = −∞
97 xnegmnf −∞ = +∞
98 96 97 syl6eq φ n M E k = 1 n A = −∞ M E k = 1 n A = +∞
99 94 98 eqtr3d φ n M E k = 1 n A = −∞ M E k = 1 n A = +∞
100 99 oveq2d φ n M E k = 1 n A = −∞ M E k = 1 n A + 𝑒 M E k = 1 n A = M E k = 1 n A + 𝑒 +∞
101 simpll φ n k 1 n φ
102 fz1ssnn 1 n
103 102 a1i φ n 1 n
104 103 sselda φ n k 1 n k
105 101 104 7 syl2anc φ n k 1 n A toCaraSiga M
106 105 ralrimiva φ n k 1 n A toCaraSiga M
107 dfiun3g k 1 n A toCaraSiga M k = 1 n A = ran k 1 n A
108 106 107 syl φ n k = 1 n A = ran k 1 n A
109 1 adantr φ n O V
110 3 adantr φ n M = 0
111 4 3adant1r φ n x ω x 𝒫 O M x * y x M y
112 fzfi 1 n Fin
113 mptfi 1 n Fin k 1 n A Fin
114 rnfi k 1 n A Fin ran k 1 n A Fin
115 112 113 114 mp2b ran k 1 n A Fin
116 115 a1i φ n ran k 1 n A Fin
117 eqid k 1 n A = k 1 n A
118 117 rnmptss k 1 n A toCaraSiga M ran k 1 n A toCaraSiga M
119 106 118 syl φ n ran k 1 n A toCaraSiga M
120 109 79 110 111 116 119 fiunelcarsg φ n ran k 1 n A toCaraSiga M
121 108 120 eqeltrd φ n k = 1 n A toCaraSiga M
122 109 79 elcarsg φ n k = 1 n A toCaraSiga M k = 1 n A O e 𝒫 O M e k = 1 n A + 𝑒 M e k = 1 n A = M e
123 121 122 mpbid φ n k = 1 n A O e 𝒫 O M e k = 1 n A + 𝑒 M e k = 1 n A = M e
124 123 simprd φ n e 𝒫 O M e k = 1 n A + 𝑒 M e k = 1 n A = M e
125 ineq1 e = E e k = 1 n A = E k = 1 n A
126 125 fveq2d e = E M e k = 1 n A = M E k = 1 n A
127 difeq1 e = E e k = 1 n A = E k = 1 n A
128 127 fveq2d e = E M e k = 1 n A = M E k = 1 n A
129 126 128 oveq12d e = E M e k = 1 n A + 𝑒 M e k = 1 n A = M E k = 1 n A + 𝑒 M E k = 1 n A
130 fveq2 e = E M e = M E
131 129 130 eqeq12d e = E M e k = 1 n A + 𝑒 M e k = 1 n A = M e M E k = 1 n A + 𝑒 M E k = 1 n A = M E
132 131 rspcv E 𝒫 O e 𝒫 O M e k = 1 n A + 𝑒 M e k = 1 n A = M e M E k = 1 n A + 𝑒 M E k = 1 n A = M E
133 80 124 132 sylc φ n M E k = 1 n A + 𝑒 M E k = 1 n A = M E
134 133 adantr φ n M E k = 1 n A = −∞ M E k = 1 n A + 𝑒 M E k = 1 n A = M E
135 xaddpnf1 M E k = 1 n A * M E k = 1 n A −∞ M E k = 1 n A + 𝑒 +∞ = +∞
136 83 85 135 syl2anc φ n M E k = 1 n A + 𝑒 +∞ = +∞
137 136 adantr φ n M E k = 1 n A = −∞ M E k = 1 n A + 𝑒 +∞ = +∞
138 100 134 137 3eqtr3d φ n M E k = 1 n A = −∞ M E = +∞
139 9 ad2antrr φ n M E k = 1 n A = −∞ M E +∞
140 139 neneqd φ n M E k = 1 n A = −∞ ¬ M E = +∞
141 138 140 pm2.65da φ n ¬ M E k = 1 n A = −∞
142 141 neqned φ n M E k = 1 n A −∞
143 xaddass M E k = 1 n A * M E k = 1 n A −∞ M E k = 1 n A * M E k = 1 n A −∞ M E k = 1 n A * M E k = 1 n A −∞ M E k = 1 n A + 𝑒 M E k = 1 n A + 𝑒 M E k = 1 n A = M E k = 1 n A + 𝑒 M E k = 1 n A + 𝑒 M E k = 1 n A
144 83 85 88 90 91 142 143 syl222anc φ n M E k = 1 n A + 𝑒 M E k = 1 n A + 𝑒 M E k = 1 n A = M E k = 1 n A + 𝑒 M E k = 1 n A + 𝑒 M E k = 1 n A
145 xnegid M E k = 1 n A * M E k = 1 n A + 𝑒 M E k = 1 n A = 0
146 88 145 syl φ n M E k = 1 n A + 𝑒 M E k = 1 n A = 0
147 146 oveq2d φ n M E k = 1 n A + 𝑒 M E k = 1 n A + 𝑒 M E k = 1 n A = M E k = 1 n A + 𝑒 0
148 xaddid1 M E k = 1 n A * M E k = 1 n A + 𝑒 0 = M E k = 1 n A
149 83 148 syl φ n M E k = 1 n A + 𝑒 0 = M E k = 1 n A
150 144 147 149 3eqtrd φ n M E k = 1 n A + 𝑒 M E k = 1 n A + 𝑒 M E k = 1 n A = M E k = 1 n A
151 133 oveq1d φ n M E k = 1 n A + 𝑒 M E k = 1 n A + 𝑒 M E k = 1 n A = M E + 𝑒 M E k = 1 n A
152 108 ineq2d φ n E k = 1 n A = E ran k 1 n A
153 152 fveq2d φ n M E k = 1 n A = M E ran k 1 n A
154 mptss 1 n k 1 n A k A
155 rnss k 1 n A k A ran k 1 n A ran k A
156 102 154 155 mp2b ran k 1 n A ran k A
157 156 a1i φ n ran k 1 n A ran k A
158 disjrnmpt Disj k A Disj y ran k A y
159 6 158 syl φ Disj y ran k A y
160 159 adantr φ n Disj y ran k A y
161 disjss1 ran k 1 n A ran k A Disj y ran k A y Disj y ran k 1 n A y
162 157 160 161 sylc φ n Disj y ran k 1 n A y
163 109 79 110 111 116 119 162 80 carsgclctunlem1 φ n M E ran k 1 n A = * y ran k 1 n A M E y
164 ineq2 y = A E y = E A
165 164 fveq2d y = A M E y = M E A
166 112 elexi 1 n V
167 166 a1i φ n 1 n V
168 101 104 29 syl2anc φ n k 1 n M E A 0 +∞
169 inss2 E A A
170 sseq2 A = E A A E A
171 169 170 mpbii A = E A
172 ss0 E A E A =
173 171 172 syl A = E A =
174 173 adantl φ n k 1 n A = E A =
175 174 fveq2d φ n k 1 n A = M E A = M
176 110 ad2antrr φ n k 1 n A = M = 0
177 175 176 eqtrd φ n k 1 n A = M E A = 0
178 6 adantr φ n Disj k A
179 disjss1 1 n Disj k A Disj k = 1 n A
180 103 178 179 sylc φ n Disj k = 1 n A
181 165 167 168 105 177 180 esumrnmpt2 φ n * y ran k 1 n A M E y = * k = 1 n M E A
182 153 163 181 3eqtrd φ n M E k = 1 n A = * k = 1 n M E A
183 150 151 182 3eqtr3rd φ n * k = 1 n M E A = M E + 𝑒 M E k = 1 n A
184 24 adantr φ n M E k A 0 +∞
185 12 184 sseldi φ n M E k A *
186 185 xnegcld φ n M E k A *
187 22 adantr φ n M E *
188 iunss1 1 n k = 1 n A k A
189 102 188 mp1i φ n k = 1 n A k A
190 189 sscond φ n E k A E k = 1 n A
191 5 3adant1r φ n x y y 𝒫 O M x M y
192 109 79 190 86 191 carsgmon φ n M E k A M E k = 1 n A
193 xleneg M E k A * M E k = 1 n A * M E k A M E k = 1 n A M E k = 1 n A M E k A
194 193 biimpa M E k A * M E k = 1 n A * M E k A M E k = 1 n A M E k = 1 n A M E k A
195 185 88 192 194 syl21anc φ n M E k = 1 n A M E k A
196 xleadd2a M E k = 1 n A * M E k A * M E * M E k = 1 n A M E k A M E + 𝑒 M E k = 1 n A M E + 𝑒 M E k A
197 91 186 187 195 196 syl31anc φ n M E + 𝑒 M E k = 1 n A M E + 𝑒 M E k A
198 183 197 eqbrtrd φ n * k = 1 n M E A M E + 𝑒 M E k A
199 78 29 198 esumgect φ * k M E A M E + 𝑒 M E k A
200 19 34 27 75 199 xrletrd φ M k E A M E + 𝑒 M E k A
201 11 200 eqbrtrrid φ M E k A M E + 𝑒 M E k A
202 xleadd1a M E k A * M E + 𝑒 M E k A * M E k A * M E k A M E + 𝑒 M E k A M E k A + 𝑒 M E k A M E + 𝑒 M E k A + 𝑒 M E k A
203 20 27 25 201 202 syl31anc φ M E k A + 𝑒 M E k A M E + 𝑒 M E k A + 𝑒 M E k A
204 xrge0npcan M E 0 +∞ M E k A 0 +∞ M E k A M E M E + 𝑒 M E k A + 𝑒 M E k A = M E
205 21 24 77 204 syl3anc φ M E + 𝑒 M E k A + 𝑒 M E k A = M E
206 203 205 breqtrd φ M E k A + 𝑒 M E k A M E