Step | Hyp | Ref
| Expression |
1 | | rpssre 11335 |
. . . 4
 |
2 | | eqid 2471 |
. . . . . . . . . . 11
  ℂfld   ℂfld |
3 | 2 | subcn 21976 |
. . . . . . . . . . . 12
    ℂfld   ℂfld   ℂfld  |
4 | 3 | a1i 11 |
. . . . . . . . . . 11
 
inf        ℂfld   ℂfld   ℂfld   |
5 | | ssid 3437 |
. . . . . . . . . . . . 13
 |
6 | | cncfmptid 22022 |
. . . . . . . . . . . . 13
 
         |
7 | 5, 5, 6 | mp2an 686 |
. . . . . . . . . . . 12
       |
8 | 7 | a1i 11 |
. . . . . . . . . . 11
 
inf            |
9 | | pntlem3.2 |
. . . . . . . . . . . . . . 15
   |
10 | 9 | adantr 472 |
. . . . . . . . . . . . . 14
 
inf      |
11 | 10 | rpcnd 11366 |
. . . . . . . . . . . . 13
 
inf      |
12 | 5 | a1i 11 |
. . . . . . . . . . . . 13
 
inf      |
13 | | cncfmptc 22021 |
. . . . . . . . . . . . 13
           |
14 | 11, 12, 12, 13 | syl3anc 1292 |
. . . . . . . . . . . 12
 
inf            |
15 | | 3nn0 10911 |
. . . . . . . . . . . . . 14
 |
16 | 2 | expcn 21982 |
. . . . . . . . . . . . . 14

         ℂfld   ℂfld   |
17 | 15, 16 | mp1i 13 |
. . . . . . . . . . . . 13
 
inf             ℂfld   ℂfld   |
18 | 2 | cncfcn1 22020 |
. . . . . . . . . . . . 13
       ℂfld
  ℂfld  |
19 | 17, 18 | syl6eleqr 2560 |
. . . . . . . . . . . 12
 
inf                |
20 | 14, 19 | mulcncf 22476 |
. . . . . . . . . . 11
 
inf                  |
21 | 2, 4, 8, 20 | cncfmpt2f 22024 |
. . . . . . . . . 10
 
inf                    |
22 | | pntlem3.1 |
. . . . . . . . . . . . . . 15
   ![[,] [,]](_icc.gif)                 
  |
23 | | ssrab2 3500 |
. . . . . . . . . . . . . . 15
   ![[,] [,]](_icc.gif)  
              
   ![[,] [,]](_icc.gif)   |
24 | 22, 23 | eqsstri 3448 |
. . . . . . . . . . . . . 14
  ![[,] [,]](_icc.gif)   |
25 | | 0re 9661 |
. . . . . . . . . . . . . . 15
 |
26 | | pntlem3.a |
. . . . . . . . . . . . . . . 16
   |
27 | 26 | rpred 11364 |
. . . . . . . . . . . . . . 15
   |
28 | | iccssre 11741 |
. . . . . . . . . . . . . . 15
 
   ![[,] [,]](_icc.gif) 
  |
29 | 25, 27, 28 | sylancr 676 |
. . . . . . . . . . . . . 14
   ![[,] [,]](_icc.gif) 
  |
30 | 24, 29 | syl5ss 3429 |
. . . . . . . . . . . . 13

  |
31 | | 0xr 9705 |
. . . . . . . . . . . . . . . . 17
 |
32 | 31 | a1i 11 |
. . . . . . . . . . . . . . . 16
   |
33 | 26 | rpxrd 11365 |
. . . . . . . . . . . . . . . 16
   |
34 | 26 | rpge0d 11368 |
. . . . . . . . . . . . . . . 16

  |
35 | | ubicc2 11775 |
. . . . . . . . . . . . . . . 16
     ![[,] [,]](_icc.gif)    |
36 | 32, 33, 34, 35 | syl3anc 1292 |
. . . . . . . . . . . . . . 15
   ![[,] [,]](_icc.gif)    |
37 | | 1rp 11329 |
. . . . . . . . . . . . . . . 16
 |
38 | | 1re 9660 |
. . . . . . . . . . . . . . . . . . . . 21
 |
39 | | elicopnf 11755 |
. . . . . . . . . . . . . . . . . . . . 21
    
     |
40 | 38, 39 | mp1i 13 |
. . . . . . . . . . . . . . . . . . . 20
          |
41 | 40 | simprbda 635 |
. . . . . . . . . . . . . . . . . . 19
 
      |
42 | | 0red 9662 |
. . . . . . . . . . . . . . . . . . . 20
 
      |
