Mathbox for Mario Carneiro < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  cvmliftlem10 Structured version   Visualization version   Unicode version

Theorem cvmliftlem10 30089
 Description: Lemma for cvmlift 30094. The function is going to be our complete lifted path, formed by unioning together all the functions (each of which is defined on one segment of the interval). Here we prove by induction that is a continuous function and a lift of by applying cvmliftlem6 30085, cvmliftlem7 30086 (to show it is a function and a lift), cvmliftlem8 30087 (to show it is continuous), and cvmliftlem9 30088 (to show that different functions agree on the intersection of their domains, so that the pasting lemma paste 20387 gives that is well-defined and continuous). (Contributed by Mario Carneiro, 14-Feb-2015.)
Hypotheses
Ref Expression
cvmliftlem.1 t t
cvmliftlem.b
cvmliftlem.x
cvmliftlem.f CovMap
cvmliftlem.g
cvmliftlem.p
cvmliftlem.e
cvmliftlem.n
cvmliftlem.t
cvmliftlem.a
cvmliftlem.l
cvmliftlem.q
cvmliftlem.k
cvmliftlem10.1 t
Assertion
Ref Expression
cvmliftlem10 t
Distinct variable groups:   ,,,   ,,,,,,,,,,   ,,   ,,,,,,,,   ,,,,,,,,   ,,,,,   ,,,,,,,,   ,,,,,,,,,   ,   ,,,,,,,,,,   ,,,,,,,,,   ,,,,,,,,,   ,,,,,,,,
Allowed substitution hints:   (,,,,)   (,,,,,,,,,)   (,,,,,,)   (,)   (,)   (,)   ()   ()   ()   (,,,,,,,,,)   (,,,,,,,)   (,)   (,,,,,,,,)

