Step | Hyp | Ref
| Expression |
1 | | fzssp1 11841 |
. . . 4
               |
2 | | cvmliftlem.n |
. . . . . . . 8
   |
3 | 2 | nncnd 10625 |
. . . . . . 7
   |
4 | 3 | adantr 467 |
. . . . . 6
 
       |
5 | | ax-1cn 9597 |
. . . . . 6
 |
6 | | npcan 9884 |
. . . . . 6
 
       |
7 | 4, 5, 6 | sylancl 668 |
. . . . 5
 
           |
8 | 7 | oveq2d 6306 |
. . . 4
 
                   |
9 | 1, 8 | syl5sseq 3480 |
. . 3
 
                 |
10 | | simpr 463 |
. . . 4
 
           |
11 | | elfzelz 11800 |
. . . . 5
       |
12 | 2 | nnzd 11039 |
. . . . 5
   |
13 | | elfzm1b 11872 |
. . . . 5
 
                 |
14 | 11, 12, 13 | syl2anr 481 |
. . . 4
 
     
   
     
     |
15 | 10, 14 | mpbid 214 |
. . 3
 
     
         |
16 | 9, 15 | sseldd 3433 |
. 2
 
     
       |
17 | | elfznn0 11887 |
. . . 4
       
   |
18 | 17 | adantl 468 |
. . 3
 
       
   |
19 | | eleq1 2517 |
. . . . . . 7
     
       |
20 | | fveq2 5865 |
. . . . . . . . 9
           |
21 | | oveq1 6297 |
. . . . . . . . 9
       |
22 | 20, 21 | fveq12d 5871 |
. . . . . . . 8
                       |
23 | 21 | fveq2d 5869 |
. . . . . . . . . 10
               |
24 | 23 | sneqd 3980 |
. . . . . . . . 9
                   |
25 | 24 | imaeq2d 5168 |
. . . . . . . 8
                             |
26 | 22, 25 | eleq12d 2523 |
. . . . . . 7
                        
                          |
27 | 19, 26 | imbi12d 322 |
. . . . . 6
                              
                                |
28 | 27 | imbi2d 318 |
. . . . 5
  
                             
                                  |
29 | | eleq1 2517 |
. . . . . . 7
     
       |
30 | | fveq2 5865 |
. . . . . . . . 9
           |
31 | | oveq1 6297 |
. . . . . . . . 9
       |
32 | 30, 31 | fveq12d 5871 |
. . . . . . . 8
                       |
33 | 31 | fveq2d 5869 |
. . . . . . . . . 10
               |
34 | 33 | sneqd 3980 |
. . . . . . . . 9
                   |
35 | 34 | imaeq2d 5168 |
. . . . . . . 8
                             |
36 | 32, 35 | eleq12d 2523 |
. . . . . . 7
                        
                          |
37 | 29, 36 | imbi12d 322 |
. . . . . 6
                              
    
                           |
38 | 37 | imbi2d 318 |
. . . . 5
  
                             
             
                    |
39 | | eleq1 2517 |
. . . . . . 7
       
         |
40 | | fveq2 5865 |
. . . . . . . . 9
          
    |
41 | | oveq1 6297 |
. . . . . . . . 9
           |
42 | 40, 41 | fveq12d 5871 |
. . . . . . . 8
                 
           |
43 | 41 | fveq2d 5869 |
. . . . . . . . . 10
                   |
44 | 43 | sneqd 3980 |
. . . . . . . . 9
                       |
45 | 44 | imaeq2d 5168 |
. . . . . . . 8
                                 |
46 | 42, 45 | eleq12d 2523 |
. . . . . . 7
                          
                                |
47 | 39, 46 | imbi12d 322 |
. . . . . 6
                                
                                        |
48 | 47 | imbi2d 318 |
. . . . 5
    
                             
                                          |
49 | | eleq1 2517 |
. . . . . . 7
       
         |
50 | | fveq2 5865 |
. . . . . . . . 9
          
    |
51 | | oveq1 6297 |
. . . . . . . . 9
           |
52 | 50, 51 | fveq12d 5871 |
. . . . . . . 8
                 
           |
53 | 51 | fveq2d 5869 |
. . . . . . . . . 10
                   |
54 | 53 | sneqd 3980 |
. . . . . . . . 9
                       |
