Metamath Proof Explorer

Theorem dig2nn1st

Description: The first (relevant) digit of a positive integer in a binary system is 1. (Contributed by AV, 26-May-2020)

Ref Expression
Assertion dig2nn1st ( 𝑁 ∈ ℕ → ( ( ( #b ‘ 𝑁 ) − 1 ) ( digit ‘ 2 ) 𝑁 ) = 1 )

Proof

Step Hyp Ref Expression
1 2nn ⊢ 2 ∈ ℕ
2 1 a1i ⊢ ( 𝑁 ∈ ℕ → 2 ∈ ℕ )
3 blennnelnn ⊢ ( 𝑁 ∈ ℕ → ( #b ‘ 𝑁 ) ∈ ℕ )
4 nnm1nn0 ⊢ ( ( #b ‘ 𝑁 ) ∈ ℕ → ( ( #b ‘ 𝑁 ) − 1 ) ∈ ℕ0 )
5 3 4 syl ⊢ ( 𝑁 ∈ ℕ → ( ( #b ‘ 𝑁 ) − 1 ) ∈ ℕ0 )
6 nnre ⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℝ )
7 nnnn0 ⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℕ0 )
8 7 nn0ge0d ⊢ ( 𝑁 ∈ ℕ → 0 ≤ 𝑁 )
9 elrege0 ⊢ ( 𝑁 ∈ ( 0 [,) +∞ ) ↔ ( 𝑁 ∈ ℝ ∧ 0 ≤ 𝑁 ) )
10 6 8 9 sylanbrc ⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ( 0 [,) +∞ ) )
11 nn0digval ⊢ ( ( 2 ∈ ℕ ∧ ( ( #b ‘ 𝑁 ) − 1 ) ∈ ℕ0 ∧ 𝑁 ∈ ( 0 [,) +∞ ) ) → ( ( ( #b ‘ 𝑁 ) − 1 ) ( digit ‘ 2 ) 𝑁 ) = ( ( ⌊ ‘ ( 𝑁 / ( 2 ↑ ( ( #b ‘ 𝑁 ) − 1 ) ) ) ) mod 2 ) )
12 2 5 10 11 syl3anc ⊢ ( 𝑁 ∈ ℕ → ( ( ( #b ‘ 𝑁 ) − 1 ) ( digit ‘ 2 ) 𝑁 ) = ( ( ⌊ ‘ ( 𝑁 / ( 2 ↑ ( ( #b ‘ 𝑁 ) − 1 ) ) ) ) mod 2 ) )
13 n2dvds1 ⊢ ¬ 2 ∥ 1
14 blennn ⊢ ( 𝑁 ∈ ℕ → ( #b ‘ 𝑁 ) = ( ( ⌊ ‘ ( 2 logb 𝑁 ) ) + 1 ) )
15 14 oveq1d ⊢ ( 𝑁 ∈ ℕ → ( ( #b ‘ 𝑁 ) − 1 ) = ( ( ( ⌊ ‘ ( 2 logb 𝑁 ) ) + 1 ) − 1 ) )
16 2z ⊢ 2 ∈ ℤ
17 uzid ⊢ ( 2 ∈ ℤ → 2 ∈ ( ℤ≥ ‘ 2 ) )
18 16 17 ax-mp ⊢ 2 ∈ ( ℤ≥ ‘ 2 )
19 nnrp ⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℝ+ )
20 relogbzcl ⊢ ( ( 2 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℝ+ ) → ( 2 logb 𝑁 ) ∈ ℝ )
21 18 19 20 sylancr ⊢ ( 𝑁 ∈ ℕ → ( 2 logb 𝑁 ) ∈ ℝ )
22 21 flcld ⊢ ( 𝑁 ∈ ℕ → ( ⌊ ‘ ( 2 logb 𝑁 ) ) ∈ ℤ )
23 22 zcnd ⊢ ( 𝑁 ∈ ℕ → ( ⌊ ‘ ( 2 logb 𝑁 ) ) ∈ ℂ )
24 pncan1 ⊢ ( ( ⌊ ‘ ( 2 logb 𝑁 ) ) ∈ ℂ → ( ( ( ⌊ ‘ ( 2 logb 𝑁 ) ) + 1 ) − 1 ) = ( ⌊ ‘ ( 2 logb 𝑁 ) ) )
25 23 24 syl ⊢ ( 𝑁 ∈ ℕ → ( ( ( ⌊ ‘ ( 2 logb 𝑁 ) ) + 1 ) − 1 ) = ( ⌊ ‘ ( 2 logb 𝑁 ) ) )
26 15 25 eqtrd ⊢ ( 𝑁 ∈ ℕ → ( ( #b ‘ 𝑁 ) − 1 ) = ( ⌊ ‘ ( 2 logb 𝑁 ) ) )
27 26 oveq2d ⊢ ( 𝑁 ∈ ℕ → ( 2 ↑ ( ( #b ‘ 𝑁 ) − 1 ) ) = ( 2 ↑ ( ⌊ ‘ ( 2 logb 𝑁 ) ) ) )
28 27 oveq2d ⊢ ( 𝑁 ∈ ℕ → ( 𝑁 / ( 2 ↑ ( ( #b ‘ 𝑁 ) − 1 ) ) ) = ( 𝑁 / ( 2 ↑ ( ⌊ ‘ ( 2 logb 𝑁 ) ) ) ) )
29 28 fveq2d ⊢ ( 𝑁 ∈ ℕ → ( ⌊ ‘ ( 𝑁 / ( 2 ↑ ( ( #b ‘ 𝑁 ) − 1 ) ) ) ) = ( ⌊ ‘ ( 𝑁 / ( 2 ↑ ( ⌊ ‘ ( 2 logb 𝑁 ) ) ) ) ) )
30 fldivexpfllog2 ⊢ ( 𝑁 ∈ ℝ+ → ( ⌊ ‘ ( 𝑁 / ( 2 ↑ ( ⌊ ‘ ( 2 logb 𝑁 ) ) ) ) ) = 1 )
31 19 30 syl ⊢ ( 𝑁 ∈ ℕ → ( ⌊ ‘ ( 𝑁 / ( 2 ↑ ( ⌊ ‘ ( 2 logb 𝑁 ) ) ) ) ) = 1 )
32 29 31 eqtrd ⊢ ( 𝑁 ∈ ℕ → ( ⌊ ‘ ( 𝑁 / ( 2 ↑ ( ( #b ‘ 𝑁 ) − 1 ) ) ) ) = 1 )
33 32 breq2d ⊢ ( 𝑁 ∈ ℕ → ( 2 ∥ ( ⌊ ‘ ( 𝑁 / ( 2 ↑ ( ( #b ‘ 𝑁 ) − 1 ) ) ) ) ↔ 2 ∥ 1 ) )
34 13 33 mtbiri ⊢ ( 𝑁 ∈ ℕ → ¬ 2 ∥ ( ⌊ ‘ ( 𝑁 / ( 2 ↑ ( ( #b ‘ 𝑁 ) − 1 ) ) ) ) )
35 2re ⊢ 2 ∈ ℝ
36 35 a1i ⊢ ( 𝑁 ∈ ℕ → 2 ∈ ℝ )
37 36 5 reexpcld ⊢ ( 𝑁 ∈ ℕ → ( 2 ↑ ( ( #b ‘ 𝑁 ) − 1 ) ) ∈ ℝ )
38 2cnd ⊢ ( 𝑁 ∈ ℕ → 2 ∈ ℂ )
39 2ne0 ⊢ 2 ≠ 0
40 39 a1i ⊢ ( 𝑁 ∈ ℕ → 2 ≠ 0 )
41 5 nn0zd ⊢ ( 𝑁 ∈ ℕ → ( ( #b ‘ 𝑁 ) − 1 ) ∈ ℤ )
42 38 40 41 expne0d ⊢ ( 𝑁 ∈ ℕ → ( 2 ↑ ( ( #b ‘ 𝑁 ) − 1 ) ) ≠ 0 )
43 6 37 42 redivcld ⊢ ( 𝑁 ∈ ℕ → ( 𝑁 / ( 2 ↑ ( ( #b ‘ 𝑁 ) − 1 ) ) ) ∈ ℝ )
44 43 flcld ⊢ ( 𝑁 ∈ ℕ → ( ⌊ ‘ ( 𝑁 / ( 2 ↑ ( ( #b ‘ 𝑁 ) − 1 ) ) ) ) ∈ ℤ )
45 mod2eq1n2dvds ⊢ ( ( ⌊ ‘ ( 𝑁 / ( 2 ↑ ( ( #b ‘ 𝑁 ) − 1 ) ) ) ) ∈ ℤ → ( ( ( ⌊ ‘ ( 𝑁 / ( 2 ↑ ( ( #b ‘ 𝑁 ) − 1 ) ) ) ) mod 2 ) = 1 ↔ ¬ 2 ∥ ( ⌊ ‘ ( 𝑁 / ( 2 ↑ ( ( #b ‘ 𝑁 ) − 1 ) ) ) ) ) )
46 44 45 syl ⊢ ( 𝑁 ∈ ℕ → ( ( ( ⌊ ‘ ( 𝑁 / ( 2 ↑ ( ( #b ‘ 𝑁 ) − 1 ) ) ) ) mod 2 ) = 1 ↔ ¬ 2 ∥ ( ⌊ ‘ ( 𝑁 / ( 2 ↑ ( ( #b ‘ 𝑁 ) − 1 ) ) ) ) ) )
47 34 46 mpbird ⊢ ( 𝑁 ∈ ℕ → ( ( ⌊ ‘ ( 𝑁 / ( 2 ↑ ( ( #b ‘ 𝑁 ) − 1 ) ) ) ) mod 2 ) = 1 )
48 12 47 eqtrd ⊢ ( 𝑁 ∈ ℕ → ( ( ( #b ‘ 𝑁 ) − 1 ) ( digit ‘ 2 ) 𝑁 ) = 1 )