Step | Hyp | Ref
| Expression |
1 | | cauappcvgpr.f |
. . . . . . 7
       |
2 | | cauappcvgpr.app |
. . . . . . 7
                               |
3 | | cauappcvgpr.bnd |
. . . . . . 7
        |
4 | | cauappcvgpr.lim |
. . . . . . 7
           
          |
5 | 1, 2, 3, 4 | cauappcvgprlemcl 7630 |
. . . . . 6
   |
6 | | cauappcvgprlemladd.s |
. . . . . . 7
   |
7 | | nqprlu 7524 |
. . . . . . 7
          |
8 | 6, 7 | syl 14 |
. . . . . 6
       
  |
9 | | df-iplp 7445 |
. . . . . . 7


            
                
       |
10 | | addclnq 7352 |
. . . . . . 7
 
     |
11 | 9, 10 | genpelvu 7490 |
. . . . . 6
        
       
                               |
12 | 5, 8, 11 | syl2anc 411 |
. . . . 5
       
                               |
13 | 12 | biimpa 296 |
. . . 4
 
     
                      
        |
14 | | breq2 4004 |
. . . . . . . . . . . . . . . 16
       
         |
15 | 14 | rexbidv 2478 |
. . . . . . . . . . . . . . 15
  
     
          |
16 | 4 | fveq2i 5513 |
. . . . . . . . . . . . . . . 16
         
         
          |
17 | | nqex 7340 |
. . . . . . . . . . . . . . . . . 18
 |
18 | 17 | rabex 4144 |
. . . . . . . . . . . . . . . . 17
 
        |
19 | 17 | rabex 4144 |
. . . . . . . . . . . . . . . . 17
        
 |
20 | 18, 19 | op2nd 6141 |
. . . . . . . . . . . . . . . 16
             
            
        |
21 | 16, 20 | eqtri 2198 |
. . . . . . . . . . . . . . 15
     
        |
22 | 15, 21 | elrab2 2896 |
. . . . . . . . . . . . . 14
     
          |
23 | 22 | biimpi 120 |
. . . . . . . . . . . . 13
    
           |
24 | 23 | adantr 276 |
. . . . . . . . . . . 12
             
               |
25 | 24 | adantl 277 |
. . . . . . . . . . 11
        
                    
                |
26 | 25 | adantr 276 |
. . . . . . . . . 10
   
        
                                     |
27 | 26 | simpld 112 |
. . . . . . . . 9
   
        
                            |
28 | | vex 2740 |
. . . . . . . . . . . . . 14
 |
29 | | breq2 4004 |
. . . . . . . . . . . . . 14
 
   |
30 | | ltnqex 7526 |
. . . . . . . . . . . . . . 15
   |
31 | | gtnqex 7527 |
. . . . . . . . . . . . . . 15

  |
32 | 30, 31 | op2nd 6141 |
. . . . . . . . . . . . . 14
    
         |
33 | 28, 29, 32 | elab2 2885 |
. . . . . . . . . . . . 13
        
  
  |
34 | | ltrelnq 7342 |
. . . . . . . . . . . . . 14
   |
35 | 34 | brel 4674 |
. . . . . . . . . . . . 13

    |
36 | 33, 35 | sylbi 121 |
. . . . . . . . . . . 12
        
  
    |
37 | 36 | simprd 114 |
. . . . . . . . . . 11
        
  
  |
38 | 37 | ad2antll 491 |
. . . . . . . . . 10
        
                    
       |
39 | 38 | adantr 276 |
. . . . . . . . 9
   
        
                            |
40 | | addclnq 7352 |
. . . . . . . . 9
 
     |
41 | 27, 39, 40 | syl2anc 411 |
. . . . . . . 8
   
        
                              |
42 | | eleq1 2240 |
. . . . . . . . 9
   
     |
43 | 42 | adantl 277 |
. . . . . . . 8
   
        
                                |
44 | 41, 43 | mpbird 167 |
. . . . . . 7
   
        
                            |
45 | 26 | simprd 114 |
. . . . . . . 8
   
        
                          
        |
46 | 33 | biimpi 120 |
. . . . . . . . . . . . . . . 16
        
  
  |
