Metamath Proof Explorer

Theorem blen1b

Description: The binary length of a nonnegative integer is 1 if the integer is 0 or 1. (Contributed by AV, 30-May-2020)

Ref Expression
Assertion blen1b ( 𝑁 ∈ ℕ0 → ( ( #b ‘ 𝑁 ) = 1 ↔ ( 𝑁 = 0 ∨ 𝑁 = 1 ) ) )

Proof

Step Hyp Ref Expression
1 elnn0 ⊢ ( 𝑁 ∈ ℕ0 ↔ ( 𝑁 ∈ ℕ ∨ 𝑁 = 0 ) )
2 blennn ⊢ ( 𝑁 ∈ ℕ → ( #b ‘ 𝑁 ) = ( ( ⌊ ‘ ( 2 logb 𝑁 ) ) + 1 ) )
3 2 eqeq1d ⊢ ( 𝑁 ∈ ℕ → ( ( #b ‘ 𝑁 ) = 1 ↔ ( ( ⌊ ‘ ( 2 logb 𝑁 ) ) + 1 ) = 1 ) )
4 2rp ⊢ 2 ∈ ℝ+
5 4 a1i ⊢ ( 𝑁 ∈ ℕ → 2 ∈ ℝ+ )
6 nnrp ⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℝ+ )
7 1ne2 ⊢ 1 ≠ 2
8 7 necomi ⊢ 2 ≠ 1
9 8 a1i ⊢ ( 𝑁 ∈ ℕ → 2 ≠ 1 )
10 relogbcl ⊢ ( ( 2 ∈ ℝ+ ∧ 𝑁 ∈ ℝ+ ∧ 2 ≠ 1 ) → ( 2 logb 𝑁 ) ∈ ℝ )
11 5 6 9 10 syl3anc ⊢ ( 𝑁 ∈ ℕ → ( 2 logb 𝑁 ) ∈ ℝ )
12 11 flcld ⊢ ( 𝑁 ∈ ℕ → ( ⌊ ‘ ( 2 logb 𝑁 ) ) ∈ ℤ )
13 12 zcnd ⊢ ( 𝑁 ∈ ℕ → ( ⌊ ‘ ( 2 logb 𝑁 ) ) ∈ ℂ )
14 1cnd ⊢ ( 𝑁 ∈ ℕ → 1 ∈ ℂ )
15 13 14 14 addlsub ⊢ ( 𝑁 ∈ ℕ → ( ( ( ⌊ ‘ ( 2 logb 𝑁 ) ) + 1 ) = 1 ↔ ( ⌊ ‘ ( 2 logb 𝑁 ) ) = ( 1 − 1 ) ) )
16 1m1e0 ⊢ ( 1 − 1 ) = 0
17 16 a1i ⊢ ( 𝑁 ∈ ℕ → ( 1 − 1 ) = 0 )
18 17 eqeq2d ⊢ ( 𝑁 ∈ ℕ → ( ( ⌊ ‘ ( 2 logb 𝑁 ) ) = ( 1 − 1 ) ↔ ( ⌊ ‘ ( 2 logb 𝑁 ) ) = 0 ) )
19 0z ⊢ 0 ∈ ℤ
20 flbi ⊢ ( ( ( 2 logb 𝑁 ) ∈ ℝ ∧ 0 ∈ ℤ ) → ( ( ⌊ ‘ ( 2 logb 𝑁 ) ) = 0 ↔ ( 0 ≤ ( 2 logb 𝑁 ) ∧ ( 2 logb 𝑁 ) < ( 0 + 1 ) ) ) )
21 11 19 20 sylancl ⊢ ( 𝑁 ∈ ℕ → ( ( ⌊ ‘ ( 2 logb 𝑁 ) ) = 0 ↔ ( 0 ≤ ( 2 logb 𝑁 ) ∧ ( 2 logb 𝑁 ) < ( 0 + 1 ) ) ) )
22 15 18 21 3bitrd ⊢ ( 𝑁 ∈ ℕ → ( ( ( ⌊ ‘ ( 2 logb 𝑁 ) ) + 1 ) = 1 ↔ ( 0 ≤ ( 2 logb 𝑁 ) ∧ ( 2 logb 𝑁 ) < ( 0 + 1 ) ) ) )
23 0p1e1 ⊢ ( 0 + 1 ) = 1
24 23 breq2i ⊢ ( ( 2 logb 𝑁 ) < ( 0 + 1 ) ↔ ( 2 logb 𝑁 ) < 1 )
25 24 anbi2i ⊢ ( ( 0 ≤ ( 2 logb 𝑁 ) ∧ ( 2 logb 𝑁 ) < ( 0 + 1 ) ) ↔ ( 0 ≤ ( 2 logb 𝑁 ) ∧ ( 2 logb 𝑁 ) < 1 ) )
26 nnlog2ge0lt1 ⊢ ( 𝑁 ∈ ℕ → ( 𝑁 = 1 ↔ ( 0 ≤ ( 2 logb 𝑁 ) ∧ ( 2 logb 𝑁 ) < 1 ) ) )
27 26 biimpar ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 0 ≤ ( 2 logb 𝑁 ) ∧ ( 2 logb 𝑁 ) < 1 ) ) → 𝑁 = 1 )
28 27 olcd ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 0 ≤ ( 2 logb 𝑁 ) ∧ ( 2 logb 𝑁 ) < 1 ) ) → ( 𝑁 = 0 ∨ 𝑁 = 1 ) )
29 28 ex ⊢ ( 𝑁 ∈ ℕ → ( ( 0 ≤ ( 2 logb 𝑁 ) ∧ ( 2 logb 𝑁 ) < 1 ) → ( 𝑁 = 0 ∨ 𝑁 = 1 ) ) )
30 25 29 syl5bi ⊢ ( 𝑁 ∈ ℕ → ( ( 0 ≤ ( 2 logb 𝑁 ) ∧ ( 2 logb 𝑁 ) < ( 0 + 1 ) ) → ( 𝑁 = 0 ∨ 𝑁 = 1 ) ) )
31 22 30 sylbid ⊢ ( 𝑁 ∈ ℕ → ( ( ( ⌊ ‘ ( 2 logb 𝑁 ) ) + 1 ) = 1 → ( 𝑁 = 0 ∨ 𝑁 = 1 ) ) )
32 3 31 sylbid ⊢ ( 𝑁 ∈ ℕ → ( ( #b ‘ 𝑁 ) = 1 → ( 𝑁 = 0 ∨ 𝑁 = 1 ) ) )
33 orc ⊢ ( 𝑁 = 0 → ( 𝑁 = 0 ∨ 𝑁 = 1 ) )
34 33 a1d ⊢ ( 𝑁 = 0 → ( ( #b ‘ 𝑁 ) = 1 → ( 𝑁 = 0 ∨ 𝑁 = 1 ) ) )
35 32 34 jaoi ⊢ ( ( 𝑁 ∈ ℕ ∨ 𝑁 = 0 ) → ( ( #b ‘ 𝑁 ) = 1 → ( 𝑁 = 0 ∨ 𝑁 = 1 ) ) )
36 1 35 sylbi ⊢ ( 𝑁 ∈ ℕ0 → ( ( #b ‘ 𝑁 ) = 1 → ( 𝑁 = 0 ∨ 𝑁 = 1 ) ) )
37 fveq2 ⊢ ( 𝑁 = 0 → ( #b ‘ 𝑁 ) = ( #b ‘ 0 ) )
38 blen0 ⊢ ( #b ‘ 0 ) = 1
39 37 38 eqtrdi ⊢ ( 𝑁 = 0 → ( #b ‘ 𝑁 ) = 1 )
40 fveq2 ⊢ ( 𝑁 = 1 → ( #b ‘ 𝑁 ) = ( #b ‘ 1 ) )
41 blen1 ⊢ ( #b ‘ 1 ) = 1
42 40 41 eqtrdi ⊢ ( 𝑁 = 1 → ( #b ‘ 𝑁 ) = 1 )
43 39 42 jaoi ⊢ ( ( 𝑁 = 0 ∨ 𝑁 = 1 ) → ( #b ‘ 𝑁 ) = 1 )
44 36 43 impbid1 ⊢ ( 𝑁 ∈ ℕ0 → ( ( #b ‘ 𝑁 ) = 1 ↔ ( 𝑁 = 0 ∨ 𝑁 = 1 ) ) )