Step | Hyp | Ref
| Expression |
1 | | ennnfonelemkh.p |
. 2
   |
2 | | fveq2 5517 |
. . . . . . 7
           |
3 | 2 | dmeqd 4831 |
. . . . . 6
           |
4 | | fveq2 5517 |
. . . . . 6
             |
5 | 3, 4 | sseq12d 3188 |
. . . . 5
     
        
        |
6 | 5 | imbi2d 230 |
. . . 4
  
         
              |
7 | | fveq2 5517 |
. . . . . . 7
           |
8 | 7 | dmeqd 4831 |
. . . . . 6
           |
9 | | fveq2 5517 |
. . . . . 6
             |
10 | 8, 9 | sseq12d 3188 |
. . . . 5
     
        
        |
11 | 10 | imbi2d 230 |
. . . 4
  
         
              |
12 | | fveq2 5517 |
. . . . . . 7
          
    |
13 | 12 | dmeqd 4831 |
. . . . . 6
               |
14 | | fveq2 5517 |
. . . . . 6
                 |
15 | 13, 14 | sseq12d 3188 |
. . . . 5
       
          
          |
16 | 15 | imbi2d 230 |
. . . 4
    
         
    
             |
17 | | fveq2 5517 |
. . . . . . 7
           |
18 | 17 | dmeqd 4831 |
. . . . . 6
           |
19 | | fveq2 5517 |
. . . . . 6
             |
20 | 18, 19 | sseq12d 3188 |
. . . . 5
     
        
        |
21 | 20 | imbi2d 230 |
. . . 4
  
         
              |
22 | | ennnfonelemh.dceq |
. . . . . . . . 9
  
DECID   |
23 | | ennnfonelemh.f |
. . . . . . . . 9
       |
24 | | ennnfonelemh.ne |
. . . . . . . . 9
   
           |
25 | | ennnfonelemh.g |
. . . . . . . . 9
 
 
                          |
26 | | ennnfonelemh.n |
. . . . . . . . 9
frec        |
27 | | ennnfonelemh.j |
. . . . . . . . 9
               |
28 | | ennnfonelemh.h |
. . . . . . . . 9
      |
29 | 22, 23, 24, 25, 26, 27, 28 | ennnfonelem0 12408 |
. . . . . . . 8
       |
30 | 29 | dmeqd 4831 |
. . . . . . 7
       |
31 | | dm0 4843 |
. . . . . . 7
 |
32 | 30, 31 | eqtrdi 2226 |
. . . . . 6
       |
33 | | 0ss 3463 |
. . . . . 6
      |
34 | 32, 33 | eqsstrdi 3209 |
. . . . 5
            |
35 | 34 | a1i 9 |
. . . 4
 
            |
36 | 26 | frechashgf1o 10430 |
. . . . . . . . . . . . . 14
     |
37 | | f1of 5463 |
. . . . . . . . . . . . . 14
    
      |
38 | 36, 37 | mp1i 10 |
. . . . . . . . . . . . 13
   
        
     
                         |
39 | 22 | ad2antrr 488 |
. . . . . . . . . . . . . . 15
       
         


DECID
  |
40 | 23 | ad2antrr 488 |
. . . . . . . . . . . . . . 15
       
         
      |
41 | 24 | ad2antrr 488 |
. . . . . . . . . . . . . . 15
       
         
              |
42 | | simplr 528 |
. . . . . . . . . . . . . . . . 17
       
         
      |
43 | | nn0uz 9564 |
. . . . . . . . . . . . . . . . 17
     |
44 | 42, 43 | eleqtrrdi 2271 |
. . . . . . . . . . . . . . . 16
       
         
  |
45 | | peano2nn0 9218 |
. . . . . . . . . . . . . . . 16

    |
46 | 44, 45 | syl 14 |
. . . . . . . . . . . . . . 15
       
         
    |
47 | 39, 40, 41, 25, 26, 27, 28, 46 | ennnfonelemom 12411 |
. . . . . . . . . . . . . 14
       
         
        |
48 | 47 | adantr 276 |
. . . . . . . . . . . . 13
   
        
     
                           |
49 | 38, 48 | ffvelcdmd 5654 |
. . . . . . . . . . . 12
   
        
     
                               |
50 | 49 | nn0red 9232 |
. . . . . . . . . . 11
   
        
     
                               |
51 | 44 | nn0red 9232 |
. . . . . . . . . . . 12
       
         
  |
52 | 51 | adantr 276 |
. . . . . . . . . . 11
   
        
     
                     |
53 | | peano2re 8095 |
. . . . . . . . . . . 12
     |
