Step | Hyp | Ref
| Expression |
1 | | pcorev.1 |
. . . . 5
   ![[,] [,]](_icc.gif)          |
2 | | iitopon 21911 |
. . . . . . 7
TopOn   ![[,] [,]](_icc.gif)    |
3 | 2 | a1i 11 |
. . . . . 6
   TopOn   ![[,] [,]](_icc.gif)     |
4 | | iirevcn 21958 |
. . . . . . 7
   ![[,] [,]](_icc.gif)        |
5 | 4 | a1i 11 |
. . . . . 6
      ![[,] [,]](_icc.gif)         |
6 | | id 22 |
. . . . . 6
       |
7 | 3, 5, 6 | cnmpt11f 20679 |
. . . . 5
      ![[,] [,]](_icc.gif)             |
8 | 1, 7 | syl5eqel 2533 |
. . . 4
       |
9 | | 1elunit 11751 |
. . . . 5
  ![[,] [,]](_icc.gif)   |
10 | | oveq2 6298 |
. . . . . . . 8
       |
11 | | 1m1e0 10678 |
. . . . . . . 8
   |
12 | 10, 11 | syl6eq 2501 |
. . . . . . 7
     |
13 | 12 | fveq2d 5869 |
. . . . . 6
             |
14 | | fvex 5875 |
. . . . . 6
     |
15 | 13, 1, 14 | fvmpt 5948 |
. . . . 5
   ![[,] [,]](_icc.gif)            |
16 | 9, 15 | mp1i 13 |
. . . 4
             |
17 | 8, 6, 16 | pcocn 22048 |
. . 3
               |
18 | | cntop2 20257 |
. . . . . 6
     |
19 | | eqid 2451 |
. . . . . . 7
   |
20 | 19 | toptopon 19948 |
. . . . . 6

TopOn     |
21 | 18, 20 | sylib 200 |
. . . . 5
   TopOn     |
22 | | iiuni 21913 |
. . . . . . 7
  ![[,] [,]](_icc.gif)    |
23 | 22, 19 | cnf 20262 |
. . . . . 6
       ![[,] [,]](_icc.gif)       |
24 | | ffvelrn 6020 |
. . . . . 6
      ![[,] [,]](_icc.gif)       ![[,] [,]](_icc.gif)          |
25 | 23, 9, 24 | sylancl 668 |
. . . . 5
          |
26 | | pcorev.2 |
. . . . . 6
   ![[,] [,]](_icc.gif)          |
27 | 26 | pcoptcl 22052 |
. . . . 5
  TopOn                               |
28 | 21, 25, 27 | syl2anc 667 |
. . . 4
   
                     |
29 | 28 | simp1d 1020 |
. . 3
       |
30 | | pcorevlem.3 |
. . . 4
   ![[,] [,]](_icc.gif)     ![[,] [,]](_icc.gif)                                   |
31 | | eqid 2451 |
. . . . . 6
         |
32 | | eqid 2451 |
. . . . . 6
     ↾t   ![[,] [,]](_icc.gif)          ↾t   ![[,] [,]](_icc.gif)      |
33 | | eqid 2451 |
. . . . . 6
     ↾t     ![[,] [,]](_icc.gif)        ↾t     ![[,] [,]](_icc.gif)    |
34 | | dfii2 21914 |
. . . . . 6
     ↾t   ![[,] [,]](_icc.gif)    |
35 | | 0red 9644 |
. . . . . 6
     |
36 | | 1red 9658 |
. . . . . 6
     |
37 | | halfre 10828 |
. . . . . . . 8
   |
38 | | 0re 9643 |
. . . . . . . . 9
 |
39 | | halfgt0 10830 |
. . . . . . . . 9
   |
40 | 38, 37, 39 | ltleii 9757 |
. . . . . . . 8
   |
41 | | 1re 9642 |
. . . . . . . . 9
 |
42 | | halflt1 10831 |
. . . . . . . . 9
   |
