Step | Hyp | Ref
| Expression |
1 | | breq2 4406 |
. . . . . . . . . . 11
             
               |
2 | 1 | imbi2d 318 |
. . . . . . . . . 10
                                         |
3 | 2 | 2ralbidv 2832 |
. . . . . . . . 9
  

                  

                     |
4 | 3 | rexbidv 2901 |
. . . . . . . 8
  


                 
       
                |
5 | 4 | cbvralv 3019 |
. . . . . . 7
 
       
            
   
                    |
6 | | r19.12 2916 |
. . . . . . . 8
  

                  


                    |
7 | 6 | ralimi 2781 |
. . . . . . 7
 
       
                                     |
8 | 5, 7 | sylbi 199 |
. . . . . 6
 
       
                                     |
9 | | rphalfcl 11327 |
. . . . . . . . 9

    |
10 | | breq2 4406 |
. . . . . . . . . . . . . . . 16
               
                 |
11 | 10 | imbi2d 318 |
. . . . . . . . . . . . . . 15
                                             |
12 | 11 | ralbidv 2827 |
. . . . . . . . . . . . . 14
    
                  
                       |
13 | 12 | rexbidv 2901 |
. . . . . . . . . . . . 13
    

                 
      
                  |
14 | 13 | ralbidv 2827 |
. . . . . . . . . . . 12
    


                 

      
                  |
15 | 14 | rspcva 3148 |
. . . . . . . . . . 11
    

      
              


                      |
16 | | heicant.j |
. . . . . . . . . . . . . . 15
       |
17 | 16 | ad3antrrr 736 |
. . . . . . . . . . . . . 14
                                 
      |
18 | | heicant.c |
. . . . . . . . . . . . . . . . . . . . . . . 24
        |
19 | 18 | ad2antrr 732 |
. . . . . . . . . . . . . . . . . . . . . . 23
       

       |
20 | 19 | anim1i 572 |
. . . . . . . . . . . . . . . . . . . . . 22
          
         |
21 | | rphalfcl 11327 |
. . . . . . . . . . . . . . . . . . . . . . 23

    |
22 | 21 | rpxrd 11342 |
. . . . . . . . . . . . . . . . . . . . . 22

    |
23 | | eqid 2451 |
. . . . . . . . . . . . . . . . . . . . . . . 24
         |
24 | 23 | blopn 21515 |
. . . . . . . . . . . . . . . . . . . . . . 23
                          |
25 | 24 | 3expa 1208 |
. . . . . . . . . . . . . . . . . . . . . 22
       
                    |
26 | 20, 22, 25 | syl2an 480 |
. . . . . . . . . . . . . . . . . . . . 21
           

                |
27 | 26 | adantr 467 |
. . . . . . . . . . . . . . . . . . . 20
     
        
                    
                |
28 | 21 | rpgt0d 11344 |
. . . . . . . . . . . . . . . . . . . . . . 23

    |
29 | 22, 28 | jca 535 |
. . . . . . . . . . . . . . . . . . . . . 22

  
     |
30 | | xblcntr 21426 |
. . . . . . . . . . . . . . . . . . . . . . 23
             
            |
31 | 30 | 3expa 1208 |
. . . . . . . . . . . . . . . . . . . . . 22
       
       
            |
32 | 20, 29, 31 | syl2an 480 |
. . . . . . . . . . . . . . . . . . . . 21
           

            |
33 | 32 | adantr 467 |
. . . . . . . . . . . . . . . . . . . 20
     
        
                    
            |
34 | | opelxpi 4866 |
. . . . . . . . . . . . . . . . . . . . . . 23
              |
35 | 21, 34 | sylan2 477 |
. . . . . . . . . . . . . . . . . . . . . 22
 
          |
36 | 35 | ad4ant23 1239 |
. . . . . . . . . . . . . . . . . . . . 21
     
        
                    
         |
37 | | rpcn 11310 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28

  |
38 | 37 | 2halvesd 10858 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27

        |
39 | 38 | breq2d 4414 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26

          
       |
40 | 39 | imbi1d 319 |
. . . . . . . . . . . . . . . . . . . . . . . . 25

                                                  |
41 | 40 | ralbidv 2827 |
. . . . . . . . . . . . . . . . . . . . . . . 24

 
                          
                       |
42 | | oveq2 6298 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
           |
43 | 42 | breq1d 4412 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
     
       |
44 | | fveq2 5865 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
           |
45 | 44 | oveq2d 6306 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
                           |
