Theorem 3lexlogpow5ineq2

Description: Second inequality in inequality chain, proposed by Mario Carneiro. (Contributed by metakunt, 22-May-2024)

	Ref	Expression
Hypotheses	3lexlogpow5ineq2.1	$$⊢\phi \to X\in ℝ$$
	3lexlogpow5ineq2.2	$$⊢\phi \to 3\le X$$
Assertion	3lexlogpow5ineq2	$$⊢\phi \to {\left(\frac{11}{7}\right)}^5\le {{\log }_{2}X}^5$$

Proof

Step	Hyp	Ref	Expression
1		3lexlogpow5ineq2.1	$$⊢\phi \to X\in ℝ$$
2		3lexlogpow5ineq2.2	$$⊢\phi \to 3\le X$$
3		1nn0	$$⊢1\in {\mathbb{N}}_0$$
4		1nn	$$⊢1\in \mathbb{N}$$
5	3 4	decnncl	$$⊢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		2re	$$⊢2\in ℝ$$
17	16	a1i	$$⊢\phi \to 2\in ℝ$$
18		2pos	$$⊢0<2$$
19	18	a1i	$$⊢\phi \to 0<2$$
20		3re	$$⊢3\in ℝ$$
21	20	a1i	$$⊢\phi \to 3\in ℝ$$
22		3pos	$$⊢0<3$$
23	22	a1i	$$⊢\phi \to 0<3$$
24	10 21 1 23 2	ltletrd	$$⊢\phi \to 0<X$$
25		1red	$$⊢\phi \to 1\in ℝ$$
26		1lt2	$$⊢1<2$$
27	26	a1i	$$⊢\phi \to 1<2$$
28	25 27	ltned	$$⊢\phi \to 1\ne 2$$
29	28	necomd	$$⊢\phi \to 2\ne 1$$
30	17 19 1 24 29	relogbcld	$$⊢\phi \to {\log }_{2}X\in ℝ$$
31		5nn0	$$⊢5\in {\mathbb{N}}_0$$
32	31	a1i	$$⊢\phi \to 5\in {\mathbb{N}}_0$$
33		7nn	$$⊢7\in \mathbb{N}$$
34	33	a1i	$$⊢\phi \to 7\in \mathbb{N}$$
35	34	nnrpd	$$⊢\phi \to 7\in {ℝ}^{+}$$
36		0nn0	$$⊢0\in {\mathbb{N}}_0$$
37		tru	$$⊢\top$$
38		0red	$$⊢\top \to 0\in ℝ$$
39		9re	$$⊢9\in ℝ$$
40	39	a1i	$$⊢\top \to 9\in ℝ$$
41		9pos	$$⊢0<9$$
42	41	a1i	$$⊢\top \to 0<9$$
43	38 40 42	ltled	$$⊢\top \to 0\le 9$$
44	37 43	ax-mp	$$⊢0\le 9$$
45	4 3 36 44	declei	$$⊢0\le 11$$
46	45	a1i	$$⊢\phi \to 0\le 11$$
47	7 35 46	divge0d	$$⊢\phi \to 0\le \frac{11}{7}$$
48	17 19 21 23 29	relogbcld	$$⊢\phi \to {\log }_{2}3\in ℝ$$
49		2exp11	$$⊢2^{11}=2048$$
50	49	eqcomi	$$⊢2048=2^{11}$$
51	50	a1i	$$⊢\phi \to 2048=2^{11}$$
52	51	oveq2d	$$⊢\phi \to {\log }_{2}2048={\log }_2{2}^{11}$$
53	17 19	elrpd	$$⊢\phi \to 2\in {ℝ}^{+}$$
54	6	nnzd	$$⊢\phi \to 11\in \mathbb{Z}$$
55	53 29 54	relogbexpd	$$⊢\phi \to {\log }_2{2}^{11}=11$$
56	52 55	eqtrd	$$⊢\phi \to {\log }_{2}2048=11$$
57	56	eqcomd	$$⊢\phi \to 11={\log }_{2}2048$$
58		2z	$$⊢2\in \mathbb{Z}$$
59	58	a1i	$$⊢\phi \to 2\in \mathbb{Z}$$
60	17	leidd	$$⊢\phi \to 2\le 2$$
61		2nn0	$$⊢2\in {\mathbb{N}}_0$$
62	61 36	deccl	$$⊢20\in {\mathbb{N}}_0$$
63		4nn0	$$⊢4\in {\mathbb{N}}_0$$
64	62 63	deccl	$$⊢204\in {\mathbb{N}}_0$$
65		8nn	$$⊢8\in \mathbb{N}$$
66	64 65	decnncl	$$⊢2048\in \mathbb{N}$$
67	66	a1i	$$⊢\phi \to 2048\in \mathbb{N}$$
68	67	nnred	$$⊢\phi \to 2048\in ℝ$$
69		4nn	$$⊢4\in \mathbb{N}$$
70	62 69	decnncl	$$⊢204\in \mathbb{N}$$
71		8nn0	$$⊢8\in {\mathbb{N}}_0$$
72	70 71 36 44	decltdi	$$⊢0<2048$$
73	72	a1i	$$⊢\phi \to 0<2048$$
74	61 3	deccl	$$⊢21\in {\mathbb{N}}_0$$
75	74 71	deccl	$$⊢218\in {\mathbb{N}}_0$$
76	75 33	decnncl	$$⊢2187\in \mathbb{N}$$
77	76	a1i	$$⊢\phi \to 2187\in \mathbb{N}$$
78	77	nnred	$$⊢\phi \to 2187\in ℝ$$
79	74 65	decnncl	$$⊢218\in \mathbb{N}$$
80		7nn0	$$⊢7\in {\mathbb{N}}_0$$
81	79 80 36 44	decltdi	$$⊢0<2187$$
82	81	a1i	$$⊢\phi \to 0<2187$$
83		8re	$$⊢8\in ℝ$$
84	83 3	nn0addge1i	$$⊢8\le 8+1$$
85		8p1e9	$$⊢8+1=9$$
86	84 85	breqtri	$$⊢8\le 9$$
87		4lt10	$$⊢4<10$$
88		0lt1	$$⊢0<1$$
89	61 36 4 88	declt	$$⊢20<21$$
90	62 74 63 71 87 89	decltc	$$⊢204<218$$
91	64 75 71 80 86 90	decleh	$$⊢2048\le 2187$$
92	91	a1i	$$⊢\phi \to 2048\le 2187$$
93	59 60 68 73 78 82 92	logblebd	$$⊢\phi \to {\log }_{2}2048\le {\log }_{2}2187$$
94	57 93	eqbrtrd	$$⊢\phi \to 11\le {\log }_{2}2187$$
95	7	recnd	$$⊢\phi \to 11\in ℂ$$
96	9	recnd	$$⊢\phi \to 7\in ℂ$$
97	95 96 14	divcan1d	$$⊢\phi \to \left(\frac{11}{7}\right)\cdot 7=11$$
98	97	eqcomd	$$⊢\phi \to 11=\left(\frac{11}{7}\right)\cdot 7$$
99		3exp7	$$⊢3^7=2187$$
100	99	eqcomi	$$⊢2187=3^7$$
101	100	a1i	$$⊢\phi \to 2187=3^7$$
102	101	oveq2d	$$⊢\phi \to {\log }_{2}2187={\log }_2{3}^7$$
103	21 23	elrpd	$$⊢\phi \to 3\in {ℝ}^{+}$$
104	34	nnzd	$$⊢\phi \to 7\in \mathbb{Z}$$
105	53 29 103 104	relogbzexpd	$$⊢\phi \to {\log }_2{3}^7=7{\log }_{2}3$$
106	102 105	eqtrd	$$⊢\phi \to {\log }_{2}2187=7{\log }_{2}3$$
107	48	recnd	$$⊢\phi \to {\log }_{2}3\in ℂ$$
108	96 107	mulcomd	$$⊢\phi \to 7{\log }_{2}3={\log }_{2}3\cdot 7$$
109	106 108	eqtrd	$$⊢\phi \to {\log }_{2}2187={\log }_{2}3\cdot 7$$
110	94 98 109	3brtr3d	$$⊢\phi \to \left(\frac{11}{7}\right)\cdot 7\le {\log }_{2}3\cdot 7$$
111	15 48 35	lemul1d	$$⊢\phi \to \left(\frac{11}{7}\le {\log }_{2}3\leftrightarrow \left(\frac{11}{7}\right)\cdot 7\le {\log }_{2}3\cdot 7\right)$$
112	110 111	mpbird	$$⊢\phi \to \frac{11}{7}\le {\log }_{2}3$$
113	59 60 21 23 1 24 2	logblebd	$$⊢\phi \to {\log }_{2}3\le {\log }_{2}X$$
114	15 48 30 112 113	letrd	$$⊢\phi \to \frac{11}{7}\le {\log }_{2}X$$
115	15 30 32 47 114	leexp1ad	$$⊢\phi \to {\left(\frac{11}{7}\right)}^5\le {{\log }_{2}X}^5$$