Theorem bitsfval

Description: Expand the definition of the bits of an integer. (Contributed by Mario Carneiro, 5-Sep-2016)

	Ref	Expression
Assertion	bitsfval	⊢ ( 𝑁 ∈ ℤ → ( bits ‘ 𝑁 ) = { 𝑚 ∈ ℕ0 ∣ ¬ 2 ∥ ( ⌊ ‘ ( 𝑁 / ( 2 ↑ 𝑚 ) ) ) } )

Proof

Step	Hyp	Ref	Expression
1		fvoveq1	⊢ ( 𝑛 = 𝑁 → ( ⌊ ‘ ( 𝑛 / ( 2 ↑ 𝑚 ) ) ) = ( ⌊ ‘ ( 𝑁 / ( 2 ↑ 𝑚 ) ) ) )
2	1	breq2d	⊢ ( 𝑛 = 𝑁 → ( 2 ∥ ( ⌊ ‘ ( 𝑛 / ( 2 ↑ 𝑚 ) ) ) ↔ 2 ∥ ( ⌊ ‘ ( 𝑁 / ( 2 ↑ 𝑚 ) ) ) ) )
3	2	notbid	⊢ ( 𝑛 = 𝑁 → ( ¬ 2 ∥ ( ⌊ ‘ ( 𝑛 / ( 2 ↑ 𝑚 ) ) ) ↔ ¬ 2 ∥ ( ⌊ ‘ ( 𝑁 / ( 2 ↑ 𝑚 ) ) ) ) )
4	3	rabbidv	⊢ ( 𝑛 = 𝑁 → { 𝑚 ∈ ℕ0 ∣ ¬ 2 ∥ ( ⌊ ‘ ( 𝑛 / ( 2 ↑ 𝑚 ) ) ) } = { 𝑚 ∈ ℕ0 ∣ ¬ 2 ∥ ( ⌊ ‘ ( 𝑁 / ( 2 ↑ 𝑚 ) ) ) } )
5		df-bits	⊢ bits = ( 𝑛 ∈ ℤ ↦ { 𝑚 ∈ ℕ0 ∣ ¬ 2 ∥ ( ⌊ ‘ ( 𝑛 / ( 2 ↑ 𝑚 ) ) ) } )
6		nn0ex	⊢ ℕ0 ∈ V
7	6	rabex	⊢ { 𝑚 ∈ ℕ0 ∣ ¬ 2 ∥ ( ⌊ ‘ ( 𝑁 / ( 2 ↑ 𝑚 ) ) ) } ∈ V
8	4 5 7	fvmpt	⊢ ( 𝑁 ∈ ℤ → ( bits ‘ 𝑁 ) = { 𝑚 ∈ ℕ0 ∣ ¬ 2 ∥ ( ⌊ ‘ ( 𝑁 / ( 2 ↑ 𝑚 ) ) ) } )