Step | Hyp | Ref
| Expression |
1 | | pcohtpy.5 |
. . . . 5
       |
2 | | isphtpc 22025 |
. . . . 5
 
     


           |
3 | 1, 2 | sylib 200 |
. . . 4
                 |
4 | 3 | simp1d 1020 |
. . 3
     |
5 | | pcohtpy.6 |
. . . . 5
       |
6 | | isphtpc 22025 |
. . . . 5
 
     


           |
7 | 5, 6 | sylib 200 |
. . . 4
                 |
8 | 7 | simp1d 1020 |
. . 3
     |
9 | | pcohtpy.4 |
. . 3
           |
10 | 4, 8, 9 | pcocn 22048 |
. 2
             |
11 | 3 | simp2d 1021 |
. . 3
     |
12 | 7 | simp2d 1021 |
. . 3
     |
13 | | pcohtpylem.8 |
. . . . . 6
           |
14 | 4, 11, 13 | phtpy01 22016 |
. . . . 5
                     |
15 | 14 | simprd 465 |
. . . 4
           |
16 | | pcohtpylem.9 |
. . . . . 6
           |
17 | 8, 12, 16 | phtpy01 22016 |
. . . . 5
                     |
18 | 17 | simpld 461 |
. . . 4
           |
19 | 9, 15, 18 | 3eqtr3d 2493 |
. . 3
           |
20 | 11, 12, 19 | pcocn 22048 |
. 2
             |
21 | | pcohtpylem.7 |
. . 3
   ![[,] [,]](_icc.gif)     ![[,] [,]](_icc.gif)                         |
22 | | eqid 2451 |
. . . 4
         |
23 | | eqid 2451 |
. . . 4
     ↾t   ![[,] [,]](_icc.gif)          ↾t   ![[,] [,]](_icc.gif)      |
24 | | eqid 2451 |
. . . 4
     ↾t     ![[,] [,]](_icc.gif)        ↾t     ![[,] [,]](_icc.gif)    |
25 | | dfii2 21914 |
. . . 4
     ↾t   ![[,] [,]](_icc.gif)    |
26 | | 0red 9644 |
. . . 4
   |
27 | | 1red 9658 |
. . . 4
   |
28 | | halfre 10828 |
. . . . . 6
   |
29 | | 0re 9643 |
. . . . . . 7
 |
30 | | halfgt0 10830 |
. . . . . . 7
   |
31 | 29, 28, 30 | ltleii 9757 |
. . . . . 6
   |
32 | | 1re 9642 |
. . . . . . 7
 |
33 | | halflt1 10831 |
. . . . . . 7
   |
34 | 28, 32, 33 | ltleii 9757 |
. . . . . 6
   |
35 | 29, 32 | elicc2i 11700 |
. . . . . 6
     ![[,] [,]](_icc.gif) 
    
     |
36 | 28, 31, 34, 35 | mpbir3an 1190 |
. . . . 5
    ![[,] [,]](_icc.gif)   |
37 | 36 | a1i 11 |
. . . 4
     ![[,] [,]](_icc.gif)    |
38 | | iitopon 21911 |
. . . . 5
TopOn   ![[,] [,]](_icc.gif)    |
39 | 38 | a1i 11 |
. . . 4
 TopOn   ![[,] [,]](_icc.gif)     |
40 | 9 | adantr 467 |
. . . . . 6
 
     ![[,] [,]](_icc.gif)              |
41 | 4, 11, 13 | phtpyi 22015 |
. . . . . . . 8
 
  ![[,] [,]](_icc.gif)                       |
42 | 41 | simprd 465 |
. . . . . . 7
 
  ![[,] [,]](_icc.gif)             |
43 | 42 | adantrl 722 |
. . . . . 6
 
     ![[,] [,]](_icc.gif)              |
44 | 8, 12, 16 | phtpyi 22015 |
. . . . . . . 8
 
  ![[,] [,]](_icc.gif)                       |
45 | 44 | simpld 461 |
. . . . . . 7
 
  ![[,] [,]](_icc.gif)             |
46 | 45 | adantrl 722 |
. . . . . 6
 
     ![[,] [,]](_icc.gif)              |
47 | 40, 43, 46 | 3eqtr4d 2495 |
. . . . 5
 
     ![[,] [,]](_icc.gif)              |
48 | | simprl 764 |
. . . . . . . 8
 
     ![[,] [,]](_icc.gif)   
    |
49 | 48 | oveq2d 6306 |
. . . . . . 7
 
     ![[,] [,]](_icc.gif)            |
50 | | 2cn 10680 |
. . . . . . . 8
 |
