P. 422 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 42101-42200   *Has distinct variable group(s)

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𝑁))
21.29.7  Sticks and stones
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(♯‘𝑆)))
21.29.8  Continuation AKS
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 𝐷) ≠ ∅)