Metamath Proof Explorer

Theorem aks4d1p6

Description: The maximal prime power exponent is smaller than the binary logarithm floor of B . (Contributed by metakunt, 30-Oct-2024)

Ref Expression
Hypotheses aks4d1p6.1 
|- ( ph -> N e. ( ZZ>= ` 3 ) )
aks4d1p6.2 
|- A = ( ( N ^ ( |_ ` ( 2 logb B ) ) ) x. prod_ k e. ( 1 ... ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) ( ( N ^ k ) - 1 ) )
aks4d1p6.3 
|- B = ( |^ ` ( ( 2 logb N ) ^ 5 ) )
aks4d1p6.4 
|- R = inf ( { r e. ( 1 ... B ) | -. r || A } , RR , < )
aks4d1p6.5 
|- ( ph -> P e. Prime )
aks4d1p6.6 
|- ( ph -> P || R )
aks4d1p6.7 
|- K = ( P pCnt R )
Assertion aks4d1p6 
|- ( ph -> K <_ ( |_ ` ( 2 logb B ) ) )

Proof

Step Hyp Ref Expression
1 aks4d1p6.1 
 |-  ( ph -> N e. ( ZZ>= ` 3 ) )
2 aks4d1p6.2 
 |-  A = ( ( N ^ ( |_ ` ( 2 logb B ) ) ) x. prod_ k e. ( 1 ... ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) ( ( N ^ k ) - 1 ) )
3 aks4d1p6.3 
 |-  B = ( |^ ` ( ( 2 logb N ) ^ 5 ) )
4 aks4d1p6.4 
 |-  R = inf ( { r e. ( 1 ... B ) | -. r || A } , RR , < )
5 aks4d1p6.5 
 |-  ( ph -> P e. Prime )
6 aks4d1p6.6 
 |-  ( ph -> P || R )
7 aks4d1p6.7 
 |-  K = ( P pCnt R )
8 7 a1i 
 |-  ( ph -> K = ( P pCnt R ) )
9 1 2 3 4 aks4d1p4 
 |-  ( ph -> ( R e. ( 1 ... B ) /\ -. R || A ) )
10 9 simpld 
 |-  ( ph -> R e. ( 1 ... B ) )
11 elfznn 
 |-  ( R e. ( 1 ... B ) -> R e. NN )
12 10 11 syl 
 |-  ( ph -> R e. NN )
13 5 12 pccld 
 |-  ( ph -> ( P pCnt R ) e. NN0 )
14 8 13 eqeltrd 
 |-  ( ph -> K e. NN0 )
15 14 nn0zd 
 |-  ( ph -> K e. ZZ )
16 15 zred 
 |-  ( ph -> K e. RR )
17 prmnn 
 |-  ( P e. Prime -> P e. NN )
18 5 17 syl 
 |-  ( ph -> P e. NN )
19 18 nnred 
 |-  ( ph -> P e. RR )
20 18 nngt0d 
 |-  ( ph -> 0 < P )
21 3 a1i 
 |-  ( ph -> B = ( |^ ` ( ( 2 logb N ) ^ 5 ) ) )
22 2re 
 |-  2 e. RR
23 22 a1i 
 |-  ( ph -> 2 e. RR )
24 2pos 
 |-  0 < 2
25 24 a1i 
 |-  ( ph -> 0 < 2 )
26 eluzelz 
 |-  ( N e. ( ZZ>= ` 3 ) -> N e. ZZ )
27 1 26 syl 
 |-  ( ph -> N e. ZZ )
28 27 zred 
 |-  ( ph -> N e. RR )
29 0red 
 |-  ( ph -> 0 e. RR )
30 3re 
 |-  3 e. RR
31 30 a1i 
 |-  ( ph -> 3 e. RR )
32 3pos 
 |-  0 < 3
33 32 a1i 
 |-  ( ph -> 0 < 3 )
34 eluzle 
 |-  ( N e. ( ZZ>= ` 3 ) -> 3 <_ N )
35 1 34 syl 
 |-  ( ph -> 3 <_ N )
36 29 31 28 33 35 ltletrd 
 |-  ( ph -> 0 < N )
37 1red 
 |-  ( ph -> 1 e. RR )
38 1lt2 
 |-  1 < 2
39 38 a1i 
 |-  ( ph -> 1 < 2 )
40 37 39 ltned 
 |-  ( ph -> 1 =/= 2 )
41 40 necomd 
 |-  ( ph -> 2 =/= 1 )
42 23 25 28 36 41 relogbcld 
 |-  ( ph -> ( 2 logb N ) e. RR )
43 5nn0 
 |-  5 e. NN0
44 43 a1i 
 |-  ( ph -> 5 e. NN0 )
45 42 44 reexpcld 
 |-  ( ph -> ( ( 2 logb N ) ^ 5 ) e. RR )
