Step | Hyp | Ref
| Expression |
1 | | bitsfzo.1 |
. . 3
|
2 | | nn0uz 11722 |
. . 3
|
3 | 1, 2 | syl6eleq 2711 |
. 2
|
4 | | 2nn 11185 |
. . . . 5
|
5 | 4 | a1i 11 |
. . . 4
|
6 | | bitsfzo.2 |
. . . 4
|
7 | 5, 6 | nnexpcld 13030 |
. . 3
|
8 | 7 | nnzd 11481 |
. 2
|
9 | | bitsfzo.3 |
. . . . . . . 8
bits ..^ |
10 | 9 | adantr 481 |
. . . . . . 7
bits ..^ |
11 | | n2dvds1 15104 |
. . . . . . . . 9
|
12 | 4 | a1i 11 |
. . . . . . . . . . . . . . . 16
|
13 | | ssrab2 3687 |
. . . . . . . . . . . . . . . . . . . . 21
|
14 | | bitsfzo.4 |
. . . . . . . . . . . . . . . . . . . . . 22
inf
|
15 | 13, 2 | sseqtri 3637 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
16 | | nnssnn0 11295 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
17 | 1 | nn0red 11352 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
18 | | 2re 11090 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
19 | 18 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
20 | | 1lt2 11194 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
21 | 20 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
22 | | expnbnd 12993 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
23 | 17, 19, 21, 22 | syl3anc 1326 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
24 | | ssrexv 3667 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
25 | 16, 23, 24 | mpsyl 68 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
26 | | rabn0 3958 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
27 | 25, 26 | sylibr 224 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
28 | | infssuzcl 11772 |
. . . . . . . . . . . . . . . . . . . . . . 23
inf
|
29 | 15, 27, 28 | sylancr 695 |
. . . . . . . . . . . . . . . . . . . . . 22
inf
|
30 | 14, 29 | syl5eqel 2705 |
. . . . . . . . . . . . . . . . . . . . 21
|
31 | 13, 30 | sseldi 3601 |
. . . . . . . . . . . . . . . . . . . 20
|
32 | 31 | nn0zd 11480 |
. . . . . . . . . . . . . . . . . . 19
|
33 | 32 | adantr 481 |
. . . . . . . . . . . . . . . . . 18
|
34 | | 0red 10041 |
. . . . . . . . . . . . . . . . . . 19
|
35 | 6 | nn0zd 11480 |
. . . . . . . . . . . . . . . . . . . . 21
|
36 | 35 | adantr 481 |
. . . . . . . . . . . . . . . . . . . 20
|
37 | 36 | zred 11482 |
. . . . . . . . . . . . . . . . . . 19
|
38 | 33 | zred 11482 |
. . . . . . . . . . . . . . . . . . 19
|
39 | 6 | adantr 481 |
. . . . . . . . . . . . . . . . . . . 20
|
40 | 39 | nn0ge0d 11354 |
. . . . . . . . . . . . . . . . . . 19
|
41 | 18 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . 22
|
42 | 41, 39 | reexpcld 13025 |
. . . . . . . . . . . . . . . . . . . . 21
|
43 | 17 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . 21
|
44 | 5, 31 | nnexpcld 13030 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
45 | 44 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . 22
|
46 | 45 | nnred 11035 |
. . . . . . . . . . . . . . . . . . . . 21
|
47 | | simpr 477 |
. . . . . . . . . . . . . . . . . . . . 21
|
48 | 30 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . 22
|
49 | | oveq2 6658 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
50 | 49 | breq2d 4665 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
51 | | oveq2 6658 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
52 | 51 | breq2d 4665 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
53 | 52 | cbvrabv 3199 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
54 | 50, 53 | elrab2 3366 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
55 | 54 | simprbi 480 |
. . . . . . . . . . . . . . . . . . . . . 22
|
56 | 48, 55 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
|
57 | 42, 43, 46, 47, 56 | lelttrd 10195 |
. . . . . . . . . . . . . . . . . . . 20
|
58 | 20 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . 21
|
59 | 41, 36, 33, 58 | ltexp2d 13038 |
. . . . . . . . . . . . . . . . . . . 20
|
60 | 57, 59 | mpbird 247 |
. . . . . . . . . . . . . . . . . . 19
|
61 | 34, 37, 38, 40, 60 | lelttrd 10195 |
. . . . . . . . . . . . . . . . . 18
|
62 | | elnnz 11387 |
. . . . . . . . . . . . . . . . . 18
|
63 | 33, 61, 62 | sylanbrc 698 |
. . . . . . . . . . . . . . . . 17
|
64 | | nnm1nn0 11334 |
. . . . . . . . . . . . . . . . 17
|
65 | 63, 64 | syl 17 |
. . . . . . . . . . . . . . . 16
|
66 | 12, 65 | nnexpcld 13030 |
. . . . . . . . . . . . . . 15
|
67 | 66 | nncnd 11036 |
. . . . . . . . . . . . . 14
|
68 | 67 | mulid2d 10058 |
. . . . . . . . . . . . 13
|
69 | 38 | ltm1d 10956 |
. . . . . . . . . . . . . . . 16
|
70 | 65 | nn0red 11352 |
. . . . . . . . . . . . . . . . 17
|
71 | 70, 38 | ltnled 10184 |
. . . . . . . . . . . . . . . 16
|
72 | 69, 71 | mpbid 222 |
. . . . . . . . . . . . . . 15
|
73 | | oveq2 6658 |
. . . . . . . . . . . . . . . . . . 19
|
74 | 73 | breq2d 4665 |
. . . . . . . . . . . . . . . . . 18
|
75 | 74, 53 | elrab2 3366 |
. . . . . . . . . . . . . . . . 17
|
76 | | infssuzle 11771 |
. . . . . . . . . . . . . . . . . . . 20
inf
|
77 | 15, 76 | mpan 706 |
. . . . . . . . . . . . . . . . . . 19
inf
|
78 | 14, 77 | syl5eqbr 4688 |
. . . . . . . . . . . . . . . . . 18
|
79 | 78 | a1i 11 |
. . . . . . . . . . . . . . . . 17
|
80 | 75, 79 | syl5bir 233 |
. . . . . . . . . . . . . . . 16
|
81 | 65, 80 | mpand 711 |
. . . . . . . . . . . . . . 15
|
82 | 72, 81 | mtod 189 |
. . . . . . . . . . . . . 14
|
83 | 66 | nnred 11035 |
. . . . . . . . . . . . . . 15
|
84 | 83, 43 | lenltd 10183 |
. . . . . . . . . . . . . 14
|
85 | 82, 84 | mpbird 247 |
. . . . . . . . . . . . 13
|
86 | 68, 85 | eqbrtrd 4675 |
. . . . . . . . . . . 12
|
87 | | 1red 10055 |
. . . . . . . . . . . . 13
|
88 | | 2rp 11837 |
. . . . . . . . . . . . . . 15
|
89 | 88 | a1i 11 |
. . . . . . . . . . . . . 14
|
90 | | 1z 11407 |
. . . . . . . . . . . . . . . 16
|
91 | 90 | a1i 11 |
. . . . . . . . . . . . . . 15
|
92 | 33, 91 | zsubcld 11487 |
. . . . . . . . . . . . . 14
|
93 | 89, 92 | rpexpcld 13032 |
. . . . . . . . . . . . 13
|
94 | 87, 43, 93 | lemuldivd 11921 |
. . . . . . . . . . . 12
|
95 | 86, 94 | mpbid 222 |
. . . . . . . . . . 11
|
96 | | 2cn 11091 |
. . . . . . . . . . . . . . 15
|
97 | | expm1t 12888 |
. . . . . . . . . . . . . . 15
|
98 | 96, 63, 97 | sylancr 695 |
. . . . . . . . . . . . . 14
|
99 | 56, 98 | breqtrd 4679 |
. . . . . . . . . . . . 13
|
100 | 43, 41, 93 | ltdivmuld 11923 |
. . . . . . . . . . . . 13
|
101 | 99, 100 | mpbird 247 |
. . . . . . . . . . . 12
|
102 | | df-2 11079 |
. . . . . . . . . . . 12
|
103 | 101, 102 | syl6breq 4694 |
. . . . . . . . . . 11
|
104 | 43, 93 | rerpdivcld 11903 |
. . . . . . . . . . . 12
|
105 | | flbi 12617 |
. . . . . . . . . . . 12
|
106 | 104, 90, 105 | sylancl 694 |
. . . . . . . . . . 11
|
107 | 95, 103, 106 | mpbir2and 957 |
. . . . . . . . . 10
|
108 | 107 | breq2d 4665 |
. . . . . . . . 9
|
109 | 11, 108 | mtbiri 317 |
. . . . . . . 8
|
110 | 1 | nn0zd 11480 |
. . . . . . . . . 10
|
111 | 110 | adantr 481 |
. . . . . . . . 9
|
112 | | bitsval2 15147 |
. . . . . . . . 9
bits
|
113 | 111, 65, 112 | syl2anc 693 |
. . . . . . . 8
bits
|
114 | 109, 113 | mpbird 247 |
. . . . . . 7
bits |
115 | 10, 114 | sseldd 3604 |
. . . . . 6
..^ |
116 | | elfzolt2 12479 |
. . . . . 6
..^
|
117 | 115, 116 | syl 17 |
. . . . 5
|
118 | | zlem1lt 11429 |
. . . . . 6
|
119 | 33, 36, 118 | syl2anc 693 |
. . . . 5
|
120 | 117, 119 | mpbird 247 |
. . . 4
|
121 | 37, 38 | ltnled 10184 |
. . . . 5
|
122 | 60, 121 | mpbid 222 |
. . . 4
|
123 | 120, 122 | pm2.65da 600 |
. . 3
|
124 | 7 | nnred 11035 |
. . . 4
|
125 | 17, 124 | ltnled 10184 |
. . 3
|
126 | 123, 125 | mpbird 247 |
. 2
|
127 | | elfzo2 12473 |
. 2
..^ |
128 | 3, 8, 126, 127 | syl3anbrc 1246 |
1
..^ |