Step | Hyp | Ref
| Expression |
1 | | iftrue 3878 |
. . . . . . . . . . 11
    
               |
2 | 1 | fveq2d 5883 |
. . . . . . . . . 10
                       
                                    |
3 | 2 | adantl 473 |
. . . . . . . . 9
     ![[,] [,]](_icc.gif)                          
                                    |
4 | | 2cn 10702 |
. . . . . . . . . . . . 13
 |
5 | | 0re 9661 |
. . . . . . . . . . . . . . . . 17
 |
6 | | 1re 9660 |
. . . . . . . . . . . . . . . . 17
 |
7 | 5, 6 | elicc2i 11725 |
. . . . . . . . . . . . . . . 16
   ![[,] [,]](_icc.gif) 
    |
8 | 7 | simp1bi 1045 |
. . . . . . . . . . . . . . 15
   ![[,] [,]](_icc.gif)    |
9 | 8 | adantr 472 |
. . . . . . . . . . . . . 14
    ![[,] [,]](_icc.gif)    
  |
10 | 9 | recnd 9687 |
. . . . . . . . . . . . 13
    ![[,] [,]](_icc.gif)    
  |
11 | | mulcom 9643 |
. . . . . . . . . . . . 13
 
       |
12 | 4, 10, 11 | sylancr 676 |
. . . . . . . . . . . 12
    ![[,] [,]](_icc.gif)           |
13 | 7 | simp2bi 1046 |
. . . . . . . . . . . . . . 15
   ![[,] [,]](_icc.gif)    |
14 | 13 | adantr 472 |
. . . . . . . . . . . . . 14
    ![[,] [,]](_icc.gif)    
  |
15 | | simpr 468 |
. . . . . . . . . . . . . 14
    ![[,] [,]](_icc.gif)         |
16 | | 4nn 10792 |
. . . . . . . . . . . . . . . 16
 |
17 | | nnrecre 10668 |
. . . . . . . . . . . . . . . 16
     |
18 | 16, 17 | ax-mp 5 |
. . . . . . . . . . . . . . 15
   |
19 | 5, 18 | elicc2i 11725 |
. . . . . . . . . . . . . 14
   ![[,] [,]](_icc.gif)   
      |
20 | 9, 14, 15, 19 | syl3anbrc 1214 |
. . . . . . . . . . . . 13
    ![[,] [,]](_icc.gif)    
  ![[,] [,]](_icc.gif)      |
21 | | 2rp 11330 |
. . . . . . . . . . . . . 14
 |
22 | 4 | mul02i 9840 |
. . . . . . . . . . . . . 14
   |
23 | 18 | recni 9673 |
. . . . . . . . . . . . . . 15
   |
24 | 23 | 2timesi 10753 |
. . . . . . . . . . . . . . . 16
           |
25 | | 2ne0 10724 |
. . . . . . . . . . . . . . . . . . . 20
 |
26 | | recdiv2 10342 |
. . . . . . . . . . . . . . . . . . . 20
                 |
27 | 4, 25, 4, 25, 26 | mp4an 687 |
. . . . . . . . . . . . . . . . . . 19
         |
28 | | 2t2e4 10782 |
. . . . . . . . . . . . . . . . . . . 20
   |
29 | 28 | oveq2i 6319 |
. . . . . . . . . . . . . . . . . . 19
       |
30 | 27, 29 | eqtri 2493 |
. . . . . . . . . . . . . . . . . 18
       |
31 | 30, 30 | oveq12i 6320 |
. . . . . . . . . . . . . . . . 17
                 |
32 | | halfcn 10852 |
. . . . . . . . . . . . . . . . . 18
   |
33 | | 2halves 10864 |
. . . . . . . . . . . . . . . . . 18
                 |
34 | 32, 33 | ax-mp 5 |
. . . . . . . . . . . . . . . . 17
             |
35 | 31, 34 | eqtr3i 2495 |
. . . . . . . . . . . . . . . 16
         |
36 | 24, 35 | eqtri 2493 |
. . . . . . . . . . . . . . 15
       |
37 | 4, 23, 36 | mulcomli 9668 |
. . . . . . . . . . . . . 14
       |
38 | 5, 18, 21, 22, 37 | iccdili 11797 |
. . . . . . . . . . . . 13
   ![[,] [,]](_icc.gif)        ![[,] [,]](_icc.gif)      |
39 | 20, 38 | syl 17 |
. . . . . . . . . . . 12
    ![[,] [,]](_icc.gif)         ![[,] [,]](_icc.gif)      |
40 | 12, 39 | eqeltrd 2549 |
. . . . . . . . . . 11
    ![[,] [,]](_icc.gif)         ![[,] [,]](_icc.gif)      |
41 | | pcoass.2 |
. . . . . . . . . . . . 13
     |
42 | | pcoass.3 |
. . . . . . . . . . . . . 14
     |
43 | | pcoass.4 |
. . . . . . . . . . . . . 14
     |
44 | | pcoass.6 |
. . . . . . . . . . . . . 14
           |
45 | 42, 43, 44 | pcocn 22126 |
. . . . . . . . . . . . 13
             |
46 | 41, 45 | pcoval1 22122 |
. . . . . . . . . . . 12
 
    ![[,] [,]](_icc.gif)                                     |
47 | 41, 42 | pcoval1 22122 |
. . . . . . . . . . . 12
 
    ![[,] [,]](_icc.gif)                             |
48 | 46, 47 | eqtr4d 2508 |
. . . . . . . . . . 11
 
    ![[,] [,]](_icc.gif)                                           |
49 | 40, 48 | sylan2 482 |
. . . . . . . . . 10
 
   ![[,] [,]](_icc.gif) 
                                          |
50 | 49 | anassrs 660 |
. . . . . . . . 9
     ![[,] [,]](_icc.gif)                                            |