Proof of Theorem cvmliftlem10
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 cvmliftlem.n . . . 4
2 nnuz 11218 . . . 4
31, 2syl6eleq 2559 . . 3
4 eluzfz2 11833 . . 3
53, 4syl 17 . 2
6 eleq1 2537 . . . . . 6
7 oveq2 6316 . . . . . . . . . . 11
8 1z 10991 . . . . . . . . . . . 12
9 fzsn 11866 . . . . . . . . . . . 12
108, 9ax-mp 5 . . . . . . . . . . 11
117, 10syl6eq 2521 . . . . . . . . . 10
1211iuneq1d 4294 . . . . . . . . 9
13 1ex 9656 . . . . . . . . . 10
14 fveq2 5879 . . . . . . . . . 10
1513, 14iunxsn 4352 . . . . . . . . 9
1612, 15syl6eq 2521 . . . . . . . 8
17 oveq1 6315 . . . . . . . . . . 11
1817oveq2d 6324 . . . . . . . . . 10
1918oveq2d 6324 . . . . . . . . 9 t t
2019oveq1d 6323 . . . . . . . 8 t t
2116, 20eleq12d 2543 . . . . . . 7 t t
2216coeq2d 5002 . . . . . . . 8
2318reseq2d 5111 . . . . . . . 8
2422, 23eqeq12d 2486 . . . . . . 7
2521, 24anbi12d 725 . . . . . 6 t t
266, 25imbi12d 327 . . . . 5 t t
2726imbi2d 323 . . . 4 t t
28 eleq1 2537 . . . . . 6
29 oveq2 6316 . . . . . . . . 9
3029iuneq1d 4294 . . . . . . . 8
31 oveq1 6315 . . . . . . . . . . 11
3231oveq2d 6324 . . . . . . . . . 10
3332oveq2d 6324 . . . . . . . . 9 t t
3433oveq1d 6323 . . . . . . . 8 t t
3530, 34eleq12d 2543 . . . . . . 7 t t
3630coeq2d 5002 . . . . . . . 8
3732reseq2d 5111 . . . . . . . 8
3836, 37eqeq12d 2486 . . . . . . 7
3935, 38anbi12d 725 . . . . . 6 t t
4028, 39imbi12d 327 . . . . 5 t t
4140imbi2d 323 . . . 4 t t
42 eleq1 2537 . . . . . 6
43 oveq2 6316 . . . . . . . . 9
4443iuneq1d 4294 . . . . . . . 8
45 oveq1 6315 . . . . . . . . . . 11
4645oveq2d 6324 . . . . . . . . . 10
4746oveq2d 6324 . . . . . . . . 9 t t
4847oveq1d 6323 . . . . . . . 8 t t
4944, 48eleq12d 2543 . . . . . . 7 t t
5044coeq2d 5002 . . . . . . . 8
5146reseq2d 5111 . . . . . . . 8
5250, 51eqeq12d 2486 . . . . . . 7
5349, 52anbi12d 725 . . . . . 6 t t
5442, 53imbi12d 327 . . . . 5 t t
5554imbi2d 323 . . . 4 t t
56 eleq1 2537 . . . . . 6
57 oveq2 6316 . . . . . . . . . 10
5857iuneq1d 4294 . . . . . . . . 9
59 cvmliftlem.k . . . . . . . . 9
6058, 59syl6eqr 2523 . . . . . . . 8
61 oveq1 6315 . . . . . . . . . . 11
6261oveq2d 6324 . . . . . . . . . 10
6362oveq2d 6324 . . . . . . . . 9 t t
6463oveq1d 6323 . . . . . . . 8 t t
6560, 64eleq12d 2543 . . . . . . 7 t t
6660coeq2d 5002 . . . . . . . 8
6762reseq2d 5111 . . . . . . . 8
6866, 67eqeq12d 2486 . . . . . . 7
6965, 68anbi12d 725 . . . . . 6 t t
7056, 69imbi12d 327 . . . . 5 t t
7170imbi2d 323 . . . 4 t t
72 eluzfz1 11832 . . . . . . . . 9
733, 72syl 17 . . . . . . . 8
74 cvmliftlem.1 . . . . . . . . 9 t t
75 cvmliftlem.b . . . . . . . . 9
76 cvmliftlem.x . . . . . . . . 9
77 cvmliftlem.f . . . . . . . . 9 CovMap
78 cvmliftlem.g . . . . . . . . 9
79 cvmliftlem.p . . . . . . . . 9
80 cvmliftlem.e . . . . . . . . 9
81 cvmliftlem.t . . . . . . . . 9
82 cvmliftlem.a . . . . . . . . 9
83 cvmliftlem.l . . . . . . . . 9
84 cvmliftlem.q . . . . . . . . 9
85 eqid 2471 . . . . . . . . 9
8674, 75, 76, 77, 78, 79, 80, 1, 81, 82, 83, 84, 85cvmliftlem8 30087 . . . . . . . 8 t
8773, 86mpdan 681 . . . . . . 7 t
88 1m1e0 10700 . . . . . . . . . . . 12
8988oveq1i 6318 . . . . . . . . . . 11
901nncnd 10647 . . . . . . . . . . . 12
911nnne0d 10676 . . . . . . . . . . . 12
9290, 91div0d 10404 . . . . . . . . . . 11
9389, 92syl5eq 2517 . . . . . . . . . 10
9493oveq1d 6323 . . . . . . . . 9
9594oveq2d 6324 . . . . . . . 8 t t
9695oveq1d 6323 . . . . . . 7 t t
9787, 96eleqtrd 2551 . . . . . 6 t
98 simpr 468 . . . . . . . . . 10
9974, 75, 76, 77, 78, 79, 80, 1, 81, 82, 83, 84, 85cvmliftlem7 30086 . . . . . . . . . 10
10074, 75, 76, 77, 78, 79, 80, 1, 81, 82, 83, 84, 85, 98, 99cvmliftlem6 30085 . . . . . . . . 9
10173, 100mpdan 681 . . . . . . . 8
102101simprd 470 . . . . . . 7
10394reseq2d 5111 . . . . . . 7
104102, 103eqtrd 2505 . . . . . 6
10597, 104jca 541 . . . . 5 t
106105a1d 25 . . . 4 t
107 elnnuz 11219 . . . . . . . . . . 11
108107biimpi 199 . . . . . . . . . 10
109108adantl 473 . . . . . . . . 9
110 peano2fzr 11838 . . . . . . . . . 10
111110ex 441 . . . . . . . . 9
112109, 111syl 17 . . . . . . . 8
113112imim1d 77 . . . . . . 7 t t
114 cvmliftlem10.1 . . . . . . . . . . 11 t
115 eqid 2471 . . . . . . . . . . . . 13 t t
116 0re 9661 . . . . . . . . . . . . . . 15
117114simplbi 467 . . . . . . . . . . . . . . . . . . . 20
118117adantl 473 . . . . . . . . . . . . . . . . . . 19
119118simprd 470 . . . . . . . . . . . . . . . . . 18
120 elfznn 11854 . . . . . . . . . . . . . . . . . 18
121119, 120syl 17 . . . . . . . . . . . . . . . . 17
122121nnred 10646 . . . . . . . . . . . . . . . 16
1231adantr 472 . . . . . . . . . . . . . . . 16
124122, 123nndivred 10680 . . . . . . . . . . . . . . 15
125 iccssre 11741 . . . . . . . . . . . . . . 15
126116, 124, 125sylancr 676 . . . . . . . . . . . . . 14
127117simpld 466 . . . . . . . . . . . . . . . . . . 19
128127adantl 473 . . . . . . . . . . . . . . . . . 18
129128nnred 10646 . . . . . . . . . . . . . . . . 17
130129, 123nndivred 10680 . . . . . . . . . . . . . . . 16
131 icccld 21865 . . . . . . . . . . . . . . . 16
132116, 130, 131sylancr 676 . . . . . . . . . . . . . . 15
13383fveq2i 5882 . . . . . . . . . . . . . . 15
134132, 133syl6eleqr 2560 . . . . . . . . . . . . . 14
135 ssun1 3588 . . . . . . . . . . . . . . 15
136116a1i 11 . . . . . . . . . . . . . . . 16
137128nnnn0d 10949 . . . . . . . . . . . . . . . . . . 19
138137nn0ge0d 10952 . . . . . . . . . . . . . . . . . 18
139123nnred 10646 . . . . . . . . . . . . . . . . . 18
140123nngt0d 10675 . . . . . . . . . . . . . . . . . 18
141 divge0 10496 . . . . . . . . . . . . . . . . . 18
142129, 138, 139, 140, 141syl22anc 1293 . . . . . . . . . . . . . . . . 17
143129ltp1d 10559 . . . . . . . . . . . . . . . . . . 19
144 ltdiv1 10491 . . . . . . . . . . . . . . . . . . . 20
145129, 122, 139, 140, 144syl112anc 1296 . . . . . . . . . . . . . . . . . . 19
146143, 145mpbid 215 . . . . . . . . . . . . . . . . . 18
147130, 124, 146ltled 9800 . . . . . . . . . . . . . . . . 17
148 elicc2 11724 . . . . . . . . . . . . . . . . . 18
149116, 124, 148sylancr 676 . . . . . . . . . . . . . . . . 17
150130, 142, 147, 149mpbir3and 1213 . . . . . . . . . . . . . . . 16
151 iccsplit 11791 . . . . . . . . . . . . . . . 16
152136, 124, 150, 151syl3anc 1292 . . . . . . . . . . . . . . 15
153135, 152syl5sseqr 3467 . . . . . . . . . . . . . 14
154 uniretop 21861 . . . . . . . . . . . . . . . 16
15583unieqi 4199 . . . . . . . . . . . . . . . 16
156154, 155eqtr4i 2496 . . . . . . . . . . . . . . 15
157156restcldi 20266 . . . . . . . . . . . . . 14 t
158126, 134, 153, 157syl3anc 1292 . . . . . . . . . . . . 13 t
159 icccld 21865 . . . . . . . . . . . . . . . 16
160130, 124, 159syl2anc 673 . . . . . . . . . . . . . . 15
161160, 133syl6eleqr 2560 . . . . . . . . . . . . . 14
162 ssun2 3589 . . . . . . . . . . . . . . 15
163162, 152syl5sseqr 3467 . . . . . . . . . . . . . 14
164156restcldi 20266 . . . . . . . . . . . . . 14 t
165126, 161, 163, 164syl3anc 1292 . . . . . . . . . . . . 13 t
166 retop 21860 . . . . . . . . . . . . . . . 16
16783, 166eqeltri 2545 . . . . . . . . . . . . . . 15
168156restuni 20255 . . . . . . . . . . . . . . 15 t
169167, 126, 168sylancr 676 . . . . . . . . . . . . . 14 t
170152, 169eqtr3d 2507 . . . . . . . . . . . . 13 t
171114simprbi 471 . . . . . . . . . . . . . . . . . . . 20 t
172171adantl 473 . . . . . . . . . . . . . . . . . . 19 t
173172simpld 466 . . . . . . . . . . . . . . . . . 18 t
174 eqid 2471 . . . . . . . . . . . . . . . . . . 19 t t
175174, 75cnf 20339 . . . . . . . . . . . . . . . . . 18 t t
176173, 175syl 17 . . . . . . . . . . . . . . . . 17 t
177 iccssre 11741 . . . . . . . . . . . . . . . . . . . 20
178116, 130, 177sylancr 676 . . . . . . . . . . . . . . . . . . 19
179156restuni 20255 . . . . . . . . . . . . . . . . . . 19 t
180167, 178, 179sylancr 676 . . . . . . . . . . . . . . . . . 18 t
181180feq2d 5725 . . . . . . . . . . . . . . . . 17 t
182176, 181mpbird 240 . . . . . . . . . . . . . . . 16
183 eqid 2471 . . . . . . . . . . . . . . . . . . . 20
184 simpr 468 . . . . . . . . . . . . . . . . . . . 20
18574, 75, 76, 77, 78, 79, 80, 1, 81, 82, 83, 84, 183cvmliftlem7 30086 . . . . . . . . . . . . . . . . . . . 20
18674, 75, 76, 77, 78, 79, 80, 1, 81, 82, 83, 84, 183, 184, 185cvmliftlem6 30085 . . . . . . . . . . . . . . . . . . 19
187119, 186syldan 478 . . . . . . . . . . . . . . . . . 18
188187simpld 466 . . . . . . . . . . . . . . . . 17
189128nncnd 10647 . . . . . . . . . . . . . . . . . . . . 21
190 ax-1cn 9615 . . . . . . . . . . . . . . . . . . . . 21
191 pncan 9901 . . . . . . . . . . . . . . . . . . . . 21
192189, 190, 191sylancl 675 . . . . . . . . . . . . . . . . . . . 20
193192oveq1d 6323 . . . . . . . . . . . . . . . . . . 19
194193oveq1d 6323 . . . . . . . . . . . . . . . . . 18
195194feq2d 5725 . . . . . . . . . . . . . . . . 17
196188, 195mpbid 215 . . . . . . . . . . . . . . . 16
197 ffun 5742 . . . . . . . . . . . . . . . . . . . . . . 23
198182, 197syl 17 . . . . . . . . . . . . . . . . . . . . . 22
199128, 108syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24
200 eluzfz2 11833 . . . . . . . . . . . . . . . . . . . . . . . 24
201199, 200syl 17 . . . . . . . . . . . . . . . . . . . . . . 23
202 fveq2 5879 . . . . . . . . . . . . . . . . . . . . . . . 24
203202ssiun2s 4313 . . . . . . . . . . . . . . . . . . . . . . 23
204201, 203syl 17 . . . . . . . . . . . . . . . . . . . . . 22
205 peano2rem 9961 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
206129, 205syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . 26
207206, 123nndivred 10680 . . . . . . . . . . . . . . . . . . . . . . . . 25
208207rexrd 9708 . . . . . . . . . . . . . . . . . . . . . . . 24
209130rexrd 9708 . . . . . . . . . . . . . . . . . . . . . . . 24
210129ltm1d 10561 . . . . . . . . . . . . . . . . . . . . . . . . . 26
211 ltdiv1 10491 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
212206, 129, 139, 140, 211syl112anc 1296 . . . . . . . . . . . . . . . . . . . . . . . . . 26
213210, 212mpbid 215 . . . . . . . . . . . . . . . . . . . . . . . . 25
214207, 130, 213ltled 9800 . . . . . . . . . . . . . . . . . . . . . . . 24
215 ubicc2 11775 . . . . . . . . . . . . . . . . . . . . . . . 24
216208, 209, 214, 215syl3anc 1292 . . . . . . . . . . . . . . . . . . . . . . 23
217199, 119, 110syl2anc 673 . . . . . . . . . . . . . . . . . . . . . . . . . 26
218 eqid 2471 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
219 simpr 468 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
22074, 75, 76, 77, 78, 79, 80, 1, 81, 82, 83, 84, 218cvmliftlem7 30086 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
22174, 75, 76, 77, 78, 79, 80, 1, 81, 82, 83, 84, 218, 219, 220cvmliftlem6 30085 . . . . . . . . . . . . . . . . . . . . . . . . . 26
222217, 221syldan 478 . . . . . . . . . . . . . . . . . . . . . . . . 25
223222simpld 466 . . . . . . . . . . . . . . . . . . . . . . . 24
224 fdm 5745 . . . . . . . . . . . . . . . . . . . . . . . 24
225223, 224syl 17 . . . . . . . . . . . . . . . . . . . . . . 23
226216, 225eleqtrrd 2552 . . . . . . . . . . . . . . . . . . . . . 22
227 funssfv 5894 . . . . . . . . . . . . . . . . . . . . . 22
228198, 204, 226, 227syl3anc 1292 . . . . . . . . . . . . . . . . . . . . 21
229192fveq2d 5883 . . . . . . . . . . . . . . . . . . . . . 22
230229, 193fveq12d 5885 . . . . . . . . . . . . . . . . . . . . 21
23174, 75, 76, 77, 78, 79, 80, 1, 81, 82, 83, 84cvmliftlem9 30088 . . . . . . . . . . . . . . . . . . . . . . 23
232119, 231syldan 478 . . . . . . . . . . . . . . . . . . . . . 22
233193fveq2d 5883 . . . . . . . . . . . . . . . . . . . . . 22
234232, 233eqtr3d 2507 . . . . . . . . . . . . . . . . . . . . 21
235228, 230, 2343eqtr2d 2511 . . . . . . . . . . . . . . . . . . . 20
236235opeq2d 4165 . . . . . . . . . . . . . . . . . . 19
237236sneqd 3971 . . . . . . . . . . . . . . . . . 18
238 ffn 5739 . . . . . . . . . . . . . . . . . . . 20
239182, 238syl 17 . . . . . . . . . . . . . . . . . . 19
240 0xr 9705 . . . . . . . . . . . . . . . . . . . . 21
241240a1i 11 . . . . . . . . . . . . . . . . . . . 20
242 ubicc2 11775 . . . . . . . . . . . . . . . . . . . 20
243241, 209, 142, 242syl3anc 1292 . . . . . . . . . . . . . . . . . . 19
244 fnressn 6092 . . . . . . . . . . . . . . . . . . 19
245239, 243, 244syl2anc 673 . . . . . . . . . . . . . . . . . 18
246 ffn 5739 . . . . . . . . . . . . . . . . . . . 20
247196, 246syl 17 . . . . . . . . . . . . . . . . . . 19
248124rexrd 9708 . . . . . . . . . . . . . . . . . . . 20
249 lbicc2 11774 . . . . . . . . . . . . . . . . . . . 20
250209, 248, 147, 249syl3anc 1292 . . . . . . . . . . . . . . . . . . 19
251 fnressn 6092 . . . . . . . . . . . . . . . . . . 19
252247, 250, 251syl2anc 673 . . . . . . . . . . . . . . . . . 18
253237, 245, 2523eqtr4d 2515 . . . . . . . . . . . . . . . . 17
254 df-icc 11667 . . . . . . . . . . . . . . . . . . . . 21
255 xrmaxle 11501 . . . . . . . . . . . . . . . . . . . . 21
256 xrlemin 11502 . . . . . . . . . . . . . . . . . . . . 21
257254, 255, 256ixxin 11677 . . . . . . . . . . . . . . . . . . . 20
258241, 209, 209, 248, 257syl22anc 1293 . . . . . . . . . . . . . . . . . . 19
259142iftrued 3880 . . . . . . . . . . . . . . . . . . . 20
260147iftrued 3880 . . . . . . . . . . . . . . . . . . . 20
261259, 260oveq12d 6326 . . . . . . . . . . . . . . . . . . 19
262 iccid 11706 . . . . . . . . . . . . . . . . . . . 20
263209, 262syl 17 . . . . . . . . . . . . . . . . . . 19
264258, 261, 2633eqtrd 2509 . . . . . . . . . . . . . . . . . 18
265264reseq2d 5111 . . . . . . . . . . . . . . . . 17
266264reseq2d 5111 . . . . . . . . . . . . . . . . 17
267253, 265, 2663eqtr4d 2515 . . . . . . . . . . . . . . . 16
268 fresaun 5766 . . . . . . . . . . . . . . . 16
269182, 196, 267, 268syl3anc 1292 . . . . . . . . . . . . . . 15
270 fzsuc 11869 . . . . . . . . . . . . . . . . . . 19
271199, 270syl 17 . . . . . . . . . . . . . . . . . 18
272271iuneq1d 4294 . . . . . . . . . . . . . . . . 17
273 iunxun 4354 . . . . . . . . . . . . . . . . . 18
274 ovex 6336 . . . . . . . . . . . . . . . . . . . 20
275 fveq2 5879 . . . . . . . . . . . . . . . . . . . 20
276274, 275iunxsn 4352 . . . . . . . . . . . . . . . . . . 19
277276uneq2i 3576 . . . . . . . . . . . . . . . . . 18
278273, 277eqtri 2493 . . . . . . . . . . . . . . . . 17
279272, 278syl6req 2522 . . . . . . . . . . . . . . . 16
280279feq1d 5724 . . . . . . . . . . . . . . 15
281269, 280mpbid 215 . . . . . . . . . . . . . 14
282170feq2d 5725 . . . . . . . . . . . . . 14 t
283281, 282mpbid 215 . . . . . . . . . . . . 13 t
284279reseq1d 5110 . . . . . . . . . . . . . . 15
285 fresaunres1 5768 . . . . . . . . . . . . . . . 16
286182, 196, 267, 285syl3anc 1292 . . . . . . . . . . . . . . 15
287284, 286eqtr3d 2507 . . . . . . . . . . . . . 14
288167a1i 11 . . . . . . . . . . . . . . . 16
289 ovex 6336 . . . . . . . . . . . . . . . . 17
290289a1i 11 . . . . . . . . . . . . . . . 16
291 restabs 20258 . . . . . . . . . . . . . . . 16 t t t
292288, 153, 290, 291syl3anc 1292 . . . . . . . . . . . . . . 15 t t t
293292oveq1d 6323 . . . . . . . . . . . . . 14 t t t
294173, 287, 2933eltr4d 2564 . . . . . . . . . . . . 13 t t
29574, 75, 76, 77, 78, 79, 80, 1, 81, 82, 83, 84, 183cvmliftlem8 30087 . . . . . . . . . . . . . . . 16 t
296119, 295syldan 478 . . . . . . . . . . . . . . 15 t
297194oveq2d 6324 . . . . . . . . . . . . . . . 16 t t
298297oveq1d 6323 . . . . . . . . . . . . . . 15 t t
299296, 298eleqtrd 2551 . . . . . . . . . . . . . 14 t
300279reseq1d 5110 . . . . . . . . . . . . . . 15
301 fresaunres2 5767 . . . . . . . . . . . . . . . 16
302182, 196, 267, 301syl3anc 1292 . . . . . . . . . . . . . . 15
303300, 302eqtr3d 2507 . . . . . . . . . . . . . 14
304 restabs 20258 . . . . . . . . . . . . . . . 16 t t t
305288, 163, 290, 304syl3anc 1292 . . . . . . . . . . . . . . 15 t t t
306305oveq1d 6323 . . . . . . . . . . . . . 14 t t t
307299, 303, 3063eltr4d 2564 . . . . . . . . . . . . 13 t t
308115, 75, 158, 165, 170, 283, 294, 307paste 20387 . . . . . . . . . . . 12 t
309152reseq2d 5111 . . . . . . . . . . . . 13
310172simprd 470 . . . . . . . . . . . . . . 15
311187simprd 470 . . . . . . . . . . . . . . . 16
312194reseq2d 5111 . . . . . . . . . . . . . . . 16
313311, 312eqtrd 2505 . . . . . . . . . . . . . . 15
314310, 313uneq12d 3580 . . . . . . . . . . . . . 14
315 coundi 5343 . . . . . . . . . . . . . 14
316 resundi 5124 . . . . . . . . . . . . . 14
317314, 315, 3163eqtr4g 2530 . . . . . . . . . . . . 13
318279coeq2d 5002 . . . . . . . . . . . . 13
319309, 317, 3183eqtr2rd 2512 . . . . . . . . . . . 12
320308, 319jca 541 . . . . . . . . . . 11 t
321114, 320sylan2br 484 . . . . . . . . . 10 t t
322321expr 626 . . . . . . . . 9 t t
323322expr 626 . . . . . . . 8 t t
324323a2d 28 . . . . . . 7 t t