43 | 38 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
 
      |
44 | | 0lt1 10157 |
. . . . . . . . . . . . . . . . . . . . 21
 |
45 | 44 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
 
      |
46 | 40 | simplbda 636 |
. . . . . . . . . . . . . . . . . . . 20
 
      |
47 | 42, 43, 41, 45, 46 | ltletrd 9812 |
. . . . . . . . . . . . . . . . . . 19
 
      |
48 | 41, 47 | elrpd 11361 |
. . . . . . . . . . . . . . . . . 18
 
      |
49 | | pntlem3.A |
. . . . . . . . . . . . . . . . . . 19
              |
50 | 49 | adantr 472 |
. . . . . . . . . . . . . . . . . 18
 
              
  |
51 | | fveq2 5879 |
. . . . . . . . . . . . . . . . . . . . . 22
           |
52 | | id 22 |
. . . . . . . . . . . . . . . . . . . . . 22
   |
53 | 51, 52 | oveq12d 6326 |
. . . . . . . . . . . . . . . . . . . . 21
               |
54 | 53 | fveq2d 5883 |
. . . . . . . . . . . . . . . . . . . 20
                       |
55 | 54 | breq1d 4405 |
. . . . . . . . . . . . . . . . . . 19
           
             |
56 | 55 | rspcv 3132 |
. . . . . . . . . . . . . . . . . 18

 
                   
   |
57 | 48, 50, 56 | sylc 61 |
. . . . . . . . . . . . . . . . 17
 
                |
58 | 57 | ralrimiva 2809 |
. . . . . . . . . . . . . . . 16
               
  |
59 | | oveq1 6315 |
. . . . . . . . . . . . . . . . . 18
  
      |
60 | 59 | raleqdv 2979 |
. . . . . . . . . . . . . . . . 17
  
 
           
              
   |
61 | 60 | rspcev 3136 |
. . . . . . . . . . . . . . . 16
  
               
              
  |
62 | 37, 58, 61 | sylancr 676 |
. . . . . . . . . . . . . . 15
                   |
63 | | breq2 4399 |
. . . . . . . . . . . . . . . . 17
           
             |
64 | 63 | rexralbidv 2898 |
. . . . . . . . . . . . . . . 16
  
              
               
   |
65 | 64, 22 | elrab2 3186 |
. . . . . . . . . . . . . . 15

   ![[,] [,]](_icc.gif) 
               
   |
66 | 36, 62, 65 | sylanbrc 677 |
. . . . . . . . . . . . . 14
   |
67 | | ne0i 3728 |
. . . . . . . . . . . . . 14
   |
68 | 66, 67 | syl 17 |
. . . . . . . . . . . . 13
   |
69 | | elicc2 11724 |
. . . . . . . . . . . . . . . . . . . 20
 
    ![[,] [,]](_icc.gif)  
    |
70 | 25, 27, 69 | sylancr 676 |
. . . . . . . . . . . . . . . . . . 19
    ![[,] [,]](_icc.gif)  
    |
71 | 70 | biimpa 492 |
. . . . . . . . . . . . . . . . . 18
 
  ![[,] [,]](_icc.gif)       |
72 | 71 | simp2d 1043 |
. . . . . . . . . . . . . . . . 17
 
  ![[,] [,]](_icc.gif)     |
73 | 72 | a1d 25 |
. . . . . . . . . . . . . . . 16
 
  ![[,] [,]](_icc.gif)    
              
   |
74 | 73 | ralrimiva 2809 |
. . . . . . . . . . . . . . 15
    ![[,] [,]](_icc.gif)                   
   |
75 | 22 | raleqi 2977 |
. . . . . . . . . . . . . . . 16
 
    ![[,] [,]](_icc.gif)                      |
76 | | breq2 4399 |
. . . . . . . . . . . . . . . . 17
 
   |
77 | 76 | ralrab2 3192 |
. . . . . . . . . . . . . . . 16
 
   ![[,] [,]](_icc.gif)                 
 
   ![[,] [,]](_icc.gif)                   
   |
78 | 75, 77 | bitri 257 |
. . . . . . . . . . . . . . 15
 
   ![[,] [,]](_icc.gif)                   
   |
79 | 74, 78 | sylibr 217 |
. . . . . . . . . . . . . 14
 
  |
80 | | breq1 4398 |
. . . . . . . . . . . . . . . 16
 
   |
81 | 80 | ralbidv 2829 |
. . . . . . . . . . . . . . 15
  

   |
82 | 81 | rspcev 3136 |
. . . . . . . . . . . . . 14
    
   |
