Step | Hyp | Ref
| Expression |
1 | | 2re 10495 |
. . . . . . . 8
 |
2 | | 3re 10499 |
. . . . . . . 8
 |
3 | | 2lt3 10593 |
. . . . . . . 8
 |
4 | 1, 2, 3 | ltleii 9601 |
. . . . . . 7
 |
5 | | 2z 10782 |
. . . . . . . 8
 |
6 | | 3z 10783 |
. . . . . . . 8
 |
7 | | eluz 10978 |
. . . . . . . 8
 
     
   |
8 | 5, 6, 7 | mp2an 672 |
. . . . . . 7
       |
9 | 4, 8 | mpbir 209 |
. . . . . 6
     |
10 | | uzss 10985 |
. . . . . 6
    
          |
11 | 9, 10 | ax-mp 5 |
. . . . 5
         |
12 | 11 | sseli 3453 |
. . . 4
    
      |
13 | | 0re 9490 |
. . . . 5
 |
14 | 13, 13 | axlowdimlem5 23337 |
. . . 4
    
                         |
15 | 12, 14 | syl 16 |
. . 3
    
                         |
16 | | 1re 9489 |
. . . . 5
 |
17 | 16, 13 | axlowdimlem5 23337 |
. . . 4
    
                         |
18 | 12, 17 | syl 16 |
. . 3
    
                         |
19 | 13, 16 | axlowdimlem5 23337 |
. . . 4
    
                         |
20 | 12, 19 | syl 16 |
. . 3
    
                         |
21 | | eqid 2451 |
. . . 4
                                            
                        
  
     
                                  |
22 | 21 | axlowdimlem15 23347 |
. . 3
    
    
                                 
     
                           |
23 | | eqid 2451 |
. . . . . 6
                                         |
24 | | eqid 2451 |
. . . . . 6
       
     
                                 |
25 | | eqid 2451 |
. . . . . 6
     
                    
            |
26 | 23, 24, 25, 13, 13 | axlowdimlem17 23349 |
. . . . 5
         
                              
              Cgr                              
                |
27 | | eqid 2451 |
. . . . . 6
     
                    
            |
28 | 23, 24, 27, 16, 13 | axlowdimlem17 23349 |
. . . . 5
         
                              
              Cgr                              
                |
29 | | eqid 2451 |
. . . . . 6
     
                    
            |
30 | 23, 24, 29, 13, 16 | axlowdimlem17 23349 |
. . . . 5
         
                              
              Cgr                              
                |
31 | | 1z 10780 |
. . . . . . . . . . . . . . 15
 |
32 | 31 | a1i 11 |
. . . . . . . . . . . . . 14
 
   |
33 | | peano2zm 10792 |
. . . . . . . . . . . . . . 15
 
   |
34 | 33 | 3ad2ant2 1010 |
. . . . . . . . . . . . . 14
 
 
   |
35 | | 2m1e1 10540 |
. . . . . . . . . . . . . . 15
   |
36 | | zre 10754 |
. . . . . . . . . . . . . . . . . . . 20
   |
37 | | letr 9572 |
. . . . . . . . . . . . . . . . . . . . 21
 
  
    |
38 | 1, 2, 37 | mp3an12 1305 |
. . . . . . . . . . . . . . . . . . . 20
  
    |
39 | 36, 38 | syl 16 |
. . . . . . . . . . . . . . . . . . 19
  
    |
40 | 4, 39 | mpani 676 |
. . . . . . . . . . . . . . . . . 18
 
   |
41 | 40 | imp 429 |
. . . . . . . . . . . . . . . . 17
  
  |
42 | 41 | 3adant1 1006 |
. . . . . . . . . . . . . . . 16
 
   |
43 | 36 | 3ad2ant2 1010 |
. . . . . . . . . . . . . . . . 17
 
   |
44 | | lesub1 9937 |
. . . . . . . . . . . . . . . . . 18
 
 
       |
45 | 1, 16, 44 | mp3an13 1306 |
. . . . . . . . . . . . . . . . 17
 
       |
46 | 43, 45 | syl 16 |
. . . . . . . . . . . . . . . 16
 
 
       |
47 | 42, 46 | mpbid 210 |
. . . . . . . . . . . . . . 15
 
       |
