Metamath Proof Explorer


Theorem 3lexlogpow5ineq2

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

Ref Expression
Hypotheses 3lexlogpow5ineq2.1 φ X
3lexlogpow5ineq2.2 φ 3 X
Assertion 3lexlogpow5ineq2 φ 11 7 5 log 2 X 5

Proof

Step Hyp Ref Expression
1 3lexlogpow5ineq2.1 φ X
2 3lexlogpow5ineq2.2 φ 3 X
3 1nn0 1 0
4 1nn 1
5 3 4 decnncl 11
6 5 a1i φ 11
7 6 nnred φ 11
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 φ 11 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 < X
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 φ log 2 X
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 11
46 45 a1i φ 0 11
47 7 35 46 divge0d φ 0 11 7
48 17 19 21 23 29 relogbcld φ log 2 3
49 2exp11 2 11 = 2048
50 49 eqcomi 2048 = 2 11
51 50 a1i φ 2048 = 2 11
52 51 oveq2d φ log 2 2048 = log 2 2 11
53 17 19 elrpd φ 2 +
54 6 nnzd φ 11
55 53 29 54 relogbexpd φ log 2 2 11 = 11
56 52 55 eqtrd φ log 2 2048 = 11
57 56 eqcomd φ 11 = log 2 2048
58 2z 2
59 58 a1i φ 2
60 17 leidd φ 2 2
61 2nn0 2 0
62 61 36 deccl 20 0
63 4nn0 4 0
64 62 63 deccl 204 0
65 8nn 8
66 64 65 decnncl 2048
67 66 a1i φ 2048
68 67 nnred φ 2048
69 4nn 4
70 62 69 decnncl 204
71 8nn0 8 0
72 70 71 36 44 decltdi 0 < 2048
73 72 a1i φ 0 < 2048
74 61 3 deccl 21 0
75 74 71 deccl 218 0
76 75 33 decnncl 2187
77 76 a1i φ 2187
78 77 nnred φ 2187
79 74 65 decnncl 218
80 7nn0 7 0
81 79 80 36 44 decltdi 0 < 2187
82 81 a1i φ 0 < 2187
83 8re 8
84 83 3 nn0addge1i 8 8 + 1
85 8p1e9 8 + 1 = 9
86 84 85 breqtri 8 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 2187
92 91 a1i φ 2048 2187
93 59 60 68 73 78 82 92 logblebd φ log 2 2048 log 2 2187
94 57 93 eqbrtrd φ 11 log 2 2187
95 7 recnd φ 11
96 9 recnd φ 7
97 95 96 14 divcan1d φ 11 7 7 = 11
98 97 eqcomd φ 11 = 11 7 7
99 3exp7 3 7 = 2187
100 99 eqcomi 2187 = 3 7
101 100 a1i φ 2187 = 3 7
102 101 oveq2d φ log 2 2187 = log 2 3 7
103 21 23 elrpd φ 3 +
104 34 nnzd φ 7
105 53 29 103 104 relogbzexpd φ log 2 3 7 = 7 log 2 3
106 102 105 eqtrd φ log 2 2187 = 7 log 2 3
107 48 recnd φ log 2 3
108 96 107 mulcomd φ 7 log 2 3 = log 2 3 7
109 106 108 eqtrd φ log 2 2187 = log 2 3 7
110 94 98 109 3brtr3d φ 11 7 7 log 2 3 7
111 15 48 35 lemul1d φ 11 7 log 2 3 11 7 7 log 2 3 7
112 110 111 mpbird φ 11 7 log 2 3
113 59 60 21 23 1 24 2 logblebd φ log 2 3 log 2 X
114 15 48 30 112 113 letrd φ 11 7 log 2 X
115 15 30 32 47 114 leexp1ad φ 11 7 5 log 2 X 5