Step | Hyp | Ref
| Expression |
1 | | cvmliftlem.n |
. . . 4
   |
2 | | nnuz 10485 |
. . . 4
     |
3 | 1, 2 | syl6eleq 2502 |
. . 3
       |
4 | | eluzfz2 11029 |
. . 3
    
      |
5 | 3, 4 | syl 16 |
. 2
       |
6 | | eleq1 2472 |
. . . . . 6
     
       |
7 | | oveq2 6056 |
. . . . . . . . . . 11
           |
8 | | 1z 10275 |
. . . . . . . . . . . 12
 |
9 | | fzsn 11058 |
. . . . . . . . . . . 12
         |
10 | 8, 9 | ax-mp 8 |
. . . . . . . . . . 11
       |
11 | 7, 10 | syl6eq 2460 |
. . . . . . . . . 10
         |
12 | 11 | iuneq1d 4084 |
. . . . . . . . 9
           
        |
13 | | 1ex 9050 |
. . . . . . . . . 10
 |
14 | | fveq2 5695 |
. . . . . . . . . 10
           |
15 | 13, 14 | iunxsn 4138 |
. . . . . . . . 9
            |
16 | 12, 15 | syl6eq 2460 |
. . . . . . . 8
                 |
17 | | oveq1 6055 |
. . . . . . . . . . 11
       |
18 | 17 | oveq2d 6064 |
. . . . . . . . . 10
   ![[,] [,]](_icc.gif)      ![[,] [,]](_icc.gif)      |
19 | 18 | oveq2d 6064 |
. . . . . . . . 9
  ↾t   ![[,] [,]](_icc.gif)      ↾t   ![[,] [,]](_icc.gif)       |
20 | 19 | oveq1d 6063 |
. . . . . . . 8
  
↾t   ![[,] [,]](_icc.gif)       
↾t   ![[,] [,]](_icc.gif)        |
21 | 16, 20 | eleq12d 2480 |
. . . . . . 7
  
           ↾t   ![[,] [,]](_icc.gif)            ↾t   ![[,] [,]](_icc.gif)         |
22 | 16 | coeq2d 5002 |
. . . . . . . 8
 
                   |
23 | 18 | reseq2d 5113 |
. . . . . . . 8
    ![[,] [,]](_icc.gif)        ![[,] [,]](_icc.gif)       |
24 | 22, 23 | eqeq12d 2426 |
. . . . . . 7
   
             ![[,] [,]](_icc.gif)    
      
  ![[,] [,]](_icc.gif)        |
25 | 21, 24 | anbi12d 692 |
. . . . . 6
               ↾t   ![[,] [,]](_icc.gif)     
            
  ![[,] [,]](_icc.gif)             ↾t   ![[,] [,]](_icc.gif)      
        ![[,] [,]](_icc.gif)         |
26 | 6, 25 | imbi12d 312 |
. . . . 5
                   
↾t   ![[,] [,]](_icc.gif)      
              ![[,] [,]](_icc.gif)      
            ↾t   ![[,] [,]](_icc.gif)     
      
  ![[,] [,]](_icc.gif)          |
27 | 26 | imbi2d 308 |
. . . 4
  
      
           ↾t   ![[,] [,]](_icc.gif)                     ![[,] [,]](_icc.gif)                    
↾t   ![[,] [,]](_icc.gif)      
        ![[,] [,]](_icc.gif)           |
28 | | eleq1 2472 |
. . . . . 6
     
       |
29 | | oveq2 6056 |
. . . . . . . . 9
           |
30 | 29 | iuneq1d 4084 |
. . . . . . . 8
           
           |
31 | | oveq1 6055 |
. . . . . . . . . . 11
       |
32 | 31 | oveq2d 6064 |
. . . . . . . . . 10
   ![[,] [,]](_icc.gif)      ![[,] [,]](_icc.gif)      |
33 | 32 | oveq2d 6064 |
. . . . . . . . 9
  ↾t   ![[,] [,]](_icc.gif)      ↾t   ![[,] [,]](_icc.gif)       |
34 | 33 | oveq1d 6063 |
. . . . . . . 8
  
↾t   ![[,] [,]](_icc.gif)       
↾t   ![[,] [,]](_icc.gif)        |
35 | 30, 34 | eleq12d 2480 |
. . . . . . 7
  
           ↾t   ![[,] [,]](_icc.gif)      
           ↾t   ![[,] [,]](_icc.gif)         |
36 | 30 | coeq2d 5002 |
. . . . . . . 8
 
            
            |
37 | 32 | reseq2d 5113 |
. . . . . . . 8
    ![[,] [,]](_icc.gif)        ![[,] [,]](_icc.gif)       |
38 | 36, 37 | eqeq12d 2426 |
. . . . . . 7
   
             ![[,] [,]](_icc.gif)    
            
  ![[,] [,]](_icc.gif)        |
39 | 35, 38 | anbi12d 692 |
. . . . . 6
               ↾t   ![[,] [,]](_icc.gif)     
            
  ![[,] [,]](_icc.gif)                  
↾t   ![[,] [,]](_icc.gif)      
              ![[,] [,]](_icc.gif)         |
40 | 28, 39 | imbi12d 312 |
. . . . 5
                   
↾t   ![[,] [,]](_icc.gif)      
              ![[,] [,]](_icc.gif)      
    
 
           ↾t   ![[,] [,]](_icc.gif)                     ![[,] [,]](_icc.gif)          |
41 | 40 | imbi2d 308 |
. . . 4
  
      
           ↾t   ![[,] [,]](_icc.gif)                     ![[,] [,]](_icc.gif)                           ↾t   ![[,] [,]](_icc.gif)     
            
  ![[,] [,]](_icc.gif)           |
42 | | eleq1 2472 |
. . . . . 6
       
         |
43 | | oveq2 6056 |
. . . . . . . . 9
               |
44 | 43 | iuneq1d 4084 |
. . . . . . . 8
             
             |
45 | | oveq1 6055 |
. . . . . . . . . . 11
           |
46 | 45 | oveq2d 6064 |
. . . . . . . . . 10
     ![[,] [,]](_icc.gif)      ![[,] [,]](_icc.gif)        |
