Theorem dig2bits

Description: The K th digit of a nonnegative integer N in a binary system is its K th bit. (Contributed by AV, 24-May-2020)

	Ref	Expression
Assertion	dig2bits	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ℕ0 ) → ( ( 𝐾 ( digit ‘ 2 ) 𝑁 ) = 1 ↔ 𝐾 ∈ ( bits ‘ 𝑁 ) ) )

Proof

Step	Hyp	Ref	Expression
1		nn0re	⊢ ( 𝑁 ∈ ℕ0 → 𝑁 ∈ ℝ )
2	1	adantr	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ℕ0 ) → 𝑁 ∈ ℝ )
3		2re	⊢ 2 ∈ ℝ
4	3	a1i	⊢ ( 𝑁 ∈ ℕ0 → 2 ∈ ℝ )
5		reexpcl	⊢ ( ( 2 ∈ ℝ ∧ 𝐾 ∈ ℕ0 ) → ( 2 ↑ 𝐾 ) ∈ ℝ )
6	4 5	sylan	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ℕ0 ) → ( 2 ↑ 𝐾 ) ∈ ℝ )
7		2cnd	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ℕ0 ) → 2 ∈ ℂ )
8		2ne0	⊢ 2 ≠ 0
9	8	a1i	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ℕ0 ) → 2 ≠ 0 )
10		nn0z	⊢ ( 𝐾 ∈ ℕ0 → 𝐾 ∈ ℤ )
11	10	adantl	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ℕ0 ) → 𝐾 ∈ ℤ )
12	7 9 11	expne0d	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ℕ0 ) → ( 2 ↑ 𝐾 ) ≠ 0 )
13	2 6 12	redivcld	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ℕ0 ) → ( 𝑁 / ( 2 ↑ 𝐾 ) ) ∈ ℝ )
14	13	flcld	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ℕ0 ) → ( ⌊ ‘ ( 𝑁 / ( 2 ↑ 𝐾 ) ) ) ∈ ℤ )
15		mod2eq1n2dvds	⊢ ( ( ⌊ ‘ ( 𝑁 / ( 2 ↑ 𝐾 ) ) ) ∈ ℤ → ( ( ( ⌊ ‘ ( 𝑁 / ( 2 ↑ 𝐾 ) ) ) mod 2 ) = 1 ↔ ¬ 2 ∥ ( ⌊ ‘ ( 𝑁 / ( 2 ↑ 𝐾 ) ) ) ) )
16	14 15	syl	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ℕ0 ) → ( ( ( ⌊ ‘ ( 𝑁 / ( 2 ↑ 𝐾 ) ) ) mod 2 ) = 1 ↔ ¬ 2 ∥ ( ⌊ ‘ ( 𝑁 / ( 2 ↑ 𝐾 ) ) ) ) )
17		2nn	⊢ 2 ∈ ℕ
18	17	a1i	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ℕ0 ) → 2 ∈ ℕ )
19		simpr	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ℕ0 ) → 𝐾 ∈ ℕ0 )
20		nn0rp0	⊢ ( 𝑁 ∈ ℕ0 → 𝑁 ∈ ( 0 [,) +∞ ) )
21	20	adantr	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ℕ0 ) → 𝑁 ∈ ( 0 [,) +∞ ) )
22		nn0digval	⊢ ( ( 2 ∈ ℕ ∧ 𝐾 ∈ ℕ0 ∧ 𝑁 ∈ ( 0 [,) +∞ ) ) → ( 𝐾 ( digit ‘ 2 ) 𝑁 ) = ( ( ⌊ ‘ ( 𝑁 / ( 2 ↑ 𝐾 ) ) ) mod 2 ) )
23	18 19 21 22	syl3anc	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ℕ0 ) → ( 𝐾 ( digit ‘ 2 ) 𝑁 ) = ( ( ⌊ ‘ ( 𝑁 / ( 2 ↑ 𝐾 ) ) ) mod 2 ) )
24	23	eqeq1d	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ℕ0 ) → ( ( 𝐾 ( digit ‘ 2 ) 𝑁 ) = 1 ↔ ( ( ⌊ ‘ ( 𝑁 / ( 2 ↑ 𝐾 ) ) ) mod 2 ) = 1 ) )
25		nn0z	⊢ ( 𝑁 ∈ ℕ0 → 𝑁 ∈ ℤ )
26		bitsval2	⊢ ( ( 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℕ0 ) → ( 𝐾 ∈ ( bits ‘ 𝑁 ) ↔ ¬ 2 ∥ ( ⌊ ‘ ( 𝑁 / ( 2 ↑ 𝐾 ) ) ) ) )
27	25 26	sylan	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ℕ0 ) → ( 𝐾 ∈ ( bits ‘ 𝑁 ) ↔ ¬ 2 ∥ ( ⌊ ‘ ( 𝑁 / ( 2 ↑ 𝐾 ) ) ) ) )
28	16 24 27	3bitr4d	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ℕ0 ) → ( ( 𝐾 ( digit ‘ 2 ) 𝑁 ) = 1 ↔ 𝐾 ∈ ( bits ‘ 𝑁 ) ) )