55 | 54 | imaeq2d 5168 |
. . . . . . . 8
                                 |
56 | 52, 55 | eleq12d 2523 |
. . . . . . 7
                          
                                |
57 | 49, 56 | imbi12d 322 |
. . . . . 6
                                
 
         
                            |
58 | 57 | imbi2d 318 |
. . . . 5
    
                             
                                          |
59 | | cvmliftlem.1 |
. . . . . . . . . . 11
                       
    ↾t    
↾t        |
60 | | cvmliftlem.b |
. . . . . . . . . . 11
  |
61 | | cvmliftlem.x |
. . . . . . . . . . 11
  |
62 | | cvmliftlem.f |
. . . . . . . . . . 11
  CovMap    |
63 | | cvmliftlem.g |
. . . . . . . . . . 11
     |
64 | | cvmliftlem.p |
. . . . . . . . . . 11
   |
65 | | cvmliftlem.e |
. . . . . . . . . . 11
           |
66 | | cvmliftlem.t |
. . . . . . . . . . 11
                    |
67 | | cvmliftlem.a |
. . . . . . . . . . 11
                ![[,] [,]](_icc.gif)    
          |
68 | | cvmliftlem.l |
. . . . . . . . . . 11
     |
69 | | cvmliftlem.q |
. . . . . . . . . . 11
    
       ![[,] [,]](_icc.gif)                                                     |
70 | 59, 60, 61, 62, 63, 64, 65, 2, 66, 67, 68, 69 | cvmliftlem4 30011 |
. . . . . . . . . 10
          |
71 | 70 | a1i 11 |
. . . . . . . . 9
       
    |
72 | 2 | nnne0d 10654 |
. . . . . . . . . 10
   |
73 | 3, 72 | div0d 10382 |
. . . . . . . . 9
     |
74 | 71, 73 | fveq12d 5871 |
. . . . . . . 8
                      |
75 | | 0nn0 10884 |
. . . . . . . . 9
 |
76 | | fvsng 6098 |
. . . . . . . . 9
 
            |
77 | 75, 64, 76 | sylancr 669 |
. . . . . . . 8
            |
78 | 74, 77 | eqtrd 2485 |
. . . . . . 7
             |
79 | 73 | fveq2d 5869 |
. . . . . . . . 9
             |
80 | 65, 79 | eqtr4d 2488 |
. . . . . . . 8
             |
81 | | cvmcn 29985 |
. . . . . . . . . . 11
  CovMap 

   |
82 | 62, 81 | syl 17 |
. . . . . . . . . 10
     |
83 | 60, 61 | cnf 20262 |
. . . . . . . . . 10
         |
84 | | ffn 5728 |
. . . . . . . . . 10
    
  |
85 | 82, 83, 84 | 3syl 18 |
. . . . . . . . 9
   |
86 | | fniniseg 6003 |
. . . . . . . . 9
 
                            |
87 | 85, 86 | syl 17 |
. . . . . . . 8
              

              |
88 | 64, 80, 87 | mpbir2and 933 |
. . . . . . 7
                |
89 | 78, 88 | eqeltrd 2529 |
. . . . . 6
                          |
90 | 89 | a1d 26 |
. . . . 5
                                |
91 | | id 22 |
. . . . . . . . . . . 12

  |
92 | | nn0uz 11193 |
. . . . . . . . . . . 12
     |
93 | 91, 92 | syl6eleq 2539 |
. . . . . . . . . . 11

      |
94 | 93 | adantl 468 |
. . . . . . . . . 10
 

      |
95 | | peano2fzr 11812 |
. . . . . . . . . . 11
            
      |
96 | 95 | ex 436 |
. . . . . . . . . 10
    
              |
97 | 94, 96 | syl 17 |
. . . . . . . . 9
 

              |
98 | 97 | imim1d 78 |
. . . . . . . 8
 

                                            
                   |
99 | | eqid 2451 |
. . . . . . . . . . . . . . 15
        ![[,] [,]](_icc.gif)              ![[,] [,]](_icc.gif)       |
100 | | simprlr 773 |
. . . . . . . . . . . . . . . . 17
 
  
             
                         |
101 | | elfzle2 11803 |
. . . . . . . . . . . . . . . . 17
           |
