Step | Hyp | Ref
| Expression |
1 | | df-seqfrec 10419 |
. 2
 
 frec               
               |
2 | | seq3val.m |
. . . . . 6
   |
3 | | fveq2 5510 |
. . . . . . . 8
           |
4 | 3 | eleq1d 2246 |
. . . . . . 7
     
       |
5 | | seq3val.f |
. . . . . . . 8
 
    
      |
6 | 5 | ralrimiva 2550 |
. . . . . . 7
             |
7 | | uzid 9518 |
. . . . . . . 8
       |
8 | 2, 7 | syl 14 |
. . . . . . 7
       |
9 | 4, 6, 8 | rspcdva 2846 |
. . . . . 6
       |
10 | | ssv 3177 |
. . . . . . 7
 |
11 | 10 | a1i 9 |
. . . . . 6

  |
12 | | seq3val.pl |
. . . . . . 7
 

      |
13 | 5, 12 | iseqovex 10429 |
. . . . . 6
 
    
         
             |
14 | | seq3val.r |
. . . . . 6
frec      
                                   |
15 | 2, 9, 11, 13, 14 | frecuzrdgrclt 10388 |
. . . . 5
             |
16 | | ffn 5360 |
. . . . 5
             |
17 | 15, 16 | syl 14 |
. . . 4
   |
18 | | 1st2nd2 6169 |
. . . . . . . . . . . 12
      
             |
19 | 18 | adantl 277 |
. . . . . . . . . . 11
 
      
             |
20 | 19 | fveq2d 5514 |
. . . . . . . . . 10
 
      
                                                             |
21 | | df-ov 5871 |
. . . . . . . . . 10
                    
                          
                    |
22 | 20, 21 | eqtr4di 2228 |
. . . . . . . . 9
 
      
                                            
             |
23 | | xp1st 6159 |
. . . . . . . . . . 11
      
          |
24 | 23 | adantl 277 |
. . . . . . . . . 10
 
      
          |
25 | | xp2nd 6160 |
. . . . . . . . . . . 12
      
      |
26 | 25 | adantl 277 |
. . . . . . . . . . 11
 
      
      |
27 | 26 | elexd 2750 |
. . . . . . . . . 10
 
      
      |
28 | | peano2uz 9559 |
. . . . . . . . . . . 12
        
            |
29 | 24, 28 | syl 14 |
. . . . . . . . . . 11
 
      
            |
30 | 12 | caovclg 6020 |
. . . . . . . . . . . . 13
 

      |
31 | 30 | adantlr 477 |
. . . . . . . . . . . 12
                 |
32 | | fveq2 5510 |
. . . . . . . . . . . . . 14
      
                |
33 | 32 | eleq1d 2246 |
. . . . . . . . . . . . 13
      
    
             |
34 | 6 | adantr 276 |
. . . . . . . . . . . . 13
 
      
            |
35 | 33, 34, 29 | rspcdva 2846 |
. . . . . . . . . . . 12
 
      
            |
36 | 31, 26, 35 | caovcld 6021 |
. . . . . . . . . . 11
 
      
                  |
37 | | opelxpi 4654 |
. . . . . . . . . . 11
           
                                                  |
38 | 29, 36, 37 | syl2anc 411 |
. . . . . . . . . 10
 
      
            
                    |
39 | | oveq1 5875 |
. . . . . . . . . . . 12
    
          |
40 | | fvoveq1 5891 |
. . . . . . . . . . . . 13
    
                  |
41 | 40 | oveq2d 5884 |
. . . . . . . . . . . 12
    
                      |
42 | 39, 41 | opeq12d 3784 |
. . . . . . . . . . 11
    
            
                       |
43 | | oveq1 5875 |
. . . . . . . . . . . 12
    
                
             |
44 | 43 | opeq2d 3783 |
. . . . . . . . . . 11
    
                    
            
              |
45 | | eqid 2177 |
. . . . . . . . . . 11
                   
                     |
46 | 42, 44, 45 | ovmpog 6002 |
. . . . . . . . . 10
             
            
                              
        
                                      |
47 | 24, 27, 38, 46 | syl3anc 1238 |
. . . . . . . . 9
 
      
                                                           |
48 | 22, 47 | eqtrd 2210 |
. . . . . . . 8
 
      
                                                   |
49 | 48, 38 | eqeltrd 2254 |
. . . . . . 7
 
      
                                |
50 | 49 | ralrimiva 2550 |
. . . . . 6
                                         |
51 | | opelxpi 4654 |
. . . . . . 7
                          |
52 | 8, 9, 51 | syl2anc 411 |
. . . . . 6
                |
53 | 50, 52 | jca 306 |
. . . . 5
                
        
                              |
