Step | Hyp | Ref
| Expression |
1 | | df-seqfrec 10419 |
. 2
 
 frec               
               |
2 | | seqvalcd.m |
. . . . . 6
   |
3 | | seqvalcd.f0 |
. . . . . 6
       |
4 | | ssv 3177 |
. . . . . . 7
 |
5 | 4 | a1i 9 |
. . . . . 6

  |
6 | | eqidd 2178 |
. . . . . . . 8
 
    
       
              
           |
7 | | simprr 531 |
. . . . . . . . 9
               |
8 | | simprl 529 |
. . . . . . . . . 10
               |
9 | 8 | fvoveq1d 5890 |
. . . . . . . . 9
                      
    |
10 | 7, 9 | oveq12d 5886 |
. . . . . . . 8
             
                 |
11 | | simprl 529 |
. . . . . . . 8
 
    
        |
12 | | simprr 531 |
. . . . . . . 8
 
    
    |
13 | | seqvalcd.pl |
. . . . . . . . . . . 12
 

      |
14 | 13 | ralrimivva 2559 |
. . . . . . . . . . 11
  

   |
15 | | oveq1 5875 |
. . . . . . . . . . . . 13
 
     |
16 | 15 | eleq1d 2246 |
. . . . . . . . . . . 12
   
     |
17 | | oveq2 5876 |
. . . . . . . . . . . . 13
 
     |
18 | 17 | eleq1d 2246 |
. . . . . . . . . . . 12
   
     |
19 | 16, 18 | cbvral2v 2716 |
. . . . . . . . . . 11
 



 
    |
20 | 14, 19 | sylib 122 |
. . . . . . . . . 10
  
    |
21 | 20 | adantr 276 |
. . . . . . . . 9
 
    
  

    |
22 | | fveq2 5510 |
. . . . . . . . . . . 12
          
    |
23 | 22 | eleq1d 2246 |
. . . . . . . . . . 11
       
         |
24 | | seqvalcd.fp1 |
. . . . . . . . . . . . . 14
 
      
      |
25 | 24 | ralrimiva 2550 |
. . . . . . . . . . . . 13
               |
26 | | fveq2 5510 |
. . . . . . . . . . . . . . 15
           |
27 | 26 | eleq1d 2246 |
. . . . . . . . . . . . . 14
     
       |
28 | 27 | cbvralv 2703 |
. . . . . . . . . . . . 13
 
   
                     |
29 | 25, 28 | sylib 122 |
. . . . . . . . . . . 12
               |
30 | 29 | adantr 276 |
. . . . . . . . . . 11
 
    
                |
31 | | eluzp1p1 9529 |
. . . . . . . . . . . 12
    
          |
32 | 11, 31 | syl 14 |
. . . . . . . . . . 11
 
    
       
    |
33 | 23, 30, 32 | rspcdva 2846 |
. . . . . . . . . 10
 
    
          |
34 | | oveq12 5877 |
. . . . . . . . . . . 12
 
             
     |
35 | 34 | eleq1d 2246 |
. . . . . . . . . . 11
 
                     |
36 | 35 | rspc2gv 2853 |
. . . . . . . . . 10
                         |
37 | 12, 33, 36 | syl2anc 411 |
. . . . . . . . 9
 
    
   

             |
38 | 21, 37 | mpd 13 |
. . . . . . . 8
 
    
  
         |
39 | 6, 10, 11, 12, 38 | ovmpod 5995 |
. . . . . . 7
 
    
         
                     |
40 | 39, 38 | eqeltrd 2254 |
. . . . . 6
 
    
         
             |
41 | | seqvalcd.r |
. . . . . 6
frec      
                                   |
42 | 2, 3, 5, 40, 41 | frecuzrdgrclt 10388 |
. . . . 5
             |
43 | 42 | ffnd 5361 |
. . . 4
   |
44 | | 1st2nd2 6169 |
. . . . . . . . . . . 12
      
             |
45 | 44 | adantl 277 |
. . . . . . . . . . 11
 
      
             |
46 | 45 | fveq2d 5514 |
. . . . . . . . . 10
 
      
                                                             |
47 | | df-ov 5871 |
. . . . . . . . . 10
                    
                          
                    |
