Step | Hyp | Ref
| Expression |
1 | | seq3val.m |
. . . . . 6
   |
2 | | fveq2 5375 |
. . . . . . . 8
           |
3 | 2 | eleq1d 2183 |
. . . . . . 7
     
       |
4 | | seq3val.f |
. . . . . . . 8
 
    
      |
5 | 4 | ralrimiva 2479 |
. . . . . . 7
             |
6 | | uzid 9242 |
. . . . . . . 8
       |
7 | 1, 6 | syl 14 |
. . . . . . 7
       |
8 | 3, 5, 7 | rspcdva 2765 |
. . . . . 6
       |
9 | | ssv 3085 |
. . . . . . 7
 |
10 | 9 | a1i 9 |
. . . . . 6

  |
11 | | seq3val.pl |
. . . . . . 7
 

      |
12 | 4, 11 | iseqovex 10122 |
. . . . . 6
 
    
         
             |
13 | | seq3val.r |
. . . . . 6
frec      
                                   |
14 | 1, 8, 10, 12, 13 | frecuzrdgrclt 10081 |
. . . . 5
             |
15 | | ffn 5230 |
. . . . 5
             |
16 | 14, 15 | syl 14 |
. . . 4
   |
17 | | 1st2nd2 6027 |
. . . . . . . . . . . 12
      
             |
18 | 17 | adantl 273 |
. . . . . . . . . . 11
 
      
             |
19 | 18 | fveq2d 5379 |
. . . . . . . . . 10
 
      
                                                             |
20 | | df-ov 5731 |
. . . . . . . . . 10
                    
                          
                    |
21 | 19, 20 | syl6eqr 2165 |
. . . . . . . . 9
 
      
                                            
             |
22 | | xp1st 6017 |
. . . . . . . . . . 11
      
          |
23 | 22 | adantl 273 |
. . . . . . . . . 10
 
      
          |
24 | | xp2nd 6018 |
. . . . . . . . . . . 12
      
      |
25 | 24 | adantl 273 |
. . . . . . . . . . 11
 
      
      |
26 | 25 | elexd 2670 |
. . . . . . . . . 10
 
      
      |
27 | | peano2uz 9280 |
. . . . . . . . . . . 12
        
            |
28 | 23, 27 | syl 14 |
. . . . . . . . . . 11
 
      
            |
29 | 11 | caovclg 5877 |
. . . . . . . . . . . . 13
 

      |
30 | 29 | adantlr 466 |
. . . . . . . . . . . 12
                 |
31 | | fveq2 5375 |
. . . . . . . . . . . . . 14
      
                |
32 | 31 | eleq1d 2183 |
. . . . . . . . . . . . 13
      
    
             |
33 | 5 | adantr 272 |
. . . . . . . . . . . . 13
 
      
            |
34 | 32, 33, 28 | rspcdva 2765 |
. . . . . . . . . . . 12
 
      
            |
35 | 30, 25, 34 | caovcld 5878 |
. . . . . . . . . . 11
 
      
                  |
36 | | opelxpi 4531 |
. . . . . . . . . . 11
           
                                                  |
37 | 28, 35, 36 | syl2anc 406 |
. . . . . . . . . 10
 
      
            
                    |
38 | | oveq1 5735 |
. . . . . . . . . . . 12
    
          |
39 | | fvoveq1 5751 |
. . . . . . . . . . . . 13
    
                  |
40 | 39 | oveq2d 5744 |
. . . . . . . . . . . 12
    
                      |
41 | 38, 40 | opeq12d 3679 |
. . . . . . . . . . 11
    
            
                       |
42 | | oveq1 5735 |
. . . . . . . . . . . 12
    
                
             |
43 | 42 | opeq2d 3678 |
. . . . . . . . . . 11
    
                    
            
              |
44 | | eqid 2115 |
. . . . . . . . . . 11
                   
                     |
45 | 41, 43, 44 | ovmpog 5859 |
. . . . . . . . . 10
             
            
                              
        
                                      |
46 | 23, 26, 37, 45 | syl3anc 1199 |
. . . . . . . . 9
 
      
                                                           |
47 | 21, 46 | eqtrd 2147 |
. . . . . . . 8
 
      
                                                   |
48 | 47, 37 | eqeltrd 2191 |
. . . . . . 7
 
      
                                |
49 | 48 | ralrimiva 2479 |
. . . . . 6
                                         |
50 | | opelxpi 4531 |
. . . . . . 7
                          |
51 | 7, 8, 50 | syl2anc 406 |
. . . . . 6
                |
52 | 49, 51 | jca 302 |
. . . . 5
                
        
                              |
53 | | frecfcl 6256 |
. . . . 5
                                                      frec      
        
                          |
