![]() |
Metamath
Proof Explorer Theorem List (p. 416 of 483) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | ![]() (1-30741) |
![]() (30742-32264) |
![]() (32265-48238) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | lcmineqlem2 41501* | Part of lcm inequality lemma, this part eventually shows that F times the least common multiple of 1 to n is an integer. (Contributed by metakunt, 29-Apr-2024.) |
⊢ 𝐹 = ∫(0[,]1)((𝑥↑(𝑀 − 1)) · ((1 − 𝑥)↑(𝑁 − 𝑀))) d𝑥 & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ (𝜑 → 𝑀 ≤ 𝑁) ⇒ ⊢ (𝜑 → 𝐹 = Σ𝑘 ∈ (0...(𝑁 − 𝑀))(((-1↑𝑘) · ((𝑁 − 𝑀)C𝑘)) · ∫(0[,]1)((𝑥↑(𝑀 − 1)) · (𝑥↑𝑘)) d𝑥)) | ||
Theorem | lcmineqlem3 41502* | Part of lcm inequality lemma, this part eventually shows that F times the least common multiple of 1 to n is an integer. (Contributed by metakunt, 30-Apr-2024.) |
⊢ 𝐹 = ∫(0[,]1)((𝑥↑(𝑀 − 1)) · ((1 − 𝑥)↑(𝑁 − 𝑀))) d𝑥 & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ (𝜑 → 𝑀 ≤ 𝑁) ⇒ ⊢ (𝜑 → 𝐹 = Σ𝑘 ∈ (0...(𝑁 − 𝑀))(((-1↑𝑘) · ((𝑁 − 𝑀)C𝑘)) · (1 / (𝑀 + 𝑘)))) | ||
Theorem | lcmineqlem4 41503 | Part of lcm inequality lemma, this part eventually shows that F times the least common multiple of 1 to n is an integer. F is found in lcmineqlem6 41505. (Contributed by metakunt, 10-May-2024.) |
⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ (𝜑 → 𝑀 ≤ 𝑁) & ⊢ (𝜑 → 𝐾 ∈ (0...(𝑁 − 𝑀))) ⇒ ⊢ (𝜑 → ((lcm‘(1...𝑁)) / (𝑀 + 𝐾)) ∈ ℤ) | ||
Theorem | lcmineqlem5 41504 | Technical lemma for reciprocal multiplication in deduction form. (Contributed by metakunt, 10-May-2024.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ≠ 0) ⇒ ⊢ (𝜑 → (𝐴 · (𝐵 · (1 / 𝐶))) = (𝐵 · (𝐴 / 𝐶))) | ||
Theorem | lcmineqlem6 41505* | Part of lcm inequality lemma, this part eventually shows that F times the least common multiple of 1 to n is an integer. (Contributed by metakunt, 10-May-2024.) |
⊢ 𝐹 = ∫(0[,]1)((𝑥↑(𝑀 − 1)) · ((1 − 𝑥)↑(𝑁 − 𝑀))) d𝑥 & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ (𝜑 → 𝑀 ≤ 𝑁) ⇒ ⊢ (𝜑 → ((lcm‘(1...𝑁)) · 𝐹) ∈ ℤ) | ||
Theorem | lcmineqlem7 41506 | Derivative of 1-x for chain rule application. (Contributed by metakunt, 12-May-2024.) |
⊢ (ℂ D (𝑥 ∈ ℂ ↦ (1 − 𝑥))) = (𝑥 ∈ ℂ ↦ -1) | ||
Theorem | lcmineqlem8 41507* | Derivative of (1-x)^(N-M). (Contributed by metakunt, 12-May-2024.) |
⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 𝑀 < 𝑁) ⇒ ⊢ (𝜑 → (ℂ D (𝑥 ∈ ℂ ↦ ((1 − 𝑥)↑(𝑁 − 𝑀)))) = (𝑥 ∈ ℂ ↦ (-(𝑁 − 𝑀) · ((1 − 𝑥)↑((𝑁 − 𝑀) − 1))))) | ||
Theorem | lcmineqlem9 41508* | (1-x)^(N-M) is continuous. (Contributed by metakunt, 12-May-2024.) |
⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 𝑀 ≤ 𝑁) ⇒ ⊢ (𝜑 → (𝑥 ∈ ℂ ↦ ((1 − 𝑥)↑(𝑁 − 𝑀))) ∈ (ℂ–cn→ℂ)) | ||
Theorem | lcmineqlem10 41509* | Induction step of lcmineqlem13 41512 (deduction form). (Contributed by metakunt, 12-May-2024.) |
⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 𝑀 < 𝑁) ⇒ ⊢ (𝜑 → ∫(0[,]1)((𝑥↑((𝑀 + 1) − 1)) · ((1 − 𝑥)↑(𝑁 − (𝑀 + 1)))) d𝑥 = ((𝑀 / (𝑁 − 𝑀)) · ∫(0[,]1)((𝑥↑(𝑀 − 1)) · ((1 − 𝑥)↑(𝑁 − 𝑀))) d𝑥)) | ||
Theorem | lcmineqlem11 41510 | Induction step, continuation for binomial coefficients. (Contributed by metakunt, 12-May-2024.) |
⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 𝑀 < 𝑁) ⇒ ⊢ (𝜑 → (1 / ((𝑀 + 1) · (𝑁C(𝑀 + 1)))) = ((𝑀 / (𝑁 − 𝑀)) · (1 / (𝑀 · (𝑁C𝑀))))) | ||
Theorem | lcmineqlem12 41511* | Base case for induction. (Contributed by metakunt, 12-May-2024.) |
⊢ (𝜑 → 𝑁 ∈ ℕ) ⇒ ⊢ (𝜑 → ∫(0[,]1)((𝑡↑(1 − 1)) · ((1 − 𝑡)↑(𝑁 − 1))) d𝑡 = (1 / (1 · (𝑁C1)))) | ||
Theorem | lcmineqlem13 41512* | Induction proof for lcm integral. (Contributed by metakunt, 12-May-2024.) |
⊢ 𝐹 = ∫(0[,]1)((𝑥↑(𝑀 − 1)) · ((1 − 𝑥)↑(𝑁 − 𝑀))) d𝑥 & ⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 𝑀 ≤ 𝑁) ⇒ ⊢ (𝜑 → 𝐹 = (1 / (𝑀 · (𝑁C𝑀)))) | ||
Theorem | lcmineqlem14 41513 | Technical lemma for inequality estimate. (Contributed by metakunt, 12-May-2024.) |
⊢ (𝜑 → 𝐴 ∈ ℕ) & ⊢ (𝜑 → 𝐵 ∈ ℕ) & ⊢ (𝜑 → 𝐶 ∈ ℕ) & ⊢ (𝜑 → 𝐷 ∈ ℕ) & ⊢ (𝜑 → 𝐸 ∈ ℕ) & ⊢ (𝜑 → (𝐴 · 𝐶) ∥ 𝐷) & ⊢ (𝜑 → (𝐵 · 𝐶) ∥ 𝐸) & ⊢ (𝜑 → 𝐷 ∥ 𝐸) & ⊢ (𝜑 → (𝐴 gcd 𝐵) = 1) ⇒ ⊢ (𝜑 → ((𝐴 · 𝐵) · 𝐶) ∥ 𝐸) | ||
Theorem | lcmineqlem15 41514* | F times the least common multiple of 1 to n is a natural number. (Contributed by metakunt, 10-May-2024.) |
⊢ 𝐹 = ∫(0[,]1)((𝑥↑(𝑀 − 1)) · ((1 − 𝑥)↑(𝑁 − 𝑀))) d𝑥 & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ (𝜑 → 𝑀 ≤ 𝑁) ⇒ ⊢ (𝜑 → ((lcm‘(1...𝑁)) · 𝐹) ∈ ℕ) | ||
Theorem | lcmineqlem16 41515 | Technical divisibility lemma. (Contributed by metakunt, 12-May-2024.) |
⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 𝑀 ≤ 𝑁) ⇒ ⊢ (𝜑 → (𝑀 · (𝑁C𝑀)) ∥ (lcm‘(1...𝑁))) | ||
Theorem | lcmineqlem17 41516 | Inequality of 2^{2n}. (Contributed by metakunt, 29-Apr-2024.) |
⊢ (𝜑 → 𝑁 ∈ ℕ0) ⇒ ⊢ (𝜑 → (2↑(2 · 𝑁)) ≤ (((2 · 𝑁) + 1) · ((2 · 𝑁)C𝑁))) | ||
Theorem | lcmineqlem18 41517 | Technical lemma to shift factors in binomial coefficient. (Contributed by metakunt, 12-May-2024.) |
⊢ (𝜑 → 𝑁 ∈ ℕ) ⇒ ⊢ (𝜑 → ((𝑁 + 1) · (((2 · 𝑁) + 1)C(𝑁 + 1))) = (((2 · 𝑁) + 1) · ((2 · 𝑁)C𝑁))) | ||
Theorem | lcmineqlem19 41518 | Dividing implies inequality for lcm inequality lemma. (Contributed by metakunt, 12-May-2024.) |
⊢ (𝜑 → 𝑁 ∈ ℕ) ⇒ ⊢ (𝜑 → ((𝑁 · ((2 · 𝑁) + 1)) · ((2 · 𝑁)C𝑁)) ∥ (lcm‘(1...((2 · 𝑁) + 1)))) | ||
Theorem | lcmineqlem20 41519 | Inequality for lcm lemma. (Contributed by metakunt, 12-May-2024.) |
⊢ (𝜑 → 𝑁 ∈ ℕ) ⇒ ⊢ (𝜑 → (𝑁 · (2↑(2 · 𝑁))) ≤ (lcm‘(1...((2 · 𝑁) + 1)))) | ||
Theorem | lcmineqlem21 41520 | The lcm inequality lemma without base cases 7 and 8. (Contributed by metakunt, 12-May-2024.) |
⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 4 ≤ 𝑁) ⇒ ⊢ (𝜑 → (2↑((2 · 𝑁) + 2)) ≤ (lcm‘(1...((2 · 𝑁) + 1)))) | ||
Theorem | lcmineqlem22 41521 | The lcm inequality lemma without base cases 7 and 8. (Contributed by metakunt, 12-May-2024.) |
⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 4 ≤ 𝑁) ⇒ ⊢ (𝜑 → ((2↑((2 · 𝑁) + 1)) ≤ (lcm‘(1...((2 · 𝑁) + 1))) ∧ (2↑((2 · 𝑁) + 2)) ≤ (lcm‘(1...((2 · 𝑁) + 2))))) | ||
Theorem | lcmineqlem23 41522 | Penultimate step to the lcm inequality lemma. (Contributed by metakunt, 12-May-2024.) |
⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 9 ≤ 𝑁) ⇒ ⊢ (𝜑 → (2↑𝑁) ≤ (lcm‘(1...𝑁))) | ||
Theorem | lcmineqlem 41523 | The least common multiple inequality lemma, a central result for future use. Theorem 3.1 from https://www3.nd.edu/%7eandyp/notes/AKS.pdf (Contributed by metakunt, 16-May-2024.) |
⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 7 ≤ 𝑁) ⇒ ⊢ (𝜑 → (2↑𝑁) ≤ (lcm‘(1...𝑁))) | ||
Theorem | 3exp7 41524 | 3 to the power of 7 equals 2187. (Contributed by metakunt, 21-Aug-2024.) |
⊢ (3↑7) = ;;;2187 | ||
Theorem | 3lexlogpow5ineq1 41525 | First inequality in inequality chain, proposed by Mario Carneiro (Contributed by metakunt, 22-May-2024.) |
⊢ 9 < ((;11 / 7)↑5) | ||
Theorem | 3lexlogpow5ineq2 41526 | Second inequality in inequality chain, proposed by Mario Carneiro. (Contributed by metakunt, 22-May-2024.) |
⊢ (𝜑 → 𝑋 ∈ ℝ) & ⊢ (𝜑 → 3 ≤ 𝑋) ⇒ ⊢ (𝜑 → ((;11 / 7)↑5) ≤ ((2 logb 𝑋)↑5)) | ||
Theorem | 3lexlogpow5ineq4 41527 | Sharper logarithm inequality chain. (Contributed by metakunt, 21-Aug-2024.) |
⊢ (𝜑 → 𝑋 ∈ ℝ) & ⊢ (𝜑 → 3 ≤ 𝑋) ⇒ ⊢ (𝜑 → 9 < ((2 logb 𝑋)↑5)) | ||
Theorem | 3lexlogpow5ineq3 41528 | Combined inequality chain for a specific power of the binary logarithm, proposed by Mario Carneiro. (Contributed by metakunt, 22-May-2024.) |
⊢ (𝜑 → 𝑋 ∈ ℝ) & ⊢ (𝜑 → 3 ≤ 𝑋) ⇒ ⊢ (𝜑 → 7 < ((2 logb 𝑋)↑5)) | ||
Theorem | 3lexlogpow2ineq1 41529 | Result for bound in AKS inequality lemma. (Contributed by metakunt, 21-Aug-2024.) |
⊢ ((3 / 2) < (2 logb 3) ∧ (2 logb 3) < (5 / 3)) | ||
Theorem | 3lexlogpow2ineq2 41530 | Result for bound in AKS inequality lemma. (Contributed by metakunt, 21-Aug-2024.) |
⊢ (2 < ((2 logb 3)↑2) ∧ ((2 logb 3)↑2) < 3) | ||
Theorem | 3lexlogpow5ineq5 41531 | Result for bound in AKS inequality lemma. (Contributed by metakunt, 21-Aug-2024.) |
⊢ ((2 logb 3)↑5) ≤ ;15 | ||
Theorem | intlewftc 41532* | Inequality inference by invoking fundamental theorem of calculus. (Contributed by metakunt, 22-Jul-2024.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐴 ≤ 𝐵) & ⊢ (𝜑 → 𝐹 ∈ ((𝐴[,]𝐵)–cn→ℝ)) & ⊢ (𝜑 → 𝐺 ∈ ((𝐴[,]𝐵)–cn→ℝ)) & ⊢ (𝜑 → 𝐷 = (ℝ D 𝐹)) & ⊢ (𝜑 → 𝐸 = (ℝ D 𝐺)) & ⊢ (𝜑 → 𝐷 ∈ ((𝐴(,)𝐵)–cn→ℝ)) & ⊢ (𝜑 → 𝐸 ∈ ((𝐴(,)𝐵)–cn→ℝ)) & ⊢ (𝜑 → 𝐷 ∈ 𝐿1) & ⊢ (𝜑 → 𝐸 ∈ 𝐿1) & ⊢ (𝜑 → 𝐷 = (𝑥 ∈ (𝐴(,)𝐵) ↦ 𝑃)) & ⊢ (𝜑 → 𝐸 = (𝑥 ∈ (𝐴(,)𝐵) ↦ 𝑄)) & ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → 𝑃 ≤ 𝑄) & ⊢ (𝜑 → (𝐹‘𝐴) ≤ (𝐺‘𝐴)) ⇒ ⊢ (𝜑 → (𝐹‘𝐵) ≤ (𝐺‘𝐵)) | ||
Theorem | aks4d1lem1 41533 | Technical lemma to reduce proof size. (Contributed by metakunt, 14-Nov-2024.) |
⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘3)) & ⊢ 𝐵 = (⌈‘((2 logb 𝑁)↑5)) ⇒ ⊢ (𝜑 → (𝐵 ∈ ℕ ∧ 9 < 𝐵)) | ||
Theorem | aks4d1p1p1 41534* | Exponential law for finite products, special case. (Contributed by metakunt, 22-Jul-2024.) |
⊢ (𝜑 → 𝐴 ∈ ℝ+) & ⊢ (𝜑 → 𝑁 ∈ ℕ) ⇒ ⊢ (𝜑 → ∏𝑘 ∈ (1...𝑁)(𝐴↑𝑐𝑘) = (𝐴↑𝑐Σ𝑘 ∈ (1...𝑁)𝑘)) | ||
Theorem | dvrelog2 41535* | The derivative of the logarithm, ftc2 25992 version. (Contributed by metakunt, 11-Aug-2024.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 0 < 𝐴) & ⊢ (𝜑 → 𝐴 ≤ 𝐵) & ⊢ 𝐹 = (𝑥 ∈ (𝐴[,]𝐵) ↦ (log‘𝑥)) & ⊢ 𝐺 = (𝑥 ∈ (𝐴(,)𝐵) ↦ (1 / 𝑥)) ⇒ ⊢ (𝜑 → (ℝ D 𝐹) = 𝐺) | ||
Theorem | dvrelog3 41536* | The derivative of the logarithm on an open interval. (Contributed by metakunt, 11-Aug-2024.) |
⊢ (𝜑 → 𝐴 ∈ ℝ*) & ⊢ (𝜑 → 𝐵 ∈ ℝ*) & ⊢ (𝜑 → 0 ≤ 𝐴) & ⊢ (𝜑 → 𝐴 ≤ 𝐵) & ⊢ 𝐹 = (𝑥 ∈ (𝐴(,)𝐵) ↦ (log‘𝑥)) & ⊢ 𝐺 = (𝑥 ∈ (𝐴(,)𝐵) ↦ (1 / 𝑥)) ⇒ ⊢ (𝜑 → (ℝ D 𝐹) = 𝐺) | ||
Theorem | dvrelog2b 41537* | Derivative of the binary logarithm. (Contributed by metakunt, 11-Aug-2024.) |
⊢ (𝜑 → 𝐴 ∈ ℝ*) & ⊢ (𝜑 → 𝐵 ∈ ℝ*) & ⊢ (𝜑 → 0 ≤ 𝐴) & ⊢ (𝜑 → 𝐴 ≤ 𝐵) & ⊢ 𝐹 = (𝑥 ∈ (𝐴(,)𝐵) ↦ (2 logb 𝑥)) & ⊢ 𝐺 = (𝑥 ∈ (𝐴(,)𝐵) ↦ (1 / (𝑥 · (log‘2)))) ⇒ ⊢ (𝜑 → (ℝ D 𝐹) = 𝐺) | ||
Theorem | 0nonelalab 41538 | Technical lemma for open interval. (Contributed by metakunt, 12-Aug-2024.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 0 < 𝐴) & ⊢ (𝜑 → 𝐴 ≤ 𝐵) & ⊢ (𝜑 → 𝐶 ∈ (𝐴(,)𝐵)) ⇒ ⊢ (𝜑 → 0 ≠ 𝐶) | ||
Theorem | dvrelogpow2b 41539* | Derivative of the power of the binary logarithm. (Contributed by metakunt, 12-Aug-2024.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 0 < 𝐴) & ⊢ (𝜑 → 𝐴 ≤ 𝐵) & ⊢ 𝐹 = (𝑥 ∈ (𝐴(,)𝐵) ↦ ((2 logb 𝑥)↑𝑁)) & ⊢ 𝐺 = (𝑥 ∈ (𝐴(,)𝐵) ↦ (𝐶 · (((log‘𝑥)↑(𝑁 − 1)) / 𝑥))) & ⊢ 𝐶 = (𝑁 / ((log‘2)↑𝑁)) & ⊢ (𝜑 → 𝑁 ∈ ℕ) ⇒ ⊢ (𝜑 → (ℝ D 𝐹) = 𝐺) | ||
Theorem | aks4d1p1p3 41540 | Bound of a ceiling of the binary logarithm to the fifth power. (Contributed by metakunt, 19-Aug-2024.) |
⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ 𝐵 = (⌈‘((2 logb 𝑁)↑5)) & ⊢ (𝜑 → 3 ≤ 𝑁) ⇒ ⊢ (𝜑 → (𝑁↑𝑐(⌊‘(2 logb 𝐵))) < (𝑁↑𝑐(2 logb (((2 logb 𝑁)↑5) + 1)))) | ||
Theorem | aks4d1p1p2 41541* | Rewrite 𝐴 in more suitable form. (Contributed by metakunt, 19-Aug-2024.) |
⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ 𝐴 = ((𝑁↑(⌊‘(2 logb 𝐵))) · ∏𝑘 ∈ (1...(⌊‘((2 logb 𝑁)↑2)))((𝑁↑𝑘) − 1)) & ⊢ 𝐵 = (⌈‘((2 logb 𝑁)↑5)) & ⊢ (𝜑 → 3 ≤ 𝑁) ⇒ ⊢ (𝜑 → 𝐴 < (𝑁↑𝑐(((2 logb (((2 logb 𝑁)↑5) + 1)) + (((2 logb 𝑁)↑2) / 2)) + (((2 logb 𝑁)↑4) / 2)))) | ||
Theorem | aks4d1p1p4 41542* | Technical step for inequality. The hard work is in to prove the final hypothesis. (Contributed by metakunt, 19-Aug-2024.) |
⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ 𝐴 = ((𝑁↑(⌊‘(2 logb 𝐵))) · ∏𝑘 ∈ (1...(⌊‘((2 logb 𝑁)↑2)))((𝑁↑𝑘) − 1)) & ⊢ 𝐵 = (⌈‘((2 logb 𝑁)↑5)) & ⊢ (𝜑 → 3 ≤ 𝑁) & ⊢ 𝐶 = (2 logb (((2 logb 𝑁)↑5) + 1)) & ⊢ 𝐷 = ((2 logb 𝑁)↑2) & ⊢ 𝐸 = ((2 logb 𝑁)↑4) & ⊢ (𝜑 → ((2 · 𝐶) + 𝐷) ≤ 𝐸) ⇒ ⊢ (𝜑 → 𝐴 < (2↑𝐵)) | ||
Theorem | dvle2 41543* | Collapsed dvle 25953. (Contributed by metakunt, 19-Aug-2024.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝐸) ∈ ((𝐴[,]𝐵)–cn→ℝ)) & ⊢ (𝜑 → (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝐺) ∈ ((𝐴[,]𝐵)–cn→ℝ)) & ⊢ (𝜑 → (ℝ D (𝑥 ∈ (𝐴(,)𝐵) ↦ 𝐸)) = (𝑥 ∈ (𝐴(,)𝐵) ↦ 𝐹)) & ⊢ (𝜑 → (ℝ D (𝑥 ∈ (𝐴(,)𝐵) ↦ 𝐺)) = (𝑥 ∈ (𝐴(,)𝐵) ↦ 𝐻)) & ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → 𝐹 ≤ 𝐻) & ⊢ (𝑥 = 𝐴 → 𝐸 = 𝑃) & ⊢ (𝑥 = 𝐴 → 𝐺 = 𝑄) & ⊢ (𝑥 = 𝐵 → 𝐸 = 𝑅) & ⊢ (𝑥 = 𝐵 → 𝐺 = 𝑆) & ⊢ (𝜑 → 𝑃 ≤ 𝑄) & ⊢ (𝜑 → 𝐴 ≤ 𝐵) ⇒ ⊢ (𝜑 → 𝑅 ≤ 𝑆) | ||
Theorem | aks4d1p1p6 41544* | Inequality lift to differentiable functions for a term in AKS inequality lemma. (Contributed by metakunt, 19-Aug-2024.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 3 ≤ 𝐴) & ⊢ (𝜑 → 𝐴 ≤ 𝐵) ⇒ ⊢ (𝜑 → (ℝ D (𝑥 ∈ (𝐴(,)𝐵) ↦ ((2 · (2 logb (((2 logb 𝑥)↑5) + 1))) + ((2 logb 𝑥)↑2)))) = (𝑥 ∈ (𝐴(,)𝐵) ↦ ((2 · ((1 / ((((2 logb 𝑥)↑5) + 1) · (log‘2))) · (((5 · ((2 logb 𝑥)↑4)) · (1 / (𝑥 · (log‘2)))) + 0))) + ((2 / ((log‘2)↑2)) · (((log‘𝑥)↑(2 − 1)) / 𝑥))))) | ||
Theorem | aks4d1p1p7 41545 | Bound of intermediary of inequality step. (Contributed by metakunt, 19-Aug-2024.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 4 ≤ 𝐴) ⇒ ⊢ (𝜑 → ((2 · ((1 / ((((2 logb 𝐴)↑5) + 1) · (log‘2))) · (((5 · ((2 logb 𝐴)↑4)) · (1 / (𝐴 · (log‘2)))) + 0))) + ((2 / ((log‘2)↑2)) · (((log‘𝐴)↑(2 − 1)) / 𝐴))) ≤ ((4 / ((log‘2)↑4)) · (((log‘𝐴)↑3) / 𝐴))) | ||
Theorem | aks4d1p1p5 41546* | Show inequality for existence of a non-divisor. (Contributed by metakunt, 19-Aug-2024.) |
⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ 𝐴 = ((𝑁↑(⌊‘(2 logb 𝐵))) · ∏𝑘 ∈ (1...(⌊‘((2 logb 𝑁)↑2)))((𝑁↑𝑘) − 1)) & ⊢ 𝐵 = (⌈‘((2 logb 𝑁)↑5)) & ⊢ (𝜑 → 4 ≤ 𝑁) & ⊢ 𝐶 = (2 logb (((2 logb 𝑁)↑5) + 1)) & ⊢ 𝐷 = ((2 logb 𝑁)↑2) & ⊢ 𝐸 = ((2 logb 𝑁)↑4) ⇒ ⊢ (𝜑 → 𝐴 < (2↑𝐵)) | ||
Theorem | aks4d1p1 41547* | Show inequality for existence of a non-divisor. (Contributed by metakunt, 21-Aug-2024.) |
⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘3)) & ⊢ 𝐴 = ((𝑁↑(⌊‘(2 logb 𝐵))) · ∏𝑘 ∈ (1...(⌊‘((2 logb 𝑁)↑2)))((𝑁↑𝑘) − 1)) & ⊢ 𝐵 = (⌈‘((2 logb 𝑁)↑5)) ⇒ ⊢ (𝜑 → 𝐴 < (2↑𝐵)) | ||
Theorem | aks4d1p2 41548 | Technical lemma for existence of non-divisor. (Contributed by metakunt, 27-Oct-2024.) |
⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘3)) & ⊢ 𝐴 = ((𝑁↑(⌊‘(2 logb 𝐵))) · ∏𝑘 ∈ (1...(⌊‘((2 logb 𝑁)↑2)))((𝑁↑𝑘) − 1)) & ⊢ 𝐵 = (⌈‘((2 logb 𝑁)↑5)) ⇒ ⊢ (𝜑 → (2↑𝐵) ≤ (lcm‘(1...𝐵))) | ||
Theorem | aks4d1p3 41549* | There exists a small enough number such that it does not divide 𝐴. (Contributed by metakunt, 27-Oct-2024.) |
⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘3)) & ⊢ 𝐴 = ((𝑁↑(⌊‘(2 logb 𝐵))) · ∏𝑘 ∈ (1...(⌊‘((2 logb 𝑁)↑2)))((𝑁↑𝑘) − 1)) & ⊢ 𝐵 = (⌈‘((2 logb 𝑁)↑5)) ⇒ ⊢ (𝜑 → ∃𝑟 ∈ (1...𝐵) ¬ 𝑟 ∥ 𝐴) | ||
Theorem | aks4d1p4 41550* | There exists a small enough number such that it does not divide 𝐴. (Contributed by metakunt, 28-Oct-2024.) |
⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘3)) & ⊢ 𝐴 = ((𝑁↑(⌊‘(2 logb 𝐵))) · ∏𝑘 ∈ (1...(⌊‘((2 logb 𝑁)↑2)))((𝑁↑𝑘) − 1)) & ⊢ 𝐵 = (⌈‘((2 logb 𝑁)↑5)) & ⊢ 𝑅 = inf({𝑟 ∈ (1...𝐵) ∣ ¬ 𝑟 ∥ 𝐴}, ℝ, < ) ⇒ ⊢ (𝜑 → (𝑅 ∈ (1...𝐵) ∧ ¬ 𝑅 ∥ 𝐴)) | ||
Theorem | aks4d1p5 41551* | Show that 𝑁 and 𝑅 are coprime for AKS existence theorem. Precondition will be eliminated in further theorem. (Contributed by metakunt, 30-Oct-2024.) |
⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘3)) & ⊢ 𝐴 = ((𝑁↑(⌊‘(2 logb 𝐵))) · ∏𝑘 ∈ (1...(⌊‘((2 logb 𝑁)↑2)))((𝑁↑𝑘) − 1)) & ⊢ 𝐵 = (⌈‘((2 logb 𝑁)↑5)) & ⊢ 𝑅 = inf({𝑟 ∈ (1...𝐵) ∣ ¬ 𝑟 ∥ 𝐴}, ℝ, < ) & ⊢ (((𝜑 ∧ 1 < (𝑁 gcd 𝑅)) ∧ (𝑅 / (𝑁 gcd 𝑅)) ∥ 𝐴) → ¬ (𝑅 / (𝑁 gcd 𝑅)) ∥ 𝐴) ⇒ ⊢ (𝜑 → (𝑁 gcd 𝑅) = 1) | ||
Theorem | aks4d1p6 41552* | The maximal prime power exponent is smaller than the binary logarithm floor of 𝐵. (Contributed by metakunt, 30-Oct-2024.) |
⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘3)) & ⊢ 𝐴 = ((𝑁↑(⌊‘(2 logb 𝐵))) · ∏𝑘 ∈ (1...(⌊‘((2 logb 𝑁)↑2)))((𝑁↑𝑘) − 1)) & ⊢ 𝐵 = (⌈‘((2 logb 𝑁)↑5)) & ⊢ 𝑅 = inf({𝑟 ∈ (1...𝐵) ∣ ¬ 𝑟 ∥ 𝐴}, ℝ, < ) & ⊢ (𝜑 → 𝑃 ∈ ℙ) & ⊢ (𝜑 → 𝑃 ∥ 𝑅) & ⊢ 𝐾 = (𝑃 pCnt 𝑅) ⇒ ⊢ (𝜑 → 𝐾 ≤ (⌊‘(2 logb 𝐵))) | ||
Theorem | aks4d1p7d1 41553* | Technical step in AKS lemma 4.1 (Contributed by metakunt, 31-Oct-2024.) |
⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘3)) & ⊢ 𝐴 = ((𝑁↑(⌊‘(2 logb 𝐵))) · ∏𝑘 ∈ (1...(⌊‘((2 logb 𝑁)↑2)))((𝑁↑𝑘) − 1)) & ⊢ 𝐵 = (⌈‘((2 logb 𝑁)↑5)) & ⊢ 𝑅 = inf({𝑟 ∈ (1...𝐵) ∣ ¬ 𝑟 ∥ 𝐴}, ℝ, < ) & ⊢ (𝜑 → ∀𝑝 ∈ ℙ (𝑝 ∥ 𝑅 → 𝑝 ∥ 𝑁)) ⇒ ⊢ (𝜑 → 𝑅 ∥ (𝑁↑(⌊‘(2 logb 𝐵)))) | ||
Theorem | aks4d1p7 41554* | Technical step in AKS lemma 4.1 (Contributed by metakunt, 31-Oct-2024.) |
⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘3)) & ⊢ 𝐴 = ((𝑁↑(⌊‘(2 logb 𝐵))) · ∏𝑘 ∈ (1...(⌊‘((2 logb 𝑁)↑2)))((𝑁↑𝑘) − 1)) & ⊢ 𝐵 = (⌈‘((2 logb 𝑁)↑5)) & ⊢ 𝑅 = inf({𝑟 ∈ (1...𝐵) ∣ ¬ 𝑟 ∥ 𝐴}, ℝ, < ) ⇒ ⊢ (𝜑 → ∃𝑝 ∈ ℙ (𝑝 ∥ 𝑅 ∧ ¬ 𝑝 ∥ 𝑁)) | ||
Theorem | aks4d1p8d1 41555 | If a prime divides one number 𝑀, but not another number 𝑁, then it divides the quotient of 𝑀 and the gcd of 𝑀 and 𝑁. (Contributed by Thierry Arnoux, 10-Nov-2024.) |
⊢ (𝜑 → 𝑃 ∈ ℙ) & ⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 𝑃 ∥ 𝑀) & ⊢ (𝜑 → ¬ 𝑃 ∥ 𝑁) ⇒ ⊢ (𝜑 → 𝑃 ∥ (𝑀 / (𝑀 gcd 𝑁))) | ||
Theorem | aks4d1p8d2 41556 | Any prime power dividing a positive integer is less than that integer if that integer has another prime factor. (Contributed by metakunt, 13-Nov-2024.) |
⊢ (𝜑 → 𝑅 ∈ ℕ) & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 𝑃 ∈ ℙ) & ⊢ (𝜑 → 𝑄 ∈ ℙ) & ⊢ (𝜑 → 𝑃 ∥ 𝑅) & ⊢ (𝜑 → 𝑄 ∥ 𝑅) & ⊢ (𝜑 → ¬ 𝑃 ∥ 𝑁) & ⊢ (𝜑 → 𝑄 ∥ 𝑁) ⇒ ⊢ (𝜑 → (𝑃↑(𝑃 pCnt 𝑅)) < 𝑅) | ||
Theorem | aks4d1p8d3 41557 | The remainder of a division with its maximal prime power is coprime with that prime power. (Contributed by metakunt, 13-Nov-2024.) |
⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 𝑃 ∈ ℙ) & ⊢ (𝜑 → 𝑃 ∥ 𝑁) ⇒ ⊢ (𝜑 → ((𝑁 / (𝑃↑(𝑃 pCnt 𝑁))) gcd (𝑃↑(𝑃 pCnt 𝑁))) = 1) | ||
Theorem | aks4d1p8 41558* | Show that 𝑁 and 𝑅 are coprime for AKS existence theorem, with eliminated hypothesis. (Contributed by metakunt, 10-Nov-2024.) (Proof sketch by Thierry Arnoux.) |
⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘3)) & ⊢ 𝐴 = ((𝑁↑(⌊‘(2 logb 𝐵))) · ∏𝑘 ∈ (1...(⌊‘((2 logb 𝑁)↑2)))((𝑁↑𝑘) − 1)) & ⊢ 𝐵 = (⌈‘((2 logb 𝑁)↑5)) & ⊢ 𝑅 = inf({𝑟 ∈ (1...𝐵) ∣ ¬ 𝑟 ∥ 𝐴}, ℝ, < ) ⇒ ⊢ (𝜑 → (𝑁 gcd 𝑅) = 1) | ||
Theorem | aks4d1p9 41559* | Show that the order is bound by the squared binary logarithm. (Contributed by metakunt, 14-Nov-2024.) |
⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘3)) & ⊢ 𝐴 = ((𝑁↑(⌊‘(2 logb 𝐵))) · ∏𝑘 ∈ (1...(⌊‘((2 logb 𝑁)↑2)))((𝑁↑𝑘) − 1)) & ⊢ 𝐵 = (⌈‘((2 logb 𝑁)↑5)) & ⊢ 𝑅 = inf({𝑟 ∈ (1...𝐵) ∣ ¬ 𝑟 ∥ 𝐴}, ℝ, < ) ⇒ ⊢ (𝜑 → ((2 logb 𝑁)↑2) < ((odℤ‘𝑅)‘𝑁)) | ||
Theorem | aks4d1 41560* | Lemma 4.1 from https://www3.nd.edu/%7eandyp/notes/AKS.pdf, existence of a polynomially bounded number by the digit size of 𝑁 that asserts the polynomial subspace that we need to search to guarantee that 𝑁 is prime. Eventually we want to show that the polynomial searching space is bounded by degree 𝐵. (Contributed by metakunt, 14-Nov-2024.) |
⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘3)) & ⊢ 𝐵 = (⌈‘((2 logb 𝑁)↑5)) ⇒ ⊢ (𝜑 → ∃𝑟 ∈ (1...𝐵)((𝑁 gcd 𝑟) = 1 ∧ ((2 logb 𝑁)↑2) < ((odℤ‘𝑟)‘𝑁))) | ||
Theorem | fldhmf1 41561 | A field homomorphism is injective. This follows immediately from the definition of the ring homomorphism that sends the multiplicative identity to the multiplicative identity. (Contributed by metakunt, 7-Jan-2025.) |
⊢ (𝜑 → 𝐾 ∈ Field) & ⊢ (𝜑 → 𝐿 ∈ Field) & ⊢ (𝜑 → 𝐹 ∈ (𝐾 RingHom 𝐿)) & ⊢ 𝐴 = (Base‘𝐾) & ⊢ 𝐵 = (Base‘𝐿) ⇒ ⊢ (𝜑 → 𝐹:𝐴–1-1→𝐵) | ||
Syntax | cprimroots 41562 | Define the class of primitive roots. (Contributed by metakunt, 25-Apr-2025.) |
class PrimRoots | ||
Definition | df-primroots 41563* | A 𝑟-th primitive root is a root of unity such that the exponent divides 𝑟. (Contributed by metakunt, 25-Apr-2025.) |
⊢ PrimRoots = (𝑟 ∈ CMnd, 𝑘 ∈ ℕ0 ↦ ⦋(Base‘𝑟) / 𝑏⦌{𝑎 ∈ 𝑏 ∣ ((𝑘(.g‘𝑟)𝑎) = (0g‘𝑟) ∧ ∀𝑙 ∈ ℕ0 ((𝑙(.g‘𝑟)𝑎) = (0g‘𝑟) → 𝑘 ∥ 𝑙))}) | ||
Theorem | isprimroot 41564* | The value of a primitive root. (Contributed by metakunt, 25-Apr-2025.) |
⊢ (𝜑 → 𝑅 ∈ CMnd) & ⊢ (𝜑 → 𝐾 ∈ ℕ0) & ⊢ ↑ = (.g‘𝑅) ⇒ ⊢ (𝜑 → (𝑀 ∈ (𝑅 PrimRoots 𝐾) ↔ (𝑀 ∈ (Base‘𝑅) ∧ (𝐾 ↑ 𝑀) = (0g‘𝑅) ∧ ∀𝑙 ∈ ℕ0 ((𝑙 ↑ 𝑀) = (0g‘𝑅) → 𝐾 ∥ 𝑙)))) | ||
Theorem | mndmolinv 41565* | An element of a monoid that has a right inverse has at most one left inverse. (Contributed by metakunt, 25-Apr-2025.) |
⊢ 𝐵 = (Base‘𝑀) & ⊢ (𝜑 → 𝑀 ∈ Mnd) & ⊢ (𝜑 → 𝐴 ∈ 𝐵) & ⊢ (𝜑 → ∃𝑥 ∈ 𝐵 (𝐴(+g‘𝑀)𝑥) = (0g‘𝑀)) ⇒ ⊢ (𝜑 → ∃*𝑥 ∈ 𝐵 (𝑥(+g‘𝑀)𝐴) = (0g‘𝑀)) | ||
Theorem | linvh 41566* | If an element has a unique left inverse, then the value satisfies the left inverse value equation. (Contributed by metakunt, 25-Apr-2025.) |
⊢ (𝜑 → 𝑋 ∈ (Base‘𝑅)) & ⊢ (𝜑 → ∃!𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑋) = (0g‘𝑅)) ⇒ ⊢ (𝜑 → (((invg‘𝑅)‘𝑋)(+g‘𝑅)𝑋) = (0g‘𝑅)) | ||
Theorem | primrootsunit1 41567* | Primitive roots have left inverses. (Contributed by metakunt, 25-Apr-2025.) |
⊢ (𝜑 → 𝑅 ∈ CMnd) & ⊢ (𝜑 → 𝐾 ∈ ℕ) & ⊢ 𝑈 = {𝑎 ∈ (Base‘𝑅) ∣ ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑎) = (0g‘𝑅)} ⇒ ⊢ (𝜑 → ((𝑅 PrimRoots 𝐾) = ((𝑅 ↾s 𝑈) PrimRoots 𝐾) ∧ (𝑅 ↾s 𝑈) ∈ Abel)) | ||
Theorem | primrootsunit 41568* | Primitive roots have left inverses. (Contributed by metakunt, 25-Apr-2025.) |
⊢ (𝜑 → 𝑅 ∈ CMnd) & ⊢ (𝜑 → 𝐾 ∈ ℕ) & ⊢ 𝑈 = {𝑎 ∈ (Base‘𝑅) ∣ ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑎) = (0g‘𝑅)} ⇒ ⊢ (𝜑 → ((𝑅 PrimRoots 𝐾) = ((𝑅 ↾s 𝑈) PrimRoots 𝐾) ∧ (𝑅 ↾s 𝑈) ∈ Abel)) | ||
Theorem | ressmulgnnd 41569 | Values for the group multiple function in a restricted structure, a deduction version. (Contributed by metakunt, 14-May-2025.) |
⊢ 𝐻 = (𝐺 ↾s 𝐴) & ⊢ (𝜑 → 𝐴 ⊆ (Base‘𝐺)) & ⊢ (𝜑 → 𝑋 ∈ 𝐴) & ⊢ (𝜑 → 𝑁 ∈ ℕ) ⇒ ⊢ (𝜑 → (𝑁(.g‘𝐻)𝑋) = (𝑁(.g‘𝐺)𝑋)) | ||
Theorem | primrootscoprmpow 41570* | Coprime powers of primitive roots are primitive roots. (Contributed by metakunt, 25-Apr-2025.) |
⊢ (𝜑 → 𝑅 ∈ CMnd) & ⊢ (𝜑 → 𝐾 ∈ ℕ) & ⊢ (𝜑 → 𝐸 ∈ ℕ) & ⊢ (𝜑 → (𝐸 gcd 𝐾) = 1) & ⊢ (𝜑 → 𝑀 ∈ (𝑅 PrimRoots 𝐾)) & ⊢ 𝑈 = {𝑎 ∈ (Base‘𝑅) ∣ ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑎) = (0g‘𝑅)} ⇒ ⊢ (𝜑 → (𝐸(.g‘𝑅)𝑀) ∈ (𝑅 PrimRoots 𝐾)) | ||
Theorem | posbezout 41571* | Bezout's identity restricted on positive integers in all but one variable. (Contributed by metakunt, 26-Apr-2025.) |
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) → ∃𝑥 ∈ ℕ ∃𝑦 ∈ ℤ (𝐴 gcd 𝐵) = ((𝐴 · 𝑥) + (𝐵 · 𝑦))) | ||
Theorem | primrootscoprf 41572* | Coprime powers of primitive roots are primitive roots, as a function. (Contributed by metakunt, 26-Apr-2025.) |
⊢ 𝐹 = (𝑚 ∈ (𝑅 PrimRoots 𝐾) ↦ (𝐸(.g‘𝑅)𝑚)) & ⊢ (𝜑 → 𝑅 ∈ CMnd) & ⊢ (𝜑 → 𝐾 ∈ ℕ) & ⊢ (𝜑 → 𝐸 ∈ ℕ) & ⊢ (𝜑 → (𝐸 gcd 𝐾) = 1) ⇒ ⊢ (𝜑 → 𝐹:(𝑅 PrimRoots 𝐾)⟶(𝑅 PrimRoots 𝐾)) | ||
Theorem | primrootscoprbij 41573* | A bijection between coprime powers of primitive roots and primitive roots. (Contributed by metakunt, 26-Apr-2025.) |
⊢ 𝐹 = (𝑚 ∈ (𝑅 PrimRoots 𝐾) ↦ (𝐼(.g‘𝑅)𝑚)) & ⊢ (𝜑 → 𝑅 ∈ CMnd) & ⊢ (𝜑 → 𝐾 ∈ ℕ) & ⊢ (𝜑 → 𝐼 ∈ ℕ) & ⊢ (𝜑 → 𝐽 ∈ ℕ) & ⊢ (𝜑 → 𝑍 ∈ ℤ) & ⊢ (𝜑 → 1 = ((𝐼 · 𝐽) + (𝐾 · 𝑍))) & ⊢ 𝑈 = {𝑎 ∈ (Base‘𝑅) ∣ ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑎) = (0g‘𝑅)} ⇒ ⊢ (𝜑 → 𝐹:(𝑅 PrimRoots 𝐾)–1-1-onto→(𝑅 PrimRoots 𝐾)) | ||
Theorem | primrootscoprbij2 41574* | A bijection between coprime powers of primitive roots and primitive roots. (Contributed by metakunt, 26-Apr-2025.) |
⊢ 𝐹 = (𝑚 ∈ (𝑅 PrimRoots 𝐾) ↦ (𝐼(.g‘𝑅)𝑚)) & ⊢ (𝜑 → 𝑅 ∈ CMnd) & ⊢ (𝜑 → 𝐾 ∈ ℕ) & ⊢ (𝜑 → 𝐼 ∈ ℕ) & ⊢ (𝜑 → (𝐼 gcd 𝐾) = 1) ⇒ ⊢ (𝜑 → 𝐹:(𝑅 PrimRoots 𝐾)–1-1-onto→(𝑅 PrimRoots 𝐾)) | ||
Theorem | remexz 41575* | Division with rest. (Contributed by metakunt, 15-May-2025.) |
⊢ (𝜑 → 𝑁 ∈ ℤ) & ⊢ (𝜑 → 𝐴 ∈ ℕ) ⇒ ⊢ (𝜑 → ∃𝑥 ∈ ℤ ∃𝑦 ∈ (0...(𝐴 − 1))𝑁 = ((𝑥 · 𝐴) + 𝑦)) | ||
Theorem | primrootlekpowne0 41576 | There is no smaller power of a primitive root that sends it to the neutral element. (Contributed by metakunt, 15-May-2025.) |
⊢ (𝜑 → 𝑅 ∈ CMnd) & ⊢ (𝜑 → 𝐾 ∈ ℕ) & ⊢ (𝜑 → 𝑀 ∈ (𝑅 PrimRoots 𝐾)) & ⊢ (𝜑 → 𝑁 ∈ (1...(𝐾 − 1))) ⇒ ⊢ (𝜑 → (𝑁(.g‘𝑅)𝑀) ≠ (0g‘𝑅)) | ||
Theorem | primrootspoweq0 41577* | The power of a 𝑅-th primitive root is zero if and only if it divides 𝑅. (Contributed by metakunt, 15-May-2025.) |
⊢ (𝜑 → 𝑅 ∈ CMnd) & ⊢ (𝜑 → 𝐾 ∈ ℕ) & ⊢ (𝜑 → 𝑀 ∈ (𝑅 PrimRoots 𝐾)) & ⊢ 𝑈 = {𝑎 ∈ (Base‘𝑅) ∣ ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑎) = (0g‘𝑅)} & ⊢ (𝜑 → 𝑁 ∈ ℤ) ⇒ ⊢ (𝜑 → ((𝑁(.g‘(𝑅 ↾s 𝑈))𝑀) = (0g‘(𝑅 ↾s 𝑈)) ↔ 𝐾 ∥ 𝑁)) | ||
Theorem | aks6d1c1p1 41578* | Definition of the introspective relation. (Contributed by metakunt, 25-Apr-2025.) |
⊢ ∼ = {〈𝑒, 𝑓〉 ∣ (𝑒 ∈ ℕ ∧ 𝑓 ∈ 𝐵 ∧ ∀𝑦 ∈ (𝐾 PrimRoots 𝑅)(𝑒 ↑ ((𝑂‘𝑓)‘𝑦)) = ((𝑂‘𝑓)‘(𝑒𝐷𝑦)))} & ⊢ (𝜑 → 𝐹 ∈ 𝐵) & ⊢ (𝜑 → 𝐸 ∈ ℕ) ⇒ ⊢ (𝜑 → (𝐸 ∼ 𝐹 ↔ ∀𝑦 ∈ (𝐾 PrimRoots 𝑅)(𝐸 ↑ ((𝑂‘𝐹)‘𝑦)) = ((𝑂‘𝐹)‘(𝐸𝐷𝑦)))) | ||
Theorem | aks6d1c1p1rcl 41579* | Reverse closure of the introspective relation. (Contributed by metakunt, 25-Apr-2025.) |
⊢ ∼ = {〈𝑒, 𝑓〉 ∣ (𝑒 ∈ ℕ ∧ 𝑓 ∈ 𝐵 ∧ ∀𝑦 ∈ (𝐾 PrimRoots 𝑅)(𝑒 ↑ ((𝑂‘𝑓)‘𝑦)) = ((𝑂‘𝑓)‘(𝑒𝐷𝑦)))} & ⊢ (𝜑 → 𝐸 ∼ 𝐹) ⇒ ⊢ (𝜑 → (𝐸 ∈ ℕ ∧ 𝐹 ∈ 𝐵)) | ||
Theorem | aks6d1c1p2 41580* | 𝑃 and linear factors are introspective. (Contributed by metakunt, 25-Apr-2025.) |
⊢ ∼ = {〈𝑒, 𝑓〉 ∣ (𝑒 ∈ ℕ ∧ 𝑓 ∈ 𝐵 ∧ ∀𝑦 ∈ (𝑉 PrimRoots 𝑅)(𝑒 ↑ ((𝑂‘𝑓)‘𝑦)) = ((𝑂‘𝑓)‘(𝑒 ↑ 𝑦)))} & ⊢ 𝑆 = (Poly1‘𝐾) & ⊢ 𝐵 = (Base‘𝑆) & ⊢ 𝑋 = (var1‘𝐾) & ⊢ 𝑊 = (mulGrp‘𝑆) & ⊢ 𝑉 = (mulGrp‘𝐾) & ⊢ ↑ = (.g‘𝑉) & ⊢ 𝐶 = (algSc‘𝑆) & ⊢ 𝐷 = (.g‘𝑊) & ⊢ 𝑃 = (chr‘𝐾) & ⊢ 𝑂 = (eval1‘𝐾) & ⊢ + = (+g‘𝑆) & ⊢ (𝜑 → 𝐾 ∈ Field) & ⊢ (𝜑 → 𝑃 ∈ ℙ) & ⊢ (𝜑 → 𝑅 ∈ ℕ) & ⊢ (𝜑 → (𝑁 gcd 𝑅) = 1) & ⊢ (𝜑 → 𝑃 ∥ 𝑁) & ⊢ 𝐹 = (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝐴))) & ⊢ (𝜑 → 𝐴 ∈ ℤ) ⇒ ⊢ (𝜑 → 𝑃 ∼ 𝐹) | ||
Theorem | aks6d1c1p3 41581* | In a field with a Frobenius isomorphism (read: algebraic closure or finite field), 𝑁 and linear factors are introspective. (Contributed by metakunt, 25-Apr-2025.) |
⊢ ∼ = {〈𝑒, 𝑓〉 ∣ (𝑒 ∈ ℕ ∧ 𝑓 ∈ 𝐵 ∧ ∀𝑦 ∈ (𝑉 PrimRoots 𝑅)(𝑒 ↑ ((𝑂‘𝑓)‘𝑦)) = ((𝑂‘𝑓)‘(𝑒 ↑ 𝑦)))} & ⊢ 𝑆 = (Poly1‘𝐾) & ⊢ 𝐵 = (Base‘𝑆) & ⊢ 𝑋 = (var1‘𝐾) & ⊢ 𝑊 = (mulGrp‘𝑆) & ⊢ 𝑉 = (mulGrp‘𝐾) & ⊢ ↑ = (.g‘𝑉) & ⊢ 𝐶 = (algSc‘𝑆) & ⊢ 𝐷 = (.g‘𝑊) & ⊢ 𝑃 = (chr‘𝐾) & ⊢ 𝑂 = (eval1‘𝐾) & ⊢ + = (+g‘𝑆) & ⊢ (𝜑 → 𝐾 ∈ Field) & ⊢ (𝜑 → 𝑃 ∈ ℙ) & ⊢ (𝜑 → 𝑅 ∈ ℕ) & ⊢ (𝜑 → (𝑁 gcd 𝑅) = 1) & ⊢ (𝜑 → 𝑃 ∥ 𝑁) & ⊢ 𝐹 = (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝐴))) & ⊢ (𝜑 → 𝐴 ∈ ℤ) & ⊢ (𝜑 → 𝑁 ∼ 𝐹) & ⊢ (𝜑 → (𝑥 ∈ (Base‘𝐾) ↦ (𝑃 ↑ 𝑥)) ∈ (𝐾 RingIso 𝐾)) ⇒ ⊢ (𝜑 → (𝑁 / 𝑃) ∼ 𝐹) | ||
Theorem | aks6d1c1p4 41582* | The product of polynomials is introspective. (Contributed by metakunt, 25-Apr-2025.) |
⊢ ∼ = {〈𝑒, 𝑓〉 ∣ (𝑒 ∈ ℕ ∧ 𝑓 ∈ 𝐵 ∧ ∀𝑦 ∈ (𝑉 PrimRoots 𝑅)(𝑒 ↑ ((𝑂‘𝑓)‘𝑦)) = ((𝑂‘𝑓)‘(𝑒 ↑ 𝑦)))} & ⊢ 𝑆 = (Poly1‘𝐾) & ⊢ 𝐵 = (Base‘𝑆) & ⊢ 𝑋 = (var1‘𝐾) & ⊢ 𝑊 = (mulGrp‘𝑆) & ⊢ 𝑉 = (mulGrp‘𝐾) & ⊢ ↑ = (.g‘𝑉) & ⊢ 𝐶 = (algSc‘𝑆) & ⊢ 𝐷 = (.g‘𝑊) & ⊢ 𝑃 = (chr‘𝐾) & ⊢ 𝑂 = (eval1‘𝐾) & ⊢ + = (+g‘𝑆) & ⊢ (𝜑 → 𝐾 ∈ Field) & ⊢ (𝜑 → 𝑃 ∈ ℙ) & ⊢ (𝜑 → 𝑅 ∈ ℕ) & ⊢ (𝜑 → (𝑁 gcd 𝑅) = 1) & ⊢ (𝜑 → 𝑃 ∥ 𝑁) & ⊢ (𝜑 → 𝐸 ∼ 𝐹) & ⊢ (𝜑 → 𝐸 ∼ 𝐺) ⇒ ⊢ (𝜑 → 𝐸 ∼ (𝐹(+g‘𝑊)𝐺)) | ||
Theorem | aks6d1c1p5 41583* | The product of exponents is introspective. (Contributed by metakunt, 26-Apr-2025.) |
⊢ ∼ = {〈𝑒, 𝑓〉 ∣ (𝑒 ∈ ℕ ∧ 𝑓 ∈ 𝐵 ∧ ∀𝑦 ∈ (𝑉 PrimRoots 𝑅)(𝑒 ↑ ((𝑂‘𝑓)‘𝑦)) = ((𝑂‘𝑓)‘(𝑒 ↑ 𝑦)))} & ⊢ 𝑆 = (Poly1‘𝐾) & ⊢ 𝐵 = (Base‘𝑆) & ⊢ 𝑋 = (var1‘𝐾) & ⊢ 𝑊 = (mulGrp‘𝑆) & ⊢ 𝑉 = (mulGrp‘𝐾) & ⊢ ↑ = (.g‘𝑉) & ⊢ 𝐶 = (algSc‘𝑆) & ⊢ 𝑃 = (chr‘𝐾) & ⊢ 𝑂 = (eval1‘𝐾) & ⊢ + = (+g‘𝑆) & ⊢ (𝜑 → 𝐾 ∈ Field) & ⊢ (𝜑 → 𝑃 ∈ ℙ) & ⊢ (𝜑 → 𝑅 ∈ ℕ) & ⊢ (𝜑 → (𝐸 gcd 𝑅) = 1) & ⊢ (𝜑 → 𝑃 ∥ 𝑁) & ⊢ (𝜑 → 𝐷 ∼ 𝐹) & ⊢ (𝜑 → 𝐸 ∼ 𝐹) ⇒ ⊢ (𝜑 → (𝐷 · 𝐸) ∼ 𝐹) | ||
Theorem | aks6d1c1p7 41584* | 𝑋 is introspective to all positive integers. (Contributed by metakunt, 30-Apr-2025.) |
⊢ ∼ = {〈𝑒, 𝑓〉 ∣ (𝑒 ∈ ℕ ∧ 𝑓 ∈ 𝐵 ∧ ∀𝑦 ∈ (𝑉 PrimRoots 𝑅)(𝑒 ↑ ((𝑂‘𝑓)‘𝑦)) = ((𝑂‘𝑓)‘(𝑒 ↑ 𝑦)))} & ⊢ 𝑆 = (Poly1‘𝐾) & ⊢ 𝐵 = (Base‘𝑆) & ⊢ 𝑋 = (var1‘𝐾) & ⊢ 𝑉 = (mulGrp‘𝐾) & ⊢ ↑ = (.g‘𝑉) & ⊢ 𝑃 = (chr‘𝐾) & ⊢ 𝑂 = (eval1‘𝐾) & ⊢ (𝜑 → 𝐾 ∈ Field) & ⊢ (𝜑 → 𝑃 ∈ ℙ) & ⊢ (𝜑 → 𝑅 ∈ ℕ) & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 𝑃 ∥ 𝑁) & ⊢ (𝜑 → (𝑁 gcd 𝑅) = 1) & ⊢ (𝜑 → 𝐿 ∈ ℕ) ⇒ ⊢ (𝜑 → 𝐿 ∼ 𝑋) | ||
Theorem | aks6d1c1p6 41585* | If a polynomials 𝐹 is introspective to 𝐸, then so are its powers. (Contributed by metakunt, 30-Apr-2025.) |
⊢ ∼ = {〈𝑒, 𝑓〉 ∣ (𝑒 ∈ ℕ ∧ 𝑓 ∈ 𝐵 ∧ ∀𝑦 ∈ (𝑉 PrimRoots 𝑅)(𝑒 ↑ ((𝑂‘𝑓)‘𝑦)) = ((𝑂‘𝑓)‘(𝑒 ↑ 𝑦)))} & ⊢ 𝑆 = (Poly1‘𝐾) & ⊢ 𝐵 = (Base‘𝑆) & ⊢ 𝑋 = (var1‘𝐾) & ⊢ 𝑊 = (mulGrp‘𝑆) & ⊢ 𝑉 = (mulGrp‘𝐾) & ⊢ ↑ = (.g‘𝑉) & ⊢ 𝐶 = (algSc‘𝑆) & ⊢ 𝐷 = (.g‘𝑊) & ⊢ 𝑃 = (chr‘𝐾) & ⊢ 𝑂 = (eval1‘𝐾) & ⊢ + = (+g‘𝑆) & ⊢ (𝜑 → 𝐾 ∈ Field) & ⊢ (𝜑 → 𝑃 ∈ ℙ) & ⊢ (𝜑 → 𝑅 ∈ ℕ) & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 𝑃 ∥ 𝑁) & ⊢ (𝜑 → (𝑁 gcd 𝑅) = 1) & ⊢ (𝜑 → 𝐸 ∼ 𝐹) & ⊢ (𝜑 → 𝐿 ∈ ℕ0) ⇒ ⊢ (𝜑 → 𝐸 ∼ (𝐿𝐷𝐹)) | ||
Theorem | aks6d1c1p8 41586* | If a number 𝐸 is introspective to 𝐹, then so are its powers. (Contributed by metakunt, 30-Apr-2025.) |
⊢ ∼ = {〈𝑒, 𝑓〉 ∣ (𝑒 ∈ ℕ ∧ 𝑓 ∈ 𝐵 ∧ ∀𝑦 ∈ (𝑉 PrimRoots 𝑅)(𝑒 ↑ ((𝑂‘𝑓)‘𝑦)) = ((𝑂‘𝑓)‘(𝑒 ↑ 𝑦)))} & ⊢ 𝑆 = (Poly1‘𝐾) & ⊢ 𝐵 = (Base‘𝑆) & ⊢ 𝑋 = (var1‘𝐾) & ⊢ 𝑊 = (mulGrp‘𝑆) & ⊢ 𝑉 = (mulGrp‘𝐾) & ⊢ ↑ = (.g‘𝑉) & ⊢ 𝐶 = (algSc‘𝑆) & ⊢ 𝐷 = (.g‘𝑊) & ⊢ 𝑃 = (chr‘𝐾) & ⊢ 𝑂 = (eval1‘𝐾) & ⊢ + = (+g‘𝑆) & ⊢ (𝜑 → 𝐾 ∈ Field) & ⊢ (𝜑 → 𝑃 ∈ ℙ) & ⊢ (𝜑 → 𝑅 ∈ ℕ) & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 𝑃 ∥ 𝑁) & ⊢ (𝜑 → (𝑁 gcd 𝑅) = 1) & ⊢ (𝜑 → 𝐸 ∼ 𝐹) & ⊢ (𝜑 → 𝐿 ∈ ℕ0) & ⊢ (𝜑 → (𝐸 gcd 𝑅) = 1) ⇒ ⊢ (𝜑 → (𝐸↑𝐿) ∼ 𝐹) | ||
Theorem | aks6d1c1 41587* | Claim 1 of Theorem 6.1 https://www3.nd.edu/%7eandyp/notes/AKS.pdf. (Contributed by metakunt, 30-Apr-2025.) |
⊢ ∼ = {〈𝑒, 𝑓〉 ∣ (𝑒 ∈ ℕ ∧ 𝑓 ∈ 𝐵 ∧ ∀𝑦 ∈ (𝑉 PrimRoots 𝑅)(𝑒 ↑ ((𝑂‘𝑓)‘𝑦)) = ((𝑂‘𝑓)‘(𝑒 ↑ 𝑦)))} & ⊢ 𝑆 = (Poly1‘𝐾) & ⊢ 𝐵 = (Base‘𝑆) & ⊢ 𝑋 = (var1‘𝐾) & ⊢ 𝑊 = (mulGrp‘𝑆) & ⊢ 𝑉 = (mulGrp‘𝐾) & ⊢ ↑ = (.g‘𝑉) & ⊢ 𝐶 = (algSc‘𝑆) & ⊢ 𝐷 = (.g‘𝑊) & ⊢ 𝑃 = (chr‘𝐾) & ⊢ 𝑂 = (eval1‘𝐾) & ⊢ + = (+g‘𝑆) & ⊢ (𝜑 → 𝐾 ∈ Field) & ⊢ (𝜑 → 𝑃 ∈ ℙ) & ⊢ (𝜑 → 𝑅 ∈ ℕ) & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 𝑃 ∥ 𝑁) & ⊢ (𝜑 → (𝑁 gcd 𝑅) = 1) & ⊢ (𝜑 → 𝐹:(0...𝐴)⟶ℕ0) & ⊢ 𝐺 = (𝑔 ∈ (ℕ0 ↑m (0...𝐴)) ↦ (𝑊 Σg (𝑖 ∈ (0...𝐴) ↦ ((𝑔‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))))) & ⊢ (𝜑 → 𝐴 ∈ ℕ0) & ⊢ (𝜑 → 𝑈 ∈ ℕ0) & ⊢ (𝜑 → 𝐿 ∈ ℕ0) & ⊢ 𝐸 = ((𝑃↑𝑈) · ((𝑁 / 𝑃)↑𝐿)) & ⊢ (𝜑 → ∀𝑎 ∈ (1...𝐴)𝑁 ∼ (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑎)))) & ⊢ (𝜑 → (𝑥 ∈ (Base‘𝐾) ↦ (𝑃 ↑ 𝑥)) ∈ (𝐾 RingIso 𝐾)) ⇒ ⊢ (𝜑 → 𝐸 ∼ (𝐺‘𝐹)) | ||
Theorem | evl1gprodd 41588* | Polynomial evaluation builder for a finite group product of polynomials. (Contributed by metakunt, 29-Apr-2025.) |
⊢ 𝑂 = (eval1‘𝑅) & ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝑄 = (mulGrp‘𝑃) & ⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝑈 = (Base‘𝑃) & ⊢ 𝑆 = (mulGrp‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ CRing) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → ∀𝑥 ∈ 𝑁 𝑀 ∈ 𝑈) & ⊢ (𝜑 → 𝑁 ∈ Fin) ⇒ ⊢ (𝜑 → ((𝑂‘(𝑄 Σg (𝑥 ∈ 𝑁 ↦ 𝑀)))‘𝑌) = (𝑆 Σg (𝑥 ∈ 𝑁 ↦ ((𝑂‘𝑀)‘𝑌)))) | ||
Theorem | aks6d1c2p1 41589* | In the AKS-theorem the subset defined by 𝐸 takes values in the positive integers. (Contributed by metakunt, 7-Jan-2025.) |
⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 𝑃 ∈ ℙ) & ⊢ (𝜑 → 𝑃 ∥ 𝑁) & ⊢ 𝐸 = (𝑘 ∈ ℕ0, 𝑙 ∈ ℕ0 ↦ ((𝑃↑𝑘) · ((𝑁 / 𝑃)↑𝑙))) ⇒ ⊢ (𝜑 → 𝐸:(ℕ0 × ℕ0)⟶ℕ) | ||
Theorem | aks6d1c2p2 41590* | Injective condition for countability argument assuming that 𝑁 is not a prime power. (Contributed by metakunt, 7-Jan-2025.) |
⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 𝑃 ∈ ℙ) & ⊢ (𝜑 → 𝑃 ∥ 𝑁) & ⊢ 𝐸 = (𝑘 ∈ ℕ0, 𝑙 ∈ ℕ0 ↦ ((𝑃↑𝑘) · ((𝑁 / 𝑃)↑𝑙))) & ⊢ (𝜑 → 𝑄 ∈ ℙ) & ⊢ (𝜑 → 𝑄 ∥ 𝑁) & ⊢ (𝜑 → 𝑃 ≠ 𝑄) ⇒ ⊢ (𝜑 → 𝐸:(ℕ0 × ℕ0)–1-1→ℕ) | ||
Theorem | hashscontpowcl 41591 | Closure of E for https://www3.nd.edu/%7eandyp/notes/AKS.pdf Theorem 6.1. (Contributed by metakunt, 28-Apr-2025.) |
⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 𝑃 ∈ ℙ) & ⊢ (𝜑 → 𝑃 ∥ 𝑁) & ⊢ (𝜑 → 𝑅 ∈ ℕ) & ⊢ (𝜑 → (𝑁 gcd 𝑅) = 1) & ⊢ 𝐸 = (𝑘 ∈ ℕ0, 𝑙 ∈ ℕ0 ↦ ((𝑃↑𝑘) · ((𝑁 / 𝑃)↑𝑙))) & ⊢ 𝐿 = (ℤRHom‘𝑌) & ⊢ 𝑌 = (ℤ/nℤ‘𝑅) ⇒ ⊢ (𝜑 → (♯‘(𝐿 “ (𝐸 “ (ℕ0 × ℕ0)))) ∈ ℕ0) | ||
Theorem | hashscontpow1 41592 | Helper lemma for to prove inequality in Zr. (Contributed by metakunt, 28-Apr-2025.) |
⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 𝐴 ∈ (1...((odℤ‘𝑅)‘𝑁))) & ⊢ (𝜑 → 𝐵 ∈ (1...((odℤ‘𝑅)‘𝑁))) & ⊢ (𝜑 → 𝑅 ∈ ℕ) & ⊢ (𝜑 → (𝑁 gcd 𝑅) = 1) & ⊢ 𝐿 = (ℤRHom‘𝑌) & ⊢ 𝑌 = (ℤ/nℤ‘𝑅) & ⊢ (𝜑 → 𝐴 < 𝐵) ⇒ ⊢ (𝜑 → (𝐿‘(𝑁↑𝐴)) ≠ (𝐿‘(𝑁↑𝐵))) | ||
Theorem | hashscontpow 41593* | If a set contains all 𝑁-th powers, then the size of the image under the ZR homomorphism is greater than the 𝑅-th order of 𝑁. (Contributed by metakunt, 28-Apr-2025.) |
⊢ (𝜑 → 𝐸 ⊆ ℤ) & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → ∀𝑘 ∈ ℕ0 (𝑁↑𝑘) ∈ 𝐸) & ⊢ (𝜑 → 𝑅 ∈ ℕ) & ⊢ (𝜑 → (𝑁 gcd 𝑅) = 1) & ⊢ 𝐿 = (ℤRHom‘𝑌) & ⊢ 𝑌 = (ℤ/nℤ‘𝑅) ⇒ ⊢ (𝜑 → ((odℤ‘𝑅)‘𝑁) ≤ (♯‘(𝐿 “ 𝐸))) | ||
Theorem | aks6d1c3 41594* | Claim 3 of Theorem 6.1 of the AKS inequality lemma. https://www3.nd.edu/%7eandyp/notes/AKS.pdf (Contributed by metakunt, 28-Apr-2025.) |
⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 𝑃 ∈ ℙ) & ⊢ (𝜑 → 𝑃 ∥ 𝑁) & ⊢ (𝜑 → 𝑅 ∈ ℕ) & ⊢ (𝜑 → (𝑁 gcd 𝑅) = 1) & ⊢ 𝐸 = (𝑘 ∈ ℕ0, 𝑙 ∈ ℕ0 ↦ ((𝑃↑𝑘) · ((𝑁 / 𝑃)↑𝑙))) & ⊢ 𝐿 = (ℤRHom‘𝑌) & ⊢ 𝑌 = (ℤ/nℤ‘𝑅) & ⊢ (𝜑 → ((2 logb 𝑁)↑2) < ((odℤ‘𝑅)‘𝑁)) ⇒ ⊢ (𝜑 → ((2 logb 𝑁)↑2) < (♯‘(𝐿 “ (𝐸 “ (ℕ0 × ℕ0))))) | ||
Theorem | aks6d1c4 41595* | Claim 4 of Theorem 6.1 of the AKS inequality lemma. https://www3.nd.edu/%7eandyp/notes/AKS.pdf (Contributed by metakunt, 12-May-2025.) |
⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 𝑃 ∈ ℙ) & ⊢ (𝜑 → 𝑃 ∥ 𝑁) & ⊢ (𝜑 → 𝑅 ∈ ℕ) & ⊢ (𝜑 → (𝑁 gcd 𝑅) = 1) & ⊢ 𝐸 = (𝑘 ∈ ℕ0, 𝑙 ∈ ℕ0 ↦ ((𝑃↑𝑘) · ((𝑁 / 𝑃)↑𝑙))) & ⊢ 𝐿 = (ℤRHom‘(ℤ/nℤ‘𝑅)) ⇒ ⊢ (𝜑 → (♯‘(𝐿 “ (𝐸 “ (ℕ0 × ℕ0)))) ≤ (ϕ‘𝑅)) | ||
Theorem | aks6d1c1rh 41596* | Claim 1 of AKS primality proof with collapsed definitions since their ease of use is no longer needed. (Contributed by metakunt, 1-May-2025.) |
⊢ ∼ = {〈𝑒, 𝑓〉 ∣ (𝑒 ∈ ℕ ∧ 𝑓 ∈ (Base‘(Poly1‘𝐾)) ∧ ∀𝑦 ∈ ((mulGrp‘𝐾) PrimRoots 𝑅)(𝑒(.g‘(mulGrp‘𝐾))(((eval1‘𝐾)‘𝑓)‘𝑦)) = (((eval1‘𝐾)‘𝑓)‘(𝑒(.g‘(mulGrp‘𝐾))𝑦)))} & ⊢ 𝑃 = (chr‘𝐾) & ⊢ (𝜑 → 𝐾 ∈ Field) & ⊢ (𝜑 → 𝑃 ∈ ℙ) & ⊢ (𝜑 → 𝑅 ∈ ℕ) & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 𝑃 ∥ 𝑁) & ⊢ (𝜑 → (𝑁 gcd 𝑅) = 1) & ⊢ (𝜑 → 𝐹:(0...𝐴)⟶ℕ0) & ⊢ 𝐺 = (𝑔 ∈ (ℕ0 ↑m (0...𝐴)) ↦ ((mulGrp‘(Poly1‘𝐾)) Σg (𝑖 ∈ (0...𝐴) ↦ ((𝑔‘𝑖)(.g‘(mulGrp‘(Poly1‘𝐾)))((var1‘𝐾)(+g‘(Poly1‘𝐾))((algSc‘(Poly1‘𝐾))‘((ℤRHom‘𝐾)‘𝑖))))))) & ⊢ (𝜑 → 𝐴 ∈ ℕ0) & ⊢ (𝜑 → 𝑈 ∈ ℕ0) & ⊢ (𝜑 → 𝐿 ∈ ℕ0) & ⊢ 𝐸 = ((𝑃↑𝑈) · ((𝑁 / 𝑃)↑𝐿)) & ⊢ (𝜑 → ∀𝑎 ∈ (1...𝐴)𝑁 ∼ ((var1‘𝐾)(+g‘(Poly1‘𝐾))((algSc‘(Poly1‘𝐾))‘((ℤRHom‘𝐾)‘𝑎)))) & ⊢ (𝜑 → (𝑥 ∈ (Base‘𝐾) ↦ (𝑃(.g‘(mulGrp‘𝐾))𝑥)) ∈ (𝐾 RingIso 𝐾)) ⇒ ⊢ (𝜑 → 𝐸 ∼ (𝐺‘𝐹)) | ||
Theorem | aks6d1c2lem3 41597* | Lemma for aks6d1c2 41601 to simplify context. (Contributed by metakunt, 1-May-2025.) |
⊢ ∼ = {〈𝑒, 𝑓〉 ∣ (𝑒 ∈ ℕ ∧ 𝑓 ∈ (Base‘(Poly1‘𝐾)) ∧ ∀𝑦 ∈ ((mulGrp‘𝐾) PrimRoots 𝑅)(𝑒(.g‘(mulGrp‘𝐾))(((eval1‘𝐾)‘𝑓)‘𝑦)) = (((eval1‘𝐾)‘𝑓)‘(𝑒(.g‘(mulGrp‘𝐾))𝑦)))} & ⊢ 𝑃 = (chr‘𝐾) & ⊢ (𝜑 → 𝐾 ∈ Field) & ⊢ (𝜑 → 𝑃 ∈ ℙ) & ⊢ (𝜑 → 𝑅 ∈ ℕ) & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 𝑃 ∥ 𝑁) & ⊢ (𝜑 → (𝑁 gcd 𝑅) = 1) & ⊢ (𝜑 → 𝐹:(0...𝐴)⟶ℕ0) & ⊢ 𝐺 = (𝑔 ∈ (ℕ0 ↑m (0...𝐴)) ↦ ((mulGrp‘(Poly1‘𝐾)) Σg (𝑖 ∈ (0...𝐴) ↦ ((𝑔‘𝑖)(.g‘(mulGrp‘(Poly1‘𝐾)))((var1‘𝐾)(+g‘(Poly1‘𝐾))((algSc‘(Poly1‘𝐾))‘((ℤRHom‘𝐾)‘𝑖))))))) & ⊢ (𝜑 → 𝐴 ∈ ℕ0) & ⊢ 𝐸 = (𝑘 ∈ ℕ0, 𝑙 ∈ ℕ0 ↦ ((𝑃↑𝑘) · ((𝑁 / 𝑃)↑𝑙))) & ⊢ 𝐿 = (ℤRHom‘(ℤ/nℤ‘𝑅)) & ⊢ (𝜑 → ∀𝑎 ∈ (1...𝐴)𝑁 ∼ ((var1‘𝐾)(+g‘(Poly1‘𝐾))((algSc‘(Poly1‘𝐾))‘((ℤRHom‘𝐾)‘𝑎)))) & ⊢ (𝜑 → (𝑥 ∈ (Base‘𝐾) ↦ (𝑃(.g‘(mulGrp‘𝐾))𝑥)) ∈ (𝐾 RingIso 𝐾)) & ⊢ (𝜑 → 𝑀 ∈ ((mulGrp‘𝐾) PrimRoots 𝑅)) & ⊢ 𝐻 = (ℎ ∈ (ℕ0 ↑m (0...𝐴)) ↦ (((eval1‘𝐾)‘(𝐺‘ℎ))‘𝑀)) & ⊢ 𝐵 = (⌊‘(√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 × ℕ0)))))) & ⊢ 𝐶 = (𝐸 “ ((0...𝐵) × (0...𝐵))) & ⊢ (𝜑 → 𝐼 ∈ 𝐶) & ⊢ (𝜑 → 𝐽 ∈ 𝐶) & ⊢ (𝜑 → 𝐼 < 𝐽) & ⊢ ↑ = (.g‘(mulGrp‘(Poly1‘𝐾))) & ⊢ 𝑋 = (var1‘𝐾) & ⊢ 𝑆 = ((𝐽 ↑ 𝑋)(-g‘(Poly1‘𝐾))(𝐼 ↑ 𝑋)) & ⊢ (𝜑 → 𝑈 ∈ ℕ) & ⊢ (𝜑 → 𝐽 = (𝐼 + (𝑈 · 𝑅))) & ⊢ (𝜑 → 𝑠 ∈ (ℕ0 ↑m (0...𝐴))) & ⊢ (𝜑 → 𝑟 ∈ (0...𝐵)) & ⊢ (𝜑 → 𝑜 ∈ (0...𝐵)) & ⊢ (𝜑 → 𝐽 = (𝑟𝐸𝑜)) & ⊢ (𝜑 → 𝑝 ∈ (0...𝐵)) & ⊢ (𝜑 → 𝑞 ∈ (0...𝐵)) & ⊢ (𝜑 → 𝐼 = (𝑝𝐸𝑞)) & ⊢ (𝜑 → 𝐼 ∈ ℕ0) ⇒ ⊢ (𝜑 → (𝐽(.g‘(mulGrp‘𝐾))(((eval1‘𝐾)‘(𝐺‘𝑠))‘𝑀)) = (𝐼(.g‘(mulGrp‘𝐾))(((eval1‘𝐾)‘(𝐺‘𝑠))‘𝑀))) | ||
Theorem | aks6d1c2lem4 41598* | Claim 2 of Theorem 6.1 AKS, Preparation for injectivity proof. (Contributed by metakunt, 1-May-2025.) |
⊢ ∼ = {〈𝑒, 𝑓〉 ∣ (𝑒 ∈ ℕ ∧ 𝑓 ∈ (Base‘(Poly1‘𝐾)) ∧ ∀𝑦 ∈ ((mulGrp‘𝐾) PrimRoots 𝑅)(𝑒(.g‘(mulGrp‘𝐾))(((eval1‘𝐾)‘𝑓)‘𝑦)) = (((eval1‘𝐾)‘𝑓)‘(𝑒(.g‘(mulGrp‘𝐾))𝑦)))} & ⊢ 𝑃 = (chr‘𝐾) & ⊢ (𝜑 → 𝐾 ∈ Field) & ⊢ (𝜑 → 𝑃 ∈ ℙ) & ⊢ (𝜑 → 𝑅 ∈ ℕ) & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 𝑃 ∥ 𝑁) & ⊢ (𝜑 → (𝑁 gcd 𝑅) = 1) & ⊢ (𝜑 → 𝐹:(0...𝐴)⟶ℕ0) & ⊢ 𝐺 = (𝑔 ∈ (ℕ0 ↑m (0...𝐴)) ↦ ((mulGrp‘(Poly1‘𝐾)) Σg (𝑖 ∈ (0...𝐴) ↦ ((𝑔‘𝑖)(.g‘(mulGrp‘(Poly1‘𝐾)))((var1‘𝐾)(+g‘(Poly1‘𝐾))((algSc‘(Poly1‘𝐾))‘((ℤRHom‘𝐾)‘𝑖))))))) & ⊢ (𝜑 → 𝐴 ∈ ℕ0) & ⊢ 𝐸 = (𝑘 ∈ ℕ0, 𝑙 ∈ ℕ0 ↦ ((𝑃↑𝑘) · ((𝑁 / 𝑃)↑𝑙))) & ⊢ 𝐿 = (ℤRHom‘(ℤ/nℤ‘𝑅)) & ⊢ (𝜑 → ∀𝑎 ∈ (1...𝐴)𝑁 ∼ ((var1‘𝐾)(+g‘(Poly1‘𝐾))((algSc‘(Poly1‘𝐾))‘((ℤRHom‘𝐾)‘𝑎)))) & ⊢ (𝜑 → (𝑥 ∈ (Base‘𝐾) ↦ (𝑃(.g‘(mulGrp‘𝐾))𝑥)) ∈ (𝐾 RingIso 𝐾)) & ⊢ (𝜑 → 𝑀 ∈ ((mulGrp‘𝐾) PrimRoots 𝑅)) & ⊢ 𝐻 = (ℎ ∈ (ℕ0 ↑m (0...𝐴)) ↦ (((eval1‘𝐾)‘(𝐺‘ℎ))‘𝑀)) & ⊢ 𝐵 = (⌊‘(√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 × ℕ0)))))) & ⊢ 𝐶 = (𝐸 “ ((0...𝐵) × (0...𝐵))) & ⊢ (𝜑 → 𝐼 ∈ 𝐶) & ⊢ (𝜑 → 𝐽 ∈ 𝐶) & ⊢ (𝜑 → 𝐼 < 𝐽) & ⊢ ↑ = (.g‘(mulGrp‘(Poly1‘𝐾))) & ⊢ 𝑋 = (var1‘𝐾) & ⊢ 𝑆 = ((𝐽 ↑ 𝑋)(-g‘(Poly1‘𝐾))(𝐼 ↑ 𝑋)) & ⊢ (𝜑 → 𝑈 ∈ ℕ) & ⊢ (𝜑 → 𝐽 = (𝐼 + (𝑈 · 𝑅))) ⇒ ⊢ (𝜑 → (♯‘(𝐻 “ (ℕ0 ↑m (0...𝐴)))) ≤ (𝑁↑𝐵)) | ||
Theorem | hashnexinj 41599* | If the number of elements of the domain are greater than the number of elements in a codomain, then there are two different values that map to the same. (Contributed by metakunt, 2-May-2025.) |
⊢ (𝜑 → 𝐴 ∈ Fin) & ⊢ (𝜑 → 𝐵 ∈ Fin) & ⊢ (𝜑 → (♯‘𝐵) < (♯‘𝐴)) & ⊢ (𝜑 → 𝐹:𝐴⟶𝐵) ⇒ ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐴 ((𝐹‘𝑥) = (𝐹‘𝑦) ∧ 𝑥 ≠ 𝑦)) | ||
Theorem | hashnexinjle 41600* | If the number of elements of the domain are greater than the number of elements in a codomain, then there are two different values that map to the same. Also we introduce a one sided inequality to simplify a duplicateable proof. (Contributed by metakunt, 2-May-2025.) |
⊢ (𝜑 → 𝐴 ∈ Fin) & ⊢ (𝜑 → 𝐵 ∈ Fin) & ⊢ (𝜑 → (♯‘𝐵) < (♯‘𝐴)) & ⊢ (𝜑 → 𝐹:𝐴⟶𝐵) & ⊢ (𝜑 → 𝐴 ⊆ ℝ) ⇒ ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐴 ((𝐹‘𝑥) = (𝐹‘𝑦) ∧ 𝑥 < 𝑦)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |