Step | Hyp | Ref
| Expression |
1 | | frec2uzrdg.b |
. 2
   |
2 | | fveq2 5511 |
. . . . 5
           |
3 | | fveq2 5511 |
. . . . . 6
           |
4 | 2 | fveq2d 5515 |
. . . . . 6
                   |
5 | 3, 4 | opeq12d 3784 |
. . . . 5
                                 |
6 | 2, 5 | eqeq12d 2192 |
. . . 4
                                           |
7 | 6 | imbi2d 230 |
. . 3
  
                                            |
8 | | fveq2 5511 |
. . . . 5

          |
9 | | fveq2 5511 |
. . . . . 6

          |
10 | 8 | fveq2d 5515 |
. . . . . 6

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

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

                                          |
13 | | fveq2 5511 |
. . . . 5
           |
14 | | fveq2 5511 |
. . . . . 6
           |
15 | 13 | fveq2d 5515 |
. . . . . 6
                   |
16 | 14, 15 | opeq12d 3784 |
. . . . 5
                                 |
17 | 13, 16 | eqeq12d 2192 |
. . . 4
                                           |
18 | | fveq2 5511 |
. . . . 5
       
   |
19 | | fveq2 5511 |
. . . . . 6
       
   |
20 | 18 | fveq2d 5515 |
. . . . . 6
                   |
21 | 19, 20 | opeq12d 3784 |
. . . . 5
                                 |
22 | 18, 21 | eqeq12d 2192 |
. . . 4
                                           |
23 | | frecuzrdgrrn.2 |
. . . . . . 7
frec      
                |
24 | 23 | fveq1i 5512 |
. . . . . 6
    frec      
                   |
25 | | frec2uz.1 |
. . . . . . . 8
   |
26 | | frecuzrdgrrn.a |
. . . . . . . 8
   |
27 | | opexg 4225 |
. . . . . . . 8
 
      |
28 | 25, 26, 27 | syl2anc 411 |
. . . . . . 7
      |
29 | | frec0g 6392 |
. . . . . . 7
  
 frec                              |
30 | 28, 29 | syl 14 |
. . . . . 6
 frec                              |
31 | 24, 30 | eqtrid 2222 |
. . . . 5
          |
32 | | frec2uz.2 |
. . . . . . 7
frec        |
33 | 25, 32 | frec2uz0d 10385 |
. . . . . 6
       |
34 | 31 | fveq2d 5515 |
. . . . . . 7
                  |
35 | | uzid 9531 |
. . . . . . . . 9
       |
36 | 25, 35 | syl 14 |
. . . . . . . 8
       |
37 | | op2ndg 6146 |
. . . . . . . 8
                |
38 | 36, 26, 37 | syl2anc 411 |
. . . . . . 7
          |
39 | 34, 38 | eqtrd 2210 |
. . . . . 6
           |
40 | 33, 39 | opeq12d 3784 |
. . . . 5
               
     |
41 | 31, 40 | eqtr4d 2213 |
. . . 4
                      |
42 | | 1st2nd2 6170 |
. . . . . . . . . . . . . . 15
      
             |
43 | 42 | adantl 277 |
. . . . . . . . . . . . . 14
          
             |
44 | 43 | fveq2d 5515 |
. . . . . . . . . . . . 13
          
                                                     |
45 | | df-ov 5872 |
. . . . . . . . . . . . . . 15
                                                            |
46 | | xp1st 6160 |
. . . . . . . . . . . . . . . . 17
      
          |
47 | 46 | adantl 277 |
. . . . . . . . . . . . . . . 16
          
          |
48 | | xp2nd 6161 |
. . . . . . . . . . . . . . . . 17
      
      |
49 | 48 | adantl 277 |
. . . . . . . . . . . . . . . 16
          
      |
50 | | peano2uz 9572 |
. . . . . . . . . . . . . . . . . 18
        
            |
51 | 47, 50 | syl 14 |
. . . . . . . . . . . . . . . . 17
          
            |
