Step | Hyp | Ref
| Expression |
1 | | fveq2 5791 |
. . . . . . 7
           |
2 | 1 | eleq2d 2521 |
. . . . . 6
         
           |
3 | 2 | rexbidv 2848 |
. . . . 5
  
                    |
4 | 3 | imbi2d 316 |
. . . 4
                   
                           
             |
5 | | fveq2 5791 |
. . . . . . 7
           |
6 | 5 | eleq2d 2521 |
. . . . . 6
         
           |
7 | 6 | rexbidv 2848 |
. . . . 5
  
                    |
8 | 7 | imbi2d 316 |
. . . 4
                   
                           
             |
9 | | fveq2 5791 |
. . . . . . 7
               |
10 | 9 | eleq2d 2521 |
. . . . . 6
           
             |
11 | 10 | rexbidv 2848 |
. . . . 5
    
                      |
12 | 11 | imbi2d 316 |
. . . 4
                     
                           
               |
13 | | fveq2 5791 |
. . . . . . 7
           |
14 | 13 | eleq2d 2521 |
. . . . . 6
         
           |
15 | 14 | rexbidv 2848 |
. . . . 5
  
                    |
16 | 15 | imbi2d 316 |
. . . 4
                   
                           
             |
17 | | 1nn 10436 |
. . . . . . 7
 |
18 | | ne0i 3743 |
. . . . . . 7
   |
19 | 17, 18 | ax-mp 5 |
. . . . . 6
 |
20 | | ffvelrn 5942 |
. . . . . . . 8
     
       |
21 | | elnnuz 11000 |
. . . . . . . 8
    
          |
22 | 20, 21 | sylib 196 |
. . . . . . 7
     
           |
23 | 22 | ralrimiva 2822 |
. . . . . 6
                |
24 | | r19.2z 3869 |
. . . . . 6
  
        
           |
25 | 19, 23, 24 | sylancr 663 |
. . . . 5
                |
26 | 25 | adantr 465 |
. . . 4
                             |
27 | | peano2nn 10437 |
. . . . . . . . . 10
     |
28 | 27 | adantl 466 |
. . . . . . . . 9
                          |
29 | | nnre 10432 |
. . . . . . . . . . . . 13
   |
30 | 29 | ad2antrr 725 |
. . . . . . . . . . . 12
                        |
31 | 20 | nnred 10440 |
. . . . . . . . . . . . . 14
     
       |
32 | 31 | adantlr 714 |
. . . . . . . . . . . . 13
                          |
33 | 32 | adantll 713 |
. . . . . . . . . . . 12
                            |
34 | | 1re 9488 |
. . . . . . . . . . . . 13
 |
35 | 34 | a1i 11 |
. . . . . . . . . . . 12
                        |
36 | 30, 33, 35 | leadd1d 10036 |
. . . . . . . . . . 11
                      
   
           |
37 | | fveq2 5791 |
. . . . . . . . . . . . . . . . . 18
           |
38 | | oveq1 6199 |
. . . . . . . . . . . . . . . . . . 19
       |
39 | 38 | fveq2d 5795 |
. . . . . . . . . . . . . . . . . 18
          
    |
40 | 37, 39 | breq12d 4405 |
. . . . . . . . . . . . . . . . 17
     
     
             |
41 | 40 | rspcv 3167 |
. . . . . . . . . . . . . . . 16
  
       
               |
42 | 41 | imdistani 690 |
. . . . . . . . . . . . . . 15
                      
     |
43 | | ffvelrn 5942 |
. . . . . . . . . . . . . . . . . . 19
      
     
    |
44 | 27, 43 | sylan2 474 |
. . . . . . . . . . . . . . . . . 18
     
         |
45 | | nnltp1le 10803 |
. . . . . . . . . . . . . . . . . 18
                             
         |
46 | 20, 44, 45 | syl2anc 661 |
. . . . . . . . . . . . . . . . 17
     
                 
         |
47 | 46 | biimpa 484 |
. . . . . . . . . . . . . . . 16
                  
              |
48 | 47 | anasss 647 |
. . . . . . . . . . . . . . 15
      
   
                      |