54 | 52, 53 | syl 14 |
. . . . . . . . . . 11
   
        
     
                       |
55 | 39, 40, 41, 25, 26, 27, 28, 44 | ennnfonelemp1 12409 |
. . . . . . . . . . . . . . . 16
       
         
                                                           |
56 | 55 | adantr 276 |
. . . . . . . . . . . . . . 15
   
        
     
                                                                              |
57 | | simpr 110 |
. . . . . . . . . . . . . . . 16
   
        
     
                                       |
58 | 57 | iftrued 3543 |
. . . . . . . . . . . . . . 15
   
        
     
                                                                            |
59 | 56, 58 | eqtrd 2210 |
. . . . . . . . . . . . . 14
   
        
     
                               |
60 | 59 | dmeqd 4831 |
. . . . . . . . . . . . 13
   
        
     
                               |
61 | 60 | fveq2d 5521 |
. . . . . . . . . . . 12
   
        
     
                                       |
62 | | simpr 110 |
. . . . . . . . . . . . . . 15
       
         
           |
63 | | 0zd 9267 |
. . . . . . . . . . . . . . . 16
       
         
  |
64 | 39, 40, 41, 25, 26, 27, 28, 44 | ennnfonelemom 12411 |
. . . . . . . . . . . . . . . 16
       
         
      |
65 | | f1ocnv 5476 |
. . . . . . . . . . . . . . . . . . . 20
    
       |
66 | 36, 65 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . 19
      |
67 | | f1of 5463 |
. . . . . . . . . . . . . . . . . . 19
     
       |
68 | 66, 67 | mp1i 10 |
. . . . . . . . . . . . . . . . . 18

       |
69 | | id 19 |
. . . . . . . . . . . . . . . . . 18

  |
70 | 68, 69 | ffvelcdmd 5654 |
. . . . . . . . . . . . . . . . 17

       |
71 | 44, 70 | syl 14 |
. . . . . . . . . . . . . . . 16
       
         
       |
72 | 63, 26, 64, 71 | frec2uzled 10431 |
. . . . . . . . . . . . . . 15
       
         
         
                    |
73 | 62, 72 | mpbid 147 |
. . . . . . . . . . . . . 14
       
         
                   |
74 | | f1ocnvfv2 5781 |
. . . . . . . . . . . . . . 15
                  |
75 | 36, 44, 74 | sylancr 414 |
. . . . . . . . . . . . . 14
       
         
           |
76 | 73, 75 | breqtrd 4031 |
. . . . . . . . . . . . 13
       
         
          |
77 | 76 | adantr 276 |
. . . . . . . . . . . 12
   
        
     
                             |
78 | 61, 77 | eqbrtrd 4027 |
. . . . . . . . . . 11
   
        
     
                               |
79 | 52 | lep1d 8890 |
. . . . . . . . . . 11
   
        
     
                       |
80 | 50, 52, 54, 78, 79 | letrd 8083 |
. . . . . . . . . 10
   
        
     
                                 |
81 | | f1ocnvfv2 5781 |
. . . . . . . . . . . 12
                        |
82 | 36, 46, 81 | sylancr 414 |
. . . . . . . . . . 11
       
         
       
       |
83 | 82 | adantr 276 |
. . . . . . . . . 10
   
        
     
                                  |
84 | 80, 83 | breqtrrd 4033 |
. . . . . . . . 9
   
        
     
                                          |
85 | 66, 67 | mp1i 10 |
. . . . . . . . . . . 12
       
         
       |
86 | 85, 46 | ffvelcdmd 5654 |
. . . . . . . . . . 11
       
         
         |
87 | 63, 26, 47, 86 | frec2uzled 10431 |
. . . . . . . . . 10
       
         
             
      
                 |
88 | 87 | adantr 276 |
. . . . . . . . 9
   
        
     
                         
                
       
      |
89 | 84, 88 | mpbird 167 |
. . . . . . . 8
   
        
     
                                  |
90 | 55 | adantr 276 |
. . . . . . . . . . . . . . . . . 18
   
        
     
                      
                                                       |
91 | | simpr 110 |
. . . . . . . . . . . . . . . . . . 19
   
        
     
                  
                    |
92 | 91 | iffalsed 3546 |
. . . . . . . . . . . . . . . . . 18
   
        
     
                                                                            
                   |
93 | 90, 92 | eqtrd 2210 |
. . . . . . . . . . . . . . . . 17
   
        
     
                      
                            |
94 | 93 | dmeqd 4831 |
. . . . . . . . . . . . . . . 16
   
        
     
                  
                                |