48 | 46, 47 | eqtr4di 2228 |
. . . . . . . . 9
 
      
                                            
             |
49 | | xp1st 6159 |
. . . . . . . . . . 11
      
          |
50 | 49 | adantl 277 |
. . . . . . . . . 10
 
      
          |
51 | | xp2nd 6160 |
. . . . . . . . . . . 12
      
      |
52 | 51 | adantl 277 |
. . . . . . . . . . 11
 
      
      |
53 | 52 | elexd 2750 |
. . . . . . . . . 10
 
      
      |
54 | | peano2uz 9559 |
. . . . . . . . . . . 12
        
            |
55 | 50, 54 | syl 14 |
. . . . . . . . . . 11
 
      
            |
56 | 14 | adantr 276 |
. . . . . . . . . . . 12
 
      


    |
57 | | fveq2 5510 |
. . . . . . . . . . . . . . 15
      
                |
58 | 57 | eleq1d 2246 |
. . . . . . . . . . . . . 14
      
    
             |
59 | 25 | adantr 276 |
. . . . . . . . . . . . . 14
 
      
              |
60 | | eluzp1p1 9529 |
. . . . . . . . . . . . . . 15
        
              |
61 | 50, 60 | syl 14 |
. . . . . . . . . . . . . 14
 
      
              |
62 | 58, 59, 61 | rspcdva 2846 |
. . . . . . . . . . . . 13
 
      
            |
63 | | oveq12 5877 |
. . . . . . . . . . . . . . 15
                 
                   |
64 | 63 | eleq1d 2246 |
. . . . . . . . . . . . . 14
                   
                   |
65 | 64 | rspc2gv 2853 |
. . . . . . . . . . . . 13
                          
              |
66 | 52, 62, 65 | syl2anc 411 |
. . . . . . . . . . . 12
 
      
 



                   |
67 | 56, 66 | mpd 13 |
. . . . . . . . . . 11
 
      
                  |
68 | 55, 67 | opelxpd 4655 |
. . . . . . . . . 10
 
      
            
                    |
69 | | oveq1 5875 |
. . . . . . . . . . . 12
    
          |
70 | | fvoveq1 5891 |
. . . . . . . . . . . . 13
    
                  |
71 | 70 | oveq2d 5884 |
. . . . . . . . . . . 12
    
                      |
72 | 69, 71 | opeq12d 3784 |
. . . . . . . . . . 11
    
            
                       |
73 | | oveq1 5875 |
. . . . . . . . . . . 12
    
                
             |
74 | 73 | opeq2d 3783 |
. . . . . . . . . . 11
    
                    
            
              |
75 | | eqid 2177 |
. . . . . . . . . . 11
                   
                     |
76 | 72, 74, 75 | ovmpog 6002 |
. . . . . . . . . 10
             
            
                              
        
                                      |
77 | 50, 53, 68, 76 | syl3anc 1238 |
. . . . . . . . 9
 
      
                                                           |
78 | 48, 77 | eqtrd 2210 |
. . . . . . . 8
 
      
                                                   |
79 | 78, 68 | eqeltrd 2254 |
. . . . . . 7
 
      
                                |
80 | 79 | ralrimiva 2550 |
. . . . . 6
                                         |
81 | | uzid 9518 |
. . . . . . . 8
       |
82 | 2, 81 | syl 14 |
. . . . . . 7
       |
83 | 82, 3 | opelxpd 4655 |
. . . . . 6
                |
84 | 80, 83 | jca 306 |
. . . . 5
                
        
                              |
85 | | frecfcl 6399 |
. . . . 5
                                                      frec      
        
                          |
86 | | ffn 5360 |
. . . . 5
frec               
                        frec                                |
87 | 84, 85, 86 | 3syl 17 |
. . . 4
 frec      
        
                |
88 | | fveq2 5510 |
. . . . . . . 8

          |
89 | | fveq2 5510 |
. . . . . . . 8

frec               
                 frec               
                   |
90 | 88, 89 | eqeq12d 2192 |
. . . . . . 7

     frec                                
    frec      
        
                    |
91 | 90 | imbi2d 230 |
. . . . . 6

      frec      
        
                 
     frec                                     |
92 | | fveq2 5510 |
. . . . . . . 8
           |
