Theorem bitsfzolem

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

	Ref	Expression
Hypotheses	bitsfzo.1	$$⊢\phi \to N\in {\mathbb{N}}_0$$
	bitsfzo.2	$$⊢\phi \to M\in {\mathbb{N}}_0$$
	bitsfzo.3	$$⊢\phi \to \mathrm{bits}\left(N\right)\subseteq \left(0..^M\right)$$
	bitsfzo.4	$$⊢S=sup\left(\left\{n\in {\mathbb{N}}_0|N<2^n\right\},ℝ,<\right)$$
Assertion	bitsfzolem	$$⊢\phi \to N\in \left(0..^2^M\right)$$

Proof

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