83 | 25, 79, 82 | sylancr 676 |
. . . . . . . . . . . . 13
     |
84 | | infrecl 10612 |
. . . . . . . . . . . . 13
 
  
inf     |
85 | 30, 68, 83, 84 | syl3anc 1292 |
. . . . . . . . . . . 12
 inf     |
86 | 85 | recnd 9687 |
. . . . . . . . . . 11
 inf     |
87 | 86 | adantr 472 |
. . . . . . . . . 10
 
inf    inf     |
88 | | elrp 11327 |
. . . . . . . . . . . . . 14
inf  
inf 
 inf  
   |
89 | 88 | biimpri 211 |
. . . . . . . . . . . . 13
 inf  
inf   
inf     |
90 | 85, 89 | sylan 479 |
. . . . . . . . . . . 12
 
inf    inf     |
91 | | 3z 10994 |
. . . . . . . . . . . 12
 |
92 | | rpexpcl 12329 |
. . . . . . . . . . . 12
 inf    inf        |
93 | 90, 91, 92 | sylancl 675 |
. . . . . . . . . . 11
 
inf    inf        |
94 | 10, 93 | rpmulcld 11380 |
. . . . . . . . . 10
 
inf    
inf 
       |
95 | | cncfi 22004 |
. . . . . . . . . 10
   

           inf 
 
inf              
inf            
            

        inf 
     inf          |
96 | 21, 87, 94, 95 | syl3anc 1292 |
. . . . . . . . 9
 
inf           inf 
  
                     
        inf       inf          |
97 | 85 | ad2antrr 740 |
. . . . . . . . . . . . 13
   inf   
 inf     |
98 | | rphalfcl 11350 |
. . . . . . . . . . . . . 14

    |
99 | 98 | adantl 473 |
. . . . . . . . . . . . 13
   inf   
     |
100 | 97, 99 | ltaddrpd 11394 |
. . . . . . . . . . . 12
   inf   
 inf   inf        |
101 | 99 | rpred 11364 |
. . . . . . . . . . . . . 14
   inf   
     |
102 | 97, 101 | readdcld 9688 |
. . . . . . . . . . . . 13
   inf   
 inf  
     |
103 | 97, 102 | ltnled 9799 |
. . . . . . . . . . . 12
   inf   
 inf  
inf  
  
inf      inf  
   |
104 | 100, 103 | mpbid 215 |
. . . . . . . . . . 11
   inf   
 inf  
   inf     |
105 | | ax-resscn 9614 |
. . . . . . . . . . . . . . 15
 |
106 | 30, 105 | syl6ss 3430 |
. . . . . . . . . . . . . 14

  |
107 | 106 | ad2antrr 740 |
. . . . . . . . . . . . 13
   inf   
   |
108 | | ssralv 3479 |
. . . . . . . . . . . . 13

 
    
inf            
            

        inf 
     inf        
    
inf            
            

        inf 
     inf           |
109 | 107, 108 | syl 17 |
. . . . . . . . . . . 12
   inf   
        inf 
  
                     
        inf       inf        
    
inf            
            

        inf 
     inf           |
110 | 30 | ad2antrr 740 |
. . . . . . . . . . . . . . . . . . 19
   inf   
   |
111 | 110 | sselda 3418 |
. . . . . . . . . . . . . . . . . 18
    inf  
  
  |
112 | 102 | adantr 472 |
. . . . . . . . . . . . . . . . . 18
    inf  
  
inf 
      |
113 | 111, 112 | ltnled 9799 |
. . . . . . . . . . . . . . . . 17
    inf  
  
 inf  
  
inf         |
114 | 85 | ad3antrrr 744 |
. . . . . . . . . . . . . . . . . . . . 21
    inf  
  
inf     |
115 | 101 | adantr 472 |
. . . . . . . . . . . . . . . . . . . . 21
    inf  
  
    |
116 | 114, 115 | resubcld 10068 |
. . . . . . . . . . . . . . . . . . . 20
    inf  
  
inf 
      |
117 | 97, 99 | ltsubrpd 11393 |
. . . . . . . . . . . . . . . . . . . . 21
   inf   
 inf  
   inf 
   |
118 | 117 | adantr 472 |
. . . . . . . . . . . . . . . . . . . 20
    inf  
  
inf 
    inf  
  |
119 | 30 | ad3antrrr 744 |
. . . . . . . . . . . . . . . . . . . . 21
    inf  
  
  |
120 | 83 | ad3antrrr 744 |
. . . . . . . . . . . . . . . . . . . . 21
    inf  
  
    |
