Step | Hyp | Ref
| Expression |
1 | | caucvgpr.f |
. . . . . . 7
       |
2 | | caucvgpr.cau |
. . . . . . 7
             
            
                  |
3 | | caucvgpr.bnd |
. . . . . . 7
        |
4 | | caucvgpr.lim |
. . . . . . 7
   
               
                  |
5 | 1, 2, 3, 4 | caucvgprlemcl 6647 |
. . . . . 6
   |
6 | | caucvgprlemladd.s |
. . . . . . 7
   |
7 | | nqprlu 6530 |
. . . . . . 7
     
    |
8 | 6, 7 | syl 14 |
. . . . . 6
  
       |
9 | | df-iplp 6451 |
. . . . . . 7


    
             

         
       |
10 | | addclnq 6359 |
. . . . . . 7
 
  
  |
11 | 9, 10 | genpelvu 6496 |
. . . . . 6
      
 
       
             
    
            |
12 | 5, 8, 11 | syl2anc 391 |
. . . . 5
       
             
    
            |
13 | 12 | biimpa 280 |
. . . 4
       
       
                       |
14 | | breq2 3759 |
. . . . . . . . . . . . . . . 16
               
                 |
15 | 14 | rexbidv 2321 |
. . . . . . . . . . . . . . 15
  
             
              
   |
16 | 4 | fveq2i 5124 |
. . . . . . . . . . . . . . . 16
         
                               
    |
17 | | nqex 6347 |
. . . . . . . . . . . . . . . . . 18
 |
18 | 17 | rabex 3892 |
. . . . . . . . . . . . . . . . 17
 
              
 |
19 | 17 | rabex 3892 |
. . . . . . . . . . . . . . . . 17
               
  |
20 | 18, 19 | op2nd 5716 |
. . . . . . . . . . . . . . . 16
                                     
                  
  |
21 | 16, 20 | eqtri 2057 |
. . . . . . . . . . . . . . 15
    

                |
22 | 15, 21 | elrab2 2694 |
. . . . . . . . . . . . . 14
      
                 |
23 | 22 | biimpi 113 |
. . . . . . . . . . . . 13
     
              
   |
24 | 23 | adantr 261 |
. . . . . . . . . . . 12
             
                       |
25 | 24 | adantl 262 |
. . . . . . . . . . 11
        
       
            
     

                 |
26 | 25 | adantr 261 |
. . . . . . . . . 10
   
        
     
   
       
    
    
                 |
27 | 26 | simpld 105 |
. . . . . . . . 9
   
        
     
   
       
    
     |
28 | | vex 2554 |
. . . . . . . . . . . . . 14
 |
29 | | breq2 3759 |
. . . . . . . . . . . . . 14
     |
30 | | ltnqex 6531 |
. . . . . . . . . . . . . . 15
   |
31 | | gtnqex 6532 |
. . . . . . . . . . . . . . 15

  |
32 | 30, 31 | op2nd 5716 |
. . . . . . . . . . . . . 14
    
         |
33 | 28, 29, 32 | elab2 2684 |
. . . . . . . . . . . . 13
        
     |
34 | | ltrelnq 6349 |
. . . . . . . . . . . . . 14
   |
35 | 34 | brel 4335 |
. . . . . . . . . . . . 13


   |
36 | 33, 35 | sylbi 114 |
. . . . . . . . . . . 12
        
       |
37 | 36 | simprd 107 |
. . . . . . . . . . 11
        
     |
38 | 37 | ad2antll 460 |
. . . . . . . . . 10
        
       
            
       |
39 | 38 | adantr 261 |
. . . . . . . . 9
   
        
     
   
       
    
     |
40 | | addclnq 6359 |
. . . . . . . . 9
 
  
  |
41 | 27, 39, 40 | syl2anc 391 |
. . . . . . . 8
   
        
     
   
       
    
       |
42 | | eleq1 2097 |
. . . . . . . . 9
         |
43 | 42 | adantl 262 |
. . . . . . . 8
   
        
     
   
       
    
         |
44 | 41, 43 | mpbird 156 |
. . . . . . 7
   
        
     
   
       
    
     |
45 | 26 | simprd 107 |
. . . . . . . . . 10
   
        
     
   
       
    
                 
  |
46 | | fveq2 5121 |
. . . . . . . . . . . . 13
           |
47 | | opeq1 3540 |
. . . . . . . . . . . . . . 15
         |
48 | 47 | eceq1d 6078 |
. . . . . . . . . . . . . 14
            |
49 | 48 | fveq2d 5125 |
. . . . . . . . . . . . 13
                   |
50 | 46, 49 | oveq12d 5473 |
. . . . . . . . . . . 12
                               |
51 | 50 | breq1d 3765 |
. . . . . . . . . . 11
               
                 |
52 | 51 | cbvrexv 2528 |
. . . . . . . . . 10
 
             
              
  |
53 | 45, 52 | sylib 127 |
. . . . . . . . 9
   
        
     
   
       
    
                 
  |
54 | 33 | biimpi 113 |
. . . . . . . . . . . . . . . . 17
        
     |
55 | 54 | ad2antll 460 |
. . . . . . . . . . . . . . . 16
        
       
            
       |
56 | 55 | adantr 261 |
. . . . . . . . . . . . . . 15
   
        
     
   
       
    
     |
57 | 56 | ad2antrr 457 |
. . . . . . . . . . . . . 14
           
       
            
    
  
     
            |
58 | 6 | ad5antr 465 |
. . . . . . . . . . . . . . 15
           
       
            
    
  
     
            |
59 | 39 | ad2antrr 457 |
. . . . . . . . . . . . . . 15
           
       
            
    
  
     
            |
60 | 1 | ad5antr 465 |
. . . . . . . . . . . . . . . . 17
           
       
            
    
  
     
                |
61 | | simplr 482 |
. . . . . . . . . . . . . . . . 17
           
       
            
    
  
     
            |
62 | 60, 61 | ffvelrnd 5246 |
. . . . . . . . . . . . . . . 16
           
       
            
    
  
     
                |
63 | | nnnq 6405 |
. . . . . . . . . . . . . . . . 17
        |
64 | | recclnq 6376 |
. . . . . . . . . . . . . . . . 17
             
  |
65 | 61, 63, 64 | 3syl 17 |
. . . . . . . . . . . . . . . 16
           
       
            
    
  
     
                 
  |
66 | | addclnq 6359 |
. . . . . . . . . . . . . . . 16
     
                         |
67 | 62, 65, 66 | syl2anc 391 |
. . . . . . . . . . . . . . 15
           
       
            
    
  
     
                          |
68 | | ltanqg 6384 |
. . . . . . . . . . . . . . 15
 
               
                     
             |
69 | 58, 59, 67, 68 | syl3anc 1134 |
. . . . . . . . . . . . . 14
           
       
            
    
  
     
          
                     
             |
70 | 57, 69 | mpbid 135 |
. . . . . . . . . . . . 13
           
       
            
    
  
     
               
               
            |
71 | | simpr 103 |
. . . . . . . . . . . . . 14
           
       
            
    
  
     
                          |
72 | | ltanqg 6384 |
. . . . . . . . . . . . . . . 16
 
         |
73 | 72 | adantl 262 |
. . . . . . . . . . . . . . 15
            
       
            
    
  
     
          
          |
74 | 27 | ad2antrr 457 |
. . . . . . . . . . . . . . 15
           
       
            
    
  
     
            |
75 | | addcomnqg 6365 |
. . . . . . . . . . . . . . . 16
 
  
    |
76 | 75 | adantl 262 |
. . . . . . . . . . . . . . 15
            
       
            
    
  
     
          
   
    |
77 | 73, 67, 74, 59, 76 | caovord2d 5612 |
. . . . . . . . . . . . . 14
           
       
            
    
  
     
               
                              |
78 | 71, 77 | mpbid 135 |
. . . . . . . . . . . . 13
           
       
            
    
  
     
               
              |
79 | | ltsonq 6382 |
. . . . . . . . . . . . . 14
 |
80 | 79, 34 | sotri 4663 |
. . . . . . . . . . . . 13
                
                      
                                 |
81 | 70, 78, 80 | syl2anc 391 |
. . . . . . . . . . . 12
           
       
            
    
  
     
               
              |
82 | | simpllr 486 |
. . . . . . . . . . . 12
           
       
            
    
  
     
              |
83 | 81, 82 | breqtrrd 3781 |
. . . . . . . . . . 11
           
       
            
    
  
     
               
            |
84 | 83 | ex 108 |
. . . . . . . . . 10
             
     
   
       
    
                  
                   |
85 | 84 | reximdva 2415 |
. . . . . . . . 9
   
        
     
   
       
    
    
             
                    |
86 | 53, 85 | mpd 13 |
. . . . . . . 8
   
        
     
   
       
    
                      |
87 | 50 | oveq1d 5470 |
. . . . . . . . . 10
                               
   |
88 | 87 | breq1d 3765 |
. . . . . . . . 9
       
                        
    |
89 | 88 | cbvrexv 2528 |
. . . . . . . 8
 
                      
            |
90 | 86, 89 | sylibr 137 |
. . . . . . 7
   
        
     
   
       
    
                      |
91 | | breq2 3759 |
. . . . . . . . 9
       
                        
    |
92 | 91 | rexbidv 2321 |
. . . . . . . 8
  
     
                
             |
93 | 92 | elrab 2692 |
. . . . . . 7
                    
                    |
94 | 44, 90, 93 | sylanbrc 394 |
. . . . . 6
   
        
     
   
       
    
          
             |
95 | 94 | ex 108 |
. . . . 5
        
       
            
     
                        |
96 | 95 | rexlimdvva 2434 |
. . . 4
       
       
 
     
       
      

                    |
97 | 13, 96 | mpd 13 |
. . 3
       
       
       
             |
98 | 97 | ex 108 |
. 2
       
       

                    |
99 | 98 | ssrdv 2945 |
1
      
                            |