Theorem bitsinv1lem 16380

Description: Lemma for bitsinv1 16381. (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 7376	. . 3 ⊢ ((2↑𝑀) = if(𝑀 ∈ (bits‘𝑁), (2↑𝑀), 0) → ((𝑁 mod (2↑𝑀)) + (2↑𝑀)) = ((𝑁 mod (2↑𝑀)) + if(𝑀 ∈ (bits‘𝑁), (2↑𝑀), 0)))
2	1	eqeq2d 2748	. 2 ⊢ ((2↑𝑀) = if(𝑀 ∈ (bits‘𝑁), (2↑𝑀), 0) → ((𝑁 mod (2↑(𝑀 + 1))) = ((𝑁 mod (2↑𝑀)) + (2↑𝑀)) ↔ (𝑁 mod (2↑(𝑀 + 1))) = ((𝑁 mod (2↑𝑀)) + if(𝑀 ∈ (bits‘𝑁), (2↑𝑀), 0))))
3		oveq2 7376	. . 3 ⊢ (0 = if(𝑀 ∈ (bits‘𝑁), (2↑𝑀), 0) → ((𝑁 mod (2↑𝑀)) + 0) = ((𝑁 mod (2↑𝑀)) + if(𝑀 ∈ (bits‘𝑁), (2↑𝑀), 0)))
4	3	eqeq2d 2748	. 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 12230	. . . . . . . . 9 ⊢ 2 ∈ ℕ
7	6	a1i 11	. . . . . . . 8 ⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → 2 ∈ ℕ)
8		simpr 484	. . . . . . . 8 ⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → 𝑀 ∈ ℕ0)
9	7, 8	nnexpcld 14180	. . . . . . 7 ⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → (2↑𝑀) ∈ ℕ)
10	5, 9	zmodcld 13824	. . . . . 6 ⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → (𝑁 mod (2↑𝑀)) ∈ ℕ0)
11	10	nn0cnd 12476	. . . . 5 ⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → (𝑁 mod (2↑𝑀)) ∈ ℂ)
12	11	adantr 480	. . . 4 ⊢ (((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) ∧ 𝑀 ∈ (bits‘𝑁)) → (𝑁 mod (2↑𝑀)) ∈ ℂ)
13		1nn0 12429	. . . . . . . . . 10 ⊢ 1 ∈ ℕ0
14	13	a1i 11	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → 1 ∈ ℕ0)
15	8, 14	nn0addcld 12478	. . . . . . . 8 ⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → (𝑀 + 1) ∈ ℕ0)
16	7, 15	nnexpcld 14180	. . . . . . 7 ⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → (2↑(𝑀 + 1)) ∈ ℕ)
17	5, 16	zmodcld 13824	. . . . . 6 ⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → (𝑁 mod (2↑(𝑀 + 1))) ∈ ℕ0)
18	17	nn0cnd 12476	. . . . 5 ⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → (𝑁 mod (2↑(𝑀 + 1))) ∈ ℂ)
19	18	adantr 480	. . . 4 ⊢ (((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) ∧ 𝑀 ∈ (bits‘𝑁)) → (𝑁 mod (2↑(𝑀 + 1))) ∈ ℂ)
20	12, 19	pncan3d 11507	. . 3 ⊢ (((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) ∧ 𝑀 ∈ (bits‘𝑁)) → ((𝑁 mod (2↑𝑀)) + ((𝑁 mod (2↑(𝑀 + 1))) − (𝑁 mod (2↑𝑀)))) = (𝑁 mod (2↑(𝑀 + 1))))
21	18, 11	subcld 11504	. . . . . 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 769	. . . . . . 7 ⊢ (((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) ∧ 𝑀 ∈ (bits‘𝑁)) → 𝑀 ∈ ℕ0)
25	23, 24	nnexpcld 14180	. . . . . 6 ⊢ (((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) ∧ 𝑀 ∈ (bits‘𝑁)) → (2↑𝑀) ∈ ℕ)
26	25	nncnd 12173	. . . . 5 ⊢ (((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) ∧ 𝑀 ∈ (bits‘𝑁)) → (2↑𝑀) ∈ ℂ)
27		2cnd 12235	. . . . . . 7 ⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → 2 ∈ ℂ)
28		2ne0 12261	. . . . . . . 8 ⊢ 2 ≠ 0
29	28	a1i 11	. . . . . . 7 ⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → 2 ≠ 0)
30	8	nn0zd 12525	. . . . . . 7 ⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → 𝑀 ∈ ℤ)
31	27, 29, 30	expne0d 14087	. . . . . 6 ⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → (2↑𝑀) ≠ 0)
32	31	adantr 480	. . . . 5 ⊢ (((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) ∧ 𝑀 ∈ (bits‘𝑁)) → (2↑𝑀) ≠ 0)
33		z0even 16306	. . . . . . . . . 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 5138	. . . . . . . . 9 ⊢ ((((𝑁 mod (2↑(𝑀 + 1))) − (𝑁 mod (2↑𝑀))) / (2↑𝑀)) = 0 → 2 ∥ (((𝑁 mod (2↑(𝑀 + 1))) − (𝑁 mod (2↑𝑀))) / (2↑𝑀)))
36		bitsval2 16364	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → (𝑀 ∈ (bits‘𝑁) ↔ ¬ 2 ∥ (⌊‘(𝑁 / (2↑𝑀)))))
37	5	zred 12608	. . . . . . . . . . . . . . 15 ⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → 𝑁 ∈ ℝ)
38	9	nnrpd 12959	. . . . . . . . . . . . . . 15 ⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → (2↑𝑀) ∈ ℝ+)
39		moddiffl 13814	. . . . . . . . . . . . . . 15 ⊢ ((𝑁 ∈ ℝ ∧ (2↑𝑀) ∈ ℝ+) → ((𝑁 − (𝑁 mod (2↑𝑀))) / (2↑𝑀)) = (⌊‘(𝑁 / (2↑𝑀))))
40	37, 38, 39	syl2anc 585	. . . . . . . . . . . . . 14 ⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → ((𝑁 − (𝑁 mod (2↑𝑀))) / (2↑𝑀)) = (⌊‘(𝑁 / (2↑𝑀))))
41	40	breq2d 5112	. . . . . . . . . . . . 13 ⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → (2 ∥ ((𝑁 − (𝑁 mod (2↑𝑀))) / (2↑𝑀)) ↔ 2 ∥ (⌊‘(𝑁 / (2↑𝑀)))))
42		2z 12535	. . . . . . . . . . . . . . 15 ⊢ 2 ∈ ℤ
43	42	a1i 11	. . . . . . . . . . . . . 14 ⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → 2 ∈ ℤ)
44		moddifz 13815	. . . . . . . . . . . . . . 15 ⊢ ((𝑁 ∈ ℝ ∧ (2↑𝑀) ∈ ℝ+) → ((𝑁 − (𝑁 mod (2↑𝑀))) / (2↑𝑀)) ∈ ℤ)
45	37, 38, 44	syl2anc 585	. . . . . . . . . . . . . 14 ⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → ((𝑁 − (𝑁 mod (2↑𝑀))) / (2↑𝑀)) ∈ ℤ)
46	5	zcnd 12609	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → 𝑁 ∈ ℂ)
47	46, 11, 18	nnncan1d 11538	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → ((𝑁 − (𝑁 mod (2↑𝑀))) − (𝑁 − (𝑁 mod (2↑(𝑀 + 1))))) = ((𝑁 mod (2↑(𝑀 + 1))) − (𝑁 mod (2↑𝑀))))
48	47	oveq1d 7383	. . . . . . . . . . . . . . . 16 ⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → (((𝑁 − (𝑁 mod (2↑𝑀))) − (𝑁 − (𝑁 mod (2↑(𝑀 + 1))))) / (2↑𝑀)) = (((𝑁 mod (2↑(𝑀 + 1))) − (𝑁 mod (2↑𝑀))) / (2↑𝑀)))
49	46, 11	subcld 11504	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → (𝑁 − (𝑁 mod (2↑𝑀))) ∈ ℂ)
50	46, 18	subcld 11504	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → (𝑁 − (𝑁 mod (2↑(𝑀 + 1)))) ∈ ℂ)
51	9	nncnd 12173	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → (2↑𝑀) ∈ ℂ)
52	49, 50, 51, 31	divsubdird 11968	. . . . . . . . . . . . . . . 16 ⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → (((𝑁 − (𝑁 mod (2↑𝑀))) − (𝑁 − (𝑁 mod (2↑(𝑀 + 1))))) / (2↑𝑀)) = (((𝑁 − (𝑁 mod (2↑𝑀))) / (2↑𝑀)) − ((𝑁 − (𝑁 mod (2↑(𝑀 + 1)))) / (2↑𝑀))))
53	48, 52	eqtr3d 2774	. . . . . . . . . . . . . . 15 ⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → (((𝑁 mod (2↑(𝑀 + 1))) − (𝑁 mod (2↑𝑀))) / (2↑𝑀)) = (((𝑁 − (𝑁 mod (2↑𝑀))) / (2↑𝑀)) − ((𝑁 − (𝑁 mod (2↑(𝑀 + 1)))) / (2↑𝑀))))
54	27, 50	mulcomd 11165	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → (2 · (𝑁 − (𝑁 mod (2↑(𝑀 + 1))))) = ((𝑁 − (𝑁 mod (2↑(𝑀 + 1)))) · 2))
55	27, 51	mulcomd 11165	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → (2 · (2↑𝑀)) = ((2↑𝑀) · 2))
56	27, 8	expp1d 14082	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → (2↑(𝑀 + 1)) = ((2↑𝑀) · 2))
57	55, 56	eqtr4d 2775	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → (2 · (2↑𝑀)) = (2↑(𝑀 + 1)))
58	54, 57	oveq12d 7386	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → ((2 · (𝑁 − (𝑁 mod (2↑(𝑀 + 1))))) / (2 · (2↑𝑀))) = (((𝑁 − (𝑁 mod (2↑(𝑀 + 1)))) · 2) / (2↑(𝑀 + 1))))
59	50, 51, 27, 31, 29	divcan5d 11955	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → ((2 · (𝑁 − (𝑁 mod (2↑(𝑀 + 1))))) / (2 · (2↑𝑀))) = ((𝑁 − (𝑁 mod (2↑(𝑀 + 1)))) / (2↑𝑀)))
60	16	nncnd 12173	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → (2↑(𝑀 + 1)) ∈ ℂ)
61	30	peano2zd 12611	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → (𝑀 + 1) ∈ ℤ)
62	27, 29, 61	expne0d 14087	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → (2↑(𝑀 + 1)) ≠ 0)
63	50, 27, 60, 62	div23d 11966	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → (((𝑁 − (𝑁 mod (2↑(𝑀 + 1)))) · 2) / (2↑(𝑀 + 1))) = (((𝑁 − (𝑁 mod (2↑(𝑀 + 1)))) / (2↑(𝑀 + 1))) · 2))
64	58, 59, 63	3eqtr3d 2780	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → ((𝑁 − (𝑁 mod (2↑(𝑀 + 1)))) / (2↑𝑀)) = (((𝑁 − (𝑁 mod (2↑(𝑀 + 1)))) / (2↑(𝑀 + 1))) · 2))
65	16	nnrpd 12959	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → (2↑(𝑀 + 1)) ∈ ℝ+)
66		moddifz 13815	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑁 ∈ ℝ ∧ (2↑(𝑀 + 1)) ∈ ℝ+) → ((𝑁 − (𝑁 mod (2↑(𝑀 + 1)))) / (2↑(𝑀 + 1))) ∈ ℤ)
67	37, 65, 66	syl2anc 585	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → ((𝑁 − (𝑁 mod (2↑(𝑀 + 1)))) / (2↑(𝑀 + 1))) ∈ ℤ)
68	67, 43	zmulcld 12614	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → (((𝑁 − (𝑁 mod (2↑(𝑀 + 1)))) / (2↑(𝑀 + 1))) · 2) ∈ ℤ)
69	64, 68	eqeltrd 2837	. . . . . . . . . . . . . . . 16 ⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → ((𝑁 − (𝑁 mod (2↑(𝑀 + 1)))) / (2↑𝑀)) ∈ ℤ)
70	45, 69	zsubcld 12613	. . . . . . . . . . . . . . 15 ⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → (((𝑁 − (𝑁 mod (2↑𝑀))) / (2↑𝑀)) − ((𝑁 − (𝑁 mod (2↑(𝑀 + 1)))) / (2↑𝑀))) ∈ ℤ)
71	53, 70	eqeltrd 2837	. . . . . . . . . . . . . 14 ⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → (((𝑁 mod (2↑(𝑀 + 1))) − (𝑁 mod (2↑𝑀))) / (2↑𝑀)) ∈ ℤ)
72		dvdsmul2 16217	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑁 − (𝑁 mod (2↑(𝑀 + 1)))) / (2↑(𝑀 + 1))) ∈ ℤ ∧ 2 ∈ ℤ) → 2 ∥ (((𝑁 − (𝑁 mod (2↑(𝑀 + 1)))) / (2↑(𝑀 + 1))) · 2))
73	67, 43, 72	syl2anc 585	. . . . . . . . . . . . . . 15 ⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → 2 ∥ (((𝑁 − (𝑁 mod (2↑(𝑀 + 1)))) / (2↑(𝑀 + 1))) · 2))
74	46, 18, 11	nnncan2d 11539	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → ((𝑁 − (𝑁 mod (2↑𝑀))) − ((𝑁 mod (2↑(𝑀 + 1))) − (𝑁 mod (2↑𝑀)))) = (𝑁 − (𝑁 mod (2↑(𝑀 + 1)))))
75	74	oveq1d 7383	. . . . . . . . . . . . . . . 16 ⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → (((𝑁 − (𝑁 mod (2↑𝑀))) − ((𝑁 mod (2↑(𝑀 + 1))) − (𝑁 mod (2↑𝑀)))) / (2↑𝑀)) = ((𝑁 − (𝑁 mod (2↑(𝑀 + 1)))) / (2↑𝑀)))
76	49, 21, 51, 31	divsubdird 11968	. . . . . . . . . . . . . . . 16 ⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → (((𝑁 − (𝑁 mod (2↑𝑀))) − ((𝑁 mod (2↑(𝑀 + 1))) − (𝑁 mod (2↑𝑀)))) / (2↑𝑀)) = (((𝑁 − (𝑁 mod (2↑𝑀))) / (2↑𝑀)) − (((𝑁 mod (2↑(𝑀 + 1))) − (𝑁 mod (2↑𝑀))) / (2↑𝑀))))
77	75, 76, 64	3eqtr3d 2780	. . . . . . . . . . . . . . 15 ⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → (((𝑁 − (𝑁 mod (2↑𝑀))) / (2↑𝑀)) − (((𝑁 mod (2↑(𝑀 + 1))) − (𝑁 mod (2↑𝑀))) / (2↑𝑀))) = (((𝑁 − (𝑁 mod (2↑(𝑀 + 1)))) / (2↑(𝑀 + 1))) · 2))
78	73, 77	breqtrrd 5128	. . . . . . . . . . . . . 14 ⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → 2 ∥ (((𝑁 − (𝑁 mod (2↑𝑀))) / (2↑𝑀)) − (((𝑁 mod (2↑(𝑀 + 1))) − (𝑁 mod (2↑𝑀))) / (2↑𝑀))))
79		dvdssub2 16240	. . . . . . . . . . . . . 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 1376	. . . . . . . . . . . . 13 ⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → (2 ∥ ((𝑁 − (𝑁 mod (2↑𝑀))) / (2↑𝑀)) ↔ 2 ∥ (((𝑁 mod (2↑(𝑀 + 1))) − (𝑁 mod (2↑𝑀))) / (2↑𝑀))))
81	41, 80	bitr3d 281	. . . . . . . . . . . 12 ⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → (2 ∥ (⌊‘(𝑁 / (2↑𝑀))) ↔ 2 ∥ (((𝑁 mod (2↑(𝑀 + 1))) − (𝑁 mod (2↑𝑀))) / (2↑𝑀))))
82	81	notbid 318	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → (¬ 2 ∥ (⌊‘(𝑁 / (2↑𝑀))) ↔ ¬ 2 ∥ (((𝑁 mod (2↑(𝑀 + 1))) − (𝑁 mod (2↑𝑀))) / (2↑𝑀))))
83	36, 82	bitrd 279	. . . . . . . . . 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	imbitrid 244	. . . . . . . 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 11379	. . . . . . . . . . . . . . 15 ⊢ -1 = (0 − 1)
88	51	mulm1d 11601	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → (-1 · (2↑𝑀)) = -(2↑𝑀))
89	9	nnred 12172	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → (2↑𝑀) ∈ ℝ)
90	89	renegcld 11576	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → -(2↑𝑀) ∈ ℝ)
91	37, 38	modcld 13807	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → (𝑁 mod (2↑𝑀)) ∈ ℝ)
92	91	renegcld 11576	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → -(𝑁 mod (2↑𝑀)) ∈ ℝ)
93	37, 65	modcld 13807	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → (𝑁 mod (2↑(𝑀 + 1))) ∈ ℝ)
94	93, 91	resubcld 11577	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → ((𝑁 mod (2↑(𝑀 + 1))) − (𝑁 mod (2↑𝑀))) ∈ ℝ)
95		modlt 13812	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑁 ∈ ℝ ∧ (2↑𝑀) ∈ ℝ+) → (𝑁 mod (2↑𝑀)) < (2↑𝑀))
96	37, 38, 95	syl2anc 585	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → (𝑁 mod (2↑𝑀)) < (2↑𝑀))
97	91, 89	ltnegd 11727	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → ((𝑁 mod (2↑𝑀)) < (2↑𝑀) ↔ -(2↑𝑀) < -(𝑁 mod (2↑𝑀))))
98	96, 97	mpbid 232	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → -(2↑𝑀) < -(𝑁 mod (2↑𝑀)))
99		df-neg 11379	. . . . . . . . . . . . . . . . . . 19 ⊢ -(𝑁 mod (2↑𝑀)) = (0 − (𝑁 mod (2↑𝑀)))
100		0red 11147	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → 0 ∈ ℝ)
101		modge0 13811	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑁 ∈ ℝ ∧ (2↑(𝑀 + 1)) ∈ ℝ+) → 0 ≤ (𝑁 mod (2↑(𝑀 + 1))))
102	37, 65, 101	syl2anc 585	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → 0 ≤ (𝑁 mod (2↑(𝑀 + 1))))
103	100, 93, 91, 102	lesub1dd 11765	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → (0 − (𝑁 mod (2↑𝑀))) ≤ ((𝑁 mod (2↑(𝑀 + 1))) − (𝑁 mod (2↑𝑀))))
104	99, 103	eqbrtrid 5135	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → -(𝑁 mod (2↑𝑀)) ≤ ((𝑁 mod (2↑(𝑀 + 1))) − (𝑁 mod (2↑𝑀))))
105	90, 92, 94, 98, 104	ltletrd 11305	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → -(2↑𝑀) < ((𝑁 mod (2↑(𝑀 + 1))) − (𝑁 mod (2↑𝑀))))
106	88, 105	eqbrtrd 5122	. . . . . . . . . . . . . . . 16 ⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → (-1 · (2↑𝑀)) < ((𝑁 mod (2↑(𝑀 + 1))) − (𝑁 mod (2↑𝑀))))
107		1red 11145	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → 1 ∈ ℝ)
108	107	renegcld 11576	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → -1 ∈ ℝ)
109	108, 94, 38	ltmuldivd 13008	. . . . . . . . . . . . . . . 16 ⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → ((-1 · (2↑𝑀)) < ((𝑁 mod (2↑(𝑀 + 1))) − (𝑁 mod (2↑𝑀))) ↔ -1 < (((𝑁 mod (2↑(𝑀 + 1))) − (𝑁 mod (2↑𝑀))) / (2↑𝑀))))
110	106, 109	mpbid 232	. . . . . . . . . . . . . . 15 ⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → -1 < (((𝑁 mod (2↑(𝑀 + 1))) − (𝑁 mod (2↑𝑀))) / (2↑𝑀)))
111	87, 110	eqbrtrrid 5136	. . . . . . . . . . . . . 14 ⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → (0 − 1) < (((𝑁 mod (2↑(𝑀 + 1))) − (𝑁 mod (2↑𝑀))) / (2↑𝑀)))
112		0zd 12512	. . . . . . . . . . . . . . 15 ⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → 0 ∈ ℤ)
113		zlem1lt 12555	. . . . . . . . . . . . . . 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 585	. . . . . . . . . . . . . 14 ⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → (0 ≤ (((𝑁 mod (2↑(𝑀 + 1))) − (𝑁 mod (2↑𝑀))) / (2↑𝑀)) ↔ (0 − 1) < (((𝑁 mod (2↑(𝑀 + 1))) − (𝑁 mod (2↑𝑀))) / (2↑𝑀))))
115	111, 114	mpbird 257	. . . . . . . . . . . . 13 ⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → 0 ≤ (((𝑁 mod (2↑(𝑀 + 1))) − (𝑁 mod (2↑𝑀))) / (2↑𝑀)))
116		elnn0z 12513	. . . . . . . . . . . . 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 584	. . . . . . . . . . . 12 ⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → (((𝑁 mod (2↑(𝑀 + 1))) − (𝑁 mod (2↑𝑀))) / (2↑𝑀)) ∈ ℕ0)
118		nn0uz 12801	. . . . . . . . . . . 12 ⊢ ℕ0 = (ℤ≥‘0)
119	117, 118	eleqtrdi 2847	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → (((𝑁 mod (2↑(𝑀 + 1))) − (𝑁 mod (2↑𝑀))) / (2↑𝑀)) ∈ (ℤ≥‘0))
120	16	nnred 12172	. . . . . . . . . . . . . 14 ⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → (2↑(𝑀 + 1)) ∈ ℝ)
121		modge0 13811	. . . . . . . . . . . . . . . 16 ⊢ ((𝑁 ∈ ℝ ∧ (2↑𝑀) ∈ ℝ+) → 0 ≤ (𝑁 mod (2↑𝑀)))
122	37, 38, 121	syl2anc 585	. . . . . . . . . . . . . . 15 ⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → 0 ≤ (𝑁 mod (2↑𝑀)))
123	93, 91	subge02d 11741	. . . . . . . . . . . . . . 15 ⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → (0 ≤ (𝑁 mod (2↑𝑀)) ↔ ((𝑁 mod (2↑(𝑀 + 1))) − (𝑁 mod (2↑𝑀))) ≤ (𝑁 mod (2↑(𝑀 + 1)))))
124	122, 123	mpbid 232	. . . . . . . . . . . . . 14 ⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → ((𝑁 mod (2↑(𝑀 + 1))) − (𝑁 mod (2↑𝑀))) ≤ (𝑁 mod (2↑(𝑀 + 1))))
125		modlt 13812	. . . . . . . . . . . . . . 15 ⊢ ((𝑁 ∈ ℝ ∧ (2↑(𝑀 + 1)) ∈ ℝ+) → (𝑁 mod (2↑(𝑀 + 1))) < (2↑(𝑀 + 1)))
126	37, 65, 125	syl2anc 585	. . . . . . . . . . . . . 14 ⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → (𝑁 mod (2↑(𝑀 + 1))) < (2↑(𝑀 + 1)))
127	94, 93, 120, 124, 126	lelttrd 11303	. . . . . . . . . . . . 13 ⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → ((𝑁 mod (2↑(𝑀 + 1))) − (𝑁 mod (2↑𝑀))) < (2↑(𝑀 + 1)))
128	127, 56	breqtrd 5126	. . . . . . . . . . . 12 ⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → ((𝑁 mod (2↑(𝑀 + 1))) − (𝑁 mod (2↑𝑀))) < ((2↑𝑀) · 2))
129	7	nnred 12172	. . . . . . . . . . . . 13 ⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → 2 ∈ ℝ)
130	94, 129, 38	ltdivmuld 13012	. . . . . . . . . . . 12 ⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → ((((𝑁 mod (2↑(𝑀 + 1))) − (𝑁 mod (2↑𝑀))) / (2↑𝑀)) < 2 ↔ ((𝑁 mod (2↑(𝑀 + 1))) − (𝑁 mod (2↑𝑀))) < ((2↑𝑀) · 2)))
131	128, 130	mpbird 257	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → (((𝑁 mod (2↑(𝑀 + 1))) − (𝑁 mod (2↑𝑀))) / (2↑𝑀)) < 2)
132		elfzo2 13590	. . . . . . . . . . 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 1345	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → (((𝑁 mod (2↑(𝑀 + 1))) − (𝑁 mod (2↑𝑀))) / (2↑𝑀)) ∈ (0..^2))
134		fzo0to2pr 13678	. . . . . . . . . 10 ⊢ (0..^2) = {0, 1}
135	133, 134	eleqtrdi 2847	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → (((𝑁 mod (2↑(𝑀 + 1))) − (𝑁 mod (2↑𝑀))) / (2↑𝑀)) ∈ {0, 1})
136		elpri 4606	. . . . . . . . 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 865	. . . . . . 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 11937	. . . 4 ⊢ (((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) ∧ 𝑀 ∈ (bits‘𝑁)) → ((𝑁 mod (2↑(𝑀 + 1))) − (𝑁 mod (2↑𝑀))) = (2↑𝑀))
142	141	oveq2d 7384	. . 3 ⊢ (((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) ∧ 𝑀 ∈ (bits‘𝑁)) → ((𝑁 mod (2↑𝑀)) + ((𝑁 mod (2↑(𝑀 + 1))) − (𝑁 mod (2↑𝑀)))) = ((𝑁 mod (2↑𝑀)) + (2↑𝑀)))
143	20, 142	eqtr3d 2774	. 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 16307	. . . . . . . . . 10 ⊢ ¬ 2 ∥ 1
150		breq2 5104	. . . . . . . . . 10 ⊢ ((((𝑁 mod (2↑(𝑀 + 1))) − (𝑁 mod (2↑𝑀))) / (2↑𝑀)) = 1 → (2 ∥ (((𝑁 mod (2↑(𝑀 + 1))) − (𝑁 mod (2↑𝑀))) / (2↑𝑀)) ↔ 2 ∥ 1))
151	149, 150	mtbiri 327	. . . . . . . . 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 259	. . . . . . 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 11936	. . . 4 ⊢ (((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) ∧ ¬ 𝑀 ∈ (bits‘𝑁)) → ((𝑁 mod (2↑(𝑀 + 1))) − (𝑁 mod (2↑𝑀))) = 0)
157	144, 145, 156	subeq0d 11512	. . 3 ⊢ (((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) ∧ ¬ 𝑀 ∈ (bits‘𝑁)) → (𝑁 mod (2↑(𝑀 + 1))) = (𝑁 mod (2↑𝑀)))
158	145	addridd 11345	. . 3 ⊢ (((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) ∧ ¬ 𝑀 ∈ (bits‘𝑁)) → ((𝑁 mod (2↑𝑀)) + 0) = (𝑁 mod (2↑𝑀)))
159	157, 158	eqtr4d 2775	. 2 ⊢ (((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) ∧ ¬ 𝑀 ∈ (bits‘𝑁)) → (𝑁 mod (2↑(𝑀 + 1))) = ((𝑁 mod (2↑𝑀)) + 0))
160	2, 4, 143, 159	ifbothda 4520	1 ⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → (𝑁 mod (2↑(𝑀 + 1))) = ((𝑁 mod (2↑𝑀)) + if(𝑀 ∈ (bits‘𝑁), (2↑𝑀), 0)))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395   ∨ wo 848   = wceq 1542   ∈ wcel 2114   ≠ wne 2933  ifcif 4481  {cpr 4584   class class class wbr 5100  ‘cfv 6500  (class class class)co 7368  ℂcc 11036  ℝcr 11037  0cc0 11038  1c1 11039   + caddc 11041   · cmul 11043   < clt 11178   ≤ cle 11179   − cmin 11376  -cneg 11377   / cdiv 11806  ℕcn 12157  2c2 12212  ℕ₀cn0 12413  ℤcz 12500  ℤ_≥cuz 12763  ℝ⁺crp 12917  ..^cfzo 13582  ⌊cfl 13722   mod cmo 13801  ↑cexp 13996   ∥ cdvds 16191  bitscbits 16358

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5243  ax-nul 5253  ax-pow 5312  ax-pr 5379  ax-un 7690  ax-cnex 11094  ax-resscn 11095  ax-1cn 11096  ax-icn 11097  ax-addcl 11098  ax-addrcl 11099  ax-mulcl 11100  ax-mulrcl 11101  ax-mulcom 11102  ax-addass 11103  ax-mulass 11104  ax-distr 11105  ax-i2m1 11106  ax-1ne0 11107  ax-1rid 11108  ax-rnegex 11109  ax-rrecex 11110  ax-cnre 11111  ax-pre-lttri 11112  ax-pre-lttrn 11113  ax-pre-ltadd 11114  ax-pre-mulgt0 11115  ax-pre-sup 11116

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-nel 3038  df-ral 3053  df-rex 3063  df-rmo 3352  df-reu 3353  df-rab 3402  df-v 3444  df-sbc 3743  df-csb 3852  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-pss 3923  df-nul 4288  df-if 4482  df-pw 4558  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-iun 4950  df-br 5101  df-opab 5163  df-mpt 5182  df-tr 5208  df-id 5527  df-eprel 5532  df-po 5540  df-so 5541  df-fr 5585  df-we 5587  df-xp 5638  df-rel 5639  df-cnv 5640  df-co 5641  df-dm 5642  df-rn 5643  df-res 5644  df-ima 5645  df-pred 6267  df-ord 6328  df-on 6329  df-lim 6330  df-suc 6331  df-iota 6456  df-fun 6502  df-fn 6503  df-f 6504  df-f1 6505  df-fo 6506  df-f1o 6507  df-fv 6508  df-riota 7325  df-ov 7371  df-oprab 7372  df-mpo 7373  df-om 7819  df-1st 7943  df-2nd 7944  df-frecs 8233  df-wrecs 8264  df-recs 8313  df-rdg 8351  df-er 8645  df-en 8896  df-dom 8897  df-sdom 8898  df-sup 9357  df-inf 9358  df-pnf 11180  df-mnf 11181  df-xr 11182  df-ltxr 11183  df-le 11184  df-sub 11378  df-neg 11379  df-div 11807  df-nn 12158  df-2 12220  df-n0 12414  df-z 12501  df-uz 12764  df-rp 12918  df-fz 13436  df-fzo 13583  df-fl 13724  df-mod 13802  df-seq 13937  df-exp 13997  df-dvds 16192  df-bits 16361

This theorem is referenced by:  bitsinv1  16381  smumullem  16431