121 | | simpr 468 |
. . . . . . . . . . . . . . . . . . . . 21
    inf  
  
  |
122 | | infrelb 10618 |
. . . . . . . . . . . . . . . . . . . . 21
 



inf     |
123 | 119, 120,
121, 122 | syl3anc 1292 |
. . . . . . . . . . . . . . . . . . . 20
    inf  
  
inf     |
124 | 116, 114,
111, 118, 123 | ltletrd 9812 |
. . . . . . . . . . . . . . . . . . 19
    inf  
  
inf 
      |
125 | 111, 114,
115 | absdifltd 13572 |
. . . . . . . . . . . . . . . . . . . 20
    inf  
  
     inf        inf      inf  
       |
126 | 125 | biimprd 231 |
. . . . . . . . . . . . . . . . . . 19
    inf  
  
  inf  
  
inf      
    inf 
        |
127 | 124, 126 | mpand 689 |
. . . . . . . . . . . . . . . . . 18
    inf  
  
 inf  
       inf          |
128 | | rphalflt 11352 |
. . . . . . . . . . . . . . . . . . . 20

    |
129 | 128 | ad2antlr 741 |
. . . . . . . . . . . . . . . . . . 19
    inf  
  
    |
130 | 111, 114 | resubcld 10068 |
. . . . . . . . . . . . . . . . . . . . . 22
    inf  
  
 inf      |
131 | 130 | recnd 9687 |
. . . . . . . . . . . . . . . . . . . . 21
    inf  
  
 inf      |
132 | 131 | abscld 13575 |
. . . . . . . . . . . . . . . . . . . 20
    inf  
  
    inf 
     |
133 | | rpre 11331 |
. . . . . . . . . . . . . . . . . . . . 21

  |
134 | 133 | ad2antlr 741 |
. . . . . . . . . . . . . . . . . . . 20
    inf  
  
  |
135 | | lttr 9728 |
. . . . . . . . . . . . . . . . . . . 20
     
inf      
       inf 
    
       inf        |
136 | 132, 115,
134, 135 | syl3anc 1292 |
. . . . . . . . . . . . . . . . . . 19
    inf  
  
     
inf         
    inf 
      |
137 | 129, 136 | mpan2d 688 |
. . . . . . . . . . . . . . . . . 18
    inf  
  
     inf      
    inf 
      |
138 | 127, 137 | syld 44 |
. . . . . . . . . . . . . . . . 17
    inf  
  
 inf  
       inf        |
139 | 113, 138 | sylbird 243 |
. . . . . . . . . . . . . . . 16
    inf  
  
 inf     
    inf  
     |
140 | 139 | con1d 129 |
. . . . . . . . . . . . . . 15
    inf  
  
     inf  
  inf  
      |
141 | 111 | recnd 9687 |
. . . . . . . . . . . . . . . . . . . 20
    inf  
  
  |
142 | | id 22 |
. . . . . . . . . . . . . . . . . . . . . 22
   |
143 | | oveq1 6315 |
. . . . . . . . . . . . . . . . . . . . . . 23
           |
144 | 143 | oveq2d 6324 |
. . . . . . . . . . . . . . . . . . . . . 22
 
             |
145 | 142, 144 | oveq12d 6326 |
. . . . . . . . . . . . . . . . . . . . 21
          
        |
146 | | eqid 2471 |
. . . . . . . . . . . . . . . . . . . . 21
            
        |
147 | | ovex 6336 |
. . . . . . . . . . . . . . . . . . . . 21
         |
148 | 145, 146,
147 | fvmpt 5963 |
. . . . . . . . . . . . . . . . . . . 20
   

                    |
149 | 141, 148 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
    inf  
  
               
        |
150 | 87 | ad2antrr 740 |
. . . . . . . . . . . . . . . . . . . 20
    inf  
  
inf     |
151 | | id 22 |
. . . . . . . . . . . . . . . . . . . . . 22
 inf  
inf     |
152 | | oveq1 6315 |
. . . . . . . . . . . . . . . . . . . . . . 23
 inf  
    inf        |
153 | 152 | oveq2d 6324 |
. . . . . . . . . . . . . . . . . . . . . 22
 inf  
       inf         |
154 | 151, 153 | oveq12d 6326 |
. . . . . . . . . . . . . . . . . . . . 21
 inf  
 
      inf    inf          |
155 | | ovex 6336 |
. . . . . . . . . . . . . . . . . . . . 21
inf    inf         |
156 | 154, 146,
155 | fvmpt 5963 |
. . . . . . . . . . . . . . . . . . . 20
inf     

        inf 
  inf   
