Step | Hyp | Ref
| Expression |
1 | | seqvalcd.m |
. . . . . 6
   |
2 | | seqvalcd.f0 |
. . . . . 6
       |
3 | | ssv 3085 |
. . . . . . 7
 |
4 | 3 | a1i 9 |
. . . . . 6

  |
5 | | eqidd 2116 |
. . . . . . . 8
 
    
       
              
           |
6 | | simprr 504 |
. . . . . . . . 9
               |
7 | | simprl 503 |
. . . . . . . . . 10
               |
8 | 7 | fvoveq1d 5750 |
. . . . . . . . 9
                      
    |
9 | 6, 8 | oveq12d 5746 |
. . . . . . . 8
             
                 |
10 | | simprl 503 |
. . . . . . . 8
 
    
        |
11 | | simprr 504 |
. . . . . . . 8
 
    
    |
12 | | seqvalcd.pl |
. . . . . . . . . . . 12
 

      |
13 | 12 | ralrimivva 2488 |
. . . . . . . . . . 11
  

   |
14 | | oveq1 5735 |
. . . . . . . . . . . . 13
 
     |
15 | 14 | eleq1d 2183 |
. . . . . . . . . . . 12
   
     |
16 | | oveq2 5736 |
. . . . . . . . . . . . 13
 
     |
17 | 16 | eleq1d 2183 |
. . . . . . . . . . . 12
   
     |
18 | 15, 17 | cbvral2v 2636 |
. . . . . . . . . . 11
 



 
    |
19 | 13, 18 | sylib 121 |
. . . . . . . . . 10
  
    |
20 | 19 | adantr 272 |
. . . . . . . . 9
 
    
  

    |
21 | | fveq2 5375 |
. . . . . . . . . . . 12
          
    |
22 | 21 | eleq1d 2183 |
. . . . . . . . . . 11
       
         |
23 | | seqvalcd.fp1 |
. . . . . . . . . . . . . 14
 
      
      |
24 | 23 | ralrimiva 2479 |
. . . . . . . . . . . . 13
               |
25 | | fveq2 5375 |
. . . . . . . . . . . . . . 15
           |
26 | 25 | eleq1d 2183 |
. . . . . . . . . . . . . 14
     
       |
27 | 26 | cbvralv 2628 |
. . . . . . . . . . . . 13
 
   
                     |
28 | 24, 27 | sylib 121 |
. . . . . . . . . . . 12
               |
29 | 28 | adantr 272 |
. . . . . . . . . . 11
 
    
                |
30 | | eluzp1p1 9253 |
. . . . . . . . . . . 12
    
          |
31 | 10, 30 | syl 14 |
. . . . . . . . . . 11
 
    
       
    |
32 | 22, 29, 31 | rspcdva 2765 |
. . . . . . . . . 10
 
    
          |
33 | | oveq12 5737 |
. . . . . . . . . . . 12
 
             
     |
34 | 33 | eleq1d 2183 |
. . . . . . . . . . 11
 
                     |
35 | 34 | rspc2gv 2771 |
. . . . . . . . . 10
                         |
36 | 11, 32, 35 | syl2anc 406 |
. . . . . . . . 9
 
    
   

             |
37 | 20, 36 | mpd 13 |
. . . . . . . 8
 
    
  
         |
38 | 5, 9, 10, 11, 37 | ovmpod 5852 |
. . . . . . 7
 
    
         
                     |
39 | 38, 37 | eqeltrd 2191 |
. . . . . 6
 
    
         
             |
40 | | seqvalcd.r |
. . . . . 6
frec      
                                   |
41 | 1, 2, 4, 39, 40 | frecuzrdgrclt 10081 |
. . . . 5
             |
42 | 41 | ffnd 5231 |
. . . 4
   |
43 | | 1st2nd2 6027 |
. . . . . . . . . . . 12
      
             |
44 | 43 | adantl 273 |
. . . . . . . . . . 11
 
      
             |
45 | 44 | fveq2d 5379 |
. . . . . . . . . 10
 
      
                                                             |
46 | | df-ov 5731 |
. . . . . . . . . 10
                    
                          
                    |
47 | 45, 46 | syl6eqr 2165 |
. . . . . . . . 9
 
      
                                            
             |
