Step | Hyp | Ref
| Expression |
1 | | rpssre 10578 |
. . . 4
 |
2 | | eqid 2404 |
. . . . . . . . . . 11
  ℂfld   ℂfld |
3 | 2 | subcn 18849 |
. . . . . . . . . . . 12
    ℂfld   ℂfld   ℂfld  |
4 | 3 | a1i 11 |
. . . . . . . . . . 11
 
   
     ℂfld
  ℂfld   ℂfld   |
5 | | ssid 3327 |
. . . . . . . . . . . . 13
 |
6 | | cncfmptid 18895 |
. . . . . . . . . . . . 13
 
         |
7 | 5, 5, 6 | mp2an 654 |
. . . . . . . . . . . 12
       |
8 | 7 | a1i 11 |
. . . . . . . . . . 11
 
   
         |
9 | 2 | mulcn 18850 |
. . . . . . . . . . . . 13
    ℂfld   ℂfld   ℂfld  |
10 | 9 | a1i 11 |
. . . . . . . . . . . 12
 
   
     ℂfld
  ℂfld   ℂfld   |
11 | | pntlem3.2 |
. . . . . . . . . . . . . . 15
   |
12 | 11 | adantr 452 |
. . . . . . . . . . . . . 14
 
   
   |
13 | 12 | rpcnd 10606 |
. . . . . . . . . . . . 13
 
   
   |
14 | 5 | a1i 11 |
. . . . . . . . . . . . 13
 
   
   |
15 | | cncfmptc 18894 |
. . . . . . . . . . . . 13
           |
16 | 13, 14, 14, 15 | syl3anc 1184 |
. . . . . . . . . . . 12
 
   
         |
17 | | 3nn0 10195 |
. . . . . . . . . . . . . 14
 |
18 | 2 | expcn 18855 |
. . . . . . . . . . . . . 14

         ℂfld   ℂfld   |
19 | 17, 18 | mp1i 12 |
. . . . . . . . . . . . 13
 
   
          ℂfld
  ℂfld   |
20 | 2 | cncfcn1 18893 |
. . . . . . . . . . . . 13
       ℂfld
  ℂfld  |
21 | 19, 20 | syl6eleqr 2495 |
. . . . . . . . . . . 12
 
   
             |
22 | 2, 10, 16, 21 | cncfmpt2f 18897 |
. . . . . . . . . . 11
 
   
               |
23 | 2, 4, 8, 22 | cncfmpt2f 18897 |
. . . . . . . . . 10
 
   
   
             |
24 | | pntlem3.1 |
. . . . . . . . . . . . . . 15
   ![[,] [,]](_icc.gif)                 
  |
25 | | ssrab2 3388 |
. . . . . . . . . . . . . . 15
   ![[,] [,]](_icc.gif)  
              
   ![[,] [,]](_icc.gif)   |
26 | 24, 25 | eqsstri 3338 |
. . . . . . . . . . . . . 14
  ![[,] [,]](_icc.gif)   |
27 | | 0re 9047 |
. . . . . . . . . . . . . . 15
 |
28 | | pntlem3.a |
. . . . . . . . . . . . . . . 16
   |
29 | 28 | rpred 10604 |
. . . . . . . . . . . . . . 15
   |
30 | | iccssre 10948 |
. . . . . . . . . . . . . . 15
 
   ![[,] [,]](_icc.gif) 
  |
31 | 27, 29, 30 | sylancr 645 |
. . . . . . . . . . . . . 14
   ![[,] [,]](_icc.gif) 
  |
32 | 26, 31 | syl5ss 3319 |
. . . . . . . . . . . . 13

  |
33 | | 0xr 9087 |
. . . . . . . . . . . . . . . . 17
 |
34 | 33 | a1i 11 |
. . . . . . . . . . . . . . . 16
   |
35 | 28 | rpxrd 10605 |
. . . . . . . . . . . . . . . 16
   |
36 | 28 | rpge0d 10608 |
. . . . . . . . . . . . . . . 16

  |
37 | | ubicc2 10970 |
. . . . . . . . . . . . . . . 16
     ![[,] [,]](_icc.gif)    |
38 | 34, 35, 36, 37 | syl3anc 1184 |
. . . . . . . . . . . . . . 15
   ![[,] [,]](_icc.gif)    |
39 | | 1rp 10572 |
. . . . . . . . . . . . . . . 16
 |
40 | | 1re 9046 |
. . . . . . . . . . . . . . . . . . . . 21
 |