46 | 45 | breq1d 4412 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
               
                 |
47 | 43, 46 | imbi12d 322 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
                                             |
48 | 47 | cbvralv 3019 |
. . . . . . . . . . . . . . . . . . . . . . . 24
 
                    
                      |
49 | 41, 48 | syl6bb 265 |
. . . . . . . . . . . . . . . . . . . . . . 23

 
                          
                       |
50 | 49 | biimpar 488 |
. . . . . . . . . . . . . . . . . . . . . 22
  
                    

                            |
51 | 50 | adantll 720 |
. . . . . . . . . . . . . . . . . . . . 21
     
        
                    

                            |
52 | | vex 3048 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
 |
53 | | ovex 6318 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
   |
54 | 52, 53 | op1std 6803 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
            |
55 | 52, 53 | op2ndd 6804 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
              |
56 | 54, 55 | oveq12d 6308 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
                                  |
57 | 56 | eqcomd 2457 |
. . . . . . . . . . . . . . . . . . . . . . . 24
                                  |
58 | 57 | biantrurd 511 |
. . . . . . . . . . . . . . . . . . . . . . 23
       
                  
                                              
                  
                       |
59 | 54 | oveq1d 6305 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
                    |
60 | 55, 55 | oveq12d 6308 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
                        |
61 | 59, 60 | breq12d 4415 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
                        
             |
62 | 54 | fveq2d 5869 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
                    |
63 | 62 | oveq1d 6305 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
                                    |
64 | 63 | breq1d 4412 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
                                          |
65 | 61, 64 | imbi12d 322 |
. . . . . . . . . . . . . . . . . . . . . . . 24
                         
                             
                  |
66 | 65 | ralbidv 2827 |
. . . . . . . . . . . . . . . . . . . . . . 23
       
                  
                                                 |
67 | 58, 66 | bitr3d 259 |
. . . . . . . . . . . . . . . . . . . . . 22
                                  
                  
                   

                             |
68 | 67 | rspcev 3150 |
. . . . . . . . . . . . . . . . . . . . 21
                    
                
                              
                  
                      |
69 | 36, 51, 68 | syl2anc 667 |
. . . . . . . . . . . . . . . . . . . 20
     
        
                    
                               
                  
                      |
70 | | eleq2 2518 |
. . . . . . . . . . . . . . . . . . . . . 22
           
             |
71 | | eqeq1 2455 |
. . . . . . . . . . . . . . . . . . . . . . . 24
                           
                             |
72 | 71 | anbi1d 711 |
. . . . . . . . . . . . . . . . . . . . . . 23
                             
                  
                   
                           
                  
                       |
73 | 72 | rexbidv 2901 |
. . . . . . . . . . . . . . . . . . . . . 22
            
                                       
                   
                               
                  
                       |
74 | 70, 73 | anbi12d 717 |
. . . . . . . . . . . . . . . . . . . . 21
                                  
                  
                    
                                          
                  
                        |
75 | 74 | rspcev 3150 |
. . . . . . . . . . . . . . . . . . . 20
               
                                          
                  
                                                                     
                       |
76 | 27, 33, 69, 75 | syl12anc 1266 |
. . . . . . . . . . . . . . . . . . 19
     
        
                    
                            
                  
                       |
77 | 76 | ex 436 |
. . . . . . . . . . . . . . . . . 18
           

 
                                                                   
                        |
78 | 77 | rexlimdva 2879 |
. . . . . . . . . . . . . . . . 17
          
 

                    
                                              
                        |
79 | 78 | ralimdva 2796 |
. . . . . . . . . . . . . . . 16
       
                          
                                              
                        |
80 | 79 | imp 431 |
. . . . . . . . . . . . . . 15
                                 

                            
                  
                       |
81 | 23 | mopnuni 21456 |
. . . . . . . . . . . . . . . . . 18
             |
82 | 18, 81 | syl 17 |
. . . . . . . . . . . . . . . . 17
        |
83 | 82 | raleqdv 2993 |
. . . . . . . . . . . . . . . 16
                               
                  
                    
                                   
                  
                        |
84 | 83 | ad3antrrr 736 |
. . . . . . . . . . . . . . 15
                                 
 

      
                                       
                    
                                   
                  
                        |
85 | 80, 84 | mpbid 214 |
. . . . . . . . . . . . . 14
                                 
                                   
                  
                       |
86 | | eqid 2451 |
. . . . . . . . . . . . . . 15
           |
87 | | fveq2 5865 |
. . . . . . . . . . . . . . . . . 18
                   |
