Step | Hyp | Ref
| Expression |
1 | | iseqf1o.4 |
. . 3
       |
2 | | eluzfz2 9446 |
. . 3
    
      |
3 | 1, 2 | syl 14 |
. 2
       |
4 | | oveq2 5660 |
. . . . . . 7
           |
5 | 4 | raleqdv 2568 |
. . . . . 6
  
        
             |
6 | 5 | 3anbi2d 1253 |
. . . . 5
                          
   
                               
   
          |
7 | 6 | exbidv 1753 |
. . . 4
                            
   
                                 
   
          |
8 | 7 | imbi2d 228 |
. . 3
  
                          
   
                                   
   
           |
9 | | oveq2 5660 |
. . . . . . 7
           |
10 | 9 | raleqdv 2568 |
. . . . . 6
  
        
             |
11 | 10 | 3anbi2d 1253 |
. . . . 5
                          
   
                               
   
          |
12 | 11 | exbidv 1753 |
. . . 4
                            
   
                                 
   
          |
13 | 12 | imbi2d 228 |
. . 3
  
                          
   
                                   
   
           |
14 | | oveq2 5660 |
. . . . . . 7
               |
15 | 14 | raleqdv 2568 |
. . . . . 6
    
        
               |
16 | 15 | 3anbi2d 1253 |
. . . . 5
                            
   
                                 
   
          |
17 | 16 | exbidv 1753 |
. . . 4
                              
   
                                   
   
          |
18 | 17 | imbi2d 228 |
. . 3
    
                          
   
                                     
   
           |
19 | | oveq2 5660 |
. . . . . . 7
           |
20 | 19 | raleqdv 2568 |
. . . . . 6
  
        
             |
21 | 20 | 3anbi2d 1253 |
. . . . 5
                          
   
                               
   
          |
22 | 21 | exbidv 1753 |
. . . 4
                            
   
                                 
   
          |
23 | 22 | imbi2d 228 |
. . 3
  
                          
   
                                   
   
           |
24 | | iseqf1o.1 |
. . . . 5
 

      |
25 | | iseqf1o.2 |
. . . . 5
 

        |
26 | | iseqf1o.3 |
. . . . 5
 

            |
27 | | iseqf1o.6 |
. . . . 5
               |
28 | | iseqf1o.7 |
. . . . 5
 
    
      |
29 | | eluzfz1 9445 |
. . . . . 6
    
      |
30 | 1, 29 | syl 14 |
. . . . 5
       |
31 | | ral0 3383 |
. . . . . . 7
      |
32 | | fzo0 9579 |
. . . . . . . 8
 ..^  |
33 | 32 | raleqi 2566 |
. . . . . . 7
 
 ..^             |
34 | 31, 33 | mpbir 144 |
. . . . . 6
  ..^       |
35 | 34 | a1i 9 |
. . . . 5
   ..^        |
36 | | f1of 5253 |
. . . . . . . . . 10
            
              |
37 | 27, 36 | syl 14 |
. . . . . . . . 9
               |
38 | | eluzel2 9024 |
. . . . . . . . . . 11
    
  |
39 | 1, 38 | syl 14 |
. . . . . . . . . 10
   |
40 | | eluzelz 9028 |
. . . . . . . . . . 11
    
  |
41 | 1, 40 | syl 14 |
. . . . . . . . . 10
   |
42 | 39, 41 | fzfigd 9838 |
. . . . . . . . 9
       |
43 | | fex 5524 |
. . . . . . . . 9
                     |
44 | 37, 42, 43 | syl2anc 403 |
. . . . . . . 8
   |
45 | | fveq1 5304 |
. . . . . . . . . . . . 13
           |
46 | 45 | fveq2d 5309 |
. . . . . . . . . . . 12
                   |
47 | 46 | ifeq1d 3408 |
. . . . . . . . . . 11
  
                                  |
48 | 47 | mpteq2dv 3929 |
. . . . . . . . . 10
       
                                         |
49 | | iseqf1o.p |
. . . . . . . . . 10
                        |