41 | | elicopnf 10956 |
. . . . . . . . . . . . . . . . . . . . 21
    
     |
42 | 40, 41 | mp1i 12 |
. . . . . . . . . . . . . . . . . . . 20
          |
43 | 42 | simprbda 607 |
. . . . . . . . . . . . . . . . . . 19
 
      |
44 | 27 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
 
      |
45 | 40 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
 
      |
46 | | 0lt1 9506 |
. . . . . . . . . . . . . . . . . . . . 21
 |
47 | 46 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
 
      |
48 | 42 | simplbda 608 |
. . . . . . . . . . . . . . . . . . . 20
 
      |
49 | 44, 45, 43, 47, 48 | ltletrd 9186 |
. . . . . . . . . . . . . . . . . . 19
 
      |
50 | 43, 49 | elrpd 10602 |
. . . . . . . . . . . . . . . . . 18
 
      |
51 | | pntlem3.A |
. . . . . . . . . . . . . . . . . . 19
              |
52 | 51 | adantr 452 |
. . . . . . . . . . . . . . . . . 18
 
              
  |
53 | | fveq2 5687 |
. . . . . . . . . . . . . . . . . . . . . 22
           |
54 | | id 20 |
. . . . . . . . . . . . . . . . . . . . . 22
   |
55 | 53, 54 | oveq12d 6058 |
. . . . . . . . . . . . . . . . . . . . 21
               |
56 | 55 | fveq2d 5691 |
. . . . . . . . . . . . . . . . . . . 20
                       |
57 | 56 | breq1d 4182 |
. . . . . . . . . . . . . . . . . . 19
           
             |
58 | 57 | rspcv 3008 |
. . . . . . . . . . . . . . . . . 18

 
                   
   |
59 | 50, 52, 58 | sylc 58 |
. . . . . . . . . . . . . . . . 17
 
                |
60 | 59 | ralrimiva 2749 |
. . . . . . . . . . . . . . . 16
               
  |
61 | | oveq1 6047 |
. . . . . . . . . . . . . . . . . 18
  
      |
62 | 61 | raleqdv 2870 |
. . . . . . . . . . . . . . . . 17
  
 
           
              
   |
63 | 62 | rspcev 3012 |
. . . . . . . . . . . . . . . 16
  
              
               
  |
64 | 39, 60, 63 | sylancr 645 |
. . . . . . . . . . . . . . 15
                   |
65 | | breq2 4176 |
. . . . . . . . . . . . . . . . 17
           
             |
66 | 65 | rexralbidv 2710 |
. . . . . . . . . . . . . . . 16
  
              
               
   |
67 | 66, 24 | elrab2 3054 |
. . . . . . . . . . . . . . 15

   ![[,] [,]](_icc.gif) 
               
   |
68 | 38, 64, 67 | sylanbrc 646 |
. . . . . . . . . . . . . 14
   |
69 | | ne0i 3594 |
. . . . . . . . . . . . . 14
   |
70 | 68, 69 | syl 16 |
. . . . . . . . . . . . 13
   |
71 | | elicc2 10931 |
. . . . . . . . . . . . . . . . . . . 20
 
    ![[,] [,]](_icc.gif)  
    |
72 | 27, 29, 71 | sylancr 645 |
. . . . . . . . . . . . . . . . . . 19
    ![[,] [,]](_icc.gif)  
    |
73 | 72 | biimpa 471 |
. . . . . . . . . . . . . . . . . 18
 
  ![[,] [,]](_icc.gif)       |
74 | 73 | simp2d 970 |
. . . . . . . . . . . . . . . . 17
 
  ![[,] [,]](_icc.gif)     |
75 | 74 | a1d 23 |
. . . . . . . . . . . . . . . 16
 
  ![[,] [,]](_icc.gif)    
              
   |
76 | 75 | ralrimiva 2749 |
. . . . . . . . . . . . . . 15
    ![[,] [,]](_icc.gif)                   
   |
77 | 24 | raleqi 2868 |
. . . . . . . . . . . . . . . 16
 
    ![[,] [,]](_icc.gif)                      |
78 | | breq2 4176 |
. . . . . . . . . . . . . . . . 17
 
   |
79 | 78 | ralrab2 3060 |
. . . . . . . . . . . . . . . 16
 
   ![[,] [,]](_icc.gif)                 
 
   ![[,] [,]](_icc.gif)                   
   |
80 | 77, 79 | bitri 241 |
. . . . . . . . . . . . . . 15
 
   ![[,] [,]](_icc.gif)                   
   |
