MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  bitsinv1lem Structured version   Visualization version   GIF version

Theorem bitsinv1lem 15385
Description: Lemma for bitsinv1 15386. (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
StepHypRef Expression
1 oveq2 6885 . . 3 ((2↑𝑀) = if(𝑀 ∈ (bits‘𝑁), (2↑𝑀), 0) → ((𝑁 mod (2↑𝑀)) + (2↑𝑀)) = ((𝑁 mod (2↑𝑀)) + if(𝑀 ∈ (bits‘𝑁), (2↑𝑀), 0)))
21eqeq2d 2823 . 2 ((2↑𝑀) = if(𝑀 ∈ (bits‘𝑁), (2↑𝑀), 0) → ((𝑁 mod (2↑(𝑀 + 1))) = ((𝑁 mod (2↑𝑀)) + (2↑𝑀)) ↔ (𝑁 mod (2↑(𝑀 + 1))) = ((𝑁 mod (2↑𝑀)) + if(𝑀 ∈ (bits‘𝑁), (2↑𝑀), 0))))
3 oveq2 6885 . . 3 (0 = if(𝑀 ∈ (bits‘𝑁), (2↑𝑀), 0) → ((𝑁 mod (2↑𝑀)) + 0) = ((𝑁 mod (2↑𝑀)) + if(𝑀 ∈ (bits‘𝑁), (2↑𝑀), 0)))
43eqeq2d 2823 . 2 (0 = if(𝑀 ∈ (bits‘𝑁), (2↑𝑀), 0) → ((𝑁 mod (2↑(𝑀 + 1))) = ((𝑁 mod (2↑𝑀)) + 0) ↔ (𝑁 mod (2↑(𝑀 + 1))) = ((𝑁 mod (2↑𝑀)) + if(𝑀 ∈ (bits‘𝑁), (2↑𝑀), 0))))
5 simpl 470 . . . . . . 7 ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → 𝑁 ∈ ℤ)
6 2nn 11465 . . . . . . . . 9 2 ∈ ℕ
76a1i 11 . . . . . . . 8 ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → 2 ∈ ℕ)
8 simpr 473 . . . . . . . 8 ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → 𝑀 ∈ ℕ0)
97, 8nnexpcld 13256 . . . . . . 7 ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → (2↑𝑀) ∈ ℕ)
105, 9zmodcld 12918 . . . . . 6 ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → (𝑁 mod (2↑𝑀)) ∈ ℕ0)
1110nn0cnd 11622 . . . . 5 ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → (𝑁 mod (2↑𝑀)) ∈ ℂ)
1211adantr 468 . . . 4 (((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) ∧ 𝑀 ∈ (bits‘𝑁)) → (𝑁 mod (2↑𝑀)) ∈ ℂ)
13 1nn0 11578 . . . . . . . . . 10 1 ∈ ℕ0
1413a1i 11 . . . . . . . . 9 ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → 1 ∈ ℕ0)
158, 14nn0addcld 11624 . . . . . . . 8 ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → (𝑀 + 1) ∈ ℕ0)
167, 15nnexpcld 13256 . . . . . . 7 ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → (2↑(𝑀 + 1)) ∈ ℕ)
175, 16zmodcld 12918 . . . . . 6 ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → (𝑁 mod (2↑(𝑀 + 1))) ∈ ℕ0)
1817nn0cnd 11622 . . . . 5 ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → (𝑁 mod (2↑(𝑀 + 1))) ∈ ℂ)
1918adantr 468 . . . 4 (((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) ∧ 𝑀 ∈ (bits‘𝑁)) → (𝑁 mod (2↑(𝑀 + 1))) ∈ ℂ)
2012, 19pncan3d 10683 . . 3 (((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) ∧ 𝑀 ∈ (bits‘𝑁)) → ((𝑁 mod (2↑𝑀)) + ((𝑁 mod (2↑(𝑀 + 1))) − (𝑁 mod (2↑𝑀)))) = (𝑁 mod (2↑(𝑀 + 1))))
2118, 11subcld 10680 . . . . . 6 ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → ((𝑁 mod (2↑(𝑀 + 1))) − (𝑁 mod (2↑𝑀))) ∈ ℂ)
2221adantr 468 . . . . 5 (((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) ∧ 𝑀 ∈ (bits‘𝑁)) → ((𝑁 mod (2↑(𝑀 + 1))) − (𝑁 mod (2↑𝑀))) ∈ ℂ)
236a1i 11 . . . . . . 7 (((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) ∧ 𝑀 ∈ (bits‘𝑁)) → 2 ∈ ℕ)
24 simplr 776 . . . . . . 7 (((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) ∧ 𝑀 ∈ (bits‘𝑁)) → 𝑀 ∈ ℕ0)
2523, 24nnexpcld 13256 . . . . . 6 (((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) ∧ 𝑀 ∈ (bits‘𝑁)) → (2↑𝑀) ∈ ℕ)
2625nncnd 11324 . . . . 5 (((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) ∧ 𝑀 ∈ (bits‘𝑁)) → (2↑𝑀) ∈ ℂ)
27 2cnd 11380 . . . . . . 7 ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → 2 ∈ ℂ)
28 2ne0 11399 . . . . . . . 8 2 ≠ 0
2928a1i 11 . . . . . . 7 ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → 2 ≠ 0)
308nn0zd 11749 . . . . . . 7 ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → 𝑀 ∈ ℤ)
3127, 29, 30expne0d 13240 . . . . . 6 ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → (2↑𝑀) ≠ 0)
3231adantr 468 . . . . 5 (((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) ∧ 𝑀 ∈ (bits‘𝑁)) → (2↑𝑀) ≠ 0)
33 2z 11678 . . . . . . . . . . 11 2 ∈ ℤ
34 dvds0 15223 . . . . . . . . . . 11 (2 ∈ ℤ → 2 ∥ 0)
3533, 34ax-mp 5 . . . . . . . . . 10 2 ∥ 0
36 id 22 . . . . . . . . . 10 ((((𝑁 mod (2↑(𝑀 + 1))) − (𝑁 mod (2↑𝑀))) / (2↑𝑀)) = 0 → (((𝑁 mod (2↑(𝑀 + 1))) − (𝑁 mod (2↑𝑀))) / (2↑𝑀)) = 0)
3735, 36syl5breqr 4889 . . . . . . . . 9 ((((𝑁 mod (2↑(𝑀 + 1))) − (𝑁 mod (2↑𝑀))) / (2↑𝑀)) = 0 → 2 ∥ (((𝑁 mod (2↑(𝑀 + 1))) − (𝑁 mod (2↑𝑀))) / (2↑𝑀)))
38 bitsval2 15369 . . . . . . . . . . 11 ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → (𝑀 ∈ (bits‘𝑁) ↔ ¬ 2 ∥ (⌊‘(𝑁 / (2↑𝑀)))))
395zred 11751 . . . . . . . . . . . . . . 15 ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → 𝑁 ∈ ℝ)
409nnrpd 12087 . . . . . . . . . . . . . . 15 ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → (2↑𝑀) ∈ ℝ+)
41 moddiffl 12908 . . . . . . . . . . . . . . 15 ((𝑁 ∈ ℝ ∧ (2↑𝑀) ∈ ℝ+) → ((𝑁 − (𝑁 mod (2↑𝑀))) / (2↑𝑀)) = (⌊‘(𝑁 / (2↑𝑀))))
4239, 40, 41syl2anc 575 . . . . . . . . . . . . . 14 ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → ((𝑁 − (𝑁 mod (2↑𝑀))) / (2↑𝑀)) = (⌊‘(𝑁 / (2↑𝑀))))
4342breq2d 4863 . . . . . . . . . . . . 13 ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → (2 ∥ ((𝑁 − (𝑁 mod (2↑𝑀))) / (2↑𝑀)) ↔ 2 ∥ (⌊‘(𝑁 / (2↑𝑀)))))
4433a1i 11 . . . . . . . . . . . . . 14 ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → 2 ∈ ℤ)
45 moddifz 12909 . . . . . . . . . . . . . . 15 ((𝑁 ∈ ℝ ∧ (2↑𝑀) ∈ ℝ+) → ((𝑁 − (𝑁 mod (2↑𝑀))) / (2↑𝑀)) ∈ ℤ)
4639, 40, 45syl2anc 575 . . . . . . . . . . . . . 14 ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → ((𝑁 − (𝑁 mod (2↑𝑀))) / (2↑𝑀)) ∈ ℤ)
475zcnd 11752 . . . . . . . . . . . . . . . . . 18 ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → 𝑁 ∈ ℂ)
4847, 11, 18nnncan1d 10714 . . . . . . . . . . . . . . . . 17 ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → ((𝑁 − (𝑁 mod (2↑𝑀))) − (𝑁 − (𝑁 mod (2↑(𝑀 + 1))))) = ((𝑁 mod (2↑(𝑀 + 1))) − (𝑁 mod (2↑𝑀))))
4948oveq1d 6892 . . . . . . . . . . . . . . . 16 ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → (((𝑁 − (𝑁 mod (2↑𝑀))) − (𝑁 − (𝑁 mod (2↑(𝑀 + 1))))) / (2↑𝑀)) = (((𝑁 mod (2↑(𝑀 + 1))) − (𝑁 mod (2↑𝑀))) / (2↑𝑀)))
5047, 11subcld 10680 . . . . . . . . . . . . . . . . 17 ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → (𝑁 − (𝑁 mod (2↑𝑀))) ∈ ℂ)
5147, 18subcld 10680 . . . . . . . . . . . . . . . . 17 ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → (𝑁 − (𝑁 mod (2↑(𝑀 + 1)))) ∈ ℂ)
529nncnd 11324 . . . . . . . . . . . . . . . . 17 ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → (2↑𝑀) ∈ ℂ)
5350, 51, 52, 31divsubdird 11128 . . . . . . . . . . . . . . . 16 ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → (((𝑁 − (𝑁 mod (2↑𝑀))) − (𝑁 − (𝑁 mod (2↑(𝑀 + 1))))) / (2↑𝑀)) = (((𝑁 − (𝑁 mod (2↑𝑀))) / (2↑𝑀)) − ((𝑁 − (𝑁 mod (2↑(𝑀 + 1)))) / (2↑𝑀))))
5449, 53eqtr3d 2849 . . . . . . . . . . . . . . 15 ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → (((𝑁 mod (2↑(𝑀 + 1))) − (𝑁 mod (2↑𝑀))) / (2↑𝑀)) = (((𝑁 − (𝑁 mod (2↑𝑀))) / (2↑𝑀)) − ((𝑁 − (𝑁 mod (2↑(𝑀 + 1)))) / (2↑𝑀))))
5527, 51mulcomd 10349 . . . . . . . . . . . . . . . . . . 19 ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → (2 · (𝑁 − (𝑁 mod (2↑(𝑀 + 1))))) = ((𝑁 − (𝑁 mod (2↑(𝑀 + 1)))) · 2))
5627, 52mulcomd 10349 . . . . . . . . . . . . . . . . . . . 20 ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → (2 · (2↑𝑀)) = ((2↑𝑀) · 2))
5727, 8expp1d 13235 . . . . . . . . . . . . . . . . . . . 20 ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → (2↑(𝑀 + 1)) = ((2↑𝑀) · 2))
5856, 57eqtr4d 2850 . . . . . . . . . . . . . . . . . . 19 ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → (2 · (2↑𝑀)) = (2↑(𝑀 + 1)))
5955, 58oveq12d 6895 . . . . . . . . . . . . . . . . . 18 ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → ((2 · (𝑁 − (𝑁 mod (2↑(𝑀 + 1))))) / (2 · (2↑𝑀))) = (((𝑁 − (𝑁 mod (2↑(𝑀 + 1)))) · 2) / (2↑(𝑀 + 1))))
6051, 52, 27, 31, 29divcan5d 11115 . . . . . . . . . . . . . . . . . 18 ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → ((2 · (𝑁 − (𝑁 mod (2↑(𝑀 + 1))))) / (2 · (2↑𝑀))) = ((𝑁 − (𝑁 mod (2↑(𝑀 + 1)))) / (2↑𝑀)))
6116nncnd 11324 . . . . . . . . . . . . . . . . . . 19 ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → (2↑(𝑀 + 1)) ∈ ℂ)
6230peano2zd 11754 . . . . . . . . . . . . . . . . . . . 20 ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → (𝑀 + 1) ∈ ℤ)
6327, 29, 62expne0d 13240 . . . . . . . . . . . . . . . . . . 19 ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → (2↑(𝑀 + 1)) ≠ 0)
6451, 27, 61, 63div23d 11126 . . . . . . . . . . . . . . . . . 18 ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → (((𝑁 − (𝑁 mod (2↑(𝑀 + 1)))) · 2) / (2↑(𝑀 + 1))) = (((𝑁 − (𝑁 mod (2↑(𝑀 + 1)))) / (2↑(𝑀 + 1))) · 2))
6559, 60, 643eqtr3d 2855 . . . . . . . . . . . . . . . . 17 ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → ((𝑁 − (𝑁 mod (2↑(𝑀 + 1)))) / (2↑𝑀)) = (((𝑁 − (𝑁 mod (2↑(𝑀 + 1)))) / (2↑(𝑀 + 1))) · 2))
6616nnrpd 12087 . . . . . . . . . . . . . . . . . . 19 ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → (2↑(𝑀 + 1)) ∈ ℝ+)
67 moddifz 12909 . . . . . . . . . . . . . . . . . . 19 ((𝑁 ∈ ℝ ∧ (2↑(𝑀 + 1)) ∈ ℝ+) → ((𝑁 − (𝑁 mod (2↑(𝑀 + 1)))) / (2↑(𝑀 + 1))) ∈ ℤ)
6839, 66, 67syl2anc 575 . . . . . . . . . . . . . . . . . 18 ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → ((𝑁 − (𝑁 mod (2↑(𝑀 + 1)))) / (2↑(𝑀 + 1))) ∈ ℤ)
6968, 44zmulcld 11757 . . . . . . . . . . . . . . . . 17 ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → (((𝑁 − (𝑁 mod (2↑(𝑀 + 1)))) / (2↑(𝑀 + 1))) · 2) ∈ ℤ)
7065, 69eqeltrd 2892 . . . . . . . . . . . . . . . 16 ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → ((𝑁 − (𝑁 mod (2↑(𝑀 + 1)))) / (2↑𝑀)) ∈ ℤ)
7146, 70zsubcld 11756 . . . . . . . . . . . . . . 15 ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → (((𝑁 − (𝑁 mod (2↑𝑀))) / (2↑𝑀)) − ((𝑁 − (𝑁 mod (2↑(𝑀 + 1)))) / (2↑𝑀))) ∈ ℤ)
7254, 71eqeltrd 2892 . . . . . . . . . . . . . 14 ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → (((𝑁 mod (2↑(𝑀 + 1))) − (𝑁 mod (2↑𝑀))) / (2↑𝑀)) ∈ ℤ)
73 dvdsmul2 15230 . . . . . . . . . . . . . . . 16 ((((𝑁 − (𝑁 mod (2↑(𝑀 + 1)))) / (2↑(𝑀 + 1))) ∈ ℤ ∧ 2 ∈ ℤ) → 2 ∥ (((𝑁 − (𝑁 mod (2↑(𝑀 + 1)))) / (2↑(𝑀 + 1))) · 2))
7468, 44, 73syl2anc 575 . . . . . . . . . . . . . . 15 ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → 2 ∥ (((𝑁 − (𝑁 mod (2↑(𝑀 + 1)))) / (2↑(𝑀 + 1))) · 2))
7547, 18, 11nnncan2d 10715 . . . . . . . . . . . . . . . . 17 ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → ((𝑁 − (𝑁 mod (2↑𝑀))) − ((𝑁 mod (2↑(𝑀 + 1))) − (𝑁 mod (2↑𝑀)))) = (𝑁 − (𝑁 mod (2↑(𝑀 + 1)))))
7675oveq1d 6892 . . . . . . . . . . . . . . . 16 ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → (((𝑁 − (𝑁 mod (2↑𝑀))) − ((𝑁 mod (2↑(𝑀 + 1))) − (𝑁 mod (2↑𝑀)))) / (2↑𝑀)) = ((𝑁 − (𝑁 mod (2↑(𝑀 + 1)))) / (2↑𝑀)))
7750, 21, 52, 31divsubdird 11128 . . . . . . . . . . . . . . . 16 ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → (((𝑁 − (𝑁 mod (2↑𝑀))) − ((𝑁 mod (2↑(𝑀 + 1))) − (𝑁 mod (2↑𝑀)))) / (2↑𝑀)) = (((𝑁 − (𝑁 mod (2↑𝑀))) / (2↑𝑀)) − (((𝑁 mod (2↑(𝑀 + 1))) − (𝑁 mod (2↑𝑀))) / (2↑𝑀))))
7876, 77, 653eqtr3d 2855 . . . . . . . . . . . . . . 15 ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → (((𝑁 − (𝑁 mod (2↑𝑀))) / (2↑𝑀)) − (((𝑁 mod (2↑(𝑀 + 1))) − (𝑁 mod (2↑𝑀))) / (2↑𝑀))) = (((𝑁 − (𝑁 mod (2↑(𝑀 + 1)))) / (2↑(𝑀 + 1))) · 2))
7974, 78breqtrrd 4879 . . . . . . . . . . . . . 14 ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → 2 ∥ (((𝑁 − (𝑁 mod (2↑𝑀))) / (2↑𝑀)) − (((𝑁 mod (2↑(𝑀 + 1))) − (𝑁 mod (2↑𝑀))) / (2↑𝑀))))
80 dvdssub2 15249 . . . . . . . . . . . . . 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↑𝑀))))
8144, 46, 72, 79, 80syl31anc 1485 . . . . . . . . . . . . 13 ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → (2 ∥ ((𝑁 − (𝑁 mod (2↑𝑀))) / (2↑𝑀)) ↔ 2 ∥ (((𝑁 mod (2↑(𝑀 + 1))) − (𝑁 mod (2↑𝑀))) / (2↑𝑀))))
8243, 81bitr3d 272 . . . . . . . . . . . 12 ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → (2 ∥ (⌊‘(𝑁 / (2↑𝑀))) ↔ 2 ∥ (((𝑁 mod (2↑(𝑀 + 1))) − (𝑁 mod (2↑𝑀))) / (2↑𝑀))))
8382notbid 309 . . . . . . . . . . 11 ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → (¬ 2 ∥ (⌊‘(𝑁 / (2↑𝑀))) ↔ ¬ 2 ∥ (((𝑁 mod (2↑(𝑀 + 1))) − (𝑁 mod (2↑𝑀))) / (2↑𝑀))))
8438, 83bitrd 270 . . . . . . . . . 10 ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → (𝑀 ∈ (bits‘𝑁) ↔ ¬ 2 ∥ (((𝑁 mod (2↑(𝑀 + 1))) − (𝑁 mod (2↑𝑀))) / (2↑𝑀))))
8584con2bid 345 . . . . . . . . 9 ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → (2 ∥ (((𝑁 mod (2↑(𝑀 + 1))) − (𝑁 mod (2↑𝑀))) / (2↑𝑀)) ↔ ¬ 𝑀 ∈ (bits‘𝑁)))
8637, 85syl5ib 235 . . . . . . . 8 ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → ((((𝑁 mod (2↑(𝑀 + 1))) − (𝑁 mod (2↑𝑀))) / (2↑𝑀)) = 0 → ¬ 𝑀 ∈ (bits‘𝑁)))
8786con2d 131 . . . . . . 7 ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → (𝑀 ∈ (bits‘𝑁) → ¬ (((𝑁 mod (2↑(𝑀 + 1))) − (𝑁 mod (2↑𝑀))) / (2↑𝑀)) = 0))
88 df-neg 10557 . . . . . . . . . . . . . . 15 -1 = (0 − 1)
8952mulm1d 10770 . . . . . . . . . . . . . . . . 17 ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → (-1 · (2↑𝑀)) = -(2↑𝑀))
909nnred 11323 . . . . . . . . . . . . . . . . . . 19 ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → (2↑𝑀) ∈ ℝ)
9190renegcld 10745 . . . . . . . . . . . . . . . . . 18 ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → -(2↑𝑀) ∈ ℝ)
9239, 40modcld 12901 . . . . . . . . . . . . . . . . . . 19 ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → (𝑁 mod (2↑𝑀)) ∈ ℝ)
9392renegcld 10745 . . . . . . . . . . . . . . . . . 18 ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → -(𝑁 mod (2↑𝑀)) ∈ ℝ)
9439, 66modcld 12901 . . . . . . . . . . . . . . . . . . 19 ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → (𝑁 mod (2↑(𝑀 + 1))) ∈ ℝ)
9594, 92resubcld 10746 . . . . . . . . . . . . . . . . . 18 ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → ((𝑁 mod (2↑(𝑀 + 1))) − (𝑁 mod (2↑𝑀))) ∈ ℝ)
96 modlt 12906 . . . . . . . . . . . . . . . . . . . 20 ((𝑁 ∈ ℝ ∧ (2↑𝑀) ∈ ℝ+) → (𝑁 mod (2↑𝑀)) < (2↑𝑀))
9739, 40, 96syl2anc 575 . . . . . . . . . . . . . . . . . . 19 ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → (𝑁 mod (2↑𝑀)) < (2↑𝑀))
9892, 90ltnegd 10893 . . . . . . . . . . . . . . . . . . 19 ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → ((𝑁 mod (2↑𝑀)) < (2↑𝑀) ↔ -(2↑𝑀) < -(𝑁 mod (2↑𝑀))))
9997, 98mpbid 223 . . . . . . . . . . . . . . . . . 18 ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → -(2↑𝑀) < -(𝑁 mod (2↑𝑀)))
100 df-neg 10557 . . . . . . . . . . . . . . . . . . 19 -(𝑁 mod (2↑𝑀)) = (0 − (𝑁 mod (2↑𝑀)))
101 0red 10331 . . . . . . . . . . . . . . . . . . . 20 ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → 0 ∈ ℝ)
102 modge0 12905 . . . . . . . . . . . . . . . . . . . . 21 ((𝑁 ∈ ℝ ∧ (2↑(𝑀 + 1)) ∈ ℝ+) → 0 ≤ (𝑁 mod (2↑(𝑀 + 1))))
10339, 66, 102syl2anc 575 . . . . . . . . . . . . . . . . . . . 20 ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → 0 ≤ (𝑁 mod (2↑(𝑀 + 1))))
104101, 94, 92, 103lesub1dd 10931 . . . . . . . . . . . . . . . . . . 19 ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → (0 − (𝑁 mod (2↑𝑀))) ≤ ((𝑁 mod (2↑(𝑀 + 1))) − (𝑁 mod (2↑𝑀))))
105100, 104syl5eqbr 4886 . . . . . . . . . . . . . . . . . 18 ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → -(𝑁 mod (2↑𝑀)) ≤ ((𝑁 mod (2↑(𝑀 + 1))) − (𝑁 mod (2↑𝑀))))
10691, 93, 95, 99, 105ltletrd 10485 . . . . . . . . . . . . . . . . 17 ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → -(2↑𝑀) < ((𝑁 mod (2↑(𝑀 + 1))) − (𝑁 mod (2↑𝑀))))
10789, 106eqbrtrd 4873 . . . . . . . . . . . . . . . 16 ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → (-1 · (2↑𝑀)) < ((𝑁 mod (2↑(𝑀 + 1))) − (𝑁 mod (2↑𝑀))))
108 1red 10329 . . . . . . . . . . . . . . . . . 18 ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → 1 ∈ ℝ)
109108renegcld 10745 . . . . . . . . . . . . . . . . 17 ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → -1 ∈ ℝ)
110109, 95, 40ltmuldivd 12136 . . . . . . . . . . . . . . . 16 ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → ((-1 · (2↑𝑀)) < ((𝑁 mod (2↑(𝑀 + 1))) − (𝑁 mod (2↑𝑀))) ↔ -1 < (((𝑁 mod (2↑(𝑀 + 1))) − (𝑁 mod (2↑𝑀))) / (2↑𝑀))))
111107, 110mpbid 223 . . . . . . . . . . . . . . 15 ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → -1 < (((𝑁 mod (2↑(𝑀 + 1))) − (𝑁 mod (2↑𝑀))) / (2↑𝑀)))
11288, 111syl5eqbrr 4887 . . . . . . . . . . . . . 14 ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → (0 − 1) < (((𝑁 mod (2↑(𝑀 + 1))) − (𝑁 mod (2↑𝑀))) / (2↑𝑀)))
113 0zd 11658 . . . . . . . . . . . . . . 15 ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → 0 ∈ ℤ)
114 zlem1lt 11698 . . . . . . . . . . . . . . 15 ((0 ∈ ℤ ∧ (((𝑁 mod (2↑(𝑀 + 1))) − (𝑁 mod (2↑𝑀))) / (2↑𝑀)) ∈ ℤ) → (0 ≤ (((𝑁 mod (2↑(𝑀 + 1))) − (𝑁 mod (2↑𝑀))) / (2↑𝑀)) ↔ (0 − 1) < (((𝑁 mod (2↑(𝑀 + 1))) − (𝑁 mod (2↑𝑀))) / (2↑𝑀))))
115113, 72, 114syl2anc 575 . . . . . . . . . . . . . 14 ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → (0 ≤ (((𝑁 mod (2↑(𝑀 + 1))) − (𝑁 mod (2↑𝑀))) / (2↑𝑀)) ↔ (0 − 1) < (((𝑁 mod (2↑(𝑀 + 1))) − (𝑁 mod (2↑𝑀))) / (2↑𝑀))))
116112, 115mpbird 248 . . . . . . . . . . . . 13 ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → 0 ≤ (((𝑁 mod (2↑(𝑀 + 1))) − (𝑁 mod (2↑𝑀))) / (2↑𝑀)))
117 elnn0z 11659 . . . . . . . . . . . . 13 ((((𝑁 mod (2↑(𝑀 + 1))) − (𝑁 mod (2↑𝑀))) / (2↑𝑀)) ∈ ℕ0 ↔ ((((𝑁 mod (2↑(𝑀 + 1))) − (𝑁 mod (2↑𝑀))) / (2↑𝑀)) ∈ ℤ ∧ 0 ≤ (((𝑁 mod (2↑(𝑀 + 1))) − (𝑁 mod (2↑𝑀))) / (2↑𝑀))))
11872, 116, 117sylanbrc 574 . . . . . . . . . . . 12 ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → (((𝑁 mod (2↑(𝑀 + 1))) − (𝑁 mod (2↑𝑀))) / (2↑𝑀)) ∈ ℕ0)
119 nn0uz 11943 . . . . . . . . . . . 12 0 = (ℤ‘0)
120118, 119syl6eleq 2902 . . . . . . . . . . 11 ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → (((𝑁 mod (2↑(𝑀 + 1))) − (𝑁 mod (2↑𝑀))) / (2↑𝑀)) ∈ (ℤ‘0))
12116nnred 11323 . . . . . . . . . . . . . 14 ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → (2↑(𝑀 + 1)) ∈ ℝ)
122 modge0 12905 . . . . . . . . . . . . . . . 16 ((𝑁 ∈ ℝ ∧ (2↑𝑀) ∈ ℝ+) → 0 ≤ (𝑁 mod (2↑𝑀)))
12339, 40, 122syl2anc 575 . . . . . . . . . . . . . . 15 ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → 0 ≤ (𝑁 mod (2↑𝑀)))
12494, 92subge02d 10907 . . . . . . . . . . . . . . 15 ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → (0 ≤ (𝑁 mod (2↑𝑀)) ↔ ((𝑁 mod (2↑(𝑀 + 1))) − (𝑁 mod (2↑𝑀))) ≤ (𝑁 mod (2↑(𝑀 + 1)))))
125123, 124mpbid 223 . . . . . . . . . . . . . 14 ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → ((𝑁 mod (2↑(𝑀 + 1))) − (𝑁 mod (2↑𝑀))) ≤ (𝑁 mod (2↑(𝑀 + 1))))
126 modlt 12906 . . . . . . . . . . . . . . 15 ((𝑁 ∈ ℝ ∧ (2↑(𝑀 + 1)) ∈ ℝ+) → (𝑁 mod (2↑(𝑀 + 1))) < (2↑(𝑀 + 1)))
12739, 66, 126syl2anc 575 . . . . . . . . . . . . . 14 ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → (𝑁 mod (2↑(𝑀 + 1))) < (2↑(𝑀 + 1)))
12895, 94, 121, 125, 127lelttrd 10483 . . . . . . . . . . . . 13 ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → ((𝑁 mod (2↑(𝑀 + 1))) − (𝑁 mod (2↑𝑀))) < (2↑(𝑀 + 1)))
129128, 57breqtrd 4877 . . . . . . . . . . . 12 ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → ((𝑁 mod (2↑(𝑀 + 1))) − (𝑁 mod (2↑𝑀))) < ((2↑𝑀) · 2))
1307nnred 11323 . . . . . . . . . . . . 13 ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → 2 ∈ ℝ)
13195, 130, 40ltdivmuld 12140 . . . . . . . . . . . 12 ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → ((((𝑁 mod (2↑(𝑀 + 1))) − (𝑁 mod (2↑𝑀))) / (2↑𝑀)) < 2 ↔ ((𝑁 mod (2↑(𝑀 + 1))) − (𝑁 mod (2↑𝑀))) < ((2↑𝑀) · 2)))
132129, 131mpbird 248 . . . . . . . . . . 11 ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → (((𝑁 mod (2↑(𝑀 + 1))) − (𝑁 mod (2↑𝑀))) / (2↑𝑀)) < 2)
133 elfzo2 12700 . . . . . . . . . . 11 ((((𝑁 mod (2↑(𝑀 + 1))) − (𝑁 mod (2↑𝑀))) / (2↑𝑀)) ∈ (0..^2) ↔ ((((𝑁 mod (2↑(𝑀 + 1))) − (𝑁 mod (2↑𝑀))) / (2↑𝑀)) ∈ (ℤ‘0) ∧ 2 ∈ ℤ ∧ (((𝑁 mod (2↑(𝑀 + 1))) − (𝑁 mod (2↑𝑀))) / (2↑𝑀)) < 2))
134120, 44, 132, 133syl3anbrc 1436 . . . . . . . . . 10 ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → (((𝑁 mod (2↑(𝑀 + 1))) − (𝑁 mod (2↑𝑀))) / (2↑𝑀)) ∈ (0..^2))
135 fzo0to2pr 12780 . . . . . . . . . 10 (0..^2) = {0, 1}
136134, 135syl6eleq 2902 . . . . . . . . 9 ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → (((𝑁 mod (2↑(𝑀 + 1))) − (𝑁 mod (2↑𝑀))) / (2↑𝑀)) ∈ {0, 1})
137 elpri 4399 . . . . . . . . 9 ((((𝑁 mod (2↑(𝑀 + 1))) − (𝑁 mod (2↑𝑀))) / (2↑𝑀)) ∈ {0, 1} → ((((𝑁 mod (2↑(𝑀 + 1))) − (𝑁 mod (2↑𝑀))) / (2↑𝑀)) = 0 ∨ (((𝑁 mod (2↑(𝑀 + 1))) − (𝑁 mod (2↑𝑀))) / (2↑𝑀)) = 1))
138136, 137syl 17 . . . . . . . 8 ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → ((((𝑁 mod (2↑(𝑀 + 1))) − (𝑁 mod (2↑𝑀))) / (2↑𝑀)) = 0 ∨ (((𝑁 mod (2↑(𝑀 + 1))) − (𝑁 mod (2↑𝑀))) / (2↑𝑀)) = 1))
139138ord 882 . . . . . . 7 ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → (¬ (((𝑁 mod (2↑(𝑀 + 1))) − (𝑁 mod (2↑𝑀))) / (2↑𝑀)) = 0 → (((𝑁 mod (2↑(𝑀 + 1))) − (𝑁 mod (2↑𝑀))) / (2↑𝑀)) = 1))
14087, 139syld 47 . . . . . 6 ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → (𝑀 ∈ (bits‘𝑁) → (((𝑁 mod (2↑(𝑀 + 1))) − (𝑁 mod (2↑𝑀))) / (2↑𝑀)) = 1))
141140imp 395 . . . . 5 (((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) ∧ 𝑀 ∈ (bits‘𝑁)) → (((𝑁 mod (2↑(𝑀 + 1))) − (𝑁 mod (2↑𝑀))) / (2↑𝑀)) = 1)
14222, 26, 32, 141diveq1d 11097 . . . 4 (((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) ∧ 𝑀 ∈ (bits‘𝑁)) → ((𝑁 mod (2↑(𝑀 + 1))) − (𝑁 mod (2↑𝑀))) = (2↑𝑀))
143142oveq2d 6893 . . 3 (((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) ∧ 𝑀 ∈ (bits‘𝑁)) → ((𝑁 mod (2↑𝑀)) + ((𝑁 mod (2↑(𝑀 + 1))) − (𝑁 mod (2↑𝑀)))) = ((𝑁 mod (2↑𝑀)) + (2↑𝑀)))
14420, 143eqtr3d 2849 . 2 (((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) ∧ 𝑀 ∈ (bits‘𝑁)) → (𝑁 mod (2↑(𝑀 + 1))) = ((𝑁 mod (2↑𝑀)) + (2↑𝑀)))
14518adantr 468 . . . 4 (((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) ∧ ¬ 𝑀 ∈ (bits‘𝑁)) → (𝑁 mod (2↑(𝑀 + 1))) ∈ ℂ)
14611adantr 468 . . . 4 (((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) ∧ ¬ 𝑀 ∈ (bits‘𝑁)) → (𝑁 mod (2↑𝑀)) ∈ ℂ)
14721adantr 468 . . . . 5 (((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) ∧ ¬ 𝑀 ∈ (bits‘𝑁)) → ((𝑁 mod (2↑(𝑀 + 1))) − (𝑁 mod (2↑𝑀))) ∈ ℂ)
14852adantr 468 . . . . 5 (((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) ∧ ¬ 𝑀 ∈ (bits‘𝑁)) → (2↑𝑀) ∈ ℂ)
14931adantr 468 . . . . 5 (((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) ∧ ¬ 𝑀 ∈ (bits‘𝑁)) → (2↑𝑀) ≠ 0)
150 n2dvds1 15327 . . . . . . . . . 10 ¬ 2 ∥ 1
151 breq2 4855 . . . . . . . . . 10 ((((𝑁 mod (2↑(𝑀 + 1))) − (𝑁 mod (2↑𝑀))) / (2↑𝑀)) = 1 → (2 ∥ (((𝑁 mod (2↑(𝑀 + 1))) − (𝑁 mod (2↑𝑀))) / (2↑𝑀)) ↔ 2 ∥ 1))
152150, 151mtbiri 318 . . . . . . . . 9 ((((𝑁 mod (2↑(𝑀 + 1))) − (𝑁 mod (2↑𝑀))) / (2↑𝑀)) = 1 → ¬ 2 ∥ (((𝑁 mod (2↑(𝑀 + 1))) − (𝑁 mod (2↑𝑀))) / (2↑𝑀)))
153139, 152syl6 35 . . . . . . . 8 ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → (¬ (((𝑁 mod (2↑(𝑀 + 1))) − (𝑁 mod (2↑𝑀))) / (2↑𝑀)) = 0 → ¬ 2 ∥ (((𝑁 mod (2↑(𝑀 + 1))) − (𝑁 mod (2↑𝑀))) / (2↑𝑀))))
154153, 84sylibrd 250 . . . . . . 7 ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → (¬ (((𝑁 mod (2↑(𝑀 + 1))) − (𝑁 mod (2↑𝑀))) / (2↑𝑀)) = 0 → 𝑀 ∈ (bits‘𝑁)))
155154con1d 141 . . . . . 6 ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → (¬ 𝑀 ∈ (bits‘𝑁) → (((𝑁 mod (2↑(𝑀 + 1))) − (𝑁 mod (2↑𝑀))) / (2↑𝑀)) = 0))
156155imp 395 . . . . 5 (((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) ∧ ¬ 𝑀 ∈ (bits‘𝑁)) → (((𝑁 mod (2↑(𝑀 + 1))) − (𝑁 mod (2↑𝑀))) / (2↑𝑀)) = 0)
157147, 148, 149, 156diveq0d 11096 . . . 4 (((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) ∧ ¬ 𝑀 ∈ (bits‘𝑁)) → ((𝑁 mod (2↑(𝑀 + 1))) − (𝑁 mod (2↑𝑀))) = 0)
158145, 146, 157subeq0d 10688 . . 3 (((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) ∧ ¬ 𝑀 ∈ (bits‘𝑁)) → (𝑁 mod (2↑(𝑀 + 1))) = (𝑁 mod (2↑𝑀)))
159146addid1d 10524 . . 3 (((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) ∧ ¬ 𝑀 ∈ (bits‘𝑁)) → ((𝑁 mod (2↑𝑀)) + 0) = (𝑁 mod (2↑𝑀)))
160158, 159eqtr4d 2850 . 2 (((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) ∧ ¬ 𝑀 ∈ (bits‘𝑁)) → (𝑁 mod (2↑(𝑀 + 1))) = ((𝑁 mod (2↑𝑀)) + 0))
1612, 4, 144, 160ifbothda 4323 1 ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → (𝑁 mod (2↑(𝑀 + 1))) = ((𝑁 mod (2↑𝑀)) + if(𝑀 ∈ (bits‘𝑁), (2↑𝑀), 0)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 197  wa 384  wo 865   = wceq 1637  wcel 2157  wne 2985  ifcif 4286  {cpr 4379   class class class wbr 4851  cfv 6104  (class class class)co 6877  cc 10222  cr 10223  0cc0 10224  1c1 10225   + caddc 10227   · cmul 10229   < clt 10362  cle 10363  cmin 10554  -cneg 10555   / cdiv 10972  cn 11308  2c2 11359  0cn0 11562  cz 11646  cuz 11907  +crp 12049  ..^cfzo 12692  cfl 12818   mod cmo 12895  cexp 13086  cdvds 15206  bitscbits 15363
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2069  ax-7 2105  ax-8 2159  ax-9 2166  ax-10 2186  ax-11 2202  ax-12 2215  ax-13 2422  ax-ext 2791  ax-sep 4982  ax-nul 4990  ax-pow 5042  ax-pr 5103  ax-un 7182  ax-cnex 10280  ax-resscn 10281  ax-1cn 10282  ax-icn 10283  ax-addcl 10284  ax-addrcl 10285  ax-mulcl 10286  ax-mulrcl 10287  ax-mulcom 10288  ax-addass 10289  ax-mulass 10290  ax-distr 10291  ax-i2m1 10292  ax-1ne0 10293  ax-1rid 10294  ax-rnegex 10295  ax-rrecex 10296  ax-cnre 10297  ax-pre-lttri 10298  ax-pre-lttrn 10299  ax-pre-ltadd 10300  ax-pre-mulgt0 10301  ax-pre-sup 10302
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3or 1101  df-3an 1102  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2062  df-mo 2635  df-eu 2638  df-clab 2800  df-cleq 2806  df-clel 2809  df-nfc 2944  df-ne 2986  df-nel 3089  df-ral 3108  df-rex 3109  df-reu 3110  df-rmo 3111  df-rab 3112  df-v 3400  df-sbc 3641  df-csb 3736  df-dif 3779  df-un 3781  df-in 3783  df-ss 3790  df-pss 3792  df-nul 4124  df-if 4287  df-pw 4360  df-sn 4378  df-pr 4380  df-tp 4382  df-op 4384  df-uni 4638  df-iun 4721  df-br 4852  df-opab 4914  df-mpt 4931  df-tr 4954  df-id 5226  df-eprel 5231  df-po 5239  df-so 5240  df-fr 5277  df-we 5279  df-xp 5324  df-rel 5325  df-cnv 5326  df-co 5327  df-dm 5328  df-rn 5329  df-res 5330  df-ima 5331  df-pred 5900  df-ord 5946  df-on 5947  df-lim 5948  df-suc 5949  df-iota 6067  df-fun 6106  df-fn 6107  df-f 6108  df-f1 6109  df-fo 6110  df-f1o 6111  df-fv 6112  df-riota 6838  df-ov 6880  df-oprab 6881  df-mpt2 6882  df-om 7299  df-1st 7401  df-2nd 7402  df-wrecs 7645  df-recs 7707  df-rdg 7745  df-er 7982  df-en 8196  df-dom 8197  df-sdom 8198  df-sup 8590  df-inf 8591  df-pnf 10364  df-mnf 10365  df-xr 10366  df-ltxr 10367  df-le 10368  df-sub 10556  df-neg 10557  df-div 10973  df-nn 11309  df-2 11367  df-n0 11563  df-z 11647  df-uz 11908  df-rp 12050  df-fz 12553  df-fzo 12693  df-fl 12820  df-mod 12896  df-seq 13028  df-exp 13087  df-dvds 15207  df-bits 15366
This theorem is referenced by:  bitsinv1  15386  smumullem  15436
  Copyright terms: Public domain W3C validator