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 
|- ( ph -> X e. RR )
3lexlogpow5ineq2.2 
|- ( ph -> 3 <_ X )
Assertion 3lexlogpow5ineq2 
|- ( ph -> ( ( ; 1 1 / 7 ) ^ 5 ) <_ ( ( 2 logb X ) ^ 5 ) )

Proof

Step Hyp Ref Expression
1 3lexlogpow5ineq2.1 
 |-  ( ph -> X e. RR )
2 3lexlogpow5ineq2.2 
 |-  ( ph -> 3 <_ X )
3 1nn0 
 |-  1 e. NN0
4 1nn 
 |-  1 e. NN
5 3 4 decnncl 
 |-  ; 1 1 e. NN
6 5 a1i 
 |-  ( ph -> ; 1 1 e. NN )
7 6 nnred 
 |-  ( ph -> ; 1 1 e. RR )
8 7re 
 |-  7 e. RR
9 8 a1i 
 |-  ( ph -> 7 e. RR )
10 0red 
 |-  ( ph -> 0 e. RR )
11 7pos 
 |-  0 < 7
12 11 a1i 
 |-  ( ph -> 0 < 7 )
13 10 12 ltned 
 |-  ( ph -> 0 =/= 7 )
14 13 necomd 
 |-  ( ph -> 7 =/= 0 )
15 7 9 14 redivcld 
 |-  ( ph -> ( ; 1 1 / 7 ) e. RR )
16 2re 
 |-  2 e. RR
17 16 a1i 
 |-  ( ph -> 2 e. RR )
18 2pos 
 |-  0 < 2
19 18 a1i 
 |-  ( ph -> 0 < 2 )
20 3re 
 |-  3 e. RR
21 20 a1i 
 |-  ( ph -> 3 e. RR )
22 3pos 
 |-  0 < 3
23 22 a1i 
 |-  ( ph -> 0 < 3 )
24 10 21 1 23 2 ltletrd 
 |-  ( ph -> 0 < X )
25 1red 
 |-  ( ph -> 1 e. RR )
26 1lt2 
 |-  1 < 2
27 26 a1i 
 |-  ( ph -> 1 < 2 )
28 25 27 ltned 
 |-  ( ph -> 1 =/= 2 )
29 28 necomd 
 |-  ( ph -> 2 =/= 1 )
30 17 19 1 24 29 relogbcld 
 |-  ( ph -> ( 2 logb X ) e. RR )
31 5nn0 
 |-  5 e. NN0
32 31 a1i 
 |-  ( ph -> 5 e. NN0 )
33 7nn 
 |-  7 e. NN
34 33 a1i 
 |-  ( ph -> 7 e. NN )
35 34 nnrpd 
 |-  ( ph -> 7 e. RR+ )
36 0nn0 
 |-  0 e. NN0
37 tru 
 |-  T.
38 0red 
 |-  ( T. -> 0 e. RR )
39 9re 
 |-  9 e. RR
40 39 a1i 
 |-  ( T. -> 9 e. RR )
41 9pos 
 |-  0 < 9
42 41 a1i 
 |-  ( T. -> 0 < 9 )
43 38 40 42 ltled 
 |-  ( T. -> 0 <_ 9 )
44 37 43 ax-mp 
 |-  0 <_ 9
45 4 3 36 44 declei 
 |-  0 <_ ; 1 1
46 45 a1i 
 |-  ( ph -> 0 <_ ; 1 1 )
47 7 35 46 divge0d 
 |-  ( ph -> 0 <_ ( ; 1 1 / 7 ) )
48 17 19 21 23 29 relogbcld 
 |-  ( ph -> ( 2 logb 3 ) e. RR )
49 2exp11 
 |-  ( 2 ^ ; 1 1 ) = ; ; ; 2 0 4 8
50 49 eqcomi 
 |-  ; ; ; 2 0 4 8 = ( 2 ^ ; 1 1 )
51 50 a1i 
 |-  ( ph -> ; ; ; 2 0 4 8 = ( 2 ^ ; 1 1 ) )
52 51 oveq2d 
 |-  ( ph -> ( 2 logb ; ; ; 2 0 4 8 ) = ( 2 logb ( 2 ^ ; 1 1 ) ) )
53 17 19 elrpd 
 |-  ( ph -> 2 e. RR+ )
54 6 nnzd 
 |-  ( ph -> ; 1 1 e. ZZ )
55 53 29 54 relogbexpd 
 |-  ( ph -> ( 2 logb ( 2 ^ ; 1 1 ) ) = ; 1 1 )
56 52 55 eqtrd 
 |-  ( ph -> ( 2 logb ; ; ; 2 0 4 8 ) = ; 1 1 )
57 56 eqcomd 
 |-  ( ph -> ; 1 1 = ( 2 logb ; ; ; 2 0 4 8 ) )
58 2z 
 |-  2 e. ZZ
59 58 a1i 
 |-  ( ph -> 2 e. ZZ )
60 17 leidd 
 |-  ( ph -> 2 <_ 2 )
61 2nn0 
 |-  2 e. NN0
62 61 36 deccl 
 |-  ; 2 0 e. NN0
