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 ( 𝑁 ∈ ℕ → ( 𝑁 = 1 ↔ ( 0 ≤ ( 2 logb 𝑁 ) ∧ ( 2 logb 𝑁 ) < 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 ) → ( 2 logb 1 ) = 0 )
7 2 3 5 6 mp3an ( 2 logb 1 ) = 0
8 1 7 breqtrri 0 ≤ ( 2 logb 1 )
9 0lt1 0 < 1
10 7 9 eqbrtri ( 2 logb 1 ) < 1
11 8 10 pm3.2i ( 0 ≤ ( 2 logb 1 ) ∧ ( 2 logb 1 ) < 1 )
12 oveq2 ( 𝑁 = 1 → ( 2 logb 𝑁 ) = ( 2 logb 1 ) )
13 12 breq2d ( 𝑁 = 1 → ( 0 ≤ ( 2 logb 𝑁 ) ↔ 0 ≤ ( 2 logb 1 ) ) )
14 12 breq1d ( 𝑁 = 1 → ( ( 2 logb 𝑁 ) < 1 ↔ ( 2 logb 1 ) < 1 ) )
15 13 14 anbi12d ( 𝑁 = 1 → ( ( 0 ≤ ( 2 logb 𝑁 ) ∧ ( 2 logb 𝑁 ) < 1 ) ↔ ( 0 ≤ ( 2 logb 1 ) ∧ ( 2 logb 1 ) < 1 ) ) )
16 11 15 mpbiri ( 𝑁 = 1 → ( 0 ≤ ( 2 logb 𝑁 ) ∧ ( 2 logb 𝑁 ) < 1 ) )
17 2z 2 ∈ ℤ
18 uzid ( 2 ∈ ℤ → 2 ∈ ( ℤ ‘ 2 ) )
19 17 18 ax-mp 2 ∈ ( ℤ ‘ 2 )
20 19 a1i ( 𝑁 ∈ ℕ → 2 ∈ ( ℤ ‘ 2 ) )
21 nnrp ( 𝑁 ∈ ℕ → 𝑁 ∈ ℝ+ )
22 logbge0b ( ( 2 ∈ ( ℤ ‘ 2 ) ∧ 𝑁 ∈ ℝ+ ) → ( 0 ≤ ( 2 logb 𝑁 ) ↔ 1 ≤ 𝑁 ) )
23 20 21 22 syl2anc ( 𝑁 ∈ ℕ → ( 0 ≤ ( 2 logb 𝑁 ) ↔ 1 ≤ 𝑁 ) )
24 logblt1b ( ( 2 ∈ ( ℤ ‘ 2 ) ∧ 𝑁 ∈ ℝ+ ) → ( ( 2 logb 𝑁 ) < 1 ↔ 𝑁 < 2 ) )
25 20 21 24 syl2anc ( 𝑁 ∈ ℕ → ( ( 2 logb 𝑁 ) < 1 ↔ 𝑁 < 2 ) )
26 23 25 anbi12d ( 𝑁 ∈ ℕ → ( ( 0 ≤ ( 2 logb 𝑁 ) ∧ ( 2 logb 𝑁 ) < 1 ) ↔ ( 1 ≤ 𝑁𝑁 < 2 ) ) )
27 df-2 2 = ( 1 + 1 )
28 27 breq2i ( 𝑁 < 2 ↔ 𝑁 < ( 1 + 1 ) )
29 28 a1i ( 𝑁 ∈ ℕ → ( 𝑁 < 2 ↔ 𝑁 < ( 1 + 1 ) ) )
30 29 anbi2d ( 𝑁 ∈ ℕ → ( ( 1 ≤ 𝑁𝑁 < 2 ) ↔ ( 1 ≤ 𝑁𝑁 < ( 1 + 1 ) ) ) )
31 nnre ( 𝑁 ∈ ℕ → 𝑁 ∈ ℝ )
32 1zzd ( 𝑁 ∈ ℕ → 1 ∈ ℤ )
33 flbi ( ( 𝑁 ∈ ℝ ∧ 1 ∈ ℤ ) → ( ( ⌊ ‘ 𝑁 ) = 1 ↔ ( 1 ≤ 𝑁𝑁 < ( 1 + 1 ) ) ) )
34 31 32 33 syl2anc ( 𝑁 ∈ ℕ → ( ( ⌊ ‘ 𝑁 ) = 1 ↔ ( 1 ≤ 𝑁𝑁 < ( 1 + 1 ) ) ) )
35 30 34 bitr4d ( 𝑁 ∈ ℕ → ( ( 1 ≤ 𝑁𝑁 < 2 ) ↔ ( ⌊ ‘ 𝑁 ) = 1 ) )
36 nnz ( 𝑁 ∈ ℕ → 𝑁 ∈ ℤ )
37 flid ( 𝑁 ∈ ℤ → ( ⌊ ‘ 𝑁 ) = 𝑁 )
38 36 37 syl ( 𝑁 ∈ ℕ → ( ⌊ ‘ 𝑁 ) = 𝑁 )
39 38 eqcomd ( 𝑁 ∈ ℕ → 𝑁 = ( ⌊ ‘ 𝑁 ) )
40 39 adantr ( ( 𝑁 ∈ ℕ ∧ ( ⌊ ‘ 𝑁 ) = 1 ) → 𝑁 = ( ⌊ ‘ 𝑁 ) )
41 simpr ( ( 𝑁 ∈ ℕ ∧ ( ⌊ ‘ 𝑁 ) = 1 ) → ( ⌊ ‘ 𝑁 ) = 1 )
42 40 41 eqtrd ( ( 𝑁 ∈ ℕ ∧ ( ⌊ ‘ 𝑁 ) = 1 ) → 𝑁 = 1 )
43 42 ex ( 𝑁 ∈ ℕ → ( ( ⌊ ‘ 𝑁 ) = 1 → 𝑁 = 1 ) )
44 35 43 sylbid ( 𝑁 ∈ ℕ → ( ( 1 ≤ 𝑁𝑁 < 2 ) → 𝑁 = 1 ) )
45 26 44 sylbid ( 𝑁 ∈ ℕ → ( ( 0 ≤ ( 2 logb 𝑁 ) ∧ ( 2 logb 𝑁 ) < 1 ) → 𝑁 = 1 ) )
46 16 45 impbid2 ( 𝑁 ∈ ℕ → ( 𝑁 = 1 ↔ ( 0 ≤ ( 2 logb 𝑁 ) ∧ ( 2 logb 𝑁 ) < 1 ) ) )