48 | 35, 47 | syl5eqbrr 4427 |
. . . . . . . . . . . . . 14
 
     |
49 | 32, 34, 48 | 3jca 1168 |
. . . . . . . . . . . . 13
 
  
      |
50 | | eluz2 10971 |
. . . . . . . . . . . . 13
         |
51 | | eluz2 10971 |
. . . . . . . . . . . . 13
               |
52 | 49, 50, 51 | 3imtr4i 266 |
. . . . . . . . . . . 12
    
        |
53 | | eluzfz1 11568 |
. . . . . . . . . . . 12
      
   
    |
54 | 52, 53 | syl 16 |
. . . . . . . . . . 11
    
   
    |
55 | 54 | adantr 465 |
. . . . . . . . . 10
         
      
    |
56 | | eqeq1 2455 |
. . . . . . . . . . . 12
     |
57 | | oveq1 6200 |
. . . . . . . . . . . . . . 15
       |
58 | 57 | opeq1d 4166 |
. . . . . . . . . . . . . 14
             |
59 | 58 | sneqd 3990 |
. . . . . . . . . . . . 13
                 |
60 | 57 | sneqd 3990 |
. . . . . . . . . . . . . . 15
           |
61 | 60 | difeq2d 3575 |
. . . . . . . . . . . . . 14
     
         
       |
62 | 61 | xpeq1d 4964 |
. . . . . . . . . . . . 13
                               |
63 | 59, 62 | uneq12d 3612 |
. . . . . . . . . . . 12
              
                                  |
64 | 56, 63 | ifbieq2d 3915 |
. . . . . . . . . . 11
       
  
     
                                                               
     
            |
65 | | snex 4634 |
. . . . . . . . . . . . 13
  
  
 |
66 | | ovex 6218 |
. . . . . . . . . . . . . . 15
     |
67 | | difexg 4541 |
. . . . . . . . . . . . . . 15
         
     |
68 | 66, 67 | ax-mp 5 |
. . . . . . . . . . . . . 14
         |
69 | | snex 4634 |
. . . . . . . . . . . . . 14
   |
70 | 68, 69 | xpex 6611 |
. . . . . . . . . . . . 13
     
       |
71 | 65, 70 | unex 6481 |
. . . . . . . . . . . 12
                     |
72 | | snex 4634 |
. . . . . . . . . . . . 13
        |
73 | | difexg 4541 |
. . . . . . . . . . . . . . 15
         
       |
74 | 66, 73 | ax-mp 5 |
. . . . . . . . . . . . . 14
           |
75 | 74, 69 | xpex 6611 |
. . . . . . . . . . . . 13
     
         |
76 | 72, 75 | unex 6481 |
. . . . . . . . . . . 12
       
     
          |
77 | 71, 76 | ifex 3959 |
. . . . . . . . . . 11
                                     
           |
78 | 64, 21, 77 | fvmpt 5876 |
. . . . . . . . . 10
                                              
     
                                                   
            |
79 | 55, 78 | syl 16 |
. . . . . . . . 9
         
                                          
     
                                                   
            |
80 | | eqid 2451 |
. . . . . . . . . 10
 |
81 | 80 | iftruei 3899 |
. . . . . . . . 9
                                     
                               |
82 | 79, 81 | syl6eq 2508 |
. . . . . . . 8
         
                                          
     
                                    |
83 | 82 | opeq1d 4166 |
. . . . . . 7
         
                                           
     
                    
                  
  
     
           
                  |
84 | | 2nn 10583 |
. . . . . . . . . . . . . 14
 |
85 | | nnuz 11000 |
. . . . . . . . . . . . . 14
     |
86 | 84, 85 | eleqtri 2537 |
. . . . . . . . . . . . 13
     |
87 | | fzss1 11607 |
. . . . . . . . . . . . 13
    
         
    |
88 | 86, 87 | ax-mp 5 |
. . . . . . . . . . . 12
         
   |
89 | 88 | sseli 3453 |
. . . . . . . . . . 11
          
    |
90 | 89 | adantl 466 |
. . . . . . . . . 10
         
      
    |
91 | | eqeq1 2455 |
. . . . . . . . . . . 12
     |
92 | | oveq1 6200 |
. . . . . . . . . . . . . . 15
       |