102 | 100, 101 | syl 17 |
. . . . . . . . . . . . . . . 16
 
  
             
                     |
103 | | simprll 772 |
. . . . . . . . . . . . . . . . . . 19
 
  
             
                   |
104 | | nn0p1nn 10909 |
. . . . . . . . . . . . . . . . . . 19

    |
105 | 103, 104 | syl 17 |
. . . . . . . . . . . . . . . . . 18
 
  
             
                     |
106 | | nnuz 11194 |
. . . . . . . . . . . . . . . . . 18
     |
107 | 105, 106 | syl6eleq 2539 |
. . . . . . . . . . . . . . . . 17
 
  
             
                         |
108 | 12 | adantr 467 |
. . . . . . . . . . . . . . . . 17
 
  
             
                   |
109 | | elfz5 11792 |
. . . . . . . . . . . . . . . . 17
               
     |
110 | 107, 108,
109 | syl2anc 667 |
. . . . . . . . . . . . . . . 16
 
  
             
                             |
111 | 102, 110 | mpbird 236 |
. . . . . . . . . . . . . . 15
 
  
             
                         |
112 | | simprr 766 |
. . . . . . . . . . . . . . . 16
 
  
             
                        
                 |
113 | 103 | nn0cnd 10927 |
. . . . . . . . . . . . . . . . . . 19
 
  
             
                   |
114 | | pncan 9881 |
. . . . . . . . . . . . . . . . . . 19
 
       |
115 | 113, 5, 114 | sylancl 668 |
. . . . . . . . . . . . . . . . . 18
 
  
             
                       |
116 | 115 | fveq2d 5869 |
. . . . . . . . . . . . . . . . 17
 
  
             
                               |
117 | 115 | oveq1d 6305 |
. . . . . . . . . . . . . . . . 17
 
  
             
                           |
118 | 116, 117 | fveq12d 5871 |
. . . . . . . . . . . . . . . 16
 
  
             
                                               |
119 | 117 | fveq2d 5869 |
. . . . . . . . . . . . . . . . . 18
 
  
             
                                   |
120 | 119 | sneqd 3980 |
. . . . . . . . . . . . . . . . 17
 
  
             
                                       |
121 | 120 | imaeq2d 5168 |
. . . . . . . . . . . . . . . 16
 
  
             
                                          
      |
122 | 112, 118,
121 | 3eltr4d 2544 |
. . . . . . . . . . . . . . 15
 
  
             
                                                      |
123 | 59, 60, 61, 62, 63, 64, 65, 2, 66, 67, 68, 69, 99, 111, 122 | cvmliftlem6 30013 |
. . . . . . . . . . . . . 14
 
  
             
                                  ![[,] [,]](_icc.gif)        
                ![[,] [,]](_icc.gif)          |
124 | 123 | simpld 461 |
. . . . . . . . . . . . 13
 
  
             
                    
            ![[,] [,]](_icc.gif)          |
125 | 103 | nn0red 10926 |
. . . . . . . . . . . . . . . . 17
 
  
             
                   |
126 | 2 | adantr 467 |
. . . . . . . . . . . . . . . . 17
 
  
             
                   |
127 | 125, 126 | nndivred 10658 |
. . . . . . . . . . . . . . . 16
 
  
             
                     |
128 | 127 | rexrd 9690 |
. . . . . . . . . . . . . . 15
 
  
             
                     |
129 | | peano2re 9806 |
. . . . . . . . . . . . . . . . . 18
     |
130 | 125, 129 | syl 17 |
. . . . . . . . . . . . . . . . 17
 
  
             
                     |
131 | 130, 126 | nndivred 10658 |
. . . . . . . . . . . . . . . 16
 
  
             
                       |
132 | 131 | rexrd 9690 |
. . . . . . . . . . . . . . 15
 
  
             
                       |
133 | 125 | ltp1d 10537 |
. . . . . . . . . . . . . . . . 17
 
  
             
                     |
134 | 126 | nnred 10624 |
. . . . . . . . . . . . . . . . . 18
 
  
             
                   |
135 | 126 | nngt0d 10653 |
. . . . . . . . . . . . . . . . . 18
 
  
             
                   |
136 | | ltdiv1 10469 |
. . . . . . . . . . . . . . . . . 18
  
 
 
            |