54 | | frecfcl 6399 |
. . . . 5
                                                      frec      
        
                          |
55 | | ffn 5360 |
. . . . 5
frec               
                        frec                                |
56 | 53, 54, 55 | 3syl 17 |
. . . 4
 frec      
        
                |
57 | | fveq2 5510 |
. . . . . . . 8

          |
58 | | fveq2 5510 |
. . . . . . . 8

frec               
                 frec               
                   |
59 | 57, 58 | eqeq12d 2192 |
. . . . . . 7

     frec                                
    frec      
        
                    |
60 | 59 | imbi2d 230 |
. . . . . 6

      frec      
        
                 
     frec                                     |
61 | | fveq2 5510 |
. . . . . . . 8
           |
62 | | fveq2 5510 |
. . . . . . . 8
 frec      
        
                 frec               
                   |
63 | 61, 62 | eqeq12d 2192 |
. . . . . . 7
      frec               
                     frec      
        
                    |
64 | 63 | imbi2d 230 |
. . . . . 6
  
    frec                                 
     frec               
                     |
65 | | fveq2 5510 |
. . . . . . . 8
       
   |
66 | | fveq2 5510 |
. . . . . . . 8
 frec                                 frec               
                   |
67 | 65, 66 | eqeq12d 2192 |
. . . . . . 7
      frec      
        
                     frec      
        
                    |
68 | 67 | imbi2d 230 |
. . . . . 6
       frec                                 
     frec      
        
                     |
69 | | fveq2 5510 |
. . . . . . . 8
           |
70 | | fveq2 5510 |
. . . . . . . 8
 frec      
        
                 frec               
                   |
71 | 69, 70 | eqeq12d 2192 |
. . . . . . 7
      frec               
                     frec      
        
                    |
72 | 71 | imbi2d 230 |
. . . . . 6
  
    frec                                 
     frec               
                     |
73 | 14 | fveq1i 5511 |
. . . . . . . 8
    frec      
                                      |
74 | | frec0g 6391 |
. . . . . . . . 9
  
           frec      
                                              |
75 | 52, 74 | syl 14 |
. . . . . . . 8
 frec                  
                                  |
76 | 73, 75 | eqtrid 2222 |
. . . . . . 7
              |
77 | | frec0g 6391 |
. . . . . . . 8
  
           frec      
        
                          |
78 | 52, 77 | syl 14 |
. . . . . . 7
 frec                                          |
79 | 76, 78 | eqtr4d 2213 |
. . . . . 6
     frec                                   |
80 | 15 | ad2antlr 489 |
. . . . . . . . . . . 12
        frec                                              |
81 | | simpll 527 |
. . . . . . . . . . . 12
        frec                                    |
82 | 80, 81 | ffvelcdmd 5647 |
. . . . . . . . . . 11
        frec                                              |
83 | | xp1st 6159 |
. . . . . . . . . . 11
          
              |
84 | 82, 83 | syl 14 |
. . . . . . . . . 10
        frec                                                |
85 | | xp2nd 6160 |
. . . . . . . . . . . 12
          
          |
86 | 82, 85 | syl 14 |
. . . . . . . . . . 11
        frec                                            |
87 | 86 | elexd 2750 |
. . . . . . . . . 10
        frec                                            |
88 | 30 | adantll 476 |
. . . . . . . . . . . . . . 15
    
 
    |
89 | 88 | adantlr 477 |
. . . . . . . . . . . . . 14
   
     frec                                  
  
   |
90 | | fveq2 5510 |
. . . . . . . . . . . . . . . 16
          
                    |
91 | 90 | eleq1d 2246 |
. . . . . . . . . . . . . . 15
          
    
                 |
92 | | fveq2 5510 |
. . . . . . . . . . . . . . . . . . 19
           |
93 | 92 | eleq1d 2246 |
. . . . . . . . . . . . . . . . . 18
     
       |
94 | 93 | cbvralv 2703 |
. . . . . . . . . . . . . . . . 17
 
                     |
95 | 6, 94 | sylib 122 |
. . . . . . . . . . . . . . . 16
             |
96 | 95 | ad2antlr 489 |
. . . . . . . . . . . . . . 15
        frec                                              |
97 | | peano2uz 9559 |
. . . . . . . . . . . . . . . 16
            
                |
98 | 84, 97 | syl 14 |
. . . . . . . . . . . . . . 15
        frec                                                  |
99 | 91, 96, 98 | rspcdva 2846 |
. . . . . . . . . . . . . 14
        frec                                                  |
100 | 89, 86, 99 | caovcld 6021 |
. . . . . . . . . . . . 13
        frec                                          
                 |
101 | | fvoveq1 5891 |
. . . . . . . . . . . . . . 15
        
                      |
