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≤log2N∧log2N<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→log21=0
7 2 3 5 6 mp3an ⊢log21=0
8 1 7 breqtrri ⊢0≤log21
9 0lt1 ⊢0<1
10 7 9 eqbrtri ⊢log21<1
11 8 10 pm3.2i ⊢0≤log21∧log21<1
12 oveq2 ⊢N=1→log2N=log21
13 12 breq2d ⊢N=1→0≤log2N↔0≤log21
14 12 breq1d ⊢N=1→log2N<1↔log21<1
15 13 14 anbi12d ⊢N=1→0≤log2N∧log2N<1↔0≤log21∧log21<1
16 11 15 mpbiri ⊢N=1→0≤log2N∧log2N<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≤log2N↔1≤N
23 20 21 22 syl2anc ⊢N∈ℕ→0≤log2N↔1≤N
24 logblt1b ⊢2∈ℤ≥2∧N∈ℝ+→log2N<1↔N<2
25 20 21 24 syl2anc ⊢N∈ℕ→log2N<1↔N<2
26 23 25 anbi12d ⊢N∈ℕ→0≤log2N∧log2N<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≤log2N∧log2N<1→N=1
46 16 45 impbid2 ⊢N∈ℕ→N=1↔0≤log2N∧log2N<1