bitsfzolem

Description: Lemma for bitsfzo . (Contributed by Mario Carneiro, 5-Sep-2016) (Revised by AV, 1-Oct-2020)

	Ref	Expression
Hypotheses	bitsfzo.1	$⊢ φ \to N \in ℕ_{0}$
	bitsfzo.2	$⊢ φ \to M \in ℕ_{0}$
	bitsfzo.3	$⊢ φ \to bits (N) \subseteq (0 ..^M)$
	bitsfzo.4	$⊢ S = sup (\{n \in ℕ_{0} \| N < 2^{n}\} ℝ <)$
Assertion	bitsfzolem	$⊢ φ \to N \in (0 ..^2^{M})$

Proof

Step	Hyp	Ref	Expression
1		bitsfzo.1	$⊢ φ \to N \in ℕ_{0}$
2		bitsfzo.2	$⊢ φ \to M \in ℕ_{0}$
3		bitsfzo.3	$⊢ φ \to bits (N) \subseteq (0 ..^M)$
4		bitsfzo.4	$⊢ S = sup (\{n \in ℕ_{0} \| N < 2^{n}\} ℝ <)$
5		nn0uz	$⊢ ℕ_{0} = ℤ_{\geq 0}$
6	1 5	eleqtrdi	$⊢ φ \to N \in ℤ_{\geq 0}$
7		2nn	$⊢ 2 \in ℕ$
8	7	a1i	$⊢ φ \to 2 \in ℕ$
9	8 2	nnexpcld	$⊢ φ \to 2^{M} \in ℕ$
10	9	nnzd	$⊢ φ \to 2^{M} \in ℤ$
11	3	adantr	$⊢ (φ \land 2^{M} \leq N) \to bits (N) \subseteq (0 ..^M)$
12		n2dvds1	$⊢ \neg 2 ∥ 1$
13	7	a1i	$⊢ (φ \land 2^{M} \leq N) \to 2 \in ℕ$
14		ssrab2	$⊢ \{n \in ℕ_{0} \| N < 2^{n}\} \subseteq ℕ_{0}$
15	14 5	sseqtri	$⊢ \{n \in ℕ_{0} \| N < 2^{n}\} \subseteq ℤ_{\geq 0}$
16		nnssnn0	$⊢ ℕ \subseteq ℕ_{0}$
17	1	nn0red	$⊢ φ \to N \in ℝ$
18		2re	$⊢ 2 \in ℝ$
19	18	a1i	$⊢ φ \to 2 \in ℝ$
20		1lt2	$⊢ 1 < 2$
21	20	a1i	$⊢ φ \to 1 < 2$
22		expnbnd	$⊢ (N \in ℝ \land 2 \in ℝ \land 1 < 2) \to \exists n \in ℕ N < 2^{n}$
23	17 19 21 22	syl3anc	$⊢ φ \to \exists n \in ℕ N < 2^{n}$
24		ssrexv	$⊢ ℕ \subseteq ℕ_{0} \to (\exists n \in ℕ N < 2^{n} \to \exists n \in ℕ_{0} N < 2^{n})$
25	16 23 24	mpsyl	$⊢ φ \to \exists n \in ℕ_{0} N < 2^{n}$
26		rabn0	$⊢ \{n \in ℕ_{0} \| N < 2^{n}\} \neq \emptyset \leftrightarrow \exists n \in ℕ_{0} N < 2^{n}$
27	25 26	sylibr	$⊢ φ \to \{n \in ℕ_{0} \| N < 2^{n}\} \neq \emptyset$
28		infssuzcl	$⊢ (\{n \in ℕ_{0} \| N < 2^{n}\} \subseteq ℤ_{\geq 0} \land \{n \in ℕ_{0} \| N < 2^{n}\} \neq \emptyset) \to sup (\{n \in ℕ_{0} \| N < 2^{n}\} ℝ <) \in \{n \in ℕ_{0} \| N < 2^{n}\}$
29	15 27 28	sylancr	$⊢ φ \to sup (\{n \in ℕ_{0} \| N < 2^{n}\} ℝ <) \in \{n \in ℕ_{0} \| N < 2^{n}\}$
30	4 29	eqeltrid	$⊢ φ \to S \in \{n \in ℕ_{0} \| N < 2^{n}\}$
31	14 30	sselid	$⊢ φ \to S \in ℕ_{0}$
32	31	nn0zd	$⊢ φ \to S \in ℤ$
33	32	adantr	$⊢ (φ \land 2^{M} \leq N) \to S \in ℤ$
34		0red	$⊢ (φ \land 2^{M} \leq N) \to 0 \in ℝ$
35	2	nn0zd	$⊢ φ \to M \in ℤ$
36	35	adantr	$⊢ (φ \land 2^{M} \leq N) \to M \in ℤ$
37	36	zred	$⊢ (φ \land 2^{M} \leq N) \to M \in ℝ$
38	33	zred	$⊢ (φ \land 2^{M} \leq N) \to S \in ℝ$
39	2	adantr	$⊢ (φ \land 2^{M} \leq N) \to M \in ℕ_{0}$
40	39	nn0ge0d	$⊢ (φ \land 2^{M} \leq N) \to 0 \leq M$
41	18	a1i	$⊢ (φ \land 2^{M} \leq N) \to 2 \in ℝ$
42	41 39	reexpcld	$⊢ (φ \land 2^{M} \leq N) \to 2^{M} \in ℝ$
43	17	adantr	$⊢ (φ \land 2^{M} \leq N) \to N \in ℝ$
44	8 31	nnexpcld	$⊢ φ \to 2^{S} \in ℕ$
45	44	adantr	$⊢ (φ \land 2^{M} \leq N) \to 2^{S} \in ℕ$
46	45	nnred	$⊢ (φ \land 2^{M} \leq N) \to 2^{S} \in ℝ$
47		simpr	$⊢ (φ \land 2^{M} \leq N) \to 2^{M} \leq N$
48	30	adantr	$⊢ (φ \land 2^{M} \leq N) \to S \in \{n \in ℕ_{0} \| N < 2^{n}\}$
49		oveq2	$⊢ m = S \to 2^{m} = 2^{S}$
50	49	breq2d	$⊢ m = S \to (N < 2^{m} \leftrightarrow N < 2^{S})$
51		oveq2	$⊢ n = m \to 2^{n} = 2^{m}$
52	51	breq2d	$⊢ n = m \to (N < 2^{n} \leftrightarrow N < 2^{m})$
53	52	cbvrabv	$⊢ \{n \in ℕ_{0} \| N < 2^{n}\} = \{m \in ℕ_{0} \| N < 2^{m}\}$
54	50 53	elrab2	$⊢ S \in \{n \in ℕ_{0} \| N < 2^{n}\} \leftrightarrow (S \in ℕ_{0} \land N < 2^{S})$
55	54	simprbi	$⊢ S \in \{n \in ℕ_{0} \| N < 2^{n}\} \to N < 2^{S}$
56	48 55	syl	$⊢ (φ \land 2^{M} \leq N) \to N < 2^{S}$
57	42 43 46 47 56	lelttrd	$⊢ (φ \land 2^{M} \leq N) \to 2^{M} < 2^{S}$
58	20	a1i	$⊢ (φ \land 2^{M} \leq N) \to 1 < 2$
59	41 36 33 58	ltexp2d	$⊢ (φ \land 2^{M} \leq N) \to (M < S \leftrightarrow 2^{M} < 2^{S})$
60	57 59	mpbird	$⊢ (φ \land 2^{M} \leq N) \to M < S$
61	34 37 38 40 60	lelttrd	$⊢ (φ \land 2^{M} \leq N) \to 0 < S$
62		elnnz	$⊢ S \in ℕ \leftrightarrow (S \in ℤ \land 0 < S)$
63	33 61 62	sylanbrc	$⊢ (φ \land 2^{M} \leq N) \to S \in ℕ$
64		nnm1nn0	$⊢ S \in ℕ \to S - 1 \in ℕ_{0}$
65	63 64	syl	$⊢ (φ \land 2^{M} \leq N) \to S - 1 \in ℕ_{0}$
66	13 65	nnexpcld	$⊢ (φ \land 2^{M} \leq N) \to 2^{S - 1} \in ℕ$
67	66	nncnd	$⊢ (φ \land 2^{M} \leq N) \to 2^{S - 1} \in ℂ$
68	67	mulid2d	$⊢ (φ \land 2^{M} \leq N) \to 1 2^{S - 1} = 2^{S - 1}$
69	66	nnred	$⊢ (φ \land 2^{M} \leq N) \to 2^{S - 1} \in ℝ$
70	38	ltm1d	$⊢ (φ \land 2^{M} \leq N) \to S - 1 < S$
71	65	nn0red	$⊢ (φ \land 2^{M} \leq N) \to S - 1 \in ℝ$
72	71 38	ltnled	$⊢ (φ \land 2^{M} \leq N) \to (S - 1 < S \leftrightarrow \neg S \leq S - 1)$
73	70 72	mpbid	$⊢ (φ \land 2^{M} \leq N) \to \neg S \leq S - 1$
74		oveq2	$⊢ m = S - 1 \to 2^{m} = 2^{S - 1}$
75	74	breq2d	$⊢ m = S - 1 \to (N < 2^{m} \leftrightarrow N < 2^{S - 1})$
76	75 53	elrab2	$⊢ S - 1 \in \{n \in ℕ_{0} \| N < 2^{n}\} \leftrightarrow (S - 1 \in ℕ_{0} \land N < 2^{S - 1})$
77		infssuzle	$⊢ (\{n \in ℕ_{0} \| N < 2^{n}\} \subseteq ℤ_{\geq 0} \land S - 1 \in \{n \in ℕ_{0} \| N < 2^{n}\}) \to sup (\{n \in ℕ_{0} \| N < 2^{n}\} ℝ <) \leq S - 1$
78	15 77	mpan	$⊢ S - 1 \in \{n \in ℕ_{0} \| N < 2^{n}\} \to sup (\{n \in ℕ_{0} \| N < 2^{n}\} ℝ <) \leq S - 1$
79	4 78	eqbrtrid	$⊢ S - 1 \in \{n \in ℕ_{0} \| N < 2^{n}\} \to S \leq S - 1$
80	79	a1i	$⊢ (φ \land 2^{M} \leq N) \to (S - 1 \in \{n \in ℕ_{0} \| N < 2^{n}\} \to S \leq S - 1)$
81	76 80	syl5bir	$⊢ (φ \land 2^{M} \leq N) \to ((S - 1 \in ℕ_{0} \land N < 2^{S - 1}) \to S \leq S - 1)$
82	65 81	mpand	$⊢ (φ \land 2^{M} \leq N) \to (N < 2^{S - 1} \to S \leq S - 1)$
83	73 82	mtod	$⊢ (φ \land 2^{M} \leq N) \to \neg N < 2^{S - 1}$
84	69 43 83	nltled	$⊢ (φ \land 2^{M} \leq N) \to 2^{S - 1} \leq N$
85	68 84	eqbrtrd	$⊢ (φ \land 2^{M} \leq N) \to 1 2^{S - 1} \leq N$
86		1red	$⊢ (φ \land 2^{M} \leq N) \to 1 \in ℝ$
87		2rp	$⊢ 2 \in ℝ^{+}$
88	87	a1i	$⊢ (φ \land 2^{M} \leq N) \to 2 \in ℝ^{+}$
89		1z	$⊢ 1 \in ℤ$
90	89	a1i	$⊢ (φ \land 2^{M} \leq N) \to 1 \in ℤ$
91	33 90	zsubcld	$⊢ (φ \land 2^{M} \leq N) \to S - 1 \in ℤ$
92	88 91	rpexpcld	$⊢ (φ \land 2^{M} \leq N) \to 2^{S - 1} \in ℝ^{+}$
93	86 43 92	lemuldivd	$⊢ (φ \land 2^{M} \leq N) \to (1 2^{S - 1} \leq N \leftrightarrow 1 \leq \frac{N}{2^{S - 1}})$
94	85 93	mpbid	$⊢ (φ \land 2^{M} \leq N) \to 1 \leq \frac{N}{2^{S - 1}}$
95		2cn	$⊢ 2 \in ℂ$
96		expm1t	$⊢ (2 \in ℂ \land S \in ℕ) \to 2^{S} = 2^{S - 1} \cdot 2$
97	95 63 96	sylancr	$⊢ (φ \land 2^{M} \leq N) \to 2^{S} = 2^{S - 1} \cdot 2$
98	56 97	breqtrd	$⊢ (φ \land 2^{M} \leq N) \to N < 2^{S - 1} \cdot 2$
99	43 41 92	ltdivmuld	$⊢ (φ \land 2^{M} \leq N) \to (\frac{N}{2^{S - 1}} < 2 \leftrightarrow N < 2^{S - 1} \cdot 2)$
100	98 99	mpbird	$⊢ (φ \land 2^{M} \leq N) \to \frac{N}{2^{S - 1}} < 2$
101		df-2	$⊢ 2 = 1 + 1$
102	100 101	breqtrdi	$⊢ (φ \land 2^{M} \leq N) \to \frac{N}{2^{S - 1}} < 1 + 1$
103	43 92	rerpdivcld	$⊢ (φ \land 2^{M} \leq N) \to \frac{N}{2^{S - 1}} \in ℝ$
104		flbi	$⊢ (\frac{N}{2^{S - 1}} \in ℝ \land 1 \in ℤ) \to (⌊\frac{N}{2^{S - 1}}⌋ = 1 \leftrightarrow (1 \leq \frac{N}{2^{S - 1}} \land \frac{N}{2^{S - 1}} < 1 + 1))$
105	103 89 104	sylancl	$⊢ (φ \land 2^{M} \leq N) \to (⌊\frac{N}{2^{S - 1}}⌋ = 1 \leftrightarrow (1 \leq \frac{N}{2^{S - 1}} \land \frac{N}{2^{S - 1}} < 1 + 1))$
106	94 102 105	mpbir2and	$⊢ (φ \land 2^{M} \leq N) \to ⌊\frac{N}{2^{S - 1}}⌋ = 1$
107	106	breq2d	$⊢ (φ \land 2^{M} \leq N) \to (2 ∥ ⌊\frac{N}{2^{S - 1}}⌋ \leftrightarrow 2 ∥ 1)$
108	12 107	mtbiri	$⊢ (φ \land 2^{M} \leq N) \to \neg 2 ∥ ⌊\frac{N}{2^{S - 1}}⌋$
109	1	nn0zd	$⊢ φ \to N \in ℤ$
110		bitsval2	$⊢ (N \in ℤ \land S - 1 \in ℕ_{0}) \to (S - 1 \in bits (N) \leftrightarrow \neg 2 ∥ ⌊\frac{N}{2^{S - 1}}⌋)$
111	109 65 110	syl2an2r	$⊢ (φ \land 2^{M} \leq N) \to (S - 1 \in bits (N) \leftrightarrow \neg 2 ∥ ⌊\frac{N}{2^{S - 1}}⌋)$
112	108 111	mpbird	$⊢ (φ \land 2^{M} \leq N) \to S - 1 \in bits (N)$
113	11 112	sseldd	$⊢ (φ \land 2^{M} \leq N) \to S - 1 \in (0 ..^M)$
114		elfzolt2	$⊢ S - 1 \in (0 ..^M) \to S - 1 < M$
115	113 114	syl	$⊢ (φ \land 2^{M} \leq N) \to S - 1 < M$
116		zlem1lt	$⊢ (S \in ℤ \land M \in ℤ) \to (S \leq M \leftrightarrow S - 1 < M)$
117	32 36 116	syl2an2r	$⊢ (φ \land 2^{M} \leq N) \to (S \leq M \leftrightarrow S - 1 < M)$
118	115 117	mpbird	$⊢ (φ \land 2^{M} \leq N) \to S \leq M$
119	37 38	ltnled	$⊢ (φ \land 2^{M} \leq N) \to (M < S \leftrightarrow \neg S \leq M)$
120	60 119	mpbid	$⊢ (φ \land 2^{M} \leq N) \to \neg S \leq M$
121	118 120	pm2.65da	$⊢ φ \to \neg 2^{M} \leq N$
122	9	nnred	$⊢ φ \to 2^{M} \in ℝ$
123	17 122	ltnled	$⊢ φ \to (N < 2^{M} \leftrightarrow \neg 2^{M} \leq N)$
124	121 123	mpbird	$⊢ φ \to N < 2^{M}$
125		elfzo2	$⊢ N \in (0 ..^2^{M}) \leftrightarrow (N \in ℤ_{\geq 0} \land 2^{M} \in ℤ \land N < 2^{M})$
126	6 10 124 125	syl3anbrc	$⊢ φ \to N \in (0 ..^2^{M})$

Metamath Proof Explorer

Theorem bitsfzolem

Proof