52 | | frecuzrdgrrn.f |
. . . . . . . . . . . . . . . . . . . 20
 
    
        |
53 | 52 | ralrimivva 2559 |
. . . . . . . . . . . . . . . . . . 19
       
      |
54 | 53 | ad2antrr 488 |
. . . . . . . . . . . . . . . . . 18
          
      
      |
55 | | oveq1 5876 |
. . . . . . . . . . . . . . . . . . . . 21
    
              |
56 | 55 | eleq1d 2246 |
. . . . . . . . . . . . . . . . . . . 20
    
    
           |
57 | | oveq2 5877 |
. . . . . . . . . . . . . . . . . . . . 21
    
                      |
58 | 57 | eleq1d 2246 |
. . . . . . . . . . . . . . . . . . . 20
    
        
               |
59 | 56, 58 | rspc2v 2854 |
. . . . . . . . . . . . . . . . . . 19
                
     
                   |
60 | 47, 49, 59 | syl2anc 411 |
. . . . . . . . . . . . . . . . . 18
          
 
     
   
               |
61 | 54, 60 | mpd 13 |
. . . . . . . . . . . . . . . . 17
          
              |
62 | | opelxp 4653 |
. . . . . . . . . . . . . . . . 17
                     
     
          
               |
63 | 51, 61, 62 | sylanbrc 417 |
. . . . . . . . . . . . . . . 16
          
                             |
64 | | oveq1 5876 |
. . . . . . . . . . . . . . . . . 18
    
          |
65 | 64, 55 | opeq12d 3784 |
. . . . . . . . . . . . . . . . 17
    
        
                   |
66 | 57 | opeq2d 3783 |
. . . . . . . . . . . . . . . . 17
    
                
                       |
67 | | eqid 2177 |
. . . . . . . . . . . . . . . . 17
               
                 |
68 | 65, 66, 67 | ovmpog 6003 |
. . . . . . . . . . . . . . . 16
                                  
                  
                                       |
69 | 47, 49, 63, 68 | syl3anc 1238 |
. . . . . . . . . . . . . . 15
          
                                                   |
70 | 45, 69 | eqtr3id 2224 |
. . . . . . . . . . . . . 14
          
                                                      |
71 | 70, 63 | eqeltrd 2254 |
. . . . . . . . . . . . 13
          
                                       |
72 | 44, 71 | eqeltrd 2254 |
. . . . . . . . . . . 12
          
                            |
73 | 72 | ralrimiva 2550 |
. . . . . . . . . . 11
 

              
                     |
74 | 36 | adantr 276 |
. . . . . . . . . . . 12
 

      |
75 | 26 | adantr 276 |
. . . . . . . . . . . 12
 

  |
76 | | opelxp 4653 |
. . . . . . . . . . . 12
  
           
   |
77 | 74, 75, 76 | sylanbrc 417 |
. . . . . . . . . . 11
 

           |
78 | | simpr 110 |
. . . . . . . . . . 11
 

  |
79 | | frecsuc 6402 |
. . . . . . . . . . 11
                                              frec      
                                     frec                            |
80 | 73, 77, 78, 79 | syl3anc 1238 |
. . . . . . . . . 10
 

frec                                            frec                            |
81 | 23 | fveq1i 5512 |
. . . . . . . . . 10
  
 frec                          |
82 | 23 | fveq1i 5512 |
. . . . . . . . . . 11
    frec                          |
83 | 82 | fveq2i 5514 |
. . . . . . . . . 10
                                           frec                           |
84 | 80, 81, 83 | 3eqtr4g 2235 |
. . . . . . . . 9
 

          
                   |
85 | 84 | adantr 276 |
. . . . . . . 8
                       
  
                           |
86 | | fveq2 5511 |
. . . . . . . . 9
                                                                                 |
87 | | df-ov 5872 |
. . . . . . . . . 10
                                                                    |
88 | 25 | adantr 276 |
. . . . . . . . . . . 12
 

  |
89 | 88, 32, 78 | frec2uzuzd 10388 |
. . . . . . . . . . 11
 

          |