51 | 3, 50 | eqtrd 2505 |
. . . . . . . 8
     ![[,] [,]](_icc.gif)                          
                            |
52 | 51 | adantlr 729 |
. . . . . . 7
   
  ![[,] [,]](_icc.gif)                             
                            |
53 | | simplll 776 |
. . . . . . . . . 10
   
  ![[,] [,]](_icc.gif)           |
54 | 8 | ad2antlr 741 |
. . . . . . . . . . . . 13
     ![[,] [,]](_icc.gif)        |
55 | 54 | adantr 472 |
. . . . . . . . . . . 12
   
  ![[,] [,]](_icc.gif)           |
56 | | letric 9752 |
. . . . . . . . . . . . . 14
             |
57 | 54, 18, 56 | sylancl 675 |
. . . . . . . . . . . . 13
     ![[,] [,]](_icc.gif)      
   
   |
58 | 57 | orcanai 927 |
. . . . . . . . . . . 12
   
  ![[,] [,]](_icc.gif)             |
59 | | simplr 770 |
. . . . . . . . . . . 12
   
  ![[,] [,]](_icc.gif)             |
60 | | halfre 10851 |
. . . . . . . . . . . . 13
   |
61 | 18, 60 | elicc2i 11725 |
. . . . . . . . . . . 12
     ![[,] [,]](_icc.gif)   
        |
62 | 55, 58, 59, 61 | syl3anbrc 1214 |
. . . . . . . . . . 11
   
  ![[,] [,]](_icc.gif)             ![[,] [,]](_icc.gif)      |
63 | 61 | simp1bi 1045 |
. . . . . . . . . . . . 13
     ![[,] [,]](_icc.gif)      |
64 | | readdcl 9640 |
. . . . . . . . . . . . 13
           |
65 | 63, 18, 64 | sylancl 675 |
. . . . . . . . . . . 12
     ![[,] [,]](_icc.gif)          |
66 | 18 | a1i 11 |
. . . . . . . . . . . . . 14
     ![[,] [,]](_icc.gif)        |
67 | 61 | simp2bi 1046 |
. . . . . . . . . . . . . 14
     ![[,] [,]](_icc.gif)        |
68 | 66, 63, 66, 67 | leadd1dd 10248 |
. . . . . . . . . . . . 13
     ![[,] [,]](_icc.gif)                |
69 | 35, 68 | syl5eqbrr 4430 |
. . . . . . . . . . . 12
     ![[,] [,]](_icc.gif)            |
70 | 60 | a1i 11 |
. . . . . . . . . . . . . 14
     ![[,] [,]](_icc.gif)        |
71 | 61 | simp3bi 1047 |
. . . . . . . . . . . . . 14
     ![[,] [,]](_icc.gif)        |
72 | | 2lt4 10803 |
. . . . . . . . . . . . . . . . 17
 |
73 | | 2re 10701 |
. . . . . . . . . . . . . . . . . 18
 |
74 | | 4re 10708 |
. . . . . . . . . . . . . . . . . 18
 |
75 | | 2pos 10723 |
. . . . . . . . . . . . . . . . . 18
 |
76 | | 4pos 10727 |
. . . . . . . . . . . . . . . . . 18
 |
77 | 73, 74, 75, 76 | ltrecii 10545 |
. . . . . . . . . . . . . . . . 17

      |
78 | 72, 77 | mpbi 213 |
. . . . . . . . . . . . . . . 16
     |
79 | 18, 60, 78 | ltleii 9775 |
. . . . . . . . . . . . . . 15
     |
80 | 79 | a1i 11 |
. . . . . . . . . . . . . 14
     ![[,] [,]](_icc.gif)          |
81 | 63, 66, 70, 70, 71, 80 | le2addd 10253 |
. . . . . . . . . . . . 13
     ![[,] [,]](_icc.gif)                |
82 | | ax-1cn 9615 |
. . . . . . . . . . . . . 14
 |
83 | | 2halves 10864 |
. . . . . . . . . . . . . 14
         |
84 | 82, 83 | ax-mp 5 |
. . . . . . . . . . . . 13
       |
85 | 81, 84 | syl6breq 4435 |
. . . . . . . . . . . 12
     ![[,] [,]](_icc.gif)          |
86 | 60, 6 | elicc2i 11725 |
. . . . . . . . . . . 12
         ![[,] [,]](_icc.gif) 
                  |
87 | 65, 69, 85, 86 | syl3anbrc 1214 |
. . . . . . . . . . 11
     ![[,] [,]](_icc.gif)            ![[,] [,]](_icc.gif)    |
88 | 62, 87 | syl 17 |
. . . . . . . . . 10
   
  ![[,] [,]](_icc.gif)                 ![[,] [,]](_icc.gif)    |
89 | | pcoass.5 |
. . . . . . . . . . . 12
           |
90 | 42, 43 | pco0 22123 |
. . . . . . . . . . . 12
                   |
91 | 89, 90 | eqtr4d 2508 |
. . . . . . . . . . 11
                   |
92 | 41, 45, 91 | pcoval2 22125 |
. . . . . . . . . 10
 
        ![[,] [,]](_icc.gif)                                                 |
93 | 53, 88, 92 | syl2anc 673 |
. . . . . . . . 9
   
  ![[,] [,]](_icc.gif)                                                       |
94 | 84 | oveq2i 6319 |
. . . . . . . . . . . 12
                       |
95 | | 2cnd 10704 |
. . . . . . . . . . . . . . 15
   
  ![[,] [,]](_icc.gif)           |
96 | 55 | recnd 9687 |
. . . . . . . . . . . . . . 15
   
  ![[,] [,]](_icc.gif)           |
97 | 23 | a1i 11 |
. . . . . . . . . . . . . . 15
   
  ![[,] [,]](_icc.gif)             |
