Metamath Proof Explorer

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 )