Metamath Proof Explorer

Theorem 3lexlogpow5ineq4

Description: Sharper logarithm inequality chain. (Contributed by metakunt, 21-Aug-2024)

Ref Expression
Hypotheses 3lexlogpow5ineq4.1 
|- ( ph -> X e. RR )
3lexlogpow5ineq4.2 
|- ( ph -> 3 <_ X )
Assertion 3lexlogpow5ineq4 
|- ( ph -> 9 < ( ( 2 logb X ) ^ 5 ) )

Proof

Step Hyp Ref Expression
1 3lexlogpow5ineq4.1 
 |-  ( ph -> X e. RR )
2 3lexlogpow5ineq4.2 
 |-  ( ph -> 3 <_ X )
3 9re 
 |-  9 e. RR
4 3 a1i 
 |-  ( ph -> 9 e. RR )
5 11nn 
 |-  ; 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 5nn0 
 |-  5 e. NN0
17 16 a1i 
 |-  ( ph -> 5 e. NN0 )
18 15 17 reexpcld 
 |-  ( ph -> ( ( ; 1 1 / 7 ) ^ 5 ) e. RR )
19 2re 
 |-  2 e. RR
20 19 a1i 
 |-  ( ph -> 2 e. RR )
21 2pos 
 |-  0 < 2
22 21 a1i 
 |-  ( ph -> 0 < 2 )
23 3re 
 |-  3 e. RR
24 23 a1i 
 |-  ( ph -> 3 e. RR )
25 3pos 
 |-  0 < 3
26 25 a1i 
 |-  ( ph -> 0 < 3 )
27 10 24 1 26 2 ltletrd 
 |-  ( ph -> 0 < X )
28 1red 
 |-  ( ph -> 1 e. RR )
29 1lt2 
 |-  1 < 2
30 29 a1i 
 |-  ( ph -> 1 < 2 )
31 28 30 ltned 
 |-  ( ph -> 1 =/= 2 )
32 31 necomd 
 |-  ( ph -> 2 =/= 1 )
33 20 22 1 27 32 relogbcld 
 |-  ( ph -> ( 2 logb X ) e. RR )
34 33 17 reexpcld 
 |-  ( ph -> ( ( 2 logb X ) ^ 5 ) e. RR )
35 3lexlogpow5ineq1 
 |-  9 < ( ( ; 1 1 / 7 ) ^ 5 )
36 35 a1i 
 |-  ( ph -> 9 < ( ( ; 1 1 / 7 ) ^ 5 ) )
37 1 2 3lexlogpow5ineq2 
 |-  ( ph -> ( ( ; 1 1 / 7 ) ^ 5 ) <_ ( ( 2 logb X ) ^ 5 ) )
38 4 18 34 36 37 ltletrd 
 |-  ( ph -> 9 < ( ( 2 logb X ) ^ 5 ) )