50 | | iseqf1o.l |
. . . . . . . . . 10
                        |
51 | 48, 49, 50 | 3eqtr4g 2145 |
. . . . . . . . 9
   |
52 | 51 | adantl 271 |
. . . . . . . 8
 
   |
53 | 44, 52 | csbied 2974 |
. . . . . . 7
   ![]_ ]_](_urbrack.gif)
  |
54 | 53 | seqeq3d 9866 |
. . . . . 6
     ![]_ ]_](_urbrack.gif)       |
55 | 54 | fveq1d 5307 |
. . . . 5
     ![]_ ]_](_urbrack.gif)    
        |
56 | 24, 25, 26, 1, 27, 28, 30, 27, 35, 55, 49 | seq3f1olemstep 9930 |
. . . 4
               
           
   
         |
57 | 56 | a1i 9 |
. . 3
    
               
           
   
          |
58 | | nfv 1466 |
. . . . . . . 8
                          
   
        |
59 | | nfv 1466 |
. . . . . . . . 9
              |
60 | | nfv 1466 |
. . . . . . . . 9
             |
61 | | nfcv 2228 |
. . . . . . . . . . . 12
   |
62 | | nfcv 2228 |
. . . . . . . . . . . 12
  |
63 | | nfcsb1v 2963 |
. . . . . . . . . . . 12
  
 ![]_ ]_](_urbrack.gif)  |
64 | 61, 62, 63 | nfseq 9869 |
. . . . . . . . . . 11
   
 ![]_ ]_](_urbrack.gif)   |
65 | | nfcv 2228 |
. . . . . . . . . . 11
   |
66 | 64, 65 | nffv 5315 |
. . . . . . . . . 10
      ![]_ ]_](_urbrack.gif)      |
67 | 66 | nfeq1 2238 |
. . . . . . . . 9
      ![]_ ]_](_urbrack.gif)    
       |
68 | 59, 60, 67 | nf3an 1503 |
. . . . . . . 8
                          
  ![]_ ]_](_urbrack.gif)    
        |
69 | | f1oeq1 5244 |
. . . . . . . . 9
             
               |
70 | | fveq1 5304 |
. . . . . . . . . . 11
           |
71 | 70 | eqeq1d 2096 |
. . . . . . . . . 10
     
       |
72 | 71 | ralbidv 2380 |
. . . . . . . . 9
  
        
             |
73 | | csbeq1a 2941 |
. . . . . . . . . . . 12
   ![]_ ]_](_urbrack.gif)   |
74 | 73 | seqeq3d 9866 |
. . . . . . . . . . 11
      
 ![]_ ]_](_urbrack.gif)    |
75 | 74 | fveq1d 5307 |
. . . . . . . . . 10
         
 ![]_ ]_](_urbrack.gif)       |
76 | 75 | eqeq1d 2096 |
. . . . . . . . 9
               
  ![]_ ]_](_urbrack.gif)    
         |
77 | 69, 72, 76 | 3anbi123d 1248 |
. . . . . . . 8
                          
   
                               
  ![]_ ]_](_urbrack.gif)    
          |
78 | 58, 68, 77 | cbvex 1686 |
. . . . . . 7
                           
   
                                 
  ![]_ ]_](_urbrack.gif)    
         |
79 | | fveq2 5305 |
. . . . . . . . . . 11
           |
80 | | id 19 |
. . . . . . . . . . 11
   |
81 | 79, 80 | eqeq12d 2102 |
. . . . . . . . . 10
     
       |
82 | 81 | cbvralv 2590 |
. . . . . . . . 9
 
                     |
83 | 82 | 3anbi2i 1135 |
. . . . . . . 8
                          
 ![]_ ]_](_urbrack.gif)           
            
           
  ![]_ ]_](_urbrack.gif)    
         |
84 | 83 | exbii 1541 |
. . . . . . 7
                           
  ![]_ ]_](_urbrack.gif)    
                                 
  ![]_ ]_](_urbrack.gif)    
         |
