Theorem bitsval

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

	Ref	Expression
Assertion	bitsval	⊢ ( 𝑀 ∈ ( bits ‘ 𝑁 ) ↔ ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ∧ ¬ 2 ∥ ( ⌊ ‘ ( 𝑁 / ( 2 ↑ 𝑀 ) ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		df-bits	⊢ bits = ( 𝑛 ∈ ℤ ↦ { 𝑚 ∈ ℕ0 ∣ ¬ 2 ∥ ( ⌊ ‘ ( 𝑛 / ( 2 ↑ 𝑚 ) ) ) } )
2	1	mptrcl	⊢ ( 𝑀 ∈ ( bits ‘ 𝑁 ) → 𝑁 ∈ ℤ )
3		bitsfval	⊢ ( 𝑁 ∈ ℤ → ( bits ‘ 𝑁 ) = { 𝑚 ∈ ℕ0 ∣ ¬ 2 ∥ ( ⌊ ‘ ( 𝑁 / ( 2 ↑ 𝑚 ) ) ) } )
4	3	eleq2d	⊢ ( 𝑁 ∈ ℤ → ( 𝑀 ∈ ( bits ‘ 𝑁 ) ↔ 𝑀 ∈ { 𝑚 ∈ ℕ0 ∣ ¬ 2 ∥ ( ⌊ ‘ ( 𝑁 / ( 2 ↑ 𝑚 ) ) ) } ) )
5		oveq2	⊢ ( 𝑚 = 𝑀 → ( 2 ↑ 𝑚 ) = ( 2 ↑ 𝑀 ) )
6	5	oveq2d	⊢ ( 𝑚 = 𝑀 → ( 𝑁 / ( 2 ↑ 𝑚 ) ) = ( 𝑁 / ( 2 ↑ 𝑀 ) ) )
7	6	fveq2d	⊢ ( 𝑚 = 𝑀 → ( ⌊ ‘ ( 𝑁 / ( 2 ↑ 𝑚 ) ) ) = ( ⌊ ‘ ( 𝑁 / ( 2 ↑ 𝑀 ) ) ) )
8	7	breq2d	⊢ ( 𝑚 = 𝑀 → ( 2 ∥ ( ⌊ ‘ ( 𝑁 / ( 2 ↑ 𝑚 ) ) ) ↔ 2 ∥ ( ⌊ ‘ ( 𝑁 / ( 2 ↑ 𝑀 ) ) ) ) )
9	8	notbid	⊢ ( 𝑚 = 𝑀 → ( ¬ 2 ∥ ( ⌊ ‘ ( 𝑁 / ( 2 ↑ 𝑚 ) ) ) ↔ ¬ 2 ∥ ( ⌊ ‘ ( 𝑁 / ( 2 ↑ 𝑀 ) ) ) ) )
10	9	elrab	⊢ ( 𝑀 ∈ { 𝑚 ∈ ℕ0 ∣ ¬ 2 ∥ ( ⌊ ‘ ( 𝑁 / ( 2 ↑ 𝑚 ) ) ) } ↔ ( 𝑀 ∈ ℕ0 ∧ ¬ 2 ∥ ( ⌊ ‘ ( 𝑁 / ( 2 ↑ 𝑀 ) ) ) ) )
11	4 10	bitrdi	⊢ ( 𝑁 ∈ ℤ → ( 𝑀 ∈ ( bits ‘ 𝑁 ) ↔ ( 𝑀 ∈ ℕ0 ∧ ¬ 2 ∥ ( ⌊ ‘ ( 𝑁 / ( 2 ↑ 𝑀 ) ) ) ) ) )
12	2 11	biadanii	⊢ ( 𝑀 ∈ ( bits ‘ 𝑁 ) ↔ ( 𝑁 ∈ ℤ ∧ ( 𝑀 ∈ ℕ0 ∧ ¬ 2 ∥ ( ⌊ ‘ ( 𝑁 / ( 2 ↑ 𝑀 ) ) ) ) ) )
13		3anass	⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ∧ ¬ 2 ∥ ( ⌊ ‘ ( 𝑁 / ( 2 ↑ 𝑀 ) ) ) ) ↔ ( 𝑁 ∈ ℤ ∧ ( 𝑀 ∈ ℕ0 ∧ ¬ 2 ∥ ( ⌊ ‘ ( 𝑁 / ( 2 ↑ 𝑀 ) ) ) ) ) )
14	12 13	bitr4i	⊢ ( 𝑀 ∈ ( bits ‘ 𝑁 ) ↔ ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ∧ ¬ 2 ∥ ( ⌊ ‘ ( 𝑁 / ( 2 ↑ 𝑀 ) ) ) ) )