102 | 101 | oveq2d 5884 |
. . . . . . . . . . . . . 14
        
                          |
103 | | oveq1 5875 |
. . . . . . . . . . . . . 14
        
                        
                 |
104 | | eqid 2177 |
. . . . . . . . . . . . . 14
                    
          |
105 | 102, 103,
104 | ovmpog 6002 |
. . . . . . . . . . . . 13
                                              
               
                           
                 |
106 | 84, 86, 100, 105 | syl3anc 1238 |
. . . . . . . . . . . 12
        frec                                                 
                           
                 |
107 | 106 | opeq2d 3783 |
. . . . . . . . . . 11
        frec                                                                                                                         |
108 | 106, 100 | eqeltrd 2254 |
. . . . . . . . . . . 12
        frec                                                 
                     |
109 | | opelxpi 4654 |
. . . . . . . . . . . 12
               
               
                   
                           
                            |
110 | 98, 108, 109 | syl2anc 411 |
. . . . . . . . . . 11
        frec                                                                                          |
111 | 107, 110 | eqeltrrd 2255 |
. . . . . . . . . 10
        frec                                                                               |
112 | | oveq1 5875 |
. . . . . . . . . . . 12
        
              |
113 | | fvoveq1 5891 |
. . . . . . . . . . . . 13
        
                      |
114 | 113 | oveq2d 5884 |
. . . . . . . . . . . 12
        
                          |
115 | 112, 114 | opeq12d 3784 |
. . . . . . . . . . 11
        
            
                               |
116 | | oveq1 5875 |
. . . . . . . . . . . 12
        
                        
                 |
117 | 116 | opeq2d 3783 |
. . . . . . . . . . 11
        
                            
                    
                  |
118 | 115, 117,
45 | ovmpog 6002 |
. . . . . . . . . 10
                     
                    
                                      
        
                                                      |
119 | 84, 87, 111, 118 | syl3anc 1238 |
. . . . . . . . 9
        frec                                                 
        
                                                      |
120 | 50 | ad2antlr 489 |
. . . . . . . . . . . 12
        frec                                                
        
                |
121 | 52 | ad2antlr 489 |
. . . . . . . . . . . 12
        frec                                                 |
122 | | frecsuc 6401 |
. . . . . . . . . . . 12
                                                      frec      
        
                                
       frec               
                    |
123 | 120, 121,
81, 122 | syl3anc 1238 |
. . . . . . . . . . 11
        frec                                  frec      
        
                                
       frec               
                    |
124 | | simpr 110 |
. . . . . . . . . . . 12
        frec                                      frec                                   |
125 | 124 | fveq2d 5514 |
. . . . . . . . . . 11
        frec                                                 
                  
        
       frec               
                    |
126 | 123, 125 | eqtr4d 2213 |
. . . . . . . . . 10
        frec                                  frec      
        
                                
              |
127 | | 1st2nd2 6169 |
. . . . . . . . . . . . 13
          
                         |
128 | 82, 127 | syl 14 |
. . . . . . . . . . . 12
        frec                                                           |
129 | 128 | fveq2d 5514 |
. . . . . . . . . . 11
        frec                                                 
                  
        
                             |
130 | | df-ov 5871 |
. . . . . . . . . . 11
                        
                              
                            |
131 | 129, 130 | eqtr4di 2228 |
. . . . . . . . . 10
        frec                                                 
                           
        
                 |
132 | 126, 131 | eqtrd 2210 |
. . . . . . . . 9
        frec                                  frec      
        
                                
        
                 |
133 | 14 | fveq1i 5511 |
. . . . . . . . . . . . . . 15
  
 frec                  
                          |
134 | 19 | fveq2d 5514 |
. . . . . . . . . . . . . . . . . . . . 21
 
      
                  
                                                                |
135 | | df-ov 5871 |
. . . . . . . . . . . . . . . . . . . . 21
                                                                                          |
136 | 134, 135 | eqtr4di 2228 |
. . . . . . . . . . . . . . . . . . . 20
 
      
                  
                           
                                 |
137 | | fvoveq1 5891 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
    
                  |
138 | 137 | oveq2d 5884 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
    
                      |
139 | | oveq1 5875 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
    
                
             |
140 | 138, 139,
104 | ovmpog 6002 |
. . . . . . . . . . . . . . . . . . . . . . . 24
                              
           
                   
             |
141 | 24, 26, 36, 140 | syl3anc 1238 |
. . . . . . . . . . . . . . . . . . . . . . 23
 
      
           
                   
             |
142 | 141, 36 | eqeltrd 2254 |
. . . . . . . . . . . . . . . . . . . . . 22
 
      
           
                 |
