Step | Hyp | Ref
| Expression |
1 | | seqf1o.4 |
. . 3
       |
2 | | eluzfz2 10088 |
. . 3
    
      |
3 | 1, 2 | syl 14 |
. 2
       |
4 | | fveq2 5546 |
. . . . . 6
               |
5 | 4 | oveq2d 5926 |
. . . . 5
     
           
         |
6 | 4 | oveq1d 5925 |
. . . . 5
       
       
           |
7 | 5, 6 | eqeq12d 2208 |
. . . 4
                                                     |
8 | 7 | imbi2d 230 |
. . 3
  
      
           
      
      
           
         |
9 | | fveq2 5546 |
. . . . . 6
               |
10 | 9 | oveq2d 5926 |
. . . . 5
     
           
         |
11 | 9 | oveq1d 5925 |
. . . . 5
       
       
           |
12 | 10, 11 | eqeq12d 2208 |
. . . 4
                                                     |
13 | 12 | imbi2d 230 |
. . 3
  
      
           
      
      
           
         |
14 | | fveq2 5546 |
. . . . . 6
                   |
15 | 14 | oveq2d 5926 |
. . . . 5
       
           
           |
16 | 14 | oveq1d 5925 |
. . . . 5
         
       
             |
17 | 15, 16 | eqeq12d 2208 |
. . . 4
                                                           |
18 | 17 | imbi2d 230 |
. . 3
    
      
           
      
      
                         |
19 | | fveq2 5546 |
. . . . . 6
               |
20 | 19 | oveq2d 5926 |
. . . . 5
     
           
         |
21 | 19 | oveq1d 5925 |
. . . . 5
       
       
           |
22 | 20, 21 | eqeq12d 2208 |
. . . 4
                                                     |
23 | 22 | imbi2d 230 |
. . 3
  
      
           
      
      
           
         |
24 | | seqf1o.2 |
. . . . 5
 

        |
25 | | seqf1olem2a.1 |
. . . . . 6
       |
26 | | seqf1olem2a.3 |
. . . . . 6
   |
27 | 25, 26 | ffvelcdmd 5686 |
. . . . 5
       |
28 | | eluzel2 9587 |
. . . . . . . 8
    
  |
29 | 1, 28 | syl 14 |
. . . . . . 7
   |
30 | | seqf1oglem2a.a |
. . . . . . . 8
   |
31 | 25, 30 | fexd 5780 |
. . . . . . 7
   |
32 | | seqf1og.p |
. . . . . . 7
   |
33 | | seq1g 10524 |
. . . . . . 7
 
             |
34 | 29, 31, 32, 33 | syl3anc 1249 |
. . . . . 6
             |
35 | | seqf1olem2a.4 |
. . . . . . . 8
    
  |
36 | | eluzfz1 10087 |
. . . . . . . . 9
    
      |
37 | 1, 36 | syl 14 |
. . . . . . . 8
       |
38 | 35, 37 | sseldd 3180 |
. . . . . . 7
   |
39 | 25, 38 | ffvelcdmd 5686 |
. . . . . 6
       |
40 | 34, 39 | eqeltrd 2270 |
. . . . 5
         |
41 | 24, 27, 40 | caovcomd 6067 |
. . . 4
                           |
42 | 41 | a1i 9 |
. . 3
    
                            |
43 | | oveq1 5917 |
. . . . . 6
     
                  
     
                                    |
44 | | elfzouz 10207 |
. . . . . . . . . . 11
  ..^
      |
45 | 44 | adantl 277 |
. . . . . . . . . 10
 
 ..^        |
46 | 31 | adantr 276 |
. . . . . . . . . 10
 
 ..^    |
47 | 32 | adantr 276 |
. . . . . . . . . 10
 
 ..^ 
  |
48 | | seqp1g 10527 |
. . . . . . . . . 10
                     
         |
49 | 45, 46, 47, 48 | syl3anc 1249 |
. . . . . . . . 9
 
 ..^   
            
         |
50 | 49 | oveq2d 5926 |
. . . . . . . 8
 
 ..^                    
      
          |
51 | | seqf1o.3 |
. . . . . . . . . 10
 

            |
52 | 51 | adantlr 477 |
. . . . . . . . 9
    ..^  
            |
