Metamath Proof Explorer

Theorem aks4d1p1p3

Description: Bound of a ceiling of the binary logarithm to the fifth power. (Contributed by metakunt, 19-Aug-2024)

Ref Expression
Hypotheses aks4d1p1p3.1 
|- ( ph -> N e. NN )
aks4d1p1p3.2 
|- B = ( |^ ` ( ( 2 logb N ) ^ 5 ) )
aks4d1p1p3.3 
|- ( ph -> 3 <_ N )
Assertion aks4d1p1p3 
|- ( ph -> ( N ^c ( |_ ` ( 2 logb B ) ) ) < ( N ^c ( 2 logb ( ( ( 2 logb N ) ^ 5 ) + 1 ) ) ) )

Proof

Step Hyp Ref Expression
1 aks4d1p1p3.1 
 |-  ( ph -> N e. NN )
2 aks4d1p1p3.2 
 |-  B = ( |^ ` ( ( 2 logb N ) ^ 5 ) )
3 aks4d1p1p3.3 
 |-  ( ph -> 3 <_ N )
4 2re 
 |-  2 e. RR
5 4 a1i 
 |-  ( ph -> 2 e. RR )
6 2pos 
 |-  0 < 2
7 6 a1i 
 |-  ( ph -> 0 < 2 )
8 1 nnred 
 |-  ( ph -> N e. RR )
9 1 nngt0d 
 |-  ( ph -> 0 < N )
10 1red 
 |-  ( ph -> 1 e. RR )
11 1lt2 
 |-  1 < 2
12 11 a1i 
 |-  ( ph -> 1 < 2 )
13 10 12 ltned 
 |-  ( ph -> 1 =/= 2 )
14 13 necomd 
 |-  ( ph -> 2 =/= 1 )
15 5 7 8 9 14 relogbcld 
 |-  ( ph -> ( 2 logb N ) e. RR )
16 5nn0 
 |-  5 e. NN0
17 16 a1i 
 |-  ( ph -> 5 e. NN0 )
18 15 17 reexpcld 
 |-  ( ph -> ( ( 2 logb N ) ^ 5 ) e. RR )
19 ceilcl 
 |-  ( ( ( 2 logb N ) ^ 5 ) e. RR -> ( |^ ` ( ( 2 logb N ) ^ 5 ) ) e. ZZ )
20 18 19 syl 
 |-  ( ph -> ( |^ ` ( ( 2 logb N ) ^ 5 ) ) e. ZZ )
21 20 zred 
 |-  ( ph -> ( |^ ` ( ( 2 logb N ) ^ 5 ) ) e. RR )
22 2 a1i 
 |-  ( ph -> B = ( |^ ` ( ( 2 logb N ) ^ 5 ) ) )
23 22 eleq1d 
 |-  ( ph -> ( B e. RR <-> ( |^ ` ( ( 2 logb N ) ^ 5 ) ) e. RR ) )
24 21 23 mpbird 
 |-  ( ph -> B e. RR )
25 0red 
 |-  ( ph -> 0 e. RR )
26 7re 
 |-  7 e. RR
27 26 a1i 
 |-  ( ph -> 7 e. RR )
28 7pos 
 |-  0 < 7
29 28 a1i 
 |-  ( ph -> 0 < 7 )
30 8 3 3lexlogpow5ineq3 
 |-  ( ph -> 7 < ( ( 2 logb N ) ^ 5 ) )
31 ceilge 
 |-  ( ( ( 2 logb N ) ^ 5 ) e. RR -> ( ( 2 logb N ) ^ 5 ) <_ ( |^ ` ( ( 2 logb N ) ^ 5 ) ) )
32 18 31 syl 
 |-  ( ph -> ( ( 2 logb N ) ^ 5 ) <_ ( |^ ` ( ( 2 logb N ) ^ 5 ) ) )
33 27 18 21 30 32 ltletrd 
 |-  ( ph -> 7 < ( |^ ` ( ( 2 logb N ) ^ 5 ) ) )
34 22 eqcomd 
 |-  ( ph -> ( |^ ` ( ( 2 logb N ) ^ 5 ) ) = B )
35 33 34 breqtrd 
 |-  ( ph -> 7 < B )
36 25 27 24 29 35 lttrd 
 |-  ( ph -> 0 < B )
37 5 7 24 36 14 relogbcld 
 |-  ( ph -> ( 2 logb B ) e. RR )
38 37 flcld 
 |-  ( ph -> ( |_ ` ( 2 logb B ) ) e. ZZ )
39 38 zred 
 |-  ( ph -> ( |_ ` ( 2 logb B ) ) e. RR )
40 18 10 readdcld 
 |-  ( ph -> ( ( ( 2 logb N ) ^ 5 ) + 1 ) e. RR )