43 | 37, 41, 42 | ltleii 9757 |
. . . . . . . 8
   |
44 | 38, 41 | elicc2i 11700 |
. . . . . . . 8
     ![[,] [,]](_icc.gif) 
    
     |
45 | 37, 40, 43, 44 | mpbir3an 1190 |
. . . . . . 7
    ![[,] [,]](_icc.gif)   |
46 | 45 | a1i 11 |
. . . . . 6
       ![[,] [,]](_icc.gif)    |
47 | | simprl 764 |
. . . . . . . . . . 11
         ![[,] [,]](_icc.gif)        |
48 | 47 | oveq2d 6306 |
. . . . . . . . . 10
         ![[,] [,]](_icc.gif)            |
49 | | 2cn 10680 |
. . . . . . . . . . 11
 |
50 | | 2ne0 10702 |
. . . . . . . . . . 11
 |
51 | 49, 50 | recidi 10338 |
. . . . . . . . . 10
     |
52 | 48, 51 | syl6eq 2501 |
. . . . . . . . 9
         ![[,] [,]](_icc.gif)        |
53 | 52 | oveq1d 6305 |
. . . . . . . . . . . 12
         ![[,] [,]](_icc.gif)            |
54 | 53, 11 | syl6eq 2501 |
. . . . . . . . . . 11
         ![[,] [,]](_icc.gif)          |
55 | 54 | oveq2d 6306 |
. . . . . . . . . 10
         ![[,] [,]](_icc.gif)              |
56 | | 1m0e1 10720 |
. . . . . . . . . 10
   |
57 | 55, 56 | syl6eq 2501 |
. . . . . . . . 9
         ![[,] [,]](_icc.gif)            |
58 | 52, 57 | eqtr4d 2488 |
. . . . . . . 8
         ![[,] [,]](_icc.gif)              |
59 | 58 | oveq2d 6306 |
. . . . . . 7
         ![[,] [,]](_icc.gif)                      |
60 | 59 | oveq2d 6306 |
. . . . . 6
         ![[,] [,]](_icc.gif)                          |
61 | | retopon 21784 |
. . . . . . . . 9
    TopOn   |
62 | | iccssre 11716 |
. . . . . . . . . 10
       ![[,] [,]](_icc.gif)      |
63 | 38, 37, 62 | mp2an 678 |
. . . . . . . . 9
  ![[,] [,]](_icc.gif)     |
64 | | resttopon 20177 |
. . . . . . . . 9
      TopOn    ![[,] [,]](_icc.gif)   
      ↾t   ![[,] [,]](_icc.gif)     TopOn   ![[,] [,]](_icc.gif)       |
65 | 61, 63, 64 | mp2an 678 |
. . . . . . . 8
     ↾t   ![[,] [,]](_icc.gif)     TopOn   ![[,] [,]](_icc.gif)      |
66 | 65 | a1i 11 |
. . . . . . 7
        ↾t   ![[,] [,]](_icc.gif)     TopOn   ![[,] [,]](_icc.gif)       |
67 | 66, 3 | cnmpt2nd 20684 |
. . . . . . . . 9
      ![[,] [,]](_icc.gif)       ![[,] [,]](_icc.gif)          ↾t   ![[,] [,]](_icc.gif)         |
68 | | oveq2 6298 |
. . . . . . . . 9
       |
69 | 66, 3, 67, 3, 5, 68 | cnmpt21 20686 |
. . . . . . . 8
      ![[,] [,]](_icc.gif)       ![[,] [,]](_icc.gif)            ↾t   ![[,] [,]](_icc.gif)         |
70 | 66, 3 | cnmpt1st 20683 |
. . . . . . . . 9
      ![[,] [,]](_icc.gif)       ![[,] [,]](_icc.gif)          ↾t   ![[,] [,]](_icc.gif)          
↾t   ![[,] [,]](_icc.gif)        |
71 | 32 | iihalf1cn 21960 |
. . . . . . . . . 10
   ![[,] [,]](_icc.gif)             ↾t   ![[,] [,]](_icc.gif)       |
