Step | Hyp | Ref
| Expression |
1 | | fveq2 5527 |
. . . . . 6
           |
2 | 1 | breq2d 4027 |
. . . . 5
     
       |
3 | | caucvgprpr.bnd |
. . . . 5
        |
4 | | 1pi 7327 |
. . . . . 6
 |
5 | 4 | a1i 9 |
. . . . 5
   |
6 | 2, 3, 5 | rspcdva 2858 |
. . . 4

      |
7 | | ltrelpr 7517 |
. . . . . 6
   |
8 | 7 | brel 4690 |
. . . . 5
     
       |
9 | 8 | simpld 112 |
. . . 4
       |
10 | 6, 9 | syl 14 |
. . 3
   |
11 | | prop 7487 |
. . . 4
              |
12 | | prml 7489 |
. . . 4
            
      |
13 | 11, 12 | syl 14 |
. . 3
        |
14 | 10, 13 | syl 14 |
. 2
 
      |
15 | | subhalfnqq 7426 |
. . . 4
      |
16 | 15 | ad2antrl 490 |
. . 3
 
       
    |
17 | | simplr 528 |
. . . . . 6
    
         
  |
18 | | archrecnq 7675 |
. . . . . . . 8
            |
19 | 17, 18 | syl 14 |
. . . . . . 7
    
         
           |
20 | | simpr 110 |
. . . . . . . . . . . . . 14
     
      
   
         
          |
21 | | simplr 528 |
. . . . . . . . . . . . . . . 16
     
      
   
         
  |
22 | | nnnq 7434 |
. . . . . . . . . . . . . . . 16
        |
23 | | recclnq 7404 |
. . . . . . . . . . . . . . . 16
             
  |
24 | 21, 22, 23 | 3syl 17 |
. . . . . . . . . . . . . . 15
     
      
   
         
          |
25 | 17 | ad2antrr 488 |
. . . . . . . . . . . . . . 15
     
      
   
         
  |
26 | | ltanqg 7412 |
. . . . . . . . . . . . . . 15
         
                         |
27 | 24, 25, 25, 26 | syl3anc 1248 |
. . . . . . . . . . . . . 14
     
      
   
         
                        |
28 | 20, 27 | mpbid 147 |
. . . . . . . . . . . . 13
     
      
   
         
              |
29 | | simpllr 534 |
. . . . . . . . . . . . 13
     
      
   
         
    |
30 | | ltsonq 7410 |
. . . . . . . . . . . . . 14
 |
31 | | ltrelnq 7377 |
. . . . . . . . . . . . . 14
   |
32 | 30, 31 | sotri 5036 |
. . . . . . . . . . . . 13
                             |
33 | 28, 29, 32 | syl2anc 411 |
. . . . . . . . . . . 12
     
      
   
         
            |
34 | 10 | ad5antr 496 |
. . . . . . . . . . . . 13
     
      
   
         
  |
35 | | simprr 531 |
. . . . . . . . . . . . . 14
 
      
      |
36 | 35 | ad4antr 494 |
. . . . . . . . . . . . 13
     
      
   
         
      |
37 | | prcdnql 7496 |
. . . . . . . . . . . . . 14
                                              |
38 | 11, 37 | sylan 283 |
. . . . . . . . . . . . 13
 
                                 |
39 | 34, 36, 38 | syl2anc 411 |
. . . . . . . . . . . 12
     
      
   
         
                            |
40 | 33, 39 | mpd 13 |
. . . . . . . . . . 11
     
      
   
         
                |
41 | | addclnq 7387 |
. . . . . . . . . . . . 13
         
             |
42 | 25, 24, 41 | syl2anc 411 |
. . . . . . . . . . . 12
     
      
   
         
            |
43 | | nqprl 7563 |
. . . . . . . . . . . 12
           
                 
                            |
44 | 42, 34, 43 | syl2anc 411 |
. . . . . . . . . . 11
     
      
   
         
              
 
                            |
45 | 40, 44 | mpbid 147 |
. . . . . . . . . 10
     
      
   
         
 
                           |
46 | | fveq2 5527 |
. . . . . . . . . . . 12
           |
47 | 46 | breq2d 4027 |
. . . . . . . . . . 11
     
       |
48 | 3 | ad5antr 496 |
. . . . . . . . . . 11
     
      
   
         
       |
49 | 47, 48, 21 | rspcdva 2858 |
. . . . . . . . . 10
     
      
   
         
      |
50 | | ltsopr 7608 |
. . . . . . . . . . 11
 |
51 | 50, 7 | sotri 5036 |
. . . . . . . . . 10
                                                                   |
52 | 45, 49, 51 | syl2anc 411 |
. . . . . . . . 9
     
      
   
         
 
                               |
53 | 52 | ex 115 |
. . . . . . . 8
               

          
                                |
54 | 53 | reximdva 2589 |
. . . . . . 7
    
         
 
       
  
                                |
55 | 19, 54 | mpd 13 |
. . . . . 6
    
         
  
                               |
56 | | oveq1 5895 |
. . . . . . . . . . . 12
                       |
57 | 56 | breq2d 4027 |
. . . . . . . . . . 11
           
             |
58 | 57 | abbidv 2305 |
. . . . . . . . . 10
 
           
             |
59 | 56 | breq1d 4025 |
. . . . . . . . . . 11
           
             |
60 | 59 | abbidv 2305 |
. . . . . . . . . 10
                           |
61 | 58, 60 | opeq12d 3798 |
. . . . . . . . 9
  
                                                      |
62 | 61 | breq1d 4025 |
. . . . . . . 8
                                  
                                |
63 | 62 | rexbidv 2488 |
. . . . . . 7
  
 
                                                                |
64 | | caucvgprpr.lim |
. . . . . . . . 9
    
                              
                                
        |
65 | 64 | fveq2i 5530 |
. . . . . . . 8
         
 
                              
                                
         |
66 | | nqex 7375 |
. . . . . . . . . 10
 |
67 | 66 | rabex 4159 |
. . . . . . . . 9
 
 
                             
 |
68 | 66 | rabex 4159 |
. . . . . . . . 9
                                
       |
69 | 67, 68 | op1st 6160 |
. . . . . . . 8
       
                                
                                          
                               |
70 | 65, 69 | eqtri 2208 |
. . . . . . 7
     
 
                               |
71 | 63, 70 | elrab2 2908 |
. . . . . 6
     
  
                                |
72 | 17, 55, 71 | sylanbrc 417 |
. . . . 5
    
         
      |
73 | 72 | ex 115 |
. . . 4
   
                 |
74 | 73 | reximdva 2589 |
. . 3
 
           
       |
75 | 16, 74 | mpd 13 |
. 2
 
       
      |
76 | 14, 75 | rexlimddv 2609 |
1
 
      |