48 | | xp1st 6017 |
. . . . . . . . . . 11
      
          |
49 | 48 | adantl 273 |
. . . . . . . . . 10
 
      
          |
50 | | xp2nd 6018 |
. . . . . . . . . . . 12
      
      |
51 | 50 | adantl 273 |
. . . . . . . . . . 11
 
      
      |
52 | 51 | elexd 2670 |
. . . . . . . . . 10
 
      
      |
53 | | peano2uz 9280 |
. . . . . . . . . . . 12
        
            |
54 | 49, 53 | syl 14 |
. . . . . . . . . . 11
 
      
            |
55 | 13 | adantr 272 |
. . . . . . . . . . . 12
 
      


    |
56 | | fveq2 5375 |
. . . . . . . . . . . . . . 15
      
                |
57 | 56 | eleq1d 2183 |
. . . . . . . . . . . . . 14
      
    
             |
58 | 24 | adantr 272 |
. . . . . . . . . . . . . 14
 
      
              |
59 | | eluzp1p1 9253 |
. . . . . . . . . . . . . . 15
        
              |
60 | 49, 59 | syl 14 |
. . . . . . . . . . . . . 14
 
      
              |
61 | 57, 58, 60 | rspcdva 2765 |
. . . . . . . . . . . . 13
 
      
            |
62 | | oveq12 5737 |
. . . . . . . . . . . . . . 15
                 
                   |
63 | 62 | eleq1d 2183 |
. . . . . . . . . . . . . 14
                   
                   |
64 | 63 | rspc2gv 2771 |
. . . . . . . . . . . . 13
                          
              |
65 | 51, 61, 64 | syl2anc 406 |
. . . . . . . . . . . 12
 
      
 



                   |
66 | 55, 65 | mpd 13 |
. . . . . . . . . . 11
 
      
                  |
67 | 54, 66 | opelxpd 4532 |
. . . . . . . . . 10
 
      
            
                    |
68 | | oveq1 5735 |
. . . . . . . . . . . 12
    
          |
69 | | fvoveq1 5751 |
. . . . . . . . . . . . 13
    
                  |
70 | 69 | oveq2d 5744 |
. . . . . . . . . . . 12
    
                      |
71 | 68, 70 | opeq12d 3679 |
. . . . . . . . . . 11
    
            
                       |
72 | | oveq1 5735 |
. . . . . . . . . . . 12
    
                
             |
73 | 72 | opeq2d 3678 |
. . . . . . . . . . 11
    
                    
            
              |
74 | | eqid 2115 |
. . . . . . . . . . 11
                   
                     |
75 | 71, 73, 74 | ovmpog 5859 |
. . . . . . . . . 10
             
            
                              
        
                                      |
76 | 49, 52, 67, 75 | syl3anc 1199 |
. . . . . . . . 9
 
      
                                                           |
77 | 47, 76 | eqtrd 2147 |
. . . . . . . 8
 
      
                                                   |
78 | 77, 67 | eqeltrd 2191 |
. . . . . . 7
 
      
                                |
79 | 78 | ralrimiva 2479 |
. . . . . 6
                                         |
80 | | uzid 9242 |
. . . . . . . 8
       |
81 | 1, 80 | syl 14 |
. . . . . . 7
       |
82 | 81, 2 | opelxpd 4532 |
. . . . . 6
                |
83 | 79, 82 | jca 302 |
. . . . 5
                
        
                              |
84 | | frecfcl 6256 |
. . . . 5
                                                      frec      
        
                          |
85 | | ffn 5230 |
. . . . 5
frec               
                        frec                                |
86 | 83, 84, 85 | 3syl 17 |
. . . 4
 frec      
        
                |
87 | | fveq2 5375 |
. . . . . . . 8

          |
88 | | fveq2 5375 |
. . . . . . . 8

frec               
                 frec               
                   |
89 | 87, 88 | eqeq12d 2129 |
. . . . . . 7

     frec                                
    frec      
        
                    |
90 | 89 | imbi2d 229 |
. . . . . 6

      frec      
        
                 
     frec                                     |
91 | | fveq2 5375 |
. . . . . . . 8
           |
92 | | fveq2 5375 |
. . . . . . . 8
 frec      
        
                 frec               
                   |