46 ceilcl 
 |-  ( ( ( 2 logb N ) ^ 5 ) e. RR -> ( |^ ` ( ( 2 logb N ) ^ 5 ) ) e. ZZ )
47 45 46 syl 
 |-  ( ph -> ( |^ ` ( ( 2 logb N ) ^ 5 ) ) e. ZZ )
48 21 47 eqeltrd 
 |-  ( ph -> B e. ZZ )
49 48 zred 
 |-  ( ph -> B e. RR )
50 9re 
 |-  9 e. RR
51 50 a1i 
 |-  ( ph -> 9 e. RR )
52 9pos 
 |-  0 < 9
53 52 a1i 
 |-  ( ph -> 0 < 9 )
54 28 35 3lexlogpow5ineq4 
 |-  ( ph -> 9 < ( ( 2 logb N ) ^ 5 ) )
55 29 51 45 53 54 lttrd 
 |-  ( ph -> 0 < ( ( 2 logb N ) ^ 5 ) )
56 ceilge 
 |-  ( ( ( 2 logb N ) ^ 5 ) e. RR -> ( ( 2 logb N ) ^ 5 ) <_ ( |^ ` ( ( 2 logb N ) ^ 5 ) ) )
57 45 56 syl 
 |-  ( ph -> ( ( 2 logb N ) ^ 5 ) <_ ( |^ ` ( ( 2 logb N ) ^ 5 ) ) )
58 57 21 breqtrrd 
 |-  ( ph -> ( ( 2 logb N ) ^ 5 ) <_ B )
59 29 45 49 55 58 ltletrd 
 |-  ( ph -> 0 < B )
60 48 59 jca 
 |-  ( ph -> ( B e. ZZ /\ 0 < B ) )
61 elnnz 
 |-  ( B e. NN <-> ( B e. ZZ /\ 0 < B ) )
62 60 61 sylibr 
 |-  ( ph -> B e. NN )
63 62 nnred 
 |-  ( ph -> B e. RR )
64 62 nngt0d 
 |-  ( ph -> 0 < B )
65 2z 
 |-  2 e. ZZ
66 65 a1i 
 |-  ( ph -> 2 e. ZZ )
67 66 zred 
 |-  ( ph -> 2 e. RR )
68 prmuz2 
 |-  ( P e. Prime -> P e. ( ZZ>= ` 2 ) )
69 5 68 syl 
 |-  ( ph -> P e. ( ZZ>= ` 2 ) )
70 eluzle 
 |-  ( P e. ( ZZ>= ` 2 ) -> 2 <_ P )
71 69 70 syl 
 |-  ( ph -> 2 <_ P )
72 37 67 19 39 71 ltletrd 
 |-  ( ph -> 1 < P )
73 37 72 ltned 
 |-  ( ph -> 1 =/= P )
74 73 necomd 
 |-  ( ph -> P =/= 1 )
75 19 20 63 64 74 relogbcld 
 |-  ( ph -> ( P logb B ) e. RR )
76 67 25 63 64 41 relogbcld 
 |-  ( ph -> ( 2 logb B ) e. RR )
77 18 nnrpd 
 |-  ( ph -> P e. RR+ )
78 77 rpcnd 
 |-  ( ph -> P e. CC )
79 77 rpne0d 
 |-  ( ph -> P =/= 0 )
80 78 79 15 cxpexpzd 
 |-  ( ph -> ( P ^c K ) = ( P ^ K ) )
81 19 14 reexpcld 
 |-  ( ph -> ( P ^ K ) e. RR )
82 12 nnred 
 |-  ( ph -> R e. RR )
83 8 oveq2d 
 |-  ( ph -> ( P ^ K ) = ( P ^ ( P pCnt R ) ) )
84 pcdvds 
 |-  ( ( P e. Prime /\ R e. NN ) -> ( P ^ ( P pCnt R ) ) || R )
85 5 12 84 syl2anc 
 |-  ( ph -> ( P ^ ( P pCnt R ) ) || R )
86 18 nnzd 
 |-  ( ph -> P e. ZZ )
87 zexpcl 
 |-  ( ( P e. ZZ /\ ( P pCnt R ) e. NN0 ) -> ( P ^ ( P pCnt R ) ) e. ZZ )
88 86 13 87 syl2anc 
 |-  ( ph -> ( P ^ ( P pCnt R ) ) e. ZZ )
89 dvdsle 
 |-  ( ( ( P ^ ( P pCnt R ) ) e. ZZ /\ R e. NN ) -> ( ( P ^ ( P pCnt R ) ) || R -> ( P ^ ( P pCnt R ) ) <_ R ) )
90 88 12 89 syl2anc 
 |-  ( ph -> ( ( P ^ ( P pCnt R ) ) || R -> ( P ^ ( P pCnt R ) ) <_ R ) )
91 85 90 mpd 
 |-  ( ph -> ( P ^ ( P pCnt R ) ) <_ R )
92 83 91 eqbrtrd 
 |-  ( ph -> ( P ^ K ) <_ R )
93 elfzle2 
 |-  ( R e. ( 1 ... B ) -> R <_ B )
94 10 93 syl 
 |-  ( ph -> R <_ B )
95 81 82 63 92 94 letrd 
 |-  ( ph -> ( P ^ K ) <_ B )
96 79 74 nelprd 
 |-  ( ph -> -. P e. { 0 , 1 } )
97 78 96 eldifd 
 |-  ( ph -> P e. ( CC \ { 0 , 1 } ) )
98 63 recnd 
 |-  ( ph -> B e. CC )
99 29 64 ltned 
 |-  ( ph -> 0 =/= B )
100 99 necomd 
 |-  ( ph -> B =/= 0 )
101 100 neneqd 
 |-  ( ph -> -. B = 0 )
102 elsng 
 |-  ( B e. NN -> ( B e. { 0 } <-> B = 0 ) )
103 62 102 syl 
 |-  ( ph -> ( B e. { 0 } <-> B = 0 ) )
104 101 103 mtbird 
 |-  ( ph -> -. B e. { 0 } )
105 98 104 eldifd 
 |-  ( ph -> B e. ( CC \ { 0 } ) )
106 cxplogb 
 |-  ( ( P e. ( CC \ { 0 , 1 } ) /\ B e. ( CC \ { 0 } ) ) -> ( P ^c ( P logb B ) ) = B )
107 97 105 106 syl2anc 
 |-  ( ph -> ( P ^c ( P logb B ) ) = B )
108 95 107 breqtrrd 
 |-  ( ph -> ( P ^ K ) <_ ( P ^c ( P logb B ) ) )
109 80 108 eqbrtrd 
 |-  ( ph -> ( P ^c K ) <_ ( P ^c ( P logb B ) ) )
110 77 rpred 
 |-  ( ph -> P e. RR )
111 37 67 110 39 71 ltletrd 
 |-  ( ph -> 1 < P )
112 110 111 16 75 cxpled 
 |-  ( ph -> ( K <_ ( P logb B ) <-> ( P ^c K ) <_ ( P ^c ( P logb B ) ) ) )
113 109 112 mpbird 
 |-  ( ph -> K <_ ( P logb B ) )
114 23 39 rplogcld 
 |-  ( ph -> ( log ` 2 ) e. RR+ )
