Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  pcohtpylem Structured version   Visualization version   Unicode version

Theorem pcohtpylem 22050
 Description: Lemma for pcohtpy 22051. (Contributed by Jeff Madsen, 15-Jun-2010.) (Revised by Mario Carneiro, 24-Feb-2015.)
Hypotheses
Ref Expression
pcohtpy.4
pcohtpy.5
pcohtpy.6
pcohtpylem.7
pcohtpylem.8
pcohtpylem.9
Assertion
Ref Expression
pcohtpylem
Distinct variable groups:   ,,   ,,   ,,   ,,   ,,   ,,   ,,   ,,
Allowed substitution hints:   (,)

Proof of Theorem pcohtpylem
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 pcohtpy.5 . . . . 5
2 isphtpc 22025 . . . . 5
31, 2sylib 200 . . . 4
43simp1d 1020 . . 3
5 pcohtpy.6 . . . . 5
6 isphtpc 22025 . . . . 5
75, 6sylib 200 . . . 4
87simp1d 1020 . . 3
9 pcohtpy.4 . . 3
104, 8, 9pcocn 22048 . 2
113simp2d 1021 . . 3
127simp2d 1021 . . 3
13 pcohtpylem.8 . . . . . 6
144, 11, 13phtpy01 22016 . . . . 5
1514simprd 465 . . . 4
16 pcohtpylem.9 . . . . . 6
178, 12, 16phtpy01 22016 . . . . 5
1817simpld 461 . . . 4
199, 15, 183eqtr3d 2493 . . 3
2011, 12, 19pcocn 22048 . 2
21 pcohtpylem.7 . . 3
22 eqid 2451 . . . 4
23 eqid 2451 . . . 4 t t
24 eqid 2451 . . . 4 t t
25 dfii2 21914 . . . 4 t
26 0red 9644 . . . 4
27 1red 9658 . . . 4
28 halfre 10828 . . . . . 6
29 0re 9643 . . . . . . 7
30 halfgt0 10830 . . . . . . 7
3129, 28, 30ltleii 9757 . . . . . 6
32 1re 9642 . . . . . . 7
33 halflt1 10831 . . . . . . 7
3428, 32, 33ltleii 9757 . . . . . 6
3529, 32elicc2i 11700 . . . . . 6
3628, 31, 34, 35mpbir3an 1190 . . . . 5
3736a1i 11 . . . 4
38 iitopon 21911 . . . . 5 TopOn
3938a1i 11 . . . 4 TopOn
409adantr 467 . . . . . 6
414, 11, 13phtpyi 22015 . . . . . . . 8
4241simprd 465 . . . . . . 7
4342adantrl 722 . . . . . 6
448, 12, 16phtpyi 22015 . . . . . . . 8
4544simpld 461 . . . . . . 7
4645adantrl 722 . . . . . 6
4740, 43, 463eqtr4d 2495 . . . . 5
48 simprl 764 . . . . . . . 8
4948oveq2d 6306 . . . . . . 7
50 2cn 10680 . . . . . . . 8
51 2ne0 10702 . . . . . . . 8
5250, 51recidi 10338 . . . . . . 7
5349, 52syl6eq 2501 . . . . . 6
5453oveq1d 6305 . . . . 5
5553oveq1d 6305 . . . . . . 7
56 1m1e0 10678 . . . . . . 7
5755, 56syl6eq 2501 . . . . . 6
5857oveq1d 6305 . . . . 5
5947, 54, 583eqtr4d 2495 . . . 4
60 retopon 21784 . . . . . . 7 TopOn
61 iccssre 11716 . . . . . . . 8
6229, 28, 61mp2an 678 . . . . . . 7
63 resttopon 20177 . . . . . . 7 TopOn t TopOn
6460, 62, 63mp2an 678 . . . . . 6 t TopOn
6564a1i 11 . . . . 5 t TopOn
6665, 39cnmpt1st 20683 . . . . . 6 t t
6723iihalf1cn 21960 . . . . . . 7 t
6867a1i 11 . . . . . 6 t
69 oveq2 6298 . . . . . 6
7065, 39, 66, 65, 68, 69cnmpt21 20686 . . . . 5 t
7165, 39cnmpt2nd 20684 . . . . 5 t
724, 11phtpycn 22014 . . . . . 6
7372, 13sseldd 3433 . . . . 5
7465, 39, 70, 71, 73cnmpt22f 20690 . . . 4 t
75 iccssre 11716 . . . . . . . 8
7628, 32, 75mp2an 678 . . . . . . 7
77 resttopon 20177 . . . . . . 7 TopOn t TopOn
7860, 76, 77mp2an 678 . . . . . 6 t TopOn
7978a1i 11 . . . . 5 t TopOn
8079, 39cnmpt1st 20683 . . . . . 6 t t
8124iihalf2cn 21962 . . . . . . 7 t
8281a1i 11 . . . . . 6 t
8369oveq1d 6305 . . . . . 6
8479, 39, 80, 79, 82, 83cnmpt21 20686 . . . . 5 t
8579, 39cnmpt2nd 20684 . . . . 5 t
868, 12phtpycn 22014 . . . . . 6
8786, 16sseldd 3433 . . . . 5
8879, 39, 84, 85, 87cnmpt22f 20690 . . . 4 t
8922, 23, 24, 25, 26, 27, 37, 39, 59, 74, 88cnmpt2pc 21956 . . 3
9021, 89syl5eqel 2533 . 2
91 simpll 760 . . . . . . 7
92 elii1 21963 . . . . . . . . 9
93 iihalf1 21959 . . . . . . . . 9
9492, 93sylbir 217 . . . . . . . 8
9594adantll 720 . . . . . . 7
964, 11phtpyhtpy 22013 . . . . . . . . 9 Htpy
9796, 13sseldd 3433 . . . . . . . 8 Htpy
9839, 4, 11, 97htpyi 22005 . . . . . . 7
9991, 95, 98syl2anc 667 . . . . . 6
10099simpld 461 . . . . 5
101 iftrue 3887 . . . . . 6
102101adantl 468 . . . . 5
103 iftrue 3887 . . . . . 6
104103adantl 468 . . . . 5
105100, 102, 1043eqtr4d 2495 . . . 4
106 simpll 760 . . . . . . 7
107 elii2 21964 . . . . . . . . 9
108107adantll 720 . . . . . . . 8
109 iihalf2 21961 . . . . . . . 8
110108, 109syl 17 . . . . . . 7
1118, 12phtpyhtpy 22013 . . . . . . . . 9 Htpy
112111, 16sseldd 3433 . . . . . . . 8 Htpy
11339, 8, 12, 112htpyi 22005 . . . . . . 7
114106, 110, 113syl2anc 667 . . . . . 6
115114simpld 461 . . . . 5
116 iffalse 3890 . . . . . 6
117116adantl 468 . . . . 5
118 iffalse 3890 . . . . . 6
119118adantl 468 . . . . 5
120115, 117, 1193eqtr4d 2495 . . . 4
121105, 120pm2.61dan 800 . . 3
122 simpr 463 . . . 4
123 0elunit 11750 . . . 4
124 simpl 459 . . . . . . 7
125124breq1d 4412 . . . . . 6
126124oveq2d 6306 . . . . . . 7
127 simpr 463 . . . . . . 7
128126, 127oveq12d 6308 . . . . . 6
129126oveq1d 6305 . . . . . . 7
130129, 127oveq12d 6308 . . . . . 6
131125, 128, 130ifbieq12d 3908 . . . . 5
132 ovex 6318 . . . . . 6
133 ovex 6318 . . . . . 6
134132, 133ifex 3949 . . . . 5
135131, 21, 134ovmpt2a 6427 . . . 4
136122, 123, 135sylancl 668 . . 3
1374, 8pcovalg 22043 . . 3
138121, 136, 1373eqtr4d 2495 . 2
13999simprd 465 . . . . 5
140 iftrue 3887 . . . . . 6
141140adantl 468 . . . . 5
142 iftrue 3887 . . . . . 6
143142adantl 468 . . . . 5
144139, 141, 1433eqtr4d 2495 . . . 4
145114simprd 465 . . . . 5
146 iffalse 3890 . . . . . 6
147146adantl 468 . . . . 5
148 iffalse 3890 . . . . . 6
149148adantl 468 . . . . 5
150145, 147, 1493eqtr4d 2495 . . . 4
151144, 150pm2.61dan 800 . . 3
152 1elunit 11751 . . . 4
153 simpl 459 . . . . . . 7
154153breq1d 4412 . . . . . 6
155153oveq2d 6306 . . . . . . 7
156 simpr 463 . . . . . . 7
157155, 156oveq12d 6308 . . . . . 6
158155oveq1d 6305 . . . . . . 7
159158, 156oveq12d 6308 . . . . . 6
160154, 157, 159ifbieq12d 3908 . . . . 5
161 ovex 6318 . . . . . 6
162 ovex 6318 . . . . . 6
163161, 162ifex 3949 . . . . 5
164160, 21, 163ovmpt2a 6427 . . . 4
165122, 152, 164sylancl 668 . . 3
16611, 12pcovalg 22043 . . 3
167151, 165, 1663eqtr4d 2495 . 2
1684, 11, 13phtpyi 22015 . . . 4
169168simpld 461 . . 3
170 simpl 459 . . . . . . . 8
171170, 31syl6eqbr 4440 . . . . . . 7
172171iftrued 3889 . . . . . 6
173170oveq2d 6306 . . . . . . . 8
174 2t0e0 10765 . . . . . . . 8
175173, 174syl6eq 2501 . . . . . . 7
176 simpr 463 . . . . . . 7
177175, 176oveq12d 6308 . . . . . 6
178172, 177eqtrd 2485 . . . . 5
179 ovex 6318 . . . . 5
180178, 21, 179ovmpt2a 6427 . . . 4
181123, 122, 180sylancr 669 . . 3
1824, 8pco0 22045 . . . 4
184169, 181, 1833eqtr4d 2495 . 2
1858, 12, 16phtpyi 22015 . . . 4
186185simprd 465 . . 3
18728, 32ltnlei 9755 . . . . . . . . 9
18833, 187mpbi 212 . . . . . . . 8
189 simpl 459 . . . . . . . . 9
190189breq1d 4412 . . . . . . . 8
191188, 190mtbiri 305 . . . . . . 7
192191iffalsed 3892 . . . . . 6
193189oveq2d 6306 . . . . . . . . . 10
194 2t1e2 10758 . . . . . . . . . 10
195193, 194syl6eq 2501 . . . . . . . . 9
196195oveq1d 6305 . . . . . . . 8
197 2m1e1 10724 . . . . . . . 8
198196, 197syl6eq 2501 . . . . . . 7
199 simpr 463 . . . . . . 7
200198, 199oveq12d 6308 . . . . . 6
201192, 200eqtrd 2485 . . . . 5
202 ovex 6318 . . . . 5
203201, 21, 202ovmpt2a 6427 . . . 4
204152, 122, 203sylancr 669 . . 3
2054, 8pco1 22046 . . . 4