inf 
        |
157 | 150, 156 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
    inf  
  
            inf    inf    inf          |
158 | 149, 157 | oveq12d 6326 |
. . . . . . . . . . . . . . . . . 18
    inf  
  
   

                      inf       
      inf    inf           |
159 | 158 | fveq2d 5883 |
. . . . . . . . . . . . . . . . 17
    inf  
  
                     
        inf           
      inf    inf            |
160 | 159 | breq1d 4405 |
. . . . . . . . . . . . . . . 16
    inf  
  
                               inf  
   
inf 
          
      inf    inf           inf          |
161 | 9 | rpred 11364 |
. . . . . . . . . . . . . . . . . . . . 21
   |
162 | 161 | ad3antrrr 744 |
. . . . . . . . . . . . . . . . . . . 20
    inf  
  
  |
163 | | reexpcl 12327 |
. . . . . . . . . . . . . . . . . . . . 21
 
       |
164 | 111, 15, 163 | sylancl 675 |
. . . . . . . . . . . . . . . . . . . 20
    inf  
  
      |
165 | 162, 164 | remulcld 9689 |
. . . . . . . . . . . . . . . . . . 19
    inf  
  
        |
166 | 111, 165 | resubcld 10068 |
. . . . . . . . . . . . . . . . . 18
    inf  
  
          |
167 | 15 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . 21
    inf  
  
  |
168 | 114, 167 | reexpcld 12471 |
. . . . . . . . . . . . . . . . . . . 20
    inf  
  
inf 
      |
169 | 162, 168 | remulcld 9689 |
. . . . . . . . . . . . . . . . . . 19
    inf  
  
 inf  
      |
170 | 114, 169 | resubcld 10068 |
. . . . . . . . . . . . . . . . . 18
    inf  
  
inf 
  inf          |
171 | 166, 170,
169 | absdifltd 13572 |
. . . . . . . . . . . . . . . . 17
    inf  
  
             inf   
inf 
         inf      
  inf  

inf        
inf 
               
       inf  

inf         inf            |
172 | 169 | recnd 9687 |
. . . . . . . . . . . . . . . . . . . . 21
    inf  
  
 inf  
      |
173 | 150, 172 | npcand 10009 |
. . . . . . . . . . . . . . . . . . . 20
    inf  
  
 inf    inf         inf        inf     |
174 | 173 | breq2d 4407 |
. . . . . . . . . . . . . . . . . . 19
    inf  
  
          inf    inf         inf         
      inf 
    |
175 | | pntlem3.3 |
. . . . . . . . . . . . . . . . . . . . . . 23
 
           |
176 | 175 | ad4ant14 1259 |
. . . . . . . . . . . . . . . . . . . . . 22
    inf  
  
          |
177 | | infrelb 10618 |
. . . . . . . . . . . . . . . . . . . . . 22
 


 
      
inf    
        |
178 | 119, 120,
176, 177 | syl3anc 1292 |
. . . . . . . . . . . . . . . . . . . . 21
    inf  
  
inf    
        |
179 | 114, 166,
178 | lensymd 9803 |
. . . . . . . . . . . . . . . . . . . 20
    inf  
  
        inf  
  |
180 | 179 | pm2.21d 109 |
. . . . . . . . . . . . . . . . . . 19
    inf  
  
         inf  
inf  
      |
181 | 174, 180 | sylbid 223 |
. . . . . . . . . . . . . . . . . 18
    inf  
  
          inf    inf         inf       
inf 
       |
182 | 181 | adantld 474 |
. . . . . . . . . . . . . . . . 17
    inf  
  
   inf    inf        
inf                 
       inf  

inf         inf         inf  
      |
183 | 171, 182 | sylbid 223 |
. . . . . . . . . . . . . . . 16
    inf  
  
             inf   
inf 
         inf       inf         |
184 | 160, 183 | sylbid 223 |
. . . . . . . . . . . . . . 15
    inf  
  
                               inf  
   
inf 
    
inf 
       |
185 | 140, 184 | jad 167 |
. . . . . . . . . . . . . 14
    inf  
  
     
inf            
            

        inf 
     inf        inf  
      |
186 | 185 | ralimdva 2805 |
. . . . . . . . . . . . 13
   inf   
        inf 
  
                     
        inf       inf        
inf     
   |
187 | 68 | ad2antrr 740 |
. . . . . . . . . . . . . 14
   inf   
   |
188 | 83 | ad2antrr 740 |
. . . . . . . . . . . . . 14
   inf   
 
   |
189 | | infregelb 10616 |
. . . . . . . . . . . . . 14
   

 inf        inf      inf    inf     
   |