93 | 91, 92 | eqeq12d 2129 |
. . . . . . 7
      frec               
                     frec      
        
                    |
94 | 93 | imbi2d 229 |
. . . . . 6
  
    frec                                 
     frec               
                     |
95 | | fveq2 5375 |
. . . . . . . 8
       
   |
96 | | fveq2 5375 |
. . . . . . . 8
 frec                                 frec               
                   |
97 | 95, 96 | eqeq12d 2129 |
. . . . . . 7
      frec      
        
                     frec      
        
                    |
98 | 97 | imbi2d 229 |
. . . . . 6
       frec                                 
     frec      
        
                     |
99 | | fveq2 5375 |
. . . . . . . 8
           |
100 | | fveq2 5375 |
. . . . . . . 8
 frec      
        
                 frec               
                   |
101 | 99, 100 | eqeq12d 2129 |
. . . . . . 7
      frec               
                     frec      
        
                    |
102 | 101 | imbi2d 229 |
. . . . . 6
  
    frec                                 
     frec               
                     |
103 | 40 | fveq1i 5376 |
. . . . . . . 8
    frec      
                                      |
104 | | frec0g 6248 |
. . . . . . . . 9
  
           frec      
                                              |
105 | 82, 104 | syl 14 |
. . . . . . . 8
 frec                  
                                  |
106 | 103, 105 | syl5eq 2159 |
. . . . . . 7
              |
107 | | frec0g 6248 |
. . . . . . . 8
  
           frec      
        
                          |
108 | 82, 107 | syl 14 |
. . . . . . 7
 frec                                          |
109 | 106, 108 | eqtr4d 2150 |
. . . . . 6
     frec                                   |
110 | 41 | ad2antlr 478 |
. . . . . . . . . . . 12
        frec                                              |
111 | | simpll 501 |
. . . . . . . . . . . 12
        frec                                    |
112 | 110, 111 | ffvelrnd 5510 |
. . . . . . . . . . 11
        frec                                              |
113 | | xp1st 6017 |
. . . . . . . . . . 11
          
              |
114 | 112, 113 | syl 14 |
. . . . . . . . . 10
        frec                                                |
115 | | xp2nd 6018 |
. . . . . . . . . . . 12
          
          |
116 | 112, 115 | syl 14 |
. . . . . . . . . . 11
        frec                                            |
117 | 116 | elexd 2670 |
. . . . . . . . . 10
        frec                                            |
118 | | peano2uz 9280 |
. . . . . . . . . . . 12
            
                |
119 | 114, 118 | syl 14 |
. . . . . . . . . . 11
        frec                                                  |
120 | 13 | ad2antlr 478 |
. . . . . . . . . . . 12
        frec                                  

    |
121 | | fveq2 5375 |
. . . . . . . . . . . . . . 15
          
                    |
122 | 121 | eleq1d 2183 |
. . . . . . . . . . . . . 14
          
    
                 |
123 | 28 | ad2antlr 478 |
. . . . . . . . . . . . . 14
        frec                                                |
124 | | eluzp1p1 9253 |
. . . . . . . . . . . . . . 15
            
                  |
125 | 114, 124 | syl 14 |
. . . . . . . . . . . . . 14
        frec                                               
    |
126 | 122, 123,
125 | rspcdva 2765 |
. . . . . . . . . . . . 13
        frec                                                  |
127 | | oveq12 5737 |
. . . . . . . . . . . . . . 15
                         
                           |
128 | 127 | eleq1d 2183 |
. . . . . . . . . . . . . 14
                           
                           |
129 | 128 | rspc2gv 2771 |
. . . . . . . . . . . . 13
                                      
                  |
130 | 116, 126,
129 | syl2anc 406 |
. . . . . . . . . . . 12
        frec                                   


         
                  |
131 | 120, 130 | mpd 13 |
. . . . . . . . . . 11
        frec                                          
                 |
132 | 119, 131 | opelxpd 4532 |
. . . . . . . . . 10
        frec                                                                               |
133 | | oveq1 5735 |
. . . . . . . . . . . 12
        
              |
134 | | fvoveq1 5751 |
. . . . . . . . . . . . 13
        
                      |
135 | 134 | oveq2d 5744 |
. . . . . . . . . . . 12
        
                          |
