Step | Hyp | Ref
| Expression |
1 | | bitsfzoOLD.1 |
. . 3
   |
2 | | nn0uz 11217 |
. . 3
     |
3 | 1, 2 | syl6eleq 2559 |
. 2
       |
4 | | 2nn 10790 |
. . . . 5
 |
5 | 4 | a1i 11 |
. . . 4
   |
6 | | bitsfzoOLD.2 |
. . . 4
   |
7 | 5, 6 | nnexpcld 12475 |
. . 3
       |
8 | 7 | nnzd 11062 |
. 2
       |
9 | | bitsfzoOLD.3 |
. . . . . . . 8
 bits   ..^   |
10 | 9 | adantr 472 |
. . . . . . 7
 
     bits   ..^   |
11 | | n2dvds1 14431 |
. . . . . . . . 9
 |
12 | 4 | a1i 11 |
. . . . . . . . . . . . . . . 16
 
       |
13 | | ssrab2 3500 |
. . . . . . . . . . . . . . . . . . . . 21
       |
14 | | bitsfzoOLD.4 |
. . . . . . . . . . . . . . . . . . . . . 22
         
 |
15 | 13, 2 | sseqtri 3450 |
. . . . . . . . . . . . . . . . . . . . . . 23
           |
16 | | nnssnn0 10896 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
 |
17 | 1 | nn0red 10950 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
   |
18 | | 2re 10701 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
 |
19 | 18 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
   |
20 | | 1lt2 10799 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
 |
21 | 20 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
   |
22 | | expnbnd 12439 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
 
        |
23 | 17, 19, 21, 22 | syl3anc 1292 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
        |
24 | | ssrexv 3480 |
. . . . . . . . . . . . . . . . . . . . . . . . 25

 
   
        |
25 | 16, 23, 24 | mpsyl 64 |
. . . . . . . . . . . . . . . . . . . . . . . 24
        |
26 | | rabn0 3755 |
. . . . . . . . . . . . . . . . . . . . . . . 24
              |
27 | 25, 26 | sylibr 217 |
. . . . . . . . . . . . . . . . . . . . . . 23
         |
28 | | infmssuzclOLD 11270 |
. . . . . . . . . . . . . . . . . . . . . . 23
           
         
               |
29 | 15, 27, 28 | sylancr 676 |
. . . . . . . . . . . . . . . . . . . . . 22
          
        |
30 | 14, 29 | syl5eqel 2553 |
. . . . . . . . . . . . . . . . . . . . 21
         |
31 | 13, 30 | sseldi 3416 |
. . . . . . . . . . . . . . . . . . . 20
   |
32 | 31 | nn0zd 11061 |
. . . . . . . . . . . . . . . . . . 19
   |
33 | 32 | adantr 472 |
. . . . . . . . . . . . . . . . . 18
 
       |
34 | | 0red 9662 |
. . . . . . . . . . . . . . . . . . 19
 
       |
35 | 6 | nn0zd 11061 |
. . . . . . . . . . . . . . . . . . . . 21
   |
36 | 35 | adantr 472 |
. . . . . . . . . . . . . . . . . . . 20
 
       |
37 | 36 | zred 11063 |
. . . . . . . . . . . . . . . . . . 19
 
       |
38 | 33 | zred 11063 |
. . . . . . . . . . . . . . . . . . 19
 
       |
39 | 6 | adantr 472 |
. . . . . . . . . . . . . . . . . . . 20
 
       |
40 | 39 | nn0ge0d 10952 |
. . . . . . . . . . . . . . . . . . 19
 
       |
41 | 18 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . 22
 
       |
42 | 41, 39 | reexpcld 12471 |
. . . . . . . . . . . . . . . . . . . . 21
 
           |
43 | 17 | adantr 472 |
. . . . . . . . . . . . . . . . . . . . 21
 
       |
44 | 5, 31 | nnexpcld 12475 |
. . . . . . . . . . . . . . . . . . . . . . 23
       |
45 | 44 | adantr 472 |
. . . . . . . . . . . . . . . . . . . . . 22
 
           |