81 | 76, 80 | sylibr 204 |
. . . . . . . . . . . . . 14
 
  |
82 | | breq1 4175 |
. . . . . . . . . . . . . . . 16
 
   |
83 | 82 | ralbidv 2686 |
. . . . . . . . . . . . . . 15
  

   |
84 | 83 | rspcev 3012 |
. . . . . . . . . . . . . 14
    
   |
85 | 27, 81, 84 | sylancr 645 |
. . . . . . . . . . . . 13
     |
86 | | infmrcl 9943 |
. . . . . . . . . . . . 13
 
  
  
   |
87 | 32, 70, 85, 86 | syl3anc 1184 |
. . . . . . . . . . . 12
    
  |
88 | 87 | recnd 9070 |
. . . . . . . . . . 11
    
  |
89 | 88 | adantr 452 |
. . . . . . . . . 10
 
   
    
  |
90 | | elrp 10570 |
. . . . . . . . . . . . . 14
    
        
   |
91 | 90 | biimpri 198 |
. . . . . . . . . . . . 13
     
   

  
   |
92 | 87, 91 | sylan 458 |
. . . . . . . . . . . 12
 
   
    
  |
93 | 17 | nn0zi 10262 |
. . . . . . . . . . . 12
 |
94 | | rpexpcl 11355 |
. . . . . . . . . . . 12
     
     
     |
95 | 92, 93, 94 | sylancl 644 |
. . . . . . . . . . 11
 
   
    
      |
96 | 12, 95 | rpmulcld 10620 |
. . . . . . . . . 10
 
   
      
      |
97 | | cncfi 18877 |
. . . . . . . . . 10
   

                    
    
                                                        
       |
98 | 23, 89, 96, 97 | syl3anc 1184 |
. . . . . . . . 9
 
   
          
                                              
       |
99 | 87 | ad2antrr 707 |
. . . . . . . . . . . . 13
      
 
  
   |
100 | | rphalfcl 10592 |
. . . . . . . . . . . . . 14

    |
101 | 100 | adantl 453 |
. . . . . . . . . . . . 13
      
 
    |
102 | 99, 101 | ltaddrpd 10633 |
. . . . . . . . . . . 12
      
 
  
     
     |
103 | 101 | rpred 10604 |
. . . . . . . . . . . . . 14
      
 
    |
104 | 99, 103 | readdcld 9071 |
. . . . . . . . . . . . 13
      
 
    
     |
105 | 99, 104 | ltnled 9176 |
. . . . . . . . . . . 12
      
 
    
                   
   |
106 | 102, 105 | mpbid 202 |
. . . . . . . . . . 11
      
 
    
         |
107 | | ax-resscn 9003 |
. . . . . . . . . . . . . . 15
 |
108 | 32, 107 | syl6ss 3320 |
. . . . . . . . . . . . . 14

  |
109 | 108 | ad2antrr 707 |
. . . . . . . . . . . . 13
      
 
  |
110 | | ssralv 3367 |
. . . . . . . . . . . . 13

 
       
                                              
    

        
         
            

                    
         |
111 | 109, 110 | syl 16 |
. . . . . . . . . . . 12
      
 
 
       
                                              
    

        
         
            

                    
         |
112 | 32 | ad2antrr 707 |
. . . . . . . . . . . . . . . . . . 19
      
 
  |
113 | 112 | sselda 3308 |
. . . . . . . . . . . . . . . . . 18
       
 
   |
114 | 104 | adantr 452 |
. . . . . . . . . . . . . . . . . 18
       
 
     
     |
115 | 113, 114 | ltnled 9176 |
. . . . . . . . . . . . . . . . 17
       
 
 
       
       
   |
116 | 87 | ad3antrrr 711 |
. . . . . . . . . . . . . . . . . . . . 21
       
 
       |
117 | 103 | adantr 452 |
. . . . . . . . . . . . . . . . . . . . 21
       
 
     |
118 | 116, 117 | resubcld 9421 |
. . . . . . . . . . . . . . . . . . . 20
       
 
     
     |
119 | 99, 101 | ltsubrpd 10632 |
. . . . . . . . . . . . . . . . . . . . 21
      
 
    
         |
120 | 119 | adantr 452 |
. . . . . . . . . . . . . . . . . . . 20
       
 
     
         |
121 | 32 | ad3antrrr 711 |
. . . . . . . . . . . . . . . . . . . . 21
       
 
   |
122 | 85 | ad3antrrr 711 |
. . . . . . . . . . . . . . . . . . . . 21
       
 
     |