63 4nn0 
 |-  4 e. NN0
64 62 63 deccl 
 |-  ; ; 2 0 4 e. NN0
65 8nn 
 |-  8 e. NN
66 64 65 decnncl 
 |-  ; ; ; 2 0 4 8 e. NN
67 66 a1i 
 |-  ( ph -> ; ; ; 2 0 4 8 e. NN )
68 67 nnred 
 |-  ( ph -> ; ; ; 2 0 4 8 e. RR )
69 4nn 
 |-  4 e. NN
70 62 69 decnncl 
 |-  ; ; 2 0 4 e. NN
71 8nn0 
 |-  8 e. NN0
72 70 71 36 44 decltdi 
 |-  0 < ; ; ; 2 0 4 8
73 72 a1i 
 |-  ( ph -> 0 < ; ; ; 2 0 4 8 )
74 61 3 deccl 
 |-  ; 2 1 e. NN0
75 74 71 deccl 
 |-  ; ; 2 1 8 e. NN0
76 75 33 decnncl 
 |-  ; ; ; 2 1 8 7 e. NN
77 76 a1i 
 |-  ( ph -> ; ; ; 2 1 8 7 e. NN )
78 77 nnred 
 |-  ( ph -> ; ; ; 2 1 8 7 e. RR )
79 74 65 decnncl 
 |-  ; ; 2 1 8 e. NN
80 7nn0 
 |-  7 e. NN0
81 79 80 36 44 decltdi 
 |-  0 < ; ; ; 2 1 8 7
82 81 a1i 
 |-  ( ph -> 0 < ; ; ; 2 1 8 7 )
83 8re 
 |-  8 e. RR
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 
 |-  ( ph -> ; ; ; 2 0 4 8 <_ ; ; ; 2 1 8 7 )
93 59 60 68 73 78 82 92 logblebd 
 |-  ( ph -> ( 2 logb ; ; ; 2 0 4 8 ) <_ ( 2 logb ; ; ; 2 1 8 7 ) )
94 57 93 eqbrtrd 
 |-  ( ph -> ; 1 1 <_ ( 2 logb ; ; ; 2 1 8 7 ) )
95 7 recnd 
 |-  ( ph -> ; 1 1 e. CC )
96 9 recnd 
 |-  ( ph -> 7 e. CC )
97 95 96 14 divcan1d 
 |-  ( ph -> ( ( ; 1 1 / 7 ) x. 7 ) = ; 1 1 )
98 97 eqcomd 
 |-  ( ph -> ; 1 1 = ( ( ; 1 1 / 7 ) x. 7 ) )
99 3exp7 
 |-  ( 3 ^ 7 ) = ; ; ; 2 1 8 7
100 99 eqcomi 
 |-  ; ; ; 2 1 8 7 = ( 3 ^ 7 )
101 100 a1i 
 |-  ( ph -> ; ; ; 2 1 8 7 = ( 3 ^ 7 ) )
102 101 oveq2d 
 |-  ( ph -> ( 2 logb ; ; ; 2 1 8 7 ) = ( 2 logb ( 3 ^ 7 ) ) )
103 21 23 elrpd 
 |-  ( ph -> 3 e. RR+ )
104 34 nnzd 
 |-  ( ph -> 7 e. ZZ )
105 53 29 103 104 relogbzexpd 
 |-  ( ph -> ( 2 logb ( 3 ^ 7 ) ) = ( 7 x. ( 2 logb 3 ) ) )
106 102 105 eqtrd 
 |-  ( ph -> ( 2 logb ; ; ; 2 1 8 7 ) = ( 7 x. ( 2 logb 3 ) ) )
107 48 recnd 
 |-  ( ph -> ( 2 logb 3 ) e. CC )
108 96 107 mulcomd 
 |-  ( ph -> ( 7 x. ( 2 logb 3 ) ) = ( ( 2 logb 3 ) x. 7 ) )
109 106 108 eqtrd 
 |-  ( ph -> ( 2 logb ; ; ; 2 1 8 7 ) = ( ( 2 logb 3 ) x. 7 ) )
110 94 98 109 3brtr3d 
 |-  ( ph -> ( ( ; 1 1 / 7 ) x. 7 ) <_ ( ( 2 logb 3 ) x. 7 ) )
111 15 48 35 lemul1d 
 |-  ( ph -> ( ( ; 1 1 / 7 ) <_ ( 2 logb 3 ) <-> ( ( ; 1 1 / 7 ) x. 7 ) <_ ( ( 2 logb 3 ) x. 7 ) ) )
112 110 111 mpbird 
 |-  ( ph -> ( ; 1 1 / 7 ) <_ ( 2 logb 3 ) )
113 59 60 21 23 1 24 2 logblebd 
 |-  ( ph -> ( 2 logb 3 ) <_ ( 2 logb X ) )
114 15 48 30 112 113 letrd 
 |-  ( ph -> ( ; 1 1 / 7 ) <_ ( 2 logb X ) )
115 15 30 32 47 114 leexp1ad 
 |-  ( ph -> ( ( ; 1 1 / 7 ) ^ 5 ) <_ ( ( 2 logb X ) ^ 5 ) )