47 | 46 | ad2antll 491 |
. . . . . . . . . . . . . . 15
        
                    
       |
48 | 47 | adantr 276 |
. . . . . . . . . . . . . 14
   
        
                            |
49 | 48 | ad2antrr 488 |
. . . . . . . . . . . . 13
     
     
                    
    
  
          |
50 | 6 | ad5antr 496 |
. . . . . . . . . . . . . 14
     
     
                    
    
  
       
  |
51 | 39 | ad2antrr 488 |
. . . . . . . . . . . . . 14
     
     
                    
    
  
          |
52 | 1 | ad5antr 496 |
. . . . . . . . . . . . . . . 16
     
     
                    
    
  
              |
53 | | simplr 528 |
. . . . . . . . . . . . . . . 16
     
     
                    
    
  
          |
54 | 52, 53 | ffvelcdmd 5647 |
. . . . . . . . . . . . . . 15
     
     
                    
    
  
              |
55 | | addclnq 7352 |
. . . . . . . . . . . . . . 15
     
         |
56 | 54, 53, 55 | syl2anc 411 |
. . . . . . . . . . . . . 14
     
     
                    
    
  
                |
57 | | ltanqg 7377 |
. . . . . . . . . . . . . 14
 
                           |
58 | 50, 51, 56, 57 | syl3anc 1238 |
. . . . . . . . . . . . 13
     
     
                    
    
  
                            |
59 | 49, 58 | mpbid 147 |
. . . . . . . . . . . 12
     
     
                    
    
  
                          |
60 | | simpr 110 |
. . . . . . . . . . . . 13
     
     
                    
    
  
                |
61 | | ltanqg 7377 |
. . . . . . . . . . . . . . 15
 
 
       |
62 | 61 | adantl 277 |
. . . . . . . . . . . . . 14
            
                    
    
  
        
 
        |
63 | 27 | ad2antrr 488 |
. . . . . . . . . . . . . 14
     
     
                    
    
  
          |
64 | | addcomnqg 7358 |
. . . . . . . . . . . . . . 15
 
       |
65 | 64 | adantl 277 |
. . . . . . . . . . . . . 14
            
                    
    
  
          
      |
66 | 62, 56, 63, 51, 65 | caovord2d 6037 |
. . . . . . . . . . . . 13
     
     
                    
    
  
                            |
67 | 60, 66 | mpbid 147 |
. . . . . . . . . . . 12
     
     
                    
    
  
                    |
68 | | ltsonq 7375 |
. . . . . . . . . . . . 13
 |
69 | 68, 34 | sotri 5019 |
. . . . . . . . . . . 12
                                         |
70 | 59, 67, 69 | syl2anc 411 |
. . . . . . . . . . 11
     
     
                    
    
  
                    |
71 | | simpllr 534 |
. . . . . . . . . . 11
     
     
                    
    
  
            |
72 | 70, 71 | breqtrrd 4028 |
. . . . . . . . . 10
     
     
                    
    
  
                  |
73 | 72 | ex 115 |
. . . . . . . . 9
             
                         
                   |
74 | 73 | reximdva 2579 |
. . . . . . . 8
   
        
                                              |
75 | 45, 74 | mpd 13 |
. . . . . . 7
   
        
                          
          |
76 | | breq2 4004 |
. . . . . . . . 9
         
           |
77 | 76 | rexbidv 2478 |
. . . . . . . 8
  
       
            |
78 | 17 | rabex 4144 |
. . . . . . . . 9
 
          |
79 | 17 | rabex 4144 |
. . . . . . . . 9
          
 |
80 | 78, 79 | op2nd 6141 |
. . . . . . . 8
                              
          |
81 | 77, 80 | elrab2 2896 |
. . . . . . 7
      
          
                         |
82 | 44, 75, 81 | sylanbrc 417 |
. . . . . 6
   
        
                                                         |
83 | 82 | ex 115 |
. . . . 5
        
                    
             
           
              |
84 | 83 | rexlimdvva 2602 |
. . . 4
 
     
         
          
                                         |
85 | 13, 84 | mpd 13 |
. . 3
 
     
             
          
              |
86 | 85 | ex 115 |
. 2
       
      
     
           
              |
87 | 86 | ssrdv 3161 |
1
      
      
                
              |