47 | 46 | oveq2d 6064 |
. . . . . . . . 9
    ↾t   ![[,] [,]](_icc.gif)      ↾t   ![[,] [,]](_icc.gif)         |
48 | 47 | oveq1d 6063 |
. . . . . . . 8
    
↾t   ![[,] [,]](_icc.gif)       
↾t   ![[,] [,]](_icc.gif)          |
49 | 44, 48 | eleq12d 2480 |
. . . . . . 7
    
           ↾t   ![[,] [,]](_icc.gif)      
             ↾t   ![[,] [,]](_icc.gif)           |
50 | 44 | coeq2d 5002 |
. . . . . . . 8
   
            
              |
51 | 46 | reseq2d 5113 |
. . . . . . . 8
      ![[,] [,]](_icc.gif)        ![[,] [,]](_icc.gif)         |
52 | 50, 51 | eqeq12d 2426 |
. . . . . . 7
     
             ![[,] [,]](_icc.gif)    
              
  ![[,] [,]](_icc.gif)          |
53 | 49, 52 | anbi12d 692 |
. . . . . 6
                 ↾t   ![[,] [,]](_icc.gif)     
            
  ![[,] [,]](_icc.gif)                    
↾t   ![[,] [,]](_icc.gif)        
                ![[,] [,]](_icc.gif)           |
54 | 42, 53 | imbi12d 312 |
. . . . 5
                     
↾t   ![[,] [,]](_icc.gif)      
              ![[,] [,]](_icc.gif)      
        
             ↾t   ![[,] [,]](_icc.gif)                         ![[,] [,]](_icc.gif)            |
55 | 54 | imbi2d 308 |
. . . 4
    
      
           ↾t   ![[,] [,]](_icc.gif)                     ![[,] [,]](_icc.gif)                               ↾t   ![[,] [,]](_icc.gif)       
              
  ![[,] [,]](_icc.gif)             |
56 | | eleq1 2472 |
. . . . . 6
     
       |
57 | | oveq2 6056 |
. . . . . . . . . 10
           |
58 | 57 | iuneq1d 4084 |
. . . . . . . . 9
           
           |
59 | | cvmliftlem.k |
. . . . . . . . 9
           |
60 | 58, 59 | syl6eqr 2462 |
. . . . . . . 8
             |
61 | | oveq1 6055 |
. . . . . . . . . . 11
       |
62 | 61 | oveq2d 6064 |
. . . . . . . . . 10
   ![[,] [,]](_icc.gif)      ![[,] [,]](_icc.gif)      |
63 | 62 | oveq2d 6064 |
. . . . . . . . 9
  ↾t   ![[,] [,]](_icc.gif)      ↾t   ![[,] [,]](_icc.gif)       |
64 | 63 | oveq1d 6063 |
. . . . . . . 8
  
↾t   ![[,] [,]](_icc.gif)       
↾t   ![[,] [,]](_icc.gif)        |
65 | 60, 64 | eleq12d 2480 |
. . . . . . 7
  
           ↾t   ![[,] [,]](_icc.gif)        ↾t   ![[,] [,]](_icc.gif)         |
66 | 60 | coeq2d 5002 |
. . . . . . . 8
 
               |
67 | 62 | reseq2d 5113 |
. . . . . . . 8
    ![[,] [,]](_icc.gif)        ![[,] [,]](_icc.gif)       |
68 | 66, 67 | eqeq12d 2426 |
. . . . . . 7
   
             ![[,] [,]](_icc.gif)    
  
  ![[,] [,]](_icc.gif)        |
69 | 65, 68 | anbi12d 692 |
. . . . . 6
               ↾t   ![[,] [,]](_icc.gif)     
            
  ![[,] [,]](_icc.gif)         ↾t   ![[,] [,]](_icc.gif)      
    ![[,] [,]](_icc.gif)         |
70 | 56, 69 | imbi12d 312 |
. . . . 5
                   
↾t   ![[,] [,]](_icc.gif)      
              ![[,] [,]](_icc.gif)      
    
   ↾t   ![[,] [,]](_icc.gif)      
    ![[,] [,]](_icc.gif)          |
71 | 70 | imbi2d 308 |
. . . 4
  
      
           ↾t   ![[,] [,]](_icc.gif)                     ![[,] [,]](_icc.gif)                
↾t   ![[,] [,]](_icc.gif)      
    ![[,] [,]](_icc.gif)           |
72 | | eluzfz1 11028 |
. . . . . . . . 9
    
      |
73 | 3, 72 | syl 16 |
. . . . . . . 8
       |
74 | | cvmliftlem.1 |
. . . . . . . . 9
                       
    ↾t  
↾t        |
75 | | cvmliftlem.b |
. . . . . . . . 9
  |
76 | | cvmliftlem.x |
. . . . . . . . 9
  |
77 | | cvmliftlem.f |
. . . . . . . . 9
  CovMap    |
78 | | cvmliftlem.g |
. . . . . . . . 9
     |
79 | | cvmliftlem.p |
. . . . . . . . 9
   |
80 | | cvmliftlem.e |
. . . . . . . . 9
           |
81 | | cvmliftlem.t |
. . . . . . . . 9
                    |
82 | | cvmliftlem.a |
. . . . . . . . 9
                ![[,] [,]](_icc.gif)    
          |
83 | | cvmliftlem.l |
. . . . . . . . 9
     |
84 | | cvmliftlem.q |
. . . . . . . . 9
   
       ![[,] [,]](_icc.gif)                                                     |
85 | | eqid 2412 |
. . . . . . . . 9
      ![[,] [,]](_icc.gif)          ![[,] [,]](_icc.gif)     |
86 | 74, 75, 76, 77, 78, 79, 80, 1, 81, 82, 83, 84, 85 | cvmliftlem8 24940 |
. . . . . . . 8
 
           ↾t       ![[,] [,]](_icc.gif)        |
87 | 73, 86 | mpdan 650 |
. . . . . . 7
       ↾t       ![[,] [,]](_icc.gif)        |
88 | | 1m1e0 10032 |
. . . . . . . . . . . 12
   |
89 | 88 | oveq1i 6058 |
. . . . . . . . . . 11
       |
90 | 1 | nncnd 9980 |
. . . . . . . . . . . 12
   |
91 | 1 | nnne0d 10008 |
. . . . . . . . . . . 12
   |