51 | | 2ne0 10702 |
. . . . . . . 8
 |
52 | 50, 51 | recidi 10338 |
. . . . . . 7
     |
53 | 49, 52 | syl6eq 2501 |
. . . . . 6
 
     ![[,] [,]](_icc.gif)        |
54 | 53 | oveq1d 6305 |
. . . . 5
 
     ![[,] [,]](_icc.gif)                |
55 | 53 | oveq1d 6305 |
. . . . . . 7
 
     ![[,] [,]](_icc.gif)            |
56 | | 1m1e0 10678 |
. . . . . . 7
   |
57 | 55, 56 | syl6eq 2501 |
. . . . . 6
 
     ![[,] [,]](_icc.gif)          |
58 | 57 | oveq1d 6305 |
. . . . 5
 
     ![[,] [,]](_icc.gif)                  |
59 | 47, 54, 58 | 3eqtr4d 2495 |
. . . 4
 
     ![[,] [,]](_icc.gif)                    |
60 | | retopon 21784 |
. . . . . . 7
    TopOn   |
61 | | iccssre 11716 |
. . . . . . . 8
       ![[,] [,]](_icc.gif)      |
62 | 29, 28, 61 | mp2an 678 |
. . . . . . 7
  ![[,] [,]](_icc.gif)     |
63 | | resttopon 20177 |
. . . . . . 7
      TopOn    ![[,] [,]](_icc.gif)   
      ↾t   ![[,] [,]](_icc.gif)     TopOn   ![[,] [,]](_icc.gif)       |
64 | 60, 62, 63 | mp2an 678 |
. . . . . 6
     ↾t   ![[,] [,]](_icc.gif)     TopOn   ![[,] [,]](_icc.gif)      |
65 | 64 | a1i 11 |
. . . . 5
      ↾t   ![[,] [,]](_icc.gif)     TopOn   ![[,] [,]](_icc.gif)       |
66 | 65, 39 | cnmpt1st 20683 |
. . . . . 6
    ![[,] [,]](_icc.gif)       ![[,] [,]](_icc.gif)         
↾t   ![[,] [,]](_icc.gif)     
     ↾t   ![[,] [,]](_icc.gif)        |
67 | 23 | iihalf1cn 21960 |
. . . . . . 7
   ![[,] [,]](_icc.gif)             ↾t   ![[,] [,]](_icc.gif)       |
68 | 67 | a1i 11 |
. . . . . 6
    ![[,] [,]](_icc.gif)             ↾t   ![[,] [,]](_icc.gif)        |
69 | | oveq2 6298 |
. . . . . 6
       |
70 | 65, 39, 66, 65, 68, 69 | cnmpt21 20686 |
. . . . 5
    ![[,] [,]](_icc.gif)       ![[,] [,]](_icc.gif)           
↾t   ![[,] [,]](_icc.gif)     
   |
71 | 65, 39 | cnmpt2nd 20684 |
. . . . 5
    ![[,] [,]](_icc.gif)       ![[,] [,]](_icc.gif)         
↾t   ![[,] [,]](_icc.gif)     
   |
72 | 4, 11 | phtpycn 22014 |
. . . . . 6
               |
73 | 72, 13 | sseldd 3433 |
. . . . 5
  
    |
74 | 65, 39, 70, 71, 73 | cnmpt22f 20690 |
. . . 4
    ![[,] [,]](_icc.gif)       ![[,] [,]](_icc.gif)               
↾t   ![[,] [,]](_icc.gif)     
   |
75 | | iccssre 11716 |
. . . . . . . 8
   
     ![[,] [,]](_icc.gif) 
  |
76 | 28, 32, 75 | mp2an 678 |
. . . . . . 7
    ![[,] [,]](_icc.gif)   |
77 | | resttopon 20177 |
. . . . . . 7
      TopOn      ![[,] [,]](_icc.gif) 
      ↾t     ![[,] [,]](_icc.gif)   TopOn     ![[,] [,]](_icc.gif)     |
78 | 60, 76, 77 | mp2an 678 |
. . . . . 6
     ↾t     ![[,] [,]](_icc.gif)   TopOn     ![[,] [,]](_icc.gif)    |
79 | 78 | a1i 11 |
. . . . 5
      ↾t     ![[,] [,]](_icc.gif)   TopOn     ![[,] [,]](_icc.gif)     |
80 | 79, 39 | cnmpt1st 20683 |
. . . . . 6
      ![[,] [,]](_icc.gif)     ![[,] [,]](_icc.gif)         
↾t     ![[,] [,]](_icc.gif)   
     ↾t     ![[,] [,]](_icc.gif)      |