88 | | fveq2 5865 |
. . . . . . . . . . . . . . . . . 18
                   |
89 | 87, 88 | oveq12d 6308 |
. . . . . . . . . . . . . . . . 17
                                               |
90 | 89 | eqeq2d 2461 |
. . . . . . . . . . . . . . . 16
                     
                           |
91 | 87 | oveq1d 6305 |
. . . . . . . . . . . . . . . . . . 19
                           |
92 | 88, 88 | oveq12d 6308 |
. . . . . . . . . . . . . . . . . . 19
                                   |
93 | 91, 92 | breq12d 4415 |
. . . . . . . . . . . . . . . . . 18
                                                         |
94 | 87 | fveq2d 5869 |
. . . . . . . . . . . . . . . . . . . 20
                           |
95 | 94 | oveq1d 6305 |
. . . . . . . . . . . . . . . . . . 19
                                           |
96 | 95 | breq1d 4412 |
. . . . . . . . . . . . . . . . . 18
                       
                         |
97 | 93, 96 | imbi12d 322 |
. . . . . . . . . . . . . . . . 17
                                           
                              
                          |
98 | 97 | ralbidv 2827 |
. . . . . . . . . . . . . . . 16
      
                                     

                              
                          |
99 | 90, 98 | anbi12d 717 |
. . . . . . . . . . . . . . 15
                       
                  
                   
                                                        
                           |
100 | 86, 99 | cmpcovf 20406 |
. . . . . . . . . . . . . 14
     
                                   
                  
                            
                                            
                              
                            |
101 | 17, 85, 100 | syl2anc 667 |
. . . . . . . . . . . . 13
                                 
                         
                                                        
                            |
102 | 101 | ex 436 |
. . . . . . . . . . . 12
       
                               
                                            
                              
                             |
103 | | elinel2 3620 |
. . . . . . . . . . . . . 14
          |
104 | | simpll 760 |
. . . . . . . . . . . . . . . . . . . . 21
       
   |
105 | 104 | anim1i 572 |
. . . . . . . . . . . . . . . . . . . 20
           
   |
106 | | frn 5735 |
. . . . . . . . . . . . . . . . . . . . . . . 24
           |
107 | | rnss 5063 |
. . . . . . . . . . . . . . . . . . . . . . . 24

 
    |
108 | 106, 107 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
      
    |
109 | | rnxpss 5269 |
. . . . . . . . . . . . . . . . . . . . . . 23
   |
110 | 108, 109 | syl6ss 3444 |
. . . . . . . . . . . . . . . . . . . . . 22
      
  |
111 | 110 | adantl 468 |
. . . . . . . . . . . . . . . . . . . . 21
   
       
      
  |
112 | | simplr 762 |
. . . . . . . . . . . . . . . . . . . . . . 23
             |
113 | | ffun 5731 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
         |
114 | | vex 3048 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
 |
115 | 114 | fundmen 7643 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28

  |
116 | 115 | ensymd 7620 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27

  |
117 | 113, 116 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
         |
118 | | fdm 5733 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
      
  |
119 | 117, 118 | breqtrd 4427 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
         |
120 | | enfii 7789 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
     |
121 | 119, 120 | sylan2 477 |
. . . . . . . . . . . . . . . . . . . . . . . 24
           |
122 | | rnfi 7857 |
. . . . . . . . . . . . . . . . . . . . . . . 24

  |
123 | | rnfi 7857 |
. . . . . . . . . . . . . . . . . . . . . . . 24
   |
124 | 121, 122,
123 | 3syl 18 |
. . . . . . . . . . . . . . . . . . . . . . 23
           |
125 | 112, 124 | sylan 474 |
. . . . . . . . . . . . . . . . . . . . . 22
   
       
         |
126 | 118 | adantl 468 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
                
  |
127 | | eqtr 2470 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
             
   |
128 | 82, 127 | sylan 474 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
 
      
   |
129 | | heicant.x |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
   |
130 | 129 | adantr 467 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
 
         |
131 | 128, 130 | eqnetrrd 2692 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
 
       
  |
132 | | unieq 4206 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30

    |
133 | | uni0 4225 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
  |
134 | 132, 133 | syl6eq 2501 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29

   |
135 | 134 | necon3i 2656 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
 
  |
136 | 131, 135 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
 
         |
137 | 136 | adantr 467 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
                   |
138 | 126, 137 | eqnetrd 2691 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
                
  |
139 | | dm0rn0 5051 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26

  |
