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	⊢ ( 𝑋 ∈ ℝ+ → ( ⌊ ‘ ( 𝑋 / ( 2 ↑ ( ⌊ ‘ ( 2 logb 𝑋 ) ) ) ) ) = 1 )

Proof

Step	Hyp	Ref	Expression
1		2z	⊢ 2 ∈ ℤ
2		uzid	⊢ ( 2 ∈ ℤ → 2 ∈ ( ℤ≥ ‘ 2 ) )
3	1 2	mp1i	⊢ ( 𝑋 ∈ ℝ+ → 2 ∈ ( ℤ≥ ‘ 2 ) )
4		id	⊢ ( 𝑋 ∈ ℝ+ → 𝑋 ∈ ℝ+ )
5		eqid	⊢ ( ⌊ ‘ ( 2 logb 𝑋 ) ) = ( ⌊ ‘ ( 2 logb 𝑋 ) )
6	3 4 5	fllogbd	⊢ ( 𝑋 ∈ ℝ+ → ( ( 2 ↑ ( ⌊ ‘ ( 2 logb 𝑋 ) ) ) ≤ 𝑋 ∧ 𝑋 < ( 2 ↑ ( ( ⌊ ‘ ( 2 logb 𝑋 ) ) + 1 ) ) ) )
7		2re	⊢ 2 ∈ ℝ
8	7	a1i	⊢ ( 𝑋 ∈ ℝ+ → 2 ∈ ℝ )
9		2ne0	⊢ 2 ≠ 0
10	9	a1i	⊢ ( 𝑋 ∈ ℝ+ → 2 ≠ 0 )
11		relogbzcl	⊢ ( ( 2 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑋 ∈ ℝ+ ) → ( 2 logb 𝑋 ) ∈ ℝ )
12	3 4 11	syl2anc	⊢ ( 𝑋 ∈ ℝ+ → ( 2 logb 𝑋 ) ∈ ℝ )
13	12	flcld	⊢ ( 𝑋 ∈ ℝ+ → ( ⌊ ‘ ( 2 logb 𝑋 ) ) ∈ ℤ )
14	8 10 13	reexpclzd	⊢ ( 𝑋 ∈ ℝ+ → ( 2 ↑ ( ⌊ ‘ ( 2 logb 𝑋 ) ) ) ∈ ℝ )
15		2pos	⊢ 0 < 2
16	15	a1i	⊢ ( 𝑋 ∈ ℝ+ → 0 < 2 )
17		expgt0	⊢ ( ( 2 ∈ ℝ ∧ ( ⌊ ‘ ( 2 logb 𝑋 ) ) ∈ ℤ ∧ 0 < 2 ) → 0 < ( 2 ↑ ( ⌊ ‘ ( 2 logb 𝑋 ) ) ) )
18	8 13 16 17	syl3anc	⊢ ( 𝑋 ∈ ℝ+ → 0 < ( 2 ↑ ( ⌊ ‘ ( 2 logb 𝑋 ) ) ) )
19	14 18	elrpd	⊢ ( 𝑋 ∈ ℝ+ → ( 2 ↑ ( ⌊ ‘ ( 2 logb 𝑋 ) ) ) ∈ ℝ+ )
20		rpre	⊢ ( 𝑋 ∈ ℝ+ → 𝑋 ∈ ℝ )
21		divge1b	⊢ ( ( ( 2 ↑ ( ⌊ ‘ ( 2 logb 𝑋 ) ) ) ∈ ℝ+ ∧ 𝑋 ∈ ℝ ) → ( ( 2 ↑ ( ⌊ ‘ ( 2 logb 𝑋 ) ) ) ≤ 𝑋 ↔ 1 ≤ ( 𝑋 / ( 2 ↑ ( ⌊ ‘ ( 2 logb 𝑋 ) ) ) ) ) )
22	21	bicomd	⊢ ( ( ( 2 ↑ ( ⌊ ‘ ( 2 logb 𝑋 ) ) ) ∈ ℝ+ ∧ 𝑋 ∈ ℝ ) → ( 1 ≤ ( 𝑋 / ( 2 ↑ ( ⌊ ‘ ( 2 logb 𝑋 ) ) ) ) ↔ ( 2 ↑ ( ⌊ ‘ ( 2 logb 𝑋 ) ) ) ≤ 𝑋 ) )
23	19 20 22	syl2anc	⊢ ( 𝑋 ∈ ℝ+ → ( 1 ≤ ( 𝑋 / ( 2 ↑ ( ⌊ ‘ ( 2 logb 𝑋 ) ) ) ) ↔ ( 2 ↑ ( ⌊ ‘ ( 2 logb 𝑋 ) ) ) ≤ 𝑋 ) )
24	23	biimprd	⊢ ( 𝑋 ∈ ℝ+ → ( ( 2 ↑ ( ⌊ ‘ ( 2 logb 𝑋 ) ) ) ≤ 𝑋 → 1 ≤ ( 𝑋 / ( 2 ↑ ( ⌊ ‘ ( 2 logb 𝑋 ) ) ) ) ) )
25		2cnd	⊢ ( 𝑋 ∈ ℝ+ → 2 ∈ ℂ )
26	25 10 13	expp1zd	⊢ ( 𝑋 ∈ ℝ+ → ( 2 ↑ ( ( ⌊ ‘ ( 2 logb 𝑋 ) ) + 1 ) ) = ( ( 2 ↑ ( ⌊ ‘ ( 2 logb 𝑋 ) ) ) · 2 ) )
27	26	breq2d	⊢ ( 𝑋 ∈ ℝ+ → ( 𝑋 < ( 2 ↑ ( ( ⌊ ‘ ( 2 logb 𝑋 ) ) + 1 ) ) ↔ 𝑋 < ( ( 2 ↑ ( ⌊ ‘ ( 2 logb 𝑋 ) ) ) · 2 ) ) )
28		ltdivmul	⊢ ( ( 𝑋 ∈ ℝ ∧ 2 ∈ ℝ ∧ ( ( 2 ↑ ( ⌊ ‘ ( 2 logb 𝑋 ) ) ) ∈ ℝ ∧ 0 < ( 2 ↑ ( ⌊ ‘ ( 2 logb 𝑋 ) ) ) ) ) → ( ( 𝑋 / ( 2 ↑ ( ⌊ ‘ ( 2 logb 𝑋 ) ) ) ) < 2 ↔ 𝑋 < ( ( 2 ↑ ( ⌊ ‘ ( 2 logb 𝑋 ) ) ) · 2 ) ) )
29	20 8 14 18 28	syl112anc	⊢ ( 𝑋 ∈ ℝ+ → ( ( 𝑋 / ( 2 ↑ ( ⌊ ‘ ( 2 logb 𝑋 ) ) ) ) < 2 ↔ 𝑋 < ( ( 2 ↑ ( ⌊ ‘ ( 2 logb 𝑋 ) ) ) · 2 ) ) )
30	27 29	bitr4d	⊢ ( 𝑋 ∈ ℝ+ → ( 𝑋 < ( 2 ↑ ( ( ⌊ ‘ ( 2 logb 𝑋 ) ) + 1 ) ) ↔ ( 𝑋 / ( 2 ↑ ( ⌊ ‘ ( 2 logb 𝑋 ) ) ) ) < 2 ) )
31	30	biimpd	⊢ ( 𝑋 ∈ ℝ+ → ( 𝑋 < ( 2 ↑ ( ( ⌊ ‘ ( 2 logb 𝑋 ) ) + 1 ) ) → ( 𝑋 / ( 2 ↑ ( ⌊ ‘ ( 2 logb 𝑋 ) ) ) ) < 2 ) )
32		1p1e2	⊢ ( 1 + 1 ) = 2
33	32	breq2i	⊢ ( ( 𝑋 / ( 2 ↑ ( ⌊ ‘ ( 2 logb 𝑋 ) ) ) ) < ( 1 + 1 ) ↔ ( 𝑋 / ( 2 ↑ ( ⌊ ‘ ( 2 logb 𝑋 ) ) ) ) < 2 )
34	31 33	imbitrrdi	⊢ ( 𝑋 ∈ ℝ+ → ( 𝑋 < ( 2 ↑ ( ( ⌊ ‘ ( 2 logb 𝑋 ) ) + 1 ) ) → ( 𝑋 / ( 2 ↑ ( ⌊ ‘ ( 2 logb 𝑋 ) ) ) ) < ( 1 + 1 ) ) )
35	24 34	anim12d	⊢ ( 𝑋 ∈ ℝ+ → ( ( ( 2 ↑ ( ⌊ ‘ ( 2 logb 𝑋 ) ) ) ≤ 𝑋 ∧ 𝑋 < ( 2 ↑ ( ( ⌊ ‘ ( 2 logb 𝑋 ) ) + 1 ) ) ) → ( 1 ≤ ( 𝑋 / ( 2 ↑ ( ⌊ ‘ ( 2 logb 𝑋 ) ) ) ) ∧ ( 𝑋 / ( 2 ↑ ( ⌊ ‘ ( 2 logb 𝑋 ) ) ) ) < ( 1 + 1 ) ) ) )
36	6 35	mpd	⊢ ( 𝑋 ∈ ℝ+ → ( 1 ≤ ( 𝑋 / ( 2 ↑ ( ⌊ ‘ ( 2 logb 𝑋 ) ) ) ) ∧ ( 𝑋 / ( 2 ↑ ( ⌊ ‘ ( 2 logb 𝑋 ) ) ) ) < ( 1 + 1 ) ) )
37	25 10 13	expne0d	⊢ ( 𝑋 ∈ ℝ+ → ( 2 ↑ ( ⌊ ‘ ( 2 logb 𝑋 ) ) ) ≠ 0 )
38	20 14 37	redivcld	⊢ ( 𝑋 ∈ ℝ+ → ( 𝑋 / ( 2 ↑ ( ⌊ ‘ ( 2 logb 𝑋 ) ) ) ) ∈ ℝ )
39		1zzd	⊢ ( 𝑋 ∈ ℝ+ → 1 ∈ ℤ )
40		flbi	⊢ ( ( ( 𝑋 / ( 2 ↑ ( ⌊ ‘ ( 2 logb 𝑋 ) ) ) ) ∈ ℝ ∧ 1 ∈ ℤ ) → ( ( ⌊ ‘ ( 𝑋 / ( 2 ↑ ( ⌊ ‘ ( 2 logb 𝑋 ) ) ) ) ) = 1 ↔ ( 1 ≤ ( 𝑋 / ( 2 ↑ ( ⌊ ‘ ( 2 logb 𝑋 ) ) ) ) ∧ ( 𝑋 / ( 2 ↑ ( ⌊ ‘ ( 2 logb 𝑋 ) ) ) ) < ( 1 + 1 ) ) ) )
41	38 39 40	syl2anc	⊢ ( 𝑋 ∈ ℝ+ → ( ( ⌊ ‘ ( 𝑋 / ( 2 ↑ ( ⌊ ‘ ( 2 logb 𝑋 ) ) ) ) ) = 1 ↔ ( 1 ≤ ( 𝑋 / ( 2 ↑ ( ⌊ ‘ ( 2 logb 𝑋 ) ) ) ) ∧ ( 𝑋 / ( 2 ↑ ( ⌊ ‘ ( 2 logb 𝑋 ) ) ) ) < ( 1 + 1 ) ) ) )
42	36 41	mpbird	⊢ ( 𝑋 ∈ ℝ+ → ( ⌊ ‘ ( 𝑋 / ( 2 ↑ ( ⌊ ‘ ( 2 logb 𝑋 ) ) ) ) ) = 1 )