Step | Hyp | Ref
| Expression |
1 | | ennnfonelemhf1o.p |
. 2
   |
2 | | fveq2 5511 |
. . . . 5
           |
3 | 2 | dmeqd 4825 |
. . . . 5
           |
4 | | fveq2 5511 |
. . . . . 6
             |
5 | 4 | imaeq2d 4966 |
. . . . 5
                     |
6 | 2, 3, 5 | f1oeq123d 5451 |
. . . 4
                      
                        |
7 | 6 | imbi2d 230 |
. . 3
  
                     
                          |
8 | | fveq2 5511 |
. . . . 5
           |
9 | 8 | dmeqd 4825 |
. . . . 5
           |
10 | | fveq2 5511 |
. . . . . 6
             |
11 | 10 | imaeq2d 4966 |
. . . . 5
                     |
12 | 8, 9, 11 | f1oeq123d 5451 |
. . . 4
                      
                        |
13 | 12 | imbi2d 230 |
. . 3
  
                     
                          |
14 | | fveq2 5511 |
. . . . 5
               |
15 | 14 | dmeqd 4825 |
. . . . 5
               |
16 | | fveq2 5511 |
. . . . . 6
                 |
17 | 16 | imaeq2d 4966 |
. . . . 5
                         |
18 | 14, 15, 17 | f1oeq123d 5451 |
. . . 4
                        
                              |
19 | 18 | imbi2d 230 |
. . 3
    
                     
                                |
20 | | fveq2 5511 |
. . . . 5
           |
21 | 20 | dmeqd 4825 |
. . . . 5
           |
22 | | fveq2 5511 |
. . . . . 6
             |
23 | 22 | imaeq2d 4966 |
. . . . 5
                     |
24 | 20, 21, 23 | f1oeq123d 5451 |
. . . 4
                      
                        |
25 | 24 | imbi2d 230 |
. . 3
  
                     
                          |
26 | | f1o0 5494 |
. . . 4
     |
27 | | ennnfonelemh.dceq |
. . . . . 6
  
DECID   |
28 | | ennnfonelemh.f |
. . . . . 6
       |
29 | | ennnfonelemh.ne |
. . . . . 6
   
           |
30 | | ennnfonelemh.g |
. . . . . 6
 
 
                          |
31 | | ennnfonelemh.n |
. . . . . 6
frec        |
32 | | ennnfonelemh.j |
. . . . . 6
               |
33 | | ennnfonelemh.h |
. . . . . 6
      |
34 | 27, 28, 29, 30, 31, 32, 33 | ennnfonelem0 12386 |
. . . . 5
       |
35 | 34 | dmeqd 4825 |
. . . . . 6
       |
36 | | dm0 4837 |
. . . . . 6
 |
37 | 35, 36 | eqtrdi 2226 |
. . . . 5
       |
38 | | 0zd 9251 |
. . . . . . . . . . . 12
  |
39 | 38, 31 | frec2uz0d 10382 |
. . . . . . . . . . 11
      |
40 | 39 | mptru 1362 |
. . . . . . . . . 10
     |
41 | 40 | fveq2i 5514 |
. . . . . . . . 9
               |
42 | 38, 31 | frec2uzf1od 10389 |
. . . . . . . . . . 11
          |
43 | 42 | mptru 1362 |
. . . . . . . . . 10
         |
44 | | peano1 4590 |
. . . . . . . . . 10
 |
45 | | f1ocnvfv1 5772 |
. . . . . . . . . 10
                      |
46 | 43, 44, 45 | mp2an 426 |
. . . . . . . . 9
          |
47 | 41, 46 | eqtr3i 2200 |
. . . . . . . 8
      |
48 | 47 | imaeq2i 4964 |
. . . . . . 7
              |
49 | | ima0 4983 |
. . . . . . 7
     |
50 | 48, 49 | eqtri 2198 |
. . . . . 6
          |
51 | 50 | a1i 9 |
. . . . 5
            |
52 | 34, 37, 51 | f1oeq123d 5451 |
. . . 4
                              |
53 | 26, 52 | mpbiri 168 |
. . 3
                        |
54 | | simplr 528 |
. . . . . . . 8
   
                                                                 |
55 | 27 | ad2antrr 488 |
. . . . . . . . . . . 12
                          

DECID
  |
56 | 28 | ad2antrr 488 |
. . . . . . . . . . . 12
                                |
57 | 29 | ad2antrr 488 |
. . . . . . . . . . . 12
                                        |
