| Metamath
Proof Explorer Theorem List (p. 422 of 494) | < 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-30937) |
(30938-32460) |
(32461-49324) |
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Theorem | posbezout 42101* | Bezout's identity restricted on positive integers in all but one variable. (Contributed by metakunt, 26-Apr-2025.) |
| ⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) → ∃𝑥 ∈ ℕ ∃𝑦 ∈ ℤ (𝐴 gcd 𝐵) = ((𝐴 · 𝑥) + (𝐵 · 𝑦))) | ||
| Theorem | primrootscoprf 42102* | 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 42103* | 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 42104* | 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 42105* | Division with rest. (Contributed by metakunt, 15-May-2025.) |
| ⊢ (𝜑 → 𝑁 ∈ ℤ) & ⊢ (𝜑 → 𝐴 ∈ ℕ) ⇒ ⊢ (𝜑 → ∃𝑥 ∈ ℤ ∃𝑦 ∈ (0...(𝐴 − 1))𝑁 = ((𝑥 · 𝐴) + 𝑦)) | ||
| Theorem | primrootlekpowne0 42106 | 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 42107* | 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 42108* | Definition of the introspective relation. (Contributed by metakunt, 25-Apr-2025.) |
| ⊢ ∼ = {〈𝑒, 𝑓〉 ∣ (𝑒 ∈ ℕ ∧ 𝑓 ∈ 𝐵 ∧ ∀𝑦 ∈ (𝐾 PrimRoots 𝑅)(𝑒 ↑ ((𝑂‘𝑓)‘𝑦)) = ((𝑂‘𝑓)‘(𝑒𝐷𝑦)))} & ⊢ (𝜑 → 𝐹 ∈ 𝐵) & ⊢ (𝜑 → 𝐸 ∈ ℕ) ⇒ ⊢ (𝜑 → (𝐸 ∼ 𝐹 ↔ ∀𝑦 ∈ (𝐾 PrimRoots 𝑅)(𝐸 ↑ ((𝑂‘𝐹)‘𝑦)) = ((𝑂‘𝐹)‘(𝐸𝐷𝑦)))) | ||
| Theorem | aks6d1c1p1rcl 42109* | Reverse closure of the introspective relation. (Contributed by metakunt, 25-Apr-2025.) |
| ⊢ ∼ = {〈𝑒, 𝑓〉 ∣ (𝑒 ∈ ℕ ∧ 𝑓 ∈ 𝐵 ∧ ∀𝑦 ∈ (𝐾 PrimRoots 𝑅)(𝑒 ↑ ((𝑂‘𝑓)‘𝑦)) = ((𝑂‘𝑓)‘(𝑒𝐷𝑦)))} & ⊢ (𝜑 → 𝐸 ∼ 𝐹) ⇒ ⊢ (𝜑 → (𝐸 ∈ ℕ ∧ 𝐹 ∈ 𝐵)) | ||
| Theorem | aks6d1c1p2 42110* | 𝑃 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 42111* | 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 42112* | 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 42113* | 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 42114* | 𝑋 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 42115* | 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 42116* | 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 42117* | 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 42118* | 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 42119* | 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 42120* | 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 42121 | 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 42122 | Helper lemma for to prove inequality in Zr. (Contributed by metakunt, 28-Apr-2025.) |
| ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 𝐴 ∈ (1...((odℤ‘𝑅)‘𝑁))) & ⊢ (𝜑 → 𝐵 ∈ (1...((odℤ‘𝑅)‘𝑁))) & ⊢ (𝜑 → 𝑅 ∈ ℕ) & ⊢ (𝜑 → (𝑁 gcd 𝑅) = 1) & ⊢ 𝐿 = (ℤRHom‘𝑌) & ⊢ 𝑌 = (ℤ/nℤ‘𝑅) & ⊢ (𝜑 → 𝐴 < 𝐵) ⇒ ⊢ (𝜑 → (𝐿‘(𝑁↑𝐴)) ≠ (𝐿‘(𝑁↑𝐵))) | ||
| Theorem | hashscontpow 42123* | 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 42124* | 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 42125* | 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 42126* | 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 42127* | Lemma for aks6d1c2 42131 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 42128* | 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 42129* | 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 42130* | 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) & ⊢ (𝜑 → (♯‘𝐵) < (♯‘𝐴)) & ⊢ (𝜑 → 𝐹:𝐴⟶𝐵) & ⊢ (𝜑 → 𝐴 ⊆ ℝ) ⇒ ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐴 ((𝐹‘𝑥) = (𝐹‘𝑦) ∧ 𝑥 < 𝑦)) | ||
| Theorem | aks6d1c2 42131* | Claim 2 of Theorem 6.1 of https://www3.nd.edu/%7eandyp/notes/AKS.pdf (Contributed by metakunt, 2-May-2025.) |
| ⊢ ∼ = {〈𝑒, 𝑓〉 ∣ (𝑒 ∈ ℕ ∧ 𝑓 ∈ (Base‘(Poly1‘𝐾)) ∧ ∀𝑦 ∈ ((mulGrp‘𝐾) PrimRoots 𝑅)(𝑒(.g‘(mulGrp‘𝐾))(((eval1‘𝐾)‘𝑓)‘𝑦)) = (((eval1‘𝐾)‘𝑓)‘(𝑒(.g‘(mulGrp‘𝐾))𝑦)))} & ⊢ 𝑃 = (chr‘𝐾) & ⊢ (𝜑 → 𝐾 ∈ Field) & ⊢ (𝜑 → 𝑃 ∈ ℙ) & ⊢ (𝜑 → 𝑅 ∈ ℕ) & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 𝑃 ∥ 𝑁) & ⊢ (𝜑 → (𝑁 gcd 𝑅) = 1) & ⊢ 𝐺 = (𝑔 ∈ (ℕ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...𝐵))) & ⊢ (𝜑 → (𝑄 ∈ ℙ ∧ 𝑄 ∥ 𝑁 ∧ 𝑃 ≠ 𝑄)) ⇒ ⊢ (𝜑 → (♯‘(𝐻 “ (ℕ0 ↑m (0...𝐴)))) ≤ (𝑁↑𝐵)) | ||
| Theorem | rspcsbnea 42132* | Special case related to rspsbc 3879. (Contributed by metakunt, 5-May-2025.) |
| ⊢ ((𝐴 ∈ 𝐵 ∧ ∀𝑥 ∈ 𝐵 𝐶 ≠ 𝐷) → ⦋𝐴 / 𝑥⦌𝐶 ≠ 𝐷) | ||
| Theorem | idomnnzpownz 42133 | A non-zero power in an integral domain is non-zero. (Contributed by metakunt, 5-May-2025.) |
| ⊢ (𝜑 → 𝑅 ∈ IDomn) & ⊢ (𝜑 → 𝐴 ∈ (Base‘𝑅)) & ⊢ (𝜑 → 𝐴 ≠ (0g‘𝑅)) & ⊢ (𝜑 → 𝑁 ∈ ℕ0) & ⊢ ↑ = (.g‘(mulGrp‘𝑅)) ⇒ ⊢ (𝜑 → (𝑁 ↑ 𝐴) ≠ (0g‘𝑅)) | ||
| Theorem | idomnnzgmulnz 42134* | A finite product of non-zero elements in an integral domain is non-zero. (Contributed by metakunt, 5-May-2025.) |
| ⊢ 𝐺 = (mulGrp‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ IDomn) & ⊢ (𝜑 → 𝑁 ∈ Fin) & ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑁) → 𝐴 ∈ (Base‘𝑅)) & ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑁) → 𝐴 ≠ (0g‘𝑅)) ⇒ ⊢ (𝜑 → (𝐺 Σg (𝑛 ∈ 𝑁 ↦ 𝐴)) ≠ (0g‘𝑅)) | ||
| Theorem | ringexp0nn 42135 | Zero to the power of a positive integer is zero. (Contributed by metakunt, 5-May-2025.) |
| ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ ↑ = (.g‘(mulGrp‘𝑅)) ⇒ ⊢ (𝜑 → (𝑁 ↑ (0g‘𝑅)) = (0g‘𝑅)) | ||
| Theorem | aks6d1c5lem0 42136* | Lemma for Claim 5 of Theorem 6.1, G defines a map into the polynomials. (Contributed by metakunt, 5-May-2025.) |
| ⊢ (𝜑 → 𝐾 ∈ Field) & ⊢ (𝜑 → 𝑃 ∈ ℙ) & ⊢ 𝑃 = (chr‘𝐾) & ⊢ (𝜑 → 𝐴 ∈ ℕ0) & ⊢ (𝜑 → 𝐴 < 𝑃) & ⊢ 𝑋 = (var1‘𝐾) & ⊢ ↑ = (.g‘(mulGrp‘(Poly1‘𝐾))) & ⊢ 𝐺 = (𝑔 ∈ (ℕ0 ↑m (0...𝐴)) ↦ ((mulGrp‘(Poly1‘𝐾)) Σg (𝑖 ∈ (0...𝐴) ↦ ((𝑔‘𝑖) ↑ (𝑋(+g‘(Poly1‘𝐾))((algSc‘(Poly1‘𝐾))‘((ℤRHom‘𝐾)‘𝑖))))))) ⇒ ⊢ (𝜑 → 𝐺:(ℕ0 ↑m (0...𝐴))⟶(Base‘(Poly1‘𝐾))) | ||
| Theorem | aks6d1c5lem1 42137 | Lemma for claim 5, evaluate the linear factor at -c to get a root. (Contributed by metakunt, 5-May-2025.) |
| ⊢ (𝜑 → 𝐾 ∈ Field) & ⊢ (𝜑 → 𝑃 ∈ ℙ) & ⊢ 𝑃 = (chr‘𝐾) & ⊢ (𝜑 → 𝐴 ∈ ℕ0) & ⊢ (𝜑 → 𝐴 < 𝑃) & ⊢ 𝑋 = (var1‘𝐾) & ⊢ ↑ = (.g‘(mulGrp‘(Poly1‘𝐾))) & ⊢ 𝐺 = (𝑔 ∈ (ℕ0 ↑m (0...𝐴)) ↦ ((mulGrp‘(Poly1‘𝐾)) Σg (𝑖 ∈ (0...𝐴) ↦ ((𝑔‘𝑖) ↑ (𝑋(+g‘(Poly1‘𝐾))((algSc‘(Poly1‘𝐾))‘((ℤRHom‘𝐾)‘𝑖))))))) & ⊢ (𝜑 → 𝐵 ∈ (0...𝐴)) & ⊢ (𝜑 → 𝐶 ∈ (0...𝐴)) ⇒ ⊢ (𝜑 → (𝐵 = 𝐶 ↔ (((eval1‘𝐾)‘(𝑋(+g‘(Poly1‘𝐾))((algSc‘(Poly1‘𝐾))‘((ℤRHom‘𝐾)‘𝐵))))‘((ℤRHom‘𝐾)‘(0 − 𝐶))) = (0g‘𝐾))) | ||
| Theorem | aks6d1c5lem3 42138* | Lemma for Claim 5, polynomial division with a linear power. (Contributed by metakunt, 5-May-2025.) |
| ⊢ (𝜑 → 𝐾 ∈ Field) & ⊢ (𝜑 → 𝑃 ∈ ℙ) & ⊢ 𝑃 = (chr‘𝐾) & ⊢ (𝜑 → 𝐴 ∈ ℕ0) & ⊢ (𝜑 → 𝐴 < 𝑃) & ⊢ 𝑋 = (var1‘𝐾) & ⊢ ↑ = (.g‘(mulGrp‘(Poly1‘𝐾))) & ⊢ 𝐺 = (𝑔 ∈ (ℕ0 ↑m (0...𝐴)) ↦ ((mulGrp‘(Poly1‘𝐾)) Σg (𝑖 ∈ (0...𝐴) ↦ ((𝑔‘𝑖) ↑ (𝑋(+g‘(Poly1‘𝐾))((algSc‘(Poly1‘𝐾))‘((ℤRHom‘𝐾)‘𝑖))))))) & ⊢ (𝜑 → 𝑌 ∈ (ℕ0 ↑m (0...𝐴))) & ⊢ (𝜑 → 𝑊 ∈ (0...𝐴)) & ⊢ (𝜑 → 𝐶 ∈ ℕ0) & ⊢ (𝜑 → 𝐶 ≤ (𝑌‘𝑊)) & ⊢ 𝑄 = (quot1p‘𝐾) & ⊢ 𝑆 = (algSc‘(Poly1‘𝐾)) & ⊢ 𝑀 = (mulGrp‘(Poly1‘𝐾)) ⇒ ⊢ (𝜑 → ((𝐺‘𝑌)𝑄(𝐶 ↑ (𝑋(+g‘(Poly1‘𝐾))(𝑆‘((ℤRHom‘𝐾)‘𝑊))))) = ((((𝑌‘𝑊) − 𝐶) ↑ (𝑋(+g‘(Poly1‘𝐾))(𝑆‘((ℤRHom‘𝐾)‘𝑊))))(+g‘𝑀)(𝑀 Σg (𝑖 ∈ ((0...𝐴) ∖ {𝑊}) ↦ ((𝑌‘𝑖) ↑ (𝑋(+g‘(Poly1‘𝐾))(𝑆‘((ℤRHom‘𝐾)‘𝑖)))))))) | ||
| Theorem | aks6d1c5lem2 42139* | Lemma for Claim 5, contradiction of different evaluations that map to the same. (Contributed by metakunt, 5-May-2025.) |
| ⊢ (𝜑 → 𝐾 ∈ Field) & ⊢ (𝜑 → 𝑃 ∈ ℙ) & ⊢ 𝑃 = (chr‘𝐾) & ⊢ (𝜑 → 𝐴 ∈ ℕ0) & ⊢ (𝜑 → 𝐴 < 𝑃) & ⊢ 𝑋 = (var1‘𝐾) & ⊢ ↑ = (.g‘(mulGrp‘(Poly1‘𝐾))) & ⊢ 𝐺 = (𝑔 ∈ (ℕ0 ↑m (0...𝐴)) ↦ ((mulGrp‘(Poly1‘𝐾)) Σg (𝑖 ∈ (0...𝐴) ↦ ((𝑔‘𝑖) ↑ (𝑋(+g‘(Poly1‘𝐾))((algSc‘(Poly1‘𝐾))‘((ℤRHom‘𝐾)‘𝑖))))))) & ⊢ (𝜑 → 𝑌 ∈ (ℕ0 ↑m (0...𝐴))) & ⊢ (𝜑 → 𝑍 ∈ (ℕ0 ↑m (0...𝐴))) & ⊢ (𝜑 → (𝐺‘𝑌) = (𝐺‘𝑍)) & ⊢ (𝜑 → 𝑊 ∈ (0...𝐴)) & ⊢ (𝜑 → (𝑌‘𝑊) < (𝑍‘𝑊)) ⇒ ⊢ (𝜑 → (0g‘𝐾) ≠ (0g‘𝐾)) | ||
| Theorem | aks6d1c5 42140* | Claim 5 of Theorem 6.1 https://www3.nd.edu/%7eandyp/notes/AKS.pdf. The mapping defined by 𝐺 is injective. (Contributed by metakunt, 5-May-2025.) |
| ⊢ (𝜑 → 𝐾 ∈ Field) & ⊢ (𝜑 → 𝑃 ∈ ℙ) & ⊢ 𝑃 = (chr‘𝐾) & ⊢ (𝜑 → 𝐴 ∈ ℕ0) & ⊢ (𝜑 → 𝐴 < 𝑃) & ⊢ 𝑋 = (var1‘𝐾) & ⊢ ↑ = (.g‘(mulGrp‘(Poly1‘𝐾))) & ⊢ 𝐺 = (𝑔 ∈ (ℕ0 ↑m (0...𝐴)) ↦ ((mulGrp‘(Poly1‘𝐾)) Σg (𝑖 ∈ (0...𝐴) ↦ ((𝑔‘𝑖) ↑ (𝑋(+g‘(Poly1‘𝐾))((algSc‘(Poly1‘𝐾))‘((ℤRHom‘𝐾)‘𝑖))))))) ⇒ ⊢ (𝜑 → 𝐺:(ℕ0 ↑m (0...𝐴))–1-1→(Base‘(Poly1‘𝐾))) | ||
| Theorem | deg1gprod 42141* | Degree multiplication is a homomorphism. (Contributed by metakunt, 6-May-2025.) |
| ⊢ (𝜑 → 𝑅 ∈ IDomn) & ⊢ (𝜑 → 𝑁 ∈ Fin) & ⊢ (𝜑 → ∀𝑥 ∈ 𝑁 (𝐶 ∈ (Base‘(Poly1‘𝑅)) ∧ 𝐶 ≠ (0g‘(Poly1‘𝑅)))) ⇒ ⊢ (𝜑 → (((deg1‘𝑅)‘((mulGrp‘(Poly1‘𝑅)) Σg (𝑥 ∈ 𝑁 ↦ 𝐶))) = Σ𝑛 ∈ 𝑁 ((deg1‘𝑅)‘((𝑥 ∈ 𝑁 ↦ 𝐶)‘𝑛)) ∧ 0 ≤ ((deg1‘𝑅)‘((mulGrp‘(Poly1‘𝑅)) Σg (𝑥 ∈ 𝑁 ↦ 𝐶))))) | ||
| Theorem | deg1pow 42142 | Exact degree of a power of a polynomial in an integral domain. (Contributed by metakunt, 6-May-2025.) |
| ⊢ (𝜑 → 𝑅 ∈ IDomn) & ⊢ (𝜑 → 𝐹 ∈ (Base‘(Poly1‘𝑅))) & ⊢ (𝜑 → 𝐹 ≠ (0g‘(Poly1‘𝑅))) & ⊢ (𝜑 → 𝐴 ∈ ℕ0) & ⊢ ↑ = (.g‘(mulGrp‘(Poly1‘𝑅))) & ⊢ 𝐷 = (deg1‘𝑅) ⇒ ⊢ (𝜑 → (𝐷‘(𝐴 ↑ 𝐹)) = (𝐴 · (𝐷‘𝐹))) | ||
| Theorem | 5bc2eq10 42143 | The value of 5 choose 2. (Contributed by metakunt, 8-Jun-2024.) |
| ⊢ (5C2) = ;10 | ||
| Theorem | facp2 42144 | The factorial of a successor's successor. (Contributed by metakunt, 19-Apr-2024.) |
| ⊢ (𝑁 ∈ ℕ0 → (!‘(𝑁 + 2)) = ((!‘𝑁) · ((𝑁 + 1) · (𝑁 + 2)))) | ||
| Theorem | 2np3bcnp1 42145 | Part of induction step for 2ap1caineq 42146. (Contributed by metakunt, 8-Jun-2024.) |
| ⊢ (𝜑 → 𝑁 ∈ ℕ0) ⇒ ⊢ (𝜑 → (((2 · (𝑁 + 1)) + 1)C(𝑁 + 1)) = ((((2 · 𝑁) + 1)C𝑁) · (2 · (((2 · 𝑁) + 3) / (𝑁 + 2))))) | ||
| Theorem | 2ap1caineq 42146 | Inequality for Theorem 6.6 for AKS. (Contributed by metakunt, 8-Jun-2024.) |
| ⊢ (𝜑 → 𝑁 ∈ ℤ) & ⊢ (𝜑 → 2 ≤ 𝑁) ⇒ ⊢ (𝜑 → (2↑(𝑁 + 1)) < (((2 · 𝑁) + 1)C𝑁)) | ||
| Theorem | sticksstones1 42147* | Different strictly monotone functions have different ranges. (Contributed by metakunt, 27-Sep-2024.) |
| ⊢ (𝜑 → 𝑁 ∈ ℕ0) & ⊢ (𝜑 → 𝐾 ∈ ℕ0) & ⊢ 𝐴 = {𝑓 ∣ (𝑓:(1...𝐾)⟶(1...𝑁) ∧ ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑓‘𝑥) < (𝑓‘𝑦)))} & ⊢ (𝜑 → 𝑋 ∈ 𝐴) & ⊢ (𝜑 → 𝑌 ∈ 𝐴) & ⊢ (𝜑 → 𝑋 ≠ 𝑌) & ⊢ 𝐼 = inf({𝑧 ∈ (1...𝐾) ∣ (𝑋‘𝑧) ≠ (𝑌‘𝑧)}, ℝ, < ) ⇒ ⊢ (𝜑 → ran 𝑋 ≠ ran 𝑌) | ||
| Theorem | sticksstones2 42148* | The range function on strictly monotone functions with finite domain and codomain is an injective mapping onto 𝐾-elemental sets. (Contributed by metakunt, 27-Sep-2024.) |
| ⊢ (𝜑 → 𝑁 ∈ ℕ0) & ⊢ (𝜑 → 𝐾 ∈ ℕ0) & ⊢ 𝐵 = {𝑎 ∈ 𝒫 (1...𝑁) ∣ (♯‘𝑎) = 𝐾} & ⊢ 𝐴 = {𝑓 ∣ (𝑓:(1...𝐾)⟶(1...𝑁) ∧ ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑓‘𝑥) < (𝑓‘𝑦)))} & ⊢ 𝐹 = (𝑧 ∈ 𝐴 ↦ ran 𝑧) ⇒ ⊢ (𝜑 → 𝐹:𝐴–1-1→𝐵) | ||
| Theorem | sticksstones3 42149* | The range function on strictly monotone functions with finite domain and codomain is an surjective mapping onto 𝐾-elemental sets. (Contributed by metakunt, 28-Sep-2024.) |
| ⊢ (𝜑 → 𝑁 ∈ ℕ0) & ⊢ (𝜑 → 𝐾 ∈ ℕ0) & ⊢ 𝐵 = {𝑎 ∈ 𝒫 (1...𝑁) ∣ (♯‘𝑎) = 𝐾} & ⊢ 𝐴 = {𝑓 ∣ (𝑓:(1...𝐾)⟶(1...𝑁) ∧ ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑓‘𝑥) < (𝑓‘𝑦)))} & ⊢ 𝐹 = (𝑧 ∈ 𝐴 ↦ ran 𝑧) ⇒ ⊢ (𝜑 → 𝐹:𝐴–onto→𝐵) | ||
| Theorem | sticksstones4 42150* | Equinumerosity lemma for sticks and stones. (Contributed by metakunt, 28-Sep-2024.) |
| ⊢ (𝜑 → 𝑁 ∈ ℕ0) & ⊢ (𝜑 → 𝐾 ∈ ℕ0) & ⊢ 𝐵 = {𝑎 ∈ 𝒫 (1...𝑁) ∣ (♯‘𝑎) = 𝐾} & ⊢ 𝐴 = {𝑓 ∣ (𝑓:(1...𝐾)⟶(1...𝑁) ∧ ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑓‘𝑥) < (𝑓‘𝑦)))} ⇒ ⊢ (𝜑 → 𝐴 ≈ 𝐵) | ||
| Theorem | sticksstones5 42151* | Count the number of strictly monotonely increasing functions on finite domains and codomains. (Contributed by metakunt, 28-Sep-2024.) |
| ⊢ (𝜑 → 𝑁 ∈ ℕ0) & ⊢ (𝜑 → 𝐾 ∈ ℕ0) & ⊢ 𝐴 = {𝑓 ∣ (𝑓:(1...𝐾)⟶(1...𝑁) ∧ ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑓‘𝑥) < (𝑓‘𝑦)))} ⇒ ⊢ (𝜑 → (♯‘𝐴) = (𝑁C𝐾)) | ||
| Theorem | sticksstones6 42152* | Function induces an order isomorphism for sticks and stones theorem. (Contributed by metakunt, 1-Oct-2024.) |
| ⊢ (𝜑 → 𝑁 ∈ ℕ0) & ⊢ (𝜑 → 𝐾 ∈ ℕ0) & ⊢ (𝜑 → 𝐺:(1...(𝐾 + 1))⟶ℕ0) & ⊢ (𝜑 → 𝑋 ∈ (1...𝐾)) & ⊢ (𝜑 → 𝑌 ∈ (1...𝐾)) & ⊢ (𝜑 → 𝑋 < 𝑌) & ⊢ 𝐹 = (𝑥 ∈ (1...𝐾) ↦ (𝑥 + Σ𝑖 ∈ (1...𝑥)(𝐺‘𝑖))) ⇒ ⊢ (𝜑 → (𝐹‘𝑋) < (𝐹‘𝑌)) | ||
| Theorem | sticksstones7 42153* | Closure property of sticks and stones function. (Contributed by metakunt, 1-Oct-2024.) |
| ⊢ (𝜑 → 𝑁 ∈ ℕ0) & ⊢ (𝜑 → 𝐾 ∈ ℕ0) & ⊢ (𝜑 → 𝐺:(1...(𝐾 + 1))⟶ℕ0) & ⊢ (𝜑 → 𝑋 ∈ (1...𝐾)) & ⊢ 𝐹 = (𝑥 ∈ (1...𝐾) ↦ (𝑥 + Σ𝑖 ∈ (1...𝑥)(𝐺‘𝑖))) & ⊢ (𝜑 → Σ𝑖 ∈ (1...(𝐾 + 1))(𝐺‘𝑖) = 𝑁) ⇒ ⊢ (𝜑 → (𝐹‘𝑋) ∈ (1...(𝑁 + 𝐾))) | ||
| Theorem | sticksstones8 42154* | Establish mapping between strictly monotone functions and functions that sum to a fixed non-negative integer. (Contributed by metakunt, 1-Oct-2024.) |
| ⊢ (𝜑 → 𝑁 ∈ ℕ0) & ⊢ (𝜑 → 𝐾 ∈ ℕ0) & ⊢ 𝐹 = (𝑎 ∈ 𝐴 ↦ (𝑗 ∈ (1...𝐾) ↦ (𝑗 + Σ𝑙 ∈ (1...𝑗)(𝑎‘𝑙)))) & ⊢ 𝐴 = {𝑔 ∣ (𝑔:(1...(𝐾 + 1))⟶ℕ0 ∧ Σ𝑖 ∈ (1...(𝐾 + 1))(𝑔‘𝑖) = 𝑁)} & ⊢ 𝐵 = {𝑓 ∣ (𝑓:(1...𝐾)⟶(1...(𝑁 + 𝐾)) ∧ ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑓‘𝑥) < (𝑓‘𝑦)))} ⇒ ⊢ (𝜑 → 𝐹:𝐴⟶𝐵) | ||
| Theorem | sticksstones9 42155* | Establish mapping between strictly monotone functions and functions that sum to a fixed non-negative integer. (Contributed by metakunt, 6-Oct-2024.) |
| ⊢ (𝜑 → 𝑁 ∈ ℕ0) & ⊢ (𝜑 → 𝐾 = 0) & ⊢ 𝐺 = (𝑏 ∈ 𝐵 ↦ if(𝐾 = 0, {〈1, 𝑁〉}, (𝑘 ∈ (1...(𝐾 + 1)) ↦ if(𝑘 = (𝐾 + 1), ((𝑁 + 𝐾) − (𝑏‘𝐾)), if(𝑘 = 1, ((𝑏‘1) − 1), (((𝑏‘𝑘) − (𝑏‘(𝑘 − 1))) − 1)))))) & ⊢ 𝐴 = {𝑔 ∣ (𝑔:(1...(𝐾 + 1))⟶ℕ0 ∧ Σ𝑖 ∈ (1...(𝐾 + 1))(𝑔‘𝑖) = 𝑁)} & ⊢ 𝐵 = {𝑓 ∣ (𝑓:(1...𝐾)⟶(1...(𝑁 + 𝐾)) ∧ ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑓‘𝑥) < (𝑓‘𝑦)))} ⇒ ⊢ (𝜑 → 𝐺:𝐵⟶𝐴) | ||
| Theorem | sticksstones10 42156* | Establish mapping between strictly monotone functions and functions that sum to a fixed non-negative integer. (Contributed by metakunt, 6-Oct-2024.) |
| ⊢ (𝜑 → 𝑁 ∈ ℕ0) & ⊢ (𝜑 → 𝐾 ∈ ℕ) & ⊢ 𝐺 = (𝑏 ∈ 𝐵 ↦ if(𝐾 = 0, {〈1, 𝑁〉}, (𝑘 ∈ (1...(𝐾 + 1)) ↦ if(𝑘 = (𝐾 + 1), ((𝑁 + 𝐾) − (𝑏‘𝐾)), if(𝑘 = 1, ((𝑏‘1) − 1), (((𝑏‘𝑘) − (𝑏‘(𝑘 − 1))) − 1)))))) & ⊢ 𝐴 = {𝑔 ∣ (𝑔:(1...(𝐾 + 1))⟶ℕ0 ∧ Σ𝑖 ∈ (1...(𝐾 + 1))(𝑔‘𝑖) = 𝑁)} & ⊢ 𝐵 = {𝑓 ∣ (𝑓:(1...𝐾)⟶(1...(𝑁 + 𝐾)) ∧ ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑓‘𝑥) < (𝑓‘𝑦)))} ⇒ ⊢ (𝜑 → 𝐺:𝐵⟶𝐴) | ||
| Theorem | sticksstones11 42157* | Establish bijective mapping between strictly monotone functions and functions that sum to a fixed non-negative integer. (Contributed by metakunt, 6-Oct-2024.) |
| ⊢ (𝜑 → 𝑁 ∈ ℕ0) & ⊢ (𝜑 → 𝐾 = 0) & ⊢ 𝐹 = (𝑎 ∈ 𝐴 ↦ (𝑗 ∈ (1...𝐾) ↦ (𝑗 + Σ𝑙 ∈ (1...𝑗)(𝑎‘𝑙)))) & ⊢ 𝐺 = (𝑏 ∈ 𝐵 ↦ if(𝐾 = 0, {〈1, 𝑁〉}, (𝑘 ∈ (1...(𝐾 + 1)) ↦ if(𝑘 = (𝐾 + 1), ((𝑁 + 𝐾) − (𝑏‘𝐾)), if(𝑘 = 1, ((𝑏‘1) − 1), (((𝑏‘𝑘) − (𝑏‘(𝑘 − 1))) − 1)))))) & ⊢ 𝐴 = {𝑔 ∣ (𝑔:(1...(𝐾 + 1))⟶ℕ0 ∧ Σ𝑖 ∈ (1...(𝐾 + 1))(𝑔‘𝑖) = 𝑁)} & ⊢ 𝐵 = {𝑓 ∣ (𝑓:(1...𝐾)⟶(1...(𝑁 + 𝐾)) ∧ ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑓‘𝑥) < (𝑓‘𝑦)))} ⇒ ⊢ (𝜑 → 𝐹:𝐴–1-1-onto→𝐵) | ||
| Theorem | sticksstones12a 42158* | Establish bijective mapping between strictly monotone functions and functions that sum to a fixed non-negative integer. (Contributed by metakunt, 11-Oct-2024.) |
| ⊢ (𝜑 → 𝑁 ∈ ℕ0) & ⊢ (𝜑 → 𝐾 ∈ ℕ) & ⊢ 𝐹 = (𝑎 ∈ 𝐴 ↦ (𝑗 ∈ (1...𝐾) ↦ (𝑗 + Σ𝑙 ∈ (1...𝑗)(𝑎‘𝑙)))) & ⊢ 𝐺 = (𝑏 ∈ 𝐵 ↦ if(𝐾 = 0, {〈1, 𝑁〉}, (𝑘 ∈ (1...(𝐾 + 1)) ↦ if(𝑘 = (𝐾 + 1), ((𝑁 + 𝐾) − (𝑏‘𝐾)), if(𝑘 = 1, ((𝑏‘1) − 1), (((𝑏‘𝑘) − (𝑏‘(𝑘 − 1))) − 1)))))) & ⊢ 𝐴 = {𝑔 ∣ (𝑔:(1...(𝐾 + 1))⟶ℕ0 ∧ Σ𝑖 ∈ (1...(𝐾 + 1))(𝑔‘𝑖) = 𝑁)} & ⊢ 𝐵 = {𝑓 ∣ (𝑓:(1...𝐾)⟶(1...(𝑁 + 𝐾)) ∧ ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑓‘𝑥) < (𝑓‘𝑦)))} ⇒ ⊢ (𝜑 → ∀𝑑 ∈ 𝐵 (𝐹‘(𝐺‘𝑑)) = 𝑑) | ||
| Theorem | sticksstones12 42159* | Establish bijective mapping between strictly monotone functions and functions that sum to a fixed non-negative integer. (Contributed by metakunt, 6-Oct-2024.) |
| ⊢ (𝜑 → 𝑁 ∈ ℕ0) & ⊢ (𝜑 → 𝐾 ∈ ℕ) & ⊢ 𝐹 = (𝑎 ∈ 𝐴 ↦ (𝑗 ∈ (1...𝐾) ↦ (𝑗 + Σ𝑙 ∈ (1...𝑗)(𝑎‘𝑙)))) & ⊢ 𝐺 = (𝑏 ∈ 𝐵 ↦ if(𝐾 = 0, {〈1, 𝑁〉}, (𝑘 ∈ (1...(𝐾 + 1)) ↦ if(𝑘 = (𝐾 + 1), ((𝑁 + 𝐾) − (𝑏‘𝐾)), if(𝑘 = 1, ((𝑏‘1) − 1), (((𝑏‘𝑘) − (𝑏‘(𝑘 − 1))) − 1)))))) & ⊢ 𝐴 = {𝑔 ∣ (𝑔:(1...(𝐾 + 1))⟶ℕ0 ∧ Σ𝑖 ∈ (1...(𝐾 + 1))(𝑔‘𝑖) = 𝑁)} & ⊢ 𝐵 = {𝑓 ∣ (𝑓:(1...𝐾)⟶(1...(𝑁 + 𝐾)) ∧ ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑓‘𝑥) < (𝑓‘𝑦)))} ⇒ ⊢ (𝜑 → 𝐹:𝐴–1-1-onto→𝐵) | ||
| Theorem | sticksstones13 42160* | Establish bijective mapping between strictly monotone functions and functions that sum to a fixed non-negative integer. (Contributed by metakunt, 6-Oct-2024.) |
| ⊢ (𝜑 → 𝑁 ∈ ℕ0) & ⊢ (𝜑 → 𝐾 ∈ ℕ0) & ⊢ 𝐹 = (𝑎 ∈ 𝐴 ↦ (𝑗 ∈ (1...𝐾) ↦ (𝑗 + Σ𝑙 ∈ (1...𝑗)(𝑎‘𝑙)))) & ⊢ 𝐺 = (𝑏 ∈ 𝐵 ↦ if(𝐾 = 0, {〈1, 𝑁〉}, (𝑘 ∈ (1...(𝐾 + 1)) ↦ if(𝑘 = (𝐾 + 1), ((𝑁 + 𝐾) − (𝑏‘𝐾)), if(𝑘 = 1, ((𝑏‘1) − 1), (((𝑏‘𝑘) − (𝑏‘(𝑘 − 1))) − 1)))))) & ⊢ 𝐴 = {𝑔 ∣ (𝑔:(1...(𝐾 + 1))⟶ℕ0 ∧ Σ𝑖 ∈ (1...(𝐾 + 1))(𝑔‘𝑖) = 𝑁)} & ⊢ 𝐵 = {𝑓 ∣ (𝑓:(1...𝐾)⟶(1...(𝑁 + 𝐾)) ∧ ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑓‘𝑥) < (𝑓‘𝑦)))} ⇒ ⊢ (𝜑 → 𝐹:𝐴–1-1-onto→𝐵) | ||
| Theorem | sticksstones14 42161* | Sticks and stones with definitions as hypotheses. (Contributed by metakunt, 7-Oct-2024.) |
| ⊢ (𝜑 → 𝑁 ∈ ℕ0) & ⊢ (𝜑 → 𝐾 ∈ ℕ0) & ⊢ 𝐹 = (𝑎 ∈ 𝐴 ↦ (𝑗 ∈ (1...𝐾) ↦ (𝑗 + Σ𝑙 ∈ (1...𝑗)(𝑎‘𝑙)))) & ⊢ 𝐺 = (𝑏 ∈ 𝐵 ↦ if(𝐾 = 0, {〈1, 𝑁〉}, (𝑘 ∈ (1...(𝐾 + 1)) ↦ if(𝑘 = (𝐾 + 1), ((𝑁 + 𝐾) − (𝑏‘𝐾)), if(𝑘 = 1, ((𝑏‘1) − 1), (((𝑏‘𝑘) − (𝑏‘(𝑘 − 1))) − 1)))))) & ⊢ 𝐴 = {𝑔 ∣ (𝑔:(1...(𝐾 + 1))⟶ℕ0 ∧ Σ𝑖 ∈ (1...(𝐾 + 1))(𝑔‘𝑖) = 𝑁)} & ⊢ 𝐵 = {𝑓 ∣ (𝑓:(1...𝐾)⟶(1...(𝑁 + 𝐾)) ∧ ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑓‘𝑥) < (𝑓‘𝑦)))} ⇒ ⊢ (𝜑 → (♯‘𝐴) = ((𝑁 + 𝐾)C𝐾)) | ||
| Theorem | sticksstones15 42162* | Sticks and stones with almost collapsed definitions for positive integers. (Contributed by metakunt, 7-Oct-2024.) |
| ⊢ (𝜑 → 𝑁 ∈ ℕ0) & ⊢ (𝜑 → 𝐾 ∈ ℕ0) & ⊢ 𝐴 = {𝑔 ∣ (𝑔:(1...(𝐾 + 1))⟶ℕ0 ∧ Σ𝑖 ∈ (1...(𝐾 + 1))(𝑔‘𝑖) = 𝑁)} ⇒ ⊢ (𝜑 → (♯‘𝐴) = ((𝑁 + 𝐾)C𝐾)) | ||
| Theorem | sticksstones16 42163* | Sticks and stones with collapsed definitions for positive integers. (Contributed by metakunt, 20-Oct-2024.) |
| ⊢ (𝜑 → 𝑁 ∈ ℕ0) & ⊢ (𝜑 → 𝐾 ∈ ℕ) & ⊢ 𝐴 = {𝑔 ∣ (𝑔:(1...𝐾)⟶ℕ0 ∧ Σ𝑖 ∈ (1...𝐾)(𝑔‘𝑖) = 𝑁)} ⇒ ⊢ (𝜑 → (♯‘𝐴) = ((𝑁 + (𝐾 − 1))C(𝐾 − 1))) | ||
| Theorem | sticksstones17 42164* | Extend sticks and stones to finite sets, bijective builder. (Contributed by metakunt, 23-Oct-2024.) |
| ⊢ (𝜑 → 𝑁 ∈ ℕ0) & ⊢ (𝜑 → 𝐾 ∈ ℕ0) & ⊢ 𝐴 = {𝑔 ∣ (𝑔:(1...𝐾)⟶ℕ0 ∧ Σ𝑖 ∈ (1...𝐾)(𝑔‘𝑖) = 𝑁)} & ⊢ 𝐵 = {ℎ ∣ (ℎ:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (ℎ‘𝑖) = 𝑁)} & ⊢ (𝜑 → 𝑍:(1...𝐾)–1-1-onto→𝑆) & ⊢ 𝐺 = (𝑏 ∈ 𝐵 ↦ (𝑦 ∈ (1...𝐾) ↦ (𝑏‘(𝑍‘𝑦)))) ⇒ ⊢ (𝜑 → 𝐺:𝐵⟶𝐴) | ||
| Theorem | sticksstones18 42165* | Extend sticks and stones to finite sets, bijective builder. (Contributed by metakunt, 23-Oct-2024.) |
| ⊢ (𝜑 → 𝑁 ∈ ℕ0) & ⊢ (𝜑 → 𝐾 ∈ ℕ0) & ⊢ 𝐴 = {𝑔 ∣ (𝑔:(1...𝐾)⟶ℕ0 ∧ Σ𝑖 ∈ (1...𝐾)(𝑔‘𝑖) = 𝑁)} & ⊢ 𝐵 = {ℎ ∣ (ℎ:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (ℎ‘𝑖) = 𝑁)} & ⊢ (𝜑 → 𝑍:(1...𝐾)–1-1-onto→𝑆) & ⊢ 𝐹 = (𝑎 ∈ 𝐴 ↦ (𝑥 ∈ 𝑆 ↦ (𝑎‘(◡𝑍‘𝑥)))) ⇒ ⊢ (𝜑 → 𝐹:𝐴⟶𝐵) | ||
| Theorem | sticksstones19 42166* | Extend sticks and stones to finite sets, bijective builder. (Contributed by metakunt, 23-Oct-2024.) |
| ⊢ (𝜑 → 𝑁 ∈ ℕ0) & ⊢ (𝜑 → 𝐾 ∈ ℕ0) & ⊢ 𝐴 = {𝑔 ∣ (𝑔:(1...𝐾)⟶ℕ0 ∧ Σ𝑖 ∈ (1...𝐾)(𝑔‘𝑖) = 𝑁)} & ⊢ 𝐵 = {ℎ ∣ (ℎ:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (ℎ‘𝑖) = 𝑁)} & ⊢ (𝜑 → 𝑍:(1...𝐾)–1-1-onto→𝑆) & ⊢ 𝐹 = (𝑎 ∈ 𝐴 ↦ (𝑥 ∈ 𝑆 ↦ (𝑎‘(◡𝑍‘𝑥)))) & ⊢ 𝐺 = (𝑏 ∈ 𝐵 ↦ (𝑦 ∈ (1...𝐾) ↦ (𝑏‘(𝑍‘𝑦)))) ⇒ ⊢ (𝜑 → 𝐹:𝐴–1-1-onto→𝐵) | ||
| Theorem | sticksstones20 42167* | Lift sticks and stones to arbitrary finite non-empty sets. (Contributed by metakung, 24-Oct-2024.) |
| ⊢ (𝜑 → 𝑁 ∈ ℕ0) & ⊢ (𝜑 → 𝑆 ∈ Fin) & ⊢ (𝜑 → 𝐾 ∈ ℕ) & ⊢ 𝐴 = {𝑔 ∣ (𝑔:(1...𝐾)⟶ℕ0 ∧ Σ𝑖 ∈ (1...𝐾)(𝑔‘𝑖) = 𝑁)} & ⊢ 𝐵 = {ℎ ∣ (ℎ:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (ℎ‘𝑖) = 𝑁)} & ⊢ (𝜑 → (♯‘𝑆) = 𝐾) ⇒ ⊢ (𝜑 → (♯‘𝐵) = ((𝑁 + (𝐾 − 1))C(𝐾 − 1))) | ||
| Theorem | sticksstones21 42168* | Lift sticks and stones to arbitrary finite non-empty sets. (Contributed by metakunt, 24-Oct-2024.) |
| ⊢ (𝜑 → 𝑁 ∈ ℕ0) & ⊢ (𝜑 → 𝑆 ∈ Fin) & ⊢ (𝜑 → 𝑆 ≠ ∅) & ⊢ 𝐴 = {𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = 𝑁)} ⇒ ⊢ (𝜑 → (♯‘𝐴) = ((𝑁 + ((♯‘𝑆) − 1))C((♯‘𝑆) − 1))) | ||
| Theorem | sticksstones22 42169* | Non-exhaustive sticks and stones. (Contributed by metakunt, 26-Oct-2024.) |
| ⊢ (𝜑 → 𝑁 ∈ ℕ0) & ⊢ (𝜑 → 𝑆 ∈ Fin) & ⊢ (𝜑 → 𝑆 ≠ ∅) & ⊢ 𝐴 = {𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑁)} ⇒ ⊢ (𝜑 → (♯‘𝐴) = ((𝑁 + (♯‘𝑆))C(♯‘𝑆))) | ||
| Theorem | sticksstones23 42170* | Non-exhaustive sticks and stones. (Contributed by metakunt, 7-May-2025.) |
| ⊢ (𝜑 → 𝑁 ∈ ℕ0) & ⊢ (𝜑 → 𝑆 ∈ Fin) & ⊢ (𝜑 → 𝑆 ≠ ∅) & ⊢ 𝐴 = {𝑓 ∈ (ℕ0 ↑m 𝑆) ∣ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑁} ⇒ ⊢ (𝜑 → (♯‘𝐴) = ((𝑁 + (♯‘𝑆))C(♯‘𝑆))) | ||
| Theorem | aks6d1c6lem1 42171* | Lemma for claim 6, deduce exact degree of the polynomial. (Contributed by metakunt, 7-May-2025.) |
| ⊢ ∼ = {〈𝑒, 𝑓〉 ∣ (𝑒 ∈ ℕ ∧ 𝑓 ∈ (Base‘(Poly1‘𝐾)) ∧ ∀𝑦 ∈ ((mulGrp‘𝐾) PrimRoots 𝑅)(𝑒(.g‘(mulGrp‘𝐾))(((eval1‘𝐾)‘𝑓)‘𝑦)) = (((eval1‘𝐾)‘𝑓)‘(𝑒(.g‘(mulGrp‘𝐾))𝑦)))} & ⊢ 𝑃 = (chr‘𝐾) & ⊢ (𝜑 → 𝐾 ∈ Field) & ⊢ (𝜑 → 𝑃 ∈ ℙ) & ⊢ (𝜑 → 𝑅 ∈ ℕ) & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 𝑃 ∥ 𝑁) & ⊢ (𝜑 → (𝑁 gcd 𝑅) = 1) & ⊢ (𝜑 → 𝐴 < 𝑃) & ⊢ 𝐺 = (𝑔 ∈ (ℕ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 ↑m (0...𝐴)) ∣ Σ𝑡 ∈ (0...𝐴)(𝑠‘𝑡) ≤ (𝐷 − 1)} & ⊢ (𝜑 → 𝑈 ∈ (ℕ0 ↑m (0...𝐴))) ⇒ ⊢ (𝜑 → ((deg1‘𝐾)‘(𝐺‘𝑈)) = Σ𝑡 ∈ (0...𝐴)(𝑈‘𝑡)) | ||
| Theorem | aks6d1c6lem2 42172* | Every primitive root is root of G(u)-G(v). (Contributed by metakunt, 8-May-2025.) |
| ⊢ ∼ = {〈𝑒, 𝑓〉 ∣ (𝑒 ∈ ℕ ∧ 𝑓 ∈ (Base‘(Poly1‘𝐾)) ∧ ∀𝑦 ∈ ((mulGrp‘𝐾) PrimRoots 𝑅)(𝑒(.g‘(mulGrp‘𝐾))(((eval1‘𝐾)‘𝑓)‘𝑦)) = (((eval1‘𝐾)‘𝑓)‘(𝑒(.g‘(mulGrp‘𝐾))𝑦)))} & ⊢ 𝑃 = (chr‘𝐾) & ⊢ (𝜑 → 𝐾 ∈ Field) & ⊢ (𝜑 → 𝑃 ∈ ℙ) & ⊢ (𝜑 → 𝑅 ∈ ℕ) & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 𝑃 ∥ 𝑁) & ⊢ (𝜑 → (𝑁 gcd 𝑅) = 1) & ⊢ (𝜑 → 𝐴 < 𝑃) & ⊢ 𝐺 = (𝑔 ∈ (ℕ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 ↑m (0...𝐴)) ∣ Σ𝑡 ∈ (0...𝐴)(𝑠‘𝑡) ≤ (𝐷 − 1)} & ⊢ (𝜑 → 𝑈 ∈ 𝑆) & ⊢ (𝜑 → 𝑉 ∈ 𝑆) & ⊢ (𝜑 → ((𝐻 ↾ 𝑆)‘𝑈) = ((𝐻 ↾ 𝑆)‘𝑉)) & ⊢ (𝜑 → 𝑈 ≠ 𝑉) & ⊢ 𝐽 = (𝑗 ∈ (ℕ0 × ℕ0) ↦ ((𝐸‘𝑗)(.g‘(mulGrp‘𝐾))𝑀)) & ⊢ (𝜑 → (♯‘(𝐿 “ (𝐸 “ (ℕ0 × ℕ0)))) ≤ (♯‘(𝐽 “ (ℕ0 × ℕ0)))) ⇒ ⊢ (𝜑 → 𝐷 ≤ (♯‘(◡((eval1‘𝐾)‘((𝐺‘𝑈)(-g‘(Poly1‘𝐾))(𝐺‘𝑉))) “ {(0g‘𝐾)}))) | ||
| Theorem | aks6d1c6lem3 42173* | Claim 6 of Theorem 6.1 of https://www3.nd.edu/%7eandyp/notes/AKS.pdf TODO, eliminate hypothesis. (Contributed by metakunt, 8-May-2025.) |
| ⊢ ∼ = {〈𝑒, 𝑓〉 ∣ (𝑒 ∈ ℕ ∧ 𝑓 ∈ (Base‘(Poly1‘𝐾)) ∧ ∀𝑦 ∈ ((mulGrp‘𝐾) PrimRoots 𝑅)(𝑒(.g‘(mulGrp‘𝐾))(((eval1‘𝐾)‘𝑓)‘𝑦)) = (((eval1‘𝐾)‘𝑓)‘(𝑒(.g‘(mulGrp‘𝐾))𝑦)))} & ⊢ 𝑃 = (chr‘𝐾) & ⊢ (𝜑 → 𝐾 ∈ Field) & ⊢ (𝜑 → 𝑃 ∈ ℙ) & ⊢ (𝜑 → 𝑅 ∈ ℕ) & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 𝑃 ∥ 𝑁) & ⊢ (𝜑 → (𝑁 gcd 𝑅) = 1) & ⊢ (𝜑 → 𝐴 < 𝑃) & ⊢ 𝐺 = (𝑔 ∈ (ℕ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 ↑m (0...𝐴)) ∣ Σ𝑡 ∈ (0...𝐴)(𝑠‘𝑡) ≤ (𝐷 − 1)} & ⊢ 𝐽 = (𝑗 ∈ (ℕ0 × ℕ0) ↦ ((𝐸‘𝑗)(.g‘(mulGrp‘𝐾))𝑀)) & ⊢ (𝜑 → (♯‘(𝐿 “ (𝐸 “ (ℕ0 × ℕ0)))) ≤ (♯‘(𝐽 “ (ℕ0 × ℕ0)))) ⇒ ⊢ (𝜑 → ((𝐷 + 𝐴)C(𝐷 − 1)) ≤ (♯‘(𝐻 “ (ℕ0 ↑m (0...𝐴))))) | ||
| Theorem | aks6d1c6lem4 42174* | Claim 6 of Theorem 6.1 of https://www3.nd.edu/%7eandyp/notes/AKS.pdf Add hypothesis on coprimality, lift function to the integers so that group operations may be applied. Inline definition. (Contributed by metakunt, 14-May-2025.) |
| ⊢ ∼ = {〈𝑒, 𝑓〉 ∣ (𝑒 ∈ ℕ ∧ 𝑓 ∈ (Base‘(Poly1‘𝐾)) ∧ ∀𝑦 ∈ ((mulGrp‘𝐾) PrimRoots 𝑅)(𝑒(.g‘(mulGrp‘𝐾))(((eval1‘𝐾)‘𝑓)‘𝑦)) = (((eval1‘𝐾)‘𝑓)‘(𝑒(.g‘(mulGrp‘𝐾))𝑦)))} & ⊢ 𝑃 = (chr‘𝐾) & ⊢ (𝜑 → 𝐾 ∈ Field) & ⊢ (𝜑 → 𝑃 ∈ ℙ) & ⊢ (𝜑 → 𝑅 ∈ ℕ) & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 𝑃 ∥ 𝑁) & ⊢ (𝜑 → (𝑁 gcd 𝑅) = 1) & ⊢ (𝜑 → ∀𝑏 ∈ (1...𝐴)(𝑏 gcd 𝑁) = 1) & ⊢ 𝐺 = (𝑔 ∈ (ℕ0 ↑m (0...𝐴)) ↦ ((mulGrp‘(Poly1‘𝐾)) Σg (𝑖 ∈ (0...𝐴) ↦ ((𝑔‘𝑖)(.g‘(mulGrp‘(Poly1‘𝐾)))((var1‘𝐾)(+g‘(Poly1‘𝐾))((algSc‘(Poly1‘𝐾))‘((ℤRHom‘𝐾)‘𝑖))))))) & ⊢ 𝐴 = (⌊‘((√‘(ϕ‘𝑅)) · (2 logb 𝑁))) & ⊢ 𝐸 = (𝑘 ∈ ℕ0, 𝑙 ∈ ℕ0 ↦ ((𝑃↑𝑘) · ((𝑁 / 𝑃)↑𝑙))) & ⊢ 𝐿 = (ℤRHom‘(ℤ/nℤ‘𝑅)) & ⊢ (𝜑 → ∀𝑎 ∈ (1...𝐴)𝑁 ∼ ((var1‘𝐾)(+g‘(Poly1‘𝐾))((algSc‘(Poly1‘𝐾))‘((ℤRHom‘𝐾)‘𝑎)))) & ⊢ (𝜑 → (𝑥 ∈ (Base‘𝐾) ↦ (𝑃(.g‘(mulGrp‘𝐾))𝑥)) ∈ (𝐾 RingIso 𝐾)) & ⊢ (𝜑 → 𝑀 ∈ ((mulGrp‘𝐾) PrimRoots 𝑅)) & ⊢ 𝐻 = (ℎ ∈ (ℕ0 ↑m (0...𝐴)) ↦ (((eval1‘𝐾)‘(𝐺‘ℎ))‘𝑀)) & ⊢ 𝐷 = (♯‘(𝐿 “ (𝐸 “ (ℕ0 × ℕ0)))) & ⊢ 𝑆 = {𝑠 ∈ (ℕ0 ↑m (0...𝐴)) ∣ Σ𝑡 ∈ (0...𝐴)(𝑠‘𝑡) ≤ (𝐷 − 1)} & ⊢ 𝐽 = (𝑗 ∈ ℤ ↦ (𝑗(.g‘((mulGrp‘𝐾) ↾s 𝑈))𝑀)) & ⊢ (𝜑 → (♯‘(𝐿 “ (𝐸 “ (ℕ0 × ℕ0)))) ≤ (♯‘(𝐽 “ (𝐸 “ (ℕ0 × ℕ0))))) & ⊢ 𝑈 = {𝑚 ∈ (Base‘(mulGrp‘𝐾)) ∣ ∃𝑛 ∈ (Base‘(mulGrp‘𝐾))(𝑛(+g‘(mulGrp‘𝐾))𝑚) = (0g‘(mulGrp‘𝐾))} ⇒ ⊢ (𝜑 → ((𝐷 + 𝐴)C(𝐷 − 1)) ≤ (♯‘(𝐻 “ (ℕ0 ↑m (0...𝐴))))) | ||
| Theorem | aks6d1c6isolem1 42175* | Lemma to construct the map out of the quotient for AKS. (Contributed by metakunt, 14-May-2025.) |
| ⊢ (𝜑 → 𝑅 ∈ CMnd) & ⊢ (𝜑 → 𝐾 ∈ ℕ) & ⊢ 𝑈 = {𝑎 ∈ (Base‘𝑅) ∣ ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑎) = (0g‘𝑅)} & ⊢ 𝐹 = (𝑥 ∈ ℤ ↦ (𝑥(.g‘(𝑅 ↾s 𝑈))𝑀)) & ⊢ (𝜑 → 𝑀 ∈ (𝑅 PrimRoots 𝐾)) ⇒ ⊢ (𝜑 → ((𝑅 ↾s 𝑈) ↾s ran 𝐹) ∈ Grp) | ||
| Theorem | aks6d1c6isolem2 42176* | Lemma to construct the group homomorphism for the AKS Theorem. (Contributed by metakunt, 14-May-2025.) |
| ⊢ (𝜑 → 𝑅 ∈ CMnd) & ⊢ (𝜑 → 𝐾 ∈ ℕ) & ⊢ 𝑈 = {𝑎 ∈ (Base‘𝑅) ∣ ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑎) = (0g‘𝑅)} & ⊢ 𝐹 = (𝑥 ∈ ℤ ↦ (𝑥(.g‘(𝑅 ↾s 𝑈))𝑀)) & ⊢ (𝜑 → 𝑀 ∈ (𝑅 PrimRoots 𝐾)) ⇒ ⊢ (𝜑 → 𝐹 ∈ (ℤring GrpHom ((𝑅 ↾s 𝑈) ↾s ran 𝐹))) | ||
| Theorem | aks6d1c6isolem3 42177* | The preimage of a map sending a primitive root to its powers of zero is equal to the set of integers that divide 𝑅. (Contributed by metakunt, 15-May-2025.) |
| ⊢ (𝜑 → 𝑅 ∈ CMnd) & ⊢ (𝜑 → 𝐾 ∈ ℕ) & ⊢ 𝑈 = {𝑎 ∈ (Base‘𝑅) ∣ ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑎) = (0g‘𝑅)} & ⊢ 𝐹 = (𝑥 ∈ ℤ ↦ (𝑥(.g‘(𝑅 ↾s 𝑈))𝑀)) & ⊢ (𝜑 → 𝑀 ∈ (𝑅 PrimRoots 𝐾)) & ⊢ 𝑆 = (RSpan‘ℤring) ⇒ ⊢ (𝜑 → (𝑆‘{𝐾}) = (◡𝐹 “ {(0g‘(𝑅 ↾s 𝑈))})) | ||
| Theorem | aks6d1c6lem5 42178* | Eliminate the size hypothesis. Claim 6. (Contributed by metakunt, 15-May-2025.) |
| ⊢ ∼ = {〈𝑒, 𝑓〉 ∣ (𝑒 ∈ ℕ ∧ 𝑓 ∈ (Base‘(Poly1‘𝐾)) ∧ ∀𝑦 ∈ ((mulGrp‘𝐾) PrimRoots 𝑅)(𝑒(.g‘(mulGrp‘𝐾))(((eval1‘𝐾)‘𝑓)‘𝑦)) = (((eval1‘𝐾)‘𝑓)‘(𝑒(.g‘(mulGrp‘𝐾))𝑦)))} & ⊢ 𝑃 = (chr‘𝐾) & ⊢ (𝜑 → 𝐾 ∈ Field) & ⊢ (𝜑 → 𝑃 ∈ ℙ) & ⊢ (𝜑 → 𝑅 ∈ ℕ) & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 𝑃 ∥ 𝑁) & ⊢ (𝜑 → (𝑁 gcd 𝑅) = 1) & ⊢ (𝜑 → ∀𝑏 ∈ (1...𝐴)(𝑏 gcd 𝑁) = 1) & ⊢ 𝐺 = (𝑔 ∈ (ℕ0 ↑m (0...𝐴)) ↦ ((mulGrp‘(Poly1‘𝐾)) Σg (𝑖 ∈ (0...𝐴) ↦ ((𝑔‘𝑖)(.g‘(mulGrp‘(Poly1‘𝐾)))((var1‘𝐾)(+g‘(Poly1‘𝐾))((algSc‘(Poly1‘𝐾))‘((ℤRHom‘𝐾)‘𝑖))))))) & ⊢ 𝐴 = (⌊‘((√‘(ϕ‘𝑅)) · (2 logb 𝑁))) & ⊢ 𝐸 = (𝑘 ∈ ℕ0, 𝑙 ∈ ℕ0 ↦ ((𝑃↑𝑘) · ((𝑁 / 𝑃)↑𝑙))) & ⊢ 𝐿 = (ℤRHom‘(ℤ/nℤ‘𝑅)) & ⊢ (𝜑 → ∀𝑎 ∈ (1...𝐴)𝑁 ∼ ((var1‘𝐾)(+g‘(Poly1‘𝐾))((algSc‘(Poly1‘𝐾))‘((ℤRHom‘𝐾)‘𝑎)))) & ⊢ (𝜑 → (𝑥 ∈ (Base‘𝐾) ↦ (𝑃(.g‘(mulGrp‘𝐾))𝑥)) ∈ (𝐾 RingIso 𝐾)) & ⊢ (𝜑 → 𝑀 ∈ ((mulGrp‘𝐾) PrimRoots 𝑅)) & ⊢ 𝐻 = (ℎ ∈ (ℕ0 ↑m (0...𝐴)) ↦ (((eval1‘𝐾)‘(𝐺‘ℎ))‘𝑀)) & ⊢ 𝐷 = (♯‘(𝐿 “ (𝐸 “ (ℕ0 × ℕ0)))) & ⊢ 𝑆 = {𝑠 ∈ (ℕ0 ↑m (0...𝐴)) ∣ Σ𝑡 ∈ (0...𝐴)(𝑠‘𝑡) ≤ (𝐷 − 1)} & ⊢ 𝐽 = (𝑗 ∈ ℤ ↦ (𝑗(.g‘((mulGrp‘𝐾) ↾s 𝑈))𝑀)) & ⊢ 𝑈 = {𝑚 ∈ (Base‘(mulGrp‘𝐾)) ∣ ∃𝑛 ∈ (Base‘(mulGrp‘𝐾))(𝑛(+g‘(mulGrp‘𝐾))𝑚) = (0g‘(mulGrp‘𝐾))} & ⊢ 𝑋 = (𝑏 ∈ (Base‘(ℤring /s (ℤring ~QG (◡𝐽 “ {(0g‘(((mulGrp‘𝐾) ↾s 𝑈) ↾s ran 𝐽))})))) ↦ ∪ (𝐽 “ 𝑏)) ⇒ ⊢ (𝜑 → ((𝐷 + 𝐴)C(𝐷 − 1)) ≤ (♯‘(𝐻 “ (ℕ0 ↑m (0...𝐴))))) | ||
| Theorem | bcled 42179 | Inequality for binomial coefficients. (Contributed by metakunt, 12-May-2025.) |
| ⊢ (𝜑 → 𝐴 ∈ ℕ0) & ⊢ (𝜑 → 𝐵 ∈ ℕ0) & ⊢ (𝜑 → 𝐶 ∈ ℤ) & ⊢ (𝜑 → 𝐴 ≤ 𝐵) ⇒ ⊢ (𝜑 → (𝐴C𝐶) ≤ (𝐵C𝐶)) | ||
| Theorem | bcle2d 42180 | Inequality for binomial coefficients. (Contributed by metakunt, 12-May-2025.) |
| ⊢ (𝜑 → 𝐴 ∈ ℕ0) & ⊢ (𝜑 → 𝐵 ∈ ℕ0) & ⊢ (𝜑 → 𝐶 ∈ ℕ0) & ⊢ (𝜑 → 𝐷 ∈ ℤ) & ⊢ (𝜑 → 𝐴 ≤ 𝐵) & ⊢ (𝜑 → 𝐷 ≤ 𝐶) ⇒ ⊢ (𝜑 → ((𝐴 + 𝐶)C(𝐴 + 𝐷)) ≤ ((𝐵 + 𝐶)C(𝐵 + 𝐷))) | ||
| Theorem | aks6d1c7lem1 42181* | The last set of inequalities of Claim 7 of Theorem 6.1 https://www3.nd.edu/%7eandyp/notes/AKS.pdf. (Contributed by metakunt, 12-May-2025.) |
| ⊢ (𝜑 → 𝑃 ∈ ℙ) & ⊢ (𝜑 → 𝑅 ∈ ℕ) & ⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘3)) & ⊢ (𝜑 → 𝑃 ∥ 𝑁) & ⊢ (𝜑 → (𝑁 gcd 𝑅) = 1) & ⊢ 𝐸 = (𝑘 ∈ ℕ0, 𝑙 ∈ ℕ0 ↦ ((𝑃↑𝑘) · ((𝑁 / 𝑃)↑𝑙))) & ⊢ 𝐿 = (ℤRHom‘(ℤ/nℤ‘𝑅)) & ⊢ 𝐷 = (♯‘(𝐿 “ (𝐸 “ (ℕ0 × ℕ0)))) & ⊢ 𝐴 = (⌊‘((√‘(ϕ‘𝑅)) · (2 logb 𝑁))) & ⊢ (𝜑 → ((2 logb 𝑁)↑2) < ((odℤ‘𝑅)‘𝑁)) ⇒ ⊢ (𝜑 → (𝑁↑(⌊‘(√‘𝐷))) < ((𝐷 + 𝐴)C(𝐷 − 1))) | ||
| Theorem | aks6d1c7lem2 42182* | Contradiction to Claim 2 and Claim 7. We assumed in Claim 2 that there are two different prime numbers 𝑃 and 𝑄. (Contributed by metakunt, 16-May-2025.) |
| ⊢ ∼ = {〈𝑒, 𝑓〉 ∣ (𝑒 ∈ ℕ ∧ 𝑓 ∈ (Base‘(Poly1‘𝐾)) ∧ ∀𝑦 ∈ ((mulGrp‘𝐾) PrimRoots 𝑅)(𝑒(.g‘(mulGrp‘𝐾))(((eval1‘𝐾)‘𝑓)‘𝑦)) = (((eval1‘𝐾)‘𝑓)‘(𝑒(.g‘(mulGrp‘𝐾))𝑦)))} & ⊢ 𝑃 = (chr‘𝐾) & ⊢ (𝜑 → 𝐾 ∈ Field) & ⊢ (𝜑 → 𝑃 ∈ ℙ) & ⊢ (𝜑 → 𝑅 ∈ ℕ) & ⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘3)) & ⊢ (𝜑 → 𝑃 ∥ 𝑁) & ⊢ (𝜑 → (𝑁 gcd 𝑅) = 1) & ⊢ 𝐸 = (𝑘 ∈ ℕ0, 𝑙 ∈ ℕ0 ↦ ((𝑃↑𝑘) · ((𝑁 / 𝑃)↑𝑙))) & ⊢ 𝐿 = (ℤRHom‘(ℤ/nℤ‘𝑅)) & ⊢ 𝐷 = (♯‘(𝐿 “ (𝐸 “ (ℕ0 × ℕ0)))) & ⊢ 𝐴 = (⌊‘((√‘(ϕ‘𝑅)) · (2 logb 𝑁))) & ⊢ (𝜑 → ((2 logb 𝑁)↑2) < ((odℤ‘𝑅)‘𝑁)) & ⊢ (𝜑 → (𝑥 ∈ (Base‘𝐾) ↦ (𝑃(.g‘(mulGrp‘𝐾))𝑥)) ∈ (𝐾 RingIso 𝐾)) & ⊢ (𝜑 → 𝑀 ∈ ((mulGrp‘𝐾) PrimRoots 𝑅)) & ⊢ 𝐻 = (ℎ ∈ (ℕ0 ↑m (0...𝐴)) ↦ (((eval1‘𝐾)‘(𝐺‘ℎ))‘𝑀)) & ⊢ 𝐵 = (⌊‘(√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 × ℕ0)))))) & ⊢ 𝐶 = (𝐸 “ ((0...𝐵) × (0...𝐵))) & ⊢ (𝜑 → (𝑄 ∈ ℙ ∧ 𝑄 ∥ 𝑁)) & ⊢ (𝜑 → ∀𝑏 ∈ (1...𝐴)(𝑏 gcd 𝑁) = 1) & ⊢ 𝐺 = (𝑔 ∈ (ℕ0 ↑m (0...𝐴)) ↦ ((mulGrp‘(Poly1‘𝐾)) Σg (𝑖 ∈ (0...𝐴) ↦ ((𝑔‘𝑖)(.g‘(mulGrp‘(Poly1‘𝐾)))((var1‘𝐾)(+g‘(Poly1‘𝐾))((algSc‘(Poly1‘𝐾))‘((ℤRHom‘𝐾)‘𝑖))))))) & ⊢ (𝜑 → ∀𝑎 ∈ (1...𝐴)𝑁 ∼ ((var1‘𝐾)(+g‘(Poly1‘𝐾))((algSc‘(Poly1‘𝐾))‘((ℤRHom‘𝐾)‘𝑎)))) & ⊢ 𝑆 = {𝑠 ∈ (ℕ0 ↑m (0...𝐴)) ∣ Σ𝑡 ∈ (0...𝐴)(𝑠‘𝑡) ≤ (𝐷 − 1)} ⇒ ⊢ (𝜑 → 𝑃 = 𝑄) | ||
| Theorem | aks6d1c7lem3 42183* | Remove lots of hypotheses now that we have the AKS contradiction. (Contributed by metakunt, 16-May-2025.) |
| ⊢ ∼ = {〈𝑒, 𝑓〉 ∣ (𝑒 ∈ ℕ ∧ 𝑓 ∈ (Base‘(Poly1‘𝐾)) ∧ ∀𝑦 ∈ ((mulGrp‘𝐾) PrimRoots 𝑅)(𝑒(.g‘(mulGrp‘𝐾))(((eval1‘𝐾)‘𝑓)‘𝑦)) = (((eval1‘𝐾)‘𝑓)‘(𝑒(.g‘(mulGrp‘𝐾))𝑦)))} & ⊢ 𝑃 = (chr‘𝐾) & ⊢ (𝜑 → 𝐾 ∈ Field) & ⊢ (𝜑 → 𝑃 ∈ ℙ) & ⊢ (𝜑 → 𝑅 ∈ ℕ) & ⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘3)) & ⊢ (𝜑 → 𝑃 ∥ 𝑁) & ⊢ (𝜑 → (𝑁 gcd 𝑅) = 1) & ⊢ 𝐴 = (⌊‘((√‘(ϕ‘𝑅)) · (2 logb 𝑁))) & ⊢ (𝜑 → ((2 logb 𝑁)↑2) < ((odℤ‘𝑅)‘𝑁)) & ⊢ (𝜑 → (𝑥 ∈ (Base‘𝐾) ↦ (𝑃(.g‘(mulGrp‘𝐾))𝑥)) ∈ (𝐾 RingIso 𝐾)) & ⊢ (𝜑 → 𝑀 ∈ ((mulGrp‘𝐾) PrimRoots 𝑅)) & ⊢ (𝜑 → ∀𝑏 ∈ (1...𝐴)(𝑏 gcd 𝑁) = 1) & ⊢ (𝜑 → ∀𝑎 ∈ (1...𝐴)𝑁 ∼ ((var1‘𝐾)(+g‘(Poly1‘𝐾))((algSc‘(Poly1‘𝐾))‘((ℤRHom‘𝐾)‘𝑎)))) & ⊢ (𝜑 → (𝑄 ∈ ℙ ∧ 𝑄 ∥ 𝑁)) ⇒ ⊢ (𝜑 → 𝑃 = 𝑄) | ||
| Theorem | aks6d1c7lem4 42184* | In the AKS algorithm there exists a unique prime number 𝑝 that divides 𝑁. (Contributed by metakunt, 16-May-2025.) |
| ⊢ ∼ = {〈𝑒, 𝑓〉 ∣ (𝑒 ∈ ℕ ∧ 𝑓 ∈ (Base‘(Poly1‘𝐾)) ∧ ∀𝑦 ∈ ((mulGrp‘𝐾) PrimRoots 𝑅)(𝑒(.g‘(mulGrp‘𝐾))(((eval1‘𝐾)‘𝑓)‘𝑦)) = (((eval1‘𝐾)‘𝑓)‘(𝑒(.g‘(mulGrp‘𝐾))𝑦)))} & ⊢ 𝑃 = (chr‘𝐾) & ⊢ (𝜑 → 𝐾 ∈ Field) & ⊢ (𝜑 → 𝑃 ∈ ℙ) & ⊢ (𝜑 → 𝑅 ∈ ℕ) & ⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘3)) & ⊢ (𝜑 → 𝑃 ∥ 𝑁) & ⊢ (𝜑 → (𝑁 gcd 𝑅) = 1) & ⊢ 𝐴 = (⌊‘((√‘(ϕ‘𝑅)) · (2 logb 𝑁))) & ⊢ (𝜑 → ((2 logb 𝑁)↑2) < ((odℤ‘𝑅)‘𝑁)) & ⊢ (𝜑 → (𝑥 ∈ (Base‘𝐾) ↦ (𝑃(.g‘(mulGrp‘𝐾))𝑥)) ∈ (𝐾 RingIso 𝐾)) & ⊢ (𝜑 → 𝑀 ∈ ((mulGrp‘𝐾) PrimRoots 𝑅)) & ⊢ (𝜑 → ∀𝑏 ∈ (1...𝐴)(𝑏 gcd 𝑁) = 1) & ⊢ (𝜑 → ∀𝑎 ∈ (1...𝐴)𝑁 ∼ ((var1‘𝐾)(+g‘(Poly1‘𝐾))((algSc‘(Poly1‘𝐾))‘((ℤRHom‘𝐾)‘𝑎)))) ⇒ ⊢ (𝜑 → ∃!𝑝 ∈ ℙ 𝑝 ∥ 𝑁) | ||
| Theorem | aks6d1c7 42185* | 𝑁 is a prime power if the hypotheses of the AKS algorithm hold. Claim 7 of Theorem 6.1 https://www3.nd.edu/%7eandyp/notes/AKS.pdf. (Contributed by metakunt, 16-May-2025.) |
| ⊢ ∼ = {〈𝑒, 𝑓〉 ∣ (𝑒 ∈ ℕ ∧ 𝑓 ∈ (Base‘(Poly1‘𝐾)) ∧ ∀𝑦 ∈ ((mulGrp‘𝐾) PrimRoots 𝑅)(𝑒(.g‘(mulGrp‘𝐾))(((eval1‘𝐾)‘𝑓)‘𝑦)) = (((eval1‘𝐾)‘𝑓)‘(𝑒(.g‘(mulGrp‘𝐾))𝑦)))} & ⊢ 𝑃 = (chr‘𝐾) & ⊢ (𝜑 → 𝐾 ∈ Field) & ⊢ (𝜑 → 𝑃 ∈ ℙ) & ⊢ (𝜑 → 𝑅 ∈ ℕ) & ⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘3)) & ⊢ (𝜑 → 𝑃 ∥ 𝑁) & ⊢ (𝜑 → (𝑁 gcd 𝑅) = 1) & ⊢ 𝐴 = (⌊‘((√‘(ϕ‘𝑅)) · (2 logb 𝑁))) & ⊢ (𝜑 → ((2 logb 𝑁)↑2) < ((odℤ‘𝑅)‘𝑁)) & ⊢ (𝜑 → (𝑥 ∈ (Base‘𝐾) ↦ (𝑃(.g‘(mulGrp‘𝐾))𝑥)) ∈ (𝐾 RingIso 𝐾)) & ⊢ (𝜑 → 𝑀 ∈ ((mulGrp‘𝐾) PrimRoots 𝑅)) & ⊢ (𝜑 → ∀𝑏 ∈ (1...𝐴)(𝑏 gcd 𝑁) = 1) & ⊢ (𝜑 → ∀𝑎 ∈ (1...𝐴)𝑁 ∼ ((var1‘𝐾)(+g‘(Poly1‘𝐾))((algSc‘(Poly1‘𝐾))‘((ℤRHom‘𝐾)‘𝑎)))) ⇒ ⊢ (𝜑 → 𝑁 = (𝑃↑(𝑃 pCnt 𝑁))) | ||
| Theorem | rhmqusspan 42186* | Ring homomorphism out of a quotient given an ideal spanned by a singleton. (Contributed by metakunt, 7-Jun-2025.) |
| ⊢ 0 = (0g‘𝐻) & ⊢ (𝜑 → 𝐹 ∈ (𝐺 RingHom 𝐻)) & ⊢ 𝐾 = (◡𝐹 “ { 0 }) & ⊢ 𝑄 = (𝐺 /s (𝐺 ~QG 𝑁)) & ⊢ 𝐽 = (𝑞 ∈ (Base‘𝑄) ↦ ∪ (𝐹 “ 𝑞)) & ⊢ (𝜑 → 𝐺 ∈ CRing) & ⊢ 𝑁 = ((RSpan‘𝐺)‘{𝑋}) & ⊢ (𝜑 → 𝑋 ∈ (Base‘𝐺)) & ⊢ (𝜑 → (𝐹‘𝑋) = 0 ) ⇒ ⊢ (𝜑 → (𝐽 ∈ (𝑄 RingHom 𝐻) ∧ ∀𝑔 ∈ (Base‘𝐺)(𝐽‘[𝑔](𝐺 ~QG 𝑁)) = (𝐹‘𝑔))) | ||
| Theorem | aks5lem1 42187* | Section 5 of https://www3.nd.edu/%7eandyp/notes/AKS.pdf. Construction of a ring homomorphism out of Zn X to K. (Contributed by metakunt, 7-Jun-2025.) |
| ⊢ (𝜑 → 𝐾 ∈ Field) & ⊢ 𝑃 = (chr‘𝐾) & ⊢ (𝜑 → (𝑃 ∈ ℙ ∧ 𝑁 ∈ ℕ ∧ 𝑃 ∥ 𝑁)) & ⊢ 𝐹 = (𝑝 ∈ (Base‘(Poly1‘(ℤ/nℤ‘𝑁))) ↦ (𝐺 ∘ 𝑝)) & ⊢ 𝐺 = (𝑞 ∈ (Base‘(ℤ/nℤ‘𝑁)) ↦ ∪ ((ℤRHom‘𝐾) “ 𝑞)) & ⊢ 𝐻 = (𝑟 ∈ (Base‘(Poly1‘𝐾)) ↦ (((eval1‘𝐾)‘𝑟)‘𝑀)) & ⊢ (𝜑 → 𝑀 ∈ (Base‘𝐾)) ⇒ ⊢ (𝜑 → (𝐻 ∘ 𝐹) ∈ ((Poly1‘(ℤ/nℤ‘𝑁)) RingHom 𝐾)) | ||
| Theorem | aks5lem2 42188* | Lemma for section 5 https://www3.nd.edu/%7eandyp/notes/AKS.pdf. Construct the quotient for the AKS reduction. (Contributed by metakunt, 7-Jun-2025.) |
| ⊢ (𝜑 → 𝐾 ∈ Field) & ⊢ 𝑃 = (chr‘𝐾) & ⊢ (𝜑 → (𝑃 ∈ ℙ ∧ 𝑁 ∈ ℕ ∧ 𝑃 ∥ 𝑁)) & ⊢ 𝐹 = (𝑝 ∈ (Base‘(Poly1‘(ℤ/nℤ‘𝑁))) ↦ (𝐺 ∘ 𝑝)) & ⊢ 𝐺 = (𝑞 ∈ (Base‘(ℤ/nℤ‘𝑁)) ↦ ∪ ((ℤRHom‘𝐾) “ 𝑞)) & ⊢ 𝐻 = (𝑟 ∈ (Base‘(Poly1‘𝐾)) ↦ (((eval1‘𝐾)‘𝑟)‘𝑀)) & ⊢ (𝜑 → 𝑀 ∈ ((mulGrp‘𝐾) PrimRoots 𝑅)) & ⊢ 𝐼 = (𝑠 ∈ (Base‘𝐴) ↦ ∪ ((𝐻 ∘ 𝐹) “ 𝑠)) & ⊢ 𝐴 = ((Poly1‘(ℤ/nℤ‘𝑁)) /s ((Poly1‘(ℤ/nℤ‘𝑁)) ~QG 𝐿)) & ⊢ 𝐿 = ((RSpan‘(Poly1‘(ℤ/nℤ‘𝑁)))‘{((𝑅(.g‘(mulGrp‘(Poly1‘(ℤ/nℤ‘𝑁))))(var1‘(ℤ/nℤ‘𝑁)))(-g‘(Poly1‘(ℤ/nℤ‘𝑁)))(1r‘(Poly1‘(ℤ/nℤ‘𝑁))))}) & ⊢ (𝜑 → 𝑅 ∈ ℕ) ⇒ ⊢ (𝜑 → (𝐼 ∈ (𝐴 RingHom 𝐾) ∧ ∀𝑔 ∈ (Base‘(Poly1‘(ℤ/nℤ‘𝑁)))(𝐼‘[𝑔]((Poly1‘(ℤ/nℤ‘𝑁)) ~QG 𝐿)) = ((𝐻 ∘ 𝐹)‘𝑔))) | ||
| Theorem | ply1asclzrhval 42189 | Transfer results from algebraic scalars and ZR ring homomorphisms. (Contributed by metakunt, 17-Jun-2025.) |
| ⊢ 𝑊 = (Poly1‘𝑅) & ⊢ 𝐴 = (algSc‘𝑊) & ⊢ 𝐵 = (ℤRHom‘𝑊) & ⊢ 𝐶 = (ℤRHom‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ CRing) & ⊢ (𝜑 → 𝑋 ∈ ℤ) ⇒ ⊢ (𝜑 → (𝐴‘(𝐶‘𝑋)) = (𝐵‘𝑋)) | ||
| Theorem | aks5lem3a 42190* | Lemma for AKS section 5. (Contributed by metakunt, 17-Jun-2025.) |
| ⊢ (𝜑 → 𝐾 ∈ Field) & ⊢ 𝑃 = (chr‘𝐾) & ⊢ (𝜑 → (𝑃 ∈ ℙ ∧ 𝑁 ∈ ℕ ∧ 𝑃 ∥ 𝑁)) & ⊢ 𝐵 = (𝑆 /s (𝑆 ~QG 𝐿)) & ⊢ 𝐿 = ((RSpan‘𝑆)‘{((𝑅(.g‘(mulGrp‘𝑆))(var1‘(ℤ/nℤ‘𝑁)))(-g‘𝑆)(1r‘𝑆))}) & ⊢ (𝜑 → 𝑅 ∈ ℕ) & ⊢ ∼ = {〈𝑒, 𝑓〉 ∣ (𝑒 ∈ ℕ ∧ 𝑓 ∈ (Base‘(Poly1‘𝐾)) ∧ ∀𝑦 ∈ ((mulGrp‘𝐾) PrimRoots 𝑅)(𝑒(.g‘(mulGrp‘𝐾))(((eval1‘𝐾)‘𝑓)‘𝑦)) = (((eval1‘𝐾)‘𝑓)‘(𝑒(.g‘(mulGrp‘𝐾))𝑦)))} & ⊢ 𝑆 = (Poly1‘(ℤ/nℤ‘𝑁)) & ⊢ 𝐹 = (𝑝 ∈ (Base‘(Poly1‘(ℤ/nℤ‘𝑁))) ↦ (𝐺 ∘ 𝑝)) & ⊢ 𝐺 = (𝑞 ∈ (Base‘(ℤ/nℤ‘𝑁)) ↦ ∪ ((ℤRHom‘𝐾) “ 𝑞)) & ⊢ 𝐻 = (𝑟 ∈ (Base‘(Poly1‘𝐾)) ↦ (((eval1‘𝐾)‘𝑟)‘𝑀)) & ⊢ (𝜑 → 𝑀 ∈ ((mulGrp‘𝐾) PrimRoots 𝑅)) & ⊢ 𝐼 = (𝑠 ∈ (Base‘𝐵) ↦ ∪ ((𝐻 ∘ 𝐹) “ 𝑠)) & ⊢ (𝜑 → 𝐴 ∈ ℤ) & ⊢ (𝜑 → [(𝑁(.g‘(mulGrp‘𝑆))((var1‘(ℤ/nℤ‘𝑁))(+g‘𝑆)((algSc‘𝑆)‘((ℤRHom‘(ℤ/nℤ‘𝑁))‘𝐴))))](𝑆 ~QG 𝐿) = [((𝑁(.g‘(mulGrp‘𝑆))(var1‘(ℤ/nℤ‘𝑁)))(+g‘𝑆)((algSc‘𝑆)‘((ℤRHom‘(ℤ/nℤ‘𝑁))‘𝐴)))](𝑆 ~QG 𝐿)) ⇒ ⊢ (𝜑 → (𝑁(.g‘(mulGrp‘𝐾))(((eval1‘𝐾)‘((var1‘𝐾)(+g‘(Poly1‘𝐾))((algSc‘(Poly1‘𝐾))‘((ℤRHom‘𝐾)‘𝐴))))‘𝑀)) = (((eval1‘𝐾)‘((var1‘𝐾)(+g‘(Poly1‘𝐾))((algSc‘(Poly1‘𝐾))‘((ℤRHom‘𝐾)‘𝐴))))‘(𝑁(.g‘(mulGrp‘𝐾))𝑀))) | ||
| Theorem | aks5lem4a 42191* | Lemma for AKS section 5, reduce hypotheses. (Contributed by metakunt, 17-Jun-2025.) |
| ⊢ (𝜑 → 𝐾 ∈ Field) & ⊢ 𝑃 = (chr‘𝐾) & ⊢ (𝜑 → (𝑃 ∈ ℙ ∧ 𝑁 ∈ ℕ ∧ 𝑃 ∥ 𝑁)) & ⊢ 𝐵 = (𝑆 /s (𝑆 ~QG 𝐿)) & ⊢ 𝐿 = ((RSpan‘𝑆)‘{((𝑅(.g‘(mulGrp‘𝑆))(var1‘(ℤ/nℤ‘𝑁)))(-g‘𝑆)(1r‘𝑆))}) & ⊢ (𝜑 → 𝑅 ∈ ℕ) & ⊢ ∼ = {〈𝑒, 𝑓〉 ∣ (𝑒 ∈ ℕ ∧ 𝑓 ∈ (Base‘(Poly1‘𝐾)) ∧ ∀𝑦 ∈ ((mulGrp‘𝐾) PrimRoots 𝑅)(𝑒(.g‘(mulGrp‘𝐾))(((eval1‘𝐾)‘𝑓)‘𝑦)) = (((eval1‘𝐾)‘𝑓)‘(𝑒(.g‘(mulGrp‘𝐾))𝑦)))} & ⊢ 𝑆 = (Poly1‘(ℤ/nℤ‘𝑁)) & ⊢ (𝜑 → 𝑀 ∈ ((mulGrp‘𝐾) PrimRoots 𝑅)) & ⊢ (𝜑 → 𝐴 ∈ ℤ) & ⊢ (𝜑 → [(𝑁(.g‘(mulGrp‘𝑆))((var1‘(ℤ/nℤ‘𝑁))(+g‘𝑆)((algSc‘𝑆)‘((ℤRHom‘(ℤ/nℤ‘𝑁))‘𝐴))))](𝑆 ~QG 𝐿) = [((𝑁(.g‘(mulGrp‘𝑆))(var1‘(ℤ/nℤ‘𝑁)))(+g‘𝑆)((algSc‘𝑆)‘((ℤRHom‘(ℤ/nℤ‘𝑁))‘𝐴)))](𝑆 ~QG 𝐿)) ⇒ ⊢ (𝜑 → (𝑁(.g‘(mulGrp‘𝐾))(((eval1‘𝐾)‘((var1‘𝐾)(+g‘(Poly1‘𝐾))((algSc‘(Poly1‘𝐾))‘((ℤRHom‘𝐾)‘𝐴))))‘𝑀)) = (((eval1‘𝐾)‘((var1‘𝐾)(+g‘(Poly1‘𝐾))((algSc‘(Poly1‘𝐾))‘((ℤRHom‘𝐾)‘𝐴))))‘(𝑁(.g‘(mulGrp‘𝐾))𝑀))) | ||
| Theorem | aks5lem5a 42192* | Lemma for AKS, section 5, connect to Theorem 6.1. (Contributed by metakunt, 17-Jun-2025.) |
| ⊢ (𝜑 → 𝐾 ∈ Field) & ⊢ 𝑃 = (chr‘𝐾) & ⊢ (𝜑 → (𝑃 ∈ ℙ ∧ 𝑁 ∈ ℕ ∧ 𝑃 ∥ 𝑁)) & ⊢ 𝐵 = (𝑆 /s (𝑆 ~QG 𝐿)) & ⊢ 𝐿 = ((RSpan‘𝑆)‘{((𝑅(.g‘(mulGrp‘𝑆))(var1‘(ℤ/nℤ‘𝑁)))(-g‘𝑆)(1r‘𝑆))}) & ⊢ (𝜑 → 𝑅 ∈ ℕ) & ⊢ ∼ = {〈𝑒, 𝑓〉 ∣ (𝑒 ∈ ℕ ∧ 𝑓 ∈ (Base‘(Poly1‘𝐾)) ∧ ∀𝑦 ∈ ((mulGrp‘𝐾) PrimRoots 𝑅)(𝑒(.g‘(mulGrp‘𝐾))(((eval1‘𝐾)‘𝑓)‘𝑦)) = (((eval1‘𝐾)‘𝑓)‘(𝑒(.g‘(mulGrp‘𝐾))𝑦)))} & ⊢ 𝑆 = (Poly1‘(ℤ/nℤ‘𝑁)) & ⊢ (𝜑 → ∀𝑎 ∈ (1...𝐴)[(𝑁(.g‘(mulGrp‘𝑆))((var1‘(ℤ/nℤ‘𝑁))(+g‘𝑆)((ℤRHom‘𝑆)‘𝑎)))](𝑆 ~QG 𝐿) = [((𝑁(.g‘(mulGrp‘𝑆))(var1‘(ℤ/nℤ‘𝑁)))(+g‘𝑆)((ℤRHom‘𝑆)‘𝑎))](𝑆 ~QG 𝐿)) ⇒ ⊢ (𝜑 → ∀𝑎 ∈ (1...𝐴)𝑁 ∼ ((var1‘𝐾)(+g‘(Poly1‘𝐾))((algSc‘(Poly1‘𝐾))‘((ℤRHom‘𝐾)‘𝑎)))) | ||
| Theorem | aks5lem6 42193* | Connect results of section 5 and Theorem 6.1 AKS. (Contributed by metakunt, 25-Jun-2025.) |
| ⊢ ∼ = {〈𝑒, 𝑓〉 ∣ (𝑒 ∈ ℕ ∧ 𝑓 ∈ (Base‘(Poly1‘𝐾)) ∧ ∀𝑦 ∈ ((mulGrp‘𝐾) PrimRoots 𝑅)(𝑒(.g‘(mulGrp‘𝐾))(((eval1‘𝐾)‘𝑓)‘𝑦)) = (((eval1‘𝐾)‘𝑓)‘(𝑒(.g‘(mulGrp‘𝐾))𝑦)))} & ⊢ 𝑃 = (chr‘𝐾) & ⊢ (𝜑 → 𝐾 ∈ Field) & ⊢ (𝜑 → 𝑃 ∈ ℙ) & ⊢ (𝜑 → 𝑅 ∈ ℕ) & ⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘3)) & ⊢ (𝜑 → 𝑃 ∥ 𝑁) & ⊢ (𝜑 → (𝑁 gcd 𝑅) = 1) & ⊢ 𝐴 = (⌊‘((√‘(ϕ‘𝑅)) · (2 logb 𝑁))) & ⊢ (𝜑 → ((2 logb 𝑁)↑2) < ((odℤ‘𝑅)‘𝑁)) & ⊢ (𝜑 → (𝑥 ∈ (Base‘𝐾) ↦ (𝑃(.g‘(mulGrp‘𝐾))𝑥)) ∈ (𝐾 RingIso 𝐾)) & ⊢ (𝜑 → 𝑀 ∈ ((mulGrp‘𝐾) PrimRoots 𝑅)) & ⊢ (𝜑 → ∀𝑏 ∈ (1...𝐴)(𝑏 gcd 𝑁) = 1) & ⊢ 𝑆 = (Poly1‘(ℤ/nℤ‘𝑁)) & ⊢ 𝐿 = ((RSpan‘𝑆)‘{((𝑅(.g‘(mulGrp‘𝑆))(var1‘(ℤ/nℤ‘𝑁)))(-g‘𝑆)(1r‘𝑆))}) & ⊢ 𝑋 = (var1‘(ℤ/nℤ‘𝑁)) & ⊢ (𝜑 → ∀𝑎 ∈ (1...𝐴)[(𝑁(.g‘(mulGrp‘𝑆))(𝑋(+g‘𝑆)((ℤRHom‘𝑆)‘𝑎)))](𝑆 ~QG 𝐿) = [((𝑁(.g‘(mulGrp‘𝑆))𝑋)(+g‘𝑆)((ℤRHom‘𝑆)‘𝑎))](𝑆 ~QG 𝐿)) ⇒ ⊢ (𝜑 → 𝑁 = (𝑃↑(𝑃 pCnt 𝑁))) | ||
| Theorem | indstrd 42194* | Strong induction, deduction version. (Contributed by Steven Nguyen, 13-Jul-2025.) |
| ⊢ (𝑥 = 𝑦 → (𝜓 ↔ 𝜒)) & ⊢ (𝑥 = 𝐴 → (𝜓 ↔ 𝜃)) & ⊢ ((𝜑 ∧ 𝑥 ∈ ℕ ∧ ∀𝑦 ∈ ℕ (𝑦 < 𝑥 → 𝜒)) → 𝜓) & ⊢ (𝜑 → 𝐴 ∈ ℕ) ⇒ ⊢ (𝜑 → 𝜃) | ||
| Theorem | grpods 42195* | Relate sums of elements of orders and roots of unity. (Contributed by metakunt, 14-Jul-2025.) |
| ⊢ 𝐵 = (Base‘𝐺) & ⊢ ↑ = (.g‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ Grp) & ⊢ (𝜑 → 𝐵 ∈ Fin) & ⊢ (𝜑 → 𝑁 ∈ ℕ) ⇒ ⊢ (𝜑 → Σ𝑘 ∈ {𝑚 ∈ (1...𝑁) ∣ 𝑚 ∥ 𝑁} (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘}) = (♯‘{𝑥 ∈ 𝐵 ∣ (𝑁 ↑ 𝑥) = (0g‘𝐺)})) | ||
| Theorem | unitscyglem1 42196* | Lemma for unitscyg. (Contributed by metakunt, 13-Jul-2025.) |
| ⊢ 𝐵 = (Base‘𝐺) & ⊢ ↑ = (.g‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ Grp) & ⊢ (𝜑 → 𝐵 ∈ Fin) & ⊢ (𝜑 → ∀𝑛 ∈ ℕ (♯‘{𝑥 ∈ 𝐵 ∣ (𝑛 ↑ 𝑥) = (0g‘𝐺)}) ≤ 𝑛) & ⊢ (𝜑 → 𝐴 ∈ 𝐵) ⇒ ⊢ (𝜑 → (♯‘{𝑥 ∈ 𝐵 ∣ (((od‘𝐺)‘𝐴) ↑ 𝑥) = (0g‘𝐺)}) = ((od‘𝐺)‘𝐴)) | ||
| Theorem | unitscyglem2 42197* | Lemma for unitscyg. (Contributed by metakunt, 13-Jul-2025.) |
| ⊢ 𝐵 = (Base‘𝐺) & ⊢ ↑ = (.g‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ Grp) & ⊢ (𝜑 → 𝐵 ∈ Fin) & ⊢ (𝜑 → ∀𝑛 ∈ ℕ (♯‘{𝑥 ∈ 𝐵 ∣ (𝑛 ↑ 𝑥) = (0g‘𝐺)}) ≤ 𝑛) & ⊢ (𝜑 → 𝐷 ∈ ℕ) & ⊢ (𝜑 → 𝐷 ∥ (♯‘𝐵)) & ⊢ (𝜑 → 𝐴 ∈ 𝐵) & ⊢ (𝜑 → ((od‘𝐺)‘𝐴) = 𝐷) & ⊢ (𝜑 → ∀𝑐 ∈ ℕ (𝑐 < 𝐷 → ((𝑐 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐}) = (ϕ‘𝑐)))) ⇒ ⊢ (𝜑 → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷}) = (ϕ‘𝐷)) | ||
| Theorem | unitscyglem3 42198* | Lemma for unitscyg. (Contributed by metakunt, 14-Jul-2025.) |
| ⊢ 𝐵 = (Base‘𝐺) & ⊢ ↑ = (.g‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ Grp) & ⊢ (𝜑 → 𝐵 ∈ Fin) & ⊢ (𝜑 → ∀𝑛 ∈ ℕ (♯‘{𝑥 ∈ 𝐵 ∣ (𝑛 ↑ 𝑥) = (0g‘𝐺)}) ≤ 𝑛) ⇒ ⊢ (𝜑 → ∀𝑑 ∈ ℕ ((𝑑 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑑} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑑}) = (ϕ‘𝑑))) | ||
| Theorem | unitscyglem4 42199* | Lemma for unitscyg (Contributed by metakunt, 14-Jul-2025.) |
| ⊢ 𝐵 = (Base‘𝐺) & ⊢ ↑ = (.g‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ Grp) & ⊢ (𝜑 → 𝐵 ∈ Fin) & ⊢ (𝜑 → ∀𝑛 ∈ ℕ (♯‘{𝑥 ∈ 𝐵 ∣ (𝑛 ↑ 𝑥) = (0g‘𝐺)}) ≤ 𝑛) & ⊢ (𝜑 → 𝐷 ∈ ℕ) & ⊢ (𝜑 → 𝐷 ∥ (♯‘𝐵)) ⇒ ⊢ (𝜑 → (♯‘{𝑦 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑦) = 𝐷}) = (ϕ‘𝐷)) | ||
| Theorem | unitscyglem5 42200 | Lemma for unitscyg (Contributed by metakunt, 9-Aug-2025.) |
| ⊢ 𝐺 = ((mulGrp‘𝑅) ↾s (Unit‘𝑅)) & ⊢ (𝜑 → 𝑅 ∈ IDomn) & ⊢ (𝜑 → (Base‘𝑅) ∈ Fin) & ⊢ (𝜑 → 𝐷 ∈ ℕ) & ⊢ (𝜑 → 𝐷 ∥ (♯‘(Base‘𝐺))) ⇒ ⊢ (𝜑 → ((mulGrp‘𝑅) PrimRoots 𝐷) ≠ ∅) | ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |