Step | Hyp | Ref
| Expression |
1 | | uzrdg.b |
. 2
   |
2 | | fveq2 5121 |
. . . . 5
           |
3 | | fveq2 5121 |
. . . . . 6
           |
4 | 2 | fveq2d 5125 |
. . . . . 6
                   |
5 | 3, 4 | opeq12d 3548 |
. . . . 5
                                 |
6 | 2, 5 | eqeq12d 2051 |
. . . 4
                    
                      |
7 | 6 | imbi2d 219 |
. . 3
            
              
                   |
8 | | fveq2 5121 |
. . . . 5

          |
9 | | fveq2 5121 |
. . . . . 6

          |
10 | 8 | fveq2d 5125 |
. . . . . 6

                  |
11 | 9, 10 | opeq12d 3548 |
. . . . 5

                                |
12 | 8, 11 | eqeq12d 2051 |
. . . 4

                   
                      |
13 | | fveq2 5121 |
. . . . 5
           |
14 | | fveq2 5121 |
. . . . . 6
           |
15 | 13 | fveq2d 5125 |
. . . . . 6
                   |
16 | 14, 15 | opeq12d 3548 |
. . . . 5
                                 |
17 | 13, 16 | eqeq12d 2051 |
. . . 4
                    
                      |
18 | | fveq2 5121 |
. . . . 5
           |
19 | | fveq2 5121 |
. . . . . 6
           |
20 | 18 | fveq2d 5125 |
. . . . . 6
                   |
21 | 19, 20 | opeq12d 3548 |
. . . . 5
      
        
     
           |
22 | 18, 21 | eqeq12d 2051 |
. . . 4
     
                  
     
            |
23 | | uzrdg.2 |
. . . . . . 7
frec        
 
            |
24 | 23 | fveq1i 5122 |
. . . . . 6
    frec      
                   |
25 | | frec2uz.1 |
. . . . . . . 8
   |
26 | | uzrdg.a |
. . . . . . . 8
   |
27 | | opexg 3955 |
. . . . . . . 8
 
      |
28 | 25, 26, 27 | syl2anc 391 |
. . . . . . 7
      |
29 | | frec0g 5922 |
. . . . . . 7
    frec      
                       |
30 | 28, 29 | syl 14 |
. . . . . 6
 frec      
                       |
31 | 24, 30 | syl5eq 2081 |
. . . . 5
          |
32 | | frec2uz.2 |
. . . . . . 7
frec  
     |
33 | 25, 32 | frec2uz0d 8866 |
. . . . . 6
       |
34 | 31 | fveq2d 5125 |
. . . . . . 7
                  |
35 | | uzid 8263 |
. . . . . . . . 9
       |
36 | 25, 35 | syl 14 |
. . . . . . . 8
       |
37 | | op2ndg 5720 |
. . . . . . . 8
     

         |
38 | 36, 26, 37 | syl2anc 391 |
. . . . . . 7
          |
39 | 34, 38 | eqtrd 2069 |
. . . . . 6
           |
40 | 33, 39 | opeq12d 3548 |
. . . . 5
               
     |
41 | 31, 40 | eqtr4d 2072 |
. . . 4
                      |
42 | | zex 8030 |
. . . . . . . . . . . . . . . 16
 |
43 | | uzssz 8268 |
. . . . . . . . . . . . . . . 16
   
 |
44 | 42, 43 | ssexi 3886 |
. . . . . . . . . . . . . . 15
   
 |
45 | 44 | a1i 9 |
. . . . . . . . . . . . . 14
      
  |
46 | | uzrdg.s |
. . . . . . . . . . . . . . 15
   |
47 | 46 | adantr 261 |
. . . . . . . . . . . . . 14
     |
48 | | mpt2exga 5777 |
. . . . . . . . . . . . . 14
       
      
          |
49 | 45, 47, 48 | syl2anc 391 |
. . . . . . . . . . . . 13
        
            |
50 | | vex 2554 |
. . . . . . . . . . . . . 14
 |
51 | 50 | a1i 9 |
. . . . . . . . . . . . 13
     |
52 | | fvexg 5137 |
. . . . . . . . . . . . 13
         
 
        
      
 
           |
53 | 49, 51, 52 | syl2anc 391 |
. . . . . . . . . . . 12
         
               |
54 | 53 | alrimiv 1751 |
. . . . . . . . . . 11
             
 
           |
55 | 28 | adantr 261 |
. . . . . . . . . . 11
        |
56 | | simpr 103 |
. . . . . . . . . . 11
     |
57 | | frecsuc 5930 |
. . . . . . . . . . 11
          
                 frec      
                 
 
      
 
        frec        
                   |
58 | 54, 55, 56, 57 | syl3anc 1134 |
. . . . . . . . . 10
   frec        
               
 
      
          frec      
                     |
59 | 23 | fveq1i 5122 |
. . . . . . . . . 10
  
 frec      
                   |
60 | 23 | fveq1i 5122 |
. . . . . . . . . . 11
    frec      
                   |