85 | 78, 84 | bitri 182 |
. . . . . 6
                           
   
                                 
  ![]_ ]_](_urbrack.gif)    
         |
86 | | simpll 496 |
. . . . . . . . . 10
    ..^              
           
  ![]_ ]_](_urbrack.gif)    
       
  |
87 | 86, 24 | sylan 277 |
. . . . . . . . 9
   
 ..^                          
  ![]_ ]_](_urbrack.gif)    
               |
88 | 86, 25 | sylan 277 |
. . . . . . . . 9
   
 ..^                          
  ![]_ ]_](_urbrack.gif)    
                 |
89 | 86, 26 | sylan 277 |
. . . . . . . . 9
   
 ..^                          
  ![]_ ]_](_urbrack.gif)    
        
            |
90 | 1 | ad2antrr 472 |
. . . . . . . . 9
    ..^              
           
  ![]_ ]_](_urbrack.gif)    
       
      |
91 | 27 | ad2antrr 472 |
. . . . . . . . 9
    ..^              
           
  ![]_ ]_](_urbrack.gif)    
       
              |
92 | 86, 28 | sylan 277 |
. . . . . . . . 9
   
 ..^                          
  ![]_ ]_](_urbrack.gif)    
            
      |
93 | | fzofzp1 9638 |
. . . . . . . . . 10
  ..^
        |
94 | 93 | ad2antlr 473 |
. . . . . . . . 9
    ..^              
           
  ![]_ ]_](_urbrack.gif)    
       
        |
95 | | simpr1 949 |
. . . . . . . . 9
    ..^              
           
  ![]_ ]_](_urbrack.gif)    
       
              |
96 | | simpr2 950 |
. . . . . . . . . . 11
    ..^              
           
  ![]_ ]_](_urbrack.gif)    
       
            |
97 | 96, 82 | sylibr 132 |
. . . . . . . . . 10
    ..^              
           
  ![]_ ]_](_urbrack.gif)    
       
            |
98 | | elfzoelz 9558 |
. . . . . . . . . . . 12
  ..^
  |
99 | 98 | ad2antlr 473 |
. . . . . . . . . . 11
    ..^              
           
  ![]_ ]_](_urbrack.gif)    
       
  |
100 | | fzval3 9615 |
. . . . . . . . . . . 12
      ..^     |
101 | 100 | raleqdv 2568 |
. . . . . . . . . . 11
  
        
  ..^           |
102 | 99, 101 | syl 14 |
. . . . . . . . . 10
    ..^              
           
  ![]_ ]_](_urbrack.gif)    
       
 
           ..^           |
103 | 97, 102 | mpbid 145 |
. . . . . . . . 9
    ..^              
           
  ![]_ ]_](_urbrack.gif)    
       
  ..^          |
104 | | simpr3 951 |
. . . . . . . . 9
    ..^              
           
  ![]_ ]_](_urbrack.gif)    
       
  
 ![]_ ]_](_urbrack.gif)             |
105 | 87, 88, 89, 90, 91, 92, 94, 95, 103, 104, 49 | seq3f1olemstep 9930 |
. . . . . . . 8
    ..^              
           
  ![]_ ]_](_urbrack.gif)    
       
                            
   
         |
106 | 105 | ex 113 |
. . . . . . 7
 
 ..^               
           
  ![]_ ]_](_urbrack.gif)    
                     
             
   
          |
107 | 106 | exlimdv 1747 |
. . . . . 6
 
 ..^                             
  ![]_ ]_](_urbrack.gif)    
                     
             
   
          |
108 | 85, 107 | syl5bi 150 |
. . . . 5
 
 ..^                             
   
                     
             
   
          |
109 | 108 | expcom 114 |
. . . 4
  ..^
                                                                    
   
           |
110 | 109 | a2d 26 |
. . 3
  ..^
                
           
   
       
               
             
   
           |
111 | 8, 13, 18, 23, 57, 110 | fzind2 9650 |
. 2
                    
           
   
          |
112 | 3, 111 | mpcom 36 |
1
               
           
   
         |