137 | 125, 130,
134, 135, 136 | syl112anc 1272 |
. . . . . . . . . . . . . . . . 17
 
  
             
                             |
138 | 133, 137 | mpbid 214 |
. . . . . . . . . . . . . . . 16
 
  
             
                         |
139 | 127, 131,
138 | ltled 9783 |
. . . . . . . . . . . . . . 15
 
  
             
                         |
140 | | ubicc2 11749 |
. . . . . . . . . . . . . . 15
       
               ![[,] [,]](_icc.gif)        |
141 | 128, 132,
139, 140 | syl3anc 1268 |
. . . . . . . . . . . . . 14
 
  
             
                         ![[,] [,]](_icc.gif)        |
142 | 117 | oveq1d 6305 |
. . . . . . . . . . . . . 14
 
  
             
                         ![[,] [,]](_icc.gif)          ![[,] [,]](_icc.gif)        |
143 | 141, 142 | eleqtrrd 2532 |
. . . . . . . . . . . . 13
 
  
             
                             ![[,] [,]](_icc.gif)        |
144 | 124, 143 | ffvelrnd 6023 |
. . . . . . . . . . . 12
 
  
             
                                 |
145 | 123 | simprd 465 |
. . . . . . . . . . . . . . 15
 
  
             
                                  ![[,] [,]](_icc.gif)         |
146 | 142 | reseq2d 5105 |
. . . . . . . . . . . . . . 15
 
  
             
                          ![[,] [,]](_icc.gif)       
    ![[,] [,]](_icc.gif)         |
147 | 145, 146 | eqtrd 2485 |
. . . . . . . . . . . . . 14
 
  
             
                              ![[,] [,]](_icc.gif)         |
148 | 147 | fveq1d 5867 |
. . . . . . . . . . . . 13
 
  
             
                      
                ![[,] [,]](_icc.gif)                |
149 | 142 | feq2d 5715 |
. . . . . . . . . . . . . . 15
 
  
             
                                  ![[,] [,]](_icc.gif)       
            ![[,] [,]](_icc.gif)           |
150 | 124, 149 | mpbid 214 |
. . . . . . . . . . . . . 14
 
  
             
                    
        ![[,] [,]](_icc.gif)          |
151 | | fvco3 5942 |
. . . . . . . . . . . . . 14
              ![[,] [,]](_icc.gif)                ![[,] [,]](_icc.gif)      
 
                                  |
152 | 150, 141,
151 | syl2anc 667 |
. . . . . . . . . . . . 13
 
  
             
                      
                              |
153 | | fvres 5879 |
. . . . . . . . . . . . . 14
         ![[,] [,]](_icc.gif)            ![[,] [,]](_icc.gif)                        |
154 | 141, 153 | syl 17 |
. . . . . . . . . . . . 13
 
  
             
                       ![[,] [,]](_icc.gif)                        |
155 | 148, 152,
154 | 3eqtr3d 2493 |
. . . . . . . . . . . 12
 
  
             
                        
                    |
156 | 85 | adantr 467 |
. . . . . . . . . . . . 13
 
  
             
                   |
157 | | fniniseg 6003 |
. . . . . . . . . . . . 13
      
                       
                                             |
158 | 156, 157 | syl 17 |
. . . . . . . . . . . 12
 
  
             
                                                                                            |
159 | 144, 155,
158 | mpbir2and 933 |
. . . . . . . . . . 11
 
  
             
                                                |
160 | 159 | expr 620 |
. . . . . . . . . 10
 
                 
                                               |
161 | 160 | expr 620 |
. . . . . . . . 9
 

                                                                |
162 | 161 | a2d 29 |
. . . . . . . 8
 

                                                                        |
163 | 98, 162 | syld 45 |
. . . . . . 7
 

                                                                      |
164 | 163 | expcom 437 |
. . . . . 6

      
                                                                 |
165 | 164 | a2d 29 |
. . . . 5

      
                                     
                             |
166 | 28, 38, 48, 58, 90, 165 | nn0ind 11030 |
. . . 4
  
                                         |
167 | 166 | impd 433 |
. . 3
  
 
           
                           |
168 | 18, 167 | mpcom 37 |
. 2
 
           
                          |
169 | 16, 168 | syldan 473 |
1
 
         
                          |