123 | | simpr 448 |
. . . . . . . . . . . . . . . . . . . . 21
       
 
   |
124 | | infmrlb 9945 |
. . . . . . . . . . . . . . . . . . . . 21
 



  
   |
125 | 121, 122,
123, 124 | syl3anc 1184 |
. . . . . . . . . . . . . . . . . . . 20
       
 
       |
126 | 118, 116,
113, 120, 125 | ltletrd 9186 |
. . . . . . . . . . . . . . . . . . 19
       
 
     
     |
127 | 113, 116,
117 | absdifltd 12191 |
. . . . . . . . . . . . . . . . . . . 20
       
 
        
    
     
  
    
       |
128 | 127 | biimprd 215 |
. . . . . . . . . . . . . . . . . . 19
       
 
      
       
            
       |
129 | 126, 128 | mpand 657 |
. . . . . . . . . . . . . . . . . 18
       
 
 
       
               |
130 | | rphalflt 10594 |
. . . . . . . . . . . . . . . . . . . 20

    |
131 | 130 | ad2antlr 708 |
. . . . . . . . . . . . . . . . . . 19
       
 
     |
132 | 113, 116 | resubcld 9421 |
. . . . . . . . . . . . . . . . . . . . . 22
       
 
    
    |
133 | 132 | recnd 9070 |
. . . . . . . . . . . . . . . . . . . . 21
       
 
    
    |
134 | 133 | abscld 12193 |
. . . . . . . . . . . . . . . . . . . 20
       
 
        
    |
135 | | rpre 10574 |
. . . . . . . . . . . . . . . . . . . . 21

  |
136 | 135 | ad2antlr 708 |
. . . . . . . . . . . . . . . . . . . 20
       
 
   |
137 | | lttr 9108 |
. . . . . . . . . . . . . . . . . . . 20
        
              
              
      |
138 | 134, 117,
136, 137 | syl3anc 1184 |
. . . . . . . . . . . . . . . . . . 19
       
 
         
              
      |
139 | 131, 138 | mpan2d 656 |
. . . . . . . . . . . . . . . . . 18
       
 
        
            
     |
140 | 129, 139 | syld 42 |
. . . . . . . . . . . . . . . . 17
       
 
 
       
             |
141 | 115, 140 | sylbird 227 |
. . . . . . . . . . . . . . . 16
       
 
                 
     |
142 | 141 | con1d 118 |
. . . . . . . . . . . . . . 15
       
 
        
       
      |
143 | 113 | recnd 9070 |
. . . . . . . . . . . . . . . . . . . 20
       
 
   |
144 | | id 20 |
. . . . . . . . . . . . . . . . . . . . . 22
   |
145 | | oveq1 6047 |
. . . . . . . . . . . . . . . . . . . . . . 23
           |
146 | 145 | oveq2d 6056 |
. . . . . . . . . . . . . . . . . . . . . 22
 
             |
147 | 144, 146 | oveq12d 6058 |
. . . . . . . . . . . . . . . . . . . . 21
          
        |
148 | | eqid 2404 |
. . . . . . . . . . . . . . . . . . . . 21
            
        |
149 | | ovex 6065 |
. . . . . . . . . . . . . . . . . . . . 21
         |
150 | 147, 148,
149 | fvmpt 5765 |
. . . . . . . . . . . . . . . . . . . 20
   

                    |
151 | 143, 150 | syl 16 |
. . . . . . . . . . . . . . . . . . 19
       
 
   

                    |
152 | 89 | ad2antrr 707 |
. . . . . . . . . . . . . . . . . . . 20
       
 
       |
153 | | id 20 |
. . . . . . . . . . . . . . . . . . . . . 22
    
   
  |
154 | | oveq1 6047 |
. . . . . . . . . . . . . . . . . . . . . . 23
    
              |
155 | 154 | oveq2d 6056 |
. . . . . . . . . . . . . . . . . . . . . 22
    
           
      |
156 | 153, 155 | oveq12d 6058 |
. . . . . . . . . . . . . . . . . . . . 21
    
                 
        |
157 | | ovex 6065 |
. . . . . . . . . . . . . . . . . . . . 21
    

    
      |
158 | 156, 148,
157 | fvmpt 5765 |
. . . . . . . . . . . . . . . . . . . 20
    
               
           
        |
159 | 152, 158 | syl 16 |
. . . . . . . . . . . . . . . . . . 19
       
 
   

                       
        |
160 | 151, 159 | oveq12d 6058 |
. . . . . . . . . . . . . . . . . 18
       
 
     
            

                            
     
        |
161 | 160 | fveq2d 5691 |
. . . . . . . . . . . . . . . . 17
       
 
                                            
          

    
         |
162 | 161 | breq1d 4182 |
. . . . . . . . . . . . . . . 16
       
 
         
            

                    
    
     
          

    
       
            |
163 | 11 | rpred 10604 |
. . . . . . . . . . . . . . . . . . . . 21
   |
164 | 163 | ad3antrrr 711 |
. . . . . . . . . . . . . . . . . . . 20
       
 
   |
165 | | reexpcl 11353 |
. . . . . . . . . . . . . . . . . . . . 21
 
       |
166 | 113, 17, 165 | sylancl 644 |
. . . . . . . . . . . . . . . . . . . 20
       
 
       |
167 | 164, 166 | remulcld 9072 |
. . . . . . . . . . . . . . . . . . 19
       
 
 
       |
168 | 113, 167 | resubcld 9421 |
. . . . . . . . . . . . . . . . . 18
       
 
           |
169 | 17 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . 21
       
 
   |
170 | 116, 169 | reexpcld 11495 |
. . . . . . . . . . . . . . . . . . . 20
       
 
     
     |
171 | 164, 170 | remulcld 9072 |
. . . . . . . . . . . . . . . . . . 19
       
 
 
           |
172 | 116, 171 | resubcld 9421 |
. . . . . . . . . . . . . . . . . 18
       
 
     

    
       |
173 | 168, 172,
171 | absdifltd 12191 |
. . . . . . . . . . . . . . . . 17
       
 
       
          

    
       
        
           
      
    
      
                   

    
          
         |
174 | 171 | recnd 9070 |
. . . . . . . . . . . . . . . . . . . . 21
       
 
 
           |
175 | 152, 174 | npcand 9371 |
. . . . . . . . . . . . . . . . . . . 20
       
 
           
           
           |
176 | 175 | breq2d 4184 |
. . . . . . . . . . . . . . . . . . 19
       
 
   
           
     
         
     
           
   |
177 | | simpll 731 |
. . . . . . . . . . . . . . . . . . . . . . 23
      
 
  |
178 | | pntlem3.3 |
. . . . . . . . . . . . . . . . . . . . . . 23
 
           |
179 | 177, 178 | sylan 458 |
. . . . . . . . . . . . . . . . . . . . . 22
       
 
           |
180 | | infmrlb 9945 |
. . . . . . . . . . . . . . . . . . . . . 22
 


 
      
  
           |
181 | 121, 122,
179, 180 | syl3anc 1184 |
. . . . . . . . . . . . . . . . . . . . 21
       
 
               |
182 | 116, 168 | lenltd 9175 |
. . . . . . . . . . . . . . . . . . . . 21
       
 
     
 
     
           
   |
183 | 181, 182 | mpbid 202 |
. . . . . . . . . . . . . . . . . . . 20
       
 
 

        
   |
184 | 183 | pm2.21d 100 |
. . . . . . . . . . . . . . . . . . 19
       
 
   
        
     
      |
185 | 176, 184 | sylbid 207 |
. . . . . . . . . . . . . . . . . 18
       
 
   
           
     
         
                 |
186 | 185 | adantld 454 |
. . . . . . . . . . . . . . . . 17
       
 
        

    
          
             

           
     
         
          
   
   |
187 | 173, 186 | sylbid 207 |
. . . . . . . . . . . . . . . 16
       
 
       
          

    
       
             
      |
188 | 162, 187 | sylbid 207 |
. . . . . . . . . . . . . . 15
       
 
         
            

                    
         
      |
189 | 142, 188 | jad 156 |
. . . . . . . . . . . . . 14
       
 
         
                                              
    
       
   |
190 | 189 | ralimdva 2744 |
. . . . . . . . . . . . 13
      
 
 
       
                                              
    

       
   |
191 | 70 | ad2antrr 707 |
. . . . . . . . . . . . . 14
      
 
  |
192 | 85 | ad2antrr 707 |
. . . . . . . . . . . . . 14
      
 
    |
193 | | infmrgelb 9944 |
. . . . . . . . . . . . . 14
   

     
         
      

       
   |
194 | 112, 191,
192, 104, 193 | syl31anc 1187 |
. . . . . . . . . . . . 13
      
 
     
      

       
   |
195 | 190, 194 | sylibrd 226 |
. . . . . . . . . . . 12
      
 
 
       
                                              
    
       
  
    |
196 | 111, 195 | syld 42 |
. . . . . . . . . . 11
      
 
 
       
                                              
    
       
  
    |
197 | 106, 196 | mtod 170 |
. . . . . . . . . 10
      
 

       
                                              
       |
198 | 197 | nrexdv 2769 |
. . . . . . . . 9
 
   

                                                        
       |
199 | 98, 198 | pm2.65da 560 |
. . . . . . . 8
       |
200 | 199 | adantr 452 |
. . . . . . 7
 

   
  |
201 | 32 | adantr 452 |
. . . . . . . . . 10
 

  |
202 | 70 | adantr 452 |
. . . . . . . . . 10
 

  |
203 | 85 | adantr 452 |
. . . . . . . . . 10
 

    |
204 | 135 | adantl 453 |
. . . . . . . . . 10
 

  |
205 | | infmrgelb 9944 |
. . . . . . . . . 10
   

  
  


   |
206 | 201, 202,
203, 204, 205 | syl31anc 1187 |
. . . . . . . . 9
 

    

   |
207 | 24 | raleqi 2868 |
. . . . . . . . . 10
 
    ![[,] [,]](_icc.gif)                      |
208 | | breq2 4176 |
. . . . . . . . . . 11
 
   |
209 | 208 | ralrab2 3060 |
. . . . . . . . . 10
 
   ![[,] [,]](_icc.gif)                 
 
   ![[,] [,]](_icc.gif)                   
   |
210 | 207, 209 | bitri 241 |
. . . . . . . . 9
 
   ![[,] [,]](_icc.gif)                   
   |
211 | 206, 210 | syl6bb 253 |
. . . . . . . 8
 

    

  ![[,] [,]](_icc.gif)                   
    |
212 | | rpgt0 10579 |
. . . . . . . . . 10

  |
213 | 212 | adantl 453 |
. . . . . . . . 9
 

  |
214 | 27 | a1i 11 |
. . . . . . . . . 10
 

  |
215 | 87 | adantr 452 |
. . . . . . . . . 10
 

  
   |
216 | | ltletr 9122 |
. . . . . . . . . 10
 
          

   
   |
217 | 214, 204,
215, 216 | syl3anc 1184 |
. . . . . . . . 9
 

 
   

   
   |
218 | 213, 217 | mpand 657 |
. . . . . . . 8
 

    
       |
219 | 211, 218 | sylbird 227 |
. . . . . . 7
 

 
  ![[,] [,]](_icc.gif)                   
   
    |
220 | 200, 219 | mtod 170 |
. . . . . 6
 

   ![[,] [,]](_icc.gif)                   
   |
221 | | rexanali 2712 |
. . . . . 6
    ![[,] [,]](_icc.gif)                    
   ![[,] [,]](_icc.gif)                   
   |
222 | 220, 221 | sylibr 204 |
. . . . 5
 

   ![[,] [,]](_icc.gif)                   
   |
223 | | fveq2 5687 |
. . . . . . . . . . . . . . 15
           |
224 | | id 20 |
. . . . . . . . . . . . . . 15
   |
225 | 223, 224 | oveq12d 6058 |
. . . . . . . . . . . . . 14
               |
226 | 225 | fveq2d 5691 |
. . . . . . . . . . . . 13
                       |
227 | 226 | breq1d 4182 |
. . . . . . . . . . . 12
           
             |
228 | 227 | cbvralv 2892 |
. . . . . . . . . . 11
 
                               |
229 | | rpre 10574 |
. . . . . . . . . . . . . . . . 17

  |
230 | 229 | ad2antll 710 |
. . . . . . . . . . . . . . . 16
         ![[,] [,]](_icc.gif)   
 
 
  |
231 | | simprl 733 |
. . . . . . . . . . . . . . . 16
         ![[,] [,]](_icc.gif)   
 
 
  |
232 | | simplr 732 |
. . . . . . . . . . . . . . . . . 18
         ![[,] [,]](_icc.gif)   
 
 
  |
233 | 232 | rpred 10604 |
. . . . . . . . . . . . . . . . 17
         ![[,] [,]](_icc.gif)   
 
 
  |
234 | | elicopnf 10956 |
. . . . . . . . . . . . . . . . 17
    
     |
235 | 233, 234 | syl 16 |
. . . . . . . . . . . . . . . 16
         ![[,] [,]](_icc.gif)   
 
 
    
    |