72 | 71 | a1i 11 |
. . . . . . . . 9
      ![[,] [,]](_icc.gif)             ↾t   ![[,] [,]](_icc.gif)        |
73 | | oveq2 6298 |
. . . . . . . . 9
       |
74 | 66, 3, 70, 66, 72, 73 | cnmpt21 20686 |
. . . . . . . 8
      ![[,] [,]](_icc.gif)       ![[,] [,]](_icc.gif)            ↾t   ![[,] [,]](_icc.gif)         |
75 | | iimulcn 21966 |
. . . . . . . . 9
   ![[,] [,]](_icc.gif)     ![[,] [,]](_icc.gif)          |
76 | 75 | a1i 11 |
. . . . . . . 8
      ![[,] [,]](_icc.gif)     ![[,] [,]](_icc.gif)      
    |
77 | | oveq12 6299 |
. . . . . . . 8
   
             |
78 | 66, 3, 69, 74, 3, 3, 76, 77 | cnmpt22 20689 |
. . . . . . 7
      ![[,] [,]](_icc.gif)       ![[,] [,]](_icc.gif)                ↾t   ![[,] [,]](_icc.gif)         |
79 | | oveq2 6298 |
. . . . . . 7
                   |
80 | 66, 3, 78, 3, 5, 79 | cnmpt21 20686 |
. . . . . 6
      ![[,] [,]](_icc.gif)       ![[,] [,]](_icc.gif)                  ↾t   ![[,] [,]](_icc.gif)         |
81 | | iccssre 11716 |
. . . . . . . . . 10
   
     ![[,] [,]](_icc.gif) 
  |
82 | 37, 41, 81 | mp2an 678 |
. . . . . . . . 9
    ![[,] [,]](_icc.gif)   |
83 | | resttopon 20177 |
. . . . . . . . 9
      TopOn      ![[,] [,]](_icc.gif) 
      ↾t     ![[,] [,]](_icc.gif)   TopOn     ![[,] [,]](_icc.gif)     |
84 | 61, 82, 83 | mp2an 678 |
. . . . . . . 8
     ↾t     ![[,] [,]](_icc.gif)   TopOn     ![[,] [,]](_icc.gif)    |
85 | 84 | a1i 11 |
. . . . . . 7
        ↾t     ![[,] [,]](_icc.gif)   TopOn     ![[,] [,]](_icc.gif)     |
86 | 85, 3 | cnmpt2nd 20684 |
. . . . . . . . 9
        ![[,] [,]](_icc.gif)     ![[,] [,]](_icc.gif)          ↾t     ![[,] [,]](_icc.gif)       |
87 | 85, 3, 86, 3, 5, 68 | cnmpt21 20686 |
. . . . . . . 8
        ![[,] [,]](_icc.gif)     ![[,] [,]](_icc.gif)            ↾t     ![[,] [,]](_icc.gif)       |
88 | 85, 3 | cnmpt1st 20683 |
. . . . . . . . . 10
        ![[,] [,]](_icc.gif)     ![[,] [,]](_icc.gif)          ↾t     ![[,] [,]](_icc.gif)        
↾t     ![[,] [,]](_icc.gif)      |
89 | 33 | iihalf2cn 21962 |
. . . . . . . . . . 11
     ![[,] [,]](_icc.gif)             ↾t     ![[,] [,]](_icc.gif)     |
90 | 89 | a1i 11 |
. . . . . . . . . 10
        ![[,] [,]](_icc.gif)             ↾t     ![[,] [,]](_icc.gif)      |
91 | 73 | oveq1d 6305 |
. . . . . . . . . 10
           |
92 | 85, 3, 88, 85, 90, 91 | cnmpt21 20686 |
. . . . . . . . 9
        ![[,] [,]](_icc.gif)     ![[,] [,]](_icc.gif)              ↾t     ![[,] [,]](_icc.gif)       |
93 | | oveq2 6298 |
. . . . . . . . 9
               |