81 | 24 | iihalf2cn 21962 |
. . . . . . 7
     ![[,] [,]](_icc.gif)             ↾t     ![[,] [,]](_icc.gif)     |
82 | 81 | a1i 11 |
. . . . . 6
      ![[,] [,]](_icc.gif)             ↾t     ![[,] [,]](_icc.gif)      |
83 | 69 | oveq1d 6305 |
. . . . . 6
           |
84 | 79, 39, 80, 79, 82, 83 | cnmpt21 20686 |
. . . . 5
      ![[,] [,]](_icc.gif)     ![[,] [,]](_icc.gif)             
↾t     ![[,] [,]](_icc.gif)   
   |
85 | 79, 39 | cnmpt2nd 20684 |
. . . . 5
      ![[,] [,]](_icc.gif)     ![[,] [,]](_icc.gif)         
↾t     ![[,] [,]](_icc.gif)   
   |
86 | 8, 12 | phtpycn 22014 |
. . . . . 6
               |
87 | 86, 16 | sseldd 3433 |
. . . . 5
  
    |
88 | 79, 39, 84, 85, 87 | cnmpt22f 20690 |
. . . 4
      ![[,] [,]](_icc.gif)     ![[,] [,]](_icc.gif)                 
↾t     ![[,] [,]](_icc.gif)   
   |
89 | 22, 23, 24, 25, 26, 27, 37, 39, 59, 74, 88 | cnmpt2pc 21956 |
. . 3
    ![[,] [,]](_icc.gif)     ![[,] [,]](_icc.gif)                          
   |
90 | 21, 89 | syl5eqel 2533 |
. 2
  
    |
91 | | simpll 760 |
. . . . . . 7
     ![[,] [,]](_icc.gif)        |
92 | | elii1 21963 |
. . . . . . . . 9
   ![[,] [,]](_icc.gif)   
   ![[,] [,]](_icc.gif) 
     |
93 | | iihalf1 21959 |
. . . . . . . . 9
   ![[,] [,]](_icc.gif)        ![[,] [,]](_icc.gif)    |
94 | 92, 93 | sylbir 217 |
. . . . . . . 8
    ![[,] [,]](_icc.gif)         ![[,] [,]](_icc.gif)    |
95 | 94 | adantll 720 |
. . . . . . 7
     ![[,] [,]](_icc.gif)          ![[,] [,]](_icc.gif)    |
96 | 4, 11 | phtpyhtpy 22013 |
. . . . . . . . 9
            Htpy      |
97 | 96, 13 | sseldd 3433 |
. . . . . . . 8
    Htpy      |
98 | 39, 4, 11, 97 | htpyi 22005 |
. . . . . . 7
 
    ![[,] [,]](_icc.gif)                               |
99 | 91, 95, 98 | syl2anc 667 |
. . . . . 6
     ![[,] [,]](_icc.gif)                                  |
100 | 99 | simpld 461 |
. . . . 5
     ![[,] [,]](_icc.gif)                    |
101 | | iftrue 3887 |
. . . . . 6
                                |
102 | 101 | adantl 468 |
. . . . 5
     ![[,] [,]](_icc.gif)                                   |
103 | | iftrue 3887 |
. . . . . 6
                                |
104 | 103 | adantl 468 |
. . . . 5
     ![[,] [,]](_icc.gif)                                   |
105 | 100, 102,
104 | 3eqtr4d 2495 |
. . . 4
     ![[,] [,]](_icc.gif)                            
                     |
106 | | simpll 760 |
. . . . . . 7
     ![[,] [,]](_icc.gif)        |
107 | | elii2 21964 |
. . . . . . . . 9
    ![[,] [,]](_icc.gif) 
       ![[,] [,]](_icc.gif)    |
108 | 107 | adantll 720 |
. . . . . . . 8
     ![[,] [,]](_icc.gif)          ![[,] [,]](_icc.gif)    |
109 | | iihalf2 21961 |
. . . . . . . 8
     ![[,] [,]](_icc.gif)        ![[,] [,]](_icc.gif)    |
110 | 108, 109 | syl 17 |
. . . . . . 7
     ![[,] [,]](_icc.gif)            ![[,] [,]](_icc.gif)    |
111 | 8, 12 | phtpyhtpy 22013 |
. . . . . . . . 9
            Htpy      |
112 | 111, 16 | sseldd 3433 |
. . . . . . . 8
    Htpy      |
113 | 39, 8, 12, 112 | htpyi 22005 |
. . . . . . 7
 
      ![[,] [,]](_icc.gif)                                       |
