Step | Hyp | Ref
| Expression |
1 | | frecabcl.as |
. . . . 5
   |
2 | 1 | adantr 276 |
. . . 4
 

  |
3 | | peano1 4590 |
. . . . . . . . 9
 |
4 | | elex2 2753 |
. . . . . . . . 9

   |
5 | | r19.9rmv 3514 |
. . . . . . . . 9
       |
6 | 3, 4, 5 | mp2b 8 |
. . . . . . . 8

   |
7 | | frecabcl.g |
. . . . . . . . . . . . . . 15
       |
8 | | fdm 5367 |
. . . . . . . . . . . . . . 15
       |
9 | 7, 8 | syl 14 |
. . . . . . . . . . . . . 14
   |
10 | 9 | adantr 276 |
. . . . . . . . . . . . 13
 

  |
11 | | eqeq2 2187 |
. . . . . . . . . . . . . 14


   |
12 | 11 | adantl 277 |
. . . . . . . . . . . . 13
 


   |
13 | 10, 12 | mpbid 147 |
. . . . . . . . . . . 12
 

  |
14 | 13 | adantr 276 |
. . . . . . . . . . 11
       |
15 | 14 | biantrurd 305 |
. . . . . . . . . 10
     

    |
16 | | peano3 4592 |
. . . . . . . . . . . . . . . 16
   |
17 | 16 | adantl 277 |
. . . . . . . . . . . . . . 15
       |
18 | 17, 14 | neeqtrrd 2377 |
. . . . . . . . . . . . . 14
    
  |
19 | 18 | necomd 2433 |
. . . . . . . . . . . . 13
    
  |
20 | 19 | neneqd 2368 |
. . . . . . . . . . . 12
       |
21 | 20 | intnanrd 932 |
. . . . . . . . . . 11
                 |
22 | | biorf 744 |
. . . . . . . . . . 11
            
  
               |
23 | 21, 22 | syl 14 |
. . . . . . . . . 10
      
  
               |
24 | 15, 23 | bitrd 188 |
. . . . . . . . 9
     
 
               |
25 | 24 | rexbidva 2474 |
. . . . . . . 8
 

 
                  |
26 | 6, 25 | bitrid 192 |
. . . . . . 7
 


                  |
27 | | r19.44mv 3517 |
. . . . . . . 8
     
           
 

               |
28 | 3, 4, 27 | mp2b 8 |
. . . . . . 7
   
           
 

              |
29 | 26, 28 | bitrdi 196 |
. . . . . 6
 


                  |
30 | 29 | alrimiv 1874 |
. . . . 5
 

                     |
31 | 2, 30 | jca 306 |
. . . 4
 


                      |
32 | | eleq1 2240 |
. . . . . 6
 
   |
33 | | eleq2 2241 |
. . . . . . . 8
 
   |
34 | 33 | bibi1d 233 |
. . . . . . 7
                                       |
35 | 34 | albidv 1824 |
. . . . . 6
                                           |
36 | 32, 35 | anbi12d 473 |
. . . . 5
     
 

                                      |
37 | 36 | spcegv 2825 |
. . . 4
     
 

             
     
 

                 |
38 | 2, 31, 37 | sylc 62 |
. . 3
 

     
 

                |
39 | | fveq2 5511 |
. . . . . . . . 9
                   |
40 | 39 | eleq1d 2246 |
. . . . . . . 8
         
           |
41 | | frecabcl.fs |
. . . . . . . . 9
        |
42 | 41 | ad2antrr 488 |
. . . . . . . 8
     
      |
43 | 7 | ad2antrr 488 |
. . . . . . . . 9
           |
44 | | vex 2740 |
. . . . . . . . . . . 12
 |
45 | 44 | sucid 4414 |
. . . . . . . . . . 11
 |
46 | | eleq2 2241 |
. . . . . . . . . . 11
     |
47 | 45, 46 | mpbiri 168 |
. . . . . . . . . 10
   |
48 | 47 | adantl 277 |
. . . . . . . . 9
       |
49 | 43, 48 | ffvelcdmd 5648 |
. . . . . . . 8
           |
50 | 40, 42, 49 | rspcdva 2846 |
. . . . . . 7
               |
51 | | simpllr 534 |
. . . . . . . . . . . . 13
   

            |
52 | 43, 8 | syl 14 |
. . . . . . . . . . . . . . . 16
       |
53 | 52 | adantr 276 |
. . . . . . . . . . . . . . 15
   

            |
54 | | simplr 528 |
. . . . . . . . . . . . . . 15
   

            |
55 | 53, 54 | eqtrd 2210 |
. . . . . . . . . . . . . 14
   

            |
56 | | simpr 110 |
. . . . . . . . . . . . . 14
   

                    |
57 | 55, 56 | jca 306 |
. . . . . . . . . . . . 13
   

          
           |
58 | | suceq 4399 |
. . . . . . . . . . . . . . . 16

  |
59 | 58 | eqeq2d 2189 |
. . . . . . . . . . . . . . 15
     |
60 | | fveq2 5511 |
. . . . . . . . . . . . . . . . 17
           |
61 | 60 | fveq2d 5515 |
. . . . . . . . . . . . . . . 16
                   |
62 | 61 | eleq2d 2247 |
. . . . . . . . . . . . . . 15
         
           |