92 | 90, 91 | div0d 9753 |
. . . . . . . . . . 11
     |
93 | 89, 92 | syl5eq 2456 |
. . . . . . . . . 10
       |
94 | 93 | oveq1d 6063 |
. . . . . . . . 9
       ![[,] [,]](_icc.gif)      ![[,] [,]](_icc.gif)      |
95 | 94 | oveq2d 6064 |
. . . . . . . 8
 
↾t       ![[,] [,]](_icc.gif)     
↾t   ![[,] [,]](_icc.gif)       |
96 | 95 | oveq1d 6063 |
. . . . . . 7
   ↾t       ![[,] [,]](_icc.gif)        ↾t   ![[,] [,]](_icc.gif)        |
97 | 87, 96 | eleqtrd 2488 |
. . . . . 6
       ↾t   ![[,] [,]](_icc.gif)        |
98 | | simpr 448 |
. . . . . . . . . 10
 
           |
99 | 74, 75, 76, 77, 78, 79, 80, 1, 81, 82, 83, 84, 85 | cvmliftlem7 24939 |
. . . . . . . . . 10
 
                                    |
100 | 74, 75, 76, 77, 78, 79, 80, 1, 81, 82, 83, 84, 85, 98, 99 | cvmliftlem6 24938 |
. . . . . . . . 9
 
                  ![[,] [,]](_icc.gif)                   ![[,] [,]](_icc.gif)        |
101 | 73, 100 | mpdan 650 |
. . . . . . . 8
              ![[,] [,]](_icc.gif)                   ![[,] [,]](_icc.gif)        |
102 | 101 | simprd 450 |
. . . . . . 7
              ![[,] [,]](_icc.gif)       |
103 | 94 | reseq2d 5113 |
. . . . . . 7
        ![[,] [,]](_icc.gif)        ![[,] [,]](_icc.gif)       |
104 | 102, 103 | eqtrd 2444 |
. . . . . 6
          ![[,] [,]](_icc.gif)       |
105 | 97, 104 | jca 519 |
. . . . 5
       
↾t   ![[,] [,]](_icc.gif)      
        ![[,] [,]](_icc.gif)        |
106 | 105 | a1d 23 |
. . . 4
             ↾t   ![[,] [,]](_icc.gif)      
        ![[,] [,]](_icc.gif)         |
107 | | elnnuz 10486 |
. . . . . . . . . . 11

      |
108 | 107 | biimpi 187 |
. . . . . . . . . 10
       |
109 | 108 | adantl 453 |
. . . . . . . . 9
 

      |
110 | | peano2fzr 11033 |
. . . . . . . . . 10
            
      |
111 | 110 | ex 424 |
. . . . . . . . 9
    
              |
112 | 109, 111 | syl 16 |
. . . . . . . 8
 

              |
113 | 112 | imim1d 71 |
. . . . . . 7
 

                   ↾t   ![[,] [,]](_icc.gif)     
            
  ![[,] [,]](_icc.gif)                           ↾t   ![[,] [,]](_icc.gif)     
            
  ![[,] [,]](_icc.gif)          |
114 | | cvmliftlem10.1 |
. . . . . . . . . . 11
                      
↾t   ![[,] [,]](_icc.gif)      
              ![[,] [,]](_icc.gif)         |
115 | | eqid 2412 |
. . . . . . . . . . . . 13
  ↾t   ![[,] [,]](_icc.gif)        
↾t   ![[,] [,]](_icc.gif)        |
116 | | 0re 9055 |
. . . . . . . . . . . . . . 15
 |
117 | 114 | simplbi 447 |
. . . . . . . . . . . . . . . . . . . 20
           |
118 | 117 | adantl 453 |
. . . . . . . . . . . . . . . . . . 19
 
           |
119 | 118 | simprd 450 |
. . . . . . . . . . . . . . . . . 18
 
         |
120 | | elfznn 11044 |
. . . . . . . . . . . . . . . . . 18
           |
121 | 119, 120 | syl 16 |
. . . . . . . . . . . . . . . . 17
 
     |
122 | 121 | nnred 9979 |
. . . . . . . . . . . . . . . 16
 
     |
123 | 1 | adantr 452 |
. . . . . . . . . . . . . . . 16
 
   |
124 | 122, 123 | nndivred 10012 |
. . . . . . . . . . . . . . 15
 
       |
125 | | iccssre 10956 |
. . . . . . . . . . . . . . 15
         ![[,] [,]](_icc.gif)        |
126 | 116, 124,
125 | sylancr 645 |
. . . . . . . . . . . . . 14
 
   ![[,] [,]](_icc.gif)     
  |
127 | 117 | simpld 446 |
. . . . . . . . . . . . . . . . . . 19

  |
128 | 127 | adantl 453 |
. . . . . . . . . . . . . . . . . 18
 
   |
129 | 128 | nnred 9979 |
. . . . . . . . . . . . . . . . 17
 
   |
130 | 129, 123 | nndivred 10012 |
. . . . . . . . . . . . . . . 16
 
     |
131 | | icccld 18762 |
. . . . . . . . . . . . . . . 16
  
    ![[,] [,]](_icc.gif)              |
132 | 116, 130,
131 | sylancr 645 |
. . . . . . . . . . . . . . 15
 
   ![[,] [,]](_icc.gif)              |
133 | 83 | fveq2i 5698 |
. . . . . . . . . . . . . . 15
             |
134 | 132, 133 | syl6eleqr 2503 |
. . . . . . . . . . . . . 14
 
   ![[,] [,]](_icc.gif)          |
135 | | ssun1 3478 |
. . . . . . . . . . . . . . 15
  ![[,] [,]](_icc.gif)       ![[,] [,]](_icc.gif)        ![[,] [,]](_icc.gif)        |
136 | 116 | a1i 11 |
. . . . . . . . . . . . . . . 16
 
   |
137 | 128 | nnnn0d 10238 |
. . . . . . . . . . . . . . . . . . 19
 
   |
138 | 137 | nn0ge0d 10241 |
. . . . . . . . . . . . . . . . . 18
 

  |
139 | 123 | nnred 9979 |
. . . . . . . . . . . . . . . . . 18
 
   |
140 | 123 | nngt0d 10007 |
. . . . . . . . . . . . . . . . . 18
 
   |
