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

     |
2 | 1 | adantl 277 |
. . . 4
   
 

     |
3 | | subhalfnqq 7413 |
. . . . . 6
      |
4 | 3 | ad2antrl 490 |
. . . . 5
      
       
   |
5 | | simprr 531 |
. . . . . . . . 9
       
      
        |
6 | | simplrl 535 |
. . . . . . . . . . 11
   
 

  |
7 | 6 | adantr 276 |
. . . . . . . . . 10
      
        |
8 | 7 | adantr 276 |
. . . . . . . . 9
       
      
      |
9 | | ltanqi 7401 |
. . . . . . . . 9
             |
10 | 5, 8, 9 | syl2anc 411 |
. . . . . . . 8
       
      
            |
11 | | simplrr 536 |
. . . . . . . 8
       
      
        |
12 | 10, 11 | breqtrd 4030 |
. . . . . . 7
       
      
          |
13 | | simprl 529 |
. . . . . . . . . 10
       
      
      |
14 | | addclnq 7374 |
. . . . . . . . . 10
 
     |
15 | 13, 13, 14 | syl2anc 411 |
. . . . . . . . 9
       
      
        |
16 | | addclnq 7374 |
. . . . . . . . 9
  
        |
17 | 8, 15, 16 | syl2anc 411 |
. . . . . . . 8
       
      
          |
18 | | simplrr 536 |
. . . . . . . . . 10
   
 

  |
19 | 18 | adantr 276 |
. . . . . . . . 9
      
        |
20 | 19 | adantr 276 |
. . . . . . . 8
       
      
      |
21 | | cauappcvgpr.f |
. . . . . . . . . . 11
       |
22 | 21 | ad4antr 494 |
. . . . . . . . . 10
       
      
          |
23 | 22, 13 | ffvelcdmd 5653 |
. . . . . . . . 9
       
      
          |
24 | | addclnq 7374 |
. . . . . . . . 9
     
         |
25 | 23, 13, 24 | syl2anc 411 |
. . . . . . . 8
       
      
            |
26 | | ltsonq 7397 |
. . . . . . . . 9
 |
27 | | sowlin 4321 |
. . . . . . . . 9
     
            
                     |
28 | 26, 27 | mpan 424 |
. . . . . . . 8
     
                                 |
29 | 17, 20, 25, 28 | syl3anc 1238 |
. . . . . . 7
       
      
        
    
                |
30 | 12, 29 | mpd 13 |
. . . . . 6
       
      
        
               |
31 | 8 | adantr 276 |
. . . . . . . . 9
     
                 
         |
32 | | simplrl 535 |
. . . . . . . . . 10
     
                 
      
  |
33 | | simpr 110 |
. . . . . . . . . . . 12
     
                 
          
        |
34 | | addassnqg 7381 |
. . . . . . . . . . . . . 14
 
           |
35 | 31, 32, 32, 34 | syl3anc 1238 |
. . . . . . . . . . . . 13
     
                 
                 |
36 | 35 | breq1d 4014 |
. . . . . . . . . . . 12
     
                 
                     
         |
37 | 33, 36 | mpbird 167 |
. . . . . . . . . . 11
     
                 
                   |
38 | | ltanqg 7399 |
. . . . . . . . . . . . 13
 
 
       |
39 | 38 | adantl 277 |
. . . . . . . . . . . 12
       
 
      
               
          |
40 | | addclnq 7374 |
. . . . . . . . . . . . 13
 
     |
41 | 31, 32, 40 | syl2anc 411 |
. . . . . . . . . . . 12
     
                 
           |
42 | 23 | adantr 276 |
. . . . . . . . . . . 12
     
                 
             |
43 | | addcomnqg 7380 |
. . . . . . . . . . . . 13
 
       |
44 | 43 | adantl 277 |
. . . . . . . . . . . 12
       
 
      
               
 
      |
45 | 39, 41, 42, 32, 44 | caovord2d 6044 |
. . . . . . . . . . 11
     
                 
                           |
46 | 37, 45 | mpbird 167 |
. . . . . . . . . 10
     
                 
               |
47 | | oveq2 5883 |
. . . . . . . . . . . 12
       |
48 | | fveq2 5516 |
. . . . . . . . . . . 12
           |
49 | 47, 48 | breq12d 4017 |
. . . . . . . . . . 11
       
         |
50 | 49 | rspcev 2842 |
. . . . . . . . . 10
         
        |
51 | 32, 46, 50 | syl2anc 411 |
. . . . . . . . 9
     
                 
       
        |
52 | | oveq1 5882 |
. . . . . . . . . . . 12
       |
53 | 52 | breq1d 4014 |
. . . . . . . . . . 11
       
         |
54 | 53 | rexbidv 2478 |
. . . . . . . . . 10
  
     
          |
55 | | cauappcvgpr.lim |
. . . . . . . . . . . 12
           
          |
56 | 55 | fveq2i 5519 |
. . . . . . . . . . 11
         
         
          |
57 | | nqex 7362 |
. . . . . . . . . . . . 13
 |
58 | 57 | rabex 4148 |
. . . . . . . . . . . 12
 
        |
59 | 57 | rabex 4148 |
. . . . . . . . . . . 12
        
 |
60 | 58, 59 | op1st 6147 |
. . . . . . . . . . 11
             
            
        |
61 | 56, 60 | eqtri 2198 |
. . . . . . . . . 10
     
        |
62 | 54, 61 | elrab2 2897 |
. . . . . . . . 9
     
          |
63 | 31, 51, 62 | sylanbrc 417 |
. . . . . . . 8
     
                 
             |
64 | 63 | ex 115 |
. . . . . . 7
       
      
        
             |
65 | 20 | adantr 276 |
. . . . . . . . 9
     
                       |
66 | | id 19 |
. . . . . . . . . . . . 13
   |
67 | 48, 66 | oveq12d 5893 |
. . . . . . . . . . . 12
               |
68 | 67 | breq1d 4014 |
. . . . . . . . . . 11
       
         |
69 | 68 | rspcev 2842 |
. . . . . . . . . 10
         
        |
70 | 13, 69 | sylan 283 |
. . . . . . . . 9
     
                     
        |
71 | | breq2 4008 |
. . . . . . . . . . 11
       
         |
72 | 71 | rexbidv 2478 |
. . . . . . . . . 10
  
     
          |
73 | 55 | fveq2i 5519 |
. . . . . . . . . . 11
         
         
          |
74 | 58, 59 | op2nd 6148 |
. . . . . . . . . . 11
             
            
        |
75 | 73, 74 | eqtri 2198 |
. . . . . . . . . 10
     
        |
76 | 72, 75 | elrab2 2897 |
. . . . . . . . 9
     
          |
77 | 65, 70, 76 | sylanbrc 417 |
. . . . . . . 8
     
                           |
78 | 77 | ex 115 |
. . . . . . 7
       
      
                  |
79 | 64, 78 | orim12d 786 |
. . . . . 6
       
      
                      
             |
80 | 30, 79 | mpd 13 |
. . . . 5
       
      
                |
81 | 4, 80 | rexlimddv 2599 |
. . . 4
      
                  |
82 | 2, 81 | rexlimddv 2599 |
. . 3
   
 

            |
83 | 82 | ex 115 |
. 2
 
                 |
84 | 83 | ralrimivva 2559 |
1
                 |