190 | 110, 187,
188, 102, 189 | syl31anc 1295 |
. . . . . . . . . . . . 13
   inf   
  inf      inf    inf     
   |
191 | 186, 190 | sylibrd 242 |
. . . . . . . . . . . 12
   inf   
        inf 
  
                     
        inf       inf        inf  
   inf      |
192 | 109, 191 | syld 44 |
. . . . . . . . . . 11
   inf   
        inf 
  
                     
        inf       inf        inf  
   inf      |
193 | 104, 192 | mtod 182 |
. . . . . . . . . 10
   inf   
      
inf            
            

        inf 
     inf          |
194 | 193 | nrexdv 2842 |
. . . . . . . . 9
 
inf           inf 
  
                     
        inf       inf          |
195 | 96, 194 | pm2.65da 586 |
. . . . . . . 8
 inf 
   |
196 | 195 | adantr 472 |
. . . . . . 7
 

inf     |
197 | 30 | adantr 472 |
. . . . . . . . . 10
 

  |
198 | 68 | adantr 472 |
. . . . . . . . . 10
 

  |
199 | 83 | adantr 472 |
. . . . . . . . . 10
 

    |
200 | 133 | adantl 473 |
. . . . . . . . . 10
 

  |
201 | | infregelb 10616 |
. . . . . . . . . 10
   

  
inf       |
202 | 197, 198,
199, 200, 201 | syl31anc 1295 |
. . . . . . . . 9
 

 inf  

   |
203 | 22 | raleqi 2977 |
. . . . . . . . . 10
 
    ![[,] [,]](_icc.gif)                      |
204 | | breq2 4399 |
. . . . . . . . . . 11
 
   |
205 | 204 | ralrab2 3192 |
. . . . . . . . . 10
 
   ![[,] [,]](_icc.gif)                 
 
   ![[,] [,]](_icc.gif)                   
   |
206 | 203, 205 | bitri 257 |
. . . . . . . . 9
 
   ![[,] [,]](_icc.gif)                   
   |
207 | 202, 206 | syl6bb 269 |
. . . . . . . 8
 

 inf  
   ![[,] [,]](_icc.gif)                   
    |
208 | | rpgt0 11336 |
. . . . . . . . . 10

  |
209 | 208 | adantl 473 |
. . . . . . . . 9
 

  |
210 | | 0red 9662 |
. . . . . . . . . 10
 

  |
211 | 85 | adantr 472 |
. . . . . . . . . 10
 

inf     |
212 | | ltletr 9743 |
. . . . . . . . . 10
 
inf 
    inf   
inf      |
213 | 210, 200,
211, 212 | syl3anc 1292 |
. . . . . . . . 9
 

 
inf  
 inf 
    |
214 | 209, 213 | mpand 689 |
. . . . . . . 8
 

 inf   inf      |
215 | 207, 214 | sylbird 243 |
. . . . . . 7
 

 
  ![[,] [,]](_icc.gif)                     inf      |
216 | 196, 215 | mtod 182 |
. . . . . 6
 

   ![[,] [,]](_icc.gif)                   
   |
217 | | rexanali 2839 |
. . . . . 6
    ![[,] [,]](_icc.gif)                    
   ![[,] [,]](_icc.gif)                   
   |
218 | 216, 217 | sylibr 217 |
. . . . 5
 

   ![[,] [,]](_icc.gif)                   
   |
219 | | fveq2 5879 |
. . . . . . . . . . . . . . 15
           |
220 | | id 22 |
. . . . . . . . . . . . . . 15
   |
221 | 219, 220 | oveq12d 6326 |
. . . . . . . . . . . . . 14
               |
222 | 221 | fveq2d 5883 |
. . . . . . . . . . . . 13
                       |
223 | 222 | breq1d 4405 |
. . . . . . . . . . . 12
           
             |
224 | 223 | cbvralv 3005 |
. . . . . . . . . . 11
 
                               |
225 | | rpre 11331 |
. . . . . . . . . . . . . . . . 17

  |
226 | 225 | ad2antll 743 |
. . . . . . . . . . . . . . . 16
         ![[,] [,]](_icc.gif)   
 
 
  |
227 | | simprl 772 |
. . . . . . . . . . . . . . . 16
         ![[,] [,]](_icc.gif)   
 
 
  |
228 | | simplr 770 |
. . . . . . . . . . . . . . . . . 18
         ![[,] [,]](_icc.gif)   
 
 
  |
229 | 228 | rpred 11364 |
. . . . . . . . . . . . . . . . 17
         ![[,] [,]](_icc.gif)   
 
 
  |