98 | 95, 96, 97 | adddid 9685 |
. . . . . . . . . . . . . 14
   
  ![[,] [,]](_icc.gif)                         |
99 | 36 | oveq2i 6319 |
. . . . . . . . . . . . . 14
               |
100 | 98, 99 | syl6eq 2521 |
. . . . . . . . . . . . 13
   
  ![[,] [,]](_icc.gif)                       |
101 | 100 | oveq1d 6323 |
. . . . . . . . . . . 12
   
  ![[,] [,]](_icc.gif)                                       |
102 | 94, 101 | syl5eqr 2519 |
. . . . . . . . . . 11
   
  ![[,] [,]](_icc.gif)                                 |
103 | | remulcl 9642 |
. . . . . . . . . . . . . 14
 
     |
104 | 73, 55, 103 | sylancr 676 |
. . . . . . . . . . . . 13
   
  ![[,] [,]](_icc.gif)             |
105 | 104 | recnd 9687 |
. . . . . . . . . . . 12
   
  ![[,] [,]](_icc.gif)             |
106 | 32 | a1i 11 |
. . . . . . . . . . . 12
   
  ![[,] [,]](_icc.gif)             |
107 | 105, 106,
106 | pnpcan2d 10043 |
. . . . . . . . . . 11
   
  ![[,] [,]](_icc.gif)                               |
108 | 102, 107 | eqtrd 2505 |
. . . . . . . . . 10
   
  ![[,] [,]](_icc.gif)                         |
109 | 108 | fveq2d 5883 |
. . . . . . . . 9
   
  ![[,] [,]](_icc.gif)                                                 |
110 | 4, 96, 11 | sylancr 676 |
. . . . . . . . . . . . 13
   
  ![[,] [,]](_icc.gif)               |
111 | 82, 4, 25 | divcan1i 10373 |
. . . . . . . . . . . . . . 15
     |
112 | 18, 60, 21, 37, 111 | iccdili 11797 |
. . . . . . . . . . . . . 14
     ![[,] [,]](_icc.gif)          ![[,] [,]](_icc.gif)    |
113 | 62, 112 | syl 17 |
. . . . . . . . . . . . 13
   
  ![[,] [,]](_icc.gif)               ![[,] [,]](_icc.gif)    |
114 | 110, 113 | eqeltrd 2549 |
. . . . . . . . . . . 12
   
  ![[,] [,]](_icc.gif)               ![[,] [,]](_icc.gif)    |
115 | 32 | subidi 9965 |
. . . . . . . . . . . . 13
       |
116 | | 1mhlfehlf 10855 |
. . . . . . . . . . . . 13
       |
117 | 60, 6, 60, 115, 116 | iccshftli 11795 |
. . . . . . . . . . . 12
       ![[,] [,]](_icc.gif)          ![[,] [,]](_icc.gif)      |
118 | 114, 117 | syl 17 |
. . . . . . . . . . 11
   
  ![[,] [,]](_icc.gif)                 ![[,] [,]](_icc.gif)      |
119 | 42, 43 | pcoval1 22122 |
. . . . . . . . . . 11
 
        ![[,] [,]](_icc.gif)                                     |
120 | 53, 118, 119 | syl2anc 673 |
. . . . . . . . . 10
   
  ![[,] [,]](_icc.gif)                                         |
121 | 95, 105, 106 | subdid 10095 |
. . . . . . . . . . . 12
   
  ![[,] [,]](_icc.gif)                             |
122 | 4, 25 | recidi 10360 |
. . . . . . . . . . . . 13
     |
123 | 122 | oveq2i 6319 |
. . . . . . . . . . . 12
                 |
124 | 121, 123 | syl6eq 2521 |
. . . . . . . . . . 11
   
  ![[,] [,]](_icc.gif)                         |
125 | 124 | fveq2d 5883 |
. . . . . . . . . 10
   
  ![[,] [,]](_icc.gif)                                 |
126 | 120, 125 | eqtrd 2505 |
. . . . . . . . 9
   
  ![[,] [,]](_icc.gif)                                       |
127 | 93, 109, 126 | 3eqtrd 2509 |
. . . . . . . 8
   
  ![[,] [,]](_icc.gif)                                             |
128 | | iffalse 3881 |
. . . . . . . . . 10

                     |
129 | 128 | fveq2d 5883 |
. . . . . . . . 9

                      
                                      |
130 | 129 | adantl 473 |
. . . . . . . 8
   
  ![[,] [,]](_icc.gif)                             
                                      |
131 | 41, 42, 89 | pcoval2 22125 |
. . . . . . . . 9
 
      ![[,] [,]](_icc.gif)                             |
132 | 53, 114, 131 | syl2anc 673 |
. . . . . . . 8
   
  ![[,] [,]](_icc.gif)                                   |
133 | 127, 130,
132 | 3eqtr4d 2515 |
. . . . . . 7
   
  ![[,] [,]](_icc.gif)                             
                            |
134 | 52, 133 | pm2.61dan 808 |
. . . . . 6
     ![[,] [,]](_icc.gif)                          
                            |
135 | | iftrue 3878 |
. . . . . . . 8
    
                         
             |
136 | 135 | fveq2d 5883 |
. . . . . . 7
                       
                                             
              |
137 | 136 | adantl 473 |
. . . . . 6
     ![[,] [,]](_icc.gif)                          
                                             
              |
138 | | iftrue 3878 |
. . . . . . 7
    
                                           |
139 | 138 | adantl 473 |
. . . . . 6
     ![[,] [,]](_icc.gif)       
                                           |
140 | 134, 137,
139 | 3eqtr4d 2515 |
. . . . 5
     ![[,] [,]](_icc.gif)                          
                                                        |
141 | | elii2 22042 |
. . . . . . . 8
    ![[,] [,]](_icc.gif) 
       ![[,] [,]](_icc.gif)    |