94 | 85, 3, 92, 3, 5, 93 | cnmpt21 20686 |
. . . . . . . 8
        ![[,] [,]](_icc.gif)     ![[,] [,]](_icc.gif)                ↾t     ![[,] [,]](_icc.gif)       |
95 | | oveq12 6299 |
. . . . . . . 8
   
                     |
96 | 85, 3, 87, 94, 3, 3, 76, 95 | cnmpt22 20689 |
. . . . . . 7
        ![[,] [,]](_icc.gif)     ![[,] [,]](_icc.gif)                    ↾t     ![[,] [,]](_icc.gif)       |
97 | | oveq2 6298 |
. . . . . . 7
                           |
98 | 85, 3, 96, 3, 5, 97 | cnmpt21 20686 |
. . . . . 6
        ![[,] [,]](_icc.gif)     ![[,] [,]](_icc.gif)                      ↾t     ![[,] [,]](_icc.gif)       |
99 | 31, 32, 33, 34, 35, 36, 46, 3, 60, 80, 98 | cnmpt2pc 21956 |
. . . . 5
      ![[,] [,]](_icc.gif)     ![[,] [,]](_icc.gif)                                    |
100 | 3, 3, 99, 6 | cnmpt21f 20687 |
. . . 4
      ![[,] [,]](_icc.gif)     ![[,] [,]](_icc.gif)      
                                 |
101 | 30, 100 | syl5eqel 2533 |
. . 3
     
   |
102 | | simpr 463 |
. . . . 5
   
  ![[,] [,]](_icc.gif)     ![[,] [,]](_icc.gif)    |
103 | | 0elunit 11750 |
. . . . 5
  ![[,] [,]](_icc.gif)   |
104 | | simpl 459 |
. . . . . . . . 9
 
   |
105 | 104 | breq1d 4412 |
. . . . . . . 8
 
         |
106 | | simpr 463 |
. . . . . . . . . . . 12
 
   |
107 | 106 | oveq2d 6306 |
. . . . . . . . . . 11
 
       |
108 | 107, 56 | syl6eq 2501 |
. . . . . . . . . 10
 
     |
109 | 104 | oveq2d 6306 |
. . . . . . . . . 10
 
       |
110 | 108, 109 | oveq12d 6308 |
. . . . . . . . 9
 
             |
111 | 110 | oveq2d 6306 |
. . . . . . . 8
 
                 |
112 | 109 | oveq1d 6305 |
. . . . . . . . . . 11
 
           |
113 | 112 | oveq2d 6306 |
. . . . . . . . . 10
 
               |
114 | 108, 113 | oveq12d 6308 |
. . . . . . . . 9
 
                     |
115 | 114 | oveq2d 6306 |
. . . . . . . 8
 
                         |
116 | 105, 111,
115 | ifbieq12d 3908 |
. . . . . . 7
 
                                                     |
117 | 116 | fveq2d 5869 |
. . . . . 6
 
                                    
                        |
118 | | fvex 5875 |
. . . . . 6
                            |
119 | 117, 30, 118 | ovmpt2a 6427 |
. . . . 5
    ![[,] [,]](_icc.gif) 
  ![[,] [,]](_icc.gif)           
                        |
120 | 102, 103,
119 | sylancl 668 |
. . . 4
   
  ![[,] [,]](_icc.gif)           
                        |
121 | | iftrue 3887 |
. . . . . . . 8
                                  |
122 | 121 | adantl 468 |
. . . . . . 7
       ![[,] [,]](_icc.gif)                                     |
123 | 122 | fveq2d 5869 |
. . . . . 6
       ![[,] [,]](_icc.gif)          
                                  |
124 | | elii1 21963 |
. . . . . . . 8
   ![[,] [,]](_icc.gif)   
   ![[,] [,]](_icc.gif) 
     |
125 | 8, 6 | pcoval1 22044 |
. . . . . . . . 9
   
  ![[,] [,]](_icc.gif)                         |
