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