58 | | simplr 528 |
. . . . . . . . . . . 12
                            |
59 | 55, 56, 57, 30, 31, 32, 33, 58 | ennnfonelemp1 12387 |
. . . . . . . . . . 11
                                                                                     |
60 | 59 | adantr 276 |
. . . . . . . . . 10
   
                                                                                                     |
61 | | simpr 110 |
. . . . . . . . . . 11
   
                                                              |
62 | 61 | iftrued 3541 |
. . . . . . . . . 10
   
                                                                                                   |
63 | 60, 62 | eqtrd 2210 |
. . . . . . . . 9
   
                                                      |
64 | 63 | dmeqd 4825 |
. . . . . . . . 9
   
                                         
            |
65 | | 0zd 9251 |
. . . . . . . . . . . . . . . . . 18
                            |
66 | 31 | frechashgf1o 10411 |
. . . . . . . . . . . . . . . . . . . . 21
     |
67 | 66 | a1i 9 |
. . . . . . . . . . . . . . . . . . . 20
                                |
68 | | f1ocnv 5470 |
. . . . . . . . . . . . . . . . . . . 20
    
       |
69 | | f1of 5457 |
. . . . . . . . . . . . . . . . . . . 20
     
       |
70 | 67, 68, 69 | 3syl 17 |
. . . . . . . . . . . . . . . . . . 19
                                 |
71 | 70, 58 | ffvelcdmd 5648 |
. . . . . . . . . . . . . . . . . 18
                                 |
72 | 65, 31, 71 | frec2uzsucd 10384 |
. . . . . . . . . . . . . . . . 17
                                                |
73 | | f1ocnvfv2 5773 |
. . . . . . . . . . . . . . . . . . 19
                  |
74 | 66, 58, 73 | sylancr 414 |
. . . . . . . . . . . . . . . . . 18
                                     |
75 | 74 | oveq1d 5884 |
. . . . . . . . . . . . . . . . 17
                                         |
76 | 72, 75 | eqtrd 2210 |
. . . . . . . . . . . . . . . 16
                                       |
77 | 76 | fveq2d 5515 |
. . . . . . . . . . . . . . 15
                                
                |
78 | | peano2 4591 |
. . . . . . . . . . . . . . . . 17
             |
79 | 71, 78 | syl 14 |
. . . . . . . . . . . . . . . 16
                                 |
80 | | f1ocnvfv1 5772 |
. . . . . . . . . . . . . . . 16
                                 |
81 | 66, 79, 80 | sylancr 414 |
. . . . . . . . . . . . . . 15
                                
              |
82 | 77, 81 | eqtr3d 2212 |
. . . . . . . . . . . . . 14
                                        |
83 | | df-suc 4368 |
. . . . . . . . . . . . . 14
                    |
84 | 82, 83 | eqtrdi 2226 |
. . . . . . . . . . . . 13
                                                 |
85 | 84 | imaeq2d 4966 |
. . . . . . . . . . . 12
                                                         |
86 | | imaundi 5037 |
. . . . . . . . . . . 12
                                         |
87 | 85, 86 | eqtrdi 2226 |
. . . . . . . . . . 11
                                                             |
88 | 87 | adantr 276 |
. . . . . . . . . 10
   
                                                                             |
89 | 61 | snssd 3736 |
. . . . . . . . . . . 12
   
                                                                |
90 | | ssequn2 3308 |
. . . . . . . . . . . 12
                    
                                 |
91 | 89, 90 | sylib 122 |
. . . . . . . . . . 11
   
                                                                           |
92 | | fofn 5436 |
. . . . . . . . . . . . . . . 16
    
  |
93 | 56, 92 | syl 14 |
. . . . . . . . . . . . . . 15
                            |
94 | | fnsnfv 5571 |
. . . . . . . . . . . . . . 15
                                |
95 | 93, 71, 94 | syl2anc 411 |
. . . . . . . . . . . . . 14
                                                  |
96 | 95 | uneq2d 3289 |
. . . . . . . . . . . . 13
                                                                        |
97 | 96 | eqeq1d 2186 |
. . . . . . . . . . . 12
                                                                                            |
98 | 97 | adantr 276 |
. . . . . . . . . . 11
   
                                                                                                            |
99 | 91, 98 | mpbid 147 |
. . . . . . . . . 10
   
                                                                           |
100 | 88, 99 | eqtrd 2210 |
. . . . . . . . 9
   
                                                                |
101 | 63, 64, 100 | f1oeq123d 5451 |
. . . . . . . 8
   
                                                                                              |