126 | | iihalf1 21959 |
. . . . . . . . . . 11
   ![[,] [,]](_icc.gif)        ![[,] [,]](_icc.gif)    |
127 | 126 | adantl 468 |
. . . . . . . . . 10
   
  ![[,] [,]](_icc.gif)         ![[,] [,]](_icc.gif)    |
128 | | oveq2 6298 |
. . . . . . . . . . . . 13
           |
129 | 128 | fveq2d 5869 |
. . . . . . . . . . . 12
                   |
130 | | fvex 5875 |
. . . . . . . . . . . 12
         |
131 | 129, 1, 130 | fvmpt 5948 |
. . . . . . . . . . 11
     ![[,] [,]](_icc.gif)                  |
132 | | unitssre 11779 |
. . . . . . . . . . . . . . . 16
  ![[,] [,]](_icc.gif)   |
133 | 132 | sseli 3428 |
. . . . . . . . . . . . . . 15
     ![[,] [,]](_icc.gif)      |
134 | 133 | recnd 9669 |
. . . . . . . . . . . . . 14
     ![[,] [,]](_icc.gif)      |
135 | 134 | mulid2d 9661 |
. . . . . . . . . . . . 13
     ![[,] [,]](_icc.gif)          |
136 | 135 | oveq2d 6306 |
. . . . . . . . . . . 12
     ![[,] [,]](_icc.gif)              |
137 | 136 | fveq2d 5869 |
. . . . . . . . . . 11
     ![[,] [,]](_icc.gif)                      |
138 | 131, 137 | eqtr4d 2488 |
. . . . . . . . . 10
     ![[,] [,]](_icc.gif)                    |
139 | 127, 138 | syl 17 |
. . . . . . . . 9
   
  ![[,] [,]](_icc.gif)                       |
140 | 125, 139 | eqtrd 2485 |
. . . . . . . 8
   
  ![[,] [,]](_icc.gif)                             |
141 | 124, 140 | sylan2br 479 |
. . . . . . 7
       ![[,] [,]](_icc.gif)                              |
142 | 141 | anassrs 654 |
. . . . . 6
       ![[,] [,]](_icc.gif)                              |
143 | 123, 142 | eqtr4d 2488 |
. . . . 5
       ![[,] [,]](_icc.gif)          
                                    |
144 | | iffalse 3890 |
. . . . . . . 8

                                     |
145 | 144 | adantl 468 |
. . . . . . 7
       ![[,] [,]](_icc.gif)                                         |
146 | 145 | fveq2d 5869 |
. . . . . 6
       ![[,] [,]](_icc.gif)          
                                      |
147 | | elii2 21964 |
. . . . . . . 8
    ![[,] [,]](_icc.gif) 
       ![[,] [,]](_icc.gif)    |
148 | 8, 6, 16 | pcoval2 22047 |
. . . . . . . . 9
   
    ![[,] [,]](_icc.gif)                         |
149 | | iihalf2 21961 |
. . . . . . . . . . . 12
     ![[,] [,]](_icc.gif)        ![[,] [,]](_icc.gif)    |
150 | 149 | adantl 468 |
. . . . . . . . . . 11
   
    ![[,] [,]](_icc.gif)         ![[,] [,]](_icc.gif)    |
151 | | ax-1cn 9597 |
. . . . . . . . . . . . . . 15
 |
152 | 132 | sseli 3428 |
. . . . . . . . . . . . . . . 16
       ![[,] [,]](_icc.gif)        |
153 | 152 | recnd 9669 |
. . . . . . . . . . . . . . 15
       ![[,] [,]](_icc.gif)        |
154 | | subcl 9874 |
. . . . . . . . . . . . . . 15
               |
155 | 151, 153,
154 | sylancr 669 |
. . . . . . . . . . . . . 14
       ![[,] [,]](_icc.gif)          |
156 | 155 | mulid2d 9661 |
. . . . . . . . . . . . 13
       ![[,] [,]](_icc.gif)                  |