141 | | divge0 9843 |
. . . . . . . . . . . . . . . . . 18
  
   
    |
142 | 129, 138,
139, 140, 141 | syl22anc 1185 |
. . . . . . . . . . . . . . . . 17
 

    |
143 | 129 | ltp1d 9905 |
. . . . . . . . . . . . . . . . . . 19
 
     |
144 | | ltdiv1 9838 |
. . . . . . . . . . . . . . . . . . . 20
  
 
 
            |
145 | 129, 122,
139, 140, 144 | syl112anc 1188 |
. . . . . . . . . . . . . . . . . . 19
 
     
       |
146 | 143, 145 | mpbid 202 |
. . . . . . . . . . . . . . . . . 18
 
  
      |
147 | 130, 124,
146 | ltled 9185 |
. . . . . . . . . . . . . . . . 17
 
  
      |
148 | | elicc2 10939 |
. . . . . . . . . . . . . . . . . 18
            ![[,] [,]](_icc.gif)          
          |
149 | 116, 124,
148 | sylancr 645 |
. . . . . . . . . . . . . . . . 17
 
      ![[,] [,]](_icc.gif)        
            |
150 | 130, 142,
147, 149 | mpbir3and 1137 |
. . . . . . . . . . . . . . . 16
 
     ![[,] [,]](_icc.gif)        |
151 | | iccsplit 10993 |
. . . . . . . . . . . . . . . 16
      
   ![[,] [,]](_icc.gif)         ![[,] [,]](_icc.gif)         ![[,] [,]](_icc.gif)        ![[,] [,]](_icc.gif)         |
152 | 136, 124,
150, 151 | syl3anc 1184 |
. . . . . . . . . . . . . . 15
 
   ![[,] [,]](_icc.gif)         ![[,] [,]](_icc.gif)        ![[,] [,]](_icc.gif)         |
153 | 135, 152 | syl5sseqr 3365 |
. . . . . . . . . . . . . 14
 
   ![[,] [,]](_icc.gif)   
  ![[,] [,]](_icc.gif)        |
154 | | uniretop 18757 |
. . . . . . . . . . . . . . . 16
      |
155 | 83 | unieqi 3993 |
. . . . . . . . . . . . . . . 16
       |
156 | 154, 155 | eqtr4i 2435 |
. . . . . . . . . . . . . . 15
  |
157 | 156 | restcldi 17199 |
. . . . . . . . . . . . . 14
    ![[,] [,]](_icc.gif)     
  ![[,] [,]](_icc.gif)       
  ![[,] [,]](_icc.gif)      ![[,] [,]](_icc.gif)         ![[,] [,]](_icc.gif)        ↾t   ![[,] [,]](_icc.gif)          |
158 | 126, 134,
153, 157 | syl3anc 1184 |
. . . . . . . . . . . . 13
 
   ![[,] [,]](_icc.gif)       
↾t   ![[,] [,]](_icc.gif)          |
159 | | icccld 18762 |
. . . . . . . . . . . . . . . 16
             ![[,] [,]](_icc.gif)                |
160 | 130, 124,
159 | syl2anc 643 |
. . . . . . . . . . . . . . 15
 
     ![[,] [,]](_icc.gif)                |
161 | 160, 133 | syl6eleqr 2503 |
. . . . . . . . . . . . . 14
 
     ![[,] [,]](_icc.gif)            |
162 | | ssun2 3479 |
. . . . . . . . . . . . . . 15
    ![[,] [,]](_icc.gif)         ![[,] [,]](_icc.gif)        ![[,] [,]](_icc.gif)        |
163 | 162, 152 | syl5sseqr 3365 |
. . . . . . . . . . . . . 14
 
     ![[,] [,]](_icc.gif)     
  ![[,] [,]](_icc.gif)        |
164 | 156 | restcldi 17199 |
. . . . . . . . . . . . . 14
    ![[,] [,]](_icc.gif)     
    ![[,] [,]](_icc.gif)         
    ![[,] [,]](_icc.gif)        ![[,] [,]](_icc.gif)           ![[,] [,]](_icc.gif)          ↾t   ![[,] [,]](_icc.gif)          |
165 | 126, 161,
163, 164 | syl3anc 1184 |
. . . . . . . . . . . . 13
 
     ![[,] [,]](_icc.gif)         
↾t   ![[,] [,]](_icc.gif)          |
166 | | retop 18756 |
. . . . . . . . . . . . . . . 16
     |
167 | 83, 166 | eqeltri 2482 |
. . . . . . . . . . . . . . 15
 |
168 | 156 | restuni 17188 |
. . . . . . . . . . . . . . 15
    ![[,] [,]](_icc.gif)     
   ![[,] [,]](_icc.gif)        ↾t   ![[,] [,]](_icc.gif)         |
169 | 167, 126,
168 | sylancr 645 |
. . . . . . . . . . . . . 14
 
   ![[,] [,]](_icc.gif)        ↾t   ![[,] [,]](_icc.gif)         |
170 | 152, 169 | eqtr3d 2446 |
. . . . . . . . . . . . 13
 
    ![[,] [,]](_icc.gif)        ![[,] [,]](_icc.gif)         ↾t   ![[,] [,]](_icc.gif)         |
171 | 114 | simprbi 451 |
. . . . . . . . . . . . . . . . . . . 20
             
↾t   ![[,] [,]](_icc.gif)      
              ![[,] [,]](_icc.gif)        |
172 | 171 | adantl 453 |
. . . . . . . . . . . . . . . . . . 19
 
             
↾t   ![[,] [,]](_icc.gif)      
              ![[,] [,]](_icc.gif)        |
173 | 172 | simpld 446 |
. . . . . . . . . . . . . . . . . 18
 
             ↾t   ![[,] [,]](_icc.gif)        |
174 | | eqid 2412 |
. . . . . . . . . . . . . . . . . . 19
  ↾t   ![[,] [,]](_icc.gif)      
↾t   ![[,] [,]](_icc.gif)      |
175 | 174, 75 | cnf 17272 |
. . . . . . . . . . . . . . . . . 18
 
           ↾t   ![[,] [,]](_icc.gif)                    ↾t   ![[,] [,]](_icc.gif)         |