95 | | dmun 4836 |
. . . . . . . . . . . . . . . 16
                                                 |
96 | 94, 95 | eqtrdi 2226 |
. . . . . . . . . . . . . . 15
   
        
     
                  
                                |
97 | | fof 5440 |
. . . . . . . . . . . . . . . . . . . 20
           |
98 | 40, 97 | syl 14 |
. . . . . . . . . . . . . . . . . . 19
       
         
      |
99 | 98, 71 | ffvelcdmd 5654 |
. . . . . . . . . . . . . . . . . 18
       
         
           |
100 | 99 | adantr 276 |
. . . . . . . . . . . . . . . . 17
   
        
     
                              |
101 | | dmsnopg 5102 |
. . . . . . . . . . . . . . . . 17
           
                        |
102 | 100, 101 | syl 14 |
. . . . . . . . . . . . . . . 16
   
        
     
                  
                          |
103 | 102 | uneq2d 3291 |
. . . . . . . . . . . . . . 15
   
        
     
                                                
        |
104 | 96, 103 | eqtrd 2210 |
. . . . . . . . . . . . . 14
   
        
     
                  
                    |
105 | | df-suc 4373 |
. . . . . . . . . . . . . 14
                 |
106 | 104, 105 | eqtr4di 2228 |
. . . . . . . . . . . . 13
   
        
     
                  
            |
107 | | simplr 528 |
. . . . . . . . . . . . . 14
   
        
     
                  
           |
108 | 71 | adantr 276 |
. . . . . . . . . . . . . . 15
   
        
     
                          |
109 | | nnsucsssuc 6495 |
. . . . . . . . . . . . . . 15
                     
            |
110 | 64, 108, 109 | syl2an2r 595 |
. . . . . . . . . . . . . 14
   
        
     
                            
            |
111 | 107, 110 | mpbid 147 |
. . . . . . . . . . . . 13
   
        
     
                  
           |
112 | 106, 111 | eqsstrd 3193 |
. . . . . . . . . . . 12
   
        
     
                  
             |
113 | | 0zd 9267 |
. . . . . . . . . . . . 13
   
        
     
                     |
114 | 47 | adantr 276 |
. . . . . . . . . . . . 13
   
        
     
                  
        |
115 | | peano2 4596 |
. . . . . . . . . . . . . 14
             |
116 | 108, 115 | syl 14 |
. . . . . . . . . . . . 13
   
        
     
                  
       |
117 | 113, 26, 114, 116 | frec2uzled 10431 |
. . . . . . . . . . . 12
   
        
     
                         
              
            |
118 | 112, 117 | mpbid 147 |
. . . . . . . . . . 11
   
        
     
                                        |
119 | 113, 26, 108 | frec2uzsucd 10403 |
. . . . . . . . . . . 12
   
        
     
                                         |
120 | 75 | adantr 276 |
. . . . . . . . . . . . 13
   
        
     
                              |
121 | 120 | oveq1d 5892 |
. . . . . . . . . . . 12
   
        
     
                                  |
122 | 119, 121 | eqtrd 2210 |
. . . . . . . . . . 11
   
        
     
                                |
123 | 118, 122 | breqtrd 4031 |
. . . . . . . . . 10
   
        
     
                                 |
124 | 82 | adantr 276 |
. . . . . . . . . 10
   
        
     
                                  |
125 | 123, 124 | breqtrrd 4033 |
. . . . . . . . 9
   
        
     
                                          |
126 | 86 | adantr 276 |
. . . . . . . . . 10
   
        
     
                            |
127 | 113, 26, 114, 126 | frec2uzled 10431 |
. . . . . . . . 9
   
        
     
                                
      
                 |
128 | 125, 127 | mpbird 167 |
. . . . . . . 8
   
        
     
                  
               |
129 | 39, 40, 71 | ennnfonelemdc 12402 |
. . . . . . . . 9
       
         
DECID                     |
130 | | exmiddc 836 |
. . . . . . . . 9
DECID                  
                                        |
131 | 129, 130 | syl 14 |
. . . . . . . 8
       
         
                                        |
132 | 89, 128, 131 | mpjaodan 798 |
. . . . . . 7
       
         
               |
133 | 132 | ex 115 |
. . . . . 6
 
    
                          |
134 | 133 | expcom 116 |
. . . . 5
    
          
                 |
135 | 134 | a2d 26 |
. . . 4
    
 
         
    
             |
136 | 6, 11, 16, 21, 35, 135 | uzind4 9590 |
. . 3
    
             |
137 | 136, 43 | eleq2s 2272 |
. 2

             |
138 | 1, 137 | mpcom 36 |
1
            |