Theorem 3lexlogpow5ineq4

Description: Sharper logarithm inequality chain. (Contributed by metakunt, 21-Aug-2024)

	Ref	Expression
Hypotheses	3lexlogpow5ineq4.1	⊢ ( 𝜑 → 𝑋 ∈ ℝ )
	3lexlogpow5ineq4.2	⊢ ( 𝜑 → 3 ≤ 𝑋 )
Assertion	3lexlogpow5ineq4	⊢ ( 𝜑 → 9 < ( ( 2 logb 𝑋 ) ↑ 5 ) )

Proof

Step	Hyp	Ref	Expression
1		3lexlogpow5ineq4.1	⊢ ( 𝜑 → 𝑋 ∈ ℝ )
2		3lexlogpow5ineq4.2	⊢ ( 𝜑 → 3 ≤ 𝑋 )
3		9re	⊢ 9 ∈ ℝ
4	3	a1i	⊢ ( 𝜑 → 9 ∈ ℝ )
5		1nn0	⊢ 1 ∈ ℕ0
6		1nn	⊢ 1 ∈ ℕ
7	5 6	decnncl	⊢ ; 1 1 ∈ ℕ
8	7	a1i	⊢ ( 𝜑 → ; 1 1 ∈ ℕ )
9	8	nnred	⊢ ( 𝜑 → ; 1 1 ∈ ℝ )
10		7re	⊢ 7 ∈ ℝ
11	10	a1i	⊢ ( 𝜑 → 7 ∈ ℝ )
12		0red	⊢ ( 𝜑 → 0 ∈ ℝ )
13		7pos	⊢ 0 < 7
14	13	a1i	⊢ ( 𝜑 → 0 < 7 )
15	12 14	ltned	⊢ ( 𝜑 → 0 ≠ 7 )
16	15	necomd	⊢ ( 𝜑 → 7 ≠ 0 )
17	9 11 16	redivcld	⊢ ( 𝜑 → ( ; 1 1 / 7 ) ∈ ℝ )
18		5nn0	⊢ 5 ∈ ℕ0
19	18	a1i	⊢ ( 𝜑 → 5 ∈ ℕ0 )
20	17 19	reexpcld	⊢ ( 𝜑 → ( ( ; 1 1 / 7 ) ↑ 5 ) ∈ ℝ )
21		2re	⊢ 2 ∈ ℝ
22	21	a1i	⊢ ( 𝜑 → 2 ∈ ℝ )
23		2pos	⊢ 0 < 2
24	23	a1i	⊢ ( 𝜑 → 0 < 2 )
25		3re	⊢ 3 ∈ ℝ
26	25	a1i	⊢ ( 𝜑 → 3 ∈ ℝ )
27		3pos	⊢ 0 < 3
28	27	a1i	⊢ ( 𝜑 → 0 < 3 )
29	12 26 1 28 2	ltletrd	⊢ ( 𝜑 → 0 < 𝑋 )
30		1red	⊢ ( 𝜑 → 1 ∈ ℝ )
31		1lt2	⊢ 1 < 2
32	31	a1i	⊢ ( 𝜑 → 1 < 2 )
33	30 32	ltned	⊢ ( 𝜑 → 1 ≠ 2 )
34	33	necomd	⊢ ( 𝜑 → 2 ≠ 1 )
35	22 24 1 29 34	relogbcld	⊢ ( 𝜑 → ( 2 logb 𝑋 ) ∈ ℝ )
36	35 19	reexpcld	⊢ ( 𝜑 → ( ( 2 logb 𝑋 ) ↑ 5 ) ∈ ℝ )
37		3lexlogpow5ineq1	⊢ 9 < ( ( ; 1 1 / 7 ) ↑ 5 )
38	37	a1i	⊢ ( 𝜑 → 9 < ( ( ; 1 1 / 7 ) ↑ 5 ) )
39	1 2	3lexlogpow5ineq2	⊢ ( 𝜑 → ( ( ; 1 1 / 7 ) ↑ 5 ) ≤ ( ( 2 logb 𝑋 ) ↑ 5 ) )
40	4 20 36 38 39	ltletrd	⊢ ( 𝜑 → 9 < ( ( 2 logb 𝑋 ) ↑ 5 ) )