142 | | halfgt0 10853 |
. . . . . . . . . . . . . . 15
   |
143 | 5, 60, 142 | ltleii 9775 |
. . . . . . . . . . . . . 14
   |
144 | | halflt1 10854 |
. . . . . . . . . . . . . . 15
   |
145 | 60, 6, 144 | ltleii 9775 |
. . . . . . . . . . . . . 14
   |
146 | 5, 6 | elicc2i 11725 |
. . . . . . . . . . . . . 14
     ![[,] [,]](_icc.gif) 
    
     |
147 | 60, 143, 145, 146 | mpbir3an 1212 |
. . . . . . . . . . . . 13
    ![[,] [,]](_icc.gif)   |
148 | | 1elunit 11777 |
. . . . . . . . . . . . 13
  ![[,] [,]](_icc.gif)   |
149 | | iccss2 11730 |
. . . . . . . . . . . . 13
      ![[,] [,]](_icc.gif) 
  ![[,] [,]](_icc.gif)       ![[,] [,]](_icc.gif)    ![[,] [,]](_icc.gif)    |
150 | 147, 148,
149 | mp2an 686 |
. . . . . . . . . . . 12
    ![[,] [,]](_icc.gif)    ![[,] [,]](_icc.gif)   |
151 | 150 | sseli 3414 |
. . . . . . . . . . 11
     ![[,] [,]](_icc.gif)    ![[,] [,]](_icc.gif)    |
152 | 4, 25 | div0i 10363 |
. . . . . . . . . . . 12
   |
153 | | eqid 2471 |
. . . . . . . . . . . 12
     |
154 | 5, 6, 21, 152, 153 | icccntri 11799 |
. . . . . . . . . . 11
   ![[,] [,]](_icc.gif)      ![[,] [,]](_icc.gif)      |
155 | 32 | addid2i 9839 |
. . . . . . . . . . . 12
       |
156 | 5, 60, 60, 155, 84 | iccshftri 11793 |
. . . . . . . . . . 11
     ![[,] [,]](_icc.gif)              ![[,] [,]](_icc.gif)    |
157 | 151, 154,
156 | 3syl 18 |
. . . . . . . . . 10
     ![[,] [,]](_icc.gif)            ![[,] [,]](_icc.gif)    |
158 | 41, 45, 91 | pcoval2 22125 |
. . . . . . . . . 10
 
          ![[,] [,]](_icc.gif)                                                     |
159 | 157, 158 | sylan2 482 |
. . . . . . . . 9
 
    ![[,] [,]](_icc.gif)                                                     |
160 | 60, 6 | elicc2i 11725 |
. . . . . . . . . . . . . . . . . 18
     ![[,] [,]](_icc.gif) 
      |
161 | 160 | simp1bi 1045 |
. . . . . . . . . . . . . . . . 17
     ![[,] [,]](_icc.gif)    |
162 | 161 | recnd 9687 |
. . . . . . . . . . . . . . . 16
     ![[,] [,]](_icc.gif)    |
163 | 82 | a1i 11 |
. . . . . . . . . . . . . . . 16
     ![[,] [,]](_icc.gif)    |
164 | | 2cnd 10704 |
. . . . . . . . . . . . . . . 16
     ![[,] [,]](_icc.gif)    |
165 | 25 | a1i 11 |
. . . . . . . . . . . . . . . 16
     ![[,] [,]](_icc.gif)    |
166 | 162, 163,
164, 165 | divdird 10443 |
. . . . . . . . . . . . . . 15
     ![[,] [,]](_icc.gif)              |
167 | 166 | oveq2d 6324 |
. . . . . . . . . . . . . 14
     ![[,] [,]](_icc.gif)                  |
168 | | peano2cn 9823 |
. . . . . . . . . . . . . . . 16
     |
169 | 162, 168 | syl 17 |
. . . . . . . . . . . . . . 15
     ![[,] [,]](_icc.gif)      |
170 | 169, 164,
165 | divcan2d 10407 |
. . . . . . . . . . . . . 14
     ![[,] [,]](_icc.gif)            |
171 | 167, 170 | eqtr3d 2507 |
. . . . . . . . . . . . 13
     ![[,] [,]](_icc.gif)              |
172 | 171 | oveq1d 6323 |
. . . . . . . . . . . 12
     ![[,] [,]](_icc.gif)                  |
173 | | pncan 9901 |
. . . . . . . . . . . . 13
 
       |
174 | 162, 82, 173 | sylancl 675 |
. . . . . . . . . . . 12
     ![[,] [,]](_icc.gif)        |
175 | 172, 174 | eqtrd 2505 |
. . . . . . . . . . 11
     ![[,] [,]](_icc.gif)              |
176 | 175 | fveq2d 5883 |
. . . . . . . . . 10
     ![[,] [,]](_icc.gif)                                      |
177 | 176 | adantl 473 |
. . . . . . . . 9
 
    ![[,] [,]](_icc.gif)                                       |
178 | 42, 43, 44 | pcoval2 22125 |
. . . . . . . . 9
 
    ![[,] [,]](_icc.gif)                         |
179 | 159, 177,
178 | 3eqtrd 2509 |
. . . . . . . 8
 
    ![[,] [,]](_icc.gif)                                       |
180 | 141, 179 | sylan2 482 |
. . . . . . 7
 
   ![[,] [,]](_icc.gif) 
                                        |
181 | 180 | anassrs 660 |
. . . . . 6
     ![[,] [,]](_icc.gif)                                          |
182 | | iffalse 3881 |
. . . . . . . 8

                                    |
183 | 182 | fveq2d 5883 |
. . . . . . 7

                      
                                                     |
184 | 183 | adantl 473 |
. . . . . 6
     ![[,] [,]](_icc.gif)                          
                                                     |