114 | 106, 110,
113 | syl2anc 667 |
. . . . . 6
     ![[,] [,]](_icc.gif)                                          |
115 | 114 | simpld 461 |
. . . . 5
     ![[,] [,]](_icc.gif)                        |
116 | | iffalse 3890 |
. . . . . 6

                                 |
117 | 116 | adantl 468 |
. . . . 5
     ![[,] [,]](_icc.gif)                                     |
118 | | iffalse 3890 |
. . . . . 6

                                 |
119 | 118 | adantl 468 |
. . . . 5
     ![[,] [,]](_icc.gif)                                     |
120 | 115, 117,
119 | 3eqtr4d 2495 |
. . . 4
     ![[,] [,]](_icc.gif)                            
                     |
121 | 105, 120 | pm2.61dan 800 |
. . 3
 
  ![[,] [,]](_icc.gif)                         
                     |
122 | | simpr 463 |
. . . 4
 
  ![[,] [,]](_icc.gif)     ![[,] [,]](_icc.gif)    |
123 | | 0elunit 11750 |
. . . 4
  ![[,] [,]](_icc.gif)   |
124 | | simpl 459 |
. . . . . . 7
 
   |
125 | 124 | breq1d 4412 |
. . . . . 6
 
         |
126 | 124 | oveq2d 6306 |
. . . . . . 7
 
       |
127 | | simpr 463 |
. . . . . . 7
 
   |
128 | 126, 127 | oveq12d 6308 |
. . . . . 6
 
               |
129 | 126 | oveq1d 6305 |
. . . . . . 7
 
           |
130 | 129, 127 | oveq12d 6308 |
. . . . . 6
 
                   |
131 | 125, 128,
130 | ifbieq12d 3908 |
. . . . 5
 
                                             |
132 | | ovex 6318 |
. . . . . 6
       |
133 | | ovex 6318 |
. . . . . 6
         |
134 | 132, 133 | ifex 3949 |
. . . . 5
 
                    |
135 | 131, 21, 134 | ovmpt2a 6427 |
. . . 4
    ![[,] [,]](_icc.gif) 
  ![[,] [,]](_icc.gif)                              |
136 | 122, 123,
135 | sylancl 668 |
. . 3
 
  ![[,] [,]](_icc.gif)                              |
137 | 4, 8 | pcovalg 22043 |
. . 3
 
  ![[,] [,]](_icc.gif)                                      |
138 | 121, 136,
137 | 3eqtr4d 2495 |
. 2
 
  ![[,] [,]](_icc.gif)                     |
139 | 99 | simprd 465 |
. . . . 5
     ![[,] [,]](_icc.gif)                    |
140 | | iftrue 3887 |
. . . . . 6
                                |
141 | 140 | adantl 468 |
. . . . 5
     ![[,] [,]](_icc.gif)                                   |
142 | | iftrue 3887 |
. . . . . 6
                                |
143 | 142 | adantl 468 |
. . . . 5
     ![[,] [,]](_icc.gif)                                   |
144 | 139, 141,
143 | 3eqtr4d 2495 |
. . . 4
     ![[,] [,]](_icc.gif)                            
                     |
145 | 114 | simprd 465 |
. . . . 5
     ![[,] [,]](_icc.gif)                        |
146 | | iffalse 3890 |
. . . . . 6

                                 |
147 | 146 | adantl 468 |
. . . . 5
     ![[,] [,]](_icc.gif)                                     |
148 | | iffalse 3890 |
. . . . . 6

                                 |
149 | 148 | adantl 468 |
. . . . 5
     ![[,] [,]](_icc.gif)                                     |
150 | 145, 147,
149 | 3eqtr4d 2495 |
. . . 4
     ![[,] [,]](_icc.gif)                            
                     |
151 | 144, 150 | pm2.61dan 800 |
. . 3
 
  ![[,] [,]](_icc.gif)                         
                     |
152 | | 1elunit 11751 |
. . . 4
  ![[,] [,]](_icc.gif)   |
153 | | simpl 459 |
. . . . . . 7
 
   |
154 | 153 | breq1d 4412 |
. . . . . 6
 
         |
155 | 153 | oveq2d 6306 |
. . . . . . 7
 
       |
156 | | simpr 463 |
. . . . . . 7
 
   |
157 | 155, 156 | oveq12d 6308 |
. . . . . 6
 
               |
158 | 155 | oveq1d 6305 |
. . . . . . 7
 
           |
159 | 158, 156 | oveq12d 6308 |
. . . . . 6
 
                   |
160 | 154, 157,
159 | ifbieq12d 3908 |
. . . . 5
 
                                             |