140 | 139 | necon3bii 2676 |
. . . . . . . . . . . . . . . . . . . . . . . . 25

  |
141 | 138, 140 | sylib 200 |
. . . . . . . . . . . . . . . . . . . . . . . 24
                
  |
142 | | relxp 4942 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
   |
143 | | relss 4922 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27

    
   |
144 | 106, 142,
143 | mpisyl 21 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
         |
145 | | relrn0 5092 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
 
   |
146 | 145 | necon3bid 2668 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
 
   |
147 | 144, 146 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
       
   |
148 | 147 | adantl 468 |
. . . . . . . . . . . . . . . . . . . . . . . 24
                 
   |
149 | 141, 148 | mpbid 214 |
. . . . . . . . . . . . . . . . . . . . . . 23
                   |
150 | 149 | adantllr 725 |
. . . . . . . . . . . . . . . . . . . . . 22
   
       
         |
151 | | rpssre 11312 |
. . . . . . . . . . . . . . . . . . . . . . 23
 |
152 | 111, 151 | syl6ss 3444 |
. . . . . . . . . . . . . . . . . . . . . 22
   
       
      
  |
153 | | ltso 9714 |
. . . . . . . . . . . . . . . . . . . . . . 23
 |
154 | | fiinfcl 8017 |
. . . . . . . . . . . . . . . . . . . . . . 23
 
  inf 
   |
155 | 153, 154 | mpan 676 |
. . . . . . . . . . . . . . . . . . . . . 22
 
 inf
 
  |
156 | 125, 150,
152, 155 | syl3anc 1268 |
. . . . . . . . . . . . . . . . . . . . 21
   
       
       inf     |
157 | 111, 156 | sseldd 3433 |
. . . . . . . . . . . . . . . . . . . 20
   
       
       inf     |
158 | 105, 157 | sylanl1 656 |
. . . . . . . . . . . . . . . . . . 19
     
                     inf
 
  |
159 | 158 | adantr 467 |
. . . . . . . . . . . . . . . . . 18
           

       
       
                         
                              
                         inf
 
  |
160 | 82 | ad3antrrr 736 |
. . . . . . . . . . . . . . . . . . . . . . 23
                  |
161 | 160 | anim1i 572 |
. . . . . . . . . . . . . . . . . . . . . 22
                   
              |
162 | 161 | ad2antrr 732 |
. . . . . . . . . . . . . . . . . . . . 21
           

       
       
                         
                              
                                        |
163 | | simpl 459 |
. . . . . . . . . . . . . . . . . . . . 21
 
   |
164 | 127 | eleq2d 2514 |
. . . . . . . . . . . . . . . . . . . . . . 23
                   |
165 | | eluni2 4202 |
. . . . . . . . . . . . . . . . . . . . . . 23
 

  |
166 | 164, 165 | syl6bb 265 |
. . . . . . . . . . . . . . . . . . . . . 22
                   |
167 | 166 | biimpa 487 |
. . . . . . . . . . . . . . . . . . . . 21
              
 
  |
168 | 162, 163,
167 | syl2an 480 |
. . . . . . . . . . . . . . . . . . . 20
                                                       
                              
                         
  
  |
169 | | nfv 1761 |
. . . . . . . . . . . . . . . . . . . . . . 23
           

       
        |
170 | | nfra1 2769 |
. . . . . . . . . . . . . . . . . . . . . . 23
                            
                              
                         |
171 | 169, 170 | nfan 2011 |
. . . . . . . . . . . . . . . . . . . . . 22
                                                       
                              
                          |
172 | | nfv 1761 |
. . . . . . . . . . . . . . . . . . . . . 22
  
  |
173 | 171, 172 | nfan 2011 |
. . . . . . . . . . . . . . . . . . . . 21
                                                        
                              
                         
   |
174 | | nfv 1761 |
. . . . . . . . . . . . . . . . . . . . 21
       inf                 |
175 | | rspa 2755 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
                            
                              
                                                  
                              
                          |
176 | | oveq2 6298 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
                           |
177 | 176 | breq1d 4412 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
                                                                 |
178 | | fveq2 5865 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
           |
179 | 178 | oveq2d 6306 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
                                           |
180 | 179 | breq1d 4412 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
                       
                         |
181 | 177, 180 | imbi12d 322 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
                                                       
                              
                          |
182 | 181 | rspcva 3148 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
                                 
                                                      
                         |
183 | | oveq2 6298 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
                           |
184 | 183 | breq1d 4412 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
                                                                 |