136 | 133, 135 | opeq12d 3679 |
. . . . . . . . . . 11
        
            
                               |
137 | | oveq1 5735 |
. . . . . . . . . . . 12
        
                        
                 |
138 | 137 | opeq2d 3678 |
. . . . . . . . . . 11
        
                            
                    
                  |
139 | 136, 138,
74 | ovmpog 5859 |
. . . . . . . . . 10
                     
                    
                                      
        
                                                      |
140 | 114, 117,
132, 139 | syl3anc 1199 |
. . . . . . . . 9
        frec                                                 
        
                                                      |
141 | 79 | ad2antlr 478 |
. . . . . . . . . . 11
        frec                                                
        
                |
142 | 82 | ad2antlr 478 |
. . . . . . . . . . 11
        frec                                                 |
143 | | frecsuc 6258 |
. . . . . . . . . . 11
                                                      frec      
        
                                
       frec               
                    |
144 | 141, 142,
111, 143 | syl3anc 1199 |
. . . . . . . . . 10
        frec                                  frec      
        
                                
       frec               
                    |
145 | | simpr 109 |
. . . . . . . . . . 11
        frec                                      frec                                   |
146 | 145 | fveq2d 5379 |
. . . . . . . . . 10
        frec                                                 
                  
        
       frec               
                    |
147 | | 1st2nd2 6027 |
. . . . . . . . . . . . 13
          
                         |
148 | 112, 147 | syl 14 |
. . . . . . . . . . . 12
        frec                                                           |
149 | 148 | fveq2d 5379 |
. . . . . . . . . . 11
        frec                                                 
                  
        
                             |
150 | | df-ov 5731 |
. . . . . . . . . . 11
                        
                              
                            |
151 | 149, 150 | syl6eqr 2165 |
. . . . . . . . . 10
        frec                                                 
                           
        
                 |
152 | 144, 146,
151 | 3eqtr2d 2153 |
. . . . . . . . 9
        frec                                  frec      
        
                                
        
                 |
153 | 44 | fveq2d 5379 |
. . . . . . . . . . . . . . . . . . 19
 
      
                  
                                                                |
154 | | df-ov 5731 |
. . . . . . . . . . . . . . . . . . 19
                                                                                          |
155 | 153, 154 | syl6eqr 2165 |
. . . . . . . . . . . . . . . . . 18
 
      
                  
                           
                                 |
156 | | fvoveq1 5751 |
. . . . . . . . . . . . . . . . . . . . . . . 24
    
                  |
157 | 156 | oveq2d 5744 |
. . . . . . . . . . . . . . . . . . . . . . 23
    
                      |
158 | | oveq1 5735 |
. . . . . . . . . . . . . . . . . . . . . . 23
    
                
             |
159 | | eqid 2115 |
. . . . . . . . . . . . . . . . . . . . . . 23
                    
          |
160 | 157, 158,
159 | ovmpog 5859 |
. . . . . . . . . . . . . . . . . . . . . 22
                              
           
                   
             |
161 | 49, 51, 66, 160 | syl3anc 1199 |
. . . . . . . . . . . . . . . . . . . . 21
 
      
           
                   
             |
162 | 161, 66 | eqeltrd 2191 |
. . . . . . . . . . . . . . . . . . . 20
 
      
           
                 |
163 | 54, 162 | opelxpd 4532 |
. . . . . . . . . . . . . . . . . . 19
 
      
                   
                        |
164 | | oveq1 5735 |
. . . . . . . . . . . . . . . . . . . . 21
    
                              
             |
165 | 68, 164 | opeq12d 3679 |
. . . . . . . . . . . . . . . . . . . 20
    
                       
                   
              |
166 | | oveq2 5736 |
. . . . . . . . . . . . . . . . . . . . 21
    
           
                      
                 |
167 | 166 | opeq2d 3678 |
. . . . . . . . . . . . . . . . . . . 20
    
                   
           
                   
                  |
168 | | eqid 2115 |
. . . . . . . . . . . . . . . . . . . 20
                 
            
                 
              |
169 | 165, 167,
168 | ovmpog 5859 |
. . . . . . . . . . . . . . . . . . 19
             
                   
                      
                       
                                                         |