176 | 173, 175 | syl 16 |
. . . . . . . . . . . . . . . . 17
 
               ↾t   ![[,] [,]](_icc.gif)         |
177 | | iccssre 10956 |
. . . . . . . . . . . . . . . . . . . 20
  
    ![[,] [,]](_icc.gif)      |
178 | 116, 130,
177 | sylancr 645 |
. . . . . . . . . . . . . . . . . . 19
 
   ![[,] [,]](_icc.gif)   
  |
179 | 156 | restuni 17188 |
. . . . . . . . . . . . . . . . . . 19
    ![[,] [,]](_icc.gif)   
   ![[,] [,]](_icc.gif)      ↾t   ![[,] [,]](_icc.gif)       |
180 | 167, 178,
179 | sylancr 645 |
. . . . . . . . . . . . . . . . . 18
 
   ![[,] [,]](_icc.gif)      ↾t   ![[,] [,]](_icc.gif)       |
181 | 180 | feq2d 5548 |
. . . . . . . . . . . . . . . . 17
 
                ![[,] [,]](_icc.gif)                    ↾t   ![[,] [,]](_icc.gif)          |
182 | 176, 181 | mpbird 224 |
. . . . . . . . . . . . . . . 16
 
               ![[,] [,]](_icc.gif)        |
183 | | eqid 2412 |
. . . . . . . . . . . . . . . . . . . 20
        ![[,] [,]](_icc.gif)              ![[,] [,]](_icc.gif)       |
184 | | simpr 448 |
. . . . . . . . . . . . . . . . . . . 20
 
               |
185 | 74, 75, 76, 77, 78, 79, 80, 1, 81, 82, 83, 84, 183 | cvmliftlem7 24939 |
. . . . . . . . . . . . . . . . . . . 20
 
                                            |
186 | 74, 75, 76, 77, 78, 79, 80, 1, 81, 82, 83, 84, 183, 184, 185 | cvmliftlem6 24938 |
. . . . . . . . . . . . . . . . . . 19
 
                        ![[,] [,]](_icc.gif)                         ![[,] [,]](_icc.gif)          |
187 | 119, 186 | syldan 457 |
. . . . . . . . . . . . . . . . . 18
 
     
            ![[,] [,]](_icc.gif)            
            ![[,] [,]](_icc.gif)          |
188 | 187 | simpld 446 |
. . . . . . . . . . . . . . . . 17
 
                 ![[,] [,]](_icc.gif)          |
189 | 128 | nncnd 9980 |
. . . . . . . . . . . . . . . . . . . . 21
 
   |
190 | | ax-1cn 9012 |
. . . . . . . . . . . . . . . . . . . . 21
 |
191 | | pncan 9275 |
. . . . . . . . . . . . . . . . . . . . 21
 
       |
192 | 189, 190,
191 | sylancl 644 |
. . . . . . . . . . . . . . . . . . . 20
 
       |
193 | 192 | oveq1d 6063 |
. . . . . . . . . . . . . . . . . . 19
 
           |
194 | 193 | oveq1d 6063 |
. . . . . . . . . . . . . . . . . 18
 
         ![[,] [,]](_icc.gif)          ![[,] [,]](_icc.gif)        |
195 | 194 | feq2d 5548 |
. . . . . . . . . . . . . . . . 17
 
     
            ![[,] [,]](_icc.gif)           
        ![[,] [,]](_icc.gif)           |
196 | 188, 195 | mpbid 202 |
. . . . . . . . . . . . . . . 16
 
             ![[,] [,]](_icc.gif)          |
197 | | ffun 5560 |
. . . . . . . . . . . . . . . . . . . . . . 23
 
             ![[,] [,]](_icc.gif)                  |
198 | 182, 197 | syl 16 |
. . . . . . . . . . . . . . . . . . . . . 22
 
             |
199 | 128, 108 | syl 16 |
. . . . . . . . . . . . . . . . . . . . . . . 24
 
       |
200 | | eluzfz2 11029 |
. . . . . . . . . . . . . . . . . . . . . . . 24
    
      |
201 | 199, 200 | syl 16 |
. . . . . . . . . . . . . . . . . . . . . . 23
 
       |
202 | | fveq2 5695 |
. . . . . . . . . . . . . . . . . . . . . . . 24
           |
203 | 202 | ssiun2s 4103 |
. . . . . . . . . . . . . . . . . . . . . . 23
                     |
204 | 201, 203 | syl 16 |
. . . . . . . . . . . . . . . . . . . . . 22
 
    
            |
205 | | peano2rem 9331 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
     |
206 | 129, 205 | syl 16 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
 
     |
207 | 206, 123 | nndivred 10012 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
 
       |
208 | 207 | rexrd 9098 |
. . . . . . . . . . . . . . . . . . . . . . . 24
 
       |
209 | 130 | rexrd 9098 |
. . . . . . . . . . . . . . . . . . . . . . . 24
 
     |
210 | 129 | ltm1d 9907 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
 
     |
211 | | ltdiv1 9838 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
   

              |
212 | 206, 129,
139, 140, 211 | syl112anc 1188 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
 
             |
213 | 210, 212 | mpbid 202 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
 
    
    |
214 | 207, 130,
213 | ltled 9185 |
. . . . . . . . . . . . . . . . . . . . . . . 24
 
    
    |
215 | | ubicc2 10978 |
. . . . . . . . . . . . . . . . . . . . . . . 24
       
               ![[,] [,]](_icc.gif)      |
216 | 208, 209,
214, 215 | syl3anc 1184 |
. . . . . . . . . . . . . . . . . . . . . . 23
 
         ![[,] [,]](_icc.gif)      |
217 | 199, 119,
110 | syl2anc 643 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
 
       |
218 | | eqid 2412 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
      ![[,] [,]](_icc.gif)          ![[,] [,]](_icc.gif)     |
219 | | simpr 448 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
 
           |
220 | 74, 75, 76, 77, 78, 79, 80, 1, 81, 82, 83, 84, 218 | cvmliftlem7 24939 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
 
                                    |
221 | 74, 75, 76, 77, 78, 79, 80, 1, 81, 82, 83, 84, 218, 219, 220 | cvmliftlem6 24938 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
 
                  ![[,] [,]](_icc.gif)                   ![[,] [,]](_icc.gif)        |
