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