Theorem 3lexlogpow5ineq3

Description: Combined inequality chain for a specific power of the binary logarithm, proposed by Mario Carneiro. (Contributed by metakunt, 22-May-2024)

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

Proof

Step	Hyp	Ref	Expression
1		3lexlogpow5ineq3.1	⊢ ( 𝜑 → 𝑋 ∈ ℝ )
2		3lexlogpow5ineq3.2	⊢ ( 𝜑 → 3 ≤ 𝑋 )
3		7re	⊢ 7 ∈ ℝ
4	3	a1i	⊢ ( 𝜑 → 7 ∈ ℝ )
5		9re	⊢ 9 ∈ ℝ
6	5	a1i	⊢ ( 𝜑 → 9 ∈ ℝ )
7		2re	⊢ 2 ∈ ℝ
8	7	a1i	⊢ ( 𝜑 → 2 ∈ ℝ )
9		2pos	⊢ 0 < 2
10	9	a1i	⊢ ( 𝜑 → 0 < 2 )
11		0red	⊢ ( 𝜑 → 0 ∈ ℝ )
12		3re	⊢ 3 ∈ ℝ
13	12	a1i	⊢ ( 𝜑 → 3 ∈ ℝ )
14		3pos	⊢ 0 < 3
15	14	a1i	⊢ ( 𝜑 → 0 < 3 )
16	11 13 1 15 2	ltletrd	⊢ ( 𝜑 → 0 < 𝑋 )
17		1red	⊢ ( 𝜑 → 1 ∈ ℝ )
18		1lt2	⊢ 1 < 2
19	18	a1i	⊢ ( 𝜑 → 1 < 2 )
20	17 19	ltned	⊢ ( 𝜑 → 1 ≠ 2 )
21	20	necomd	⊢ ( 𝜑 → 2 ≠ 1 )
22	8 10 1 16 21	relogbcld	⊢ ( 𝜑 → ( 2 logb 𝑋 ) ∈ ℝ )
23		5nn0	⊢ 5 ∈ ℕ0
24	23	a1i	⊢ ( 𝜑 → 5 ∈ ℕ0 )
25	22 24	reexpcld	⊢ ( 𝜑 → ( ( 2 logb 𝑋 ) ↑ 5 ) ∈ ℝ )
26		7lt9	⊢ 7 < 9
27	26	a1i	⊢ ( 𝜑 → 7 < 9 )
28	1 2	3lexlogpow5ineq4	⊢ ( 𝜑 → 9 < ( ( 2 logb 𝑋 ) ↑ 5 ) )
29	4 6 25 27 28	lttrd	⊢ ( 𝜑 → 7 < ( ( 2 logb 𝑋 ) ↑ 5 ) )