Theorem 3lexlogpow5ineq4

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

	Ref	Expression
Hypotheses	3lexlogpow5ineq4.1	$$⊢\phi \to X\in ℝ$$
	3lexlogpow5ineq4.2	$$⊢\phi \to 3\le X$$
Assertion	3lexlogpow5ineq4	$$⊢\phi \to 9<{{\log }_{2}X}^5$$

Proof

Step	Hyp	Ref	Expression
1		3lexlogpow5ineq4.1	$$⊢\phi \to X\in ℝ$$
2		3lexlogpow5ineq4.2	$$⊢\phi \to 3\le X$$
3		9re	$$⊢9\in ℝ$$
4	3	a1i	$$⊢\phi \to 9\in ℝ$$
5		1nn0	$$⊢1\in {\mathbb{N}}_0$$
6		1nn	$$⊢1\in \mathbb{N}$$
7	5 6	decnncl	$$⊢11\in \mathbb{N}$$
8	7	a1i	$$⊢\phi \to 11\in \mathbb{N}$$
9	8	nnred	$$⊢\phi \to 11\in ℝ$$
10		7re	$$⊢7\in ℝ$$
11	10	a1i	$$⊢\phi \to 7\in ℝ$$
12		0red	$$⊢\phi \to 0\in ℝ$$
13		7pos	$$⊢0<7$$
14	13	a1i	$$⊢\phi \to 0<7$$
15	12 14	ltned	$$⊢\phi \to 0\ne 7$$
16	15	necomd	$$⊢\phi \to 7\ne 0$$
17	9 11 16	redivcld	$$⊢\phi \to \frac{11}{7}\in ℝ$$
18		5nn0	$$⊢5\in {\mathbb{N}}_0$$
19	18	a1i	$$⊢\phi \to 5\in {\mathbb{N}}_0$$
20	17 19	reexpcld	$$⊢\phi \to {\left(\frac{11}{7}\right)}^5\in ℝ$$
21		2re	$$⊢2\in ℝ$$
22	21	a1i	$$⊢\phi \to 2\in ℝ$$
23		2pos	$$⊢0<2$$
24	23	a1i	$$⊢\phi \to 0<2$$
25		3re	$$⊢3\in ℝ$$
26	25	a1i	$$⊢\phi \to 3\in ℝ$$
27		3pos	$$⊢0<3$$
28	27	a1i	$$⊢\phi \to 0<3$$
29	12 26 1 28 2	ltletrd	$$⊢\phi \to 0<X$$
30		1red	$$⊢\phi \to 1\in ℝ$$
31		1lt2	$$⊢1<2$$
32	31	a1i	$$⊢\phi \to 1<2$$
33	30 32	ltned	$$⊢\phi \to 1\ne 2$$
34	33	necomd	$$⊢\phi \to 2\ne 1$$
35	22 24 1 29 34	relogbcld	$$⊢\phi \to {\log }_{2}X\in ℝ$$
36	35 19	reexpcld	$$⊢\phi \to {{\log }_{2}X}^5\in ℝ$$
37		3lexlogpow5ineq1	$$⊢9<{\left(\frac{11}{7}\right)}^5$$
38	37	a1i	$$⊢\phi \to 9<{\left(\frac{11}{7}\right)}^5$$
39	1 2	3lexlogpow5ineq2	$$⊢\phi \to {\left(\frac{11}{7}\right)}^5\le {{\log }_{2}X}^5$$
40	4 20 36 38 39	ltletrd	$$⊢\phi \to 9<{{\log }_{2}X}^5$$