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 ⊢ ( 𝜑 → 𝑁 ∈ ( ℤ≥ ‘ 3 ) )
aks4d1p6.2 ⊢ 𝐴 = ( ( 𝑁 ↑ ( ⌊ ‘ ( 2 logb 𝐵 ) ) ) · ∏ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ( ( 𝑁 ↑ 𝑘 ) − 1 ) )
aks4d1p6.3 ⊢ 𝐵 = ( ⌈ ‘ ( ( 2 logb 𝑁 ) ↑ 5 ) )
aks4d1p6.4 ⊢ 𝑅 = inf ( { 𝑟 ∈ ( 1 ... 𝐵 ) ∣ ¬ 𝑟 ∥ 𝐴 } , ℝ , < )
aks4d1p6.5 ⊢ ( 𝜑 → 𝑃 ∈ ℙ )
aks4d1p6.6 ⊢ ( 𝜑 → 𝑃 ∥ 𝑅 )
aks4d1p6.7 ⊢ 𝐾 = ( 𝑃 pCnt 𝑅 )
Assertion aks4d1p6 ( 𝜑 → 𝐾 ≤ ( ⌊ ‘ ( 2 logb 𝐵 ) ) )

Proof

Step Hyp Ref Expression
1 aks4d1p6.1 ⊢ ( 𝜑 → 𝑁 ∈ ( ℤ≥ ‘ 3 ) )
2 aks4d1p6.2 ⊢ 𝐴 = ( ( 𝑁 ↑ ( ⌊ ‘ ( 2 logb 𝐵 ) ) ) · ∏ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ( ( 𝑁 ↑ 𝑘 ) − 1 ) )
3 aks4d1p6.3 ⊢ 𝐵 = ( ⌈ ‘ ( ( 2 logb 𝑁 ) ↑ 5 ) )
4 aks4d1p6.4 ⊢ 𝑅 = inf ( { 𝑟 ∈ ( 1 ... 𝐵 ) ∣ ¬ 𝑟 ∥ 𝐴 } , ℝ , < )
5 aks4d1p6.5 ⊢ ( 𝜑 → 𝑃 ∈ ℙ )
6 aks4d1p6.6 ⊢ ( 𝜑 → 𝑃 ∥ 𝑅 )
7 aks4d1p6.7 ⊢ 𝐾 = ( 𝑃 pCnt 𝑅 )
8 7 a1i ⊢ ( 𝜑 → 𝐾 = ( 𝑃 pCnt 𝑅 ) )
9 1 2 3 4 aks4d1p4 ⊢ ( 𝜑 → ( 𝑅 ∈ ( 1 ... 𝐵 ) ∧ ¬ 𝑅 ∥ 𝐴 ) )
10 9 simpld ⊢ ( 𝜑 → 𝑅 ∈ ( 1 ... 𝐵 ) )
11 elfznn ⊢ ( 𝑅 ∈ ( 1 ... 𝐵 ) → 𝑅 ∈ ℕ )
12 10 11 syl ⊢ ( 𝜑 → 𝑅 ∈ ℕ )
13 5 12 pccld ⊢ ( 𝜑 → ( 𝑃 pCnt 𝑅 ) ∈ ℕ0 )
14 8 13 eqeltrd ⊢ ( 𝜑 → 𝐾 ∈ ℕ0 )
15 14 nn0zd ⊢ ( 𝜑 → 𝐾 ∈ ℤ )
16 15 zred ⊢ ( 𝜑 → 𝐾 ∈ ℝ )
17 prmnn ⊢ ( 𝑃 ∈ ℙ → 𝑃 ∈ ℕ )
18 5 17 syl ⊢ ( 𝜑 → 𝑃 ∈ ℕ )
19 18 nnred ⊢ ( 𝜑 → 𝑃 ∈ ℝ )
20 18 nngt0d ⊢ ( 𝜑 → 0 < 𝑃 )
21 3 a1i ⊢ ( 𝜑 → 𝐵 = ( ⌈ ‘ ( ( 2 logb 𝑁 ) ↑ 5 ) ) )
22 2re ⊢ 2 ∈ ℝ
23 22 a1i ⊢ ( 𝜑 → 2 ∈ ℝ )
24 2pos ⊢ 0 < 2
25 24 a1i ⊢ ( 𝜑 → 0 < 2 )
26 eluzelz ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → 𝑁 ∈ ℤ )
27 1 26 syl ⊢ ( 𝜑 → 𝑁 ∈ ℤ )
28 27 zred ⊢ ( 𝜑 → 𝑁 ∈ ℝ )
29 0red ⊢ ( 𝜑 → 0 ∈ ℝ )
30 3re ⊢ 3 ∈ ℝ
31 30 a1i ⊢ ( 𝜑 → 3 ∈ ℝ )
32 3pos ⊢ 0 < 3
33 32 a1i ⊢ ( 𝜑 → 0 < 3 )
34 eluzle ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → 3 ≤ 𝑁 )
35 1 34 syl ⊢ ( 𝜑 → 3 ≤ 𝑁 )
36 29 31 28 33 35 ltletrd ⊢ ( 𝜑 → 0 < 𝑁 )
37 1red ⊢ ( 𝜑 → 1 ∈ ℝ )
38 1lt2 ⊢ 1 < 2
39 38 a1i ⊢ ( 𝜑 → 1 < 2 )
40 37 39 ltned ⊢ ( 𝜑 → 1 ≠ 2 )
41 40 necomd ⊢ ( 𝜑 → 2 ≠ 1 )
42 23 25 28 36 41 relogbcld ⊢ ( 𝜑 → ( 2 logb 𝑁 ) ∈ ℝ )
43 5nn0 ⊢ 5 ∈ ℕ0
44 43 a1i ⊢ ( 𝜑 → 5 ∈ ℕ0 )
45 42 44 reexpcld ⊢ ( 𝜑 → ( ( 2 logb 𝑁 ) ↑ 5 ) ∈ ℝ )
46 ceilcl ⊢ ( ( ( 2 logb 𝑁 ) ↑ 5 ) ∈ ℝ → ( ⌈ ‘ ( ( 2 logb 𝑁 ) ↑ 5 ) ) ∈ ℤ )
47 45 46 syl ⊢ ( 𝜑 → ( ⌈ ‘ ( ( 2 logb 𝑁 ) ↑ 5 ) ) ∈ ℤ )
48 21 47 eqeltrd ⊢ ( 𝜑 → 𝐵 ∈ ℤ )
49 48 zred ⊢ ( 𝜑 → 𝐵 ∈ ℝ )
50 9re ⊢ 9 ∈ ℝ
51 50 a1i ⊢ ( 𝜑 → 9 ∈ ℝ )
52 9pos ⊢ 0 < 9
53 52 a1i ⊢ ( 𝜑 → 0 < 9 )
54 28 35 3lexlogpow5ineq4 ⊢ ( 𝜑 → 9 < ( ( 2 logb 𝑁 ) ↑ 5 ) )
55 29 51 45 53 54 lttrd ⊢ ( 𝜑 → 0 < ( ( 2 logb 𝑁 ) ↑ 5 ) )
56 ceilge ⊢ ( ( ( 2 logb 𝑁 ) ↑ 5 ) ∈ ℝ → ( ( 2 logb 𝑁 ) ↑ 5 ) ≤ ( ⌈ ‘ ( ( 2 logb 𝑁 ) ↑ 5 ) ) )
57 45 56 syl ⊢ ( 𝜑 → ( ( 2 logb 𝑁 ) ↑ 5 ) ≤ ( ⌈ ‘ ( ( 2 logb 𝑁 ) ↑ 5 ) ) )
58 57 21 breqtrrd ⊢ ( 𝜑 → ( ( 2 logb 𝑁 ) ↑ 5 ) ≤ 𝐵 )
59 29 45 49 55 58 ltletrd ⊢ ( 𝜑 → 0 < 𝐵 )
60 48 59 jca ⊢ ( 𝜑 → ( 𝐵 ∈ ℤ ∧ 0 < 𝐵 ) )
61 elnnz ⊢ ( 𝐵 ∈ ℕ ↔ ( 𝐵 ∈ ℤ ∧ 0 < 𝐵 ) )
62 60 61 sylibr ⊢ ( 𝜑 → 𝐵 ∈ ℕ )
63 62 nnred ⊢ ( 𝜑 → 𝐵 ∈ ℝ )
64 62 nngt0d ⊢ ( 𝜑 → 0 < 𝐵 )
65 2z ⊢ 2 ∈ ℤ
66 65 a1i ⊢ ( 𝜑 → 2 ∈ ℤ )
67 66 zred ⊢ ( 𝜑 → 2 ∈ ℝ )
68 prmuz2 ⊢ ( 𝑃 ∈ ℙ → 𝑃 ∈ ( ℤ≥ ‘ 2 ) )
69 5 68 syl ⊢ ( 𝜑 → 𝑃 ∈ ( ℤ≥ ‘ 2 ) )
70 eluzle ⊢ ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) → 2 ≤ 𝑃 )
71 69 70 syl ⊢ ( 𝜑 → 2 ≤ 𝑃 )
72 37 67 19 39 71 ltletrd ⊢ ( 𝜑 → 1 < 𝑃 )
73 37 72 ltned ⊢ ( 𝜑 → 1 ≠ 𝑃 )
74 73 necomd ⊢ ( 𝜑 → 𝑃 ≠ 1 )
75 19 20 63 64 74 relogbcld ⊢ ( 𝜑 → ( 𝑃 logb 𝐵 ) ∈ ℝ )
76 67 25 63 64 41 relogbcld ⊢ ( 𝜑 → ( 2 logb 𝐵 ) ∈ ℝ )
77 18 nnrpd ⊢ ( 𝜑 → 𝑃 ∈ ℝ+ )
78 77 rpcnd ⊢ ( 𝜑 → 𝑃 ∈ ℂ )
79 77 rpne0d ⊢ ( 𝜑 → 𝑃 ≠ 0 )
80 78 79 15 cxpexpzd ⊢ ( 𝜑 → ( 𝑃 ↑𝑐 𝐾 ) = ( 𝑃 ↑ 𝐾 ) )
81 19 14 reexpcld ⊢ ( 𝜑 → ( 𝑃 ↑ 𝐾 ) ∈ ℝ )
82 12 nnred ⊢ ( 𝜑 → 𝑅 ∈ ℝ )
83 8 oveq2d ⊢ ( 𝜑 → ( 𝑃 ↑ 𝐾 ) = ( 𝑃 ↑ ( 𝑃 pCnt 𝑅 ) ) )
84 pcdvds ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑅 ∈ ℕ ) → ( 𝑃 ↑ ( 𝑃 pCnt 𝑅 ) ) ∥ 𝑅 )
85 5 12 84 syl2anc ⊢ ( 𝜑 → ( 𝑃 ↑ ( 𝑃 pCnt 𝑅 ) ) ∥ 𝑅 )
86 18 nnzd ⊢ ( 𝜑 → 𝑃 ∈ ℤ )
87 zexpcl ⊢ ( ( 𝑃 ∈ ℤ ∧ ( 𝑃 pCnt 𝑅 ) ∈ ℕ0 ) → ( 𝑃 ↑ ( 𝑃 pCnt 𝑅 ) ) ∈ ℤ )
88 86 13 87 syl2anc ⊢ ( 𝜑 → ( 𝑃 ↑ ( 𝑃 pCnt 𝑅 ) ) ∈ ℤ )
89 dvdsle ⊢ ( ( ( 𝑃 ↑ ( 𝑃 pCnt 𝑅 ) ) ∈ ℤ ∧ 𝑅 ∈ ℕ ) → ( ( 𝑃 ↑ ( 𝑃 pCnt 𝑅 ) ) ∥ 𝑅 → ( 𝑃 ↑ ( 𝑃 pCnt 𝑅 ) ) ≤ 𝑅 ) )
90 88 12 89 syl2anc ⊢ ( 𝜑 → ( ( 𝑃 ↑ ( 𝑃 pCnt 𝑅 ) ) ∥ 𝑅 → ( 𝑃 ↑ ( 𝑃 pCnt 𝑅 ) ) ≤ 𝑅 ) )
91 85 90 mpd ⊢ ( 𝜑 → ( 𝑃 ↑ ( 𝑃 pCnt 𝑅 ) ) ≤ 𝑅 )
92 83 91 eqbrtrd ⊢ ( 𝜑 → ( 𝑃 ↑ 𝐾 ) ≤ 𝑅 )
93 elfzle2 ⊢ ( 𝑅 ∈ ( 1 ... 𝐵 ) → 𝑅 ≤ 𝐵 )
94 10 93 syl ⊢ ( 𝜑 → 𝑅 ≤ 𝐵 )
95 81 82 63 92 94 letrd ⊢ ( 𝜑 → ( 𝑃 ↑ 𝐾 ) ≤ 𝐵 )
96 79 74 nelprd ⊢ ( 𝜑 → ¬ 𝑃 ∈ { 0 , 1 } )
97 78 96 eldifd ⊢ ( 𝜑 → 𝑃 ∈ ( ℂ ∖ { 0 , 1 } ) )
98 63 recnd ⊢ ( 𝜑 → 𝐵 ∈ ℂ )
99 29 64 ltned ⊢ ( 𝜑 → 0 ≠ 𝐵 )
100 99 necomd ⊢ ( 𝜑 → 𝐵 ≠ 0 )
101 100 neneqd ⊢ ( 𝜑 → ¬ 𝐵 = 0 )
102 elsng ⊢ ( 𝐵 ∈ ℕ → ( 𝐵 ∈ { 0 } ↔ 𝐵 = 0 ) )
103 62 102 syl ⊢ ( 𝜑 → ( 𝐵 ∈ { 0 } ↔ 𝐵 = 0 ) )
104 101 103 mtbird ⊢ ( 𝜑 → ¬ 𝐵 ∈ { 0 } )
105 98 104 eldifd ⊢ ( 𝜑 → 𝐵 ∈ ( ℂ ∖ { 0 } ) )
106 cxplogb ⊢ ( ( 𝑃 ∈ ( ℂ ∖ { 0 , 1 } ) ∧ 𝐵 ∈ ( ℂ ∖ { 0 } ) ) → ( 𝑃 ↑𝑐 ( 𝑃 logb 𝐵 ) ) = 𝐵 )
107 97 105 106 syl2anc ⊢ ( 𝜑 → ( 𝑃 ↑𝑐 ( 𝑃 logb 𝐵 ) ) = 𝐵 )
108 95 107 breqtrrd ⊢ ( 𝜑 → ( 𝑃 ↑ 𝐾 ) ≤ ( 𝑃 ↑𝑐 ( 𝑃 logb 𝐵 ) ) )
109 80 108 eqbrtrd ⊢ ( 𝜑 → ( 𝑃 ↑𝑐 𝐾 ) ≤ ( 𝑃 ↑𝑐 ( 𝑃 logb 𝐵 ) ) )
110 77 rpred ⊢ ( 𝜑 → 𝑃 ∈ ℝ )
111 37 67 110 39 71 ltletrd ⊢ ( 𝜑 → 1 < 𝑃 )
112 110 111 16 75 cxpled ⊢ ( 𝜑 → ( 𝐾 ≤ ( 𝑃 logb 𝐵 ) ↔ ( 𝑃 ↑𝑐 𝐾 ) ≤ ( 𝑃 ↑𝑐 ( 𝑃 logb 𝐵 ) ) ) )
113 109 112 mpbird ⊢ ( 𝜑 → 𝐾 ≤ ( 𝑃 logb 𝐵 ) )
114 23 39 rplogcld ⊢ ( 𝜑 → ( log ‘ 2 ) ∈ ℝ+ )
115 110 111 rplogcld ⊢ ( 𝜑 → ( log ‘ 𝑃 ) ∈ ℝ+ )
116 62 nnrpd ⊢ ( 𝜑 → 𝐵 ∈ ℝ+ )
117 116 relogcld ⊢ ( 𝜑 → ( log ‘ 𝐵 ) ∈ ℝ )
118 62 nnge1d ⊢ ( 𝜑 → 1 ≤ 𝐵 )
119 63 118 logge0d ⊢ ( 𝜑 → 0 ≤ ( log ‘ 𝐵 ) )
120 2rp ⊢ 2 ∈ ℝ+
121 120 a1i ⊢ ( 𝜑 → 2 ∈ ℝ+ )
122 121 77 logled ⊢ ( 𝜑 → ( 2 ≤ 𝑃 ↔ ( log ‘ 2 ) ≤ ( log ‘ 𝑃 ) ) )
123 71 122 mpbid ⊢ ( 𝜑 → ( log ‘ 2 ) ≤ ( log ‘ 𝑃 ) )
124 114 115 117 119 123 lediv2ad ⊢ ( 𝜑 → ( ( log ‘ 𝐵 ) / ( log ‘ 𝑃 ) ) ≤ ( ( log ‘ 𝐵 ) / ( log ‘ 2 ) ) )
125 relogbval ⊢ ( ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐵 ∈ ℝ+ ) → ( 𝑃 logb 𝐵 ) = ( ( log ‘ 𝐵 ) / ( log ‘ 𝑃 ) ) )
126 69 116 125 syl2anc ⊢ ( 𝜑 → ( 𝑃 logb 𝐵 ) = ( ( log ‘ 𝐵 ) / ( log ‘ 𝑃 ) ) )
127 126 eqcomd ⊢ ( 𝜑 → ( ( log ‘ 𝐵 ) / ( log ‘ 𝑃 ) ) = ( 𝑃 logb 𝐵 ) )
128 66 uzidd ⊢ ( 𝜑 → 2 ∈ ( ℤ≥ ‘ 2 ) )
129 relogbval ⊢ ( ( 2 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐵 ∈ ℝ+ ) → ( 2 logb 𝐵 ) = ( ( log ‘ 𝐵 ) / ( log ‘ 2 ) ) )
130 128 116 129 syl2anc ⊢ ( 𝜑 → ( 2 logb 𝐵 ) = ( ( log ‘ 𝐵 ) / ( log ‘ 2 ) ) )
131 130 eqcomd ⊢ ( 𝜑 → ( ( log ‘ 𝐵 ) / ( log ‘ 2 ) ) = ( 2 logb 𝐵 ) )
132 124 127 131 3brtr3d ⊢ ( 𝜑 → ( 𝑃 logb 𝐵 ) ≤ ( 2 logb 𝐵 ) )
133 16 75 76 113 132 letrd ⊢ ( 𝜑 → 𝐾 ≤ ( 2 logb 𝐵 ) )
134 flge ⊢ ( ( ( 2 logb 𝐵 ) ∈ ℝ ∧ 𝐾 ∈ ℤ ) → ( 𝐾 ≤ ( 2 logb 𝐵 ) ↔ 𝐾 ≤ ( ⌊ ‘ ( 2 logb 𝐵 ) ) ) )
135 76 15 134 syl2anc ⊢ ( 𝜑 → ( 𝐾 ≤ ( 2 logb 𝐵 ) ↔ 𝐾 ≤ ( ⌊ ‘ ( 2 logb 𝐵 ) ) ) )
136 133 135 mpbid ⊢ ( 𝜑 → 𝐾 ≤ ( ⌊ ‘ ( 2 logb 𝐵 ) ) )