93 | | fveq2 5510 |
. . . . . . . 8
 frec      
        
                 frec               
                   |
94 | 92, 93 | eqeq12d 2192 |
. . . . . . 7
      frec               
                     frec      
        
                    |
95 | 94 | imbi2d 230 |
. . . . . 6
  
    frec                                 
     frec               
                     |
96 | | fveq2 5510 |
. . . . . . . 8
       
   |
97 | | fveq2 5510 |
. . . . . . . 8
 frec                                 frec               
                   |
98 | 96, 97 | eqeq12d 2192 |
. . . . . . 7
      frec      
        
                     frec      
        
                    |
99 | 98 | imbi2d 230 |
. . . . . 6
       frec                                 
     frec      
        
                     |
100 | | fveq2 5510 |
. . . . . . . 8
           |
101 | | fveq2 5510 |
. . . . . . . 8
 frec      
        
                 frec               
                   |
102 | 100, 101 | eqeq12d 2192 |
. . . . . . 7
      frec               
                     frec      
        
                    |
103 | 102 | imbi2d 230 |
. . . . . 6
  
    frec                                 
     frec               
                     |
104 | 41 | fveq1i 5511 |
. . . . . . . 8
    frec      
                                      |
105 | | frec0g 6391 |
. . . . . . . . 9
  
           frec      
                                              |
106 | 83, 105 | syl 14 |
. . . . . . . 8
 frec                  
                                  |
107 | 104, 106 | eqtrid 2222 |
. . . . . . 7
              |
108 | | frec0g 6391 |
. . . . . . . 8
  
           frec      
        
                          |
109 | 83, 108 | syl 14 |
. . . . . . 7
 frec                                          |
110 | 107, 109 | eqtr4d 2213 |
. . . . . 6
     frec                                   |
111 | 42 | ad2antlr 489 |
. . . . . . . . . . . 12
        frec                                              |
112 | | simpll 527 |
. . . . . . . . . . . 12
        frec                                    |
113 | 111, 112 | ffvelcdmd 5647 |
. . . . . . . . . . 11
        frec                                              |
114 | | xp1st 6159 |
. . . . . . . . . . 11
          
              |
115 | 113, 114 | syl 14 |
. . . . . . . . . 10
        frec                                                |
116 | | xp2nd 6160 |
. . . . . . . . . . . 12
          
          |
117 | 113, 116 | syl 14 |
. . . . . . . . . . 11
        frec                                            |
118 | 117 | elexd 2750 |
. . . . . . . . . 10
        frec                                            |
119 | | peano2uz 9559 |
. . . . . . . . . . . 12
            
                |
120 | 115, 119 | syl 14 |
. . . . . . . . . . 11
        frec                                                  |
121 | 14 | ad2antlr 489 |
. . . . . . . . . . . 12
        frec                                  

    |
122 | | fveq2 5510 |
. . . . . . . . . . . . . . 15
          
                    |
123 | 122 | eleq1d 2246 |
. . . . . . . . . . . . . 14
          
    
                 |
124 | 29 | ad2antlr 489 |
. . . . . . . . . . . . . 14
        frec                                                |
125 | | eluzp1p1 9529 |
. . . . . . . . . . . . . . 15
            
                  |
126 | 115, 125 | syl 14 |
. . . . . . . . . . . . . 14
        frec                                               
    |
127 | 123, 124,
126 | rspcdva 2846 |
. . . . . . . . . . . . 13
        frec                                                  |
128 | | oveq12 5877 |
. . . . . . . . . . . . . . 15
                         
                           |
129 | 128 | eleq1d 2246 |
. . . . . . . . . . . . . 14
                           
                           |
130 | 129 | rspc2gv 2853 |
. . . . . . . . . . . . 13
                                      
                  |
131 | 117, 127,
130 | syl2anc 411 |
. . . . . . . . . . . 12
        frec                                   


         
                  |
132 | 121, 131 | mpd 13 |
. . . . . . . . . . 11
        frec                                          
                 |
133 | 120, 132 | opelxpd 4655 |
. . . . . . . . . 10
        frec                                                                               |
134 | | oveq1 5875 |
. . . . . . . . . . . 12
        
              |
135 | | fvoveq1 5891 |
. . . . . . . . . . . . 13
        
                      |