102 | 54, 101 | mpbird 167 |
. . . . . . 7
   
                                                                       |
103 | | simplr 528 |
. . . . . . . . 9
   
                                                                 |
104 | 55, 56, 57, 30, 31, 32, 33, 58 | ennnfonelemom 12389 |
. . . . . . . . . . . 12
                                |
105 | 104 | adantr 276 |
. . . . . . . . . . 11
   
                                                |
106 | | fof 5434 |
. . . . . . . . . . . . . 14
           |
107 | 56, 106 | syl 14 |
. . . . . . . . . . . . 13
                                |
108 | 107, 71 | ffvelcdmd 5648 |
. . . . . . . . . . . 12
                                     |
109 | 108 | adantr 276 |
. . . . . . . . . . 11
   
                                                     |
110 | | f1osng 5498 |
. . . . . . . . . . 11
                                                         |
111 | 105, 109,
110 | syl2anc 411 |
. . . . . . . . . 10
   
                                                                                   |
112 | 95 | adantr 276 |
. . . . . . . . . . 11
   
                                                                  |
113 | | f1oeq3 5447 |
. . . . . . . . . . 11
                         
                                    
                                          |
114 | 112, 113 | syl 14 |
. . . . . . . . . 10
   
                                            
                                    
                                          |
115 | 111, 114 | mpbid 147 |
. . . . . . . . 9
   
                                                                                   |
116 | | nnord 4608 |
. . . . . . . . . 10
           |
117 | | orddisj 4542 |
. . . . . . . . . 10
         
         |
118 | 105, 116,
117 | 3syl 17 |
. . . . . . . . 9
   
                                              
         |
119 | 112 | ineq2d 3336 |
. . . . . . . . . 10
   
                                                                                        |
120 | | simpr 110 |
. . . . . . . . . . 11
   
                                                              |
121 | | disjsn 3653 |
. . . . . . . . . . 11
                                           |
122 | 120, 121 | sylibr 134 |
. . . . . . . . . 10
   
                                                                  |
123 | 119, 122 | eqtr3d 2212 |
. . . . . . . . 9
   
                                                                  |
124 | | f1oun 5477 |
. . . . . . . . 9
                                                                                                                                                                     |
125 | 103, 115,
118, 123, 124 | syl22anc 1239 |
. . . . . . . 8
   
                                                                                                          |
126 | 59 | adantr 276 |
. . . . . . . . . 10
   
                                                                                                     |
127 | 120 | iffalsed 3544 |
. . . . . . . . . 10
   
                                                                                                   
                   |
128 | 126, 127 | eqtrd 2210 |
. . . . . . . . 9
   
                                                      
                   |
129 | 55 | adantr 276 |
. . . . . . . . . . 11
   
                                          

DECID
  |
130 | 56 | adantr 276 |
. . . . . . . . . . 11
   
                                                |
131 | 57 | adantr 276 |
. . . . . . . . . . 11
   
                                                        |
132 | 58 | adantr 276 |
. . . . . . . . . . 11
   
                                            |
133 | 129, 130,
131, 30, 31, 32, 33, 132, 120 | ennnfonelemhdmp1 12390 |
. . . . . . . . . 10
   
                                                      |
134 | | df-suc 4368 |
. . . . . . . . . 10
                 |
135 | 133, 134 | eqtrdi 2226 |
. . . . . . . . 9
   
                                                              |
136 | 87 | adantr 276 |
. . . . . . . . 9
   
                                                                             |
137 | 128, 135,
136 | f1oeq123d 5451 |
. . . . . . . 8
   
                                                                            
                        
                                 |
138 | 125, 137 | mpbird 167 |
. . . . . . 7
   
                                                                       |
139 | 55, 56, 71 | ennnfonelemdc 12380 |
. . . . . . . 8
                         
DECID                     |
140 | | exmiddc 836 |
. . . . . . . 8
DECID                  
                                        |
141 | 139, 140 | syl 14 |
. . . . . . 7
                                                                  |
142 | 102, 138,
141 | mpjaodan 798 |
. . . . . 6
                                                       |
143 | 142 | ex 115 |
. . . . 5
 

                     
                              |
144 | 143 | expcom 116 |
. . . 4

                      
                               |
145 | 144 | a2d 26 |
. . 3

                                                        |
146 | 7, 13, 19, 25, 53, 145 | nn0ind 9353 |
. 2

                         |
147 | 1, 146 | mpcom 36 |
1
                        |