Step | Hyp | Ref
| Expression |
1 | | fveq2 5340 |
. . . . . 6
           |
2 | 1 | breq2d 3879 |
. . . . 5
     
       |
3 | | caucvgprpr.bnd |
. . . . 5
        |
4 | | 1pi 6971 |
. . . . . 6
 |
5 | 4 | a1i 9 |
. . . . 5
   |
6 | 2, 3, 5 | rspcdva 2741 |
. . . 4

      |
7 | | ltrelpr 7161 |
. . . . . 6
   |
8 | 7 | brel 4519 |
. . . . 5
     
       |
9 | 8 | simpld 111 |
. . . 4
       |
10 | 6, 9 | syl 14 |
. . 3
   |
11 | | prop 7131 |
. . . 4
              |
12 | | prml 7133 |
. . . 4
            
      |
13 | 11, 12 | syl 14 |
. . 3
        |
14 | 10, 13 | syl 14 |
. 2
 
      |
15 | | subhalfnqq 7070 |
. . . 4
      |
16 | 15 | ad2antrl 475 |
. . 3
 
       
    |
17 | | simplr 498 |
. . . . . 6
    
         
  |
18 | | archrecnq 7319 |
. . . . . . . 8
            |
19 | 17, 18 | syl 14 |
. . . . . . 7
    
         
           |
20 | | simpr 109 |
. . . . . . . . . . . . . 14
     
      
   
         
          |
21 | | simplr 498 |
. . . . . . . . . . . . . . . 16
     
      
   
         
  |
22 | | nnnq 7078 |
. . . . . . . . . . . . . . . 16
        |
23 | | recclnq 7048 |
. . . . . . . . . . . . . . . 16
             
  |
24 | 21, 22, 23 | 3syl 17 |
. . . . . . . . . . . . . . 15
     
      
   
         
          |
25 | 17 | ad2antrr 473 |
. . . . . . . . . . . . . . 15
     
      
   
         
  |
26 | | ltanqg 7056 |
. . . . . . . . . . . . . . 15
         
                         |
27 | 24, 25, 25, 26 | syl3anc 1181 |
. . . . . . . . . . . . . 14
     
      
   
         
                        |
28 | 20, 27 | mpbid 146 |
. . . . . . . . . . . . 13
     
      
   
         
              |
29 | | simpllr 502 |
. . . . . . . . . . . . 13
     
      
   
         
    |
30 | | ltsonq 7054 |
. . . . . . . . . . . . . 14
 |
31 | | ltrelnq 7021 |
. . . . . . . . . . . . . 14
   |
32 | 30, 31 | sotri 4860 |
. . . . . . . . . . . . 13
                             |
33 | 28, 29, 32 | syl2anc 404 |
. . . . . . . . . . . 12
     
      
   
         
            |
34 | 10 | ad5antr 481 |
. . . . . . . . . . . . 13
     
      
   
         
  |
35 | | simprr 500 |
. . . . . . . . . . . . . 14
 
      
      |
36 | 35 | ad4antr 479 |
. . . . . . . . . . . . 13
     
      
   
         
      |
37 | | prcdnql 7140 |
. . . . . . . . . . . . . 14
                                              |
38 | 11, 37 | sylan 278 |
. . . . . . . . . . . . 13
 
                                 |
39 | 34, 36, 38 | syl2anc 404 |
. . . . . . . . . . . 12
     
      
   
         
                            |
40 | 33, 39 | mpd 13 |
. . . . . . . . . . 11
     
      
   
         
                |
41 | | addclnq 7031 |
. . . . . . . . . . . . 13
         
             |
42 | 25, 24, 41 | syl2anc 404 |
. . . . . . . . . . . 12
     
      
   
         
            |
43 | | nqprl 7207 |
. . . . . . . . . . . 12
           
                 
                            |
44 | 42, 34, 43 | syl2anc 404 |
. . . . . . . . . . 11
     
      
   
         
              
 
                            |
45 | 40, 44 | mpbid 146 |
. . . . . . . . . 10
     
      
   
         
 
                           |
46 | | fveq2 5340 |
. . . . . . . . . . . 12
           |
47 | 46 | breq2d 3879 |
. . . . . . . . . . 11
     
       |
48 | 3 | ad5antr 481 |
. . . . . . . . . . 11
     
      
   
         
       |
49 | 47, 48, 21 | rspcdva 2741 |
. . . . . . . . . 10
     
      
   
         
      |
50 | | ltsopr 7252 |
. . . . . . . . . . 11
 |
51 | 50, 7 | sotri 4860 |
. . . . . . . . . 10
                                                                   |
52 | 45, 49, 51 | syl2anc 404 |
. . . . . . . . 9
     
      
   
         
 
                               |
53 | 52 | ex 114 |
. . . . . . . 8
               

          
                                |
54 | 53 | reximdva 2487 |
. . . . . . 7
    
         
 
       
  
                                |
55 | 19, 54 | mpd 13 |
. . . . . 6
    
         
  
                               |
56 | | oveq1 5697 |
. . . . . . . . . . . 12
                       |
57 | 56 | breq2d 3879 |
. . . . . . . . . . 11
           
             |
58 | 57 | abbidv 2212 |
. . . . . . . . . 10
 
           
             |
59 | 56 | breq1d 3877 |
. . . . . . . . . . 11
           
             |
60 | 59 | abbidv 2212 |
. . . . . . . . . 10
                           |
61 | 58, 60 | opeq12d 3652 |
. . . . . . . . 9
  
                                                      |
62 | 61 | breq1d 3877 |
. . . . . . . 8
                                  
                                |
63 | 62 | rexbidv 2392 |
. . . . . . 7
  
 
                                                                |
64 | | caucvgprpr.lim |
. . . . . . . . 9
    
                              
                                
        |
65 | 64 | fveq2i 5343 |
. . . . . . . 8
         
 
                              
                                
         |
66 | | nqex 7019 |
. . . . . . . . . 10
 |
67 | 66 | rabex 4004 |
. . . . . . . . 9
 
 
                             
 |
68 | 66 | rabex 4004 |
. . . . . . . . 9
                                
       |
69 | 67, 68 | op1st 5955 |
. . . . . . . 8
       
                                
                                          
                               |
70 | 65, 69 | eqtri 2115 |
. . . . . . 7
     
 
                               |
71 | 63, 70 | elrab2 2788 |
. . . . . 6
     
  
                                |
72 | 17, 55, 71 | sylanbrc 409 |
. . . . 5
    
         
      |
73 | 72 | ex 114 |
. . . 4
   
                 |
74 | 73 | reximdva 2487 |
. . 3
 
           
       |
75 | 16, 74 | mpd 13 |
. 2
 
       
      |
76 | 14, 75 | rexlimddv 2507 |
1
 
      |