Step | Hyp | Ref
| Expression |
1 | | nn0ennn 10099 |
. . . 4
 |
2 | 1 | ensymi 6630 |
. . 3
 |
3 | | entr 6632 |
. . 3
     |
4 | 2, 3 | mpan2 419 |
. 2

  |
5 | | bren 6595 |
. . . 4

       |
6 | 5 | biimpi 119 |
. . 3

       |
7 | | f1of 5323 |
. . . . . . . . . . 11
    
      |
8 | 7 | adantr 272 |
. . . . . . . . . 10
      
        |
9 | | simprl 503 |
. . . . . . . . . 10
      
    |
10 | 8, 9 | ffvelrnd 5510 |
. . . . . . . . 9
      
        |
11 | 10 | nn0zd 9075 |
. . . . . . . 8
      
        |
12 | | simprr 504 |
. . . . . . . . . 10
      
    |
13 | 8, 12 | ffvelrnd 5510 |
. . . . . . . . 9
      
        |
14 | 13 | nn0zd 9075 |
. . . . . . . 8
      
        |
15 | | zdceq 9030 |
. . . . . . . 8
           DECID           |
16 | 11, 14, 15 | syl2anc 406 |
. . . . . . 7
      
 
DECID           |
17 | | dff1o6 5631 |
. . . . . . . . . . . . 13
      

             |
18 | 17 | simp3bi 981 |
. . . . . . . . . . . 12
    


            |
19 | 18 | r19.21bi 2494 |
. . . . . . . . . . 11
     
              |
20 | 19 | r19.21bi 2494 |
. . . . . . . . . 10
        
            |
21 | 20 | anasss 394 |
. . . . . . . . 9
      
          
   |
22 | | fveq2 5375 |
. . . . . . . . 9
           |
23 | 21, 22 | impbid1 141 |
. . . . . . . 8
      
          
   |
24 | 23 | dcbid 806 |
. . . . . . 7
      
  DECID        
DECID
   |
25 | 16, 24 | mpbid 146 |
. . . . . 6
      
 
DECID
  |
26 | 25 | ralrimivva 2488 |
. . . . 5
    


DECID
  |
27 | | f1ocnv 5336 |
. . . . . . 7
    
       |
28 | | f1ofo 5330 |
. . . . . . 7
     
       |
29 | 27, 28 | syl 14 |
. . . . . 6
    
       |
30 | | peano2nn0 8921 |
. . . . . . . . 9

    |
31 | 30 | adantl 273 |
. . . . . . . 8
     
     |
32 | | elfznn0 9787 |
. . . . . . . . . . . . . . 15
       |
33 | 32 | adantl 273 |
. . . . . . . . . . . . . 14
       
       |
34 | 33 | nn0red 8935 |
. . . . . . . . . . . . 13
       
       |
35 | | elfzle2 9701 |
. . . . . . . . . . . . . . 15
       |
36 | 35 | adantl 273 |
. . . . . . . . . . . . . 14
       
       |
37 | | simplr 502 |
. . . . . . . . . . . . . . 15
       
       |
38 | | nn0leltp1 9021 |
. . . . . . . . . . . . . . 15
 
       |
39 | 33, 37, 38 | syl2anc 406 |
. . . . . . . . . . . . . 14
       
           |
40 | 36, 39 | mpbid 146 |
. . . . . . . . . . . . 13
       
         |
41 | 34, 40 | gtned 7799 |
. . . . . . . . . . . 12
       
         |
42 | 41 | neneqd 2303 |
. . . . . . . . . . 11
       
    
    |
43 | | dff1o6 5631 |
. . . . . . . . . . . . . . 15
       

            
    |
44 | 27, 43 | sylib 121 |
. . . . . . . . . . . . . 14
    
 
             
    |
45 | 44 | simp3d 978 |
. . . . . . . . . . . . 13
    
            
   |
46 | 45 | ad2antrr 477 |
. . . . . . . . . . . 12
       
                 
   |
47 | 31 | adantr 272 |
. . . . . . . . . . . . 13
       
         |
48 | | fveqeq2 5384 |
. . . . . . . . . . . . . . 15
                             |
49 | | eqeq1 2121 |
. . . . . . . . . . . . . . 15
   
     |
50 | 48, 49 | imbi12d 233 |
. . . . . . . . . . . . . 14
               
                   |
51 | | fveq2 5375 |
. . . . . . . . . . . . . . . 16
             |
52 | 51 | eqeq2d 2126 |
. . . . . . . . . . . . . . 15
      
                      |
53 | | eqeq2 2124 |
. . . . . . . . . . . . . . 15
   
     |
54 | 52, 53 | imbi12d 233 |
. . . . . . . . . . . . . 14
                 
                   |
55 | 50, 54 | rspc2v 2772 |
. . . . . . . . . . . . 13
   
                                   |
56 | 47, 33, 55 | syl2anc 406 |
. . . . . . . . . . . 12
       
                  
                    |
57 | 46, 56 | mpd 13 |
. . . . . . . . . . 11
       
                       |
58 | 42, 57 | mtod 635 |
. . . . . . . . . 10
       
    
              |
59 | 58 | neqned 2289 |
. . . . . . . . 9
       
                   |
60 | 59 | ralrimiva 2479 |
. . . . . . . 8
     
 
                   |
61 | | fveq2 5375 |
. . . . . . . . . . 11
                 |
62 | 61 | neeq1d 2300 |
. . . . . . . . . 10
                             |
63 | 62 | ralbidv 2411 |
. . . . . . . . 9
    
               
                    |
64 | 63 | rspcev 2760 |
. . . . . . . 8
                      
                   |
65 | 31, 60, 64 | syl2anc 406 |
. . . . . . 7
     
 
                  |
66 | 65 | ralrimiva 2479 |
. . . . . 6
    
                    |
67 | | cnvexg 5034 |
. . . . . . . 8
 
  |
68 | 67 | elv 2661 |
. . . . . . 7
  |
69 | | foeq1 5299 |
. . . . . . . 8
               |
70 | | fveq1 5374 |
. . . . . . . . . . 11
             |
71 | | fveq1 5374 |
. . . . . . . . . . 11
             |
72 | 70, 71 | neeq12d 2302 |
. . . . . . . . . 10
                        |
73 | 72 | rexralbidv 2435 |
. . . . . . . . 9
                 
                    |
74 | 73 | ralbidv 2411 |
. . . . . . . 8
                  
                     |
75 | 69, 74 | anbi12d 462 |
. . . . . . 7
       
                      
                      |
76 | 68, 75 | spcev 2751 |
. . . . . 6
                         
                          |
77 | 29, 66, 76 | syl2anc 406 |
. . . . 5
    
                          |
78 | 26, 77 | jca 302 |
. . . 4
    
 

DECID
                           |
79 | 78 | adantl 273 |
. . 3
        

DECID
                           |
80 | 6, 79 | exlimddv 1852 |
. 2

 

DECID
                           |
81 | 4, 80 | syl 14 |
1

 

DECID
                           |