185 | | iffalse 3881 |
. . . . . . 7

                                         |
186 | 185 | adantl 473 |
. . . . . 6
     ![[,] [,]](_icc.gif)                                             |
187 | 181, 184,
186 | 3eqtr4d 2515 |
. . . . 5
     ![[,] [,]](_icc.gif)                          
                                                        |
188 | 140, 187 | pm2.61dan 808 |
. . . 4
 
  ![[,] [,]](_icc.gif)                       
                                                        |
189 | 188 | mpteq2dva 4482 |
. . 3
    ![[,] [,]](_icc.gif)                      
                             ![[,] [,]](_icc.gif)                                  |
190 | | pcoass.7 |
. . . . . . 7
   ![[,] [,]](_icc.gif)        
                     |
191 | | iitopon 21989 |
. . . . . . . . 9
TopOn   ![[,] [,]](_icc.gif)    |
192 | 191 | a1i 11 |
. . . . . . . 8
 TopOn   ![[,] [,]](_icc.gif)     |
193 | 192 | cnmptid 20753 |
. . . . . . . 8
    ![[,] [,]](_icc.gif)       |
194 | | 0elunit 11776 |
. . . . . . . . . 10
  ![[,] [,]](_icc.gif)   |
195 | 194 | a1i 11 |
. . . . . . . . 9
   ![[,] [,]](_icc.gif)    |
196 | 192, 192,
195 | cnmptc 20754 |
. . . . . . . 8
    ![[,] [,]](_icc.gif)       |
197 | | eqid 2471 |
. . . . . . . . 9
         |
198 | | eqid 2471 |
. . . . . . . . 9
     ↾t   ![[,] [,]](_icc.gif)          ↾t   ![[,] [,]](_icc.gif)      |
199 | | eqid 2471 |
. . . . . . . . 9
     ↾t     ![[,] [,]](_icc.gif)        ↾t     ![[,] [,]](_icc.gif)    |
200 | | dfii2 21992 |
. . . . . . . . 9
     ↾t   ![[,] [,]](_icc.gif)    |
201 | | 0red 9662 |
. . . . . . . . 9
   |
202 | | 1red 9676 |
. . . . . . . . 9
   |
203 | 147 | a1i 11 |
. . . . . . . . 9
     ![[,] [,]](_icc.gif)    |
204 | | simprl 772 |
. . . . . . . . . . . 12
 
     ![[,] [,]](_icc.gif)        |
205 | 204 | oveq1d 6323 |
. . . . . . . . . . 11
 
     ![[,] [,]](_icc.gif)                |
206 | 32, 23 | addcomi 9842 |
. . . . . . . . . . 11
             |
207 | 205, 206 | syl6eq 2521 |
. . . . . . . . . 10
 
     ![[,] [,]](_icc.gif)                |
208 | 18, 60 | ltnlei 9773 |
. . . . . . . . . . . . 13
    
      |
209 | 78, 208 | mpbi 213 |
. . . . . . . . . . . 12
     |
210 | 204 | breq1d 4405 |
. . . . . . . . . . . 12
 
     ![[,] [,]](_icc.gif)        
     |
211 | 209, 210 | mtbiri 310 |
. . . . . . . . . . 11
 
     ![[,] [,]](_icc.gif)   
    |
212 | 211 | iffalsed 3883 |
. . . . . . . . . 10
 
     ![[,] [,]](_icc.gif)                       |
213 | 204 | oveq1d 6323 |
. . . . . . . . . . . 12
 
     ![[,] [,]](_icc.gif)            |
214 | 213, 30 | syl6eq 2521 |
. . . . . . . . . . 11
 
     ![[,] [,]](_icc.gif)          |
215 | 214 | oveq1d 6323 |
. . . . . . . . . 10
 
     ![[,] [,]](_icc.gif)                  |
216 | 207, 212,
215 | 3eqtr4d 2515 |
. . . . . . . . 9
 
     ![[,] [,]](_icc.gif)                         |
217 | | eqid 2471 |
. . . . . . . . . 10
     ↾t   ![[,] [,]](_icc.gif)          ↾t   ![[,] [,]](_icc.gif)      |
218 | | eqid 2471 |
. . . . . . . . . 10
     ↾t     ![[,] [,]](_icc.gif)          ↾t     ![[,] [,]](_icc.gif)      |
219 | 60 | a1i 11 |
. . . . . . . . . 10
     |
220 | 74, 76 | recgt0ii 10534 |
. . . . . . . . . . . . 13
   |
221 | 5, 18, 220 | ltleii 9775 |
. . . . . . . . . . . 12
   |
222 | 5, 60 | elicc2i 11725 |
. . . . . . . . . . . 12
     ![[,] [,]](_icc.gif)   
    
       |
223 | 18, 221, 79, 222 | mpbir3an 1212 |
. . . . . . . . . . 11
    ![[,] [,]](_icc.gif)     |
224 | 223 | a1i 11 |
. . . . . . . . . 10
     ![[,] [,]](_icc.gif)      |
225 | | simprl 772 |
. . . . . . . . . . . 12
 
     ![[,] [,]](_icc.gif)        |
226 | 225 | oveq2d 6324 |
. . . . . . . . . . 11
 
     ![[,] [,]](_icc.gif)            |
227 | 225 | oveq1d 6323 |
. . . . . . . . . . 11
 
     ![[,] [,]](_icc.gif)                |
228 | 24, 226, 227 | 3eqtr4a 2531 |
. . . . . . . . . 10
 
     ![[,] [,]](_icc.gif)            |
229 | | retopon 21862 |
. . . . . . . . . . . . 13
    TopOn   |
230 | | 0xr 9705 |
. . . . . . . . . . . . . . . 16
 |
231 | 60 | rexri 9711 |
. . . . . . . . . . . . . . . 16
   |