222 | 217, 221 | syldan 457 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
 
              ![[,] [,]](_icc.gif)                   ![[,] [,]](_icc.gif)        |
223 | 222 | simpld 446 |
. . . . . . . . . . . . . . . . . . . . . . . 24
 
             ![[,] [,]](_icc.gif)        |
224 | | fdm 5562 |
. . . . . . . . . . . . . . . . . . . . . . . 24
             ![[,] [,]](_icc.gif)                ![[,] [,]](_icc.gif)      |
225 | 223, 224 | syl 16 |
. . . . . . . . . . . . . . . . . . . . . . 23
 
           ![[,] [,]](_icc.gif)      |
226 | 216, 225 | eleqtrrd 2489 |
. . . . . . . . . . . . . . . . . . . . . 22
 
         |
227 | | funssfv 5713 |
. . . . . . . . . . . . . . . . . . . . . 22
           
                                                 |
228 | 198, 204,
226, 227 | syl3anc 1184 |
. . . . . . . . . . . . . . . . . . . . 21
 
                             |
229 | 192 | fveq2d 5699 |
. . . . . . . . . . . . . . . . . . . . . 22
 
               |
230 | 229, 193 | fveq12d 5701 |
. . . . . . . . . . . . . . . . . . . . 21
 
                               |
231 | 74, 75, 76, 77, 78, 79, 80, 1, 81, 82, 83, 84 | cvmliftlem9 24941 |
. . . . . . . . . . . . . . . . . . . . . . 23
 
                                           |
232 | 119, 231 | syldan 457 |
. . . . . . . . . . . . . . . . . . . . . 22
 
     
                               |
233 | 193 | fveq2d 5699 |
. . . . . . . . . . . . . . . . . . . . . 22
 
     
                         |
234 | 232, 233 | eqtr3d 2446 |
. . . . . . . . . . . . . . . . . . . . 21
 
                                 |
235 | 228, 230,
234 | 3eqtr2d 2450 |
. . . . . . . . . . . . . . . . . . . 20
 
                               |
236 | 235 | opeq2d 3959 |
. . . . . . . . . . . . . . . . . . 19
 
      
                                  |
237 | 236 | sneqd 3795 |
. . . . . . . . . . . . . . . . . 18
 
                       
              
      |
238 | | ffn 5558 |
. . . . . . . . . . . . . . . . . . . 20
 
             ![[,] [,]](_icc.gif)      
           ![[,] [,]](_icc.gif)      |
239 | 182, 238 | syl 16 |
. . . . . . . . . . . . . . . . . . 19
 
             ![[,] [,]](_icc.gif)      |
240 | | 0xr 9095 |
. . . . . . . . . . . . . . . . . . . . 21
 |
241 | 240 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
 
   |
242 | | ubicc2 10978 |
. . . . . . . . . . . . . . . . . . . 20
   
       ![[,] [,]](_icc.gif)      |
243 | 241, 209,
142, 242 | syl3anc 1184 |
. . . . . . . . . . . . . . . . . . 19
 
     ![[,] [,]](_icc.gif)      |
244 | | fnressn 5885 |
. . . . . . . . . . . . . . . . . . 19
              ![[,] [,]](_icc.gif)    
   ![[,] [,]](_icc.gif)                           
                  |
245 | 239, 243,
244 | syl2anc 643 |
. . . . . . . . . . . . . . . . . 18
 
                       
                  |
246 | | ffn 5558 |
. . . . . . . . . . . . . . . . . . . 20
             ![[,] [,]](_icc.gif)                  ![[,] [,]](_icc.gif)        |
247 | 196, 246 | syl 16 |
. . . . . . . . . . . . . . . . . . 19
 
           ![[,] [,]](_icc.gif)        |
248 | 124 | rexrd 9098 |
. . . . . . . . . . . . . . . . . . . 20
 
       |
249 | | lbicc2 10977 |
. . . . . . . . . . . . . . . . . . . 20
       
             ![[,] [,]](_icc.gif)        |
250 | 209, 248,
147, 249 | syl3anc 1184 |
. . . . . . . . . . . . . . . . . . 19
 
       ![[,] [,]](_icc.gif)        |
251 | | fnressn 5885 |
. . . . . . . . . . . . . . . . . . 19
            ![[,] [,]](_icc.gif)      
     ![[,] [,]](_icc.gif)                                 
      |
252 | 247, 250,
251 | syl2anc 643 |
. . . . . . . . . . . . . . . . . 18
 
     
                            |
253 | 237, 245,
252 | 3eqtr4d 2454 |
. . . . . . . . . . . . . . . . 17
 
                       
       |
254 | | df-icc 10887 |
. . . . . . . . . . . . . . . . . . . . 21




    |
255 | | xrmaxle 10735 |
. . . . . . . . . . . . . . . . . . . . 21
   
          
       |
256 | | xrlemin 10736 |
. . . . . . . . . . . . . . . . . . . . 21
   
     
   
                        |
257 | 254, 255,
256 | ixxin 10897 |
. . . . . . . . . . . . . . . . . . . 20
              
   ![[,] [,]](_icc.gif)        ![[,] [,]](_icc.gif)                  ![[,] [,]](_icc.gif)                     |
258 | 241, 209,
209, 248, 257 | syl22anc 1185 |
. . . . . . . . . . . . . . . . . . 19
 
    ![[,] [,]](_icc.gif)        ![[,] [,]](_icc.gif)                  ![[,] [,]](_icc.gif)    
                |
259 | | iftrue 3713 |
. . . . . . . . . . . . . . . . . . . . 21
                |
260 | 142, 259 | syl 16 |
. . . . . . . . . . . . . . . . . . . 20
 
              |
261 | | iftrue 3713 |
. . . . . . . . . . . . . . . . . . . . 21
                            |
262 | 147, 261 | syl 16 |
. . . . . . . . . . . . . . . . . . . 20
 
                      |
263 | 260, 262 | oveq12d 6066 |
. . . . . . . . . . . . . . . . . . 19
 
            ![[,] [,]](_icc.gif)                       ![[,] [,]](_icc.gif)      |
264 | | iccid 10925 |
. . . . . . . . . . . . . . . . . . . 20
  
    ![[,] [,]](_icc.gif)          |