157 | 156 | oveq2d 6306 |
. . . . . . . . . . . 12
       ![[,] [,]](_icc.gif)                      |
158 | | nncan 9903 |
. . . . . . . . . . . . 13
                     |
159 | 151, 153,
158 | sylancr 669 |
. . . . . . . . . . . 12
       ![[,] [,]](_icc.gif)                |
160 | 157, 159 | eqtr2d 2486 |
. . . . . . . . . . 11
       ![[,] [,]](_icc.gif)                  |
161 | 150, 160 | syl 17 |
. . . . . . . . . 10
   
    ![[,] [,]](_icc.gif)                   |
162 | 161 | fveq2d 5869 |
. . . . . . . . 9
   
    ![[,] [,]](_icc.gif)                           |
163 | 148, 162 | eqtrd 2485 |
. . . . . . . 8
   
    ![[,] [,]](_icc.gif)                               |
164 | 147, 163 | sylan2 477 |
. . . . . . 7
       ![[,] [,]](_icc.gif)                                  |
165 | 164 | anassrs 654 |
. . . . . 6
       ![[,] [,]](_icc.gif)                                  |
166 | 146, 165 | eqtr4d 2488 |
. . . . 5
       ![[,] [,]](_icc.gif)          
                                    |
167 | 143, 166 | pm2.61dan 800 |
. . . 4
   
  ![[,] [,]](_icc.gif)                                            |
168 | 120, 167 | eqtrd 2485 |
. . 3
   
  ![[,] [,]](_icc.gif)                     |
169 | 132 | sseli 3428 |
. . . . . . . . . . . . 13
   ![[,] [,]](_icc.gif)    |
170 | 169 | recnd 9669 |
. . . . . . . . . . . 12
   ![[,] [,]](_icc.gif)    |
171 | | mulcl 9623 |
. . . . . . . . . . . 12
 
     |
172 | 49, 170, 171 | sylancr 669 |
. . . . . . . . . . 11
   ![[,] [,]](_icc.gif)      |
173 | 172 | adantl 468 |
. . . . . . . . . 10
   
  ![[,] [,]](_icc.gif)       |
174 | 173 | mul02d 9831 |
. . . . . . . . 9
   
  ![[,] [,]](_icc.gif)         |
175 | 174 | oveq2d 6306 |
. . . . . . . 8
   
  ![[,] [,]](_icc.gif)             |
176 | 175, 56 | syl6eq 2501 |
. . . . . . 7
   
  ![[,] [,]](_icc.gif)           |
177 | | subcl 9874 |
. . . . . . . . . . . 12
   
       |
178 | 173, 151,
177 | sylancl 668 |
. . . . . . . . . . 11
   
  ![[,] [,]](_icc.gif)         |
179 | 151, 178,
154 | sylancr 669 |
. . . . . . . . . 10
   
  ![[,] [,]](_icc.gif)           |
180 | 179 | mul02d 9831 |
. . . . . . . . 9
   
  ![[,] [,]](_icc.gif)             |
181 | 180 | oveq2d 6306 |
. . . . . . . 8
   
  ![[,] [,]](_icc.gif)                 |
182 | 181, 56 | syl6eq 2501 |
. . . . . . 7
   
  ![[,] [,]](_icc.gif)               |
183 | 176, 182 | ifeq12d 3901 |
. . . . . 6
   
  ![[,] [,]](_icc.gif)                                   |
184 | | ifid 3918 |
. . . . . 6
 
      |
185 | 183, 184 | syl6eq 2501 |
. . . . 5
   
  ![[,] [,]](_icc.gif)                            |
186 | 185 | fveq2d 5869 |
. . . 4
   
  ![[,] [,]](_icc.gif)                                    |
187 | | simpl 459 |
. . . . . . . . 9
 
   |
188 | 187 | breq1d 4412 |
. . . . . . . 8
 
         |
189 | | simpr 463 |
. . . . . . . . . . . 12
 
   |
190 | 189 | oveq2d 6306 |
. . . . . . . . . . 11
 
       |