232 | | lbicc2 11774 |
. . . . . . . . . . . . . . . 16
   
     ![[,] [,]](_icc.gif)      |
233 | 230, 231,
143, 232 | mp3an 1390 |
. . . . . . . . . . . . . . 15
  ![[,] [,]](_icc.gif)     |
234 | | iccss2 11730 |
. . . . . . . . . . . . . . 15
    ![[,] [,]](_icc.gif)        ![[,] [,]](_icc.gif)       ![[,] [,]](_icc.gif)      ![[,] [,]](_icc.gif)      |
235 | 233, 223,
234 | mp2an 686 |
. . . . . . . . . . . . . 14
  ![[,] [,]](_icc.gif)      ![[,] [,]](_icc.gif)     |
236 | | iccssre 11741 |
. . . . . . . . . . . . . . 15
       ![[,] [,]](_icc.gif)      |
237 | 5, 60, 236 | mp2an 686 |
. . . . . . . . . . . . . 14
  ![[,] [,]](_icc.gif)     |
238 | 235, 237 | sstri 3427 |
. . . . . . . . . . . . 13
  ![[,] [,]](_icc.gif)     |
239 | | resttopon 20254 |
. . . . . . . . . . . . 13
      TopOn    ![[,] [,]](_icc.gif)   
      ↾t   ![[,] [,]](_icc.gif)     TopOn   ![[,] [,]](_icc.gif)       |
240 | 229, 238,
239 | mp2an 686 |
. . . . . . . . . . . 12
     ↾t   ![[,] [,]](_icc.gif)     TopOn   ![[,] [,]](_icc.gif)      |
241 | 240 | a1i 11 |
. . . . . . . . . . 11
      ↾t   ![[,] [,]](_icc.gif)     TopOn   ![[,] [,]](_icc.gif)       |
242 | 241, 192 | cnmpt1st 20760 |
. . . . . . . . . . 11
    ![[,] [,]](_icc.gif)       ![[,] [,]](_icc.gif)         
↾t   ![[,] [,]](_icc.gif)     
     ↾t   ![[,] [,]](_icc.gif)        |
243 | | retop 21860 |
. . . . . . . . . . . . . 14
     |
244 | | ovex 6336 |
. . . . . . . . . . . . . 14
  ![[,] [,]](_icc.gif)     |
245 | | restabs 20258 |
. . . . . . . . . . . . . 14
        ![[,] [,]](_icc.gif)      ![[,] [,]](_icc.gif)      ![[,] [,]](_icc.gif)           ↾t   ![[,] [,]](_icc.gif)    
↾t   ![[,] [,]](_icc.gif)          ↾t   ![[,] [,]](_icc.gif)       |
246 | 243, 235,
244, 245 | mp3an 1390 |
. . . . . . . . . . . . 13
      ↾t   ![[,] [,]](_icc.gif)     ↾t   ![[,] [,]](_icc.gif)          ↾t   ![[,] [,]](_icc.gif)      |
247 | 246 | eqcomi 2480 |
. . . . . . . . . . . 12
     ↾t   ![[,] [,]](_icc.gif)           ↾t   ![[,] [,]](_icc.gif)     ↾t   ![[,] [,]](_icc.gif)      |
248 | | resttopon 20254 |
. . . . . . . . . . . . . 14
      TopOn    ![[,] [,]](_icc.gif)   
      ↾t   ![[,] [,]](_icc.gif)     TopOn   ![[,] [,]](_icc.gif)       |
249 | 229, 237,
248 | mp2an 686 |
. . . . . . . . . . . . 13
     ↾t   ![[,] [,]](_icc.gif)     TopOn   ![[,] [,]](_icc.gif)      |
250 | 249 | a1i 11 |
. . . . . . . . . . . 12
      ↾t   ![[,] [,]](_icc.gif)     TopOn   ![[,] [,]](_icc.gif)       |
251 | 235 | a1i 11 |
. . . . . . . . . . . 12
   ![[,] [,]](_icc.gif)   
  ![[,] [,]](_icc.gif)      |
252 | 198 | iihalf1cn 22038 |
. . . . . . . . . . . . 13
   ![[,] [,]](_icc.gif)             ↾t   ![[,] [,]](_icc.gif)       |
253 | 252 | a1i 11 |
. . . . . . . . . . . 12
    ![[,] [,]](_icc.gif)             ↾t   ![[,] [,]](_icc.gif)        |
254 | 247, 250,
251, 253 | cnmpt1res 20768 |
. . . . . . . . . . 11
    ![[,] [,]](_icc.gif)             ↾t   ![[,] [,]](_icc.gif)        |
255 | | oveq2 6316 |
. . . . . . . . . . 11
       |
256 | 241, 192,
242, 241, 254, 255 | cnmpt21 20763 |
. . . . . . . . . 10
    ![[,] [,]](_icc.gif)       ![[,] [,]](_icc.gif)           
↾t   ![[,] [,]](_icc.gif)     
   |
257 | | iccssre 11741 |
. . . . . . . . . . . . . 14
           ![[,] [,]](_icc.gif)      |
258 | 18, 60, 257 | mp2an 686 |
. . . . . . . . . . . . 13
    ![[,] [,]](_icc.gif)     |
259 | | resttopon 20254 |
. . . . . . . . . . . . 13
      TopOn      ![[,] [,]](_icc.gif)   
      ↾t     ![[,] [,]](_icc.gif)     TopOn     ![[,] [,]](_icc.gif)       |
260 | 229, 258,
259 | mp2an 686 |
. . . . . . . . . . . 12
     ↾t     ![[,] [,]](_icc.gif)     TopOn     ![[,] [,]](_icc.gif)      |