63 | 59, 62 | anbi12d 473 |
. . . . . . . . . . . . . 14
  
        

            |
64 | 63 | rspcev 2841 |
. . . . . . . . . . . . 13
                          |
65 | 51, 57, 64 | syl2anc 411 |
. . . . . . . . . . . 12
   

                       |
66 | 65 | ex 115 |
. . . . . . . . . . 11
                            |
67 | | simpr 110 |
. . . . . . . . . . . . . . 15
          
          |
68 | 67 | adantl 277 |
. . . . . . . . . . . . . 14
     
  
         
          |
69 | 52 | ad2antrr 488 |
. . . . . . . . . . . . . . . . . . 19
     
  
         
  |
70 | | simprl 529 |
. . . . . . . . . . . . . . . . . . 19
     
  
         
  |
71 | | simpllr 534 |
. . . . . . . . . . . . . . . . . . 19
     
  
         
  |
72 | 69, 70, 71 | 3eqtr3rd 2219 |
. . . . . . . . . . . . . . . . . 18
     
  
         
  |
73 | | simplr 528 |
. . . . . . . . . . . . . . . . . . . 20
       |
74 | 73 | ad2antrr 488 |
. . . . . . . . . . . . . . . . . . 19
     
  
         
  |
75 | | simplr 528 |
. . . . . . . . . . . . . . . . . . 19
     
  
         
  |
76 | | peano4 4593 |
. . . . . . . . . . . . . . . . . . 19
 
 
   |
77 | 74, 75, 76 | syl2anc 411 |
. . . . . . . . . . . . . . . . . 18
     
  
         

   |
78 | 72, 77 | mpbid 147 |
. . . . . . . . . . . . . . . . 17
     
  
         
  |
79 | 78 | fveq2d 5515 |
. . . . . . . . . . . . . . . 16
     
  
         
          |
80 | 79 | fveq2d 5515 |
. . . . . . . . . . . . . . 15
     
  
         
                  |
81 | 80 | eleq2d 2247 |
. . . . . . . . . . . . . 14
     
  
         
        
           |
82 | 68, 81 | mpbird 167 |
. . . . . . . . . . . . 13
     
  
         
          |
83 | 82 | ex 115 |
. . . . . . . . . . . 12
   

   
                    |
84 | 83 | rexlimdva 2594 |
. . . . . . . . . . 11
                            |
85 | 66, 84 | impbid 129 |
. . . . . . . . . 10
              
             |
86 | 85 | alrimiv 1874 |
. . . . . . . . 9
                              |
87 | | peano3 4592 |
. . . . . . . . . . . . . . . . . 18
   |
88 | 73, 87 | syl 14 |
. . . . . . . . . . . . . . . . 17
    
  |
89 | | neeq1 2360 |
. . . . . . . . . . . . . . . . . 18
 
   |
90 | 89 | adantl 277 |
. . . . . . . . . . . . . . . . 17
     
   |
91 | 88, 90 | mpbird 167 |
. . . . . . . . . . . . . . . 16
       |
92 | 52, 91 | eqnetrd 2371 |
. . . . . . . . . . . . . . 15
       |
93 | 92 | neneqd 2368 |
. . . . . . . . . . . . . 14
       |
94 | 93 | intnanrd 932 |
. . . . . . . . . . . . 13
         |
95 | | biorf 744 |
. . . . . . . . . . . . 13
  
 

            

             |
96 | 94, 95 | syl 14 |
. . . . . . . . . . . 12
                
   

             |
97 | | orcom 728 |
. . . . . . . . . . . 12
               
 

              |
98 | 96, 97 | bitrdi 196 |
. . . . . . . . . . 11
                
 

               |
99 | 98 | bibi2d 232 |
. . . . . . . . . 10
                          
                            |
100 | 99 | albidv 1824 |
. . . . . . . . 9
                
           
                              |
101 | 86, 100 | mpbid 147 |
. . . . . . . 8
                                  |
102 | 50, 101 | jca 306 |
. . . . . . 7
                                            |
103 | | eleq1 2240 |
. . . . . . . . 9
        

           |
104 | | eleq2 2241 |
. . . . . . . . . . 11
        

           |
105 | 104 | bibi1d 233 |
. . . . . . . . . 10
        
 
 

                                         |
106 | 105 | albidv 1824 |
. . . . . . . . 9
        
                                                  |
107 | 103, 106 | anbi12d 473 |
. . . . . . . 8
        
                                                              |
108 | 107 | spcegv 2825 |
. . . . . . 7
                                              
     
 

                 |
109 | 50, 102, 108 | sylc 62 |
. . . . . 6
                              |
110 | 109 | ex 115 |
. . . . 5
 

      
 

                 |
111 | 110 | rexlimdva 2594 |
. . . 4
                             |
112 | 111 | imp 124 |
. . 3
 
       
 

                |
113 | | frecabcl.n |
. . . 4
   |
114 | | nn0suc 4600 |
. . . 4
 

   |
115 | 113, 114 | syl 14 |
. . 3
  
   |
116 | 38, 112, 115 | mpjaodan 798 |
. 2
                          |
117 | | clabel 2304 |
. 2
    
            
     
 

                |
118 | 116, 117 | sylibr 134 |
1
                    |