54 | | ffn 5230 |
. . . . 5
frec               
                        frec                                |
55 | 52, 53, 54 | 3syl 17 |
. . . 4
 frec      
        
                |
56 | | fveq2 5375 |
. . . . . . . 8

          |
57 | | fveq2 5375 |
. . . . . . . 8

frec               
                 frec               
                   |
58 | 56, 57 | eqeq12d 2129 |
. . . . . . 7

     frec                                
    frec      
        
                    |
59 | 58 | imbi2d 229 |
. . . . . 6

      frec      
        
                 
     frec                                     |
60 | | fveq2 5375 |
. . . . . . . 8
           |
61 | | fveq2 5375 |
. . . . . . . 8
 frec      
        
                 frec               
                   |
62 | 60, 61 | eqeq12d 2129 |
. . . . . . 7
      frec               
                     frec      
        
                    |
63 | 62 | imbi2d 229 |
. . . . . 6
  
    frec                                 
     frec               
                     |
64 | | fveq2 5375 |
. . . . . . . 8
       
   |
65 | | fveq2 5375 |
. . . . . . . 8
 frec                                 frec               
                   |
66 | 64, 65 | eqeq12d 2129 |
. . . . . . 7
      frec      
        
                     frec      
        
                    |
67 | 66 | imbi2d 229 |
. . . . . 6
       frec                                 
     frec      
        
                     |
68 | | fveq2 5375 |
. . . . . . . 8
           |
69 | | fveq2 5375 |
. . . . . . . 8
 frec      
        
                 frec               
                   |
70 | 68, 69 | eqeq12d 2129 |
. . . . . . 7
      frec               
                     frec      
        
                    |
71 | 70 | imbi2d 229 |
. . . . . 6
  
    frec                                 
     frec               
                     |
72 | 13 | fveq1i 5376 |
. . . . . . . 8
    frec      
                                      |
73 | | frec0g 6248 |
. . . . . . . . 9
  
           frec      
                                              |
74 | 51, 73 | syl 14 |
. . . . . . . 8
 frec                  
                                  |
75 | 72, 74 | syl5eq 2159 |
. . . . . . 7
              |
76 | | frec0g 6248 |
. . . . . . . 8
  
           frec      
        
                          |
77 | 51, 76 | syl 14 |
. . . . . . 7
 frec                                          |
78 | 75, 77 | eqtr4d 2150 |
. . . . . 6
     frec                                   |
79 | 14 | ad2antlr 478 |
. . . . . . . . . . . 12
        frec                                              |
80 | | simpll 501 |
. . . . . . . . . . . 12
        frec                                    |
81 | 79, 80 | ffvelrnd 5510 |
. . . . . . . . . . 11
        frec                                              |
82 | | xp1st 6017 |
. . . . . . . . . . 11
          
              |
83 | 81, 82 | syl 14 |
. . . . . . . . . 10
        frec                                                |
84 | | xp2nd 6018 |
. . . . . . . . . . . 12
          
          |
85 | 81, 84 | syl 14 |
. . . . . . . . . . 11
        frec                                            |
86 | 85 | elexd 2670 |
. . . . . . . . . 10
        frec                                            |
87 | 29 | adantll 465 |
. . . . . . . . . . . . . . 15
    
 
    |
88 | 87 | adantlr 466 |
. . . . . . . . . . . . . 14
   
     frec                                  
  
   |
89 | | fveq2 5375 |
. . . . . . . . . . . . . . . 16
          
                    |
90 | 89 | eleq1d 2183 |
. . . . . . . . . . . . . . 15
          
    
                 |
91 | | fveq2 5375 |
. . . . . . . . . . . . . . . . . . 19
           |
92 | 91 | eleq1d 2183 |
. . . . . . . . . . . . . . . . . 18
     
       |
93 | 92 | cbvralv 2628 |
. . . . . . . . . . . . . . . . 17
 
                     |
94 | 5, 93 | sylib 121 |
. . . . . . . . . . . . . . . 16
             |
95 | 94 | ad2antlr 478 |
. . . . . . . . . . . . . . 15
        frec                                              |
96 | | peano2uz 9280 |
. . . . . . . . . . . . . . . 16
            
                |
97 | 83, 96 | syl 14 |
. . . . . . . . . . . . . . 15
        frec                                                  |
98 | 90, 95, 97 | rspcdva 2765 |
. . . . . . . . . . . . . 14
        frec                                                  |
99 | 88, 85, 98 | caovcld 5878 |
. . . . . . . . . . . . 13
        frec                                          
                 |
100 | | fvoveq1 5751 |
. . . . . . . . . . . . . . 15
        
                      |