261 | 260 | a1i 11 |
. . . . . . . . . . 11
      ↾t     ![[,] [,]](_icc.gif)     TopOn     ![[,] [,]](_icc.gif)       |
262 | 261, 192 | cnmpt1st 20760 |
. . . . . . . . . . 11
      ![[,] [,]](_icc.gif)       ![[,] [,]](_icc.gif)         
↾t     ![[,] [,]](_icc.gif)     
     ↾t     ![[,] [,]](_icc.gif)        |
263 | | eqid 2471 |
. . . . . . . . . . . 12
  ℂfld   ℂfld |
264 | 258 | a1i 11 |
. . . . . . . . . . . 12
     ![[,] [,]](_icc.gif)   
  |
265 | | unitssre 11805 |
. . . . . . . . . . . . 13
  ![[,] [,]](_icc.gif)   |
266 | 265 | a1i 11 |
. . . . . . . . . . . 12
   ![[,] [,]](_icc.gif) 
  |
267 | 150, 87 | sseldi 3416 |
. . . . . . . . . . . . 13
     ![[,] [,]](_icc.gif)          ![[,] [,]](_icc.gif)    |
268 | 267 | adantl 473 |
. . . . . . . . . . . 12
 
    ![[,] [,]](_icc.gif)           ![[,] [,]](_icc.gif)    |
269 | 263 | cnfldtopon 21881 |
. . . . . . . . . . . . . 14
  ℂfld TopOn   |
270 | 269 | a1i 11 |
. . . . . . . . . . . . 13
   ℂfld
TopOn    |
271 | 270 | cnmptid 20753 |
. . . . . . . . . . . . 13
      ℂfld
  ℂfld   |
272 | 18 | a1i 11 |
. . . . . . . . . . . . . . 15
     |
273 | 272 | recnd 9687 |
. . . . . . . . . . . . . 14
     |
274 | 270, 270,
273 | cnmptc 20754 |
. . . . . . . . . . . . 13
        ℂfld
  ℂfld   |
275 | 263 | addcn 21975 |
. . . . . . . . . . . . . 14
    ℂfld   ℂfld   ℂfld  |
276 | 275 | a1i 11 |
. . . . . . . . . . . . 13
     ℂfld
  ℂfld   ℂfld   |
277 | 270, 271,
274, 276 | cnmpt12f 20758 |
. . . . . . . . . . . 12
  
       ℂfld
  ℂfld   |
278 | 263, 218,
200, 264, 266, 268, 277 | cnmptre 22033 |
. . . . . . . . . . 11
      ![[,] [,]](_icc.gif)               ↾t     ![[,] [,]](_icc.gif)        |
279 | | oveq1 6315 |
. . . . . . . . . . 11
           |
280 | 261, 192,
262, 261, 278, 279 | cnmpt21 20763 |
. . . . . . . . . 10
      ![[,] [,]](_icc.gif)       ![[,] [,]](_icc.gif)             
↾t     ![[,] [,]](_icc.gif)     
   |
281 | 197, 217,
218, 198, 201, 219, 224, 192, 228, 256, 280 | cnmpt2pc 22034 |
. . . . . . . . 9
    ![[,] [,]](_icc.gif)       ![[,] [,]](_icc.gif)                       ↾t   ![[,] [,]](_icc.gif)         |
282 | | iccssre 11741 |
. . . . . . . . . . . . 13
   
     ![[,] [,]](_icc.gif) 
  |
283 | 60, 6, 282 | mp2an 686 |
. . . . . . . . . . . 12
    ![[,] [,]](_icc.gif)   |
284 | | resttopon 20254 |
. . . . . . . . . . . 12
      TopOn      ![[,] [,]](_icc.gif) 
      ↾t     ![[,] [,]](_icc.gif)   TopOn     ![[,] [,]](_icc.gif)     |
285 | 229, 283,
284 | mp2an 686 |
. . . . . . . . . . 11
     ↾t     ![[,] [,]](_icc.gif)   TopOn     ![[,] [,]](_icc.gif)    |
286 | 285 | a1i 11 |
. . . . . . . . . 10
      ↾t     ![[,] [,]](_icc.gif)   TopOn     ![[,] [,]](_icc.gif)     |
287 | 286, 192 | cnmpt1st 20760 |
. . . . . . . . . 10
      ![[,] [,]](_icc.gif)     ![[,] [,]](_icc.gif)         
↾t     ![[,] [,]](_icc.gif)   
     ↾t     ![[,] [,]](_icc.gif)      |
288 | 283 | a1i 11 |
. . . . . . . . . . 11
     ![[,] [,]](_icc.gif) 
  |
289 | 150, 157 | sseldi 3416 |
. . . . . . . . . . . 12
     ![[,] [,]](_icc.gif)          ![[,] [,]](_icc.gif)    |
290 | 289 | adantl 473 |
. . . . . . . . . . 11
 
    ![[,] [,]](_icc.gif)           ![[,] [,]](_icc.gif)    |
291 | 263 | divccn 21983 |
. . . . . . . . . . . . . 14
    
     ℂfld
  ℂfld   |
292 | 4, 25, 291 | mp2an 686 |
. . . . . . . . . . . . 13
       ℂfld   ℂfld  |
293 | 292 | a1i 11 |
. . . . . . . . . . . 12
  
     ℂfld
  ℂfld   |
294 | 32 | a1i 11 |
. . . . . . . . . . . . 13
     |
295 | 270, 270,
294 | cnmptc 20754 |
. . . . . . . . . . . 12
        ℂfld
  ℂfld   |
296 | 270, 293,
295, 276 | cnmpt12f 20758 |
. . . . . . . . . . 11
            ℂfld
  ℂfld   |
297 | 263, 199,
200, 288, 266, 290, 296 | cnmptre 22033 |
. . . . . . . . . 10
      ![[,] [,]](_icc.gif)               ↾t     ![[,] [,]](_icc.gif)      |
