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