185 | 44 | oveq2d 6306 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
                                           |
186 | 185 | breq1d 4412 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
                       
                         |
187 | 184, 186 | imbi12d 322 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
                                                       
                              
                          |
188 | 187 | rspcva 3148 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
                                 
                                                      
                         |
189 | 182, 188 | anim12i 570 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
                                                           
                                                                                        
                                                     
                          |
190 | 189 | anandirs 840 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
  


                              
                                                                                                             
                          |
191 | | prth 575 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
                                                                                      
                                                                                                                                        |
192 | 190, 191 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
  


                              
                                                                                                                                        |
193 | 192 | adantrl 722 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
  

                                                        
                                                                                                                                         |
194 | 193 | ad4ant23 1239 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
                              
                           
                              
                                                                                                                                            |
195 | | simpll 760 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
                    
    
   |
196 | 195 | anim1i 572 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
     
                                       |
197 | 196 | anim1i 572 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
           

       
       
 
                 
    |
198 | 110, 151 | syl6ss 3444 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
      
  |
199 | 198 | adantr 467 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
       

  |
200 | | 0re 9643 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
 |
201 | | rpge0 11314 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40

  |
202 | 201 | rgen 2747 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
  |
203 | | ssralv 3493 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
   
    |
204 | 110, 202,
203 | mpisyl 21 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
       
   |
205 | | breq1 4405 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
 
   |
206 | 205 | ralbidv 2827 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
  
     |
207 | 206 | rspcev 3150 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
    
    |
208 | 200, 204,
207 | sylancr 669 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
           |
209 | 208 | adantr 467 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
       

    |
210 | 144 | adantr 467 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
       

  |
211 | | ffn 5728 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
         |
212 | | fnfvelrn 6019 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
 
       |
213 | 211, 212 | sylan 474 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
       

      |
214 | | 2ndrn 6841 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
 
    
          |
215 | 210, 213,
214 | syl2anc 667 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
       

          |
216 | | infrelb 10596 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
 
 
         inf             |
217 | 199, 209,
215, 216 | syl3anc 1268 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
       

inf  
          |
218 | 217 | adantll 720 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
                   inf             |
219 | 218 | ad2ant2r 753 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
     
             
  
 
inf  
          |
220 | 18 | ad3antrrr 736 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
                        |
221 | | xmetcl 21346 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
      

      |
222 | 221 | 3expb 1209 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
                |
223 | 220, 222 | sylan 474 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
                  
 
      |
224 | 223 | adantr 467 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
     
             
  
 
      |
225 | | simplr 762 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
                  
 
        |
226 | | simpl 459 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
 
   |
227 | | ne0i 3737 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
        
  |
228 | 215, 227 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
       

  |
229 | | infrecl 10590 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
 
   inf     |
230 | 199, 228,
209, 229 | syl3anc 1268 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
       

inf     |
231 | 230 | rexrd 9690 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
       

inf     |
232 | 225, 226,
231 | syl2an 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
     
             
  
 
inf     |
233 | | simpr 463 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
                         |
234 | 233 | ffvelrnda 6022 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
                           |
235 | | xp2nd 6824 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
      
          |
236 | 234, 235 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
                             |
237 | 236 | rpxrd 11342 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
                             |
238 | 237 | ad2ant2r 753 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
     
             
  
 
          |
239 | | xrltletr 11454 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
      inf                  inf
 
inf
 
                        |
240 | 224, 232,
238, 239 | syl3anc 1268 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
     
             
  
 
     
inf  
inf  
                        |
241 | 219, 240 | mpan2d 680 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
     
             
  
 
     inf 

               |
242 | 241 | adantlr 721 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
           
        
                                   inf                  |
243 | 18 | ad6antr 742 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
           
        
                             
       |
244 | | simpllr 769 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
     
             
                                   |
245 | | ffvelrn 6020 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
       

        |
246 | | xp1st 6823 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
      
          |
247 | 245, 246 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
       

          |
248 | 244, 226,
247 | syl2an 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
           
        
                                        |
249 | | simpr 463 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
 
   |
250 | 249 | ad3antlr 737 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
           
        
                             
  |
251 | | xmetcl 21346 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
              
               |
252 | 243, 248,
250, 251 | syl3anc 1268 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
           
        
                                            |
253 | 252 | adantr 467 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
                     
 
                                                       |
254 | 245, 235 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
       

          |
255 | 225, 254 | sylan 474 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
     
             
             |
256 | 255 | ad2ant2r 753 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
           
        
                        ![]() |