93 | 92 | opeq1d 4166 |
. . . . . . . . . . . . . 14
             |
94 | 93 | sneqd 3990 |
. . . . . . . . . . . . 13
                 |
95 | 92 | sneqd 3990 |
. . . . . . . . . . . . . . 15
           |
96 | 95 | difeq2d 3575 |
. . . . . . . . . . . . . 14
     
         
       |
97 | 96 | xpeq1d 4964 |
. . . . . . . . . . . . 13
                               |
98 | 94, 97 | uneq12d 3612 |
. . . . . . . . . . . 12
              
                                  |
99 | 91, 98 | ifbieq2d 3915 |
. . . . . . . . . . 11
       
  
     
                                                               
     
            |
100 | | snex 4634 |
. . . . . . . . . . . . 13
        |
101 | | difexg 4541 |
. . . . . . . . . . . . . . 15
         
       |
102 | 66, 101 | ax-mp 5 |
. . . . . . . . . . . . . 14
           |
103 | 102, 69 | xpex 6611 |
. . . . . . . . . . . . 13
     
         |
104 | 100, 103 | unex 6481 |
. . . . . . . . . . . 12
       
     
          |
105 | 71, 104 | ifex 3959 |
. . . . . . . . . . 11
                                     
           |
106 | 99, 21, 105 | fvmpt 5876 |
. . . . . . . . . 10
                                              
     
                                                   
            |
107 | 90, 106 | syl 16 |
. . . . . . . . 9
         
                                          
     
                                                   
            |
108 | | 1lt2 10592 |
. . . . . . . . . . . . . . . 16
 |
109 | 16, 1 | ltnlei 9599 |
. . . . . . . . . . . . . . . 16

  |
110 | 108, 109 | mpbi 208 |
. . . . . . . . . . . . . . 15
 |
111 | 110 | intnanr 906 |
. . . . . . . . . . . . . 14

    |
112 | | eluzelz 10974 |
. . . . . . . . . . . . . . . 16
    
  |
113 | 112, 33 | syl 16 |
. . . . . . . . . . . . . . 15
    
    |
114 | | elfz 11553 |
. . . . . . . . . . . . . . . 16
 

         
      |
115 | 31, 5, 114 | mp3an12 1305 |
. . . . . . . . . . . . . . 15
         
       |
116 | 113, 115 | syl 16 |
. . . . . . . . . . . . . 14
    
      
       |
117 | 111, 116 | mtbiri 303 |
. . . . . . . . . . . . 13
    
   
    |
118 | | eleq1 2523 |
. . . . . . . . . . . . . 14
       
   
     |
119 | 118 | notbid 294 |
. . . . . . . . . . . . 13
 
     
   
     |
120 | 117, 119 | syl5ibrcom 222 |
. . . . . . . . . . . 12
    

         |
121 | 120 | con2d 115 |
. . . . . . . . . . 11
    
    
 
   |
122 | 121 | imp 429 |
. . . . . . . . . 10
         
  
  |
123 | | iffalse 3900 |
. . . . . . . . . 10
       
  
     
                                                         |
124 | 122, 123 | syl 16 |
. . . . . . . . 9
         
         
  
     
                                                         |
125 | 107, 124 | eqtrd 2492 |
. . . . . . . 8
         
                                          
     
                     
     
           |
126 | 125 | opeq1d 4166 |
. . . . . . 7
         
                                           
     
                    
                                            
                |
127 | 83, 126 | breq12d 4406 |
. . . . . 6
         
          
                                 
     
                    
              Cgr      
                                 
     
                    
                                         
              Cgr                              
                 |
128 | 82 | opeq1d 4166 |
. . . . . . 7
         
                                           
     
                    
                  
  
     
           
                  |
129 | 125 | opeq1d 4166 |
. . . . . . 7
         
                                           
     
                    
                                            
                |
130 | 128, 129 | breq12d 4406 |
. . . . . 6
         
          
                                 
     
                    
              Cgr      
                                 
     
                    
                                         
              Cgr                              
                 |
131 | 54, 78 | syl 16 |
. . . . . . . . . 10
    
              
  
     
                                                                   
     
            |
132 | 131, 81 | syl6eq 2508 |
. . . . . . . . 9
    
              
  
     
                                                          |
