Metamath Proof Explorer

Theorem aks4d1lem1

Description: Technical lemma to reduce proof size. (Contributed by metakunt, 14-Nov-2024)

Ref Expression
Hypotheses aks4d1lem1.1 
|- ( ph -> N e. ( ZZ>= ` 3 ) )
aks4d1lem1.2 
|- B = ( |^ ` ( ( 2 logb N ) ^ 5 ) )
Assertion aks4d1lem1 
|- ( ph -> ( B e. NN /\ 9 < B ) )

Proof

Step Hyp Ref Expression
1 aks4d1lem1.1 
 |-  ( ph -> N e. ( ZZ>= ` 3 ) )
2 aks4d1lem1.2 
 |-  B = ( |^ ` ( ( 2 logb N ) ^ 5 ) )
3 2re 
 |-  2 e. RR
4 3 a1i 
 |-  ( ph -> 2 e. RR )
5 2pos 
 |-  0 < 2
6 5 a1i 
 |-  ( ph -> 0 < 2 )
7 eluzelz 
 |-  ( N e. ( ZZ>= ` 3 ) -> N e. ZZ )
8 1 7 syl 
 |-  ( ph -> N e. ZZ )
9 8 zred 
 |-  ( ph -> N e. RR )
10 0red 
 |-  ( ph -> 0 e. RR )
11 3re 
 |-  3 e. RR
12 11 a1i 
 |-  ( ph -> 3 e. RR )
13 3pos 
 |-  0 < 3
14 13 a1i 
 |-  ( ph -> 0 < 3 )
15 eluzle 
 |-  ( N e. ( ZZ>= ` 3 ) -> 3 <_ N )
16 1 15 syl 
 |-  ( ph -> 3 <_ N )
17 10 12 9 14 16 ltletrd 
 |-  ( ph -> 0 < N )
18 1red 
 |-  ( ph -> 1 e. RR )
19 1lt2 
 |-  1 < 2
20 19 a1i 
 |-  ( ph -> 1 < 2 )
21 18 20 ltned 
 |-  ( ph -> 1 =/= 2 )
22 21 necomd 
 |-  ( ph -> 2 =/= 1 )
23 4 6 9 17 22 relogbcld 
 |-  ( ph -> ( 2 logb N ) e. RR )
24 5nn0 
 |-  5 e. NN0
25 24 a1i 
 |-  ( ph -> 5 e. NN0 )
26 23 25 reexpcld 
 |-  ( ph -> ( ( 2 logb N ) ^ 5 ) e. RR )
27 26 ceilcld 
 |-  ( ph -> ( |^ ` ( ( 2 logb N ) ^ 5 ) ) e. ZZ )
28 9re 
 |-  9 e. RR
29 28 a1i 
 |-  ( ph -> 9 e. RR )
30 27 zred 
 |-  ( ph -> ( |^ ` ( ( 2 logb N ) ^ 5 ) ) e. RR )
31 9pos 
 |-  0 < 9
32 31 a1i 
 |-  ( ph -> 0 < 9 )
33 9 16 3lexlogpow5ineq4 
 |-  ( ph -> 9 < ( ( 2 logb N ) ^ 5 ) )
34 ceilge 
 |-  ( ( ( 2 logb N ) ^ 5 ) e. RR -> ( ( 2 logb N ) ^ 5 ) <_ ( |^ ` ( ( 2 logb N ) ^ 5 ) ) )
35 26 34 syl 
 |-  ( ph -> ( ( 2 logb N ) ^ 5 ) <_ ( |^ ` ( ( 2 logb N ) ^ 5 ) ) )
36 29 26 30 33 35 ltletrd 
 |-  ( ph -> 9 < ( |^ ` ( ( 2 logb N ) ^ 5 ) ) )
37 10 29 30 32 36 lttrd 
 |-  ( ph -> 0 < ( |^ ` ( ( 2 logb N ) ^ 5 ) ) )
38 27 37 jca 
 |-  ( ph -> ( ( |^ ` ( ( 2 logb N ) ^ 5 ) ) e. ZZ /\ 0 < ( |^ ` ( ( 2 logb N ) ^ 5 ) ) ) )
39 elnnz 
 |-  ( ( |^ ` ( ( 2 logb N ) ^ 5 ) ) e. NN <-> ( ( |^ ` ( ( 2 logb N ) ^ 5 ) ) e. ZZ /\ 0 < ( |^ ` ( ( 2 logb N ) ^ 5 ) ) ) )
40 38 39 sylibr 
 |-  ( ph -> ( |^ ` ( ( 2 logb N ) ^ 5 ) ) e. NN )
41 2 eleq1i 
 |-  ( B e. NN <-> ( |^ ` ( ( 2 logb N ) ^ 5 ) ) e. NN )
42 40 41 sylibr 
 |-  ( ph -> B e. NN )
43 2 a1i 
 |-  ( ph -> B = ( |^ ` ( ( 2 logb N ) ^ 5 ) ) )
44 36 43 breqtrrd 
 |-  ( ph -> 9 < B )
45 42 44 jca 
 |-  ( ph -> ( B e. NN /\ 9 < B ) )