Theorem bitsmod

Description: Truncating the bit sequence after some M is equivalent to reducing the argument mod 2 ^ M . (Contributed by Mario Carneiro, 6-Sep-2016)

	Ref	Expression
Assertion	bitsmod	⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) → ( bits ‘ ( 𝑁 mod ( 2 ↑ 𝑀 ) ) ) = ( ( bits ‘ 𝑁 ) ∩ ( 0 ..^ 𝑀 ) ) )

Proof

Step	Hyp	Ref	Expression
1		simpl	⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) → 𝑁 ∈ ℤ )
2		2nn	⊢ 2 ∈ ℕ
3	2	a1i	⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) → 2 ∈ ℕ )
4		simpr	⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) → 𝑀 ∈ ℕ0 )
5	3 4	nnexpcld	⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) → ( 2 ↑ 𝑀 ) ∈ ℕ )
6	1 5	zmodcld	⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) → ( 𝑁 mod ( 2 ↑ 𝑀 ) ) ∈ ℕ0 )
7	6	nn0zd	⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) → ( 𝑁 mod ( 2 ↑ 𝑀 ) ) ∈ ℤ )
8	7	biantrurd	⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) → ( ( 𝑥 ∈ ℕ0 ∧ ¬ 2 ∥ ( ⌊ ‘ ( ( 𝑁 mod ( 2 ↑ 𝑀 ) ) / ( 2 ↑ 𝑥 ) ) ) ) ↔ ( ( 𝑁 mod ( 2 ↑ 𝑀 ) ) ∈ ℤ ∧ ( 𝑥 ∈ ℕ0 ∧ ¬ 2 ∥ ( ⌊ ‘ ( ( 𝑁 mod ( 2 ↑ 𝑀 ) ) / ( 2 ↑ 𝑥 ) ) ) ) ) ) )
9	1	ad2antrr	⊢ ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) ∧ 𝑥 < 𝑀 ) → 𝑁 ∈ ℤ )
10		simplr	⊢ ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) ∧ 𝑥 < 𝑀 ) → 𝑥 ∈ ℕ0 )
11		bitsval2	⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑥 ∈ ℕ0 ) → ( 𝑥 ∈ ( bits ‘ 𝑁 ) ↔ ¬ 2 ∥ ( ⌊ ‘ ( 𝑁 / ( 2 ↑ 𝑥 ) ) ) ) )
12	9 10 11	syl2anc	⊢ ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) ∧ 𝑥 < 𝑀 ) → ( 𝑥 ∈ ( bits ‘ 𝑁 ) ↔ ¬ 2 ∥ ( ⌊ ‘ ( 𝑁 / ( 2 ↑ 𝑥 ) ) ) ) )
13		simpr	⊢ ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) ∧ 𝑥 < 𝑀 ) → 𝑥 < 𝑀 )
14	13	biantrud	⊢ ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) ∧ 𝑥 < 𝑀 ) → ( 𝑥 ∈ ( bits ‘ 𝑁 ) ↔ ( 𝑥 ∈ ( bits ‘ 𝑁 ) ∧ 𝑥 < 𝑀 ) ) )
15		2z	⊢ 2 ∈ ℤ
16	15	a1i	⊢ ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) ∧ 𝑥 < 𝑀 ) → 2 ∈ ℤ )
17	9	zred	⊢ ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) ∧ 𝑥 < 𝑀 ) → 𝑁 ∈ ℝ )
18	2	a1i	⊢ ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) ∧ 𝑥 < 𝑀 ) → 2 ∈ ℕ )
19	18 10	nnexpcld	⊢ ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) ∧ 𝑥 < 𝑀 ) → ( 2 ↑ 𝑥 ) ∈ ℕ )
20	17 19	nndivred	⊢ ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) ∧ 𝑥 < 𝑀 ) → ( 𝑁 / ( 2 ↑ 𝑥 ) ) ∈ ℝ )
21	20	flcld	⊢ ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) ∧ 𝑥 < 𝑀 ) → ( ⌊ ‘ ( 𝑁 / ( 2 ↑ 𝑥 ) ) ) ∈ ℤ )
22	7	ad2antrr	⊢ ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) ∧ 𝑥 < 𝑀 ) → ( 𝑁 mod ( 2 ↑ 𝑀 ) ) ∈ ℤ )
23	22	zred	⊢ ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) ∧ 𝑥 < 𝑀 ) → ( 𝑁 mod ( 2 ↑ 𝑀 ) ) ∈ ℝ )
24	23 19	nndivred	⊢ ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) ∧ 𝑥 < 𝑀 ) → ( ( 𝑁 mod ( 2 ↑ 𝑀 ) ) / ( 2 ↑ 𝑥 ) ) ∈ ℝ )
25	24	flcld	⊢ ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) ∧ 𝑥 < 𝑀 ) → ( ⌊ ‘ ( ( 𝑁 mod ( 2 ↑ 𝑀 ) ) / ( 2 ↑ 𝑥 ) ) ) ∈ ℤ )
26	19	nnzd	⊢ ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) ∧ 𝑥 < 𝑀 ) → ( 2 ↑ 𝑥 ) ∈ ℤ )
27	26 16	zmulcld	⊢ ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) ∧ 𝑥 < 𝑀 ) → ( ( 2 ↑ 𝑥 ) · 2 ) ∈ ℤ )
28	5	ad2antrr	⊢ ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) ∧ 𝑥 < 𝑀 ) → ( 2 ↑ 𝑀 ) ∈ ℕ )
29	28	nnzd	⊢ ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) ∧ 𝑥 < 𝑀 ) → ( 2 ↑ 𝑀 ) ∈ ℤ )
30	9 22	zsubcld	⊢ ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) ∧ 𝑥 < 𝑀 ) → ( 𝑁 − ( 𝑁 mod ( 2 ↑ 𝑀 ) ) ) ∈ ℤ )
31		2cnd	⊢ ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) ∧ 𝑥 < 𝑀 ) → 2 ∈ ℂ )
32	31 10	expp1d	⊢ ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) ∧ 𝑥 < 𝑀 ) → ( 2 ↑ ( 𝑥 + 1 ) ) = ( ( 2 ↑ 𝑥 ) · 2 ) )
33		1nn0	⊢ 1 ∈ ℕ0
34	33	a1i	⊢ ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) ∧ 𝑥 < 𝑀 ) → 1 ∈ ℕ0 )
35	10 34	nn0addcld	⊢ ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) ∧ 𝑥 < 𝑀 ) → ( 𝑥 + 1 ) ∈ ℕ0 )
36	35	nn0zd	⊢ ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) ∧ 𝑥 < 𝑀 ) → ( 𝑥 + 1 ) ∈ ℤ )
37		simplr	⊢ ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) → 𝑀 ∈ ℕ0 )
38	37	adantr	⊢ ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) ∧ 𝑥 < 𝑀 ) → 𝑀 ∈ ℕ0 )
39	38	nn0zd	⊢ ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) ∧ 𝑥 < 𝑀 ) → 𝑀 ∈ ℤ )
40		nn0ltp1le	⊢ ( ( 𝑥 ∈ ℕ0 ∧ 𝑀 ∈ ℕ0 ) → ( 𝑥 < 𝑀 ↔ ( 𝑥 + 1 ) ≤ 𝑀 ) )
41	10 38 40	syl2anc	⊢ ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) ∧ 𝑥 < 𝑀 ) → ( 𝑥 < 𝑀 ↔ ( 𝑥 + 1 ) ≤ 𝑀 ) )
42	13 41	mpbid	⊢ ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) ∧ 𝑥 < 𝑀 ) → ( 𝑥 + 1 ) ≤ 𝑀 )
43		eluz2	⊢ ( 𝑀 ∈ ( ℤ≥ ‘ ( 𝑥 + 1 ) ) ↔ ( ( 𝑥 + 1 ) ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ ( 𝑥 + 1 ) ≤ 𝑀 ) )
44	36 39 42 43	syl3anbrc	⊢ ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) ∧ 𝑥 < 𝑀 ) → 𝑀 ∈ ( ℤ≥ ‘ ( 𝑥 + 1 ) ) )
45		dvdsexp	⊢ ( ( 2 ∈ ℤ ∧ ( 𝑥 + 1 ) ∈ ℕ0 ∧ 𝑀 ∈ ( ℤ≥ ‘ ( 𝑥 + 1 ) ) ) → ( 2 ↑ ( 𝑥 + 1 ) ) ∥ ( 2 ↑ 𝑀 ) )
46	16 35 44 45	syl3anc	⊢ ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) ∧ 𝑥 < 𝑀 ) → ( 2 ↑ ( 𝑥 + 1 ) ) ∥ ( 2 ↑ 𝑀 ) )
47	32 46	eqbrtrrd	⊢ ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) ∧ 𝑥 < 𝑀 ) → ( ( 2 ↑ 𝑥 ) · 2 ) ∥ ( 2 ↑ 𝑀 ) )
48	28	nnrpd	⊢ ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) ∧ 𝑥 < 𝑀 ) → ( 2 ↑ 𝑀 ) ∈ ℝ+ )
49		moddifz	⊢ ( ( 𝑁 ∈ ℝ ∧ ( 2 ↑ 𝑀 ) ∈ ℝ+ ) → ( ( 𝑁 − ( 𝑁 mod ( 2 ↑ 𝑀 ) ) ) / ( 2 ↑ 𝑀 ) ) ∈ ℤ )
50	17 48 49	syl2anc	⊢ ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) ∧ 𝑥 < 𝑀 ) → ( ( 𝑁 − ( 𝑁 mod ( 2 ↑ 𝑀 ) ) ) / ( 2 ↑ 𝑀 ) ) ∈ ℤ )
51		2ne0	⊢ 2 ≠ 0
52	51	a1i	⊢ ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) ∧ 𝑥 < 𝑀 ) → 2 ≠ 0 )
53	31 52 39	expne0d	⊢ ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) ∧ 𝑥 < 𝑀 ) → ( 2 ↑ 𝑀 ) ≠ 0 )
54		dvdsval2	⊢ ( ( ( 2 ↑ 𝑀 ) ∈ ℤ ∧ ( 2 ↑ 𝑀 ) ≠ 0 ∧ ( 𝑁 − ( 𝑁 mod ( 2 ↑ 𝑀 ) ) ) ∈ ℤ ) → ( ( 2 ↑ 𝑀 ) ∥ ( 𝑁 − ( 𝑁 mod ( 2 ↑ 𝑀 ) ) ) ↔ ( ( 𝑁 − ( 𝑁 mod ( 2 ↑ 𝑀 ) ) ) / ( 2 ↑ 𝑀 ) ) ∈ ℤ ) )
55	29 53 30 54	syl3anc	⊢ ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) ∧ 𝑥 < 𝑀 ) → ( ( 2 ↑ 𝑀 ) ∥ ( 𝑁 − ( 𝑁 mod ( 2 ↑ 𝑀 ) ) ) ↔ ( ( 𝑁 − ( 𝑁 mod ( 2 ↑ 𝑀 ) ) ) / ( 2 ↑ 𝑀 ) ) ∈ ℤ ) )
56	50 55	mpbird	⊢ ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) ∧ 𝑥 < 𝑀 ) → ( 2 ↑ 𝑀 ) ∥ ( 𝑁 − ( 𝑁 mod ( 2 ↑ 𝑀 ) ) ) )
57	27 29 30 47 56	dvdstrd	⊢ ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) ∧ 𝑥 < 𝑀 ) → ( ( 2 ↑ 𝑥 ) · 2 ) ∥ ( 𝑁 − ( 𝑁 mod ( 2 ↑ 𝑀 ) ) ) )
58	30	zcnd	⊢ ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) ∧ 𝑥 < 𝑀 ) → ( 𝑁 − ( 𝑁 mod ( 2 ↑ 𝑀 ) ) ) ∈ ℂ )
59	19	nncnd	⊢ ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) ∧ 𝑥 < 𝑀 ) → ( 2 ↑ 𝑥 ) ∈ ℂ )
60	10	nn0zd	⊢ ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) ∧ 𝑥 < 𝑀 ) → 𝑥 ∈ ℤ )
61	31 52 60	expne0d	⊢ ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) ∧ 𝑥 < 𝑀 ) → ( 2 ↑ 𝑥 ) ≠ 0 )
62	58 59 61	divcan2d	⊢ ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) ∧ 𝑥 < 𝑀 ) → ( ( 2 ↑ 𝑥 ) · ( ( 𝑁 − ( 𝑁 mod ( 2 ↑ 𝑀 ) ) ) / ( 2 ↑ 𝑥 ) ) ) = ( 𝑁 − ( 𝑁 mod ( 2 ↑ 𝑀 ) ) ) )
63	57 62	breqtrrd	⊢ ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) ∧ 𝑥 < 𝑀 ) → ( ( 2 ↑ 𝑥 ) · 2 ) ∥ ( ( 2 ↑ 𝑥 ) · ( ( 𝑁 − ( 𝑁 mod ( 2 ↑ 𝑀 ) ) ) / ( 2 ↑ 𝑥 ) ) ) )
64	10	nn0red	⊢ ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) ∧ 𝑥 < 𝑀 ) → 𝑥 ∈ ℝ )
65	38	nn0red	⊢ ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) ∧ 𝑥 < 𝑀 ) → 𝑀 ∈ ℝ )
66	64 65 13	ltled	⊢ ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) ∧ 𝑥 < 𝑀 ) → 𝑥 ≤ 𝑀 )
67		eluz2	⊢ ( 𝑀 ∈ ( ℤ≥ ‘ 𝑥 ) ↔ ( 𝑥 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑥 ≤ 𝑀 ) )
68	60 39 66 67	syl3anbrc	⊢ ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) ∧ 𝑥 < 𝑀 ) → 𝑀 ∈ ( ℤ≥ ‘ 𝑥 ) )
69		dvdsexp	⊢ ( ( 2 ∈ ℤ ∧ 𝑥 ∈ ℕ0 ∧ 𝑀 ∈ ( ℤ≥ ‘ 𝑥 ) ) → ( 2 ↑ 𝑥 ) ∥ ( 2 ↑ 𝑀 ) )
70	16 10 68 69	syl3anc	⊢ ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) ∧ 𝑥 < 𝑀 ) → ( 2 ↑ 𝑥 ) ∥ ( 2 ↑ 𝑀 ) )
71	26 29 30 70 56	dvdstrd	⊢ ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) ∧ 𝑥 < 𝑀 ) → ( 2 ↑ 𝑥 ) ∥ ( 𝑁 − ( 𝑁 mod ( 2 ↑ 𝑀 ) ) ) )
72		dvdsval2	⊢ ( ( ( 2 ↑ 𝑥 ) ∈ ℤ ∧ ( 2 ↑ 𝑥 ) ≠ 0 ∧ ( 𝑁 − ( 𝑁 mod ( 2 ↑ 𝑀 ) ) ) ∈ ℤ ) → ( ( 2 ↑ 𝑥 ) ∥ ( 𝑁 − ( 𝑁 mod ( 2 ↑ 𝑀 ) ) ) ↔ ( ( 𝑁 − ( 𝑁 mod ( 2 ↑ 𝑀 ) ) ) / ( 2 ↑ 𝑥 ) ) ∈ ℤ ) )
73	26 61 30 72	syl3anc	⊢ ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) ∧ 𝑥 < 𝑀 ) → ( ( 2 ↑ 𝑥 ) ∥ ( 𝑁 − ( 𝑁 mod ( 2 ↑ 𝑀 ) ) ) ↔ ( ( 𝑁 − ( 𝑁 mod ( 2 ↑ 𝑀 ) ) ) / ( 2 ↑ 𝑥 ) ) ∈ ℤ ) )
74	71 73	mpbid	⊢ ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) ∧ 𝑥 < 𝑀 ) → ( ( 𝑁 − ( 𝑁 mod ( 2 ↑ 𝑀 ) ) ) / ( 2 ↑ 𝑥 ) ) ∈ ℤ )
75		dvdscmulr	⊢ ( ( 2 ∈ ℤ ∧ ( ( 𝑁 − ( 𝑁 mod ( 2 ↑ 𝑀 ) ) ) / ( 2 ↑ 𝑥 ) ) ∈ ℤ ∧ ( ( 2 ↑ 𝑥 ) ∈ ℤ ∧ ( 2 ↑ 𝑥 ) ≠ 0 ) ) → ( ( ( 2 ↑ 𝑥 ) · 2 ) ∥ ( ( 2 ↑ 𝑥 ) · ( ( 𝑁 − ( 𝑁 mod ( 2 ↑ 𝑀 ) ) ) / ( 2 ↑ 𝑥 ) ) ) ↔ 2 ∥ ( ( 𝑁 − ( 𝑁 mod ( 2 ↑ 𝑀 ) ) ) / ( 2 ↑ 𝑥 ) ) ) )
76	16 74 26 61 75	syl112anc	⊢ ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) ∧ 𝑥 < 𝑀 ) → ( ( ( 2 ↑ 𝑥 ) · 2 ) ∥ ( ( 2 ↑ 𝑥 ) · ( ( 𝑁 − ( 𝑁 mod ( 2 ↑ 𝑀 ) ) ) / ( 2 ↑ 𝑥 ) ) ) ↔ 2 ∥ ( ( 𝑁 − ( 𝑁 mod ( 2 ↑ 𝑀 ) ) ) / ( 2 ↑ 𝑥 ) ) ) )
77	63 76	mpbid	⊢ ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) ∧ 𝑥 < 𝑀 ) → 2 ∥ ( ( 𝑁 − ( 𝑁 mod ( 2 ↑ 𝑀 ) ) ) / ( 2 ↑ 𝑥 ) ) )
78	25	zcnd	⊢ ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) ∧ 𝑥 < 𝑀 ) → ( ⌊ ‘ ( ( 𝑁 mod ( 2 ↑ 𝑀 ) ) / ( 2 ↑ 𝑥 ) ) ) ∈ ℂ )
79	74	zcnd	⊢ ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) ∧ 𝑥 < 𝑀 ) → ( ( 𝑁 − ( 𝑁 mod ( 2 ↑ 𝑀 ) ) ) / ( 2 ↑ 𝑥 ) ) ∈ ℂ )
80	22	zcnd	⊢ ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) ∧ 𝑥 < 𝑀 ) → ( 𝑁 mod ( 2 ↑ 𝑀 ) ) ∈ ℂ )
81	9	zcnd	⊢ ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) ∧ 𝑥 < 𝑀 ) → 𝑁 ∈ ℂ )
82	80 81	pncan3d	⊢ ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) ∧ 𝑥 < 𝑀 ) → ( ( 𝑁 mod ( 2 ↑ 𝑀 ) ) + ( 𝑁 − ( 𝑁 mod ( 2 ↑ 𝑀 ) ) ) ) = 𝑁 )
83	82	oveq1d	⊢ ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) ∧ 𝑥 < 𝑀 ) → ( ( ( 𝑁 mod ( 2 ↑ 𝑀 ) ) + ( 𝑁 − ( 𝑁 mod ( 2 ↑ 𝑀 ) ) ) ) / ( 2 ↑ 𝑥 ) ) = ( 𝑁 / ( 2 ↑ 𝑥 ) ) )
84	80 58 59 61	divdird	⊢ ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) ∧ 𝑥 < 𝑀 ) → ( ( ( 𝑁 mod ( 2 ↑ 𝑀 ) ) + ( 𝑁 − ( 𝑁 mod ( 2 ↑ 𝑀 ) ) ) ) / ( 2 ↑ 𝑥 ) ) = ( ( ( 𝑁 mod ( 2 ↑ 𝑀 ) ) / ( 2 ↑ 𝑥 ) ) + ( ( 𝑁 − ( 𝑁 mod ( 2 ↑ 𝑀 ) ) ) / ( 2 ↑ 𝑥 ) ) ) )
85	83 84	eqtr3d	⊢ ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) ∧ 𝑥 < 𝑀 ) → ( 𝑁 / ( 2 ↑ 𝑥 ) ) = ( ( ( 𝑁 mod ( 2 ↑ 𝑀 ) ) / ( 2 ↑ 𝑥 ) ) + ( ( 𝑁 − ( 𝑁 mod ( 2 ↑ 𝑀 ) ) ) / ( 2 ↑ 𝑥 ) ) ) )
86	85	fveq2d	⊢ ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) ∧ 𝑥 < 𝑀 ) → ( ⌊ ‘ ( 𝑁 / ( 2 ↑ 𝑥 ) ) ) = ( ⌊ ‘ ( ( ( 𝑁 mod ( 2 ↑ 𝑀 ) ) / ( 2 ↑ 𝑥 ) ) + ( ( 𝑁 − ( 𝑁 mod ( 2 ↑ 𝑀 ) ) ) / ( 2 ↑ 𝑥 ) ) ) ) )
87		fladdz	⊢ ( ( ( ( 𝑁 mod ( 2 ↑ 𝑀 ) ) / ( 2 ↑ 𝑥 ) ) ∈ ℝ ∧ ( ( 𝑁 − ( 𝑁 mod ( 2 ↑ 𝑀 ) ) ) / ( 2 ↑ 𝑥 ) ) ∈ ℤ ) → ( ⌊ ‘ ( ( ( 𝑁 mod ( 2 ↑ 𝑀 ) ) / ( 2 ↑ 𝑥 ) ) + ( ( 𝑁 − ( 𝑁 mod ( 2 ↑ 𝑀 ) ) ) / ( 2 ↑ 𝑥 ) ) ) ) = ( ( ⌊ ‘ ( ( 𝑁 mod ( 2 ↑ 𝑀 ) ) / ( 2 ↑ 𝑥 ) ) ) + ( ( 𝑁 − ( 𝑁 mod ( 2 ↑ 𝑀 ) ) ) / ( 2 ↑ 𝑥 ) ) ) )
88	24 74 87	syl2anc	⊢ ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) ∧ 𝑥 < 𝑀 ) → ( ⌊ ‘ ( ( ( 𝑁 mod ( 2 ↑ 𝑀 ) ) / ( 2 ↑ 𝑥 ) ) + ( ( 𝑁 − ( 𝑁 mod ( 2 ↑ 𝑀 ) ) ) / ( 2 ↑ 𝑥 ) ) ) ) = ( ( ⌊ ‘ ( ( 𝑁 mod ( 2 ↑ 𝑀 ) ) / ( 2 ↑ 𝑥 ) ) ) + ( ( 𝑁 − ( 𝑁 mod ( 2 ↑ 𝑀 ) ) ) / ( 2 ↑ 𝑥 ) ) ) )
89	86 88	eqtrd	⊢ ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) ∧ 𝑥 < 𝑀 ) → ( ⌊ ‘ ( 𝑁 / ( 2 ↑ 𝑥 ) ) ) = ( ( ⌊ ‘ ( ( 𝑁 mod ( 2 ↑ 𝑀 ) ) / ( 2 ↑ 𝑥 ) ) ) + ( ( 𝑁 − ( 𝑁 mod ( 2 ↑ 𝑀 ) ) ) / ( 2 ↑ 𝑥 ) ) ) )
90	78 79 89	mvrladdd	⊢ ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) ∧ 𝑥 < 𝑀 ) → ( ( ⌊ ‘ ( 𝑁 / ( 2 ↑ 𝑥 ) ) ) − ( ⌊ ‘ ( ( 𝑁 mod ( 2 ↑ 𝑀 ) ) / ( 2 ↑ 𝑥 ) ) ) ) = ( ( 𝑁 − ( 𝑁 mod ( 2 ↑ 𝑀 ) ) ) / ( 2 ↑ 𝑥 ) ) )
91	77 90	breqtrrd	⊢ ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) ∧ 𝑥 < 𝑀 ) → 2 ∥ ( ( ⌊ ‘ ( 𝑁 / ( 2 ↑ 𝑥 ) ) ) − ( ⌊ ‘ ( ( 𝑁 mod ( 2 ↑ 𝑀 ) ) / ( 2 ↑ 𝑥 ) ) ) ) )
92		dvdssub2	⊢ ( ( ( 2 ∈ ℤ ∧ ( ⌊ ‘ ( 𝑁 / ( 2 ↑ 𝑥 ) ) ) ∈ ℤ ∧ ( ⌊ ‘ ( ( 𝑁 mod ( 2 ↑ 𝑀 ) ) / ( 2 ↑ 𝑥 ) ) ) ∈ ℤ ) ∧ 2 ∥ ( ( ⌊ ‘ ( 𝑁 / ( 2 ↑ 𝑥 ) ) ) − ( ⌊ ‘ ( ( 𝑁 mod ( 2 ↑ 𝑀 ) ) / ( 2 ↑ 𝑥 ) ) ) ) ) → ( 2 ∥ ( ⌊ ‘ ( 𝑁 / ( 2 ↑ 𝑥 ) ) ) ↔ 2 ∥ ( ⌊ ‘ ( ( 𝑁 mod ( 2 ↑ 𝑀 ) ) / ( 2 ↑ 𝑥 ) ) ) ) )
93	16 21 25 91 92	syl31anc	⊢ ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) ∧ 𝑥 < 𝑀 ) → ( 2 ∥ ( ⌊ ‘ ( 𝑁 / ( 2 ↑ 𝑥 ) ) ) ↔ 2 ∥ ( ⌊ ‘ ( ( 𝑁 mod ( 2 ↑ 𝑀 ) ) / ( 2 ↑ 𝑥 ) ) ) ) )
94	93	notbid	⊢ ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) ∧ 𝑥 < 𝑀 ) → ( ¬ 2 ∥ ( ⌊ ‘ ( 𝑁 / ( 2 ↑ 𝑥 ) ) ) ↔ ¬ 2 ∥ ( ⌊ ‘ ( ( 𝑁 mod ( 2 ↑ 𝑀 ) ) / ( 2 ↑ 𝑥 ) ) ) ) )
95	12 14 94	3bitr3d	⊢ ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) ∧ 𝑥 < 𝑀 ) → ( ( 𝑥 ∈ ( bits ‘ 𝑁 ) ∧ 𝑥 < 𝑀 ) ↔ ¬ 2 ∥ ( ⌊ ‘ ( ( 𝑁 mod ( 2 ↑ 𝑀 ) ) / ( 2 ↑ 𝑥 ) ) ) ) )
96		z0even	⊢ 2 ∥ 0
97	1	ad2antrr	⊢ ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) ∧ ¬ 𝑥 < 𝑀 ) → 𝑁 ∈ ℤ )
98	97	zred	⊢ ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) ∧ ¬ 𝑥 < 𝑀 ) → 𝑁 ∈ ℝ )
99		2rp	⊢ 2 ∈ ℝ+
100	99	a1i	⊢ ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) ∧ ¬ 𝑥 < 𝑀 ) → 2 ∈ ℝ+ )
101	37	nn0zd	⊢ ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) → 𝑀 ∈ ℤ )
102	101	adantr	⊢ ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) ∧ ¬ 𝑥 < 𝑀 ) → 𝑀 ∈ ℤ )
103	100 102	rpexpcld	⊢ ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) ∧ ¬ 𝑥 < 𝑀 ) → ( 2 ↑ 𝑀 ) ∈ ℝ+ )
104	98 103	modcld	⊢ ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) ∧ ¬ 𝑥 < 𝑀 ) → ( 𝑁 mod ( 2 ↑ 𝑀 ) ) ∈ ℝ )
105		simplr	⊢ ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) ∧ ¬ 𝑥 < 𝑀 ) → 𝑥 ∈ ℕ0 )
106	105	nn0zd	⊢ ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) ∧ ¬ 𝑥 < 𝑀 ) → 𝑥 ∈ ℤ )
107	100 106	rpexpcld	⊢ ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) ∧ ¬ 𝑥 < 𝑀 ) → ( 2 ↑ 𝑥 ) ∈ ℝ+ )
108	6	ad2antrr	⊢ ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) ∧ ¬ 𝑥 < 𝑀 ) → ( 𝑁 mod ( 2 ↑ 𝑀 ) ) ∈ ℕ0 )
109	108	nn0ge0d	⊢ ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) ∧ ¬ 𝑥 < 𝑀 ) → 0 ≤ ( 𝑁 mod ( 2 ↑ 𝑀 ) ) )
110	104 107 109	divge0d	⊢ ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) ∧ ¬ 𝑥 < 𝑀 ) → 0 ≤ ( ( 𝑁 mod ( 2 ↑ 𝑀 ) ) / ( 2 ↑ 𝑥 ) ) )
111	103	rpred	⊢ ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) ∧ ¬ 𝑥 < 𝑀 ) → ( 2 ↑ 𝑀 ) ∈ ℝ )
112	107	rpred	⊢ ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) ∧ ¬ 𝑥 < 𝑀 ) → ( 2 ↑ 𝑥 ) ∈ ℝ )
113		modlt	⊢ ( ( 𝑁 ∈ ℝ ∧ ( 2 ↑ 𝑀 ) ∈ ℝ+ ) → ( 𝑁 mod ( 2 ↑ 𝑀 ) ) < ( 2 ↑ 𝑀 ) )
114	98 103 113	syl2anc	⊢ ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) ∧ ¬ 𝑥 < 𝑀 ) → ( 𝑁 mod ( 2 ↑ 𝑀 ) ) < ( 2 ↑ 𝑀 ) )
115	100	rpred	⊢ ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) ∧ ¬ 𝑥 < 𝑀 ) → 2 ∈ ℝ )
116		1le2	⊢ 1 ≤ 2
117	116	a1i	⊢ ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) ∧ ¬ 𝑥 < 𝑀 ) → 1 ≤ 2 )
118	102	zred	⊢ ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) ∧ ¬ 𝑥 < 𝑀 ) → 𝑀 ∈ ℝ )
119	105	nn0red	⊢ ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) ∧ ¬ 𝑥 < 𝑀 ) → 𝑥 ∈ ℝ )
120		simpr	⊢ ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) ∧ ¬ 𝑥 < 𝑀 ) → ¬ 𝑥 < 𝑀 )
121	118 119 120	nltled	⊢ ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) ∧ ¬ 𝑥 < 𝑀 ) → 𝑀 ≤ 𝑥 )
122		eluz2	⊢ ( 𝑥 ∈ ( ℤ≥ ‘ 𝑀 ) ↔ ( 𝑀 ∈ ℤ ∧ 𝑥 ∈ ℤ ∧ 𝑀 ≤ 𝑥 ) )
123	102 106 121 122	syl3anbrc	⊢ ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) ∧ ¬ 𝑥 < 𝑀 ) → 𝑥 ∈ ( ℤ≥ ‘ 𝑀 ) )
124	115 117 123	leexp2ad	⊢ ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) ∧ ¬ 𝑥 < 𝑀 ) → ( 2 ↑ 𝑀 ) ≤ ( 2 ↑ 𝑥 ) )
125	104 111 112 114 124	ltletrd	⊢ ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) ∧ ¬ 𝑥 < 𝑀 ) → ( 𝑁 mod ( 2 ↑ 𝑀 ) ) < ( 2 ↑ 𝑥 ) )
126	107	rpcnd	⊢ ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) ∧ ¬ 𝑥 < 𝑀 ) → ( 2 ↑ 𝑥 ) ∈ ℂ )
127	126	mulridd	⊢ ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) ∧ ¬ 𝑥 < 𝑀 ) → ( ( 2 ↑ 𝑥 ) · 1 ) = ( 2 ↑ 𝑥 ) )
128	125 127	breqtrrd	⊢ ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) ∧ ¬ 𝑥 < 𝑀 ) → ( 𝑁 mod ( 2 ↑ 𝑀 ) ) < ( ( 2 ↑ 𝑥 ) · 1 ) )
129		1red	⊢ ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) ∧ ¬ 𝑥 < 𝑀 ) → 1 ∈ ℝ )
130	104 129 107	ltdivmuld	⊢ ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) ∧ ¬ 𝑥 < 𝑀 ) → ( ( ( 𝑁 mod ( 2 ↑ 𝑀 ) ) / ( 2 ↑ 𝑥 ) ) < 1 ↔ ( 𝑁 mod ( 2 ↑ 𝑀 ) ) < ( ( 2 ↑ 𝑥 ) · 1 ) ) )
131	128 130	mpbird	⊢ ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) ∧ ¬ 𝑥 < 𝑀 ) → ( ( 𝑁 mod ( 2 ↑ 𝑀 ) ) / ( 2 ↑ 𝑥 ) ) < 1 )
132		1e0p1	⊢ 1 = ( 0 + 1 )
133	131 132	breqtrdi	⊢ ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) ∧ ¬ 𝑥 < 𝑀 ) → ( ( 𝑁 mod ( 2 ↑ 𝑀 ) ) / ( 2 ↑ 𝑥 ) ) < ( 0 + 1 ) )
134	104 107	rerpdivcld	⊢ ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) ∧ ¬ 𝑥 < 𝑀 ) → ( ( 𝑁 mod ( 2 ↑ 𝑀 ) ) / ( 2 ↑ 𝑥 ) ) ∈ ℝ )
135		0z	⊢ 0 ∈ ℤ
136		flbi	⊢ ( ( ( ( 𝑁 mod ( 2 ↑ 𝑀 ) ) / ( 2 ↑ 𝑥 ) ) ∈ ℝ ∧ 0 ∈ ℤ ) → ( ( ⌊ ‘ ( ( 𝑁 mod ( 2 ↑ 𝑀 ) ) / ( 2 ↑ 𝑥 ) ) ) = 0 ↔ ( 0 ≤ ( ( 𝑁 mod ( 2 ↑ 𝑀 ) ) / ( 2 ↑ 𝑥 ) ) ∧ ( ( 𝑁 mod ( 2 ↑ 𝑀 ) ) / ( 2 ↑ 𝑥 ) ) < ( 0 + 1 ) ) ) )
137	134 135 136	sylancl	⊢ ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) ∧ ¬ 𝑥 < 𝑀 ) → ( ( ⌊ ‘ ( ( 𝑁 mod ( 2 ↑ 𝑀 ) ) / ( 2 ↑ 𝑥 ) ) ) = 0 ↔ ( 0 ≤ ( ( 𝑁 mod ( 2 ↑ 𝑀 ) ) / ( 2 ↑ 𝑥 ) ) ∧ ( ( 𝑁 mod ( 2 ↑ 𝑀 ) ) / ( 2 ↑ 𝑥 ) ) < ( 0 + 1 ) ) ) )
138	110 133 137	mpbir2and	⊢ ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) ∧ ¬ 𝑥 < 𝑀 ) → ( ⌊ ‘ ( ( 𝑁 mod ( 2 ↑ 𝑀 ) ) / ( 2 ↑ 𝑥 ) ) ) = 0 )
139	96 138	breqtrrid	⊢ ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) ∧ ¬ 𝑥 < 𝑀 ) → 2 ∥ ( ⌊ ‘ ( ( 𝑁 mod ( 2 ↑ 𝑀 ) ) / ( 2 ↑ 𝑥 ) ) ) )
140	120	intnand	⊢ ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) ∧ ¬ 𝑥 < 𝑀 ) → ¬ ( 𝑥 ∈ ( bits ‘ 𝑁 ) ∧ 𝑥 < 𝑀 ) )
141	139 140	2thd	⊢ ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) ∧ ¬ 𝑥 < 𝑀 ) → ( 2 ∥ ( ⌊ ‘ ( ( 𝑁 mod ( 2 ↑ 𝑀 ) ) / ( 2 ↑ 𝑥 ) ) ) ↔ ¬ ( 𝑥 ∈ ( bits ‘ 𝑁 ) ∧ 𝑥 < 𝑀 ) ) )
142	141	con2bid	⊢ ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) ∧ ¬ 𝑥 < 𝑀 ) → ( ( 𝑥 ∈ ( bits ‘ 𝑁 ) ∧ 𝑥 < 𝑀 ) ↔ ¬ 2 ∥ ( ⌊ ‘ ( ( 𝑁 mod ( 2 ↑ 𝑀 ) ) / ( 2 ↑ 𝑥 ) ) ) ) )
143	95 142	pm2.61dan	⊢ ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) → ( ( 𝑥 ∈ ( bits ‘ 𝑁 ) ∧ 𝑥 < 𝑀 ) ↔ ¬ 2 ∥ ( ⌊ ‘ ( ( 𝑁 mod ( 2 ↑ 𝑀 ) ) / ( 2 ↑ 𝑥 ) ) ) ) )
144	101	biantrurd	⊢ ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) → ( ( 𝑥 ∈ ( bits ‘ 𝑁 ) ∧ 𝑥 < 𝑀 ) ↔ ( 𝑀 ∈ ℤ ∧ ( 𝑥 ∈ ( bits ‘ 𝑁 ) ∧ 𝑥 < 𝑀 ) ) ) )
145	143 144	bitr3d	⊢ ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) → ( ¬ 2 ∥ ( ⌊ ‘ ( ( 𝑁 mod ( 2 ↑ 𝑀 ) ) / ( 2 ↑ 𝑥 ) ) ) ↔ ( 𝑀 ∈ ℤ ∧ ( 𝑥 ∈ ( bits ‘ 𝑁 ) ∧ 𝑥 < 𝑀 ) ) ) )
146		an12	⊢ ( ( 𝑀 ∈ ℤ ∧ ( 𝑥 ∈ ( bits ‘ 𝑁 ) ∧ 𝑥 < 𝑀 ) ) ↔ ( 𝑥 ∈ ( bits ‘ 𝑁 ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑥 < 𝑀 ) ) )
147	145 146	bitrdi	⊢ ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) → ( ¬ 2 ∥ ( ⌊ ‘ ( ( 𝑁 mod ( 2 ↑ 𝑀 ) ) / ( 2 ↑ 𝑥 ) ) ) ↔ ( 𝑥 ∈ ( bits ‘ 𝑁 ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑥 < 𝑀 ) ) ) )
148	147	pm5.32da	⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) → ( ( 𝑥 ∈ ℕ0 ∧ ¬ 2 ∥ ( ⌊ ‘ ( ( 𝑁 mod ( 2 ↑ 𝑀 ) ) / ( 2 ↑ 𝑥 ) ) ) ) ↔ ( 𝑥 ∈ ℕ0 ∧ ( 𝑥 ∈ ( bits ‘ 𝑁 ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑥 < 𝑀 ) ) ) ) )
149	8 148	bitr3d	⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) → ( ( ( 𝑁 mod ( 2 ↑ 𝑀 ) ) ∈ ℤ ∧ ( 𝑥 ∈ ℕ0 ∧ ¬ 2 ∥ ( ⌊ ‘ ( ( 𝑁 mod ( 2 ↑ 𝑀 ) ) / ( 2 ↑ 𝑥 ) ) ) ) ) ↔ ( 𝑥 ∈ ℕ0 ∧ ( 𝑥 ∈ ( bits ‘ 𝑁 ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑥 < 𝑀 ) ) ) ) )
150		3anass	⊢ ( ( ( 𝑁 mod ( 2 ↑ 𝑀 ) ) ∈ ℤ ∧ 𝑥 ∈ ℕ0 ∧ ¬ 2 ∥ ( ⌊ ‘ ( ( 𝑁 mod ( 2 ↑ 𝑀 ) ) / ( 2 ↑ 𝑥 ) ) ) ) ↔ ( ( 𝑁 mod ( 2 ↑ 𝑀 ) ) ∈ ℤ ∧ ( 𝑥 ∈ ℕ0 ∧ ¬ 2 ∥ ( ⌊ ‘ ( ( 𝑁 mod ( 2 ↑ 𝑀 ) ) / ( 2 ↑ 𝑥 ) ) ) ) ) )
151		elfzo2	⊢ ( 𝑥 ∈ ( 0 ..^ 𝑀 ) ↔ ( 𝑥 ∈ ( ℤ≥ ‘ 0 ) ∧ 𝑀 ∈ ℤ ∧ 𝑥 < 𝑀 ) )
152		elnn0uz	⊢ ( 𝑥 ∈ ℕ0 ↔ 𝑥 ∈ ( ℤ≥ ‘ 0 ) )
153	152	3anbi1i	⊢ ( ( 𝑥 ∈ ℕ0 ∧ 𝑀 ∈ ℤ ∧ 𝑥 < 𝑀 ) ↔ ( 𝑥 ∈ ( ℤ≥ ‘ 0 ) ∧ 𝑀 ∈ ℤ ∧ 𝑥 < 𝑀 ) )
154		3anass	⊢ ( ( 𝑥 ∈ ℕ0 ∧ 𝑀 ∈ ℤ ∧ 𝑥 < 𝑀 ) ↔ ( 𝑥 ∈ ℕ0 ∧ ( 𝑀 ∈ ℤ ∧ 𝑥 < 𝑀 ) ) )
155	151 153 154	3bitr2i	⊢ ( 𝑥 ∈ ( 0 ..^ 𝑀 ) ↔ ( 𝑥 ∈ ℕ0 ∧ ( 𝑀 ∈ ℤ ∧ 𝑥 < 𝑀 ) ) )
156	155	anbi2i	⊢ ( ( 𝑥 ∈ ( bits ‘ 𝑁 ) ∧ 𝑥 ∈ ( 0 ..^ 𝑀 ) ) ↔ ( 𝑥 ∈ ( bits ‘ 𝑁 ) ∧ ( 𝑥 ∈ ℕ0 ∧ ( 𝑀 ∈ ℤ ∧ 𝑥 < 𝑀 ) ) ) )
157		an12	⊢ ( ( 𝑥 ∈ ( bits ‘ 𝑁 ) ∧ ( 𝑥 ∈ ℕ0 ∧ ( 𝑀 ∈ ℤ ∧ 𝑥 < 𝑀 ) ) ) ↔ ( 𝑥 ∈ ℕ0 ∧ ( 𝑥 ∈ ( bits ‘ 𝑁 ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑥 < 𝑀 ) ) ) )
158	156 157	bitri	⊢ ( ( 𝑥 ∈ ( bits ‘ 𝑁 ) ∧ 𝑥 ∈ ( 0 ..^ 𝑀 ) ) ↔ ( 𝑥 ∈ ℕ0 ∧ ( 𝑥 ∈ ( bits ‘ 𝑁 ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑥 < 𝑀 ) ) ) )
159	149 150 158	3bitr4g	⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) → ( ( ( 𝑁 mod ( 2 ↑ 𝑀 ) ) ∈ ℤ ∧ 𝑥 ∈ ℕ0 ∧ ¬ 2 ∥ ( ⌊ ‘ ( ( 𝑁 mod ( 2 ↑ 𝑀 ) ) / ( 2 ↑ 𝑥 ) ) ) ) ↔ ( 𝑥 ∈ ( bits ‘ 𝑁 ) ∧ 𝑥 ∈ ( 0 ..^ 𝑀 ) ) ) )
160		bitsval	⊢ ( 𝑥 ∈ ( bits ‘ ( 𝑁 mod ( 2 ↑ 𝑀 ) ) ) ↔ ( ( 𝑁 mod ( 2 ↑ 𝑀 ) ) ∈ ℤ ∧ 𝑥 ∈ ℕ0 ∧ ¬ 2 ∥ ( ⌊ ‘ ( ( 𝑁 mod ( 2 ↑ 𝑀 ) ) / ( 2 ↑ 𝑥 ) ) ) ) )
161		elin	⊢ ( 𝑥 ∈ ( ( bits ‘ 𝑁 ) ∩ ( 0 ..^ 𝑀 ) ) ↔ ( 𝑥 ∈ ( bits ‘ 𝑁 ) ∧ 𝑥 ∈ ( 0 ..^ 𝑀 ) ) )
162	159 160 161	3bitr4g	⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) → ( 𝑥 ∈ ( bits ‘ ( 𝑁 mod ( 2 ↑ 𝑀 ) ) ) ↔ 𝑥 ∈ ( ( bits ‘ 𝑁 ) ∩ ( 0 ..^ 𝑀 ) ) ) )
163	162	eqrdv	⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) → ( bits ‘ ( 𝑁 mod ( 2 ↑ 𝑀 ) ) ) = ( ( bits ‘ 𝑁 ) ∩ ( 0 ..^ 𝑀 ) ) )