bitsinv1lem

		Ref	Expression
	Assertion	bitsinv1lem	$⊢ (N \in ℤ \land M \in ℕ_{0}) \to N \mod 2^{M + 1} = (N \mod 2^{M}) + if (M \in bits (N), 2^{M}, 0)$

Proof

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

Metamath Proof Explorer

Theorem bitsinv1lem

Proof