Theorem 3lexlogpow5ineq3

Description: Combined inequality chain for a specific power of the binary logarithm, proposed by Mario Carneiro. (Contributed by metakunt, 22-May-2024)

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

Proof

Step	Hyp	Ref	Expression
1		3lexlogpow5ineq3.1	|- ( ph -> X e. RR )
2		3lexlogpow5ineq3.2	|- ( ph -> 3 <_ X )
3		7re	|- 7 e. RR
4	3	a1i	|- ( ph -> 7 e. RR )
5		9re	|- 9 e. RR
6	5	a1i	|- ( ph -> 9 e. RR )
7		2re	|- 2 e. RR
8	7	a1i	|- ( ph -> 2 e. RR )
9		2pos	|- 0 < 2
10	9	a1i	|- ( ph -> 0 < 2 )
11		0red	|- ( ph -> 0 e. RR )
12		3re	|- 3 e. RR
13	12	a1i	|- ( ph -> 3 e. RR )
14		3pos	|- 0 < 3
15	14	a1i	|- ( ph -> 0 < 3 )
16	11 13 1 15 2	ltletrd	|- ( ph -> 0 < X )
17		1red	|- ( ph -> 1 e. RR )
18		1lt2	|- 1 < 2
19	18	a1i	|- ( ph -> 1 < 2 )
20	17 19	ltned	|- ( ph -> 1 =/= 2 )
21	20	necomd	|- ( ph -> 2 =/= 1 )
22	8 10 1 16 21	relogbcld	|- ( ph -> ( 2 logb X ) e. RR )
23		5nn0	|- 5 e. NN0
24	23	a1i	|- ( ph -> 5 e. NN0 )
25	22 24	reexpcld	|- ( ph -> ( ( 2 logb X ) ^ 5 ) e. RR )
26		7lt9	|- 7 < 9
27	26	a1i	|- ( ph -> 7 < 9 )
28	1 2	3lexlogpow5ineq4	|- ( ph -> 9 < ( ( 2 logb X ) ^ 5 ) )
29	4 6 25 27 28	lttrd	|- ( ph -> 7 < ( ( 2 logb X ) ^ 5 ) )