115 110 111 rplogcld 
 |-  ( ph -> ( log ` P ) e. RR+ )
116 62 nnrpd 
 |-  ( ph -> B e. RR+ )
117 116 relogcld 
 |-  ( ph -> ( log ` B ) e. RR )
118 62 nnge1d 
 |-  ( ph -> 1 <_ B )
119 63 118 logge0d 
 |-  ( ph -> 0 <_ ( log ` B ) )
120 2rp 
 |-  2 e. RR+
121 120 a1i 
 |-  ( ph -> 2 e. RR+ )
122 121 77 logled 
 |-  ( ph -> ( 2 <_ P <-> ( log ` 2 ) <_ ( log ` P ) ) )
123 71 122 mpbid 
 |-  ( ph -> ( log ` 2 ) <_ ( log ` P ) )
124 114 115 117 119 123 lediv2ad 
 |-  ( ph -> ( ( log ` B ) / ( log ` P ) ) <_ ( ( log ` B ) / ( log ` 2 ) ) )
125 relogbval 
 |-  ( ( P e. ( ZZ>= ` 2 ) /\ B e. RR+ ) -> ( P logb B ) = ( ( log ` B ) / ( log ` P ) ) )
126 69 116 125 syl2anc 
 |-  ( ph -> ( P logb B ) = ( ( log ` B ) / ( log ` P ) ) )
127 126 eqcomd 
 |-  ( ph -> ( ( log ` B ) / ( log ` P ) ) = ( P logb B ) )
128 66 uzidd 
 |-  ( ph -> 2 e. ( ZZ>= ` 2 ) )
129 relogbval 
 |-  ( ( 2 e. ( ZZ>= ` 2 ) /\ B e. RR+ ) -> ( 2 logb B ) = ( ( log ` B ) / ( log ` 2 ) ) )
130 128 116 129 syl2anc 
 |-  ( ph -> ( 2 logb B ) = ( ( log ` B ) / ( log ` 2 ) ) )
131 130 eqcomd 
 |-  ( ph -> ( ( log ` B ) / ( log ` 2 ) ) = ( 2 logb B ) )
132 124 127 131 3brtr3d 
 |-  ( ph -> ( P logb B ) <_ ( 2 logb B ) )
133 16 75 76 113 132 letrd 
 |-  ( ph -> K <_ ( 2 logb B ) )
134 flge 
 |-  ( ( ( 2 logb B ) e. RR /\ K e. ZZ ) -> ( K <_ ( 2 logb B ) <-> K <_ ( |_ ` ( 2 logb B ) ) ) )
135 76 15 134 syl2anc 
 |-  ( ph -> ( K <_ ( 2 logb B ) <-> K <_ ( |_ ` ( 2 logb B ) ) ) )
136 133 135 mpbid 
 |-  ( ph -> K <_ ( |_ ` ( 2 logb B ) ) )