Step | Hyp | Ref
| Expression |
1 | | dfnn2 8920 |
. . . 4
         |
2 | | caucvgre.f |
. . . 4
       |
3 | | caucvgre.cau |
. . . . 5
                                    |
4 | 2, 3 | caucvgrelemcau 10988 |
. . . 4
                
                      |
5 | 1, 2, 4 | ax-caucvg 7930 |
. . 3
                         |
6 | | ralrp 9674 |
. . . . 5
 
                                         |
7 | | 0re 7956 |
. . . . . . . 8
 |
8 | | ltxrlt 8022 |
. . . . . . . 8
 
     |
9 | 7, 8 | mpan 424 |
. . . . . . 7
 
   |
10 | 9 | imbi1d 231 |
. . . . . 6
                       
                     |
11 | 10 | ralbiia 2491 |
. . . . 5
 

 
                 
 
                    |
12 | 6, 11 | bitri 184 |
. . . 4
 
                    
                    |
13 | 12 | rexbii 2484 |
. . 3
  
                                          |
14 | 5, 13 | sylibr 134 |
. 2
                       |
15 | | simpr 110 |
. . . . . . . . . 10
   


   |
16 | 15 | peano2nnd 8933 |
. . . . . . . . 9
   


     |
17 | | uznnssnn 9576 |
. . . . . . . . 9
           |
18 | | ssralv 3219 |
. . . . . . . . 9
                        
                           |
19 | 16, 17, 18 | 3syl 17 |
. . . . . . . 8
   


                  
                           |
20 | | eluznn 9599 |
. . . . . . . . . . . . . 14
   
   
     |
21 | 16, 20 | sylan 283 |
. . . . . . . . . . . . 13
                 |
22 | | simplr 528 |
. . . . . . . . . . . . . . . . . 18
           |
23 | 22 | peano2nnd 8933 |
. . . . . . . . . . . . . . . . 17
             |
24 | 23 | nnzd 9373 |
. . . . . . . . . . . . . . . 16
             |
25 | | eluz1 9531 |
. . . . . . . . . . . . . . . 16
       
 
       |
26 | 24, 25 | syl 14 |
. . . . . . . . . . . . . . 15
                  
    |
27 | 26 | biimpd 144 |
. . . . . . . . . . . . . 14
                       |
28 | 27 | impancom 260 |
. . . . . . . . . . . . 13
               
       |
29 | 21, 28 | mpd 13 |
. . . . . . . . . . . 12
                     |
30 | 29 | simprd 114 |
. . . . . . . . . . 11
                   |
31 | | nnre 8925 |
. . . . . . . . . . . . . . 15
   |
32 | 31 | ad2antlr 489 |
. . . . . . . . . . . . . 14
           |
33 | | simpr 110 |
. . . . . . . . . . . . . . 15
           |
34 | 33 | nnred 8931 |
. . . . . . . . . . . . . 14
           |
35 | | 1re 7955 |
. . . . . . . . . . . . . . 15
 |
36 | | ltadd1 8385 |
. . . . . . . . . . . . . . 15
 
 
       |
37 | 35, 36 | mp3an3 1326 |
. . . . . . . . . . . . . 14
 
         |
38 | 32, 34, 37 | syl2anc 411 |
. . . . . . . . . . . . 13
                 |
39 | | nnleltp1 9311 |
. . . . . . . . . . . . . 14
   
           |
40 | 23, 33, 39 | syl2anc 411 |
. . . . . . . . . . . . 13
                   |
41 | 38, 40 | bitr4d 191 |
. . . . . . . . . . . 12
               |
42 | 21, 41 | syldan 282 |
. . . . . . . . . . 11
                     |
43 | 30, 42 | mpbird 167 |
. . . . . . . . . 10
                 |
44 | | nnre 8925 |
. . . . . . . . . . . . . . 15
   |
45 | | ltxrlt 8022 |
. . . . . . . . . . . . . . 15
 
     |
46 | 31, 44, 45 | syl2an 289 |
. . . . . . . . . . . . . 14
 
     |
47 | 46 | adantll 476 |
. . . . . . . . . . . . 13
         
   |
48 | 2 | ad4antr 494 |
. . . . . . . . . . . . . . . 16
               |
49 | 48, 33 | ffvelcdmd 5652 |
. . . . . . . . . . . . . . 15
               |
50 | | simpllr 534 |
. . . . . . . . . . . . . . . . 17
   


   |
51 | 50 | adantr 276 |
. . . . . . . . . . . . . . . 16
           |
52 | | rpre 9659 |
. . . . . . . . . . . . . . . . 17

  |
53 | 52 | ad3antlr 493 |
. . . . . . . . . . . . . . . 16
           |
54 | 51, 53 | readdcld 7986 |
. . . . . . . . . . . . . . 15
             |
55 | | ltxrlt 8022 |
. . . . . . . . . . . . . . 15
                         |
56 | 49, 54, 55 | syl2anc 411 |
. . . . . . . . . . . . . 14
                         |
57 | 49, 53 | readdcld 7986 |
. . . . . . . . . . . . . . 15
                 |
58 | | ltxrlt 8022 |
. . . . . . . . . . . . . . 15
                         |
59 | 51, 57, 58 | syl2anc 411 |
. . . . . . . . . . . . . 14
                         |
60 | 56, 59 | anbi12d 473 |
. . . . . . . . . . . . 13
                       
      
          |
61 | 47, 60 | imbi12d 234 |
. . . . . . . . . . . 12
               
         

      
           |
62 | 61 | biimprd 158 |
. . . . . . . . . . 11
          
      
        
    
             |
63 | 21, 62 | syldan 282 |
. . . . . . . . . 10
                
      
        
    
             |
64 | 43, 63 | mpid 42 |
. . . . . . . . 9
                
      
            
            |
65 | 64 | ralimdva 2544 |
. . . . . . . 8
   


                                      
            |
66 | 19, 65 | syld 45 |
. . . . . . 7
   


                  
                         |
67 | | fveq2 5515 |
. . . . . . . . . 10
           |
68 | 67 | breq1d 4013 |
. . . . . . . . 9
     
 
         |
69 | 67 | oveq1d 5889 |
. . . . . . . . . 10
               |
70 | 69 | breq2d 4015 |
. . . . . . . . 9
 
     
         |
71 | 68, 70 | anbi12d 473 |
. . . . . . . 8
                      
          |
72 | 71 | cbvralv 2703 |
. . . . . . 7
 
   
                
                        |
73 | 66, 72 | imbitrdi 161 |
. . . . . 6
   


                  
                         |
74 | 73 | reximdva 2579 |
. . . . 5
      
                 
    
                    |
75 | | fveq2 5515 |
. . . . . . . . . 10
               |
76 | 75 | raleqdv 2678 |
. . . . . . . . 9
    
         
        
                         |
77 | 76 | rspcev 2841 |
. . . . . . . 8
        
                  
                      |
78 | 16, 77 | sylan 283 |
. . . . . . 7
                                                      |
79 | 78 | ex 115 |
. . . . . 6
   


                       
                        |
80 | 79 | rexlimdva 2594 |
. . . . 5
      
    
                                         |
81 | 74, 80 | syld 45 |
. . . 4
      
                 
                       |
82 | 81 | ralimdva 2544 |
. . 3
 

 
                 
                         |
83 | 82 | reximdva 2579 |
. 2
                      
                         |
84 | 14, 83 | mpd 13 |
1
                          |