236 | 230, 231,
235 | mpbir2and 889 |
. . . . . . . . . . . . . . 15
         ![[,] [,]](_icc.gif)   
 
 
     |
237 | | pntlem3.r |
. . . . . . . . . . . . . . . . . . . . . 22
  ψ     |
238 | 237 | pntrval 21209 |
. . . . . . . . . . . . . . . . . . . . 21

     ψ     |
239 | 238 | ad2antll 710 |
. . . . . . . . . . . . . . . . . . . 20
         ![[,] [,]](_icc.gif)   
 
 
     ψ     |
240 | 239 | oveq1d 6055 |
. . . . . . . . . . . . . . . . . . 19
         ![[,] [,]](_icc.gif)   
 
 
        ψ      |
241 | | chpcl 20860 |
. . . . . . . . . . . . . . . . . . . . . 22
 ψ    |
242 | 230, 241 | syl 16 |
. . . . . . . . . . . . . . . . . . . . 21
         ![[,] [,]](_icc.gif)   
 
 
ψ    |
243 | 242 | recnd 9070 |
. . . . . . . . . . . . . . . . . . . 20
         ![[,] [,]](_icc.gif)   
 
 
ψ    |
244 | | rpcn 10576 |
. . . . . . . . . . . . . . . . . . . . 21

  |
245 | 244 | ad2antll 710 |
. . . . . . . . . . . . . . . . . . . 20
         ![[,] [,]](_icc.gif)   
 
 
  |
246 | | rpne0 10583 |
. . . . . . . . . . . . . . . . . . . . 21

  |
247 | 246 | ad2antll 710 |
. . . . . . . . . . . . . . . . . . . 20
         ![[,] [,]](_icc.gif)   
 
 
  |
248 | 243, 245,
245, 247 | divsubdird 9785 |
. . . . . . . . . . . . . . . . . . 19
         ![[,] [,]](_icc.gif)   
 
 
  ψ      ψ        |
249 | 245, 247 | dividd 9744 |
. . . . . . . . . . . . . . . . . . . 20
         ![[,] [,]](_icc.gif)   
 
 
    |
250 | 249 | oveq2d 6056 |
. . . . . . . . . . . . . . . . . . 19
         ![[,] [,]](_icc.gif)   
 
 
  ψ        ψ      |
251 | 240, 248,
250 | 3eqtrrd 2441 |
. . . . . . . . . . . . . . . . . 18
         ![[,] [,]](_icc.gif)   
 
 
  ψ            |
252 | 251 | fveq2d 5691 |
. . . . . . . . . . . . . . . . 17
         ![[,] [,]](_icc.gif)   
 
 
     ψ                 |
253 | 252 | breq1d 4182 |
. . . . . . . . . . . . . . . 16
         ![[,] [,]](_icc.gif)   
 
 
      ψ    
             |
254 | | simprr 734 |
. . . . . . . . . . . . . . . . . . 19
       ![[,] [,]](_icc.gif) 
 
  |
255 | 254 | ad2antrr 707 |
. . . . . . . . . . . . . . . . . 18
         ![[,] [,]](_icc.gif)   
 
 
  |
256 | 31 | ad2antrr 707 |
. . . . . . . . . . . . . . . . . . . . 21
       ![[,] [,]](_icc.gif) 
 
  ![[,] [,]](_icc.gif)    |
257 | 256 | ad2antrr 707 |
. . . . . . . . . . . . . . . . . . . 20
         ![[,] [,]](_icc.gif)   
 
 
  ![[,] [,]](_icc.gif)    |
258 | | simplrl 737 |
. . . . . . . . . . . . . . . . . . . . 21
   
    ![[,] [,]](_icc.gif)   
   ![[,] [,]](_icc.gif)    |
259 | 258 | adantr 452 |
. . . . . . . . . . . . . . . . . . . 20
         ![[,] [,]](_icc.gif)   
 
 
  ![[,] [,]](_icc.gif)    |
260 | 257, 259 | sseldd 3309 |
. . . . . . . . . . . . . . . . . . 19
         ![[,] [,]](_icc.gif)   
 
 
  |
261 | | simp-4r 744 |
. . . . . . . . . . . . . . . . . . . 20
         ![[,] [,]](_icc.gif)   
 
 
  |
262 | 261 | rpred 10604 |
. . . . . . . . . . . . . . . . . . 19
         ![[,] [,]](_icc.gif)   
 
 
  |
263 | 260, 262 | ltnled 9176 |
. . . . . . . . . . . . . . . . . 18
         ![[,] [,]](_icc.gif)   
 
 

   |