298 | | oveq1 6315 |
. . . . . . . . . . 11
       |
299 | 298 | oveq1d 6323 |
. . . . . . . . . 10
               |
300 | 286, 192,
287, 286, 297, 299 | cnmpt21 20763 |
. . . . . . . . 9
      ![[,] [,]](_icc.gif)     ![[,] [,]](_icc.gif)               
↾t     ![[,] [,]](_icc.gif)   
   |
301 | 197, 198,
199, 200, 201, 202, 203, 192, 216, 281, 300 | cnmpt2pc 22034 |
. . . . . . . 8
    ![[,] [,]](_icc.gif)     ![[,] [,]](_icc.gif)        
                          |
302 | | breq1 4398 |
. . . . . . . . . . . 12
 
 
     |
303 | | breq1 4398 |
. . . . . . . . . . . . 13
 
 
     |
304 | 303, 255,
279 | ifbieq12d 3899 |
. . . . . . . . . . . 12
  
                          |
305 | 302, 304,
299 | ifbieq12d 3899 |
. . . . . . . . . . 11
  
                         
                          |
306 | 305 | equcoms 1872 |
. . . . . . . . . 10
  
                         
                          |
307 | 306 | adantr 472 |
. . . . . . . . 9
 
       
                         
                     |
308 | 307 | eqcomd 2477 |
. . . . . . . 8
 
                                 
                     |
309 | 192, 193,
196, 192, 192, 301, 308 | cnmpt12 20759 |
. . . . . . 7
    ![[,] [,]](_icc.gif)        
                        |
310 | 190, 309 | syl5eqel 2553 |
. . . . . 6
     |
311 | | iiuni 21991 |
. . . . . . 7
  ![[,] [,]](_icc.gif)    |
312 | 311, 311 | cnf 20339 |
. . . . . 6
  
    ![[,] [,]](_icc.gif)      ![[,] [,]](_icc.gif)    |
313 | 310, 312 | syl 17 |
. . . . 5
     ![[,] [,]](_icc.gif)      ![[,] [,]](_icc.gif)    |
314 | 190 | fmpt 6058 |
. . . . 5
 
  ![[,] [,]](_icc.gif)                               ![[,] [,]](_icc.gif)      ![[,] [,]](_icc.gif)      ![[,] [,]](_icc.gif)    |
315 | 313, 314 | sylibr 217 |
. . . 4
    ![[,] [,]](_icc.gif)         
                     ![[,] [,]](_icc.gif)    |
316 | 190 | a1i 11 |
. . . 4
    ![[,] [,]](_icc.gif)   
                           |
317 | 41, 45, 91 | pcocn 22126 |
. . . . . 6
                     |
318 | | eqid 2471 |
. . . . . . 7
   |
319 | 311, 318 | cnf 20339 |
. . . . . 6
                                       ![[,] [,]](_icc.gif)       |
320 | 317, 319 | syl 17 |
. . . . 5
                     ![[,] [,]](_icc.gif)       |
321 | 320 | feqmptd 5932 |
. . . 4
                    ![[,] [,]](_icc.gif)                         |
322 | | fveq2 5879 |
. . . 4
       
                                                                
                      |
323 | 315, 316,
321, 322 | fmptcof 6073 |
. . 3
                      ![[,] [,]](_icc.gif)                           
                       |
324 | 41, 42, 89 | pcocn 22126 |
. . . 4
             |
325 | 324, 43 | pcoval 22120 |
. . 3
                    ![[,] [,]](_icc.gif)   
                              |
326 | 189, 323,
325 | 3eqtr4rd 2516 |
. 2
                                     |
327 | | id 22 |
. . . . . . . 8
   |
328 | 327, 143 | syl6eqbr 4433 |
. . . . . . 7
     |
329 | 328 | iftrued 3880 |
. . . . . 6
  
                         
             |
330 | 327, 221 | syl6eqbr 4433 |
. . . . . . 7
     |
331 | 330 | iftrued 3880 |
. . . . . 6
  
               |
332 | | oveq2 6316 |
. . . . . . 7
       |
333 | | 2t0e0 10788 |
. . . . . . 7
   |
334 | 332, 333 | syl6eq 2521 |
. . . . . 6
     |
335 | 329, 331,
334 | 3eqtrd 2509 |
. . . . 5
  
                          |
336 | | c0ex 9655 |
. . . . 5
 |
337 | 335, 190,
336 | fvmpt 5963 |
. . . 4
   ![[,] [,]](_icc.gif)        |
338 | 195, 337 | syl 17 |
. . 3
       |
339 | 148 | a1i 11 |
. . . 4
   ![[,] [,]](_icc.gif)    |
340 | 60, 6 | ltnlei 9773 |
. . . . . . . . 9
  
    |
341 | 144, 340 | mpbi 213 |
. . . . . . . 8
   |
342 | | breq1 4398 |
. . . . . . . 8
 
 
     |
343 | 341, 342 | mtbiri 310 |
. . . . . . 7
     |
344 | 343 | iffalsed 3883 |
. . . . . 6
  
                                |
345 | | oveq1 6315 |
. . . . . . . 8
       |
346 | 345 | oveq1d 6323 |
. . . . . . 7
               |
347 | 346, 84 | syl6eq 2521 |
. . . . . 6
         |
348 | 344, 347 | eqtrd 2505 |
. . . . 5
  
                          |
349 | | 1ex 9656 |
. . . . 5
 |
350 | 348, 190,
349 | fvmpt 5963 |
. . . 4
   ![[,] [,]](_icc.gif)        |
351 | 339, 350 | syl 17 |
. . 3
       |
352 | 317, 310,
338, 351 | reparpht 22107 |
. 2
                                         |
353 | 326, 352 | eqbrtrd 4416 |
1
                                       |