61 | 60 | fveq2i 5124 |
. . . . . . . . . 10
        
              
 
      
 
        frec        
                  |
62 | 58, 59, 61 | 3eqtr4g 2094 |
. . . . . . . . 9
               
 
               |
63 | 62 | adantr 261 |
. . . . . . . 8
                                  
                   |
64 | | fveq2 5121 |
. . . . . . . . 9
                   
 
      
 
                     
 
                          |
65 | | df-ov 5458 |
. . . . . . . . . 10
             
 
               
 
      
 
                         |
66 | 25 | adantr 261 |
. . . . . . . . . . . 12
     |
67 | 66, 32, 56 | frec2uzuzd 8869 |
. . . . . . . . . . 11
      
      |
68 | | uzrdg.f |
. . . . . . . . . . . . 13
      
 
      |
69 | 25, 32, 46, 26, 68, 23 | frecuzrdgrrn 8875 |
. . . . . . . . . . . 12
      
        |
70 | | xp2nd 5735 |
. . . . . . . . . . . 12
         
        
  |
71 | 69, 70 | syl 14 |
. . . . . . . . . . 11
          
  |
72 | | peano2uz 8302 |
. . . . . . . . . . . . 13
                     |
73 | 67, 72 | syl 14 |
. . . . . . . . . . . 12
               |
74 | 68 | caovclg 5595 |
. . . . . . . . . . . . . 14
      
 
      |
75 | 74 | adantlr 446 |
. . . . . . . . . . . . 13
    
   
        |
76 | 75, 67, 71 | caovcld 5596 |
. . . . . . . . . . . 12
                  
  |
77 | | opelxp 4317 |
. . . . . . . . . . . 12
      
                  
           
                    
   |
78 | 73, 76, 77 | sylanbrc 394 |
. . . . . . . . . . 11
                           
        |
79 | | oveq1 5462 |
. . . . . . . . . . . . 13
    

         |
80 | | oveq1 5462 |
. . . . . . . . . . . . 13
    
              |
81 | 79, 80 | opeq12d 3548 |
. . . . . . . . . . . 12
    
 
            
             |
82 | | oveq2 5463 |
. . . . . . . . . . . . 13
                                   |
83 | 82 | opeq2d 3547 |
. . . . . . . . . . . 12
                               
 
                   |
84 | | oveq1 5462 |
. . . . . . . . . . . . . 14
 
     |
85 | | oveq1 5462 |
. . . . . . . . . . . . . 14
           |
86 | 84, 85 | opeq12d 3548 |
. . . . . . . . . . . . 13
                     |
87 | | oveq2 5463 |
. . . . . . . . . . . . . 14
           |
88 | 87 | opeq2d 3547 |
. . . . . . . . . . . . 13
                     |
89 | 86, 88 | cbvmpt2v 5526 |
. . . . . . . . . . . 12
     
         

      
         |
90 | 81, 83, 89 | ovmpt2g 5577 |
. . . . . . . . . . 11
     
   
                                
                    
 
               
     
                     |
91 | 67, 71, 78, 90 | syl3anc 1134 |
. . . . . . . . . 10
                
                                             |
92 | 65, 91 | syl5eqr 2083 |
. . . . . . . . 9
         
                                 
                     |
93 | 64, 92 | sylan9eqr 2091 |
. . . . . . . 8
                         
      
 
                  
                     |
94 | 63, 93 | eqtrd 2069 |
. . . . . . 7
                                                       |
95 | 66, 32, 56 | frec2uzsucd 8868 |
. . . . . . . . 9
           
   |
96 | 95 | adantr 261 |
. . . . . . . 8
                                    |
97 | 94 | fveq2d 5125 |
. . . . . . . . 9
                                        
                      |
98 | 66, 32, 56 | frec2uzzd 8867 |
. . . . . . . . . . . 12
      
  |
99 | 98 | peano2zd 8139 |
. . . . . . . . . . 11
           |
100 | 99 | adantr 261 |
. . . . . . . . . 10
                                |
101 | 76 | adantr 261 |
. . . . . . . . . 10
                                       
  |
102 | | op2ndg 5720 |
. . . . . . . . . 10
      

               
         
                                      |
103 | 100, 101,
102 | syl2anc 391 |
. . . . . . . . 9
                                                                       |
104 | 97, 103 | eqtrd 2069 |
. . . . . . . 8
                                                  |
105 | 96, 104 | opeq12d 3548 |
. . . . . . 7
                             
              
                     |
106 | 94, 105 | eqtr4d 2072 |
. . . . . 6
                                       
     |
107 | 106 | ex 108 |
. . . . 5
             
        
               
      |
108 | 107 | expcom 109 |
. . . 4
            
        
               
       |
109 | 12, 17, 22, 41, 108 | finds2 4267 |
. . 3
     
                  |
110 | 7, 109 | vtoclga 2613 |
. 2
     
                  |
111 | 1, 110 | mpcom 32 |
1
    
                 |