Theorem bitsinv1lem

Description: Lemma for bitsinv1 . (Contributed by Mario Carneiro, 22-Sep-2016)

	Ref	Expression
Assertion	bitsinv1lem	⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) → ( 𝑁 mod ( 2 ↑ ( 𝑀 + 1 ) ) ) = ( ( 𝑁 mod ( 2 ↑ 𝑀 ) ) + if ( 𝑀 ∈ ( bits ‘ 𝑁 ) , ( 2 ↑ 𝑀 ) , 0 ) ) )

Proof

Step	Hyp	Ref	Expression
1		oveq2	⊢ ( ( 2 ↑ 𝑀 ) = if ( 𝑀 ∈ ( bits ‘ 𝑁 ) , ( 2 ↑ 𝑀 ) , 0 ) → ( ( 𝑁 mod ( 2 ↑ 𝑀 ) ) + ( 2 ↑ 𝑀 ) ) = ( ( 𝑁 mod ( 2 ↑ 𝑀 ) ) + if ( 𝑀 ∈ ( bits ‘ 𝑁 ) , ( 2 ↑ 𝑀 ) , 0 ) ) )
2	1	eqeq2d	⊢ ( ( 2 ↑ 𝑀 ) = if ( 𝑀 ∈ ( bits ‘ 𝑁 ) , ( 2 ↑ 𝑀 ) , 0 ) → ( ( 𝑁 mod ( 2 ↑ ( 𝑀 + 1 ) ) ) = ( ( 𝑁 mod ( 2 ↑ 𝑀 ) ) + ( 2 ↑ 𝑀 ) ) ↔ ( 𝑁 mod ( 2 ↑ ( 𝑀 + 1 ) ) ) = ( ( 𝑁 mod ( 2 ↑ 𝑀 ) ) + if ( 𝑀 ∈ ( bits ‘ 𝑁 ) , ( 2 ↑ 𝑀 ) , 0 ) ) ) )
3		oveq2	⊢ ( 0 = if ( 𝑀 ∈ ( bits ‘ 𝑁 ) , ( 2 ↑ 𝑀 ) , 0 ) → ( ( 𝑁 mod ( 2 ↑ 𝑀 ) ) + 0 ) = ( ( 𝑁 mod ( 2 ↑ 𝑀 ) ) + if ( 𝑀 ∈ ( bits ‘ 𝑁 ) , ( 2 ↑ 𝑀 ) , 0 ) ) )
4	3	eqeq2d	⊢ ( 0 = if ( 𝑀 ∈ ( bits ‘ 𝑁 ) , ( 2 ↑ 𝑀 ) , 0 ) → ( ( 𝑁 mod ( 2 ↑ ( 𝑀 + 1 ) ) ) = ( ( 𝑁 mod ( 2 ↑ 𝑀 ) ) + 0 ) ↔ ( 𝑁 mod ( 2 ↑ ( 𝑀 + 1 ) ) ) = ( ( 𝑁 mod ( 2 ↑ 𝑀 ) ) + if ( 𝑀 ∈ ( bits ‘ 𝑁 ) , ( 2 ↑ 𝑀 ) , 0 ) ) ) )
5		simpl	⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) → 𝑁 ∈ ℤ )
6		2nn	⊢ 2 ∈ ℕ
7	6	a1i	⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) → 2 ∈ ℕ )
8		simpr	⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) → 𝑀 ∈ ℕ0 )
9	7 8	nnexpcld	⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) → ( 2 ↑ 𝑀 ) ∈ ℕ )
10	5 9	zmodcld	⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) → ( 𝑁 mod ( 2 ↑ 𝑀 ) ) ∈ ℕ0 )
11	10	nn0cnd	⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) → ( 𝑁 mod ( 2 ↑ 𝑀 ) ) ∈ ℂ )
12	11	adantr	⊢ ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑀 ∈ ( bits ‘ 𝑁 ) ) → ( 𝑁 mod ( 2 ↑ 𝑀 ) ) ∈ ℂ )
13		1nn0	⊢ 1 ∈ ℕ0
14	13	a1i	⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) → 1 ∈ ℕ0 )
15	8 14	nn0addcld	⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) → ( 𝑀 + 1 ) ∈ ℕ0 )
16	7 15	nnexpcld	⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) → ( 2 ↑ ( 𝑀 + 1 ) ) ∈ ℕ )
17	5 16	zmodcld	⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) → ( 𝑁 mod ( 2 ↑ ( 𝑀 + 1 ) ) ) ∈ ℕ0 )
18	17	nn0cnd	⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) → ( 𝑁 mod ( 2 ↑ ( 𝑀 + 1 ) ) ) ∈ ℂ )
19	18	adantr	⊢ ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑀 ∈ ( bits ‘ 𝑁 ) ) → ( 𝑁 mod ( 2 ↑ ( 𝑀 + 1 ) ) ) ∈ ℂ )
20	12 19	pncan3d	⊢ ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑀 ∈ ( bits ‘ 𝑁 ) ) → ( ( 𝑁 mod ( 2 ↑ 𝑀 ) ) + ( ( 𝑁 mod ( 2 ↑ ( 𝑀 + 1 ) ) ) − ( 𝑁 mod ( 2 ↑ 𝑀 ) ) ) ) = ( 𝑁 mod ( 2 ↑ ( 𝑀 + 1 ) ) ) )
21	18 11	subcld	⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) → ( ( 𝑁 mod ( 2 ↑ ( 𝑀 + 1 ) ) ) − ( 𝑁 mod ( 2 ↑ 𝑀 ) ) ) ∈ ℂ )
22	21	adantr	⊢ ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑀 ∈ ( bits ‘ 𝑁 ) ) → ( ( 𝑁 mod ( 2 ↑ ( 𝑀 + 1 ) ) ) − ( 𝑁 mod ( 2 ↑ 𝑀 ) ) ) ∈ ℂ )
23	6	a1i	⊢ ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑀 ∈ ( bits ‘ 𝑁 ) ) → 2 ∈ ℕ )
24		simplr	⊢ ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑀 ∈ ( bits ‘ 𝑁 ) ) → 𝑀 ∈ ℕ0 )
25	23 24	nnexpcld	⊢ ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑀 ∈ ( bits ‘ 𝑁 ) ) → ( 2 ↑ 𝑀 ) ∈ ℕ )
26	25	nncnd	⊢ ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑀 ∈ ( bits ‘ 𝑁 ) ) → ( 2 ↑ 𝑀 ) ∈ ℂ )
27		2cnd	⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) → 2 ∈ ℂ )
28		2ne0	⊢ 2 ≠ 0
29	28	a1i	⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) → 2 ≠ 0 )
30	8	nn0zd	⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) → 𝑀 ∈ ℤ )
31	27 29 30	expne0d	⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) → ( 2 ↑ 𝑀 ) ≠ 0 )
32	31	adantr	⊢ ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑀 ∈ ( bits ‘ 𝑁 ) ) → ( 2 ↑ 𝑀 ) ≠ 0 )
33		z0even	⊢ 2 ∥ 0
34		id	⊢ ( ( ( ( 𝑁 mod ( 2 ↑ ( 𝑀 + 1 ) ) ) − ( 𝑁 mod ( 2 ↑ 𝑀 ) ) ) / ( 2 ↑ 𝑀 ) ) = 0 → ( ( ( 𝑁 mod ( 2 ↑ ( 𝑀 + 1 ) ) ) − ( 𝑁 mod ( 2 ↑ 𝑀 ) ) ) / ( 2 ↑ 𝑀 ) ) = 0 )
35	33 34	breqtrrid	⊢ ( ( ( ( 𝑁 mod ( 2 ↑ ( 𝑀 + 1 ) ) ) − ( 𝑁 mod ( 2 ↑ 𝑀 ) ) ) / ( 2 ↑ 𝑀 ) ) = 0 → 2 ∥ ( ( ( 𝑁 mod ( 2 ↑ ( 𝑀 + 1 ) ) ) − ( 𝑁 mod ( 2 ↑ 𝑀 ) ) ) / ( 2 ↑ 𝑀 ) ) )
36		bitsval2	⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) → ( 𝑀 ∈ ( bits ‘ 𝑁 ) ↔ ¬ 2 ∥ ( ⌊ ‘ ( 𝑁 / ( 2 ↑ 𝑀 ) ) ) ) )
37	5	zred	⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) → 𝑁 ∈ ℝ )
38	9	nnrpd	⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) → ( 2 ↑ 𝑀 ) ∈ ℝ+ )
39		moddiffl	⊢ ( ( 𝑁 ∈ ℝ ∧ ( 2 ↑ 𝑀 ) ∈ ℝ+ ) → ( ( 𝑁 − ( 𝑁 mod ( 2 ↑ 𝑀 ) ) ) / ( 2 ↑ 𝑀 ) ) = ( ⌊ ‘ ( 𝑁 / ( 2 ↑ 𝑀 ) ) ) )
40	37 38 39	syl2anc	⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) → ( ( 𝑁 − ( 𝑁 mod ( 2 ↑ 𝑀 ) ) ) / ( 2 ↑ 𝑀 ) ) = ( ⌊ ‘ ( 𝑁 / ( 2 ↑ 𝑀 ) ) ) )
41	40	breq2d	⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) → ( 2 ∥ ( ( 𝑁 − ( 𝑁 mod ( 2 ↑ 𝑀 ) ) ) / ( 2 ↑ 𝑀 ) ) ↔ 2 ∥ ( ⌊ ‘ ( 𝑁 / ( 2 ↑ 𝑀 ) ) ) ) )
42		2z	⊢ 2 ∈ ℤ
43	42	a1i	⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) → 2 ∈ ℤ )
44		moddifz	⊢ ( ( 𝑁 ∈ ℝ ∧ ( 2 ↑ 𝑀 ) ∈ ℝ+ ) → ( ( 𝑁 − ( 𝑁 mod ( 2 ↑ 𝑀 ) ) ) / ( 2 ↑ 𝑀 ) ) ∈ ℤ )
45	37 38 44	syl2anc	⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) → ( ( 𝑁 − ( 𝑁 mod ( 2 ↑ 𝑀 ) ) ) / ( 2 ↑ 𝑀 ) ) ∈ ℤ )
46	5	zcnd	⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) → 𝑁 ∈ ℂ )
47	46 11 18	nnncan1d	⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) → ( ( 𝑁 − ( 𝑁 mod ( 2 ↑ 𝑀 ) ) ) − ( 𝑁 − ( 𝑁 mod ( 2 ↑ ( 𝑀 + 1 ) ) ) ) ) = ( ( 𝑁 mod ( 2 ↑ ( 𝑀 + 1 ) ) ) − ( 𝑁 mod ( 2 ↑ 𝑀 ) ) ) )
48	47	oveq1d	⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) → ( ( ( 𝑁 − ( 𝑁 mod ( 2 ↑ 𝑀 ) ) ) − ( 𝑁 − ( 𝑁 mod ( 2 ↑ ( 𝑀 + 1 ) ) ) ) ) / ( 2 ↑ 𝑀 ) ) = ( ( ( 𝑁 mod ( 2 ↑ ( 𝑀 + 1 ) ) ) − ( 𝑁 mod ( 2 ↑ 𝑀 ) ) ) / ( 2 ↑ 𝑀 ) ) )
49	46 11	subcld	⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) → ( 𝑁 − ( 𝑁 mod ( 2 ↑ 𝑀 ) ) ) ∈ ℂ )
50	46 18	subcld	⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) → ( 𝑁 − ( 𝑁 mod ( 2 ↑ ( 𝑀 + 1 ) ) ) ) ∈ ℂ )
51	9	nncnd	⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) → ( 2 ↑ 𝑀 ) ∈ ℂ )
52	49 50 51 31	divsubdird	⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) → ( ( ( 𝑁 − ( 𝑁 mod ( 2 ↑ 𝑀 ) ) ) − ( 𝑁 − ( 𝑁 mod ( 2 ↑ ( 𝑀 + 1 ) ) ) ) ) / ( 2 ↑ 𝑀 ) ) = ( ( ( 𝑁 − ( 𝑁 mod ( 2 ↑ 𝑀 ) ) ) / ( 2 ↑ 𝑀 ) ) − ( ( 𝑁 − ( 𝑁 mod ( 2 ↑ ( 𝑀 + 1 ) ) ) ) / ( 2 ↑ 𝑀 ) ) ) )
53	48 52	eqtr3d	⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) → ( ( ( 𝑁 mod ( 2 ↑ ( 𝑀 + 1 ) ) ) − ( 𝑁 mod ( 2 ↑ 𝑀 ) ) ) / ( 2 ↑ 𝑀 ) ) = ( ( ( 𝑁 − ( 𝑁 mod ( 2 ↑ 𝑀 ) ) ) / ( 2 ↑ 𝑀 ) ) − ( ( 𝑁 − ( 𝑁 mod ( 2 ↑ ( 𝑀 + 1 ) ) ) ) / ( 2 ↑ 𝑀 ) ) ) )
54	27 50	mulcomd	⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) → ( 2 · ( 𝑁 − ( 𝑁 mod ( 2 ↑ ( 𝑀 + 1 ) ) ) ) ) = ( ( 𝑁 − ( 𝑁 mod ( 2 ↑ ( 𝑀 + 1 ) ) ) ) · 2 ) )
55	27 51	mulcomd	⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) → ( 2 · ( 2 ↑ 𝑀 ) ) = ( ( 2 ↑ 𝑀 ) · 2 ) )
56	27 8	expp1d	⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) → ( 2 ↑ ( 𝑀 + 1 ) ) = ( ( 2 ↑ 𝑀 ) · 2 ) )
57	55 56	eqtr4d	⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) → ( 2 · ( 2 ↑ 𝑀 ) ) = ( 2 ↑ ( 𝑀 + 1 ) ) )
58	54 57	oveq12d	⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) → ( ( 2 · ( 𝑁 − ( 𝑁 mod ( 2 ↑ ( 𝑀 + 1 ) ) ) ) ) / ( 2 · ( 2 ↑ 𝑀 ) ) ) = ( ( ( 𝑁 − ( 𝑁 mod ( 2 ↑ ( 𝑀 + 1 ) ) ) ) · 2 ) / ( 2 ↑ ( 𝑀 + 1 ) ) ) )
59	50 51 27 31 29	divcan5d	⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) → ( ( 2 · ( 𝑁 − ( 𝑁 mod ( 2 ↑ ( 𝑀 + 1 ) ) ) ) ) / ( 2 · ( 2 ↑ 𝑀 ) ) ) = ( ( 𝑁 − ( 𝑁 mod ( 2 ↑ ( 𝑀 + 1 ) ) ) ) / ( 2 ↑ 𝑀 ) ) )
60	16	nncnd	⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) → ( 2 ↑ ( 𝑀 + 1 ) ) ∈ ℂ )
61	30	peano2zd	⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) → ( 𝑀 + 1 ) ∈ ℤ )
62	27 29 61	expne0d	⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) → ( 2 ↑ ( 𝑀 + 1 ) ) ≠ 0 )
63	50 27 60 62	div23d	⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) → ( ( ( 𝑁 − ( 𝑁 mod ( 2 ↑ ( 𝑀 + 1 ) ) ) ) · 2 ) / ( 2 ↑ ( 𝑀 + 1 ) ) ) = ( ( ( 𝑁 − ( 𝑁 mod ( 2 ↑ ( 𝑀 + 1 ) ) ) ) / ( 2 ↑ ( 𝑀 + 1 ) ) ) · 2 ) )
64	58 59 63	3eqtr3d	⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) → ( ( 𝑁 − ( 𝑁 mod ( 2 ↑ ( 𝑀 + 1 ) ) ) ) / ( 2 ↑ 𝑀 ) ) = ( ( ( 𝑁 − ( 𝑁 mod ( 2 ↑ ( 𝑀 + 1 ) ) ) ) / ( 2 ↑ ( 𝑀 + 1 ) ) ) · 2 ) )
65	16	nnrpd	⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) → ( 2 ↑ ( 𝑀 + 1 ) ) ∈ ℝ+ )
66		moddifz	⊢ ( ( 𝑁 ∈ ℝ ∧ ( 2 ↑ ( 𝑀 + 1 ) ) ∈ ℝ+ ) → ( ( 𝑁 − ( 𝑁 mod ( 2 ↑ ( 𝑀 + 1 ) ) ) ) / ( 2 ↑ ( 𝑀 + 1 ) ) ) ∈ ℤ )
67	37 65 66	syl2anc	⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) → ( ( 𝑁 − ( 𝑁 mod ( 2 ↑ ( 𝑀 + 1 ) ) ) ) / ( 2 ↑ ( 𝑀 + 1 ) ) ) ∈ ℤ )
68	67 43	zmulcld	⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) → ( ( ( 𝑁 − ( 𝑁 mod ( 2 ↑ ( 𝑀 + 1 ) ) ) ) / ( 2 ↑ ( 𝑀 + 1 ) ) ) · 2 ) ∈ ℤ )
69	64 68	eqeltrd	⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) → ( ( 𝑁 − ( 𝑁 mod ( 2 ↑ ( 𝑀 + 1 ) ) ) ) / ( 2 ↑ 𝑀 ) ) ∈ ℤ )
70	45 69	zsubcld	⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) → ( ( ( 𝑁 − ( 𝑁 mod ( 2 ↑ 𝑀 ) ) ) / ( 2 ↑ 𝑀 ) ) − ( ( 𝑁 − ( 𝑁 mod ( 2 ↑ ( 𝑀 + 1 ) ) ) ) / ( 2 ↑ 𝑀 ) ) ) ∈ ℤ )
71	53 70	eqeltrd	⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) → ( ( ( 𝑁 mod ( 2 ↑ ( 𝑀 + 1 ) ) ) − ( 𝑁 mod ( 2 ↑ 𝑀 ) ) ) / ( 2 ↑ 𝑀 ) ) ∈ ℤ )
72		dvdsmul2	⊢ ( ( ( ( 𝑁 − ( 𝑁 mod ( 2 ↑ ( 𝑀 + 1 ) ) ) ) / ( 2 ↑ ( 𝑀 + 1 ) ) ) ∈ ℤ ∧ 2 ∈ ℤ ) → 2 ∥ ( ( ( 𝑁 − ( 𝑁 mod ( 2 ↑ ( 𝑀 + 1 ) ) ) ) / ( 2 ↑ ( 𝑀 + 1 ) ) ) · 2 ) )
73	67 43 72	syl2anc	⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) → 2 ∥ ( ( ( 𝑁 − ( 𝑁 mod ( 2 ↑ ( 𝑀 + 1 ) ) ) ) / ( 2 ↑ ( 𝑀 + 1 ) ) ) · 2 ) )
74	46 18 11	nnncan2d	⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) → ( ( 𝑁 − ( 𝑁 mod ( 2 ↑ 𝑀 ) ) ) − ( ( 𝑁 mod ( 2 ↑ ( 𝑀 + 1 ) ) ) − ( 𝑁 mod ( 2 ↑ 𝑀 ) ) ) ) = ( 𝑁 − ( 𝑁 mod ( 2 ↑ ( 𝑀 + 1 ) ) ) ) )
75	74	oveq1d	⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) → ( ( ( 𝑁 − ( 𝑁 mod ( 2 ↑ 𝑀 ) ) ) − ( ( 𝑁 mod ( 2 ↑ ( 𝑀 + 1 ) ) ) − ( 𝑁 mod ( 2 ↑ 𝑀 ) ) ) ) / ( 2 ↑ 𝑀 ) ) = ( ( 𝑁 − ( 𝑁 mod ( 2 ↑ ( 𝑀 + 1 ) ) ) ) / ( 2 ↑ 𝑀 ) ) )
76	49 21 51 31	divsubdird	⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) → ( ( ( 𝑁 − ( 𝑁 mod ( 2 ↑ 𝑀 ) ) ) − ( ( 𝑁 mod ( 2 ↑ ( 𝑀 + 1 ) ) ) − ( 𝑁 mod ( 2 ↑ 𝑀 ) ) ) ) / ( 2 ↑ 𝑀 ) ) = ( ( ( 𝑁 − ( 𝑁 mod ( 2 ↑ 𝑀 ) ) ) / ( 2 ↑ 𝑀 ) ) − ( ( ( 𝑁 mod ( 2 ↑ ( 𝑀 + 1 ) ) ) − ( 𝑁 mod ( 2 ↑ 𝑀 ) ) ) / ( 2 ↑ 𝑀 ) ) ) )
77	75 76 64	3eqtr3d	⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) → ( ( ( 𝑁 − ( 𝑁 mod ( 2 ↑ 𝑀 ) ) ) / ( 2 ↑ 𝑀 ) ) − ( ( ( 𝑁 mod ( 2 ↑ ( 𝑀 + 1 ) ) ) − ( 𝑁 mod ( 2 ↑ 𝑀 ) ) ) / ( 2 ↑ 𝑀 ) ) ) = ( ( ( 𝑁 − ( 𝑁 mod ( 2 ↑ ( 𝑀 + 1 ) ) ) ) / ( 2 ↑ ( 𝑀 + 1 ) ) ) · 2 ) )
78	73 77	breqtrrd	⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) → 2 ∥ ( ( ( 𝑁 − ( 𝑁 mod ( 2 ↑ 𝑀 ) ) ) / ( 2 ↑ 𝑀 ) ) − ( ( ( 𝑁 mod ( 2 ↑ ( 𝑀 + 1 ) ) ) − ( 𝑁 mod ( 2 ↑ 𝑀 ) ) ) / ( 2 ↑ 𝑀 ) ) ) )
79		dvdssub2	⊢ ( ( ( 2 ∈ ℤ ∧ ( ( 𝑁 − ( 𝑁 mod ( 2 ↑ 𝑀 ) ) ) / ( 2 ↑ 𝑀 ) ) ∈ ℤ ∧ ( ( ( 𝑁 mod ( 2 ↑ ( 𝑀 + 1 ) ) ) − ( 𝑁 mod ( 2 ↑ 𝑀 ) ) ) / ( 2 ↑ 𝑀 ) ) ∈ ℤ ) ∧ 2 ∥ ( ( ( 𝑁 − ( 𝑁 mod ( 2 ↑ 𝑀 ) ) ) / ( 2 ↑ 𝑀 ) ) − ( ( ( 𝑁 mod ( 2 ↑ ( 𝑀 + 1 ) ) ) − ( 𝑁 mod ( 2 ↑ 𝑀 ) ) ) / ( 2 ↑ 𝑀 ) ) ) ) → ( 2 ∥ ( ( 𝑁 − ( 𝑁 mod ( 2 ↑ 𝑀 ) ) ) / ( 2 ↑ 𝑀 ) ) ↔ 2 ∥ ( ( ( 𝑁 mod ( 2 ↑ ( 𝑀 + 1 ) ) ) − ( 𝑁 mod ( 2 ↑ 𝑀 ) ) ) / ( 2 ↑ 𝑀 ) ) ) )
80	43 45 71 78 79	syl31anc	⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) → ( 2 ∥ ( ( 𝑁 − ( 𝑁 mod ( 2 ↑ 𝑀 ) ) ) / ( 2 ↑ 𝑀 ) ) ↔ 2 ∥ ( ( ( 𝑁 mod ( 2 ↑ ( 𝑀 + 1 ) ) ) − ( 𝑁 mod ( 2 ↑ 𝑀 ) ) ) / ( 2 ↑ 𝑀 ) ) ) )
81	41 80	bitr3d	⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) → ( 2 ∥ ( ⌊ ‘ ( 𝑁 / ( 2 ↑ 𝑀 ) ) ) ↔ 2 ∥ ( ( ( 𝑁 mod ( 2 ↑ ( 𝑀 + 1 ) ) ) − ( 𝑁 mod ( 2 ↑ 𝑀 ) ) ) / ( 2 ↑ 𝑀 ) ) ) )
82	81	notbid	⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) → ( ¬ 2 ∥ ( ⌊ ‘ ( 𝑁 / ( 2 ↑ 𝑀 ) ) ) ↔ ¬ 2 ∥ ( ( ( 𝑁 mod ( 2 ↑ ( 𝑀 + 1 ) ) ) − ( 𝑁 mod ( 2 ↑ 𝑀 ) ) ) / ( 2 ↑ 𝑀 ) ) ) )
83	36 82	bitrd	⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) → ( 𝑀 ∈ ( bits ‘ 𝑁 ) ↔ ¬ 2 ∥ ( ( ( 𝑁 mod ( 2 ↑ ( 𝑀 + 1 ) ) ) − ( 𝑁 mod ( 2 ↑ 𝑀 ) ) ) / ( 2 ↑ 𝑀 ) ) ) )
84	83	con2bid	⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) → ( 2 ∥ ( ( ( 𝑁 mod ( 2 ↑ ( 𝑀 + 1 ) ) ) − ( 𝑁 mod ( 2 ↑ 𝑀 ) ) ) / ( 2 ↑ 𝑀 ) ) ↔ ¬ 𝑀 ∈ ( bits ‘ 𝑁 ) ) )
85	35 84	imbitrid	⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) → ( ( ( ( 𝑁 mod ( 2 ↑ ( 𝑀 + 1 ) ) ) − ( 𝑁 mod ( 2 ↑ 𝑀 ) ) ) / ( 2 ↑ 𝑀 ) ) = 0 → ¬ 𝑀 ∈ ( bits ‘ 𝑁 ) ) )
86	85	con2d	⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) → ( 𝑀 ∈ ( bits ‘ 𝑁 ) → ¬ ( ( ( 𝑁 mod ( 2 ↑ ( 𝑀 + 1 ) ) ) − ( 𝑁 mod ( 2 ↑ 𝑀 ) ) ) / ( 2 ↑ 𝑀 ) ) = 0 ) )
87		df-neg	⊢ - 1 = ( 0 − 1 )
88	51	mulm1d	⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) → ( - 1 · ( 2 ↑ 𝑀 ) ) = - ( 2 ↑ 𝑀 ) )
89	9	nnred	⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) → ( 2 ↑ 𝑀 ) ∈ ℝ )
90	89	renegcld	⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) → - ( 2 ↑ 𝑀 ) ∈ ℝ )
91	37 38	modcld	⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) → ( 𝑁 mod ( 2 ↑ 𝑀 ) ) ∈ ℝ )
92	91	renegcld	⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) → - ( 𝑁 mod ( 2 ↑ 𝑀 ) ) ∈ ℝ )
93	37 65	modcld	⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) → ( 𝑁 mod ( 2 ↑ ( 𝑀 + 1 ) ) ) ∈ ℝ )
94	93 91	resubcld	⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) → ( ( 𝑁 mod ( 2 ↑ ( 𝑀 + 1 ) ) ) − ( 𝑁 mod ( 2 ↑ 𝑀 ) ) ) ∈ ℝ )
95		modlt	⊢ ( ( 𝑁 ∈ ℝ ∧ ( 2 ↑ 𝑀 ) ∈ ℝ+ ) → ( 𝑁 mod ( 2 ↑ 𝑀 ) ) < ( 2 ↑ 𝑀 ) )
96	37 38 95	syl2anc	⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) → ( 𝑁 mod ( 2 ↑ 𝑀 ) ) < ( 2 ↑ 𝑀 ) )
97	91 89	ltnegd	⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) → ( ( 𝑁 mod ( 2 ↑ 𝑀 ) ) < ( 2 ↑ 𝑀 ) ↔ - ( 2 ↑ 𝑀 ) < - ( 𝑁 mod ( 2 ↑ 𝑀 ) ) ) )
98	96 97	mpbid	⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) → - ( 2 ↑ 𝑀 ) < - ( 𝑁 mod ( 2 ↑ 𝑀 ) ) )
99		df-neg	⊢ - ( 𝑁 mod ( 2 ↑ 𝑀 ) ) = ( 0 − ( 𝑁 mod ( 2 ↑ 𝑀 ) ) )
100		0red	⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) → 0 ∈ ℝ )
101		modge0	⊢ ( ( 𝑁 ∈ ℝ ∧ ( 2 ↑ ( 𝑀 + 1 ) ) ∈ ℝ+ ) → 0 ≤ ( 𝑁 mod ( 2 ↑ ( 𝑀 + 1 ) ) ) )
102	37 65 101	syl2anc	⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) → 0 ≤ ( 𝑁 mod ( 2 ↑ ( 𝑀 + 1 ) ) ) )
103	100 93 91 102	lesub1dd	⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) → ( 0 − ( 𝑁 mod ( 2 ↑ 𝑀 ) ) ) ≤ ( ( 𝑁 mod ( 2 ↑ ( 𝑀 + 1 ) ) ) − ( 𝑁 mod ( 2 ↑ 𝑀 ) ) ) )
104	99 103	eqbrtrid	⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) → - ( 𝑁 mod ( 2 ↑ 𝑀 ) ) ≤ ( ( 𝑁 mod ( 2 ↑ ( 𝑀 + 1 ) ) ) − ( 𝑁 mod ( 2 ↑ 𝑀 ) ) ) )
105	90 92 94 98 104	ltletrd	⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) → - ( 2 ↑ 𝑀 ) < ( ( 𝑁 mod ( 2 ↑ ( 𝑀 + 1 ) ) ) − ( 𝑁 mod ( 2 ↑ 𝑀 ) ) ) )
106	88 105	eqbrtrd	⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) → ( - 1 · ( 2 ↑ 𝑀 ) ) < ( ( 𝑁 mod ( 2 ↑ ( 𝑀 + 1 ) ) ) − ( 𝑁 mod ( 2 ↑ 𝑀 ) ) ) )
107		1red	⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) → 1 ∈ ℝ )
108	107	renegcld	⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) → - 1 ∈ ℝ )
109	108 94 38	ltmuldivd	⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) → ( ( - 1 · ( 2 ↑ 𝑀 ) ) < ( ( 𝑁 mod ( 2 ↑ ( 𝑀 + 1 ) ) ) − ( 𝑁 mod ( 2 ↑ 𝑀 ) ) ) ↔ - 1 < ( ( ( 𝑁 mod ( 2 ↑ ( 𝑀 + 1 ) ) ) − ( 𝑁 mod ( 2 ↑ 𝑀 ) ) ) / ( 2 ↑ 𝑀 ) ) ) )
110	106 109	mpbid	⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) → - 1 < ( ( ( 𝑁 mod ( 2 ↑ ( 𝑀 + 1 ) ) ) − ( 𝑁 mod ( 2 ↑ 𝑀 ) ) ) / ( 2 ↑ 𝑀 ) ) )
111	87 110	eqbrtrrid	⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) → ( 0 − 1 ) < ( ( ( 𝑁 mod ( 2 ↑ ( 𝑀 + 1 ) ) ) − ( 𝑁 mod ( 2 ↑ 𝑀 ) ) ) / ( 2 ↑ 𝑀 ) ) )
112		0zd	⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) → 0 ∈ ℤ )
113		zlem1lt	⊢ ( ( 0 ∈ ℤ ∧ ( ( ( 𝑁 mod ( 2 ↑ ( 𝑀 + 1 ) ) ) − ( 𝑁 mod ( 2 ↑ 𝑀 ) ) ) / ( 2 ↑ 𝑀 ) ) ∈ ℤ ) → ( 0 ≤ ( ( ( 𝑁 mod ( 2 ↑ ( 𝑀 + 1 ) ) ) − ( 𝑁 mod ( 2 ↑ 𝑀 ) ) ) / ( 2 ↑ 𝑀 ) ) ↔ ( 0 − 1 ) < ( ( ( 𝑁 mod ( 2 ↑ ( 𝑀 + 1 ) ) ) − ( 𝑁 mod ( 2 ↑ 𝑀 ) ) ) / ( 2 ↑ 𝑀 ) ) ) )
114	112 71 113	syl2anc	⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) → ( 0 ≤ ( ( ( 𝑁 mod ( 2 ↑ ( 𝑀 + 1 ) ) ) − ( 𝑁 mod ( 2 ↑ 𝑀 ) ) ) / ( 2 ↑ 𝑀 ) ) ↔ ( 0 − 1 ) < ( ( ( 𝑁 mod ( 2 ↑ ( 𝑀 + 1 ) ) ) − ( 𝑁 mod ( 2 ↑ 𝑀 ) ) ) / ( 2 ↑ 𝑀 ) ) ) )
115	111 114	mpbird	⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) → 0 ≤ ( ( ( 𝑁 mod ( 2 ↑ ( 𝑀 + 1 ) ) ) − ( 𝑁 mod ( 2 ↑ 𝑀 ) ) ) / ( 2 ↑ 𝑀 ) ) )
116		elnn0z	⊢ ( ( ( ( 𝑁 mod ( 2 ↑ ( 𝑀 + 1 ) ) ) − ( 𝑁 mod ( 2 ↑ 𝑀 ) ) ) / ( 2 ↑ 𝑀 ) ) ∈ ℕ0 ↔ ( ( ( ( 𝑁 mod ( 2 ↑ ( 𝑀 + 1 ) ) ) − ( 𝑁 mod ( 2 ↑ 𝑀 ) ) ) / ( 2 ↑ 𝑀 ) ) ∈ ℤ ∧ 0 ≤ ( ( ( 𝑁 mod ( 2 ↑ ( 𝑀 + 1 ) ) ) − ( 𝑁 mod ( 2 ↑ 𝑀 ) ) ) / ( 2 ↑ 𝑀 ) ) ) )
117	71 115 116	sylanbrc	⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) → ( ( ( 𝑁 mod ( 2 ↑ ( 𝑀 + 1 ) ) ) − ( 𝑁 mod ( 2 ↑ 𝑀 ) ) ) / ( 2 ↑ 𝑀 ) ) ∈ ℕ0 )
118		nn0uz	⊢ ℕ0 = ( ℤ≥ ‘ 0 )
119	117 118	eleqtrdi	⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) → ( ( ( 𝑁 mod ( 2 ↑ ( 𝑀 + 1 ) ) ) − ( 𝑁 mod ( 2 ↑ 𝑀 ) ) ) / ( 2 ↑ 𝑀 ) ) ∈ ( ℤ≥ ‘ 0 ) )
120	16	nnred	⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) → ( 2 ↑ ( 𝑀 + 1 ) ) ∈ ℝ )
121		modge0	⊢ ( ( 𝑁 ∈ ℝ ∧ ( 2 ↑ 𝑀 ) ∈ ℝ+ ) → 0 ≤ ( 𝑁 mod ( 2 ↑ 𝑀 ) ) )
122	37 38 121	syl2anc	⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) → 0 ≤ ( 𝑁 mod ( 2 ↑ 𝑀 ) ) )
123	93 91	subge02d	⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) → ( 0 ≤ ( 𝑁 mod ( 2 ↑ 𝑀 ) ) ↔ ( ( 𝑁 mod ( 2 ↑ ( 𝑀 + 1 ) ) ) − ( 𝑁 mod ( 2 ↑ 𝑀 ) ) ) ≤ ( 𝑁 mod ( 2 ↑ ( 𝑀 + 1 ) ) ) ) )
124	122 123	mpbid	⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) → ( ( 𝑁 mod ( 2 ↑ ( 𝑀 + 1 ) ) ) − ( 𝑁 mod ( 2 ↑ 𝑀 ) ) ) ≤ ( 𝑁 mod ( 2 ↑ ( 𝑀 + 1 ) ) ) )
125		modlt	⊢ ( ( 𝑁 ∈ ℝ ∧ ( 2 ↑ ( 𝑀 + 1 ) ) ∈ ℝ+ ) → ( 𝑁 mod ( 2 ↑ ( 𝑀 + 1 ) ) ) < ( 2 ↑ ( 𝑀 + 1 ) ) )
126	37 65 125	syl2anc	⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) → ( 𝑁 mod ( 2 ↑ ( 𝑀 + 1 ) ) ) < ( 2 ↑ ( 𝑀 + 1 ) ) )
127	94 93 120 124 126	lelttrd	⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) → ( ( 𝑁 mod ( 2 ↑ ( 𝑀 + 1 ) ) ) − ( 𝑁 mod ( 2 ↑ 𝑀 ) ) ) < ( 2 ↑ ( 𝑀 + 1 ) ) )
128	127 56	breqtrd	⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) → ( ( 𝑁 mod ( 2 ↑ ( 𝑀 + 1 ) ) ) − ( 𝑁 mod ( 2 ↑ 𝑀 ) ) ) < ( ( 2 ↑ 𝑀 ) · 2 ) )
129	7	nnred	⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) → 2 ∈ ℝ )
130	94 129 38	ltdivmuld	⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) → ( ( ( ( 𝑁 mod ( 2 ↑ ( 𝑀 + 1 ) ) ) − ( 𝑁 mod ( 2 ↑ 𝑀 ) ) ) / ( 2 ↑ 𝑀 ) ) < 2 ↔ ( ( 𝑁 mod ( 2 ↑ ( 𝑀 + 1 ) ) ) − ( 𝑁 mod ( 2 ↑ 𝑀 ) ) ) < ( ( 2 ↑ 𝑀 ) · 2 ) ) )
131	128 130	mpbird	⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) → ( ( ( 𝑁 mod ( 2 ↑ ( 𝑀 + 1 ) ) ) − ( 𝑁 mod ( 2 ↑ 𝑀 ) ) ) / ( 2 ↑ 𝑀 ) ) < 2 )
132		elfzo2	⊢ ( ( ( ( 𝑁 mod ( 2 ↑ ( 𝑀 + 1 ) ) ) − ( 𝑁 mod ( 2 ↑ 𝑀 ) ) ) / ( 2 ↑ 𝑀 ) ) ∈ ( 0 ..^ 2 ) ↔ ( ( ( ( 𝑁 mod ( 2 ↑ ( 𝑀 + 1 ) ) ) − ( 𝑁 mod ( 2 ↑ 𝑀 ) ) ) / ( 2 ↑ 𝑀 ) ) ∈ ( ℤ≥ ‘ 0 ) ∧ 2 ∈ ℤ ∧ ( ( ( 𝑁 mod ( 2 ↑ ( 𝑀 + 1 ) ) ) − ( 𝑁 mod ( 2 ↑ 𝑀 ) ) ) / ( 2 ↑ 𝑀 ) ) < 2 ) )
133	119 43 131 132	syl3anbrc	⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) → ( ( ( 𝑁 mod ( 2 ↑ ( 𝑀 + 1 ) ) ) − ( 𝑁 mod ( 2 ↑ 𝑀 ) ) ) / ( 2 ↑ 𝑀 ) ) ∈ ( 0 ..^ 2 ) )
134		fzo0to2pr	⊢ ( 0 ..^ 2 ) = { 0 , 1 }
135	133 134	eleqtrdi	⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) → ( ( ( 𝑁 mod ( 2 ↑ ( 𝑀 + 1 ) ) ) − ( 𝑁 mod ( 2 ↑ 𝑀 ) ) ) / ( 2 ↑ 𝑀 ) ) ∈ { 0 , 1 } )
136		elpri	⊢ ( ( ( ( 𝑁 mod ( 2 ↑ ( 𝑀 + 1 ) ) ) − ( 𝑁 mod ( 2 ↑ 𝑀 ) ) ) / ( 2 ↑ 𝑀 ) ) ∈ { 0 , 1 } → ( ( ( ( 𝑁 mod ( 2 ↑ ( 𝑀 + 1 ) ) ) − ( 𝑁 mod ( 2 ↑ 𝑀 ) ) ) / ( 2 ↑ 𝑀 ) ) = 0 ∨ ( ( ( 𝑁 mod ( 2 ↑ ( 𝑀 + 1 ) ) ) − ( 𝑁 mod ( 2 ↑ 𝑀 ) ) ) / ( 2 ↑ 𝑀 ) ) = 1 ) )
137	135 136	syl	⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) → ( ( ( ( 𝑁 mod ( 2 ↑ ( 𝑀 + 1 ) ) ) − ( 𝑁 mod ( 2 ↑ 𝑀 ) ) ) / ( 2 ↑ 𝑀 ) ) = 0 ∨ ( ( ( 𝑁 mod ( 2 ↑ ( 𝑀 + 1 ) ) ) − ( 𝑁 mod ( 2 ↑ 𝑀 ) ) ) / ( 2 ↑ 𝑀 ) ) = 1 ) )
138	137	ord	⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) → ( ¬ ( ( ( 𝑁 mod ( 2 ↑ ( 𝑀 + 1 ) ) ) − ( 𝑁 mod ( 2 ↑ 𝑀 ) ) ) / ( 2 ↑ 𝑀 ) ) = 0 → ( ( ( 𝑁 mod ( 2 ↑ ( 𝑀 + 1 ) ) ) − ( 𝑁 mod ( 2 ↑ 𝑀 ) ) ) / ( 2 ↑ 𝑀 ) ) = 1 ) )
139	86 138	syld	⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) → ( 𝑀 ∈ ( bits ‘ 𝑁 ) → ( ( ( 𝑁 mod ( 2 ↑ ( 𝑀 + 1 ) ) ) − ( 𝑁 mod ( 2 ↑ 𝑀 ) ) ) / ( 2 ↑ 𝑀 ) ) = 1 ) )
140	139	imp	⊢ ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑀 ∈ ( bits ‘ 𝑁 ) ) → ( ( ( 𝑁 mod ( 2 ↑ ( 𝑀 + 1 ) ) ) − ( 𝑁 mod ( 2 ↑ 𝑀 ) ) ) / ( 2 ↑ 𝑀 ) ) = 1 )
141	22 26 32 140	diveq1d	⊢ ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑀 ∈ ( bits ‘ 𝑁 ) ) → ( ( 𝑁 mod ( 2 ↑ ( 𝑀 + 1 ) ) ) − ( 𝑁 mod ( 2 ↑ 𝑀 ) ) ) = ( 2 ↑ 𝑀 ) )
142	141	oveq2d	⊢ ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑀 ∈ ( bits ‘ 𝑁 ) ) → ( ( 𝑁 mod ( 2 ↑ 𝑀 ) ) + ( ( 𝑁 mod ( 2 ↑ ( 𝑀 + 1 ) ) ) − ( 𝑁 mod ( 2 ↑ 𝑀 ) ) ) ) = ( ( 𝑁 mod ( 2 ↑ 𝑀 ) ) + ( 2 ↑ 𝑀 ) ) )
143	20 142	eqtr3d	⊢ ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑀 ∈ ( bits ‘ 𝑁 ) ) → ( 𝑁 mod ( 2 ↑ ( 𝑀 + 1 ) ) ) = ( ( 𝑁 mod ( 2 ↑ 𝑀 ) ) + ( 2 ↑ 𝑀 ) ) )
144	18	adantr	⊢ ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ ¬ 𝑀 ∈ ( bits ‘ 𝑁 ) ) → ( 𝑁 mod ( 2 ↑ ( 𝑀 + 1 ) ) ) ∈ ℂ )
145	11	adantr	⊢ ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ ¬ 𝑀 ∈ ( bits ‘ 𝑁 ) ) → ( 𝑁 mod ( 2 ↑ 𝑀 ) ) ∈ ℂ )
146	21	adantr	⊢ ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ ¬ 𝑀 ∈ ( bits ‘ 𝑁 ) ) → ( ( 𝑁 mod ( 2 ↑ ( 𝑀 + 1 ) ) ) − ( 𝑁 mod ( 2 ↑ 𝑀 ) ) ) ∈ ℂ )
147	51	adantr	⊢ ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ ¬ 𝑀 ∈ ( bits ‘ 𝑁 ) ) → ( 2 ↑ 𝑀 ) ∈ ℂ )
148	31	adantr	⊢ ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ ¬ 𝑀 ∈ ( bits ‘ 𝑁 ) ) → ( 2 ↑ 𝑀 ) ≠ 0 )
149		n2dvds1	⊢ ¬ 2 ∥ 1
150		breq2	⊢ ( ( ( ( 𝑁 mod ( 2 ↑ ( 𝑀 + 1 ) ) ) − ( 𝑁 mod ( 2 ↑ 𝑀 ) ) ) / ( 2 ↑ 𝑀 ) ) = 1 → ( 2 ∥ ( ( ( 𝑁 mod ( 2 ↑ ( 𝑀 + 1 ) ) ) − ( 𝑁 mod ( 2 ↑ 𝑀 ) ) ) / ( 2 ↑ 𝑀 ) ) ↔ 2 ∥ 1 ) )
151	149 150	mtbiri	⊢ ( ( ( ( 𝑁 mod ( 2 ↑ ( 𝑀 + 1 ) ) ) − ( 𝑁 mod ( 2 ↑ 𝑀 ) ) ) / ( 2 ↑ 𝑀 ) ) = 1 → ¬ 2 ∥ ( ( ( 𝑁 mod ( 2 ↑ ( 𝑀 + 1 ) ) ) − ( 𝑁 mod ( 2 ↑ 𝑀 ) ) ) / ( 2 ↑ 𝑀 ) ) )
152	138 151	syl6	⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) → ( ¬ ( ( ( 𝑁 mod ( 2 ↑ ( 𝑀 + 1 ) ) ) − ( 𝑁 mod ( 2 ↑ 𝑀 ) ) ) / ( 2 ↑ 𝑀 ) ) = 0 → ¬ 2 ∥ ( ( ( 𝑁 mod ( 2 ↑ ( 𝑀 + 1 ) ) ) − ( 𝑁 mod ( 2 ↑ 𝑀 ) ) ) / ( 2 ↑ 𝑀 ) ) ) )
153	152 83	sylibrd	⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) → ( ¬ ( ( ( 𝑁 mod ( 2 ↑ ( 𝑀 + 1 ) ) ) − ( 𝑁 mod ( 2 ↑ 𝑀 ) ) ) / ( 2 ↑ 𝑀 ) ) = 0 → 𝑀 ∈ ( bits ‘ 𝑁 ) ) )
154	153	con1d	⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) → ( ¬ 𝑀 ∈ ( bits ‘ 𝑁 ) → ( ( ( 𝑁 mod ( 2 ↑ ( 𝑀 + 1 ) ) ) − ( 𝑁 mod ( 2 ↑ 𝑀 ) ) ) / ( 2 ↑ 𝑀 ) ) = 0 ) )
155	154	imp	⊢ ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ ¬ 𝑀 ∈ ( bits ‘ 𝑁 ) ) → ( ( ( 𝑁 mod ( 2 ↑ ( 𝑀 + 1 ) ) ) − ( 𝑁 mod ( 2 ↑ 𝑀 ) ) ) / ( 2 ↑ 𝑀 ) ) = 0 )
156	146 147 148 155	diveq0d	⊢ ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ ¬ 𝑀 ∈ ( bits ‘ 𝑁 ) ) → ( ( 𝑁 mod ( 2 ↑ ( 𝑀 + 1 ) ) ) − ( 𝑁 mod ( 2 ↑ 𝑀 ) ) ) = 0 )
157	144 145 156	subeq0d	⊢ ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ ¬ 𝑀 ∈ ( bits ‘ 𝑁 ) ) → ( 𝑁 mod ( 2 ↑ ( 𝑀 + 1 ) ) ) = ( 𝑁 mod ( 2 ↑ 𝑀 ) ) )
158	145	addridd	⊢ ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ ¬ 𝑀 ∈ ( bits ‘ 𝑁 ) ) → ( ( 𝑁 mod ( 2 ↑ 𝑀 ) ) + 0 ) = ( 𝑁 mod ( 2 ↑ 𝑀 ) ) )
159	157 158	eqtr4d	⊢ ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ ¬ 𝑀 ∈ ( bits ‘ 𝑁 ) ) → ( 𝑁 mod ( 2 ↑ ( 𝑀 + 1 ) ) ) = ( ( 𝑁 mod ( 2 ↑ 𝑀 ) ) + 0 ) )
160	2 4 143 159	ifbothda	⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) → ( 𝑁 mod ( 2 ↑ ( 𝑀 + 1 ) ) ) = ( ( 𝑁 mod ( 2 ↑ 𝑀 ) ) + if ( 𝑀 ∈ ( bits ‘ 𝑁 ) , ( 2 ↑ 𝑀 ) , 0 ) ) )