Metamath Proof Explorer

Theorem aks4d1p2

Description: Technical lemma for existence of non-divisor. (Contributed by metakunt, 27-Oct-2024)

Ref Expression
Hypotheses aks4d1p2.1 
|- ( ph -> N e. ( ZZ>= ` 3 ) )
aks4d1p2.2 
|- A = ( ( N ^ ( |_ ` ( 2 logb B ) ) ) x. prod_ k e. ( 1 ... ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) ( ( N ^ k ) - 1 ) )
aks4d1p2.3 
|- B = ( |^ ` ( ( 2 logb N ) ^ 5 ) )
Assertion aks4d1p2 
|- ( ph -> ( 2 ^ B ) <_ ( _lcm ` ( 1 ... B ) ) )

Proof

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