Theorem bitsinv1lem 16076

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

Assertion

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

Proof of Theorem bitsinv1lem

Step	Hyp	Ref	Expression
1		oveq2 7263	. . 3 ⊢ ((2↑𝑀) = if(𝑀 ∈ (bits‘𝑁), (2↑𝑀), 0) → ((𝑁 mod (2↑𝑀)) + (2↑𝑀)) = ((𝑁 mod (2↑𝑀)) + if(𝑀 ∈ (bits‘𝑁), (2↑𝑀), 0)))
2	1	eqeq2d 2749	. 2 ⊢ ((2↑𝑀) = if(𝑀 ∈ (bits‘𝑁), (2↑𝑀), 0) → ((𝑁 mod (2↑(𝑀 + 1))) = ((𝑁 mod (2↑𝑀)) + (2↑𝑀)) ↔ (𝑁 mod (2↑(𝑀 + 1))) = ((𝑁 mod (2↑𝑀)) + if(𝑀 ∈ (bits‘𝑁), (2↑𝑀), 0))))
3		oveq2 7263	. . 3 ⊢ (0 = if(𝑀 ∈ (bits‘𝑁), (2↑𝑀), 0) → ((𝑁 mod (2↑𝑀)) + 0) = ((𝑁 mod (2↑𝑀)) + if(𝑀 ∈ (bits‘𝑁), (2↑𝑀), 0)))
4	3	eqeq2d 2749	. 2 ⊢ (0 = if(𝑀 ∈ (bits‘𝑁), (2↑𝑀), 0) → ((𝑁 mod (2↑(𝑀 + 1))) = ((𝑁 mod (2↑𝑀)) + 0) ↔ (𝑁 mod (2↑(𝑀 + 1))) = ((𝑁 mod (2↑𝑀)) + if(𝑀 ∈ (bits‘𝑁), (2↑𝑀), 0))))
5		simpl 482	. . . . . . 7 ⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → 𝑁 ∈ ℤ)
6		2nn 11976	. . . . . . . . 9 ⊢ 2 ∈ ℕ
7	6	a1i 11	. . . . . . . 8 ⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → 2 ∈ ℕ)
8		simpr 484	. . . . . . . 8 ⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → 𝑀 ∈ ℕ0)
9	7, 8	nnexpcld 13888	. . . . . . 7 ⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → (2↑𝑀) ∈ ℕ)
10	5, 9	zmodcld 13540	. . . . . 6 ⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → (𝑁 mod (2↑𝑀)) ∈ ℕ0)
11	10	nn0cnd 12225	. . . . 5 ⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → (𝑁 mod (2↑𝑀)) ∈ ℂ)
12	11	adantr 480	. . . 4 ⊢ (((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) ∧ 𝑀 ∈ (bits‘𝑁)) → (𝑁 mod (2↑𝑀)) ∈ ℂ)
13		1nn0 12179	. . . . . . . . . 10 ⊢ 1 ∈ ℕ0
14	13	a1i 11	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → 1 ∈ ℕ0)
15	8, 14	nn0addcld 12227	. . . . . . . 8 ⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → (𝑀 + 1) ∈ ℕ0)
16	7, 15	nnexpcld 13888	. . . . . . 7 ⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → (2↑(𝑀 + 1)) ∈ ℕ)
17	5, 16	zmodcld 13540	. . . . . 6 ⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → (𝑁 mod (2↑(𝑀 + 1))) ∈ ℕ0)
18	17	nn0cnd 12225	. . . . 5 ⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → (𝑁 mod (2↑(𝑀 + 1))) ∈ ℂ)
19	18	adantr 480	. . . 4 ⊢ (((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) ∧ 𝑀 ∈ (bits‘𝑁)) → (𝑁 mod (2↑(𝑀 + 1))) ∈ ℂ)
20	12, 19	pncan3d 11265	. . 3 ⊢ (((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) ∧ 𝑀 ∈ (bits‘𝑁)) → ((𝑁 mod (2↑𝑀)) + ((𝑁 mod (2↑(𝑀 + 1))) − (𝑁 mod (2↑𝑀)))) = (𝑁 mod (2↑(𝑀 + 1))))
21	18, 11	subcld 11262	. . . . . 6 ⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → ((𝑁 mod (2↑(𝑀 + 1))) − (𝑁 mod (2↑𝑀))) ∈ ℂ)
22	21	adantr 480	. . . . 5 ⊢ (((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) ∧ 𝑀 ∈ (bits‘𝑁)) → ((𝑁 mod (2↑(𝑀 + 1))) − (𝑁 mod (2↑𝑀))) ∈ ℂ)
23	6	a1i 11	. . . . . . 7 ⊢ (((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) ∧ 𝑀 ∈ (bits‘𝑁)) → 2 ∈ ℕ)
24		simplr 765	. . . . . . 7 ⊢ (((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) ∧ 𝑀 ∈ (bits‘𝑁)) → 𝑀 ∈ ℕ0)
25	23, 24	nnexpcld 13888	. . . . . 6 ⊢ (((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) ∧ 𝑀 ∈ (bits‘𝑁)) → (2↑𝑀) ∈ ℕ)
26	25	nncnd 11919	. . . . 5 ⊢ (((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) ∧ 𝑀 ∈ (bits‘𝑁)) → (2↑𝑀) ∈ ℂ)
27		2cnd 11981	. . . . . . 7 ⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → 2 ∈ ℂ)
28		2ne0 12007	. . . . . . . 8 ⊢ 2 ≠ 0
29	28	a1i 11	. . . . . . 7 ⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → 2 ≠ 0)
30	8	nn0zd 12353	. . . . . . 7 ⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → 𝑀 ∈ ℤ)
31	27, 29, 30	expne0d 13798	. . . . . 6 ⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → (2↑𝑀) ≠ 0)
32	31	adantr 480	. . . . 5 ⊢ (((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) ∧ 𝑀 ∈ (bits‘𝑁)) → (2↑𝑀) ≠ 0)
33		z0even 16004	. . . . . . . . . 10 ⊢ 2 ∥ 0
34		id 22	. . . . . . . . . 10 ⊢ ((((𝑁 mod (2↑(𝑀 + 1))) − (𝑁 mod (2↑𝑀))) / (2↑𝑀)) = 0 → (((𝑁 mod (2↑(𝑀 + 1))) − (𝑁 mod (2↑𝑀))) / (2↑𝑀)) = 0)
35	33, 34	breqtrrid 5108	. . . . . . . . 9 ⊢ ((((𝑁 mod (2↑(𝑀 + 1))) − (𝑁 mod (2↑𝑀))) / (2↑𝑀)) = 0 → 2 ∥ (((𝑁 mod (2↑(𝑀 + 1))) − (𝑁 mod (2↑𝑀))) / (2↑𝑀)))
36		bitsval2 16060	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → (𝑀 ∈ (bits‘𝑁) ↔ ¬ 2 ∥ (⌊‘(𝑁 / (2↑𝑀)))))
37	5	zred 12355	. . . . . . . . . . . . . . 15 ⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → 𝑁 ∈ ℝ)
38	9	nnrpd 12699	. . . . . . . . . . . . . . 15 ⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → (2↑𝑀) ∈ ℝ+)
39		moddiffl 13530	. . . . . . . . . . . . . . 15 ⊢ ((𝑁 ∈ ℝ ∧ (2↑𝑀) ∈ ℝ+) → ((𝑁 − (𝑁 mod (2↑𝑀))) / (2↑𝑀)) = (⌊‘(𝑁 / (2↑𝑀))))
40	37, 38, 39	syl2anc 583	. . . . . . . . . . . . . 14 ⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → ((𝑁 − (𝑁 mod (2↑𝑀))) / (2↑𝑀)) = (⌊‘(𝑁 / (2↑𝑀))))
41	40	breq2d 5082	. . . . . . . . . . . . 13 ⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → (2 ∥ ((𝑁 − (𝑁 mod (2↑𝑀))) / (2↑𝑀)) ↔ 2 ∥ (⌊‘(𝑁 / (2↑𝑀)))))
42		2z 12282	. . . . . . . . . . . . . . 15 ⊢ 2 ∈ ℤ
43	42	a1i 11	. . . . . . . . . . . . . 14 ⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → 2 ∈ ℤ)
44		moddifz 13531	. . . . . . . . . . . . . . 15 ⊢ ((𝑁 ∈ ℝ ∧ (2↑𝑀) ∈ ℝ+) → ((𝑁 − (𝑁 mod (2↑𝑀))) / (2↑𝑀)) ∈ ℤ)
45	37, 38, 44	syl2anc 583	. . . . . . . . . . . . . 14 ⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → ((𝑁 − (𝑁 mod (2↑𝑀))) / (2↑𝑀)) ∈ ℤ)
46	5	zcnd 12356	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → 𝑁 ∈ ℂ)
47	46, 11, 18	nnncan1d 11296	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → ((𝑁 − (𝑁 mod (2↑𝑀))) − (𝑁 − (𝑁 mod (2↑(𝑀 + 1))))) = ((𝑁 mod (2↑(𝑀 + 1))) − (𝑁 mod (2↑𝑀))))
48	47	oveq1d 7270	. . . . . . . . . . . . . . . 16 ⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → (((𝑁 − (𝑁 mod (2↑𝑀))) − (𝑁 − (𝑁 mod (2↑(𝑀 + 1))))) / (2↑𝑀)) = (((𝑁 mod (2↑(𝑀 + 1))) − (𝑁 mod (2↑𝑀))) / (2↑𝑀)))
49	46, 11	subcld 11262	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → (𝑁 − (𝑁 mod (2↑𝑀))) ∈ ℂ)
50	46, 18	subcld 11262	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → (𝑁 − (𝑁 mod (2↑(𝑀 + 1)))) ∈ ℂ)
51	9	nncnd 11919	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → (2↑𝑀) ∈ ℂ)
52	49, 50, 51, 31	divsubdird 11720	. . . . . . . . . . . . . . . 16 ⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → (((𝑁 − (𝑁 mod (2↑𝑀))) − (𝑁 − (𝑁 mod (2↑(𝑀 + 1))))) / (2↑𝑀)) = (((𝑁 − (𝑁 mod (2↑𝑀))) / (2↑𝑀)) − ((𝑁 − (𝑁 mod (2↑(𝑀 + 1)))) / (2↑𝑀))))
53	48, 52	eqtr3d 2780	. . . . . . . . . . . . . . 15 ⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → (((𝑁 mod (2↑(𝑀 + 1))) − (𝑁 mod (2↑𝑀))) / (2↑𝑀)) = (((𝑁 − (𝑁 mod (2↑𝑀))) / (2↑𝑀)) − ((𝑁 − (𝑁 mod (2↑(𝑀 + 1)))) / (2↑𝑀))))
54	27, 50	mulcomd 10927	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → (2 · (𝑁 − (𝑁 mod (2↑(𝑀 + 1))))) = ((𝑁 − (𝑁 mod (2↑(𝑀 + 1)))) · 2))
55	27, 51	mulcomd 10927	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → (2 · (2↑𝑀)) = ((2↑𝑀) · 2))
56	27, 8	expp1d 13793	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → (2↑(𝑀 + 1)) = ((2↑𝑀) · 2))
57	55, 56	eqtr4d 2781	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → (2 · (2↑𝑀)) = (2↑(𝑀 + 1)))
58	54, 57	oveq12d 7273	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → ((2 · (𝑁 − (𝑁 mod (2↑(𝑀 + 1))))) / (2 · (2↑𝑀))) = (((𝑁 − (𝑁 mod (2↑(𝑀 + 1)))) · 2) / (2↑(𝑀 + 1))))
59	50, 51, 27, 31, 29	divcan5d 11707	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → ((2 · (𝑁 − (𝑁 mod (2↑(𝑀 + 1))))) / (2 · (2↑𝑀))) = ((𝑁 − (𝑁 mod (2↑(𝑀 + 1)))) / (2↑𝑀)))
60	16	nncnd 11919	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → (2↑(𝑀 + 1)) ∈ ℂ)
61	30	peano2zd 12358	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → (𝑀 + 1) ∈ ℤ)
62	27, 29, 61	expne0d 13798	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → (2↑(𝑀 + 1)) ≠ 0)
63	50, 27, 60, 62	div23d 11718	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → (((𝑁 − (𝑁 mod (2↑(𝑀 + 1)))) · 2) / (2↑(𝑀 + 1))) = (((𝑁 − (𝑁 mod (2↑(𝑀 + 1)))) / (2↑(𝑀 + 1))) · 2))
64	58, 59, 63	3eqtr3d 2786	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → ((𝑁 − (𝑁 mod (2↑(𝑀 + 1)))) / (2↑𝑀)) = (((𝑁 − (𝑁 mod (2↑(𝑀 + 1)))) / (2↑(𝑀 + 1))) · 2))
65	16	nnrpd 12699	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → (2↑(𝑀 + 1)) ∈ ℝ+)
66		moddifz 13531	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑁 ∈ ℝ ∧ (2↑(𝑀 + 1)) ∈ ℝ+) → ((𝑁 − (𝑁 mod (2↑(𝑀 + 1)))) / (2↑(𝑀 + 1))) ∈ ℤ)
67	37, 65, 66	syl2anc 583	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → ((𝑁 − (𝑁 mod (2↑(𝑀 + 1)))) / (2↑(𝑀 + 1))) ∈ ℤ)
68	67, 43	zmulcld 12361	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → (((𝑁 − (𝑁 mod (2↑(𝑀 + 1)))) / (2↑(𝑀 + 1))) · 2) ∈ ℤ)
69	64, 68	eqeltrd 2839	. . . . . . . . . . . . . . . 16 ⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → ((𝑁 − (𝑁 mod (2↑(𝑀 + 1)))) / (2↑𝑀)) ∈ ℤ)
70	45, 69	zsubcld 12360	. . . . . . . . . . . . . . 15 ⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → (((𝑁 − (𝑁 mod (2↑𝑀))) / (2↑𝑀)) − ((𝑁 − (𝑁 mod (2↑(𝑀 + 1)))) / (2↑𝑀))) ∈ ℤ)
71	53, 70	eqeltrd 2839	. . . . . . . . . . . . . 14 ⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → (((𝑁 mod (2↑(𝑀 + 1))) − (𝑁 mod (2↑𝑀))) / (2↑𝑀)) ∈ ℤ)
72		dvdsmul2 15916	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑁 − (𝑁 mod (2↑(𝑀 + 1)))) / (2↑(𝑀 + 1))) ∈ ℤ ∧ 2 ∈ ℤ) → 2 ∥ (((𝑁 − (𝑁 mod (2↑(𝑀 + 1)))) / (2↑(𝑀 + 1))) · 2))
73	67, 43, 72	syl2anc 583	. . . . . . . . . . . . . . 15 ⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → 2 ∥ (((𝑁 − (𝑁 mod (2↑(𝑀 + 1)))) / (2↑(𝑀 + 1))) · 2))
74	46, 18, 11	nnncan2d 11297	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → ((𝑁 − (𝑁 mod (2↑𝑀))) − ((𝑁 mod (2↑(𝑀 + 1))) − (𝑁 mod (2↑𝑀)))) = (𝑁 − (𝑁 mod (2↑(𝑀 + 1)))))
75	74	oveq1d 7270	. . . . . . . . . . . . . . . 16 ⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → (((𝑁 − (𝑁 mod (2↑𝑀))) − ((𝑁 mod (2↑(𝑀 + 1))) − (𝑁 mod (2↑𝑀)))) / (2↑𝑀)) = ((𝑁 − (𝑁 mod (2↑(𝑀 + 1)))) / (2↑𝑀)))
76	49, 21, 51, 31	divsubdird 11720	. . . . . . . . . . . . . . . 16 ⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → (((𝑁 − (𝑁 mod (2↑𝑀))) − ((𝑁 mod (2↑(𝑀 + 1))) − (𝑁 mod (2↑𝑀)))) / (2↑𝑀)) = (((𝑁 − (𝑁 mod (2↑𝑀))) / (2↑𝑀)) − (((𝑁 mod (2↑(𝑀 + 1))) − (𝑁 mod (2↑𝑀))) / (2↑𝑀))))
77	75, 76, 64	3eqtr3d 2786	. . . . . . . . . . . . . . 15 ⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → (((𝑁 − (𝑁 mod (2↑𝑀))) / (2↑𝑀)) − (((𝑁 mod (2↑(𝑀 + 1))) − (𝑁 mod (2↑𝑀))) / (2↑𝑀))) = (((𝑁 − (𝑁 mod (2↑(𝑀 + 1)))) / (2↑(𝑀 + 1))) · 2))
78	73, 77	breqtrrd 5098	. . . . . . . . . . . . . 14 ⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → 2 ∥ (((𝑁 − (𝑁 mod (2↑𝑀))) / (2↑𝑀)) − (((𝑁 mod (2↑(𝑀 + 1))) − (𝑁 mod (2↑𝑀))) / (2↑𝑀))))
79		dvdssub2 15938	. . . . . . . . . . . . . 14 ⊢ (((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 1371	. . . . . . . . . . . . 13 ⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → (2 ∥ ((𝑁 − (𝑁 mod (2↑𝑀))) / (2↑𝑀)) ↔ 2 ∥ (((𝑁 mod (2↑(𝑀 + 1))) − (𝑁 mod (2↑𝑀))) / (2↑𝑀))))
81	41, 80	bitr3d 280	. . . . . . . . . . . 12 ⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → (2 ∥ (⌊‘(𝑁 / (2↑𝑀))) ↔ 2 ∥ (((𝑁 mod (2↑(𝑀 + 1))) − (𝑁 mod (2↑𝑀))) / (2↑𝑀))))
82	81	notbid 317	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → (¬ 2 ∥ (⌊‘(𝑁 / (2↑𝑀))) ↔ ¬ 2 ∥ (((𝑁 mod (2↑(𝑀 + 1))) − (𝑁 mod (2↑𝑀))) / (2↑𝑀))))
83	36, 82	bitrd 278	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → (𝑀 ∈ (bits‘𝑁) ↔ ¬ 2 ∥ (((𝑁 mod (2↑(𝑀 + 1))) − (𝑁 mod (2↑𝑀))) / (2↑𝑀))))
84	83	con2bid 354	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → (2 ∥ (((𝑁 mod (2↑(𝑀 + 1))) − (𝑁 mod (2↑𝑀))) / (2↑𝑀)) ↔ ¬ 𝑀 ∈ (bits‘𝑁)))
85	35, 84	syl5ib 243	. . . . . . . 8 ⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → ((((𝑁 mod (2↑(𝑀 + 1))) − (𝑁 mod (2↑𝑀))) / (2↑𝑀)) = 0 → ¬ 𝑀 ∈ (bits‘𝑁)))
86	85	con2d 134	. . . . . . 7 ⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → (𝑀 ∈ (bits‘𝑁) → ¬ (((𝑁 mod (2↑(𝑀 + 1))) − (𝑁 mod (2↑𝑀))) / (2↑𝑀)) = 0))
87		df-neg 11138	. . . . . . . . . . . . . . 15 ⊢ -1 = (0 − 1)
88	51	mulm1d 11357	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → (-1 · (2↑𝑀)) = -(2↑𝑀))
89	9	nnred 11918	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → (2↑𝑀) ∈ ℝ)
90	89	renegcld 11332	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → -(2↑𝑀) ∈ ℝ)
91	37, 38	modcld 13523	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → (𝑁 mod (2↑𝑀)) ∈ ℝ)
92	91	renegcld 11332	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → -(𝑁 mod (2↑𝑀)) ∈ ℝ)
93	37, 65	modcld 13523	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → (𝑁 mod (2↑(𝑀 + 1))) ∈ ℝ)
94	93, 91	resubcld 11333	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → ((𝑁 mod (2↑(𝑀 + 1))) − (𝑁 mod (2↑𝑀))) ∈ ℝ)
95		modlt 13528	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑁 ∈ ℝ ∧ (2↑𝑀) ∈ ℝ+) → (𝑁 mod (2↑𝑀)) < (2↑𝑀))
96	37, 38, 95	syl2anc 583	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → (𝑁 mod (2↑𝑀)) < (2↑𝑀))
97	91, 89	ltnegd 11483	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → ((𝑁 mod (2↑𝑀)) < (2↑𝑀) ↔ -(2↑𝑀) < -(𝑁 mod (2↑𝑀))))
98	96, 97	mpbid 231	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → -(2↑𝑀) < -(𝑁 mod (2↑𝑀)))
99		df-neg 11138	. . . . . . . . . . . . . . . . . . 19 ⊢ -(𝑁 mod (2↑𝑀)) = (0 − (𝑁 mod (2↑𝑀)))
100		0red 10909	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → 0 ∈ ℝ)
101		modge0 13527	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑁 ∈ ℝ ∧ (2↑(𝑀 + 1)) ∈ ℝ+) → 0 ≤ (𝑁 mod (2↑(𝑀 + 1))))
102	37, 65, 101	syl2anc 583	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → 0 ≤ (𝑁 mod (2↑(𝑀 + 1))))
103	100, 93, 91, 102	lesub1dd 11521	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → (0 − (𝑁 mod (2↑𝑀))) ≤ ((𝑁 mod (2↑(𝑀 + 1))) − (𝑁 mod (2↑𝑀))))
104	99, 103	eqbrtrid 5105	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → -(𝑁 mod (2↑𝑀)) ≤ ((𝑁 mod (2↑(𝑀 + 1))) − (𝑁 mod (2↑𝑀))))
105	90, 92, 94, 98, 104	ltletrd 11065	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → -(2↑𝑀) < ((𝑁 mod (2↑(𝑀 + 1))) − (𝑁 mod (2↑𝑀))))
106	88, 105	eqbrtrd 5092	. . . . . . . . . . . . . . . 16 ⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → (-1 · (2↑𝑀)) < ((𝑁 mod (2↑(𝑀 + 1))) − (𝑁 mod (2↑𝑀))))
107		1red 10907	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → 1 ∈ ℝ)
108	107	renegcld 11332	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → -1 ∈ ℝ)
109	108, 94, 38	ltmuldivd 12748	. . . . . . . . . . . . . . . 16 ⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → ((-1 · (2↑𝑀)) < ((𝑁 mod (2↑(𝑀 + 1))) − (𝑁 mod (2↑𝑀))) ↔ -1 < (((𝑁 mod (2↑(𝑀 + 1))) − (𝑁 mod (2↑𝑀))) / (2↑𝑀))))
110	106, 109	mpbid 231	. . . . . . . . . . . . . . 15 ⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → -1 < (((𝑁 mod (2↑(𝑀 + 1))) − (𝑁 mod (2↑𝑀))) / (2↑𝑀)))
111	87, 110	eqbrtrrid 5106	. . . . . . . . . . . . . 14 ⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → (0 − 1) < (((𝑁 mod (2↑(𝑀 + 1))) − (𝑁 mod (2↑𝑀))) / (2↑𝑀)))
112		0zd 12261	. . . . . . . . . . . . . . 15 ⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → 0 ∈ ℤ)
113		zlem1lt 12302	. . . . . . . . . . . . . . 15 ⊢ ((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 583	. . . . . . . . . . . . . 14 ⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → (0 ≤ (((𝑁 mod (2↑(𝑀 + 1))) − (𝑁 mod (2↑𝑀))) / (2↑𝑀)) ↔ (0 − 1) < (((𝑁 mod (2↑(𝑀 + 1))) − (𝑁 mod (2↑𝑀))) / (2↑𝑀))))
115	111, 114	mpbird 256	. . . . . . . . . . . . 13 ⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → 0 ≤ (((𝑁 mod (2↑(𝑀 + 1))) − (𝑁 mod (2↑𝑀))) / (2↑𝑀)))
116		elnn0z 12262	. . . . . . . . . . . . 13 ⊢ ((((𝑁 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 582	. . . . . . . . . . . 12 ⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → (((𝑁 mod (2↑(𝑀 + 1))) − (𝑁 mod (2↑𝑀))) / (2↑𝑀)) ∈ ℕ0)
118		nn0uz 12549	. . . . . . . . . . . 12 ⊢ ℕ0 = (ℤ≥‘0)
119	117, 118	eleqtrdi 2849	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → (((𝑁 mod (2↑(𝑀 + 1))) − (𝑁 mod (2↑𝑀))) / (2↑𝑀)) ∈ (ℤ≥‘0))
120	16	nnred 11918	. . . . . . . . . . . . . 14 ⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → (2↑(𝑀 + 1)) ∈ ℝ)
121		modge0 13527	. . . . . . . . . . . . . . . 16 ⊢ ((𝑁 ∈ ℝ ∧ (2↑𝑀) ∈ ℝ+) → 0 ≤ (𝑁 mod (2↑𝑀)))
122	37, 38, 121	syl2anc 583	. . . . . . . . . . . . . . 15 ⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → 0 ≤ (𝑁 mod (2↑𝑀)))
123	93, 91	subge02d 11497	. . . . . . . . . . . . . . 15 ⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → (0 ≤ (𝑁 mod (2↑𝑀)) ↔ ((𝑁 mod (2↑(𝑀 + 1))) − (𝑁 mod (2↑𝑀))) ≤ (𝑁 mod (2↑(𝑀 + 1)))))
124	122, 123	mpbid 231	. . . . . . . . . . . . . 14 ⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → ((𝑁 mod (2↑(𝑀 + 1))) − (𝑁 mod (2↑𝑀))) ≤ (𝑁 mod (2↑(𝑀 + 1))))
125		modlt 13528	. . . . . . . . . . . . . . 15 ⊢ ((𝑁 ∈ ℝ ∧ (2↑(𝑀 + 1)) ∈ ℝ+) → (𝑁 mod (2↑(𝑀 + 1))) < (2↑(𝑀 + 1)))
126	37, 65, 125	syl2anc 583	. . . . . . . . . . . . . 14 ⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → (𝑁 mod (2↑(𝑀 + 1))) < (2↑(𝑀 + 1)))
127	94, 93, 120, 124, 126	lelttrd 11063	. . . . . . . . . . . . 13 ⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → ((𝑁 mod (2↑(𝑀 + 1))) − (𝑁 mod (2↑𝑀))) < (2↑(𝑀 + 1)))
128	127, 56	breqtrd 5096	. . . . . . . . . . . 12 ⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → ((𝑁 mod (2↑(𝑀 + 1))) − (𝑁 mod (2↑𝑀))) < ((2↑𝑀) · 2))
129	7	nnred 11918	. . . . . . . . . . . . 13 ⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → 2 ∈ ℝ)
130	94, 129, 38	ltdivmuld 12752	. . . . . . . . . . . 12 ⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → ((((𝑁 mod (2↑(𝑀 + 1))) − (𝑁 mod (2↑𝑀))) / (2↑𝑀)) < 2 ↔ ((𝑁 mod (2↑(𝑀 + 1))) − (𝑁 mod (2↑𝑀))) < ((2↑𝑀) · 2)))
131	128, 130	mpbird 256	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → (((𝑁 mod (2↑(𝑀 + 1))) − (𝑁 mod (2↑𝑀))) / (2↑𝑀)) < 2)
132		elfzo2 13319	. . . . . . . . . . 11 ⊢ ((((𝑁 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 1341	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → (((𝑁 mod (2↑(𝑀 + 1))) − (𝑁 mod (2↑𝑀))) / (2↑𝑀)) ∈ (0..^2))
134		fzo0to2pr 13400	. . . . . . . . . 10 ⊢ (0..^2) = {0, 1}
135	133, 134	eleqtrdi 2849	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → (((𝑁 mod (2↑(𝑀 + 1))) − (𝑁 mod (2↑𝑀))) / (2↑𝑀)) ∈ {0, 1})
136		elpri 4580	. . . . . . . . 9 ⊢ ((((𝑁 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 17	. . . . . . . 8 ⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → ((((𝑁 mod (2↑(𝑀 + 1))) − (𝑁 mod (2↑𝑀))) / (2↑𝑀)) = 0 ∨ (((𝑁 mod (2↑(𝑀 + 1))) − (𝑁 mod (2↑𝑀))) / (2↑𝑀)) = 1))
138	137	ord 860	. . . . . . 7 ⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → (¬ (((𝑁 mod (2↑(𝑀 + 1))) − (𝑁 mod (2↑𝑀))) / (2↑𝑀)) = 0 → (((𝑁 mod (2↑(𝑀 + 1))) − (𝑁 mod (2↑𝑀))) / (2↑𝑀)) = 1))
139	86, 138	syld 47	. . . . . 6 ⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → (𝑀 ∈ (bits‘𝑁) → (((𝑁 mod (2↑(𝑀 + 1))) − (𝑁 mod (2↑𝑀))) / (2↑𝑀)) = 1))
140	139	imp 406	. . . . 5 ⊢ (((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) ∧ 𝑀 ∈ (bits‘𝑁)) → (((𝑁 mod (2↑(𝑀 + 1))) − (𝑁 mod (2↑𝑀))) / (2↑𝑀)) = 1)
141	22, 26, 32, 140	diveq1d 11689	. . . 4 ⊢ (((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) ∧ 𝑀 ∈ (bits‘𝑁)) → ((𝑁 mod (2↑(𝑀 + 1))) − (𝑁 mod (2↑𝑀))) = (2↑𝑀))
142	141	oveq2d 7271	. . 3 ⊢ (((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) ∧ 𝑀 ∈ (bits‘𝑁)) → ((𝑁 mod (2↑𝑀)) + ((𝑁 mod (2↑(𝑀 + 1))) − (𝑁 mod (2↑𝑀)))) = ((𝑁 mod (2↑𝑀)) + (2↑𝑀)))
143	20, 142	eqtr3d 2780	. 2 ⊢ (((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) ∧ 𝑀 ∈ (bits‘𝑁)) → (𝑁 mod (2↑(𝑀 + 1))) = ((𝑁 mod (2↑𝑀)) + (2↑𝑀)))
144	18	adantr 480	. . . 4 ⊢ (((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) ∧ ¬ 𝑀 ∈ (bits‘𝑁)) → (𝑁 mod (2↑(𝑀 + 1))) ∈ ℂ)
145	11	adantr 480	. . . 4 ⊢ (((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) ∧ ¬ 𝑀 ∈ (bits‘𝑁)) → (𝑁 mod (2↑𝑀)) ∈ ℂ)
146	21	adantr 480	. . . . 5 ⊢ (((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) ∧ ¬ 𝑀 ∈ (bits‘𝑁)) → ((𝑁 mod (2↑(𝑀 + 1))) − (𝑁 mod (2↑𝑀))) ∈ ℂ)
147	51	adantr 480	. . . . 5 ⊢ (((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) ∧ ¬ 𝑀 ∈ (bits‘𝑁)) → (2↑𝑀) ∈ ℂ)
148	31	adantr 480	. . . . 5 ⊢ (((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) ∧ ¬ 𝑀 ∈ (bits‘𝑁)) → (2↑𝑀) ≠ 0)
149		n2dvds1 16005	. . . . . . . . . 10 ⊢ ¬ 2 ∥ 1
150		breq2 5074	. . . . . . . . . 10 ⊢ ((((𝑁 mod (2↑(𝑀 + 1))) − (𝑁 mod (2↑𝑀))) / (2↑𝑀)) = 1 → (2 ∥ (((𝑁 mod (2↑(𝑀 + 1))) − (𝑁 mod (2↑𝑀))) / (2↑𝑀)) ↔ 2 ∥ 1))
151	149, 150	mtbiri 326	. . . . . . . . 9 ⊢ ((((𝑁 mod (2↑(𝑀 + 1))) − (𝑁 mod (2↑𝑀))) / (2↑𝑀)) = 1 → ¬ 2 ∥ (((𝑁 mod (2↑(𝑀 + 1))) − (𝑁 mod (2↑𝑀))) / (2↑𝑀)))
152	138, 151	syl6 35	. . . . . . . 8 ⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → (¬ (((𝑁 mod (2↑(𝑀 + 1))) − (𝑁 mod (2↑𝑀))) / (2↑𝑀)) = 0 → ¬ 2 ∥ (((𝑁 mod (2↑(𝑀 + 1))) − (𝑁 mod (2↑𝑀))) / (2↑𝑀))))
153	152, 83	sylibrd 258	. . . . . . 7 ⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → (¬ (((𝑁 mod (2↑(𝑀 + 1))) − (𝑁 mod (2↑𝑀))) / (2↑𝑀)) = 0 → 𝑀 ∈ (bits‘𝑁)))
154	153	con1d 145	. . . . . 6 ⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → (¬ 𝑀 ∈ (bits‘𝑁) → (((𝑁 mod (2↑(𝑀 + 1))) − (𝑁 mod (2↑𝑀))) / (2↑𝑀)) = 0))
155	154	imp 406	. . . . 5 ⊢ (((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) ∧ ¬ 𝑀 ∈ (bits‘𝑁)) → (((𝑁 mod (2↑(𝑀 + 1))) − (𝑁 mod (2↑𝑀))) / (2↑𝑀)) = 0)
156	146, 147, 148, 155	diveq0d 11688	. . . 4 ⊢ (((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) ∧ ¬ 𝑀 ∈ (bits‘𝑁)) → ((𝑁 mod (2↑(𝑀 + 1))) − (𝑁 mod (2↑𝑀))) = 0)
157	144, 145, 156	subeq0d 11270	. . 3 ⊢ (((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) ∧ ¬ 𝑀 ∈ (bits‘𝑁)) → (𝑁 mod (2↑(𝑀 + 1))) = (𝑁 mod (2↑𝑀)))
158	145	addid1d 11105	. . 3 ⊢ (((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) ∧ ¬ 𝑀 ∈ (bits‘𝑁)) → ((𝑁 mod (2↑𝑀)) + 0) = (𝑁 mod (2↑𝑀)))
159	157, 158	eqtr4d 2781	. 2 ⊢ (((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) ∧ ¬ 𝑀 ∈ (bits‘𝑁)) → (𝑁 mod (2↑(𝑀 + 1))) = ((𝑁 mod (2↑𝑀)) + 0))
160	2, 4, 143, 159	ifbothda 4494	1 ⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → (𝑁 mod (2↑(𝑀 + 1))) = ((𝑁 mod (2↑𝑀)) + if(𝑀 ∈ (bits‘𝑁), (2↑𝑀), 0)))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 205   ∧ wa 395   ∨ wo 843   = wceq 1539   ∈ wcel 2108   ≠ wne 2942  ifcif 4456  {cpr 4560   class class class wbr 5070  ‘cfv 6418  (class class class)co 7255  ℂcc 10800  ℝcr 10801  0cc0 10802  1c1 10803   + caddc 10805   · cmul 10807   < clt 10940   ≤ cle 10941   − cmin 11135  -cneg 11136   / cdiv 11562  ℕcn 11903  2c2 11958  ℕ₀cn0 12163  ℤcz 12249  ℤ_≥cuz 12511  ℝ⁺crp 12659  ..^cfzo 13311  ⌊cfl 13438   mod cmo 13517  ↑cexp 13710   ∥ cdvds 15891  bitscbits 16054

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2156  ax-12 2173  ax-ext 2709  ax-sep 5218  ax-nul 5225  ax-pow 5283  ax-pr 5347  ax-un 7566  ax-cnex 10858  ax-resscn 10859  ax-1cn 10860  ax-icn 10861  ax-addcl 10862  ax-addrcl 10863  ax-mulcl 10864  ax-mulrcl 10865  ax-mulcom 10866  ax-addass 10867  ax-mulass 10868  ax-distr 10869  ax-i2m1 10870  ax-1ne0 10871  ax-1rid 10872  ax-rnegex 10873  ax-rrecex 10874  ax-cnre 10875  ax-pre-lttri 10876  ax-pre-lttrn 10877  ax-pre-ltadd 10878  ax-pre-mulgt0 10879  ax-pre-sup 10880

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3or 1086  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-nf 1788  df-sb 2069  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2817  df-nfc 2888  df-ne 2943  df-nel 3049  df-ral 3068  df-rex 3069  df-reu 3070  df-rmo 3071  df-rab 3072  df-v 3424  df-sbc 3712  df-csb 3829  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-pss 3902  df-nul 4254  df-if 4457  df-pw 4532  df-sn 4559  df-pr 4561  df-tp 4563  df-op 4565  df-uni 4837  df-iun 4923  df-br 5071  df-opab 5133  df-mpt 5154  df-tr 5188  df-id 5480  df-eprel 5486  df-po 5494  df-so 5495  df-fr 5535  df-we 5537  df-xp 5586  df-rel 5587  df-cnv 5588  df-co 5589  df-dm 5590  df-rn 5591  df-res 5592  df-ima 5593  df-pred 6191  df-ord 6254  df-on 6255  df-lim 6256  df-suc 6257  df-iota 6376  df-fun 6420  df-fn 6421  df-f 6422  df-f1 6423  df-fo 6424  df-f1o 6425  df-fv 6426  df-riota 7212  df-ov 7258  df-oprab 7259  df-mpo 7260  df-om 7688  df-1st 7804  df-2nd 7805  df-frecs 8068  df-wrecs 8099  df-recs 8173  df-rdg 8212  df-er 8456  df-en 8692  df-dom 8693  df-sdom 8694  df-sup 9131  df-inf 9132  df-pnf 10942  df-mnf 10943  df-xr 10944  df-ltxr 10945  df-le 10946  df-sub 11137  df-neg 11138  df-div 11563  df-nn 11904  df-2 11966  df-n0 12164  df-z 12250  df-uz 12512  df-rp 12660  df-fz 13169  df-fzo 13312  df-fl 13440  df-mod 13518  df-seq 13650  df-exp 13711  df-dvds 15892  df-bits 16057

This theorem is referenced by:  bitsinv1  16077  smumullem  16127