90 | 25, 32, 26, 52, 23 | frecuzrdgrrn 10394 |
. . . . . . . . . . . 12
 

            |
91 | | xp2nd 6161 |
. . . . . . . . . . . 12
          
          |
92 | 90, 91 | syl 14 |
. . . . . . . . . . 11
 

          |
93 | | peano2uz 9572 |
. . . . . . . . . . . . 13
        
            |
94 | 89, 93 | syl 14 |
. . . . . . . . . . . 12
 

            |
95 | 52 | caovclg 6021 |
. . . . . . . . . . . . . 14
 
    
        |
96 | 95 | adantlr 477 |
. . . . . . . . . . . . 13
                 |
97 | 96, 89, 92 | caovcld 6022 |
. . . . . . . . . . . 12
 

                  |
98 | | opelxp 4653 |
. . . . . . . . . . . 12
                               
          
                   |
99 | 94, 97, 98 | sylanbrc 417 |
. . . . . . . . . . 11
 

                        
        |
100 | | oveq1 5876 |
. . . . . . . . . . . . 13
               |
101 | | oveq1 5876 |
. . . . . . . . . . . . 13
                   |
102 | 100, 101 | opeq12d 3784 |
. . . . . . . . . . . 12
                                 |
103 | | oveq2 5877 |
. . . . . . . . . . . . 13
        
                          |
104 | 103 | opeq2d 3783 |
. . . . . . . . . . . 12
        
                
                           |
105 | | oveq1 5876 |
. . . . . . . . . . . . . 14
       |
106 | | oveq1 5876 |
. . . . . . . . . . . . . 14
           |
107 | 105, 106 | opeq12d 3784 |
. . . . . . . . . . . . 13
                     |
108 | | oveq2 5877 |
. . . . . . . . . . . . . 14
           |
109 | 108 | opeq2d 3783 |
. . . . . . . . . . . . 13
                     |
110 | 107, 109 | cbvmpov 5949 |
. . . . . . . . . . . 12
               
                 |
111 | 102, 104,
110 | ovmpog 6003 |
. . . . . . . . . . 11
                                                                                                             |
112 | 89, 92, 99, 111 | syl3anc 1238 |
. . . . . . . . . 10
 

                                                           |
113 | 87, 112 | eqtr3id 2224 |
. . . . . . . . 9
 

                                  
                           |
114 | 86, 113 | sylan9eqr 2232 |
. . . . . . . 8
                       
                                                   |
115 | 85, 114 | eqtrd 2210 |
. . . . . . 7
                       
  
                            |
116 | 88, 32, 78 | frec2uzsucd 10387 |
. . . . . . . . 9
 

            |
117 | 116 | adantr 276 |
. . . . . . . 8
                       
  
         |
118 | 115 | fveq2d 5515 |
. . . . . . . . 9
                       
                                       |
119 | 88, 32, 78 | frec2uzzd 10386 |
. . . . . . . . . . . 12
 

      |
120 | 119 | peano2zd 9367 |
. . . . . . . . . . 11
 

        |
121 | 120 | adantr 276 |
. . . . . . . . . 10
                       
        |
122 | 97 | adantr 276 |
. . . . . . . . . 10
                       
                  |
123 | | op2ndg 6146 |
. . . . . . . . . 10
                                                                        |
124 | 121, 122,
123 | syl2anc 411 |
. . . . . . . . 9
                       
                                               |
125 | 118, 124 | eqtrd 2210 |
. . . . . . . 8
                       
                          |
126 | 117, 125 | opeq12d 3784 |
. . . . . . 7
                       
              
                           |
127 | 115, 126 | eqtr4d 2213 |
. . . . . 6
                       
  
            
     |
128 | 127 | ex 115 |
. . . . 5
 

                                          |
129 | 128 | expcom 116 |
. . . 4
                                     
       |
130 | 12, 17, 22, 41, 129 | finds2 4597 |
. . 3
                        |
131 | 7, 130 | vtoclga 2803 |
. 2
                        |
132 | 1, 131 | mpcom 36 |
1
                      |