161 | | ovex 6318 |
. . . . . 6
       |
162 | | ovex 6318 |
. . . . . 6
         |
163 | 161, 162 | ifex 3949 |
. . . . 5
 
                    |
164 | 160, 21, 163 | ovmpt2a 6427 |
. . . 4
    ![[,] [,]](_icc.gif) 
  ![[,] [,]](_icc.gif)                              |
165 | 122, 152,
164 | sylancl 668 |
. . 3
 
  ![[,] [,]](_icc.gif)                              |
166 | 11, 12 | pcovalg 22043 |
. . 3
 
  ![[,] [,]](_icc.gif)                                      |
167 | 151, 165,
166 | 3eqtr4d 2495 |
. 2
 
  ![[,] [,]](_icc.gif)                     |
168 | 4, 11, 13 | phtpyi 22015 |
. . . 4
 
  ![[,] [,]](_icc.gif)                       |
169 | 168 | simpld 461 |
. . 3
 
  ![[,] [,]](_icc.gif)             |
170 | | simpl 459 |
. . . . . . . 8
     |
171 | 170, 31 | syl6eqbr 4440 |
. . . . . . 7
       |
172 | 171 | iftrued 3889 |
. . . . . 6
                                |
173 | 170 | oveq2d 6306 |
. . . . . . . 8
         |
174 | | 2t0e0 10765 |
. . . . . . . 8
   |
175 | 173, 174 | syl6eq 2501 |
. . . . . . 7
       |
176 | | simpr 463 |
. . . . . . 7
     |
177 | 175, 176 | oveq12d 6308 |
. . . . . 6
               |
178 | 172, 177 | eqtrd 2485 |
. . . . 5
                              |
179 | | ovex 6318 |
. . . . 5
     |
180 | 178, 21, 179 | ovmpt2a 6427 |
. . . 4
    ![[,] [,]](_icc.gif) 
  ![[,] [,]](_icc.gif)             |
181 | 123, 122,
180 | sylancr 669 |
. . 3
 
  ![[,] [,]](_icc.gif)             |
182 | 4, 8 | pco0 22045 |
. . . 4
                   |
183 | 182 | adantr 467 |
. . 3
 
  ![[,] [,]](_icc.gif)                     |
184 | 169, 181,
183 | 3eqtr4d 2495 |
. 2
 
  ![[,] [,]](_icc.gif)                     |
185 | 8, 12, 16 | phtpyi 22015 |
. . . 4
 
  ![[,] [,]](_icc.gif)                       |
186 | 185 | simprd 465 |
. . 3
 
  ![[,] [,]](_icc.gif)             |
187 | 28, 32 | ltnlei 9755 |
. . . . . . . . 9
  
    |
188 | 33, 187 | mpbi 212 |
. . . . . . . 8
   |
189 | | simpl 459 |
. . . . . . . . 9
     |
190 | 189 | breq1d 4412 |
. . . . . . . 8
           |
191 | 188, 190 | mtbiri 305 |
. . . . . . 7
  
    |
192 | 191 | iffalsed 3892 |
. . . . . 6
                                  |
193 | 189 | oveq2d 6306 |
. . . . . . . . . 10
         |
194 | | 2t1e2 10758 |
. . . . . . . . . 10
   |
195 | 193, 194 | syl6eq 2501 |
. . . . . . . . 9
       |
196 | 195 | oveq1d 6305 |
. . . . . . . 8
           |
197 | | 2m1e1 10724 |
. . . . . . . 8
   |
198 | 196, 197 | syl6eq 2501 |
. . . . . . 7
         |
199 | | simpr 463 |
. . . . . . 7
     |
200 | 198, 199 | oveq12d 6308 |
. . . . . 6
                 |
201 | 192, 200 | eqtrd 2485 |
. . . . 5
                              |
202 | | ovex 6318 |
. . . . 5
     |
203 | 201, 21, 202 | ovmpt2a 6427 |
. . . 4
    ![[,] [,]](_icc.gif) 
  ![[,] [,]](_icc.gif)             |
204 | 152, 122,
203 | sylancr 669 |
. . 3
 
  ![[,] [,]](_icc.gif)             |
205 | 4, 8 | pco1 22046 |
. . . 4
                   |
206 | 205 | adantr 467 |
. . 3
 
  ![[,] [,]](_icc.gif)                     |
207 | 186, 204,
206 | 3eqtr4d 2495 |
. 2
 
  ![[,] [,]](_icc.gif)                     |
208 | 10, 20, 90, 138, 167, 184, 207 | isphtpy2d 22018 |
1
                           |