Theorem bitsp1

Description: The M + 1 -th bit of N is the M -th bit of |_ ( N / 2 ) . (Contributed by Mario Carneiro, 5-Sep-2016)

	Ref	Expression
Assertion	bitsp1	⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) → ( ( 𝑀 + 1 ) ∈ ( bits ‘ 𝑁 ) ↔ 𝑀 ∈ ( bits ‘ ( ⌊ ‘ ( 𝑁 / 2 ) ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		2nn	⊢ 2 ∈ ℕ
2	1	a1i	⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) → 2 ∈ ℕ )
3	2	nncnd	⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) → 2 ∈ ℂ )
4		simpr	⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) → 𝑀 ∈ ℕ0 )
5	3 4	expp1d	⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) → ( 2 ↑ ( 𝑀 + 1 ) ) = ( ( 2 ↑ 𝑀 ) · 2 ) )
6	2 4	nnexpcld	⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) → ( 2 ↑ 𝑀 ) ∈ ℕ )
7	6	nncnd	⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) → ( 2 ↑ 𝑀 ) ∈ ℂ )
8	7 3	mulcomd	⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) → ( ( 2 ↑ 𝑀 ) · 2 ) = ( 2 · ( 2 ↑ 𝑀 ) ) )
9	5 8	eqtrd	⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) → ( 2 ↑ ( 𝑀 + 1 ) ) = ( 2 · ( 2 ↑ 𝑀 ) ) )
10	9	oveq2d	⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) → ( 𝑁 / ( 2 ↑ ( 𝑀 + 1 ) ) ) = ( 𝑁 / ( 2 · ( 2 ↑ 𝑀 ) ) ) )
11		simpl	⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) → 𝑁 ∈ ℤ )
12	11	zcnd	⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) → 𝑁 ∈ ℂ )
13	2	nnne0d	⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) → 2 ≠ 0 )
14	6	nnne0d	⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) → ( 2 ↑ 𝑀 ) ≠ 0 )
15	12 3 7 13 14	divdiv1d	⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) → ( ( 𝑁 / 2 ) / ( 2 ↑ 𝑀 ) ) = ( 𝑁 / ( 2 · ( 2 ↑ 𝑀 ) ) ) )
16	10 15	eqtr4d	⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) → ( 𝑁 / ( 2 ↑ ( 𝑀 + 1 ) ) ) = ( ( 𝑁 / 2 ) / ( 2 ↑ 𝑀 ) ) )
17	16	fveq2d	⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) → ( ⌊ ‘ ( 𝑁 / ( 2 ↑ ( 𝑀 + 1 ) ) ) ) = ( ⌊ ‘ ( ( 𝑁 / 2 ) / ( 2 ↑ 𝑀 ) ) ) )
18	11	zred	⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) → 𝑁 ∈ ℝ )
19	18	rehalfcld	⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) → ( 𝑁 / 2 ) ∈ ℝ )
20		fldiv	⊢ ( ( ( 𝑁 / 2 ) ∈ ℝ ∧ ( 2 ↑ 𝑀 ) ∈ ℕ ) → ( ⌊ ‘ ( ( ⌊ ‘ ( 𝑁 / 2 ) ) / ( 2 ↑ 𝑀 ) ) ) = ( ⌊ ‘ ( ( 𝑁 / 2 ) / ( 2 ↑ 𝑀 ) ) ) )
21	19 6 20	syl2anc	⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) → ( ⌊ ‘ ( ( ⌊ ‘ ( 𝑁 / 2 ) ) / ( 2 ↑ 𝑀 ) ) ) = ( ⌊ ‘ ( ( 𝑁 / 2 ) / ( 2 ↑ 𝑀 ) ) ) )
22	17 21	eqtr4d	⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) → ( ⌊ ‘ ( 𝑁 / ( 2 ↑ ( 𝑀 + 1 ) ) ) ) = ( ⌊ ‘ ( ( ⌊ ‘ ( 𝑁 / 2 ) ) / ( 2 ↑ 𝑀 ) ) ) )
23	22	breq2d	⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) → ( 2 ∥ ( ⌊ ‘ ( 𝑁 / ( 2 ↑ ( 𝑀 + 1 ) ) ) ) ↔ 2 ∥ ( ⌊ ‘ ( ( ⌊ ‘ ( 𝑁 / 2 ) ) / ( 2 ↑ 𝑀 ) ) ) ) )
24	23	notbid	⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) → ( ¬ 2 ∥ ( ⌊ ‘ ( 𝑁 / ( 2 ↑ ( 𝑀 + 1 ) ) ) ) ↔ ¬ 2 ∥ ( ⌊ ‘ ( ( ⌊ ‘ ( 𝑁 / 2 ) ) / ( 2 ↑ 𝑀 ) ) ) ) )
25		peano2nn0	⊢ ( 𝑀 ∈ ℕ0 → ( 𝑀 + 1 ) ∈ ℕ0 )
26		bitsval2	⊢ ( ( 𝑁 ∈ ℤ ∧ ( 𝑀 + 1 ) ∈ ℕ0 ) → ( ( 𝑀 + 1 ) ∈ ( bits ‘ 𝑁 ) ↔ ¬ 2 ∥ ( ⌊ ‘ ( 𝑁 / ( 2 ↑ ( 𝑀 + 1 ) ) ) ) ) )
27	25 26	sylan2	⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) → ( ( 𝑀 + 1 ) ∈ ( bits ‘ 𝑁 ) ↔ ¬ 2 ∥ ( ⌊ ‘ ( 𝑁 / ( 2 ↑ ( 𝑀 + 1 ) ) ) ) ) )
28	19	flcld	⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) → ( ⌊ ‘ ( 𝑁 / 2 ) ) ∈ ℤ )
29		bitsval2	⊢ ( ( ( ⌊ ‘ ( 𝑁 / 2 ) ) ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) → ( 𝑀 ∈ ( bits ‘ ( ⌊ ‘ ( 𝑁 / 2 ) ) ) ↔ ¬ 2 ∥ ( ⌊ ‘ ( ( ⌊ ‘ ( 𝑁 / 2 ) ) / ( 2 ↑ 𝑀 ) ) ) ) )
30	28 29	sylancom	⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) → ( 𝑀 ∈ ( bits ‘ ( ⌊ ‘ ( 𝑁 / 2 ) ) ) ↔ ¬ 2 ∥ ( ⌊ ‘ ( ( ⌊ ‘ ( 𝑁 / 2 ) ) / ( 2 ↑ 𝑀 ) ) ) ) )
31	24 27 30	3bitr4d	⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) → ( ( 𝑀 + 1 ) ∈ ( bits ‘ 𝑁 ) ↔ 𝑀 ∈ ( bits ‘ ( ⌊ ‘ ( 𝑁 / 2 ) ) ) ) )