265 | 209, 264 | syl 16 |
. . . . . . . . . . . . . . . . . . 19
 
     ![[,] [,]](_icc.gif)          |
266 | 258, 263,
265 | 3eqtrd 2448 |
. . . . . . . . . . . . . . . . . 18
 
    ![[,] [,]](_icc.gif)        ![[,] [,]](_icc.gif)             |
267 | 266 | reseq2d 5113 |
. . . . . . . . . . . . . . . . 17
 
               ![[,] [,]](_icc.gif)        ![[,] [,]](_icc.gif)         
                |
268 | 266 | reseq2d 5113 |
. . . . . . . . . . . . . . . . 17
 
     
     ![[,] [,]](_icc.gif)        ![[,] [,]](_icc.gif)                      |
269 | 253, 267,
268 | 3eqtr4d 2454 |
. . . . . . . . . . . . . . . 16
 
               ![[,] [,]](_icc.gif)        ![[,] [,]](_icc.gif)                  ![[,] [,]](_icc.gif)        ![[,] [,]](_icc.gif)          |
270 | | fresaun 5581 |
. . . . . . . . . . . . . . . 16
                ![[,] [,]](_icc.gif)         
        ![[,] [,]](_icc.gif)         
            ![[,] [,]](_icc.gif)        ![[,] [,]](_icc.gif)              
   ![[,] [,]](_icc.gif)        ![[,] [,]](_icc.gif)        
 
            
        ![[,] [,]](_icc.gif)        ![[,] [,]](_icc.gif)           |
271 | 182, 196,
269, 270 | syl3anc 1184 |
. . . . . . . . . . . . . . 15
 
                        ![[,] [,]](_icc.gif)        ![[,] [,]](_icc.gif)           |
272 | | fzsuc 11060 |
. . . . . . . . . . . . . . . . . . 19
    
                  |
273 | 199, 272 | syl 16 |
. . . . . . . . . . . . . . . . . 18
 
                   |
274 | 273 | iuneq1d 4084 |
. . . . . . . . . . . . . . . . 17
 
                               |
275 | | iunxun 4140 |
. . . . . . . . . . . . . . . . . 18
                           
          |
276 | | ovex 6073 |
. . . . . . . . . . . . . . . . . . . 20
   |
277 | | fveq2 5695 |
. . . . . . . . . . . . . . . . . . . 20
          
    |
278 | 276, 277 | iunxsn 4138 |
. . . . . . . . . . . . . . . . . . 19
            
   |
279 | 278 | uneq2i 3466 |
. . . . . . . . . . . . . . . . . 18
 
                    
            
    |
280 | 275, 279 | eqtri 2432 |
. . . . . . . . . . . . . . . . 17
                                   |
281 | 274, 280 | syl6req 2461 |
. . . . . . . . . . . . . . . 16
 
                                 |
282 | 281 | feq1d 5547 |
. . . . . . . . . . . . . . 15
 
                         ![[,] [,]](_icc.gif)        ![[,] [,]](_icc.gif)         
                ![[,] [,]](_icc.gif)        ![[,] [,]](_icc.gif)            |
283 | 271, 282 | mpbid 202 |
. . . . . . . . . . . . . 14
 
                  ![[,] [,]](_icc.gif)        ![[,] [,]](_icc.gif)           |
284 | 170 | feq2d 5548 |
. . . . . . . . . . . . . 14
 
                   ![[,] [,]](_icc.gif)        ![[,] [,]](_icc.gif)                         ↾t   ![[,] [,]](_icc.gif)            |
285 | 283, 284 | mpbid 202 |
. . . . . . . . . . . . 13
 
                 ↾t   ![[,] [,]](_icc.gif)           |
286 | 281 | reseq1d 5112 |
. . . . . . . . . . . . . . 15
 
                   
  ![[,] [,]](_icc.gif)                    ![[,] [,]](_icc.gif)       |
287 | | fresaunres1 5583 |
. . . . . . . . . . . . . . . 16
                ![[,] [,]](_icc.gif)         
        ![[,] [,]](_icc.gif)         
            ![[,] [,]](_icc.gif)        ![[,] [,]](_icc.gif)              
   ![[,] [,]](_icc.gif)        ![[,] [,]](_icc.gif)        
  
            
     ![[,] [,]](_icc.gif)     
           |
288 | 182, 196,
269, 287 | syl3anc 1184 |
. . . . . . . . . . . . . . 15
 
                   
  ![[,] [,]](_icc.gif)                 |
289 | 286, 288 | eqtr3d 2446 |
. . . . . . . . . . . . . 14
 
                ![[,] [,]](_icc.gif)                 |
290 | 167 | a1i 11 |
. . . . . . . . . . . . . . . 16
 
   |
291 | | ovex 6073 |
. . . . . . . . . . . . . . . . 17
  ![[,] [,]](_icc.gif)       |
292 | 291 | a1i 11 |
. . . . . . . . . . . . . . . 16
 
   ![[,] [,]](_icc.gif)        |
293 | | restabs 17191 |
. . . . . . . . . . . . . . . 16
    ![[,] [,]](_icc.gif)   
  ![[,] [,]](_icc.gif)        ![[,] [,]](_icc.gif)         ↾t   ![[,] [,]](_icc.gif)       ↾t   ![[,] [,]](_icc.gif)      ↾t   ![[,] [,]](_icc.gif)       |
294 | 290, 153,
292, 293 | syl3anc 1184 |
. . . . . . . . . . . . . . 15
 
   ↾t   ![[,] [,]](_icc.gif)       ↾t   ![[,] [,]](_icc.gif)      ↾t   ![[,] [,]](_icc.gif)       |
295 | 294 | oveq1d 6063 |
. . . . . . . . . . . . . 14
 
    ↾t   ![[,] [,]](_icc.gif)       ↾t   ![[,] [,]](_icc.gif)        ↾t   ![[,] [,]](_icc.gif)        |
296 | 173, 289,
295 | 3eltr4d 2493 |
. . . . . . . . . . . . 13
 
                ![[,] [,]](_icc.gif)       
↾t   ![[,] [,]](_icc.gif)       ↾t   ![[,] [,]](_icc.gif)        |
297 | 74, 75, 76, 77, 78, 79, 80, 1, 81, 82, 83, 84, 183 | cvmliftlem8 24940 |
. . . . . . . . . . . . . . . 16
 
               ↾t         ![[,] [,]](_icc.gif)          |