49 | 42, 48 | sylan2 474 |
. . . . . . . . . . . . . 14
      
        
                  |
50 | 49 | anass1rs 805 |
. . . . . . . . . . . . 13
                             
    |
51 | 50 | adantll 713 |
. . . . . . . . . . . 12
                               
    |
52 | | peano2re 9645 |
. . . . . . . . . . . . . . . 16
     |
53 | 29, 52 | syl 16 |
. . . . . . . . . . . . . . 15
     |
54 | 53 | ad2antrr 725 |
. . . . . . . . . . . . . 14
             |
55 | | peano2nn 10437 |
. . . . . . . . . . . . . . . . 17
             |
56 | 20, 55 | syl 16 |
. . . . . . . . . . . . . . . 16
     
         |
57 | 56 | nnred 10440 |
. . . . . . . . . . . . . . 15
     
         |
58 | 57 | adantll 713 |
. . . . . . . . . . . . . 14
                 |
59 | 43 | nnred 10440 |
. . . . . . . . . . . . . . . 16
      
     
    |
60 | 27, 59 | sylan2 474 |
. . . . . . . . . . . . . . 15
     
         |
61 | 60 | adantll 713 |
. . . . . . . . . . . . . 14
            
    |
62 | | letr 9571 |
. . . . . . . . . . . . . 14
                                             
     |
63 | 54, 58, 61, 62 | syl3anc 1219 |
. . . . . . . . . . . . 13
                            
    
         |
64 | 63 | adantlrr 720 |
. . . . . . . . . . . 12
                                            
           |
65 | 51, 64 | mpan2d 674 |
. . . . . . . . . . 11
                        
       
         |
66 | 36, 65 | sylbid 215 |
. . . . . . . . . 10
                      
         
     |
67 | | nnz 10771 |
. . . . . . . . . . . . 13
   |
68 | 20 | nnzd 10849 |
. . . . . . . . . . . . 13
     
       |
69 | | eluz 10977 |
. . . . . . . . . . . . 13
               
       |
70 | 67, 68, 69 | syl2an 477 |
. . . . . . . . . . . 12
      
 
                |
71 | 70 | adantrlr 722 |
. . . . . . . . . . 11
                              
       |
72 | 71 | anassrs 648 |
. . . . . . . . . 10
                              
       |
73 | 67 | peano2zd 10853 |
. . . . . . . . . . . . 13
     |
74 | 43 | nnzd 10849 |
. . . . . . . . . . . . . 14
      
     
    |
75 | 27, 74 | sylan2 474 |
. . . . . . . . . . . . 13
     
         |
76 | | eluz 10977 |
. . . . . . . . . . . . 13
               
       
           |
77 | 73, 75, 76 | syl2an 477 |
. . . . . . . . . . . 12
      
 
                        |
78 | 77 | adantrlr 722 |
. . . . . . . . . . 11
                          
       
           |
79 | 78 | anassrs 648 |
. . . . . . . . . 10
                                  
           |
80 | 66, 72, 79 | 3imtr4d 268 |
. . . . . . . . 9
                                              |
81 | | fveq2 5791 |
. . . . . . . . . . 11
          
    |
82 | 81 | eleq1d 2520 |
. . . . . . . . . 10
             
               |
83 | 82 | rspcev 3171 |
. . . . . . . . 9
                              |
84 | 28, 80, 83 | syl6an 545 |
. . . . . . . 8
                                             |
85 | 84 | rexlimdva 2939 |
. . . . . . 7
                              
             |
86 | | fveq2 5791 |
. . . . . . . . 9
           |
87 | 86 | eleq1d 2520 |
. . . . . . . 8
           
             |
88 | 87 | cbvrexv 3046 |
. . . . . . 7
            
            |
89 | 85, 88 | syl6ib 226 |
. . . . . 6
                              
             |
90 | 89 | ex 434 |
. . . . 5
                  
 
                       |
91 | 90 | a2d 26 |
. . . 4
                   
                                           |
92 | 4, 8, 12, 16, 26, 91 | nnind 10443 |
. . 3
                  
            |
93 | 92 | com12 31 |
. 2
                  
            |
94 | 93 | 3impia 1185 |
1
                             |