bitsfzo

Description: The bits of a number are all at positions less than M iff the number is nonnegative and less than 2 ^ M . (Contributed by Mario Carneiro, 5-Sep-2016) (Proof shortened by AV, 1-Oct-2020)

		Ref	Expression
	Assertion	bitsfzo	$⊢ (N \in ℤ \land M \in ℕ_{0}) \to (N \in (0 ..^2^{M}) \leftrightarrow bits (N) \subseteq (0 ..^M))$

Proof

Step	Hyp	Ref	Expression
1		bitsval	$⊢ m \in bits (N) \leftrightarrow (N \in ℤ \land m \in ℕ_{0} \land \neg 2 ∥ ⌊\frac{N}{2^{m}}⌋)$
2		simp32	$⊢ ((N \in ℤ \land M \in ℕ_{0}) \land N \in (0 ..^2^{M}) \land (N \in ℤ \land m \in ℕ_{0} \land \neg 2 ∥ ⌊\frac{N}{2^{m}}⌋)) \to m \in ℕ_{0}$
3		nn0uz	$⊢ ℕ_{0} = ℤ_{\geq 0}$
4	2 3	eleqtrdi	$⊢ ((N \in ℤ \land M \in ℕ_{0}) \land N \in (0 ..^2^{M}) \land (N \in ℤ \land m \in ℕ_{0} \land \neg 2 ∥ ⌊\frac{N}{2^{m}}⌋)) \to m \in ℤ_{\geq 0}$
5		simp1r	$⊢ ((N \in ℤ \land M \in ℕ_{0}) \land N \in (0 ..^2^{M}) \land (N \in ℤ \land m \in ℕ_{0} \land \neg 2 ∥ ⌊\frac{N}{2^{m}}⌋)) \to M \in ℕ_{0}$
6	5	nn0zd	$⊢ ((N \in ℤ \land M \in ℕ_{0}) \land N \in (0 ..^2^{M}) \land (N \in ℤ \land m \in ℕ_{0} \land \neg 2 ∥ ⌊\frac{N}{2^{m}}⌋)) \to M \in ℤ$
7		2re	$⊢ 2 \in ℝ$
8	7	a1i	$⊢ ((N \in ℤ \land M \in ℕ_{0}) \land N \in (0 ..^2^{M}) \land (N \in ℤ \land m \in ℕ_{0} \land \neg 2 ∥ ⌊\frac{N}{2^{m}}⌋)) \to 2 \in ℝ$
9	8 2	reexpcld	$⊢ ((N \in ℤ \land M \in ℕ_{0}) \land N \in (0 ..^2^{M}) \land (N \in ℤ \land m \in ℕ_{0} \land \neg 2 ∥ ⌊\frac{N}{2^{m}}⌋)) \to 2^{m} \in ℝ$
10		simp1l	$⊢ ((N \in ℤ \land M \in ℕ_{0}) \land N \in (0 ..^2^{M}) \land (N \in ℤ \land m \in ℕ_{0} \land \neg 2 ∥ ⌊\frac{N}{2^{m}}⌋)) \to N \in ℤ$
11	10	zred	$⊢ ((N \in ℤ \land M \in ℕ_{0}) \land N \in (0 ..^2^{M}) \land (N \in ℤ \land m \in ℕ_{0} \land \neg 2 ∥ ⌊\frac{N}{2^{m}}⌋)) \to N \in ℝ$
12	8 5	reexpcld	$⊢ ((N \in ℤ \land M \in ℕ_{0}) \land N \in (0 ..^2^{M}) \land (N \in ℤ \land m \in ℕ_{0} \land \neg 2 ∥ ⌊\frac{N}{2^{m}}⌋)) \to 2^{M} \in ℝ$
13	9	recnd	$⊢ ((N \in ℤ \land M \in ℕ_{0}) \land N \in (0 ..^2^{M}) \land (N \in ℤ \land m \in ℕ_{0} \land \neg 2 ∥ ⌊\frac{N}{2^{m}}⌋)) \to 2^{m} \in ℂ$
14	13	mullidd	$⊢ ((N \in ℤ \land M \in ℕ_{0}) \land N \in (0 ..^2^{M}) \land (N \in ℤ \land m \in ℕ_{0} \land \neg 2 ∥ ⌊\frac{N}{2^{m}}⌋)) \to 1 2^{m} = 2^{m}$
15		simp33	$⊢ ((N \in ℤ \land M \in ℕ_{0}) \land N \in (0 ..^2^{M}) \land (N \in ℤ \land m \in ℕ_{0} \land \neg 2 ∥ ⌊\frac{N}{2^{m}}⌋)) \to \neg 2 ∥ ⌊\frac{N}{2^{m}}⌋$
16		2rp	$⊢ 2 \in ℝ^{+}$
17	16	a1i	$⊢ ((N \in ℤ \land M \in ℕ_{0}) \land N \in (0 ..^2^{M}) \land (N \in ℤ \land m \in ℕ_{0} \land \neg 2 ∥ ⌊\frac{N}{2^{m}}⌋)) \to 2 \in ℝ^{+}$
18	2	nn0zd	$⊢ ((N \in ℤ \land M \in ℕ_{0}) \land N \in (0 ..^2^{M}) \land (N \in ℤ \land m \in ℕ_{0} \land \neg 2 ∥ ⌊\frac{N}{2^{m}}⌋)) \to m \in ℤ$
19	17 18	rpexpcld	$⊢ ((N \in ℤ \land M \in ℕ_{0}) \land N \in (0 ..^2^{M}) \land (N \in ℤ \land m \in ℕ_{0} \land \neg 2 ∥ ⌊\frac{N}{2^{m}}⌋)) \to 2^{m} \in ℝ^{+}$
20	11 19	rerpdivcld	$⊢ ((N \in ℤ \land M \in ℕ_{0}) \land N \in (0 ..^2^{M}) \land (N \in ℤ \land m \in ℕ_{0} \land \neg 2 ∥ ⌊\frac{N}{2^{m}}⌋)) \to \frac{N}{2^{m}} \in ℝ$
21		1red	$⊢ ((N \in ℤ \land M \in ℕ_{0}) \land N \in (0 ..^2^{M}) \land (N \in ℤ \land m \in ℕ_{0} \land \neg 2 ∥ ⌊\frac{N}{2^{m}}⌋)) \to 1 \in ℝ$
22	20 21	ltnled	$⊢ ((N \in ℤ \land M \in ℕ_{0}) \land N \in (0 ..^2^{M}) \land (N \in ℤ \land m \in ℕ_{0} \land \neg 2 ∥ ⌊\frac{N}{2^{m}}⌋)) \to (\frac{N}{2^{m}} < 1 \leftrightarrow \neg 1 \leq \frac{N}{2^{m}})$
23		0p1e1	$⊢ 0 + 1 = 1$
24	23	breq2i	$⊢ \frac{N}{2^{m}} < 0 + 1 \leftrightarrow \frac{N}{2^{m}} < 1$
25		elfzole1	$⊢ N \in (0 ..^2^{M}) \to 0 \leq N$
26	25	3ad2ant2	$⊢ ((N \in ℤ \land M \in ℕ_{0}) \land N \in (0 ..^2^{M}) \land (N \in ℤ \land m \in ℕ_{0} \land \neg 2 ∥ ⌊\frac{N}{2^{m}}⌋)) \to 0 \leq N$
27	11 19 26	divge0d	$⊢ ((N \in ℤ \land M \in ℕ_{0}) \land N \in (0 ..^2^{M}) \land (N \in ℤ \land m \in ℕ_{0} \land \neg 2 ∥ ⌊\frac{N}{2^{m}}⌋)) \to 0 \leq \frac{N}{2^{m}}$
28		0z	$⊢ 0 \in ℤ$
29		flbi	$⊢ (\frac{N}{2^{m}} \in ℝ \land 0 \in ℤ) \to (⌊\frac{N}{2^{m}}⌋ = 0 \leftrightarrow (0 \leq \frac{N}{2^{m}} \land \frac{N}{2^{m}} < 0 + 1))$
30	20 28 29	sylancl	$⊢ ((N \in ℤ \land M \in ℕ_{0}) \land N \in (0 ..^2^{M}) \land (N \in ℤ \land m \in ℕ_{0} \land \neg 2 ∥ ⌊\frac{N}{2^{m}}⌋)) \to (⌊\frac{N}{2^{m}}⌋ = 0 \leftrightarrow (0 \leq \frac{N}{2^{m}} \land \frac{N}{2^{m}} < 0 + 1))$
31		z0even	$⊢ 2 ∥ 0$
32		id	$⊢ ⌊\frac{N}{2^{m}}⌋ = 0 \to ⌊\frac{N}{2^{m}}⌋ = 0$
33	31 32	breqtrrid	$⊢ ⌊\frac{N}{2^{m}}⌋ = 0 \to 2 ∥ ⌊\frac{N}{2^{m}}⌋$
34	30 33	biimtrrdi	$⊢ ((N \in ℤ \land M \in ℕ_{0}) \land N \in (0 ..^2^{M}) \land (N \in ℤ \land m \in ℕ_{0} \land \neg 2 ∥ ⌊\frac{N}{2^{m}}⌋)) \to ((0 \leq \frac{N}{2^{m}} \land \frac{N}{2^{m}} < 0 + 1) \to 2 ∥ ⌊\frac{N}{2^{m}}⌋)$
35	27 34	mpand	$⊢ ((N \in ℤ \land M \in ℕ_{0}) \land N \in (0 ..^2^{M}) \land (N \in ℤ \land m \in ℕ_{0} \land \neg 2 ∥ ⌊\frac{N}{2^{m}}⌋)) \to (\frac{N}{2^{m}} < 0 + 1 \to 2 ∥ ⌊\frac{N}{2^{m}}⌋)$
36	24 35	biimtrrid	$⊢ ((N \in ℤ \land M \in ℕ_{0}) \land N \in (0 ..^2^{M}) \land (N \in ℤ \land m \in ℕ_{0} \land \neg 2 ∥ ⌊\frac{N}{2^{m}}⌋)) \to (\frac{N}{2^{m}} < 1 \to 2 ∥ ⌊\frac{N}{2^{m}}⌋)$
37	22 36	sylbird	$⊢ ((N \in ℤ \land M \in ℕ_{0}) \land N \in (0 ..^2^{M}) \land (N \in ℤ \land m \in ℕ_{0} \land \neg 2 ∥ ⌊\frac{N}{2^{m}}⌋)) \to (\neg 1 \leq \frac{N}{2^{m}} \to 2 ∥ ⌊\frac{N}{2^{m}}⌋)$
38	15 37	mt3d	$⊢ ((N \in ℤ \land M \in ℕ_{0}) \land N \in (0 ..^2^{M}) \land (N \in ℤ \land m \in ℕ_{0} \land \neg 2 ∥ ⌊\frac{N}{2^{m}}⌋)) \to 1 \leq \frac{N}{2^{m}}$
39	21 11 19	lemuldivd	$⊢ ((N \in ℤ \land M \in ℕ_{0}) \land N \in (0 ..^2^{M}) \land (N \in ℤ \land m \in ℕ_{0} \land \neg 2 ∥ ⌊\frac{N}{2^{m}}⌋)) \to (1 2^{m} \leq N \leftrightarrow 1 \leq \frac{N}{2^{m}})$
40	38 39	mpbird	$⊢ ((N \in ℤ \land M \in ℕ_{0}) \land N \in (0 ..^2^{M}) \land (N \in ℤ \land m \in ℕ_{0} \land \neg 2 ∥ ⌊\frac{N}{2^{m}}⌋)) \to 1 2^{m} \leq N$
41	14 40	eqbrtrrd	$⊢ ((N \in ℤ \land M \in ℕ_{0}) \land N \in (0 ..^2^{M}) \land (N \in ℤ \land m \in ℕ_{0} \land \neg 2 ∥ ⌊\frac{N}{2^{m}}⌋)) \to 2^{m} \leq N$
42		elfzolt2	$⊢ N \in (0 ..^2^{M}) \to N < 2^{M}$
43	42	3ad2ant2	$⊢ ((N \in ℤ \land M \in ℕ_{0}) \land N \in (0 ..^2^{M}) \land (N \in ℤ \land m \in ℕ_{0} \land \neg 2 ∥ ⌊\frac{N}{2^{m}}⌋)) \to N < 2^{M}$
44	9 11 12 41 43	lelttrd	$⊢ ((N \in ℤ \land M \in ℕ_{0}) \land N \in (0 ..^2^{M}) \land (N \in ℤ \land m \in ℕ_{0} \land \neg 2 ∥ ⌊\frac{N}{2^{m}}⌋)) \to 2^{m} < 2^{M}$
45		1lt2	$⊢ 1 < 2$
46	45	a1i	$⊢ ((N \in ℤ \land M \in ℕ_{0}) \land N \in (0 ..^2^{M}) \land (N \in ℤ \land m \in ℕ_{0} \land \neg 2 ∥ ⌊\frac{N}{2^{m}}⌋)) \to 1 < 2$
47	8 18 6 46	ltexp2d	$⊢ ((N \in ℤ \land M \in ℕ_{0}) \land N \in (0 ..^2^{M}) \land (N \in ℤ \land m \in ℕ_{0} \land \neg 2 ∥ ⌊\frac{N}{2^{m}}⌋)) \to (m < M \leftrightarrow 2^{m} < 2^{M})$
48	44 47	mpbird	$⊢ ((N \in ℤ \land M \in ℕ_{0}) \land N \in (0 ..^2^{M}) \land (N \in ℤ \land m \in ℕ_{0} \land \neg 2 ∥ ⌊\frac{N}{2^{m}}⌋)) \to m < M$
49		elfzo2	$⊢ m \in (0 ..^M) \leftrightarrow (m \in ℤ_{\geq 0} \land M \in ℤ \land m < M)$
50	4 6 48 49	syl3anbrc	$⊢ ((N \in ℤ \land M \in ℕ_{0}) \land N \in (0 ..^2^{M}) \land (N \in ℤ \land m \in ℕ_{0} \land \neg 2 ∥ ⌊\frac{N}{2^{m}}⌋)) \to m \in (0 ..^M)$
51	50	3expia	$⊢ ((N \in ℤ \land M \in ℕ_{0}) \land N \in (0 ..^2^{M})) \to ((N \in ℤ \land m \in ℕ_{0} \land \neg 2 ∥ ⌊\frac{N}{2^{m}}⌋) \to m \in (0 ..^M))$
52	1 51	biimtrid	$⊢ ((N \in ℤ \land M \in ℕ_{0}) \land N \in (0 ..^2^{M})) \to (m \in bits (N) \to m \in (0 ..^M))$
53	52	ssrdv	$⊢ ((N \in ℤ \land M \in ℕ_{0}) \land N \in (0 ..^2^{M})) \to bits (N) \subseteq (0 ..^M)$
54		simpr	$⊢ (((N \in ℤ \land M \in ℕ_{0}) \land bits (N) \subseteq (0 ..^M)) \land - N \in ℕ) \to - N \in ℕ$
55	54	nnred	$⊢ (((N \in ℤ \land M \in ℕ_{0}) \land bits (N) \subseteq (0 ..^M)) \land - N \in ℕ) \to - N \in ℝ$
56		simpllr	$⊢ (((N \in ℤ \land M \in ℕ_{0}) \land bits (N) \subseteq (0 ..^M)) \land - N \in ℕ) \to M \in ℕ_{0}$
57	56	nn0red	$⊢ (((N \in ℤ \land M \in ℕ_{0}) \land bits (N) \subseteq (0 ..^M)) \land - N \in ℕ) \to M \in ℝ$
58		max2	$⊢ (- N \in ℝ \land M \in ℝ) \to M \leq if (- N \leq M, M, - N)$
59	55 57 58	syl2anc	$⊢ (((N \in ℤ \land M \in ℕ_{0}) \land bits (N) \subseteq (0 ..^M)) \land - N \in ℕ) \to M \leq if (- N \leq M, M, - N)$
60		simplr	$⊢ (((N \in ℤ \land M \in ℕ_{0}) \land bits (N) \subseteq (0 ..^M)) \land - N \in ℕ) \to bits (N) \subseteq (0 ..^M)$
61		n2dvdsm1	$⊢ \neg 2 ∥ -1$
62		simplll	$⊢ (((N \in ℤ \land M \in ℕ_{0}) \land bits (N) \subseteq (0 ..^M)) \land - N \in ℕ) \to N \in ℤ$
63	62	zred	$⊢ (((N \in ℤ \land M \in ℕ_{0}) \land bits (N) \subseteq (0 ..^M)) \land - N \in ℕ) \to N \in ℝ$
64		2nn	$⊢ 2 \in ℕ$
65	64	a1i	$⊢ (((N \in ℤ \land M \in ℕ_{0}) \land bits (N) \subseteq (0 ..^M)) \land - N \in ℕ) \to 2 \in ℕ$
66	54	nnnn0d	$⊢ (((N \in ℤ \land M \in ℕ_{0}) \land bits (N) \subseteq (0 ..^M)) \land - N \in ℕ) \to - N \in ℕ_{0}$
67	56 66	ifcld	$⊢ (((N \in ℤ \land M \in ℕ_{0}) \land bits (N) \subseteq (0 ..^M)) \land - N \in ℕ) \to if (- N \leq M, M, - N) \in ℕ_{0}$
68	65 67	nnexpcld	$⊢ (((N \in ℤ \land M \in ℕ_{0}) \land bits (N) \subseteq (0 ..^M)) \land - N \in ℕ) \to 2^{if (- N \leq M, M, - N)} \in ℕ$
69	63 68	nndivred	$⊢ (((N \in ℤ \land M \in ℕ_{0}) \land bits (N) \subseteq (0 ..^M)) \land - N \in ℕ) \to \frac{N}{2^{if (- N \leq M, M, - N)}} \in ℝ$
70		1red	$⊢ (((N \in ℤ \land M \in ℕ_{0}) \land bits (N) \subseteq (0 ..^M)) \land - N \in ℕ) \to 1 \in ℝ$
71	62	zcnd	$⊢ (((N \in ℤ \land M \in ℕ_{0}) \land bits (N) \subseteq (0 ..^M)) \land - N \in ℕ) \to N \in ℂ$
72	68	nncnd	$⊢ (((N \in ℤ \land M \in ℕ_{0}) \land bits (N) \subseteq (0 ..^M)) \land - N \in ℕ) \to 2^{if (- N \leq M, M, - N)} \in ℂ$
73		2cnd	$⊢ (((N \in ℤ \land M \in ℕ_{0}) \land bits (N) \subseteq (0 ..^M)) \land - N \in ℕ) \to 2 \in ℂ$
74		2ne0	$⊢ 2 \neq 0$
75	74	a1i	$⊢ (((N \in ℤ \land M \in ℕ_{0}) \land bits (N) \subseteq (0 ..^M)) \land - N \in ℕ) \to 2 \neq 0$
76	67	nn0zd	$⊢ (((N \in ℤ \land M \in ℕ_{0}) \land bits (N) \subseteq (0 ..^M)) \land - N \in ℕ) \to if (- N \leq M, M, - N) \in ℤ$
77	73 75 76	expne0d	$⊢ (((N \in ℤ \land M \in ℕ_{0}) \land bits (N) \subseteq (0 ..^M)) \land - N \in ℕ) \to 2^{if (- N \leq M, M, - N)} \neq 0$
78	71 72 77	divnegd	$⊢ (((N \in ℤ \land M \in ℕ_{0}) \land bits (N) \subseteq (0 ..^M)) \land - N \in ℕ) \to - \frac{N}{2^{if (- N \leq M, M, - N)}} = \frac{- N}{2^{if (- N \leq M, M, - N)}}$
79	67	nn0red	$⊢ (((N \in ℤ \land M \in ℕ_{0}) \land bits (N) \subseteq (0 ..^M)) \land - N \in ℕ) \to if (- N \leq M, M, - N) \in ℝ$
80	68	nnred	$⊢ (((N \in ℤ \land M \in ℕ_{0}) \land bits (N) \subseteq (0 ..^M)) \land - N \in ℕ) \to 2^{if (- N \leq M, M, - N)} \in ℝ$
81		max1	$⊢ (- N \in ℝ \land M \in ℝ) \to - N \leq if (- N \leq M, M, - N)$
82	55 57 81	syl2anc	$⊢ (((N \in ℤ \land M \in ℕ_{0}) \land bits (N) \subseteq (0 ..^M)) \land - N \in ℕ) \to - N \leq if (- N \leq M, M, - N)$
83		2z	$⊢ 2 \in ℤ$
84		uzid	$⊢ 2 \in ℤ \to 2 \in ℤ_{\geq 2}$
85	83 84	ax-mp	$⊢ 2 \in ℤ_{\geq 2}$
86		bernneq3	$⊢ (2 \in ℤ_{\geq 2} \land if (- N \leq M, M, - N) \in ℕ_{0}) \to if (- N \leq M, M, - N) < 2^{if (- N \leq M, M, - N)}$
87	85 67 86	sylancr	$⊢ (((N \in ℤ \land M \in ℕ_{0}) \land bits (N) \subseteq (0 ..^M)) \land - N \in ℕ) \to if (- N \leq M, M, - N) < 2^{if (- N \leq M, M, - N)}$
88	79 80 87	ltled	$⊢ (((N \in ℤ \land M \in ℕ_{0}) \land bits (N) \subseteq (0 ..^M)) \land - N \in ℕ) \to if (- N \leq M, M, - N) \leq 2^{if (- N \leq M, M, - N)}$
89	55 79 80 82 88	letrd	$⊢ (((N \in ℤ \land M \in ℕ_{0}) \land bits (N) \subseteq (0 ..^M)) \land - N \in ℕ) \to - N \leq 2^{if (- N \leq M, M, - N)}$
90	72	mulridd	$⊢ (((N \in ℤ \land M \in ℕ_{0}) \land bits (N) \subseteq (0 ..^M)) \land - N \in ℕ) \to 2^{if (- N \leq M, M, - N)} \cdot 1 = 2^{if (- N \leq M, M, - N)}$
91	89 90	breqtrrd	$⊢ (((N \in ℤ \land M \in ℕ_{0}) \land bits (N) \subseteq (0 ..^M)) \land - N \in ℕ) \to - N \leq 2^{if (- N \leq M, M, - N)} \cdot 1$
92	68	nnrpd	$⊢ (((N \in ℤ \land M \in ℕ_{0}) \land bits (N) \subseteq (0 ..^M)) \land - N \in ℕ) \to 2^{if (- N \leq M, M, - N)} \in ℝ^{+}$
93	55 70 92	ledivmuld	$⊢ (((N \in ℤ \land M \in ℕ_{0}) \land bits (N) \subseteq (0 ..^M)) \land - N \in ℕ) \to (\frac{- N}{2^{if (- N \leq M, M, - N)}} \leq 1 \leftrightarrow - N \leq 2^{if (- N \leq M, M, - N)} \cdot 1)$
94	91 93	mpbird	$⊢ (((N \in ℤ \land M \in ℕ_{0}) \land bits (N) \subseteq (0 ..^M)) \land - N \in ℕ) \to \frac{- N}{2^{if (- N \leq M, M, - N)}} \leq 1$
95	78 94	eqbrtrd	$⊢ (((N \in ℤ \land M \in ℕ_{0}) \land bits (N) \subseteq (0 ..^M)) \land - N \in ℕ) \to - \frac{N}{2^{if (- N \leq M, M, - N)}} \leq 1$
96	69 70 95	lenegcon1d	$⊢ (((N \in ℤ \land M \in ℕ_{0}) \land bits (N) \subseteq (0 ..^M)) \land - N \in ℕ) \to - 1 \leq \frac{N}{2^{if (- N \leq M, M, - N)}}$
97	54	nngt0d	$⊢ (((N \in ℤ \land M \in ℕ_{0}) \land bits (N) \subseteq (0 ..^M)) \land - N \in ℕ) \to 0 < - N$
98	68	nngt0d	$⊢ (((N \in ℤ \land M \in ℕ_{0}) \land bits (N) \subseteq (0 ..^M)) \land - N \in ℕ) \to 0 < 2^{if (- N \leq M, M, - N)}$
99	55 80 97 98	divgt0d	$⊢ (((N \in ℤ \land M \in ℕ_{0}) \land bits (N) \subseteq (0 ..^M)) \land - N \in ℕ) \to 0 < \frac{- N}{2^{if (- N \leq M, M, - N)}}$
100	99 78	breqtrrd	$⊢ (((N \in ℤ \land M \in ℕ_{0}) \land bits (N) \subseteq (0 ..^M)) \land - N \in ℕ) \to 0 < - \frac{N}{2^{if (- N \leq M, M, - N)}}$
101	69	lt0neg1d	$⊢ (((N \in ℤ \land M \in ℕ_{0}) \land bits (N) \subseteq (0 ..^M)) \land - N \in ℕ) \to (\frac{N}{2^{if (- N \leq M, M, - N)}} < 0 \leftrightarrow 0 < - \frac{N}{2^{if (- N \leq M, M, - N)}})$
102	100 101	mpbird	$⊢ (((N \in ℤ \land M \in ℕ_{0}) \land bits (N) \subseteq (0 ..^M)) \land - N \in ℕ) \to \frac{N}{2^{if (- N \leq M, M, - N)}} < 0$
103		ax-1cn	$⊢ 1 \in ℂ$
104		neg1cn	$⊢ - 1 \in ℂ$
105		1pneg1e0	$⊢ 1 + -1 = 0$
106	103 104 105	addcomli	$⊢ - 1 + 1 = 0$
107	102 106	breqtrrdi	$⊢ (((N \in ℤ \land M \in ℕ_{0}) \land bits (N) \subseteq (0 ..^M)) \land - N \in ℕ) \to \frac{N}{2^{if (- N \leq M, M, - N)}} < - 1 + 1$
108		neg1z	$⊢ - 1 \in ℤ$
109		flbi	$⊢ (\frac{N}{2^{if (- N \leq M, M, - N)}} \in ℝ \land - 1 \in ℤ) \to (⌊\frac{N}{2^{if (- N \leq M, M, - N)}}⌋ = - 1 \leftrightarrow (- 1 \leq \frac{N}{2^{if (- N \leq M, M, - N)}} \land \frac{N}{2^{if (- N \leq M, M, - N)}} < - 1 + 1))$
110	69 108 109	sylancl	$⊢ (((N \in ℤ \land M \in ℕ_{0}) \land bits (N) \subseteq (0 ..^M)) \land - N \in ℕ) \to (⌊\frac{N}{2^{if (- N \leq M, M, - N)}}⌋ = - 1 \leftrightarrow (- 1 \leq \frac{N}{2^{if (- N \leq M, M, - N)}} \land \frac{N}{2^{if (- N \leq M, M, - N)}} < - 1 + 1))$
111	96 107 110	mpbir2and	$⊢ (((N \in ℤ \land M \in ℕ_{0}) \land bits (N) \subseteq (0 ..^M)) \land - N \in ℕ) \to ⌊\frac{N}{2^{if (- N \leq M, M, - N)}}⌋ = - 1$
112	111	breq2d	$⊢ (((N \in ℤ \land M \in ℕ_{0}) \land bits (N) \subseteq (0 ..^M)) \land - N \in ℕ) \to (2 ∥ ⌊\frac{N}{2^{if (- N \leq M, M, - N)}}⌋ \leftrightarrow 2 ∥ -1)$
113	61 112	mtbiri	$⊢ (((N \in ℤ \land M \in ℕ_{0}) \land bits (N) \subseteq (0 ..^M)) \land - N \in ℕ) \to \neg 2 ∥ ⌊\frac{N}{2^{if (- N \leq M, M, - N)}}⌋$
114		bitsval2	$⊢ (N \in ℤ \land if (- N \leq M, M, - N) \in ℕ_{0}) \to (if (- N \leq M, M, - N) \in bits (N) \leftrightarrow \neg 2 ∥ ⌊\frac{N}{2^{if (- N \leq M, M, - N)}}⌋)$
115	62 67 114	syl2anc	$⊢ (((N \in ℤ \land M \in ℕ_{0}) \land bits (N) \subseteq (0 ..^M)) \land - N \in ℕ) \to (if (- N \leq M, M, - N) \in bits (N) \leftrightarrow \neg 2 ∥ ⌊\frac{N}{2^{if (- N \leq M, M, - N)}}⌋)$
116	113 115	mpbird	$⊢ (((N \in ℤ \land M \in ℕ_{0}) \land bits (N) \subseteq (0 ..^M)) \land - N \in ℕ) \to if (- N \leq M, M, - N) \in bits (N)$
117	60 116	sseldd	$⊢ (((N \in ℤ \land M \in ℕ_{0}) \land bits (N) \subseteq (0 ..^M)) \land - N \in ℕ) \to if (- N \leq M, M, - N) \in (0 ..^M)$
118		elfzolt2	$⊢ if (- N \leq M, M, - N) \in (0 ..^M) \to if (- N \leq M, M, - N) < M$
119	117 118	syl	$⊢ (((N \in ℤ \land M \in ℕ_{0}) \land bits (N) \subseteq (0 ..^M)) \land - N \in ℕ) \to if (- N \leq M, M, - N) < M$
120	79 57	ltnled	$⊢ (((N \in ℤ \land M \in ℕ_{0}) \land bits (N) \subseteq (0 ..^M)) \land - N \in ℕ) \to (if (- N \leq M, M, - N) < M \leftrightarrow \neg M \leq if (- N \leq M, M, - N))$
121	119 120	mpbid	$⊢ (((N \in ℤ \land M \in ℕ_{0}) \land bits (N) \subseteq (0 ..^M)) \land - N \in ℕ) \to \neg M \leq if (- N \leq M, M, - N)$
122	59 121	pm2.65da	$⊢ ((N \in ℤ \land M \in ℕ_{0}) \land bits (N) \subseteq (0 ..^M)) \to \neg - N \in ℕ$
123	122	intnand	$⊢ ((N \in ℤ \land M \in ℕ_{0}) \land bits (N) \subseteq (0 ..^M)) \to \neg (N \in ℝ \land - N \in ℕ)$
124		simpll	$⊢ ((N \in ℤ \land M \in ℕ_{0}) \land bits (N) \subseteq (0 ..^M)) \to N \in ℤ$
125		elznn0nn	$⊢ N \in ℤ \leftrightarrow (N \in ℕ_{0} \lor (N \in ℝ \land - N \in ℕ))$
126	124 125	sylib	$⊢ ((N \in ℤ \land M \in ℕ_{0}) \land bits (N) \subseteq (0 ..^M)) \to (N \in ℕ_{0} \lor (N \in ℝ \land - N \in ℕ))$
127	126	ord	$⊢ ((N \in ℤ \land M \in ℕ_{0}) \land bits (N) \subseteq (0 ..^M)) \to (\neg N \in ℕ_{0} \to (N \in ℝ \land - N \in ℕ))$
128	123 127	mt3d	$⊢ ((N \in ℤ \land M \in ℕ_{0}) \land bits (N) \subseteq (0 ..^M)) \to N \in ℕ_{0}$
129		simplr	$⊢ ((N \in ℤ \land M \in ℕ_{0}) \land bits (N) \subseteq (0 ..^M)) \to M \in ℕ_{0}$
130		simpr	$⊢ ((N \in ℤ \land M \in ℕ_{0}) \land bits (N) \subseteq (0 ..^M)) \to bits (N) \subseteq (0 ..^M)$
131		eqid	$⊢ inf (\{n \in ℕ_{0} \| N < 2^{n}\} ℝ <) = inf (\{n \in ℕ_{0} \| N < 2^{n}\} ℝ <)$
132	128 129 130 131	bitsfzolem	$⊢ ((N \in ℤ \land M \in ℕ_{0}) \land bits (N) \subseteq (0 ..^M)) \to N \in (0 ..^2^{M})$
133	53 132	impbida	$⊢ (N \in ℤ \land M \in ℕ_{0}) \to (N \in (0 ..^2^{M}) \leftrightarrow bits (N) \subseteq (0 ..^M))$

Metamath Proof Explorer

Theorem bitsfzo

Proof