143 | | opelxpi 4654 |
. . . . . . . . . . . . . . . . . . . . . 22
           
           
               
                   
                        |
144 | 29, 142, 143 | syl2anc 411 |
. . . . . . . . . . . . . . . . . . . . 21
 
      
                   
                        |
145 | | oveq1 5875 |
. . . . . . . . . . . . . . . . . . . . . . 23
    
                              
             |
146 | 39, 145 | opeq12d 3784 |
. . . . . . . . . . . . . . . . . . . . . 22
    
                       
                   
              |
147 | | oveq2 5876 |
. . . . . . . . . . . . . . . . . . . . . . 23
    
           
                      
                 |
148 | 147 | opeq2d 3783 |
. . . . . . . . . . . . . . . . . . . . . 22
    
                   
           
                   
                  |
149 | | eqid 2177 |
. . . . . . . . . . . . . . . . . . . . . 22
                 
            
                 
              |
150 | 146, 148,
149 | ovmpog 6002 |
. . . . . . . . . . . . . . . . . . . . 21
             
                   
                      
                       
                                                         |
151 | 24, 27, 144, 150 | syl3anc 1238 |
. . . . . . . . . . . . . . . . . . . 20
 
      
                       
                                                         |
152 | 136, 151 | eqtrd 2210 |
. . . . . . . . . . . . . . . . . . 19
 
      
                  
                                                      |
153 | 152, 144 | eqeltrd 2254 |
. . . . . . . . . . . . . . . . . 18
 
      
                  
                        |
154 | 153 | ralrimiva 2550 |
. . . . . . . . . . . . . . . . 17
                           
                        |
155 | 154 | ad2antlr 489 |
. . . . . . . . . . . . . . . 16
        frec                                                
                                    |
156 | | frecsuc 6401 |
. . . . . . . . . . . . . . . 16
                            
                                    frec      
                                                                       frec                                               |
157 | 155, 121,
81, 156 | syl3anc 1238 |
. . . . . . . . . . . . . . 15
        frec                                  frec      
                                                                       frec                                               |
158 | 133, 157 | eqtrid 2222 |
. . . . . . . . . . . . . 14
        frec                                                        
               frec                                               |
159 | 14 | fveq1i 5511 |
. . . . . . . . . . . . . . 15
    frec                  
                          |
160 | 159 | fveq2i 5513 |
. . . . . . . . . . . . . 14
                  
                                                      frec                                              |
161 | 158, 160 | eqtr4di 2228 |
. . . . . . . . . . . . 13
        frec                                                        
                      |
162 | 128 | fveq2d 5514 |
. . . . . . . . . . . . 13
        frec                                                                               
                                                 |
163 | 161, 162 | eqtrd 2210 |
. . . . . . . . . . . 12
        frec                                                        
                                     |
164 | | df-ov 5871 |
. . . . . . . . . . . 12
                                                                                                          |
165 | 163, 164 | eqtr4di 2228 |
. . . . . . . . . . 11
        frec                                                                 
                         |
166 | | oveq1 5875 |
. . . . . . . . . . . . . 14
        
                                  
             |
167 | 112, 166 | opeq12d 3784 |
. . . . . . . . . . . . 13
        
                       
                           
              |
168 | | oveq2 5876 |
. . . . . . . . . . . . . 14
        
               
                          
                     |
169 | 168 | opeq2d 3783 |
. . . . . . . . . . . . 13
        
                           
           
                           
                      |
170 | 167, 169,
149 | ovmpog 6002 |
. . . . . . . . . . . 12
                     
                           
                          
                           
                                                                         |
171 | 84, 87, 110, 170 | syl3anc 1238 |
. . . . . . . . . . 11
        frec                                                 
                                                                                     |
172 | 165, 171 | eqtrd 2210 |
. . . . . . . . . 10
        frec                                                                                        |
173 | 172, 107 | eqtrd 2210 |
. . . . . . . . 9
        frec                                                                             |
174 | 119, 132,
173 | 3eqtr4rd 2221 |
. . . . . . . 8
        frec                                      frec                                   |
175 | 174 | exp31 364 |
. . . . . . 7
       frec                                
    frec                                     |
176 | 175 | a2d 26 |
. . . . . 6
  
    frec                                       frec      
        
                     |
177 | 60, 64, 68, 72, 79, 176 | finds 4595 |
. . . . 5
      frec      
        
                    |
178 | 177 | impcom 125 |
. . . 4
 

    frec      
        
                   |
179 | 17, 56, 178 | eqfnfvd 5611 |
. . 3
 frec                                |
180 | 179 | rneqd 4851 |
. 2
 frec               
                |
181 | 1, 180 | eqtr4id 2229 |
1
      |