Step | Hyp | Ref
| Expression |
1 | | ltexnqi 7118 |
. . . . 5

     |
2 | 1 | adantl 273 |
. . . 4
   
 

     |
3 | | subhalfnqq 7123 |
. . . . . 6
      |
4 | 3 | ad2antrl 477 |
. . . . 5
      
       
   |
5 | | archrecnq 7372 |
. . . . . . 7
            |
6 | 5 | ad2antrl 477 |
. . . . . 6
       
      
               |
7 | | simpllr 504 |
. . . . . . . . . 10
       
      
      |
8 | 7 | adantr 272 |
. . . . . . . . 9
     
                           |
9 | | simplrl 505 |
. . . . . . . . . 10
       
      
      |
10 | 9 | adantr 272 |
. . . . . . . . 9
     
                           |
11 | | simplrr 506 |
. . . . . . . . . 10
       
      
        |
12 | 11 | adantr 272 |
. . . . . . . . 9
     
                             |
13 | | simplrl 505 |
. . . . . . . . 9
     
                           |
14 | | simplrr 506 |
. . . . . . . . 9
     
                             |
15 | | simprl 501 |
. . . . . . . . 9
     
                           |
16 | | simprr 502 |
. . . . . . . . 9
     
                                   |
17 | 8, 10, 12, 13, 14, 15, 16 | caucvgprprlemloccalc 7393 |
. . . . . . . 8
     
                                                                                      |
18 | | simplrl 505 |
. . . . . . . . . . . . 13
   
 

  |
19 | 18 | ad3antrrr 479 |
. . . . . . . . . . . 12
     
                           |
20 | | nnnq 7131 |
. . . . . . . . . . . . . 14
        |
21 | 20 | ad2antrl 477 |
. . . . . . . . . . . . 13
     
                                |
22 | | recclnq 7101 |
. . . . . . . . . . . . 13
             
  |
23 | 21, 22 | syl 14 |
. . . . . . . . . . . 12
     
                                   |
24 | | addclnq 7084 |
. . . . . . . . . . . 12
         
             |
25 | 19, 23, 24 | syl2anc 406 |
. . . . . . . . . . 11
     
                                     |
26 | | nqprlu 7256 |
. . . . . . . . . . 11
            
                           |
27 | 25, 26 | syl 14 |
. . . . . . . . . 10
     
                          
                           |
28 | | nqprlu 7256 |
. . . . . . . . . . 11
        
 
                       |
29 | 23, 28 | syl 14 |
. . . . . . . . . 10
     
                          
         
             |
30 | | addclpr 7246 |
. . . . . . . . . 10
                                                                                                           |
31 | 27, 29, 30 | syl2anc 406 |
. . . . . . . . 9
     
                                                                               |
32 | | simplrr 506 |
. . . . . . . . . . 11
   
 

  |
33 | 32 | ad3antrrr 479 |
. . . . . . . . . 10
     
                           |
34 | | nqprlu 7256 |
. . . . . . . . . 10
  
  
    |
35 | 33, 34 | syl 14 |
. . . . . . . . 9
     
                          
  
    |
36 | | caucvgprpr.f |
. . . . . . . . . . . 12
       |
37 | 36 | ad5antr 483 |
. . . . . . . . . . 11
     
                               |
38 | 37, 15 | ffvelrnd 5488 |
. . . . . . . . . 10
     
                               |
39 | | ltrelnq 7074 |
. . . . . . . . . . . . . 14
   |
40 | 39 | brel 4529 |
. . . . . . . . . . . . 13
                     |
41 | 40 | simpld 111 |
. . . . . . . . . . . 12
                   |
42 | 41 | ad2antll 478 |
. . . . . . . . . . 11
     
                                   |
43 | 42, 28 | syl 14 |
. . . . . . . . . 10
     
                          
         
             |
44 | | addclpr 7246 |
. . . . . . . . . 10
       
                          
 
         
              |
45 | 38, 43, 44 | syl2anc 406 |
. . . . . . . . 9
     
                             
 
         
              |
46 | | ltsopr 7305 |
. . . . . . . . . 10
 |
47 | | sowlin 4180 |
. . . . . . . . . 10
    
                                                                                          
                                                           
                                                                                                                      |
48 | 46, 47 | mpan 418 |
. . . . . . . . 9
    
                                                                                         
                                                  
        
                                                                                                                      |
49 | 31, 35, 45, 48 | syl3anc 1184 |
. . . . . . . 8
     
                            
                                                  
        
                                                                                                                      |
50 | 17, 49 | mpd 13 |
. . . . . . 7
     
                            
                                                                                                                     |
51 | 19 | adantr 272 |
. . . . . . . . . 10
       
 
      
                 
                                                                              
  |
52 | | simplrl 505 |
. . . . . . . . . . 11
       
 
      
                 
                                                                              
  |
53 | | simpr 109 |
. . . . . . . . . . . 12
       
 
      
                 
                                                                              
                                                                                   |
54 | | ltaprg 7328 |
. . . . . . . . . . . . . 14
 
 
  
    |
55 | 54 | adantl 273 |
. . . . . . . . . . . . 13
          
      
                 
                                                                              

  
  
    |