136 | 135 | oveq2d 5884 |
. . . . . . . . . . . 12
        
                          |
137 | 134, 136 | opeq12d 3784 |
. . . . . . . . . . 11
        
            
                               |
138 | | oveq1 5875 |
. . . . . . . . . . . 12
        
                        
                 |
139 | 138 | opeq2d 3783 |
. . . . . . . . . . 11
        
                            
                    
                  |
140 | 137, 139,
75 | ovmpog 6002 |
. . . . . . . . . 10
                     
                    
                                      
        
                                                      |
141 | 115, 118,
133, 140 | syl3anc 1238 |
. . . . . . . . 9
        frec                                                 
        
                                                      |
142 | 80 | ad2antlr 489 |
. . . . . . . . . . 11
        frec                                                
        
                |
143 | 83 | ad2antlr 489 |
. . . . . . . . . . 11
        frec                                                 |
144 | | frecsuc 6401 |
. . . . . . . . . . 11
                                                      frec      
        
                                
       frec               
                    |
145 | 142, 143,
112, 144 | syl3anc 1238 |
. . . . . . . . . 10
        frec                                  frec      
        
                                
       frec               
                    |
146 | | simpr 110 |
. . . . . . . . . . 11
        frec                                      frec                                   |
147 | 146 | fveq2d 5514 |
. . . . . . . . . 10
        frec                                                 
                  
        
       frec               
                    |
148 | | 1st2nd2 6169 |
. . . . . . . . . . . . 13
          
                         |
149 | 113, 148 | syl 14 |
. . . . . . . . . . . 12
        frec                                                           |
150 | 149 | fveq2d 5514 |
. . . . . . . . . . 11
        frec                                                 
                  
        
                             |
151 | | df-ov 5871 |
. . . . . . . . . . 11
                        
                              
                            |
152 | 150, 151 | eqtr4di 2228 |
. . . . . . . . . 10
        frec                                                 
                           
        
                 |
153 | 145, 147,
152 | 3eqtr2d 2216 |
. . . . . . . . 9
        frec                                  frec      
        
                                
        
                 |
154 | 45 | fveq2d 5514 |
. . . . . . . . . . . . . . . . . . 19
 
      
                  
                                                                |
155 | | df-ov 5871 |
. . . . . . . . . . . . . . . . . . 19
                                                                                          |
156 | 154, 155 | eqtr4di 2228 |
. . . . . . . . . . . . . . . . . 18
 
      
                  
                           
                                 |
157 | | fvoveq1 5891 |
. . . . . . . . . . . . . . . . . . . . . . . 24
    
                  |
158 | 157 | oveq2d 5884 |
. . . . . . . . . . . . . . . . . . . . . . 23
    
                      |
159 | | oveq1 5875 |
. . . . . . . . . . . . . . . . . . . . . . 23
    
                
             |
160 | | eqid 2177 |
. . . . . . . . . . . . . . . . . . . . . . 23
                    
          |
161 | 158, 159,
160 | ovmpog 6002 |
. . . . . . . . . . . . . . . . . . . . . 22
                              
           
                   
             |
162 | 50, 52, 67, 161 | syl3anc 1238 |
. . . . . . . . . . . . . . . . . . . . 21
 
      
           
                   
             |
163 | 162, 67 | eqeltrd 2254 |
. . . . . . . . . . . . . . . . . . . 20
 
      
           
                 |
164 | 55, 163 | opelxpd 4655 |
. . . . . . . . . . . . . . . . . . 19
 
      
                   
                        |
165 | | oveq1 5875 |
. . . . . . . . . . . . . . . . . . . . 21
    
                              
             |
166 | 69, 165 | opeq12d 3784 |
. . . . . . . . . . . . . . . . . . . 20
    
                       
                   
              |
167 | | oveq2 5876 |
. . . . . . . . . . . . . . . . . . . . 21
    
           
                      
                 |
168 | 167 | opeq2d 3783 |
. . . . . . . . . . . . . . . . . . . 20
    
                   
           
                   
                  |
169 | | eqid 2177 |
. . . . . . . . . . . . . . . . . . . 20
                 
            
                 
              |
170 | 166, 168,
169 | ovmpog 6002 |
. . . . . . . . . . . . . . . . . . 19
             
                   
                      
                       
                                                         |