53 | | seqf1o.5 |
. . . . . . . . . . 11

  |
54 | 53, 27 | sseldd 3180 |
. . . . . . . . . 10
       |
55 | 54 | adantr 276 |
. . . . . . . . 9
 
 ..^        |
56 | 53 | adantr 276 |
. . . . . . . . . . . 12
 
 ..^    |
57 | 56 | adantr 276 |
. . . . . . . . . . 11
    ..^         |
58 | 25 | adantr 276 |
. . . . . . . . . . . . 13
 
 ..^        |
59 | 58 | adantr 276 |
. . . . . . . . . . . 12
    ..^             |
60 | | elfzouz2 10218 |
. . . . . . . . . . . . . . . 16
  ..^
      |
61 | 60 | adantl 277 |
. . . . . . . . . . . . . . 15
 
 ..^        |
62 | | fzss2 10120 |
. . . . . . . . . . . . . . 15
    
          |
63 | 61, 62 | syl 14 |
. . . . . . . . . . . . . 14
 
 ..^            |
64 | 35 | adantr 276 |
. . . . . . . . . . . . . 14
 
 ..^        |
65 | 63, 64 | sstrd 3189 |
. . . . . . . . . . . . 13
 
 ..^        |
66 | 65 | sselda 3179 |
. . . . . . . . . . . 12
    ..^         |
67 | 59, 66 | ffvelcdmd 5686 |
. . . . . . . . . . 11
    ..^             |
68 | 57, 67 | sseldd 3180 |
. . . . . . . . . 10
    ..^             |
69 | | seqf1o.1 |
. . . . . . . . . . 11
 

      |
70 | 69 | adantlr 477 |
. . . . . . . . . 10
    ..^         |
71 | 45, 68, 70, 46, 47 | seqclg 10533 |
. . . . . . . . 9
 
 ..^   
      |
72 | | fzofzp1 10284 |
. . . . . . . . . . . . 13
  ..^
        |
73 | 72 | adantl 277 |
. . . . . . . . . . . 12
 
 ..^          |
74 | 64, 73 | sseldd 3180 |
. . . . . . . . . . 11
 
 ..^      |
75 | 58, 74 | ffvelcdmd 5686 |
. . . . . . . . . 10
 
 ..^     
    |
76 | 56, 75 | sseldd 3180 |
. . . . . . . . 9
 
 ..^     
    |
77 | 52, 55, 71, 76 | caovassd 6070 |
. . . . . . . 8
 
 ..^         
    
                  
          |
78 | 50, 77 | eqtr4d 2229 |
. . . . . . 7
 
 ..^                                      |
79 | 52, 71, 76, 55 | caovassd 6070 |
. . . . . . . 8
 
 ..^         
                  
               |
80 | 49 | oveq1d 5925 |
. . . . . . . 8
 
 ..^                       
              |
81 | 52, 71, 55, 76 | caovassd 6070 |
. . . . . . . . 9
 
 ..^         
                  
               |
82 | 24 | adantlr 477 |
. . . . . . . . . . 11
    ..^           |
83 | 27 | adantr 276 |
. . . . . . . . . . 11
 
 ..^        |
84 | 82, 75, 83 | caovcomd 6067 |
. . . . . . . . . 10
 
 ..^                      
     |
85 | 84 | oveq2d 5926 |
. . . . . . . . 9
 
 ..^        
                   
               |
86 | 81, 85 | eqtr4d 2229 |
. . . . . . . 8
 
 ..^         
                  
               |
87 | 79, 80, 86 | 3eqtr4d 2236 |
. . . . . . 7
 
 ..^                       
              |
88 | 78, 87 | eqeq12d 2208 |
. . . . . 6
 
 ..^         
                                                                |
89 | 43, 88 | imbitrrid 156 |
. . . . 5
 
 ..^         
           
                                    |
90 | 89 | expcom 116 |
. . . 4
  ..^
                         
    
                           |
91 | 90 | a2d 26 |
. . 3
  ..^
                                                            |
92 | 8, 13, 18, 23, 42, 91 | fzind2 10296 |
. 2
                                 |
93 | 3, 92 | mpcom 36 |
1
                           |