Metamath Proof Explorer


Theorem nnlog2ge0lt1

Description: A positive integer is 1 iff its binary logarithm is between 0 and 1. (Contributed by AV, 30-May-2020)

Ref Expression
Assertion nnlog2ge0lt1 N N = 1 0 log 2 N log 2 N < 1

Proof

Step Hyp Ref Expression
1 0le0 0 0
2 2cn 2
3 2ne0 2 0
4 1ne2 1 2
5 4 necomi 2 1
6 logb1 2 2 0 2 1 log 2 1 = 0
7 2 3 5 6 mp3an log 2 1 = 0
8 1 7 breqtrri 0 log 2 1
9 0lt1 0 < 1
10 7 9 eqbrtri log 2 1 < 1
11 8 10 pm3.2i 0 log 2 1 log 2 1 < 1
12 oveq2 N = 1 log 2 N = log 2 1
13 12 breq2d N = 1 0 log 2 N 0 log 2 1
14 12 breq1d N = 1 log 2 N < 1 log 2 1 < 1
15 13 14 anbi12d N = 1 0 log 2 N log 2 N < 1 0 log 2 1 log 2 1 < 1
16 11 15 mpbiri N = 1 0 log 2 N log 2 N < 1
17 2z 2
18 uzid 2 2 2
19 17 18 ax-mp 2 2
20 19 a1i N 2 2
21 nnrp N N +
22 logbge0b 2 2 N + 0 log 2 N 1 N
23 20 21 22 syl2anc N 0 log 2 N 1 N
24 logblt1b 2 2 N + log 2 N < 1 N < 2
25 20 21 24 syl2anc N log 2 N < 1 N < 2
26 23 25 anbi12d N 0 log 2 N log 2 N < 1 1 N N < 2
27 df-2 2 = 1 + 1
28 27 breq2i N < 2 N < 1 + 1
29 28 a1i N N < 2 N < 1 + 1
30 29 anbi2d N 1 N N < 2 1 N N < 1 + 1
31 nnre N N
32 1zzd N 1
33 flbi N 1 N = 1 1 N N < 1 + 1
34 31 32 33 syl2anc N N = 1 1 N N < 1 + 1
35 30 34 bitr4d N 1 N N < 2 N = 1
36 nnz N N
37 flid N N = N
38 36 37 syl N N = N
39 38 eqcomd N N = N
40 39 adantr N N = 1 N = N
41 simpr N N = 1 N = 1
42 40 41 eqtrd N N = 1 N = 1
43 42 ex N N = 1 N = 1
44 35 43 sylbid N 1 N N < 2 N = 1
45 26 44 sylbid N 0 log 2 N log 2 N < 1 N = 1
46 16 45 impbid2 N N = 1 0 log 2 N log 2 N < 1