191 | 190, 11 | syl6eq 2501 |
. . . . . . . . . 10
 
     |
192 | 187 | oveq2d 6306 |
. . . . . . . . . 10
 
       |
193 | 191, 192 | oveq12d 6308 |
. . . . . . . . 9
 
             |
194 | 193 | oveq2d 6306 |
. . . . . . . 8
 
                 |
195 | 192 | oveq1d 6305 |
. . . . . . . . . . 11
 
           |
196 | 195 | oveq2d 6306 |
. . . . . . . . . 10
 
               |
197 | 191, 196 | oveq12d 6308 |
. . . . . . . . 9
 
                     |
198 | 197 | oveq2d 6306 |
. . . . . . . 8
 
                         |
199 | 188, 194,
198 | ifbieq12d 3908 |
. . . . . . 7
 
                                                     |
200 | 199 | fveq2d 5869 |
. . . . . 6
 
                                    
                        |
201 | | fvex 5875 |
. . . . . 6
                            |
202 | 200, 30, 201 | ovmpt2a 6427 |
. . . . 5
    ![[,] [,]](_icc.gif) 
  ![[,] [,]](_icc.gif)           
                        |
203 | 102, 9, 202 | sylancl 668 |
. . . 4
   
  ![[,] [,]](_icc.gif)           
                        |
204 | 26 | fveq1i 5866 |
. . . . 5
        ![[,] [,]](_icc.gif)             |
205 | | fvex 5875 |
. . . . . . 7
     |
206 | 205 | fvconst2 6120 |
. . . . . 6
   ![[,] [,]](_icc.gif)      ![[,] [,]](_icc.gif)                  |
207 | 206 | adantl 468 |
. . . . 5
   
  ![[,] [,]](_icc.gif)       ![[,] [,]](_icc.gif)                  |
208 | 204, 207 | syl5eq 2497 |
. . . 4
   
  ![[,] [,]](_icc.gif)             |
209 | 186, 203,
208 | 3eqtr4d 2495 |
. . 3
   
  ![[,] [,]](_icc.gif)             |
210 | | simpl 459 |
. . . . . . . . . . 11
     |
211 | 210, 40 | syl6eqbr 4440 |
. . . . . . . . . 10
       |
212 | 211 | iftrued 3889 |
. . . . . . . . 9
                                        |
213 | | simpr 463 |
. . . . . . . . . . . 12
     |
214 | 213 | oveq2d 6306 |
. . . . . . . . . . 11
         |
215 | 210 | oveq2d 6306 |
. . . . . . . . . . . 12
         |
216 | | 2t0e0 10765 |
. . . . . . . . . . . 12
   |
217 | 215, 216 | syl6eq 2501 |
. . . . . . . . . . 11
       |
218 | 214, 217 | oveq12d 6308 |
. . . . . . . . . 10
               |
219 | 218 | oveq2d 6306 |
. . . . . . . . 9
                   |
220 | 212, 219 | eqtrd 2485 |
. . . . . . . 8
                                      |
221 | 220 | fveq2d 5869 |
. . . . . . 7
                                              |
222 | | fvex 5875 |
. . . . . . 7
           |
223 | 221, 30, 222 | ovmpt2a 6427 |
. . . . . 6
    ![[,] [,]](_icc.gif) 
  ![[,] [,]](_icc.gif)                   |
224 | 103, 223 | mpan 676 |
. . . . 5
   ![[,] [,]](_icc.gif)                  |
225 | | subcl 9874 |
. . . . . . . . . 10
 
     |
226 | 151, 170,
225 | sylancr 669 |
. . . . . . . . 9
   ![[,] [,]](_icc.gif)      |
227 | 226 | mul01d 9832 |
. . . . . . . 8
   ![[,] [,]](_icc.gif)        |
228 | 227 | oveq2d 6306 |
. . . . . . 7
   ![[,] [,]](_icc.gif)            |