101 | 100 | oveq2d 5744 |
. . . . . . . . . . . . . 14
        
                          |
102 | | oveq1 5735 |
. . . . . . . . . . . . . 14
        
                        
                 |
103 | | eqid 2115 |
. . . . . . . . . . . . . 14
                    
          |
104 | 101, 102,
103 | ovmpog 5859 |
. . . . . . . . . . . . 13
                                              
               
                           
                 |
105 | 83, 85, 99, 104 | syl3anc 1199 |
. . . . . . . . . . . 12
        frec                                                 
                           
                 |
106 | 105 | opeq2d 3678 |
. . . . . . . . . . 11
        frec                                                                                                                         |
107 | 105, 99 | eqeltrd 2191 |
. . . . . . . . . . . 12
        frec                                                 
                     |
108 | | opelxpi 4531 |
. . . . . . . . . . . 12
               
               
                   
                           
                            |
109 | 97, 107, 108 | syl2anc 406 |
. . . . . . . . . . 11
        frec                                                                                          |
110 | 106, 109 | eqeltrrd 2192 |
. . . . . . . . . 10
        frec                                                                               |
111 | | oveq1 5735 |
. . . . . . . . . . . 12
        
              |
112 | | fvoveq1 5751 |
. . . . . . . . . . . . 13
        
                      |
113 | 112 | oveq2d 5744 |
. . . . . . . . . . . 12
        
                          |
114 | 111, 113 | opeq12d 3679 |
. . . . . . . . . . 11
        
            
                               |
115 | | oveq1 5735 |
. . . . . . . . . . . 12
        
                        
                 |
116 | 115 | opeq2d 3678 |
. . . . . . . . . . 11
        
                            
                    
                  |
117 | 114, 116,
44 | ovmpog 5859 |
. . . . . . . . . 10
                     
                    
                                      
        
                                                      |
118 | 83, 86, 110, 117 | syl3anc 1199 |
. . . . . . . . 9
        frec                                                 
        
                                                      |
119 | 49 | ad2antlr 478 |
. . . . . . . . . . . 12
        frec                                                
        
                |
120 | 51 | ad2antlr 478 |
. . . . . . . . . . . 12
        frec                                                 |
121 | | frecsuc 6258 |
. . . . . . . . . . . 12
                                                      frec      
        
                                
       frec               
                    |
122 | 119, 120,
80, 121 | syl3anc 1199 |
. . . . . . . . . . 11
        frec                                  frec      
        
                                
       frec               
                    |
123 | | simpr 109 |
. . . . . . . . . . . 12
        frec                                      frec                                   |
124 | 123 | fveq2d 5379 |
. . . . . . . . . . 11
        frec                                                 
                  
        
       frec               
                    |
125 | 122, 124 | eqtr4d 2150 |
. . . . . . . . . 10
        frec                                  frec      
        
                                
              |
126 | | 1st2nd2 6027 |
. . . . . . . . . . . . 13
          
                         |
127 | 81, 126 | syl 14 |
. . . . . . . . . . . 12
        frec                                                           |
128 | 127 | fveq2d 5379 |
. . . . . . . . . . 11
        frec                                                 
                  
        
                             |
129 | | df-ov 5731 |
. . . . . . . . . . 11
                        
                              
                            |
130 | 128, 129 | syl6eqr 2165 |
. . . . . . . . . 10
        frec                                                 
                           
        
                 |
131 | 125, 130 | eqtrd 2147 |
. . . . . . . . 9
        frec                                  frec      
        
                                
        
                 |
132 | 13 | fveq1i 5376 |
. . . . . . . . . . . . . . 15
  
 frec                  
                          |
133 | 18 | fveq2d 5379 |
. . . . . . . . . . . . . . . . . . . . 21
 
      
                  
                                                                |
134 | | df-ov 5731 |
. . . . . . . . . . . . . . . . . . . . 21
                                                                                          |
135 | 133, 134 | syl6eqr 2165 |
. . . . . . . . . . . . . . . . . . . 20
 
      
                  
                           
                                 |
136 | | fvoveq1 5751 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
    
                  |
137 | 136 | oveq2d 5744 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
    
                      |
138 | | oveq1 5735 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
    
                
             |
139 | 137, 138,
103 | ovmpog 5859 |
. . . . . . . . . . . . . . . . . . . . . . . 24
                              
           
                   
             |
140 | 23, 25, 35, 139 | syl3anc 1199 |
. . . . . . . . . . . . . . . . . . . . . . 23
 
      
           
                   
             |
141 | 140, 35 | eqeltrd 2191 |
. . . . . . . . . . . . . . . . . . . . . 22
 
      
           
                 |
142 | | opelxpi 4531 |
. . . . . . . . . . . . . . . . . . . . . 22
           
           
               
                   
                        |