56 | 42 | adantr 272 |
. . . . . . . . . . . . . . 15
       
 
      
                 
                                                                              
          |
57 | 51, 56, 24 | syl2anc 406 |
. . . . . . . . . . . . . 14
       
 
      
                 
                                                                              
            |
58 | 57, 26 | syl 14 |
. . . . . . . . . . . . 13
       
 
      
                 
                                                                              
 
                           |
59 | 38 | adantr 272 |
. . . . . . . . . . . . 13
       
 
      
                 
                                                                              
      |
60 | 56, 28 | syl 14 |
. . . . . . . . . . . . 13
       
 
      
                 
                                                                              
 
         
             |
61 | | addcomprg 7287 |
. . . . . . . . . . . . . 14
 
       |
62 | 61 | adantl 273 |
. . . . . . . . . . . . 13
          
      
                 
                                                                              
         |
63 | 55, 58, 59, 60, 62 | caovord2d 5872 |
. . . . . . . . . . . 12
       
 
      
                 
                                                                              
                                                                                                                    |
64 | 53, 63 | mpbird 166 |
. . . . . . . . . . 11
       
 
      
                 
                                                                              
 
                               |
65 | | opeq1 3652 |
. . . . . . . . . . . . . . . . . . 19
   
     |
66 | 65 | eceq1d 6395 |
. . . . . . . . . . . . . . . . . 18
            |
67 | 66 | fveq2d 5357 |
. . . . . . . . . . . . . . . . 17
                   |
68 | 67 | oveq2d 5722 |
. . . . . . . . . . . . . . . 16
                       |
69 | 68 | breq2d 3887 |
. . . . . . . . . . . . . . 15
           
             |
70 | 69 | abbidv 2217 |
. . . . . . . . . . . . . 14
 
           
             |
71 | 68 | breq1d 3885 |
. . . . . . . . . . . . . . 15
           
             |
72 | 71 | abbidv 2217 |
. . . . . . . . . . . . . 14
                           |
73 | 70, 72 | opeq12d 3660 |
. . . . . . . . . . . . 13
  
                                                      |
74 | | fveq2 5353 |
. . . . . . . . . . . . 13
           |
75 | 73, 74 | breq12d 3888 |
. . . . . . . . . . . 12
                                  
                                |
76 | 75 | rspcev 2744 |
. . . . . . . . . . 11
   
                             
  
                               |
77 | 52, 64, 76 | syl2anc 406 |
. . . . . . . . . 10
       
 
      
                 
                                                                              
  
                               |
78 | | caucvgprpr.lim |
. . . . . . . . . . 11
    
                              
                                
        |
79 | 78 | caucvgprprlemell 7394 |
. . . . . . . . . 10
     
  
                                |
80 | 51, 77, 79 | sylanbrc 411 |
. . . . . . . . 9
       
 
      
                 
                                                                              
      |
81 | 80 | ex 114 |
. . . . . . . 8
     
                            
                                                                                     |
82 | 33 | adantr 272 |
. . . . . . . . . 10
       
 
      
                                             
        |
83 | | fveq2 5353 |
. . . . . . . . . . . . . 14
           |
84 | | opeq1 3652 |
. . . . . . . . . . . . . . . . . . 19
   
     |
85 | 84 | eceq1d 6395 |
. . . . . . . . . . . . . . . . . 18
            |
86 | 85 | fveq2d 5357 |
. . . . . . . . . . . . . . . . 17
                   |
87 | 86 | breq2d 3887 |
. . . . . . . . . . . . . . . 16
         
           |
88 | 87 | abbidv 2217 |
. . . . . . . . . . . . . . 15
 
        

           |
89 | 86 | breq1d 3885 |
. . . . . . . . . . . . . . . 16
                     |
90 | 89 | abbidv 2217 |
. . . . . . . . . . . . . . 15
                       |
91 | 88, 90 | opeq12d 3660 |
. . . . . . . . . . . . . 14
  
         
                                    |
92 | 83, 91 | oveq12d 5724 |
. . . . . . . . . . . . 13
     
 
         
                                           |
93 | 92 | breq1d 3885 |
. . . . . . . . . . . 12
                                     
      
                       
  
     |
94 | 93 | rspcev 2744 |
. . . . . . . . . . 11
                                                                              |
95 | 15, 94 | sylan 279 |
. . . . . . . . . 10
       
 
      
                                             
                                             |
96 | 78 | caucvgprprlemelu 7395 |
. . . . . . . . . 10
     
                               
        |
97 | 82, 95, 96 | sylanbrc 411 |
. . . . . . . . 9
       
 
      
                                             
            |
98 | 97 | ex 114 |
. . . . . . . 8
     
                                                                     |
99 | 81, 98 | orim12d 741 |
. . . . . . 7
     
                             
                                                                                                                                |
100 | 50, 99 | mpd 13 |
. . . . . 6
     
                                     |
101 | 6, 100 | rexlimddv 2513 |
. . . . 5
       
      
                |
102 | 4, 101 | rexlimddv 2513 |
. . . 4
      
                  |
103 | 2, 102 | rexlimddv 2513 |
. . 3
   
 

            |
104 | 103 | ex 114 |
. 2
 
                 |
105 | 104 | ralrimivva 2473 |
1
                 |