Theorem fllogbd

Description: A real number is between the base of a logarithm to the power of the floor of the logarithm of the number and the base of the logarithm to the power of the floor of the logarithm of the number plus one. (Contributed by AV, 23-May-2020)

	Ref	Expression
Hypotheses	fllogbd.b	⊢ ( 𝜑 → 𝐵 ∈ ( ℤ≥ ‘ 2 ) )
	fllogbd.x	⊢ ( 𝜑 → 𝑋 ∈ ℝ+ )
	fllogbd.e	⊢ 𝐸 = ( ⌊ ‘ ( 𝐵 logb 𝑋 ) )
Assertion	fllogbd	⊢ ( 𝜑 → ( ( 𝐵 ↑ 𝐸 ) ≤ 𝑋 ∧ 𝑋 < ( 𝐵 ↑ ( 𝐸 + 1 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		fllogbd.b	⊢ ( 𝜑 → 𝐵 ∈ ( ℤ≥ ‘ 2 ) )
2		fllogbd.x	⊢ ( 𝜑 → 𝑋 ∈ ℝ+ )
3		fllogbd.e	⊢ 𝐸 = ( ⌊ ‘ ( 𝐵 logb 𝑋 ) )
4		relogbzcl	⊢ ( ( 𝐵 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑋 ∈ ℝ+ ) → ( 𝐵 logb 𝑋 ) ∈ ℝ )
5	1 2 4	syl2anc	⊢ ( 𝜑 → ( 𝐵 logb 𝑋 ) ∈ ℝ )
6		flle	⊢ ( ( 𝐵 logb 𝑋 ) ∈ ℝ → ( ⌊ ‘ ( 𝐵 logb 𝑋 ) ) ≤ ( 𝐵 logb 𝑋 ) )
7	5 6	syl	⊢ ( 𝜑 → ( ⌊ ‘ ( 𝐵 logb 𝑋 ) ) ≤ ( 𝐵 logb 𝑋 ) )
8	3 7	eqbrtrid	⊢ ( 𝜑 → 𝐸 ≤ ( 𝐵 logb 𝑋 ) )
9		eluzelz	⊢ ( 𝐵 ∈ ( ℤ≥ ‘ 2 ) → 𝐵 ∈ ℤ )
10	1 9	syl	⊢ ( 𝜑 → 𝐵 ∈ ℤ )
11	10	zred	⊢ ( 𝜑 → 𝐵 ∈ ℝ )
12		eluz2b1	⊢ ( 𝐵 ∈ ( ℤ≥ ‘ 2 ) ↔ ( 𝐵 ∈ ℤ ∧ 1 < 𝐵 ) )
13	12	simprbi	⊢ ( 𝐵 ∈ ( ℤ≥ ‘ 2 ) → 1 < 𝐵 )
14	1 13	syl	⊢ ( 𝜑 → 1 < 𝐵 )
15	5	flcld	⊢ ( 𝜑 → ( ⌊ ‘ ( 𝐵 logb 𝑋 ) ) ∈ ℤ )
16	3 15	eqeltrid	⊢ ( 𝜑 → 𝐸 ∈ ℤ )
17	16	zred	⊢ ( 𝜑 → 𝐸 ∈ ℝ )
18	11 14 17 5	cxpled	⊢ ( 𝜑 → ( 𝐸 ≤ ( 𝐵 logb 𝑋 ) ↔ ( 𝐵 ↑𝑐 𝐸 ) ≤ ( 𝐵 ↑𝑐 ( 𝐵 logb 𝑋 ) ) ) )
19	8 18	mpbid	⊢ ( 𝜑 → ( 𝐵 ↑𝑐 𝐸 ) ≤ ( 𝐵 ↑𝑐 ( 𝐵 logb 𝑋 ) ) )
20	10	zcnd	⊢ ( 𝜑 → 𝐵 ∈ ℂ )
21		eluz2nn	⊢ ( 𝐵 ∈ ( ℤ≥ ‘ 2 ) → 𝐵 ∈ ℕ )
22	1 21	syl	⊢ ( 𝜑 → 𝐵 ∈ ℕ )
23	22	nnne0d	⊢ ( 𝜑 → 𝐵 ≠ 0 )
24	20 23 16	cxpexpzd	⊢ ( 𝜑 → ( 𝐵 ↑𝑐 𝐸 ) = ( 𝐵 ↑ 𝐸 ) )
25		eluz2cnn0n1	⊢ ( 𝐵 ∈ ( ℤ≥ ‘ 2 ) → 𝐵 ∈ ( ℂ ∖ { 0 , 1 } ) )
26	1 25	syl	⊢ ( 𝜑 → 𝐵 ∈ ( ℂ ∖ { 0 , 1 } ) )
27		rpcnne0	⊢ ( 𝑋 ∈ ℝ+ → ( 𝑋 ∈ ℂ ∧ 𝑋 ≠ 0 ) )
28		eldifsn	⊢ ( 𝑋 ∈ ( ℂ ∖ { 0 } ) ↔ ( 𝑋 ∈ ℂ ∧ 𝑋 ≠ 0 ) )
29	27 28	sylibr	⊢ ( 𝑋 ∈ ℝ+ → 𝑋 ∈ ( ℂ ∖ { 0 } ) )
30	2 29	syl	⊢ ( 𝜑 → 𝑋 ∈ ( ℂ ∖ { 0 } ) )
31		cxplogb	⊢ ( ( 𝐵 ∈ ( ℂ ∖ { 0 , 1 } ) ∧ 𝑋 ∈ ( ℂ ∖ { 0 } ) ) → ( 𝐵 ↑𝑐 ( 𝐵 logb 𝑋 ) ) = 𝑋 )
32	26 30 31	syl2anc	⊢ ( 𝜑 → ( 𝐵 ↑𝑐 ( 𝐵 logb 𝑋 ) ) = 𝑋 )
33	19 24 32	3brtr3d	⊢ ( 𝜑 → ( 𝐵 ↑ 𝐸 ) ≤ 𝑋 )
34		flltp1	⊢ ( ( 𝐵 logb 𝑋 ) ∈ ℝ → ( 𝐵 logb 𝑋 ) < ( ( ⌊ ‘ ( 𝐵 logb 𝑋 ) ) + 1 ) )
35	5 34	syl	⊢ ( 𝜑 → ( 𝐵 logb 𝑋 ) < ( ( ⌊ ‘ ( 𝐵 logb 𝑋 ) ) + 1 ) )
36	3	a1i	⊢ ( 𝜑 → 𝐸 = ( ⌊ ‘ ( 𝐵 logb 𝑋 ) ) )
37	36	oveq1d	⊢ ( 𝜑 → ( 𝐸 + 1 ) = ( ( ⌊ ‘ ( 𝐵 logb 𝑋 ) ) + 1 ) )
38	35 37	breqtrrd	⊢ ( 𝜑 → ( 𝐵 logb 𝑋 ) < ( 𝐸 + 1 ) )
39	16	peano2zd	⊢ ( 𝜑 → ( 𝐸 + 1 ) ∈ ℤ )
40	39	zred	⊢ ( 𝜑 → ( 𝐸 + 1 ) ∈ ℝ )
41	11 14 5 40	cxpltd	⊢ ( 𝜑 → ( ( 𝐵 logb 𝑋 ) < ( 𝐸 + 1 ) ↔ ( 𝐵 ↑𝑐 ( 𝐵 logb 𝑋 ) ) < ( 𝐵 ↑𝑐 ( 𝐸 + 1 ) ) ) )
42	38 41	mpbid	⊢ ( 𝜑 → ( 𝐵 ↑𝑐 ( 𝐵 logb 𝑋 ) ) < ( 𝐵 ↑𝑐 ( 𝐸 + 1 ) ) )
43	20 23 39	cxpexpzd	⊢ ( 𝜑 → ( 𝐵 ↑𝑐 ( 𝐸 + 1 ) ) = ( 𝐵 ↑ ( 𝐸 + 1 ) ) )
44	42 32 43	3brtr3d	⊢ ( 𝜑 → 𝑋 < ( 𝐵 ↑ ( 𝐸 + 1 ) ) )
45	33 44	jca	⊢ ( 𝜑 → ( ( 𝐵 ↑ 𝐸 ) ≤ 𝑋 ∧ 𝑋 < ( 𝐵 ↑ ( 𝐸 + 1 ) ) ) )