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 ⊢N∈ℕ0→#b ⁡ N = 1 ↔ N=0∨N=1

Proof

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