46 | 45 | nnred 10646 |
. . . . . . . . . . . . . . . . . . . . 21
 
           |
47 | | simpr 468 |
. . . . . . . . . . . . . . . . . . . . 21
 
           |
48 | 30 | adantr 472 |
. . . . . . . . . . . . . . . . . . . . . 22
 
             |
49 | | oveq2 6316 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
           |
50 | 49 | breq2d 4407 |
. . . . . . . . . . . . . . . . . . . . . . . 24
     
       |
51 | | oveq2 6316 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
           |
52 | 51 | breq2d 4407 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
     
       |
53 | 52 | cbvrabv 3030 |
. . . . . . . . . . . . . . . . . . . . . . . 24
             |
54 | 50, 53 | elrab2 3186 |
. . . . . . . . . . . . . . . . . . . . . . 23
 
     
       |
55 | 54 | simprbi 471 |
. . . . . . . . . . . . . . . . . . . . . 22
 
    
      |
56 | 48, 55 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
 
           |
57 | 42, 43, 46, 47, 56 | lelttrd 9810 |
. . . . . . . . . . . . . . . . . . . 20
 
               |
58 | 20 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . 21
 
       |
59 | 41, 36, 33, 58 | ltexp2d 12483 |
. . . . . . . . . . . . . . . . . . . 20
 
     
           |
60 | 57, 59 | mpbird 240 |
. . . . . . . . . . . . . . . . . . 19
 
       |
61 | 34, 37, 38, 40, 60 | lelttrd 9810 |
. . . . . . . . . . . . . . . . . 18
 
       |
62 | | elnnz 10971 |
. . . . . . . . . . . . . . . . . 18

    |
63 | 33, 61, 62 | sylanbrc 677 |
. . . . . . . . . . . . . . . . 17
 
       |
64 | | nnm1nn0 10935 |
. . . . . . . . . . . . . . . . 17
 
   |
65 | 63, 64 | syl 17 |
. . . . . . . . . . . . . . . 16
 
     
   |
66 | 12, 65 | nnexpcld 12475 |
. . . . . . . . . . . . . . 15
 
             |
67 | 66 | nncnd 10647 |
. . . . . . . . . . . . . 14
 
             |
68 | 67 | mulid2d 9679 |
. . . . . . . . . . . . 13
 
                     |
69 | 38 | ltm1d 10561 |
. . . . . . . . . . . . . . . 16
 
     
   |
70 | 65 | nn0red 10950 |
. . . . . . . . . . . . . . . . 17
 
     
   |
71 | 70, 38 | ltnled 9799 |
. . . . . . . . . . . . . . . 16
 
       
     |
72 | 69, 71 | mpbid 215 |
. . . . . . . . . . . . . . 15
 
         |
73 | | oveq2 6316 |
. . . . . . . . . . . . . . . . . . 19
               |
74 | 73 | breq2d 4407 |
. . . . . . . . . . . . . . . . . 18
       
         |
75 | 74, 53 | elrab2 3186 |
. . . . . . . . . . . . . . . . 17
   
       
         |
76 | | infmssuzleOLD 11269 |
. . . . . . . . . . . . . . . . . . . 20
           
        
  
      
    |
77 | 15, 76 | mpan 684 |
. . . . . . . . . . . . . . . . . . 19
   
    
  
      
    |
78 | 14, 77 | syl5eqbr 4429 |
. . . . . . . . . . . . . . . . . 18
   
    
    |
79 | 78 | a1i 11 |
. . . . . . . . . . . . . . . . 17
 
                   |
80 | 75, 79 | syl5bir 226 |
. . . . . . . . . . . . . . . 16
 
                
    |
81 | 65, 80 | mpand 689 |
. . . . . . . . . . . . . . 15
 
                 |
82 | 72, 81 | mtod 182 |
. . . . . . . . . . . . . 14
 
             |
83 | 66 | nnred 10646 |
. . . . . . . . . . . . . . 15
 
             |
84 | 83, 43 | lenltd 9798 |
. . . . . . . . . . . . . 14
 
         
 
   
     |
