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