264 | 255, 263 | mpbird 224 |
. . . . . . . . . . . . . . . . 17
         ![[,] [,]](_icc.gif)   
 
 
  |
265 | 229, 241 | syl 16 |
. . . . . . . . . . . . . . . . . . . . . . 23

ψ    |
266 | | rerpdivcl 10595 |
. . . . . . . . . . . . . . . . . . . . . . 23
  ψ  
 ψ     |
267 | 265, 266 | mpancom 651 |
. . . . . . . . . . . . . . . . . . . . . 22

 ψ     |
268 | 267 | ad2antll 710 |
. . . . . . . . . . . . . . . . . . . . 21
         ![[,] [,]](_icc.gif)   
 
 
 ψ     |
269 | | resubcl 9321 |
. . . . . . . . . . . . . . . . . . . . 21
   ψ      ψ      |
270 | 268, 40, 269 | sylancl 644 |
. . . . . . . . . . . . . . . . . . . 20
         ![[,] [,]](_icc.gif)   
 
 
  ψ      |
271 | 270 | recnd 9070 |
. . . . . . . . . . . . . . . . . . 19
         ![[,] [,]](_icc.gif)   
 
 
  ψ      |
272 | 271 | abscld 12193 |
. . . . . . . . . . . . . . . . . 18
         ![[,] [,]](_icc.gif)   
 
 
     ψ       |
273 | | lelttr 9121 |
. . . . . . . . . . . . . . . . . 18
       ψ             ψ           ψ        |
274 | 272, 260,
262, 273 | syl3anc 1184 |
. . . . . . . . . . . . . . . . 17
         ![[,] [,]](_icc.gif)   
 
 
       ψ           ψ        |
275 | 264, 274 | mpan2d 656 |
. . . . . . . . . . . . . . . 16
         ![[,] [,]](_icc.gif)   
 
 
      ψ    
     ψ        |
276 | 253, 275 | sylbird 227 |
. . . . . . . . . . . . . . 15
         ![[,] [,]](_icc.gif)   
 
 
          
     ψ        |
277 | 236, 276 | embantd 52 |
. . . . . . . . . . . . . 14
         ![[,] [,]](_icc.gif)   
 
 
                     ψ        |
278 | 277 | exp32 589 |
. . . . . . . . . . . . 13
   
    ![[,] [,]](_icc.gif)   
                 
      ψ          |
279 | 278 | com24 83 |
. . . . . . . . . . . 12
   
    ![[,] [,]](_icc.gif)   
               
        ψ          |
280 | 279 | ralimdv2 2746 |
. . . . . . . . . . 11
   
    ![[,] [,]](_icc.gif)   
                
 
     ψ         |
281 | 228, 280 | syl5bi 209 |
. . . . . . . . . 10
   
    ![[,] [,]](_icc.gif)   
                
 
     ψ         |
282 | 281 | reximdva 2778 |
. . . . . . . . 9
       ![[,] [,]](_icc.gif) 
 
 
              
        ψ         |
283 | 282 | anassrs 630 |
. . . . . . . 8
   

  ![[,] [,]](_icc.gif)     
              
        ψ         |
284 | 283 | impancom 428 |
. . . . . . 7
   

  ![[,] [,]](_icc.gif)                  
 
        ψ         |
285 | 284 | expimpd 587 |
. . . . . 6
      ![[,] [,]](_icc.gif)                    
   
     ψ         |
286 | 285 | rexlimdva 2790 |
. . . . 5
 

 
  ![[,] [,]](_icc.gif)                    
        ψ         |
287 | 222, 286 | mpd 15 |
. . . 4
 

        ψ        |
288 | | ssrexv 3368 |
. . . 4

 
       ψ      
 
     ψ         |
289 | 1, 287, 288 | mpsyl 61 |
. . 3
 

        ψ        |
290 | 289 | ralrimiva 2749 |
. 2
   
      ψ        |
291 | 267 | recnd 9070 |
. . . . 5

 ψ     |
292 | 291 | rgen 2731 |
. . . 4
  ψ    |
293 | 292 | a1i 11 |
. . 3
   ψ     |
294 | 1 | a1i 11 |
. . 3
   |
295 | | ax-1cn 9004 |
. . . 4
 |
296 | 295 | a1i 11 |
. . 3
   |
297 | 293, 294,
296 | rlim2 12245 |
. 2
    ψ     
        ψ         |
298 | 290, 297 | mpbird 224 |
1
   ψ       |