Theorem fldivexpfllog2

Description: The floor of a positive real number divided by 2 to the power of the floor of the logarithm to base 2 of the number is 1. (Contributed by AV, 26-May-2020)

	Ref	Expression
Assertion	fldivexpfllog2	$$⊢X\in {ℝ}^{+}\to ⌊\frac{X}{2^{⌊{\log }_{2}X⌋}}⌋=1$$

Proof

Step	Hyp	Ref	Expression
1		2z	$$⊢2\in \mathbb{Z}$$
2		uzid	$$⊢2\in \mathbb{Z}\to 2\in {\mathbb{Z}}_{\ge 2}$$
3	1 2	mp1i	$$⊢X\in {ℝ}^{+}\to 2\in {\mathbb{Z}}_{\ge 2}$$
4		id	$$⊢X\in {ℝ}^{+}\to X\in {ℝ}^{+}$$
5		eqid	$$⊢⌊{\log }_{2}X⌋=⌊{\log }_{2}X⌋$$
6	3 4 5	fllogbd	$$⊢X\in {ℝ}^{+}\to \left(2^{⌊{\log }_{2}X⌋}\le X\wedge X<2^{⌊{\log }_{2}X⌋+1}\right)$$
7		2re	$$⊢2\in ℝ$$
8	7	a1i	$$⊢X\in {ℝ}^{+}\to 2\in ℝ$$
9		2ne0	$$⊢2\ne 0$$
10	9	a1i	$$⊢X\in {ℝ}^{+}\to 2\ne 0$$
11		relogbzcl	$$⊢\left(2\in {\mathbb{Z}}_{\ge 2}\wedge X\in {ℝ}^{+}\right)\to {\log }_{2}X\in ℝ$$
12	3 4 11	syl2anc	$$⊢X\in {ℝ}^{+}\to {\log }_{2}X\in ℝ$$
13	12	flcld	$$⊢X\in {ℝ}^{+}\to ⌊{\log }_{2}X⌋\in \mathbb{Z}$$
14	8 10 13	reexpclzd	$$⊢X\in {ℝ}^{+}\to 2^{⌊{\log }_{2}X⌋}\in ℝ$$
15		2pos	$$⊢0<2$$
16	15	a1i	$$⊢X\in {ℝ}^{+}\to 0<2$$
17		expgt0	$$⊢\left(2\in ℝ\wedge ⌊{\log }_{2}X⌋\in \mathbb{Z}\wedge 0<2\right)\to 0<2^{⌊{\log }_{2}X⌋}$$
18	8 13 16 17	syl3anc	$$⊢X\in {ℝ}^{+}\to 0<2^{⌊{\log }_{2}X⌋}$$
19	14 18	elrpd	$$⊢X\in {ℝ}^{+}\to 2^{⌊{\log }_{2}X⌋}\in {ℝ}^{+}$$
20		rpre	$$⊢X\in {ℝ}^{+}\to X\in ℝ$$
21		divge1b	$$⊢\left(2^{⌊{\log }_{2}X⌋}\in {ℝ}^{+}\wedge X\in ℝ\right)\to \left(2^{⌊{\log }_{2}X⌋}\le X\leftrightarrow 1\le \frac{X}{2^{⌊{\log }_{2}X⌋}}\right)$$
22	21	bicomd	$$⊢\left(2^{⌊{\log }_{2}X⌋}\in {ℝ}^{+}\wedge X\in ℝ\right)\to \left(1\le \frac{X}{2^{⌊{\log }_{2}X⌋}}\leftrightarrow 2^{⌊{\log }_{2}X⌋}\le X\right)$$
23	19 20 22	syl2anc	$$⊢X\in {ℝ}^{+}\to \left(1\le \frac{X}{2^{⌊{\log }_{2}X⌋}}\leftrightarrow 2^{⌊{\log }_{2}X⌋}\le X\right)$$
24	23	biimprd	$$⊢X\in {ℝ}^{+}\to \left(2^{⌊{\log }_{2}X⌋}\le X\to 1\le \frac{X}{2^{⌊{\log }_{2}X⌋}}\right)$$
25		2cnd	$$⊢X\in {ℝ}^{+}\to 2\in ℂ$$
26	25 10 13	expp1zd	$$⊢X\in {ℝ}^{+}\to 2^{⌊{\log }_{2}X⌋+1}=2^{⌊{\log }_{2}X⌋}\cdot 2$$
27	26	breq2d	$$⊢X\in {ℝ}^{+}\to \left(X<2^{⌊{\log }_{2}X⌋+1}\leftrightarrow X<2^{⌊{\log }_{2}X⌋}\cdot 2\right)$$
28		ltdivmul	$$⊢\left(X\in ℝ\wedge 2\in ℝ\wedge \left(2^{⌊{\log }_{2}X⌋}\in ℝ\wedge 0<2^{⌊{\log }_{2}X⌋}\right)\right)\to \left(\frac{X}{2^{⌊{\log }_{2}X⌋}}<2\leftrightarrow X<2^{⌊{\log }_{2}X⌋}\cdot 2\right)$$
29	20 8 14 18 28	syl112anc	$$⊢X\in {ℝ}^{+}\to \left(\frac{X}{2^{⌊{\log }_{2}X⌋}}<2\leftrightarrow X<2^{⌊{\log }_{2}X⌋}\cdot 2\right)$$
30	27 29	bitr4d	$$⊢X\in {ℝ}^{+}\to \left(X<2^{⌊{\log }_{2}X⌋+1}\leftrightarrow \frac{X}{2^{⌊{\log }_{2}X⌋}}<2\right)$$
31	30	biimpd	$$⊢X\in {ℝ}^{+}\to \left(X<2^{⌊{\log }_{2}X⌋+1}\to \frac{X}{2^{⌊{\log }_{2}X⌋}}<2\right)$$
32		1p1e2	$$⊢1+1=2$$
33	32	breq2i	$$⊢\frac{X}{2^{⌊{\log }_{2}X⌋}}<1+1\leftrightarrow \frac{X}{2^{⌊{\log }_{2}X⌋}}<2$$
34	31 33	imbitrrdi	$$⊢X\in {ℝ}^{+}\to \left(X<2^{⌊{\log }_{2}X⌋+1}\to \frac{X}{2^{⌊{\log }_{2}X⌋}}<1+1\right)$$
35	24 34	anim12d	$$⊢X\in {ℝ}^{+}\to \left(\left(2^{⌊{\log }_{2}X⌋}\le X\wedge X<2^{⌊{\log }_{2}X⌋+1}\right)\to \left(1\le \frac{X}{2^{⌊{\log }_{2}X⌋}}\wedge \frac{X}{2^{⌊{\log }_{2}X⌋}}<1+1\right)\right)$$
36	6 35	mpd	$$⊢X\in {ℝ}^{+}\to \left(1\le \frac{X}{2^{⌊{\log }_{2}X⌋}}\wedge \frac{X}{2^{⌊{\log }_{2}X⌋}}<1+1\right)$$
37	25 10 13	expne0d	$$⊢X\in {ℝ}^{+}\to 2^{⌊{\log }_{2}X⌋}\ne 0$$
38	20 14 37	redivcld	$$⊢X\in {ℝ}^{+}\to \frac{X}{2^{⌊{\log }_{2}X⌋}}\in ℝ$$
39		1zzd	$$⊢X\in {ℝ}^{+}\to 1\in \mathbb{Z}$$
40		flbi	$$⊢\left(\frac{X}{2^{⌊{\log }_{2}X⌋}}\in ℝ\wedge 1\in \mathbb{Z}\right)\to \left(⌊\frac{X}{2^{⌊{\log }_{2}X⌋}}⌋=1\leftrightarrow \left(1\le \frac{X}{2^{⌊{\log }_{2}X⌋}}\wedge \frac{X}{2^{⌊{\log }_{2}X⌋}}<1+1\right)\right)$$
41	38 39 40	syl2anc	$$⊢X\in {ℝ}^{+}\to \left(⌊\frac{X}{2^{⌊{\log }_{2}X⌋}}⌋=1\leftrightarrow \left(1\le \frac{X}{2^{⌊{\log }_{2}X⌋}}\wedge \frac{X}{2^{⌊{\log }_{2}X⌋}}<1+1\right)\right)$$
42	36 41	mpbird	$$⊢X\in {ℝ}^{+}\to ⌊\frac{X}{2^{⌊{\log }_{2}X⌋}}⌋=1$$