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	$$⊢\phi \to X\in ℝ$$
	3lexlogpow5ineq3.2	$$⊢\phi \to 3\le X$$
Assertion	3lexlogpow5ineq3	$$⊢\phi \to 7<{{\log }_{2}X}^5$$

Proof

Step	Hyp	Ref	Expression
1		3lexlogpow5ineq3.1	$$⊢\phi \to X\in ℝ$$
2		3lexlogpow5ineq3.2	$$⊢\phi \to 3\le X$$
3		7re	$$⊢7\in ℝ$$
4	3	a1i	$$⊢\phi \to 7\in ℝ$$
5		9re	$$⊢9\in ℝ$$
6	5	a1i	$$⊢\phi \to 9\in ℝ$$
7		2re	$$⊢2\in ℝ$$
8	7	a1i	$$⊢\phi \to 2\in ℝ$$
9		2pos	$$⊢0<2$$
10	9	a1i	$$⊢\phi \to 0<2$$
11		0red	$$⊢\phi \to 0\in ℝ$$
12		3re	$$⊢3\in ℝ$$
13	12	a1i	$$⊢\phi \to 3\in ℝ$$
14		3pos	$$⊢0<3$$
15	14	a1i	$$⊢\phi \to 0<3$$
16	11 13 1 15 2	ltletrd	$$⊢\phi \to 0<X$$
17		1red	$$⊢\phi \to 1\in ℝ$$
18		1lt2	$$⊢1<2$$
19	18	a1i	$$⊢\phi \to 1<2$$
20	17 19	ltned	$$⊢\phi \to 1\ne 2$$
21	20	necomd	$$⊢\phi \to 2\ne 1$$
22	8 10 1 16 21	relogbcld	$$⊢\phi \to {\log }_{2}X\in ℝ$$
23		5nn0	$$⊢5\in {\mathbb{N}}_0$$
24	23	a1i	$$⊢\phi \to 5\in {\mathbb{N}}_0$$
25	22 24	reexpcld	$$⊢\phi \to {{\log }_{2}X}^5\in ℝ$$
26		7lt9	$$⊢7<9$$
27	26	a1i	$$⊢\phi \to 7<9$$
28	1 2	3lexlogpow5ineq4	$$⊢\phi \to 9<{{\log }_{2}X}^5$$
29	4 6 25 27 28	lttrd	$$⊢\phi \to 7<{{\log }_{2}X}^5$$