85 | 82, 84 | mpbird 240 |
. . . . . . . . . . . . 13
 
             |
86 | 68, 85 | eqbrtrd 4416 |
. . . . . . . . . . . 12
 
               |
87 | | 1red 9676 |
. . . . . . . . . . . . 13
 
       |
88 | | 2rp 11330 |
. . . . . . . . . . . . . . 15
 |
89 | 88 | a1i 11 |
. . . . . . . . . . . . . 14
 
       |
90 | | 1z 10991 |
. . . . . . . . . . . . . . . 16
 |
91 | 90 | a1i 11 |
. . . . . . . . . . . . . . 15
 
       |
92 | 33, 91 | zsubcld 11068 |
. . . . . . . . . . . . . 14
 
     
   |
93 | 89, 92 | rpexpcld 12477 |
. . . . . . . . . . . . 13
 
             |
94 | 87, 43, 93 | lemuldivd 11410 |
. . . . . . . . . . . 12
 
             
           |
95 | 86, 94 | mpbid 215 |
. . . . . . . . . . 11
 
               |
96 | | 2cn 10702 |
. . . . . . . . . . . . . . 15
 |
97 | | expm1t 12338 |
. . . . . . . . . . . . . . 15
 
               |
98 | 96, 63, 97 | sylancr 676 |
. . . . . . . . . . . . . 14
 
                   |
99 | 56, 98 | breqtrd 4420 |
. . . . . . . . . . . . 13
 
               |
100 | 43, 41, 93 | ltdivmuld 11412 |
. . . . . . . . . . . . 13
 
                         |
101 | 99, 100 | mpbird 240 |
. . . . . . . . . . . 12
 
               |
102 | | df-2 10690 |
. . . . . . . . . . . 12
   |
103 | 101, 102 | syl6breq 4435 |
. . . . . . . . . . 11
 
                 |
104 | 43, 93 | rerpdivcld 11392 |
. . . . . . . . . . . 12
 
               |
105 | | flbi 12084 |
. . . . . . . . . . . 12
         
     
                 
             |
106 | 104, 90, 105 | sylancl 675 |
. . . . . . . . . . 11
 
                 
     
                 |
107 | 95, 103, 106 | mpbir2and 936 |
. . . . . . . . . 10
 
            
      |
108 | 107 | breq2d 4407 |
. . . . . . . . 9
 
     
           
   |
109 | 11, 108 | mtbiri 310 |
. . . . . . . 8
 
        
          |
110 | 1 | nn0zd 11061 |
. . . . . . . . . 10
   |
111 | 110 | adantr 472 |
. . . . . . . . 9
 
       |
112 | | bitsval2 14477 |
. . . . . . . . 9
  
     bits 
               |
113 | 111, 65, 112 | syl2anc 673 |
. . . . . . . 8
 
        bits 
               |
114 | 109, 113 | mpbird 240 |
. . . . . . 7
 
     
 bits    |
115 | 10, 114 | sseldd 3419 |
. . . . . 6
 
     
  ..^   |
116 | | elfzolt2 11956 |
. . . . . 6
    ..^
    |
117 | 115, 116 | syl 17 |
. . . . 5
 
     
   |
118 | | zlem1lt 11012 |
. . . . . 6
 
       |
119 | 33, 36, 118 | syl2anc 673 |
. . . . 5
 
     
     |
120 | 117, 119 | mpbird 240 |
. . . 4
 
       |
121 | 37, 38 | ltnled 9799 |
. . . . 5
 
     
   |
122 | 60, 121 | mpbid 215 |
. . . 4
 
       |
123 | 120, 122 | pm2.65da 586 |
. . 3
       |
124 | 7 | nnred 10646 |
. . . 4
       |
125 | 17, 124 | ltnled 9799 |
. . 3
         
   |
126 | 123, 125 | mpbird 240 |
. 2
       |
127 | | elfzo2 11950 |
. 2
  ..^                     |
128 | 3, 8, 126, 127 | syl3anbrc 1214 |
1
  ..^       |