143 | 28, 141, 142 | syl2anc 406 |
. . . . . . . . . . . . . . . . . . . . 21
 
      
                   
                        |
144 | | oveq1 5735 |
. . . . . . . . . . . . . . . . . . . . . . 23
    
                              
             |
145 | 38, 144 | opeq12d 3679 |
. . . . . . . . . . . . . . . . . . . . . 22
    
                       
                   
              |
146 | | oveq2 5736 |
. . . . . . . . . . . . . . . . . . . . . . 23
    
           
                      
                 |
147 | 146 | opeq2d 3678 |
. . . . . . . . . . . . . . . . . . . . . 22
    
                   
           
                   
                  |
148 | | eqid 2115 |
. . . . . . . . . . . . . . . . . . . . . 22
                 
            
                 
              |
149 | 145, 147,
148 | ovmpog 5859 |
. . . . . . . . . . . . . . . . . . . . 21
             
                   
                      
                       
                                                         |
150 | 23, 26, 143, 149 | syl3anc 1199 |
. . . . . . . . . . . . . . . . . . . 20
 
      
                       
                                                         |
151 | 135, 150 | eqtrd 2147 |
. . . . . . . . . . . . . . . . . . 19
 
      
                  
                                                      |
152 | 151, 143 | eqeltrd 2191 |
. . . . . . . . . . . . . . . . . 18
 
      
                  
                        |
153 | 152 | ralrimiva 2479 |
. . . . . . . . . . . . . . . . 17
                           
                        |
154 | 153 | ad2antlr 478 |
. . . . . . . . . . . . . . . 16
        frec                                                
                                    |
155 | | frecsuc 6258 |
. . . . . . . . . . . . . . . 16
                            
                                    frec      
                                                                       frec                                               |
156 | 154, 120,
80, 155 | syl3anc 1199 |
. . . . . . . . . . . . . . 15
        frec                                  frec      
                                                                       frec                                               |
157 | 132, 156 | syl5eq 2159 |
. . . . . . . . . . . . . 14
        frec                                                        
               frec                                               |
158 | 13 | fveq1i 5376 |
. . . . . . . . . . . . . . 15
    frec                  
                          |
159 | 158 | fveq2i 5378 |
. . . . . . . . . . . . . 14
                  
                                                      frec                                              |
160 | 157, 159 | syl6eqr 2165 |
. . . . . . . . . . . . 13
        frec                                                        
                      |
161 | 127 | fveq2d 5379 |
. . . . . . . . . . . . 13
        frec                                                                               
                                                 |
162 | 160, 161 | eqtrd 2147 |
. . . . . . . . . . . 12
        frec                                                        
                                     |
163 | | df-ov 5731 |
. . . . . . . . . . . 12
                                                                                                          |
164 | 162, 163 | syl6eqr 2165 |
. . . . . . . . . . 11
        frec                                                                 
                         |
165 | | oveq1 5735 |
. . . . . . . . . . . . . 14
        
                                  
             |
166 | 111, 165 | opeq12d 3679 |
. . . . . . . . . . . . 13
        
                       
                           
              |
167 | | oveq2 5736 |
. . . . . . . . . . . . . 14
        
               
                          
                     |
168 | 167 | opeq2d 3678 |
. . . . . . . . . . . . 13
        
                           
           
                           
                      |
169 | 166, 168,
148 | ovmpog 5859 |
. . . . . . . . . . . 12
                     
                           
                          
                           
                                                                         |
170 | 83, 86, 109, 169 | syl3anc 1199 |
. . . . . . . . . . 11
        frec                                                 
                                                                                     |
171 | 164, 170 | eqtrd 2147 |
. . . . . . . . . 10
        frec                                                                                        |
172 | 171, 106 | eqtrd 2147 |
. . . . . . . . 9
        frec                                                                             |
173 | 118, 131,
172 | 3eqtr4rd 2158 |
. . . . . . . 8
        frec                                      frec                                   |
174 | 173 | exp31 359 |
. . . . . . 7
       frec                                
    frec                                     |
175 | 174 | a2d 26 |
. . . . . 6
  
    frec                                       frec      
        
                     |
176 | 59, 63, 67, 71, 78, 175 | finds 4474 |
. . . . 5
      frec      
        
                    |
177 | 176 | impcom 124 |
. . . 4
 

    frec      
        
                   |
178 | 16, 55, 177 | eqfnfvd 5475 |
. . 3
 frec                                |
179 | 178 | rneqd 4728 |
. 2
 frec               
                |
180 | | df-seqfrec 10112 |
. 2
 
 frec               
               |
181 | 179, 180 | syl6reqr 2166 |
1
      |