230 | | elicopnf 11755 |
. . . . . . . . . . . . . . . . 17
    
     |
231 | 229, 230 | syl 17 |
. . . . . . . . . . . . . . . 16
         ![[,] [,]](_icc.gif)   
 
 
    
    |
232 | 226, 227,
231 | mpbir2and 936 |
. . . . . . . . . . . . . . 15
         ![[,] [,]](_icc.gif)   
 
 
     |
233 | | pntlem3.r |
. . . . . . . . . . . . . . . . . . . . . 22
  ψ     |
234 | 233 | pntrval 24479 |
. . . . . . . . . . . . . . . . . . . . 21

     ψ     |
235 | 234 | ad2antll 743 |
. . . . . . . . . . . . . . . . . . . 20
         ![[,] [,]](_icc.gif)   
 
 
     ψ     |
236 | 235 | oveq1d 6323 |
. . . . . . . . . . . . . . . . . . 19
         ![[,] [,]](_icc.gif)   
 
 
        ψ      |
237 | | chpcl 24130 |
. . . . . . . . . . . . . . . . . . . . . 22
 ψ    |
238 | 226, 237 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
         ![[,] [,]](_icc.gif)   
 
 
ψ    |
239 | 238 | recnd 9687 |
. . . . . . . . . . . . . . . . . . . 20
         ![[,] [,]](_icc.gif)   
 
 
ψ    |
240 | | rpcn 11333 |
. . . . . . . . . . . . . . . . . . . . 21

  |
241 | 240 | ad2antll 743 |
. . . . . . . . . . . . . . . . . . . 20
         ![[,] [,]](_icc.gif)   
 
 
  |
242 | | rpne0 11340 |
. . . . . . . . . . . . . . . . . . . . 21

  |
243 | 242 | ad2antll 743 |
. . . . . . . . . . . . . . . . . . . 20
         ![[,] [,]](_icc.gif)   
 
 
  |
244 | 239, 241,
241, 243 | divsubdird 10444 |
. . . . . . . . . . . . . . . . . . 19
         ![[,] [,]](_icc.gif)   
 
 
  ψ      ψ        |
245 | 241, 243 | dividd 10403 |
. . . . . . . . . . . . . . . . . . . 20
         ![[,] [,]](_icc.gif)   
 
 
    |
246 | 245 | oveq2d 6324 |
. . . . . . . . . . . . . . . . . . 19
         ![[,] [,]](_icc.gif)   
 
 
  ψ        ψ      |
247 | 236, 244,
246 | 3eqtrrd 2510 |
. . . . . . . . . . . . . . . . . 18
         ![[,] [,]](_icc.gif)   
 
 
  ψ            |
248 | 247 | fveq2d 5883 |
. . . . . . . . . . . . . . . . 17
         ![[,] [,]](_icc.gif)   
 
 
     ψ                 |
249 | 248 | breq1d 4405 |
. . . . . . . . . . . . . . . 16
         ![[,] [,]](_icc.gif)   
 
 
      ψ    
             |
250 | | simprr 774 |
. . . . . . . . . . . . . . . . . . 19
       ![[,] [,]](_icc.gif) 
 
  |
251 | 250 | ad2antrr 740 |
. . . . . . . . . . . . . . . . . 18
         ![[,] [,]](_icc.gif)   
 
 
  |
252 | 29 | ad2antrr 740 |
. . . . . . . . . . . . . . . . . . . . 21
       ![[,] [,]](_icc.gif) 
 
  ![[,] [,]](_icc.gif)    |
253 | 252 | ad2antrr 740 |
. . . . . . . . . . . . . . . . . . . 20
         ![[,] [,]](_icc.gif)   
 
 
  ![[,] [,]](_icc.gif)    |
254 | | simplrl 778 |
. . . . . . . . . . . . . . . . . . . . 21
   
    ![[,] [,]](_icc.gif)   
   ![[,] [,]](_icc.gif)    |
255 | 254 | adantr 472 |
. . . . . . . . . . . . . . . . . . . 20
         ![[,] [,]](_icc.gif)   
 
 
  ![[,] [,]](_icc.gif)    |
256 | 253, 255 | sseldd 3419 |
. . . . . . . . . . . . . . . . . . 19
         ![[,] [,]](_icc.gif)   
 
 
  |
257 | | simp-4r 785 |
. . . . . . . . . . . . . . . . . . . 20
         ![[,] [,]](_icc.gif)   
 
 
  |