170 | 49, 52, 163, 169 | syl3anc 1199 |
. . . . . . . . . . . . . . . . . 18
 
      
                       
                                                         |
171 | 155, 170 | eqtrd 2147 |
. . . . . . . . . . . . . . . . 17
 
      
                  
                                                      |
172 | 171, 163 | eqeltrd 2191 |
. . . . . . . . . . . . . . . 16
 
      
                  
                        |
173 | 172 | ralrimiva 2479 |
. . . . . . . . . . . . . . 15
                           
                        |
174 | 173 | ad2antlr 478 |
. . . . . . . . . . . . . 14
        frec                                                
                                    |
175 | | frecsuc 6258 |
. . . . . . . . . . . . . 14
                            
                                    frec      
                                                                       frec                                               |
176 | 174, 142,
111, 175 | syl3anc 1199 |
. . . . . . . . . . . . 13
        frec                                  frec      
                                                                       frec                                               |
177 | 40 | fveq1i 5376 |
. . . . . . . . . . . . 13
  
 frec                  
                          |
178 | 40 | fveq1i 5376 |
. . . . . . . . . . . . . 14
    frec                  
                          |
179 | 178 | fveq2i 5378 |
. . . . . . . . . . . . 13
                  
                                                      frec                                              |
180 | 176, 177,
179 | 3eqtr4g 2172 |
. . . . . . . . . . . 12
        frec                                                        
                      |
181 | 148 | fveq2d 5379 |
. . . . . . . . . . . 12
        frec                                                                               
                                                 |
182 | 180, 181 | eqtrd 2147 |
. . . . . . . . . . 11
        frec                                                        
                                     |
183 | | df-ov 5731 |
. . . . . . . . . . 11
                                                                                                          |
184 | 182, 183 | syl6eqr 2165 |
. . . . . . . . . 10
        frec                                                                 
                         |
185 | | fvoveq1 5751 |
. . . . . . . . . . . . . . . 16
        
                      |
186 | 185 | oveq2d 5744 |
. . . . . . . . . . . . . . 15
        
                          |
187 | | oveq1 5735 |
. . . . . . . . . . . . . . 15
        
                        
                 |
188 | 186, 187,
159 | ovmpog 5859 |
. . . . . . . . . . . . . 14
                                              
               
                           
                 |
189 | 114, 116,
131, 188 | syl3anc 1199 |
. . . . . . . . . . . . 13
        frec                                                 
                           
                 |
190 | 189, 131 | eqeltrd 2191 |
. . . . . . . . . . . 12
        frec                                                 
                     |
191 | 119, 190 | opelxpd 4532 |
. . . . . . . . . . 11
        frec                                                                                          |
192 | | oveq1 5735 |
. . . . . . . . . . . . 13
        
                                  
             |
193 | 133, 192 | opeq12d 3679 |
. . . . . . . . . . . 12
        
                       
                           
              |
194 | | oveq2 5736 |
. . . . . . . . . . . . 13
        
               
                          
                     |
195 | 194 | opeq2d 3678 |
. . . . . . . . . . . 12
        
                           
           
                           
                      |
196 | 193, 195,
168 | ovmpog 5859 |
. . . . . . . . . . 11
                     
                           
                          
                           
                                                                         |
197 | 114, 117,
191, 196 | syl3anc 1199 |
. . . . . . . . . 10
        frec                                                 
                                                                                     |
198 | 189 | opeq2d 3678 |
. . . . . . . . . 10
        frec                                                                                                                         |
199 | 184, 197,
198 | 3eqtrd 2151 |
. . . . . . . . 9
        frec                                                                             |
200 | 140, 152,
199 | 3eqtr4rd 2158 |
. . . . . . . 8
        frec                                      frec                                   |
201 | 200 | exp31 359 |
. . . . . . 7
       frec                                
    frec                                     |
202 | 201 | a2d 26 |
. . . . . 6
  
    frec                                       frec      
        
                     |
203 | 90, 94, 98, 102, 109, 202 | finds 4474 |
. . . . 5
      frec      
        
                    |
204 | 203 | impcom 124 |
. . . 4
 

    frec      
        
                   |
205 | 42, 86, 204 | eqfnfvd 5475 |
. . 3
 frec                                |
206 | 205 | rneqd 4728 |
. 2
 frec          |