Theorem 3lexlogpow5ineq2

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

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

Proof

Step	Hyp	Ref	Expression
1		3lexlogpow5ineq2.1	⊢ ( 𝜑 → 𝑋 ∈ ℝ )
2		3lexlogpow5ineq2.2	⊢ ( 𝜑 → 3 ≤ 𝑋 )
3		1nn0	⊢ 1 ∈ ℕ0
4		1nn	⊢ 1 ∈ ℕ
5	3 4	decnncl	⊢ ; 1 1 ∈ ℕ
6	5	a1i	⊢ ( 𝜑 → ; 1 1 ∈ ℕ )
7	6	nnred	⊢ ( 𝜑 → ; 1 1 ∈ ℝ )
8		7re	⊢ 7 ∈ ℝ
9	8	a1i	⊢ ( 𝜑 → 7 ∈ ℝ )
10		0red	⊢ ( 𝜑 → 0 ∈ ℝ )
11		7pos	⊢ 0 < 7
12	11	a1i	⊢ ( 𝜑 → 0 < 7 )
13	10 12	ltned	⊢ ( 𝜑 → 0 ≠ 7 )
14	13	necomd	⊢ ( 𝜑 → 7 ≠ 0 )
15	7 9 14	redivcld	⊢ ( 𝜑 → ( ; 1 1 / 7 ) ∈ ℝ )
16		2re	⊢ 2 ∈ ℝ
17	16	a1i	⊢ ( 𝜑 → 2 ∈ ℝ )
18		2pos	⊢ 0 < 2
19	18	a1i	⊢ ( 𝜑 → 0 < 2 )
20		3re	⊢ 3 ∈ ℝ
21	20	a1i	⊢ ( 𝜑 → 3 ∈ ℝ )
22		3pos	⊢ 0 < 3
23	22	a1i	⊢ ( 𝜑 → 0 < 3 )
24	10 21 1 23 2	ltletrd	⊢ ( 𝜑 → 0 < 𝑋 )
25		1red	⊢ ( 𝜑 → 1 ∈ ℝ )
26		1lt2	⊢ 1 < 2
27	26	a1i	⊢ ( 𝜑 → 1 < 2 )
28	25 27	ltned	⊢ ( 𝜑 → 1 ≠ 2 )
29	28	necomd	⊢ ( 𝜑 → 2 ≠ 1 )
30	17 19 1 24 29	relogbcld	⊢ ( 𝜑 → ( 2 logb 𝑋 ) ∈ ℝ )
31		5nn0	⊢ 5 ∈ ℕ0
32	31	a1i	⊢ ( 𝜑 → 5 ∈ ℕ0 )
33		7nn	⊢ 7 ∈ ℕ
34	33	a1i	⊢ ( 𝜑 → 7 ∈ ℕ )
35	34	nnrpd	⊢ ( 𝜑 → 7 ∈ ℝ+ )
36		0nn0	⊢ 0 ∈ ℕ0
37		tru	⊢ ⊤
38		0red	⊢ ( ⊤ → 0 ∈ ℝ )
39		9re	⊢ 9 ∈ ℝ
40	39	a1i	⊢ ( ⊤ → 9 ∈ ℝ )
41		9pos	⊢ 0 < 9
42	41	a1i	⊢ ( ⊤ → 0 < 9 )
43	38 40 42	ltled	⊢ ( ⊤ → 0 ≤ 9 )
44	37 43	ax-mp	⊢ 0 ≤ 9
45	4 3 36 44	declei	⊢ 0 ≤ ; 1 1
46	45	a1i	⊢ ( 𝜑 → 0 ≤ ; 1 1 )
47	7 35 46	divge0d	⊢ ( 𝜑 → 0 ≤ ( ; 1 1 / 7 ) )
48	17 19 21 23 29	relogbcld	⊢ ( 𝜑 → ( 2 logb 3 ) ∈ ℝ )
49		2exp11	⊢ ( 2 ↑ ; 1 1 ) = ; ; ; 2 0 4 8
50	49	eqcomi	⊢ ; ; ; 2 0 4 8 = ( 2 ↑ ; 1 1 )
51	50	a1i	⊢ ( 𝜑 → ; ; ; 2 0 4 8 = ( 2 ↑ ; 1 1 ) )
52	51	oveq2d	⊢ ( 𝜑 → ( 2 logb ; ; ; 2 0 4 8 ) = ( 2 logb ( 2 ↑ ; 1 1 ) ) )
53	17 19	elrpd	⊢ ( 𝜑 → 2 ∈ ℝ+ )
54	6	nnzd	⊢ ( 𝜑 → ; 1 1 ∈ ℤ )
55	53 29 54	relogbexpd	⊢ ( 𝜑 → ( 2 logb ( 2 ↑ ; 1 1 ) ) = ; 1 1 )
56	52 55	eqtrd	⊢ ( 𝜑 → ( 2 logb ; ; ; 2 0 4 8 ) = ; 1 1 )
57	56	eqcomd	⊢ ( 𝜑 → ; 1 1 = ( 2 logb ; ; ; 2 0 4 8 ) )
58		2z	⊢ 2 ∈ ℤ
59	58	a1i	⊢ ( 𝜑 → 2 ∈ ℤ )
60	17	leidd	⊢ ( 𝜑 → 2 ≤ 2 )
61		2nn0	⊢ 2 ∈ ℕ0
62	61 36	deccl	⊢ ; 2 0 ∈ ℕ0
63		4nn0	⊢ 4 ∈ ℕ0
64	62 63	deccl	⊢ ; ; 2 0 4 ∈ ℕ0
65		8nn	⊢ 8 ∈ ℕ
66	64 65	decnncl	⊢ ; ; ; 2 0 4 8 ∈ ℕ
67	66	a1i	⊢ ( 𝜑 → ; ; ; 2 0 4 8 ∈ ℕ )
68	67	nnred	⊢ ( 𝜑 → ; ; ; 2 0 4 8 ∈ ℝ )
69		4nn	⊢ 4 ∈ ℕ
70	62 69	decnncl	⊢ ; ; 2 0 4 ∈ ℕ
71		8nn0	⊢ 8 ∈ ℕ0
72	70 71 36 44	decltdi	⊢ 0 < ; ; ; 2 0 4 8
73	72	a1i	⊢ ( 𝜑 → 0 < ; ; ; 2 0 4 8 )
74	61 3	deccl	⊢ ; 2 1 ∈ ℕ0
75	74 71	deccl	⊢ ; ; 2 1 8 ∈ ℕ0
76	75 33	decnncl	⊢ ; ; ; 2 1 8 7 ∈ ℕ
77	76	a1i	⊢ ( 𝜑 → ; ; ; 2 1 8 7 ∈ ℕ )
78	77	nnred	⊢ ( 𝜑 → ; ; ; 2 1 8 7 ∈ ℝ )
79	74 65	decnncl	⊢ ; ; 2 1 8 ∈ ℕ
80		7nn0	⊢ 7 ∈ ℕ0
81	79 80 36 44	decltdi	⊢ 0 < ; ; ; 2 1 8 7
82	81	a1i	⊢ ( 𝜑 → 0 < ; ; ; 2 1 8 7 )
83		8re	⊢ 8 ∈ ℝ
84	83 3	nn0addge1i	⊢ 8 ≤ ( 8 + 1 )
85		8p1e9	⊢ ( 8 + 1 ) = 9
86	84 85	breqtri	⊢ 8 ≤ 9
87		4lt10	⊢ 4 < ; 1 0
88		0lt1	⊢ 0 < 1
89	61 36 4 88	declt	⊢ ; 2 0 < ; 2 1
90	62 74 63 71 87 89	decltc	⊢ ; ; 2 0 4 < ; ; 2 1 8
91	64 75 71 80 86 90	decleh	⊢ ; ; ; 2 0 4 8 ≤ ; ; ; 2 1 8 7
92	91	a1i	⊢ ( 𝜑 → ; ; ; 2 0 4 8 ≤ ; ; ; 2 1 8 7 )
93	59 60 68 73 78 82 92	logblebd	⊢ ( 𝜑 → ( 2 logb ; ; ; 2 0 4 8 ) ≤ ( 2 logb ; ; ; 2 1 8 7 ) )
94	57 93	eqbrtrd	⊢ ( 𝜑 → ; 1 1 ≤ ( 2 logb ; ; ; 2 1 8 7 ) )
95	7	recnd	⊢ ( 𝜑 → ; 1 1 ∈ ℂ )
96	9	recnd	⊢ ( 𝜑 → 7 ∈ ℂ )
97	95 96 14	divcan1d	⊢ ( 𝜑 → ( ( ; 1 1 / 7 ) · 7 ) = ; 1 1 )
98	97	eqcomd	⊢ ( 𝜑 → ; 1 1 = ( ( ; 1 1 / 7 ) · 7 ) )
99		3exp7	⊢ ( 3 ↑ 7 ) = ; ; ; 2 1 8 7
100	99	eqcomi	⊢ ; ; ; 2 1 8 7 = ( 3 ↑ 7 )
101	100	a1i	⊢ ( 𝜑 → ; ; ; 2 1 8 7 = ( 3 ↑ 7 ) )
102	101	oveq2d	⊢ ( 𝜑 → ( 2 logb ; ; ; 2 1 8 7 ) = ( 2 logb ( 3 ↑ 7 ) ) )
103	21 23	elrpd	⊢ ( 𝜑 → 3 ∈ ℝ+ )
104	34	nnzd	⊢ ( 𝜑 → 7 ∈ ℤ )
105	53 29 103 104	relogbzexpd	⊢ ( 𝜑 → ( 2 logb ( 3 ↑ 7 ) ) = ( 7 · ( 2 logb 3 ) ) )
106	102 105	eqtrd	⊢ ( 𝜑 → ( 2 logb ; ; ; 2 1 8 7 ) = ( 7 · ( 2 logb 3 ) ) )
107	48	recnd	⊢ ( 𝜑 → ( 2 logb 3 ) ∈ ℂ )
108	96 107	mulcomd	⊢ ( 𝜑 → ( 7 · ( 2 logb 3 ) ) = ( ( 2 logb 3 ) · 7 ) )
109	106 108	eqtrd	⊢ ( 𝜑 → ( 2 logb ; ; ; 2 1 8 7 ) = ( ( 2 logb 3 ) · 7 ) )
110	94 98 109	3brtr3d	⊢ ( 𝜑 → ( ( ; 1 1 / 7 ) · 7 ) ≤ ( ( 2 logb 3 ) · 7 ) )
111	15 48 35	lemul1d	⊢ ( 𝜑 → ( ( ; 1 1 / 7 ) ≤ ( 2 logb 3 ) ↔ ( ( ; 1 1 / 7 ) · 7 ) ≤ ( ( 2 logb 3 ) · 7 ) ) )
112	110 111	mpbird	⊢ ( 𝜑 → ( ; 1 1 / 7 ) ≤ ( 2 logb 3 ) )
113	59 60 21 23 1 24 2	logblebd	⊢ ( 𝜑 → ( 2 logb 3 ) ≤ ( 2 logb 𝑋 ) )
114	15 48 30 112 113	letrd	⊢ ( 𝜑 → ( ; 1 1 / 7 ) ≤ ( 2 logb 𝑋 ) )
115	15 30 32 47 114	leexp1ad	⊢ ( 𝜑 → ( ( ; 1 1 / 7 ) ↑ 5 ) ≤ ( ( 2 logb 𝑋 ) ↑ 5 ) )