258 | 257 | rpred 11364 |
. . . . . . . . . . . . . . . . . . 19
         ![[,] [,]](_icc.gif)   
 
 
  |
259 | 256, 258 | ltnled 9799 |
. . . . . . . . . . . . . . . . . 18
         ![[,] [,]](_icc.gif)   
 
 

   |
260 | 251, 259 | mpbird 240 |
. . . . . . . . . . . . . . . . 17
         ![[,] [,]](_icc.gif)   
 
 
  |
261 | 225, 237 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23

ψ    |
262 | | rerpdivcl 11353 |
. . . . . . . . . . . . . . . . . . . . . . 23
  ψ  
 ψ     |
263 | 261, 262 | mpancom 682 |
. . . . . . . . . . . . . . . . . . . . . 22

 ψ     |
264 | 263 | ad2antll 743 |
. . . . . . . . . . . . . . . . . . . . 21
         ![[,] [,]](_icc.gif)   
 
 
 ψ     |
265 | | resubcl 9958 |
. . . . . . . . . . . . . . . . . . . . 21
   ψ      ψ      |
266 | 264, 38, 265 | sylancl 675 |
. . . . . . . . . . . . . . . . . . . 20
         ![[,] [,]](_icc.gif)   
 
 
  ψ      |
267 | 266 | recnd 9687 |
. . . . . . . . . . . . . . . . . . 19
         ![[,] [,]](_icc.gif)   
 
 
  ψ      |
268 | 267 | abscld 13575 |
. . . . . . . . . . . . . . . . . 18
         ![[,] [,]](_icc.gif)   
 
 
     ψ       |
269 | | lelttr 9742 |
. . . . . . . . . . . . . . . . . 18
       ψ             ψ           ψ        |
270 | 268, 256,
258, 269 | syl3anc 1292 |
. . . . . . . . . . . . . . . . 17
         ![[,] [,]](_icc.gif)   
 
 
       ψ           ψ        |
271 | 260, 270 | mpan2d 688 |
. . . . . . . . . . . . . . . 16
         ![[,] [,]](_icc.gif)   
 
 
      ψ    
     ψ        |
272 | 249, 271 | sylbird 243 |
. . . . . . . . . . . . . . 15
         ![[,] [,]](_icc.gif)   
 
 
          
     ψ        |
273 | 232, 272 | embantd 55 |
. . . . . . . . . . . . . 14
         ![[,] [,]](_icc.gif)   
 
 
              
      ψ        |
274 | 273 | exp32 616 |
. . . . . . . . . . . . 13
   
    ![[,] [,]](_icc.gif)   
                 
      ψ          |
275 | 274 | com24 89 |
. . . . . . . . . . . 12
   
    ![[,] [,]](_icc.gif)   
               
        ψ          |
276 | 275 | ralimdv2 2804 |
. . . . . . . . . . 11
   
    ![[,] [,]](_icc.gif)   
                
 
     ψ         |
277 | 224, 276 | syl5bi 225 |
. . . . . . . . . 10
   
    ![[,] [,]](_icc.gif)   
                
 
     ψ         |
278 | 277 | reximdva 2858 |
. . . . . . . . 9
       ![[,] [,]](_icc.gif) 
 
 
              
        ψ         |
279 | 278 | anassrs 660 |
. . . . . . . 8
   

  ![[,] [,]](_icc.gif)     
              
        ψ         |
280 | 279 | impancom 447 |
. . . . . . 7
   

  ![[,] [,]](_icc.gif)                  
 
        ψ         |
281 | 280 | expimpd 614 |
. . . . . 6
      ![[,] [,]](_icc.gif)                    
   
     ψ         |
282 | 281 | rexlimdva 2871 |
. . . . 5
 

 
  ![[,] [,]](_icc.gif)                     
       ψ         |
283 | 218, 282 | mpd 15 |
. . . 4
 

        ψ        |
284 | | ssrexv 3480 |
. . . 4

 
       ψ      
 
     ψ         |
285 | 1, 283, 284 | mpsyl 64 |
. . 3
 

        ψ        |
286 | 285 | ralrimiva 2809 |
. 2
   
      ψ        |
287 | 263 | recnd 9687 |
. . . . 5

 ψ     |
288 | 287 | rgen 2766 |
. . . 4
  ψ    |
289 | 288 | a1i 11 |
. . 3
   ψ     |
290 | 1 | a1i 11 |
. . 3
   |
291 | | 1cnd 9677 |
. . 3
   |
292 | 289, 290,
291 | rlim2 13637 |
. 2
    ψ     
        ψ         |
293 | 286, 292 | mpbird 240 |
1
   ψ       |