171 | 50, 53, 164, 170 | syl3anc 1238 |
. . . . . . . . . . . . . . . . . 18
 
      
                       
                                                         |
172 | 156, 171 | eqtrd 2210 |
. . . . . . . . . . . . . . . . 17
 
      
                  
                                                      |
173 | 172, 164 | eqeltrd 2254 |
. . . . . . . . . . . . . . . 16
 
      
                  
                        |
174 | 173 | ralrimiva 2550 |
. . . . . . . . . . . . . . 15
                           
                        |
175 | 174 | ad2antlr 489 |
. . . . . . . . . . . . . 14
        frec                                                
                                    |
176 | | frecsuc 6401 |
. . . . . . . . . . . . . 14
                            
                                    frec      
                                                                       frec                                               |
177 | 175, 143,
112, 176 | syl3anc 1238 |
. . . . . . . . . . . . 13
        frec                                  frec      
                                                                       frec                                               |
178 | 41 | fveq1i 5511 |
. . . . . . . . . . . . 13
  
 frec                  
                          |
179 | 41 | fveq1i 5511 |
. . . . . . . . . . . . . 14
    frec                  
                          |
180 | 179 | fveq2i 5513 |
. . . . . . . . . . . . 13
                  
                                                      frec                                              |
181 | 177, 178,
180 | 3eqtr4g 2235 |
. . . . . . . . . . . 12
        frec                                                        
                      |
182 | 149 | fveq2d 5514 |
. . . . . . . . . . . 12
        frec                                                                               
                                                 |
183 | 181, 182 | eqtrd 2210 |
. . . . . . . . . . 11
        frec                                                        
                                     |
184 | | df-ov 5871 |
. . . . . . . . . . 11
                                                                                                          |
185 | 183, 184 | eqtr4di 2228 |
. . . . . . . . . 10
        frec                                                                 
                         |
186 | | fvoveq1 5891 |
. . . . . . . . . . . . . . . 16
        
                      |
187 | 186 | oveq2d 5884 |
. . . . . . . . . . . . . . 15
        
                          |
188 | | oveq1 5875 |
. . . . . . . . . . . . . . 15
        
                        
                 |
189 | 187, 188,
160 | ovmpog 6002 |
. . . . . . . . . . . . . 14
                                              
               
                           
                 |
190 | 115, 117,
132, 189 | syl3anc 1238 |
. . . . . . . . . . . . 13
        frec                                                 
                           
                 |
191 | 190, 132 | eqeltrd 2254 |
. . . . . . . . . . . 12
        frec                                                 
                     |
192 | 120, 191 | opelxpd 4655 |
. . . . . . . . . . 11
        frec                                                                                          |
193 | | oveq1 5875 |
. . . . . . . . . . . . 13
        
                                  
             |
194 | 134, 193 | opeq12d 3784 |
. . . . . . . . . . . 12
        
                       
                           
              |
195 | | oveq2 5876 |
. . . . . . . . . . . . 13
        
               
                          
                     |
196 | 195 | opeq2d 3783 |
. . . . . . . . . . . 12
        
                           
           
                           
                      |
197 | 194, 196,
169 | ovmpog 6002 |
. . . . . . . . . . 11
                     
                           
                          
                           
                                                                         |
198 | 115, 118,
192, 197 | syl3anc 1238 |
. . . . . . . . . 10
        frec                                                 
                                                                                     |
199 | 190 | opeq2d 3783 |
. . . . . . . . . 10
        frec                                                                                                                         |
200 | 185, 198,
199 | 3eqtrd 2214 |
. . . . . . . . 9
        frec                                                                             |
201 | 141, 153,
200 | 3eqtr4rd 2221 |
. . . . . . . 8
        frec                                      frec                                   |
202 | 201 | exp31 364 |
. . . . . . 7
       frec                                
    frec                                     |
203 | 202 | a2d 26 |
. . . . . 6
  
    frec                                       frec      
        
                     |
204 | 91, 95, 99, 103, 110, 203 | finds 4595 |
. . . . 5
      frec      
        
                    |
205 | 204 | impcom 125 |
. . . 4
 

    frec      
        
                   |
206 | 43, 87, 205 | eqfnfvd 5611 |
. . 3
 frec         |