133 | 132 | opeq1d 4166 |
. . . . . . . 8
    
               
  
     
                                            
           
                           
                |
134 | 133 | adantr 465 |
. . . . . . 7
         
                                           
     
                    
                  
  
     
           
                  |
135 | 125 | opeq1d 4166 |
. . . . . . 7
         
                                           
     
                    
                                            
                |
136 | 134, 135 | breq12d 4406 |
. . . . . 6
         
          
                                 
     
                    
              Cgr      
                                 
     
                    
                                         
              Cgr                              
                 |
137 | 127, 130,
136 | 3anbi123d 1290 |
. . . . 5
         
                                                   
                    
              Cgr      
                                 
     
                    
                                                            
                    
              Cgr      
                                 
     
                    
                                                            
                    
              Cgr      
                                 
     
                    
                                           
              Cgr                              
                  
  
     
           
                Cgr              
             
                                           
              Cgr                              
                  |
138 | 26, 28, 30, 137 | mpbir3and 1171 |
. . . 4
         
          
                                 
     
                    
              Cgr      
                                 
     
                    
                                                            
                    
              Cgr      
                                 
     
                    
                                                            
                    
              Cgr      
                                 
     
                    
                 |
139 | 138 | ralrimiva 2825 |
. . 3
    
    
                                            
     
                    
              Cgr      
                                 
     
                    
                                                            
                    
              Cgr      
                                 
     
                    
                                                            
                    
              Cgr      
                                 
     
                    
                 |
140 | 25, 27, 29 | axlowdimlem6 23338 |
. . . 4
    
        
          
      
                     
           
     
                     
                 
                     
          
      
                     
               |
141 | 12, 140 | syl 16 |
. . 3
    
        
          
      
                     
           
     
                     
                 
                     
          
      
                     
               |
142 | | opeq2 4161 |
. . . . . . . 8
    
                                                       
     
                      
                                 
     
                    
                |
143 | | opeq2 4161 |
. . . . . . . 8
    
                                                       
     
                      
                                 
     
                    
                |
144 | 142, 143 | breq12d 4406 |
. . . . . . 7
    
                      
                                 
     
                Cgr      
                                 
     
                                                        
     
                    
              Cgr      
                                 
     
                    
                 |
145 | 144 | 3anbi1d 1294 |
. . . . . 6
    
                                                               
                Cgr      
                                 
     
                      
                                 
     
                Cgr      
                                 
     
                                                              
                Cgr      
                                 
     
                                                          
     
                    
              Cgr      
                                 
     
                    
                                                            
                Cgr      
                                 
     
                                                              
                Cgr      
                                 
     
                    |
146 | 145 | ralbidv 2841 |
. . . . 5
    
                
              
                                 
     
                Cgr      
                                 
     
                      
                                 
     
                Cgr      
                                 
     
                                                              
                Cgr      
                                 
     
                                                                        
                    
              Cgr      
                                 
     
                    
                                                            
                Cgr      
                                 
     
                                                              
                Cgr      
                                 
     
                    |
147 | | breq1 4396 |
. . . . . . 7
    
               
  
   
                     |
148 | | opeq2 4161 |
. . . . . . . 8
    
                 
     
                  |
149 | 148 | breq2d 4405 |
. . . . . . 7
    
               
  
     
                   |
150 | | opeq1 4160 |
. . . . . . . 8
    
                        
                 |
151 | 150 | breq2d 4405 |
. . . . . . 7
    
               
  
      
                  |
152 | 147, 149,
151 | 3orbi123d 1289 |
. . . . . 6
    
                                   
          
  
       
             
      
                   |
153 | 152 | notbid 294 |
. . . . 5
    
                               
                         
             
      
                   |
154 | 146, 153 | 3anbi23d 1293 |
. . . 4
    
                     
                                 
     
                        
    
                                            
     
                Cgr      
                                 
     
                      
                                 
     
                Cgr      
                                 
     
                                                              
                Cgr      
                                 
     
                

  
                                                     
                        
    
                                            
     
                    
              Cgr      
                                 
     
                    
                                                            
                Cgr      
                                 
     
                                                              
                Cgr      
                                 
     
                
        
          
  
       
             
      
                    |
155 | | opeq2 4161 |
. . . . . . . 8
    
     ![]() |