298 | 119, 297 | syldan 457 |
. . . . . . . . . . . . . . 15
 
         ↾t         ![[,] [,]](_icc.gif)          |
299 | 194 | oveq2d 6064 |
. . . . . . . . . . . . . . . 16
 
 
↾t         ![[,] [,]](_icc.gif)       
↾t     ![[,] [,]](_icc.gif)         |
300 | 299 | oveq1d 6063 |
. . . . . . . . . . . . . . 15
 
   ↾t         ![[,] [,]](_icc.gif)          ↾t     ![[,] [,]](_icc.gif)          |
301 | 298, 300 | eleqtrd 2488 |
. . . . . . . . . . . . . 14
 
         ↾t     ![[,] [,]](_icc.gif)          |
302 | 281 | reseq1d 5112 |
. . . . . . . . . . . . . . 15
 
                   
    ![[,] [,]](_icc.gif)                        ![[,] [,]](_icc.gif)         |
303 | | fresaunres2 5582 |
. . . . . . . . . . . . . . . 16
                ![[,] [,]](_icc.gif)         
        ![[,] [,]](_icc.gif)         
            ![[,] [,]](_icc.gif)        ![[,] [,]](_icc.gif)              
   ![[,] [,]](_icc.gif)        ![[,] [,]](_icc.gif)        
  
            
       ![[,] [,]](_icc.gif)               |
304 | 182, 196,
269, 303 | syl3anc 1184 |
. . . . . . . . . . . . . . 15
 
                   
    ![[,] [,]](_icc.gif)          
    |
305 | 302, 304 | eqtr3d 2446 |
. . . . . . . . . . . . . 14
 
                  ![[,] [,]](_icc.gif)               |
306 | | restabs 17191 |
. . . . . . . . . . . . . . . 16
      ![[,] [,]](_icc.gif)     
  ![[,] [,]](_icc.gif)        ![[,] [,]](_icc.gif)         ↾t   ![[,] [,]](_icc.gif)       ↾t     ![[,] [,]](_icc.gif)        ↾t     ![[,] [,]](_icc.gif)         |
307 | 290, 163,
292, 306 | syl3anc 1184 |
. . . . . . . . . . . . . . 15
 
   ↾t   ![[,] [,]](_icc.gif)       ↾t     ![[,] [,]](_icc.gif)        ↾t     ![[,] [,]](_icc.gif)         |
308 | 307 | oveq1d 6063 |
. . . . . . . . . . . . . 14
 
    ↾t   ![[,] [,]](_icc.gif)       ↾t     ![[,] [,]](_icc.gif)          ↾t     ![[,] [,]](_icc.gif)          |
309 | 301, 305,
308 | 3eltr4d 2493 |
. . . . . . . . . . . . 13
 
                  ![[,] [,]](_icc.gif)         
↾t   ![[,] [,]](_icc.gif)       ↾t     ![[,] [,]](_icc.gif)          |
310 | 115, 75, 158, 165, 170, 285, 296, 309 | paste 17320 |
. . . . . . . . . . . 12
 
               ↾t   ![[,] [,]](_icc.gif)          |
311 | 152 | reseq2d 5113 |
. . . . . . . . . . . . 13
 
    ![[,] [,]](_icc.gif)           ![[,] [,]](_icc.gif)        ![[,] [,]](_icc.gif)          |
312 | 172 | simprd 450 |
. . . . . . . . . . . . . . 15
 
  
             ![[,] [,]](_icc.gif)       |
313 | 187 | simprd 450 |
. . . . . . . . . . . . . . . 16
 
                  ![[,] [,]](_icc.gif)         |
314 | 194 | reseq2d 5113 |
. . . . . . . . . . . . . . . 16
 
          ![[,] [,]](_icc.gif)            ![[,] [,]](_icc.gif)         |
315 | 313, 314 | eqtrd 2444 |
. . . . . . . . . . . . . . 15
 
              ![[,] [,]](_icc.gif)         |
316 | 312, 315 | uneq12d 3470 |
. . . . . . . . . . . . . 14
 
                  
        ![[,] [,]](_icc.gif)          ![[,] [,]](_icc.gif)          |
317 | | coundi 5338 |
. . . . . . . . . . . . . 14
                      
              
     |
318 | | resundi 5127 |
. . . . . . . . . . . . . 14
    ![[,] [,]](_icc.gif)        ![[,] [,]](_icc.gif)            ![[,] [,]](_icc.gif)          ![[,] [,]](_icc.gif)         |
319 | 316, 317,
318 | 3eqtr4g 2469 |
. . . . . . . . . . . . 13
 
   
            
        ![[,] [,]](_icc.gif)        ![[,] [,]](_icc.gif)          |
320 | 281 | coeq2d 5002 |
. . . . . . . . . . . . 13
 
   
            
                    |
321 | 311, 319,
320 | 3eqtr2rd 2451 |
. . . . . . . . . . . 12
 
  
               ![[,] [,]](_icc.gif)         |
322 | 310, 321 | jca 519 |
. . . . . . . . . . 11
 
               
↾t   ![[,] [,]](_icc.gif)        
                ![[,] [,]](_icc.gif)          |
323 | 114, 322 | sylan2br 463 |
. . . . . . . . . 10
 
  
                  
↾t   ![[,] [,]](_icc.gif)      
              ![[,] [,]](_icc.gif)                      
↾t   ![[,] [,]](_icc.gif)        
                ![[,] [,]](_icc.gif)          |
324 | 323 | expr 599 |
. . . . . . . . 9
 
                      
↾t   ![[,] [,]](_icc.gif)      
              ![[,] [,]](_icc.gif)       
             ↾t   ![[,] [,]](_icc.gif)                         ![[,] [,]](_icc.gif)           |
325 | 324 | expr 599 |
. . . . . . . 8
 

                     ↾t   ![[,] [,]](_icc.gif)     
            
  ![[,] [,]](_icc.gif)     
 
             ↾t   ![[,] [,]](_icc.gif)                         ![[,] [,]](_icc.gif)            |
326 | 325 | a2d 24 |
. . . . . . 7
 

                    |