41 18 ltp1d 
 |-  ( ph -> ( ( 2 logb N ) ^ 5 ) < ( ( ( 2 logb N ) ^ 5 ) + 1 ) )
42 27 18 40 30 41 lttrd 
 |-  ( ph -> 7 < ( ( ( 2 logb N ) ^ 5 ) + 1 ) )
43 25 27 40 29 42 lttrd 
 |-  ( ph -> 0 < ( ( ( 2 logb N ) ^ 5 ) + 1 ) )
44 5 7 40 43 14 relogbcld 
 |-  ( ph -> ( 2 logb ( ( ( 2 logb N ) ^ 5 ) + 1 ) ) e. RR )
45 flle 
 |-  ( ( 2 logb B ) e. RR -> ( |_ ` ( 2 logb B ) ) <_ ( 2 logb B ) )
46 37 45 syl 
 |-  ( ph -> ( |_ ` ( 2 logb B ) ) <_ ( 2 logb B ) )
47 ceilm1lt 
 |-  ( ( ( 2 logb N ) ^ 5 ) e. RR -> ( ( |^ ` ( ( 2 logb N ) ^ 5 ) ) - 1 ) < ( ( 2 logb N ) ^ 5 ) )
48 18 47 syl 
 |-  ( ph -> ( ( |^ ` ( ( 2 logb N ) ^ 5 ) ) - 1 ) < ( ( 2 logb N ) ^ 5 ) )
49 21 10 18 ltsubaddd 
 |-  ( ph -> ( ( ( |^ ` ( ( 2 logb N ) ^ 5 ) ) - 1 ) < ( ( 2 logb N ) ^ 5 ) <-> ( |^ ` ( ( 2 logb N ) ^ 5 ) ) < ( ( ( 2 logb N ) ^ 5 ) + 1 ) ) )
50 48 49 mpbid 
 |-  ( ph -> ( |^ ` ( ( 2 logb N ) ^ 5 ) ) < ( ( ( 2 logb N ) ^ 5 ) + 1 ) )
51 22 50 eqbrtrd 
 |-  ( ph -> B < ( ( ( 2 logb N ) ^ 5 ) + 1 ) )
52 2z 
 |-  2 e. ZZ
53 52 a1i 
 |-  ( ph -> 2 e. ZZ )
54 53 uzidd 
 |-  ( ph -> 2 e. ( ZZ>= ` 2 ) )
55 24 36 elrpd 
 |-  ( ph -> B e. RR+ )
56 40 43 elrpd 
 |-  ( ph -> ( ( ( 2 logb N ) ^ 5 ) + 1 ) e. RR+ )
57 logblt 
 |-  ( ( 2 e. ( ZZ>= ` 2 ) /\ B e. RR+ /\ ( ( ( 2 logb N ) ^ 5 ) + 1 ) e. RR+ ) -> ( B < ( ( ( 2 logb N ) ^ 5 ) + 1 ) <-> ( 2 logb B ) < ( 2 logb ( ( ( 2 logb N ) ^ 5 ) + 1 ) ) ) )
58 54 55 56 57 syl3anc 
 |-  ( ph -> ( B < ( ( ( 2 logb N ) ^ 5 ) + 1 ) <-> ( 2 logb B ) < ( 2 logb ( ( ( 2 logb N ) ^ 5 ) + 1 ) ) ) )
59 51 58 mpbid 
 |-  ( ph -> ( 2 logb B ) < ( 2 logb ( ( ( 2 logb N ) ^ 5 ) + 1 ) ) )
60 39 37 44 46 59 lelttrd 
 |-  ( ph -> ( |_ ` ( 2 logb B ) ) < ( 2 logb ( ( ( 2 logb N ) ^ 5 ) + 1 ) ) )
61 3re 
 |-  3 e. RR
62 61 a1i 
 |-  ( ph -> 3 e. RR )
63 1lt3 
 |-  1 < 3
64 63 a1i 
 |-  ( ph -> 1 < 3 )
65 10 62 8 64 3 ltletrd 
 |-  ( ph -> 1 < N )
66 8 65 39 44 cxpltd 
 |-  ( ph -> ( ( |_ ` ( 2 logb B ) ) < ( 2 logb ( ( ( 2 logb N ) ^ 5 ) + 1 ) ) <-> ( N ^c ( |_ ` ( 2 logb B ) ) ) < ( N ^c ( 2 logb ( ( ( 2 logb N ) ^ 5 ) + 1 ) ) ) ) )
67 60 66 mpbid 
 |-  ( ph -> ( N ^c ( |_ ` ( 2 logb B ) ) ) < ( N ^c ( 2 logb ( ( ( 2 logb N ) ^ 5 ) + 1 ) ) ) )