229 | 228, 56 | syl6eq 2501 |
. . . . . 6
   ![[,] [,]](_icc.gif)          |
230 | 229 | fveq2d 5869 |
. . . . 5
   ![[,] [,]](_icc.gif)                  |
231 | 224, 230 | eqtrd 2485 |
. . . 4
   ![[,] [,]](_icc.gif)            |
232 | 8, 6 | pco0 22045 |
. . . . 5
                     |
233 | | oveq2 6298 |
. . . . . . . . 9
       |
234 | 233, 56 | syl6eq 2501 |
. . . . . . . 8
     |
235 | 234 | fveq2d 5869 |
. . . . . . 7
             |
236 | 235, 1, 205 | fvmpt 5948 |
. . . . . 6
   ![[,] [,]](_icc.gif)            |
237 | 103, 236 | ax-mp 5 |
. . . . 5
         |
238 | 232, 237 | syl6req 2502 |
. . . 4
                     |
239 | 231, 238 | sylan9eqr 2507 |
. . 3
   
  ![[,] [,]](_icc.gif)                     |
240 | 37, 41 | ltnlei 9755 |
. . . . . . . . . . . 12
  
    |
241 | 42, 240 | mpbi 212 |
. . . . . . . . . . 11
   |
242 | | simpl 459 |
. . . . . . . . . . . 12
     |
243 | 242 | breq1d 4412 |
. . . . . . . . . . 11
           |
244 | 241, 243 | mtbiri 305 |
. . . . . . . . . 10
  
    |
245 | 244 | iffalsed 3892 |
. . . . . . . . 9
                                            |
246 | | simpr 463 |
. . . . . . . . . . . 12
     |
247 | 246 | oveq2d 6306 |
. . . . . . . . . . 11
         |
248 | 242 | oveq2d 6306 |
. . . . . . . . . . . . . . . 16
         |
249 | | 2t1e2 10758 |
. . . . . . . . . . . . . . . 16
   |
250 | 248, 249 | syl6eq 2501 |
. . . . . . . . . . . . . . 15
       |
251 | 250 | oveq1d 6305 |
. . . . . . . . . . . . . 14
           |
252 | | 2m1e1 10724 |
. . . . . . . . . . . . . 14
   |
253 | 251, 252 | syl6eq 2501 |
. . . . . . . . . . . . 13
         |
254 | 253 | oveq2d 6306 |
. . . . . . . . . . . 12
             |
255 | 254, 11 | syl6eq 2501 |
. . . . . . . . . . 11
           |
256 | 247, 255 | oveq12d 6308 |
. . . . . . . . . 10
                   |
257 | 256 | oveq2d 6306 |
. . . . . . . . 9
                       |
258 | 245, 257 | eqtrd 2485 |
. . . . . . . 8
                                      |
259 | 258 | fveq2d 5869 |
. . . . . . 7
                                              |
260 | 259, 30, 222 | ovmpt2a 6427 |
. . . . . 6
    ![[,] [,]](_icc.gif) 
  ![[,] [,]](_icc.gif)                   |
261 | 9, 260 | mpan 676 |
. . . . 5
   ![[,] [,]](_icc.gif)                  |
262 | 261, 230 | eqtrd 2485 |
. . . 4
   ![[,] [,]](_icc.gif)            |
263 | 8, 6 | pco1 22046 |
. . . . 5
                     |
264 | 263 | eqcomd 2457 |
. . . 4
                     |
265 | 262, 264 | sylan9eqr 2507 |
. . 3
   
  ![[,] [,]](_icc.gif)                     |
266 | 17, 29, 101, 168, 209, 239, 265 | isphtpy2d 22018 |
. 2
                     |
267 | | ne0i 3737 |
. . . 4
                
                  |
268 | 266, 267 | syl 17 |
. . 3
                     |
269 | | isphtpc 22025 |
. . 3
         
             


                   |
270 | 17, 29, 268, 269 | syl3anbrc 1192 |
. 2
           
     |
271 | 266, 270 | jca 535 |
1
   
                        
      |