P. 431 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 43001-43100   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	aks6d1c2lem4 43001*	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 43002*	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 43003*	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 43004*	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 43005*	Special case related to rspsbc 3829. (Contributed by metakunt, 5-May-2025.)
⊢ ((𝐴 ∈ 𝐵 ∧ ∀𝑥 ∈ 𝐵 𝐶 ≠ 𝐷) → ⦋𝐴 / 𝑥⦌𝐶 ≠ 𝐷)
Theorem	idomnnzpownz 43006	A nonzero power in an integral domain is nonzero. (Contributed by metakunt, 5-May-2025.)
⊢ (𝜑 → 𝑅 ∈ IDomn)    &   ⊢ (𝜑 → 𝐴 ∈ (Base‘𝑅))    &   ⊢ (𝜑 → 𝐴 ≠ (0g‘𝑅))    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    &   ⊢ ↑ = (.g‘(mulGrp‘𝑅))    ⇒   ⊢ (𝜑 → (𝑁 ↑ 𝐴) ≠ (0g‘𝑅))
Theorem	idomnnzgmulnz 43007*	A finite product of nonzero elements in an integral domain is nonzero. (Contributed by metakunt, 5-May-2025.)
⊢ 𝐺 = (mulGrp‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ IDomn)    &   ⊢ (𝜑 → 𝑁 ∈ Fin)    &   ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑁) → 𝐴 ∈ (Base‘𝑅))    &   ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑁) → 𝐴 ≠ (0g‘𝑅))    ⇒   ⊢ (𝜑 → (𝐺 Σg (𝑛 ∈ 𝑁 ↦ 𝐴)) ≠ (0g‘𝑅))
Theorem	ringexp0nn 43008	Zero to the power of a positive integer is zero. (Contributed by metakunt, 5-May-2025.)
⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ ↑ = (.g‘(mulGrp‘𝑅))    ⇒   ⊢ (𝜑 → (𝑁 ↑ (0g‘𝑅)) = (0g‘𝑅))
Theorem	aks6d1c5lem0 43009*	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 43010	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 43011*	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 43012*	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 43013*	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 43014*	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 43015	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 43016	The value of 5 choose 2. (Contributed by metakunt, 8-Jun-2024.)
⊢ (5C2) = ;10
Theorem	facp2 43017	The factorial of a successor's successor. (Contributed by metakunt, 19-Apr-2024.)
⊢ (𝑁 ∈ ℕ0 → (!‘(𝑁 + 2)) = ((!‘𝑁) · ((𝑁 + 1) · (𝑁 + 2))))
Theorem	2np3bcnp1 43018	Part of induction step for 2ap1caineq 43019. (Contributed by metakunt, 8-Jun-2024.)
⊢ (𝜑 → 𝑁 ∈ ℕ0)    ⇒   ⊢ (𝜑 → (((2 · (𝑁 + 1)) + 1)C(𝑁 + 1)) = ((((2 · 𝑁) + 1)C𝑁) · (2 · (((2 · 𝑁) + 3) / (𝑁 + 2)))))
Theorem	2ap1caineq 43019	Inequality for Theorem 6.6 for AKS. (Contributed by metakunt, 8-Jun-2024.)
⊢ (𝜑 → 𝑁 ∈ ℤ)    &   ⊢ (𝜑 → 2 ≤ 𝑁)    ⇒   ⊢ (𝜑 → (2↑(𝑁 + 1)) < (((2 · 𝑁) + 1)C𝑁))
21.30.7  Sticks and stones
Theorem	sticksstones1 43020*	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 43021*	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 43022*	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 43023*	Equinumerosity lemma for sticks and stones. (Contributed by metakunt, 28-Sep-2024.)
⊢ (𝜑 → 𝑁 ∈ ℕ0)    &   ⊢ (𝜑 → 𝐾 ∈ ℕ0)    &   ⊢ 𝐵 = {𝑎 ∈ 𝒫 (1...𝑁) ∣ (♯‘𝑎) = 𝐾}    &   ⊢ 𝐴 = {𝑓 ∣ (𝑓:(1...𝐾)⟶(1...𝑁) ∧ ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑓‘𝑥) < (𝑓‘𝑦)))}    ⇒   ⊢ (𝜑 → 𝐴 ≈ 𝐵)
Theorem	sticksstones5 43024*	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 43025*	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 43026*	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 43027*	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 43028*	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 43029*	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 43030*	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 43031*	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 43032*	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 43033*	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 43034*	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 43035*	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 43036*	Sticks and stones with collapsed definitions for positive integers. (Contributed by metakunt, 20-Oct-2024.)
⊢ (𝜑 → 𝑁 ∈ ℕ0)    &   ⊢ (𝜑 → 𝐾 ∈ ℕ)    &   ⊢ 𝐴 = {𝑔 ∣ (𝑔:(1...𝐾)⟶ℕ0 ∧ Σ𝑖 ∈ (1...𝐾)(𝑔‘𝑖) = 𝑁)}    ⇒   ⊢ (𝜑 → (♯‘𝐴) = ((𝑁 + (𝐾 − 1))C(𝐾 − 1)))
Theorem	sticksstones17 43037*	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 43038*	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 43039*	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 43040*	Lift sticks and stones to arbitrary finite non-empty sets. (Contributed by metakunt, 24-Oct-2024.)
⊢ (𝜑 → 𝑁 ∈ ℕ0)    &   ⊢ (𝜑 → 𝑆 ∈ Fin)    &   ⊢ (𝜑 → 𝐾 ∈ ℕ)    &   ⊢ 𝐴 = {𝑔 ∣ (𝑔:(1...𝐾)⟶ℕ0 ∧ Σ𝑖 ∈ (1...𝐾)(𝑔‘𝑖) = 𝑁)}    &   ⊢ 𝐵 = {ℎ ∣ (ℎ:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (ℎ‘𝑖) = 𝑁)}    &   ⊢ (𝜑 → (♯‘𝑆) = 𝐾)    ⇒   ⊢ (𝜑 → (♯‘𝐵) = ((𝑁 + (𝐾 − 1))C(𝐾 − 1)))
Theorem	sticksstones21 43041*	Lift sticks and stones to arbitrary finite non-empty sets. (Contributed by metakunt, 24-Oct-2024.)
⊢ (𝜑 → 𝑁 ∈ ℕ0)    &   ⊢ (𝜑 → 𝑆 ∈ Fin)    &   ⊢ (𝜑 → 𝑆 ≠ ∅)    &   ⊢ 𝐴 = {𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = 𝑁)}    ⇒   ⊢ (𝜑 → (♯‘𝐴) = ((𝑁 + ((♯‘𝑆) − 1))C((♯‘𝑆) − 1)))
Theorem	sticksstones22 43042*	Non-exhaustive sticks and stones. (Contributed by metakunt, 26-Oct-2024.)
⊢ (𝜑 → 𝑁 ∈ ℕ0)    &   ⊢ (𝜑 → 𝑆 ∈ Fin)    &   ⊢ (𝜑 → 𝑆 ≠ ∅)    &   ⊢ 𝐴 = {𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑁)}    ⇒   ⊢ (𝜑 → (♯‘𝐴) = ((𝑁 + (♯‘𝑆))C(♯‘𝑆)))
Theorem	sticksstones23 43043*	Non-exhaustive sticks and stones. (Contributed by metakunt, 7-May-2025.)
⊢ (𝜑 → 𝑁 ∈ ℕ0)    &   ⊢ (𝜑 → 𝑆 ∈ Fin)    &   ⊢ (𝜑 → 𝑆 ≠ ∅)    &   ⊢ 𝐴 = {𝑓 ∈ (ℕ0 ↑m 𝑆) ∣ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑁}    ⇒   ⊢ (𝜑 → (♯‘𝐴) = ((𝑁 + (♯‘𝑆))C(♯‘𝑆)))
21.30.8  Continuation AKS
Theorem	aks6d1c6lem1 43044*	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 43045*	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 43046*	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 43047*	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 43048*	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 43049*	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 43050*	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 43051*	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 43052	Inequality for binomial coefficients. (Contributed by metakunt, 12-May-2025.)
⊢ (𝜑 → 𝐴 ∈ ℕ0)    &   ⊢ (𝜑 → 𝐵 ∈ ℕ0)    &   ⊢ (𝜑 → 𝐶 ∈ ℤ)    &   ⊢ (𝜑 → 𝐴 ≤ 𝐵)    ⇒   ⊢ (𝜑 → (𝐴C𝐶) ≤ (𝐵C𝐶))
Theorem	bcle2d 43053	Inequality for binomial coefficients. (Contributed by metakunt, 12-May-2025.)
⊢ (𝜑 → 𝐴 ∈ ℕ0)    &   ⊢ (𝜑 → 𝐵 ∈ ℕ0)    &   ⊢ (𝜑 → 𝐶 ∈ ℕ0)    &   ⊢ (𝜑 → 𝐷 ∈ ℤ)    &   ⊢ (𝜑 → 𝐴 ≤ 𝐵)    &   ⊢ (𝜑 → 𝐷 ≤ 𝐶)    ⇒   ⊢ (𝜑 → ((𝐴 + 𝐶)C(𝐴 + 𝐷)) ≤ ((𝐵 + 𝐶)C(𝐵 + 𝐷)))
Theorem	aks6d1c7lem1 43054*	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 43055*	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 43056*	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 43057*	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 43058*	𝑁 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 43059*	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 43060*	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 43061*	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 43062	Transfer results from algebraic scalars and ZR ring homomorphisms. (Contributed by metakunt, 17-Jun-2025.)
⊢ 𝑊 = (Poly1‘𝑅)    &   ⊢ 𝐴 = (algSc‘𝑊)    &   ⊢ 𝐵 = (ℤRHom‘𝑊)    &   ⊢ 𝐶 = (ℤRHom‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ CRing)    &   ⊢ (𝜑 → 𝑋 ∈ ℤ)    ⇒   ⊢ (𝜑 → (𝐴‘(𝐶‘𝑋)) = (𝐵‘𝑋))
Theorem	aks5lem3a 43063*	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 43064*	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 43065*	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 43066*	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 43067*	Strong induction, deduction version. (Contributed by Steven Nguyen, 13-Jul-2025.)
⊢ (𝑥 = 𝑦 → (𝜓 ↔ 𝜒))    &   ⊢ (𝑥 = 𝐴 → (𝜓 ↔ 𝜃))    &   ⊢ ((𝜑 ∧ 𝑥 ∈ ℕ ∧ ∀𝑦 ∈ ℕ (𝑦 < 𝑥 → 𝜒)) → 𝜓)    &   ⊢ (𝜑 → 𝐴 ∈ ℕ)    ⇒   ⊢ (𝜑 → 𝜃)
Theorem	grpods 43068*	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 43069*	Lemma for unitscyg . (Contributed by metakunt, 13-Jul-2025.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ ↑ = (.g‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ Grp)    &   ⊢ (𝜑 → 𝐵 ∈ Fin)    &   ⊢ (𝜑 → ∀𝑛 ∈ ℕ (♯‘{𝑥 ∈ 𝐵 ∣ (𝑛 ↑ 𝑥) = (0g‘𝐺)}) ≤ 𝑛)    &   ⊢ (𝜑 → 𝐴 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (♯‘{𝑥 ∈ 𝐵 ∣ (((od‘𝐺)‘𝐴) ↑ 𝑥) = (0g‘𝐺)}) = ((od‘𝐺)‘𝐴))
Theorem	unitscyglem2 43070*	Lemma for unitscyg . (Contributed by metakunt, 13-Jul-2025.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ ↑ = (.g‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ Grp)    &   ⊢ (𝜑 → 𝐵 ∈ Fin)    &   ⊢ (𝜑 → ∀𝑛 ∈ ℕ (♯‘{𝑥 ∈ 𝐵 ∣ (𝑛 ↑ 𝑥) = (0g‘𝐺)}) ≤ 𝑛)    &   ⊢ (𝜑 → 𝐷 ∈ ℕ)    &   ⊢ (𝜑 → 𝐷 ∥ (♯‘𝐵))    &   ⊢ (𝜑 → 𝐴 ∈ 𝐵)    &   ⊢ (𝜑 → ((od‘𝐺)‘𝐴) = 𝐷)    &   ⊢ (𝜑 → ∀𝑐 ∈ ℕ (𝑐 < 𝐷 → ((𝑐 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐}) = (ϕ‘𝑐))))    ⇒   ⊢ (𝜑 → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷}) = (ϕ‘𝐷))
Theorem	unitscyglem3 43071*	Lemma for unitscyg . (Contributed by metakunt, 14-Jul-2025.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ ↑ = (.g‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ Grp)    &   ⊢ (𝜑 → 𝐵 ∈ Fin)    &   ⊢ (𝜑 → ∀𝑛 ∈ ℕ (♯‘{𝑥 ∈ 𝐵 ∣ (𝑛 ↑ 𝑥) = (0g‘𝐺)}) ≤ 𝑛)    ⇒   ⊢ (𝜑 → ∀𝑑 ∈ ℕ ((𝑑 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑑} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑑}) = (ϕ‘𝑑)))
Theorem	unitscyglem4 43072*	Lemma for unitscyg . (Contributed by metakunt, 14-Jul-2025.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ ↑ = (.g‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ Grp)    &   ⊢ (𝜑 → 𝐵 ∈ Fin)    &   ⊢ (𝜑 → ∀𝑛 ∈ ℕ (♯‘{𝑥 ∈ 𝐵 ∣ (𝑛 ↑ 𝑥) = (0g‘𝐺)}) ≤ 𝑛)    &   ⊢ (𝜑 → 𝐷 ∈ ℕ)    &   ⊢ (𝜑 → 𝐷 ∥ (♯‘𝐵))    ⇒   ⊢ (𝜑 → (♯‘{𝑦 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑦) = 𝐷}) = (ϕ‘𝐷))
Theorem	unitscyglem5 43073	Lemma for unitscyg . (Contributed by metakunt, 9-Aug-2025.)
⊢ 𝐺 = ((mulGrp‘𝑅) ↾s (Unit‘𝑅))    &   ⊢ (𝜑 → 𝑅 ∈ IDomn)    &   ⊢ (𝜑 → (Base‘𝑅) ∈ Fin)    &   ⊢ (𝜑 → 𝐷 ∈ ℕ)    &   ⊢ (𝜑 → 𝐷 ∥ (♯‘(Base‘𝐺)))    ⇒   ⊢ (𝜑 → ((mulGrp‘𝑅) PrimRoots 𝐷) ≠ ∅)
Theorem	aks5lem7 43074*	Lemma for aks5. We clean up the hypotheses compared to aks5lem6 43066. (Contributed by metakunt, 9-Aug-2025.)
⊢ (𝜑 → (♯‘(Base‘𝐾)) ∈ ℕ)    &   ⊢ 𝑃 = (chr‘𝐾)    &   ⊢ (𝜑 → 𝐾 ∈ Field)    &   ⊢ (𝜑 → 𝑃 ∈ ℙ)    &   ⊢ (𝜑 → 𝑅 ∈ ℕ)    &   ⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘3))    &   ⊢ (𝜑 → 𝑃 ∥ 𝑁)    &   ⊢ (𝜑 → (𝑁 gcd 𝑅) = 1)    &   ⊢ 𝐴 = (⌊‘((√‘(ϕ‘𝑅)) · (2 logb 𝑁)))    &   ⊢ (𝜑 → ((2 logb 𝑁)↑2) < ((odℤ‘𝑅)‘𝑁))    &   ⊢ (𝜑 → 𝑅 ∥ ((♯‘(Base‘𝐾)) − 1))    &   ⊢ (𝜑 → ∀𝑎 ∈ (1...𝐴)[(𝑁(.g‘(mulGrp‘𝑆))(𝑋(+g‘𝑆)((ℤRHom‘𝑆)‘𝑎)))](𝑆 ~QG 𝐿) = [((𝑁(.g‘(mulGrp‘𝑆))𝑋)(+g‘𝑆)((ℤRHom‘𝑆)‘𝑎))](𝑆 ~QG 𝐿))    &   ⊢ (𝜑 → ∀𝑏 ∈ (1...𝐴)(𝑏 gcd 𝑁) = 1)    &   ⊢ 𝑆 = (Poly1‘(ℤ/nℤ‘𝑁))    &   ⊢ 𝐿 = ((RSpan‘𝑆)‘{((𝑅(.g‘(mulGrp‘𝑆))𝑋)(-g‘𝑆)(1r‘𝑆))})    &   ⊢ 𝑋 = (var1‘(ℤ/nℤ‘𝑁))    ⇒   ⊢ (𝜑 → 𝑁 = (𝑃↑(𝑃 pCnt 𝑁)))
Theorem	aks5lem8 43075*	Lemma for aks5. Clean up the conclusion. (Contributed by metakunt, 9-Aug-2025.)
⊢ (𝜑 → (♯‘(Base‘𝐾)) ∈ ℕ)    &   ⊢ 𝑃 = (chr‘𝐾)    &   ⊢ (𝜑 → 𝐾 ∈ Field)    &   ⊢ (𝜑 → 𝑃 ∈ ℙ)    &   ⊢ (𝜑 → 𝑅 ∈ ℕ)    &   ⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘3))    &   ⊢ (𝜑 → 𝑃 ∥ 𝑁)    &   ⊢ (𝜑 → (𝑁 gcd 𝑅) = 1)    &   ⊢ 𝐴 = (⌊‘((√‘(ϕ‘𝑅)) · (2 logb 𝑁)))    &   ⊢ (𝜑 → ((2 logb 𝑁)↑2) < ((odℤ‘𝑅)‘𝑁))    &   ⊢ (𝜑 → 𝑅 ∥ ((♯‘(Base‘𝐾)) − 1))    &   ⊢ (𝜑 → ∀𝑎 ∈ (1...𝐴)[(𝑁(.g‘(mulGrp‘𝑆))(𝑋(+g‘𝑆)((ℤRHom‘𝑆)‘𝑎)))](𝑆 ~QG 𝐿) = [((𝑁(.g‘(mulGrp‘𝑆))𝑋)(+g‘𝑆)((ℤRHom‘𝑆)‘𝑎))](𝑆 ~QG 𝐿))    &   ⊢ (𝜑 → ∀𝑏 ∈ (1...𝐴)(𝑏 gcd 𝑁) = 1)    &   ⊢ 𝑆 = (Poly1‘(ℤ/nℤ‘𝑁))    &   ⊢ 𝐿 = ((RSpan‘𝑆)‘{((𝑅(.g‘(mulGrp‘𝑆))𝑋)(-g‘𝑆)(1r‘𝑆))})    &   ⊢ 𝑋 = (var1‘(ℤ/nℤ‘𝑁))    ⇒   ⊢ (𝜑 → ∃𝑝 ∈ ℙ ∃𝑛 ∈ ℕ 𝑁 = (𝑝↑𝑛))
Axiom	ax-exfinfld 43076*	Existence axiom for finite fields, eventually we want to construct them. (Contributed by metakunt, 13-Jul-2025.)
⊢ ∀𝑝 ∈ ℙ ∀𝑛 ∈ ℕ ∃𝑘 ∈ Field ((♯‘(Base‘𝑘)) = (𝑝↑𝑛) ∧ (chr‘𝑘) = 𝑝)
Theorem	exfinfldd 43077*	For any prime 𝑃 and any positive integer 𝑁 there exists a field 𝑘 such that 𝑘 contains 𝑃↑𝑁 elements. (Contributed by metakunt, 13-Jul-2025.)
⊢ (𝜑 → 𝑃 ∈ ℙ)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    ⇒   ⊢ (𝜑 → ∃𝑘 ∈ Field ((♯‘(Base‘𝑘)) = (𝑃↑𝑁) ∧ (chr‘𝑘) = 𝑃))
Theorem	aks5 43078*	The AKS Primality test, given an integer 𝑁 greater than or equal to 3, find a coprime 𝑅 such that 𝑅 is big enough. Then, if a bunch of polynomial equalities in the residue ring hold then 𝑁 is a prime power. Currently depends on the axiom ax-exfinfld 43076, since we currently do not have the existence of finite fields in the database. (Contributed by metakunt, 16-Aug-2025.)
⊢ 𝐴 = (⌊‘((√‘(ϕ‘𝑅)) · (2 logb 𝑁)))    &   ⊢ 𝑋 = (var1‘(ℤ/nℤ‘𝑁))    &   ⊢ 𝑆 = (Poly1‘(ℤ/nℤ‘𝑁))    &   ⊢ 𝐿 = ((RSpan‘𝑆)‘{((𝑅(.g‘(mulGrp‘𝑆))𝑋)(-g‘𝑆)(1r‘𝑆))})    &   ⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘3))    &   ⊢ (𝜑 → 𝑅 ∈ ℕ)    &   ⊢ (𝜑 → (𝑁 gcd 𝑅) = 1)    &   ⊢ (𝜑 → ((2 logb 𝑁)↑2) < ((odℤ‘𝑅)‘𝑁))    &   ⊢ (𝜑 → ∀𝑎 ∈ (1...𝐴)[(𝑁(.g‘(mulGrp‘𝑆))(𝑋(+g‘𝑆)((ℤRHom‘𝑆)‘𝑎)))](𝑆 ~QG 𝐿) = [((𝑁(.g‘(mulGrp‘𝑆))𝑋)(+g‘𝑆)((ℤRHom‘𝑆)‘𝑎))](𝑆 ~QG 𝐿))    &   ⊢ (𝜑 → ∀𝑎 ∈ (1...𝐴)(𝑎 gcd 𝑁) = 1)    ⇒   ⊢ (𝜑 → ∃𝑝 ∈ ℙ ∃𝑛 ∈ ℕ 𝑁 = (𝑝↑𝑛))
21.31  Mathbox for Luke Murphy
21.31.1  Solutions of quadratic equations
Theorem	quadfac 43079	The solution of a quadratic equation via factoring. (Contributed by Luke Murphy, 10-Jul-2026.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐴 ≠ 0)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    &   ⊢ (𝜑 → 𝑋 ∈ ℂ)    &   ⊢ (𝜑 → 𝑀 ∈ ℂ)    &   ⊢ (𝜑 → 𝑁 ∈ ℂ)    &   ⊢ (𝜑 → (𝑀 + 𝑁) = -(𝐵 / 𝐴))    &   ⊢ (𝜑 → (𝑀 · 𝑁) = (𝐶 / 𝐴))    ⇒   ⊢ (𝜑 → (((𝐴 · (𝑋↑2)) + ((𝐵 · 𝑋) + 𝐶)) = 0 ↔ (𝑋 = 𝑀 ∨ 𝑋 = 𝑁)))
21.31.2  April Fool's theorem
Theorem	25or6to4 43080	Question 67 of 68 from a lecture Prof. Loof Lirpa held last Saturday in Lincoln Park. When asked why the smaller root wasn't reduced to 3/2, Lirpa responded "It really doesn't matter anyhow." (Contributed by Luke Murphy, 10-Jul-2026.)
⊢ (𝜑 → 𝐴 = 1)    &   ⊢ (𝜑 → 𝐵 = -(;53 / 2))    &   ⊢ (𝜑 → 𝐶 = (;75 / 2))    &   ⊢ (𝜑 → 𝑋 ∈ ℂ)    ⇒   ⊢ (𝜑 → (((𝐴 · (𝑋↑2)) + ((𝐵 · 𝑋) + 𝐶)) = 0 ↔ (𝑋 = ;25 ∨ 𝑋 = (6 / 4))))
21.32  Mathbox for Steven Nguyen
21.32.1  Utility theorems
Theorem	jarrii 43081	Inference associated with jarri 108. A consequence of ax-mp 5 and ax-1 6. (Contributed by SN, 14-Oct-2025.)
⊢ 𝜓    &   ⊢ ((𝜑 → 𝜓) → 𝜒)    ⇒   ⊢ 𝜒
Theorem	intnanrt 43082	Introduction of conjunct inside of a contradiction. Would be used in elfvov1 7459. (Contributed by SN, 18-May-2025.)
⊢ (¬ 𝜑 → ¬ (𝜑 ∧ 𝜓))
Theorem	ioin9i8 43083	Miscellaneous inference creating a biconditional from an implied converse implication. (Contributed by Steven Nguyen, 17-Jul-2022.)
⊢ (𝜑 → (𝜓 ∨ 𝜒))    &   ⊢ (𝜒 → ¬ 𝜃)    &   ⊢ (𝜓 → 𝜃)    ⇒   ⊢ (𝜑 → (𝜓 ↔ 𝜃))
Theorem	jaodd 43084	Double deduction form of jaoi 871. (Contributed by Steven Nguyen, 17-Jul-2022.)
⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))    &   ⊢ (𝜑 → (𝜓 → (𝜏 → 𝜃)))    ⇒   ⊢ (𝜑 → (𝜓 → ((𝜒 ∨ 𝜏) → 𝜃)))
Theorem	syl3an12 43085	A double syllogism inference. (Contributed by SN, 15-Sep-2024.)
⊢ (𝜑 → 𝜓)    &   ⊢ (𝜒 → 𝜃)    &   ⊢ ((𝜓 ∧ 𝜃 ∧ 𝜏) → 𝜂)    ⇒   ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜏) → 𝜂)
Theorem	exbiii 43086	Inference associated with exbii 1881. Weaker version of eximii 1870. (Contributed by SN, 14-Oct-2025.)
⊢ ∃𝑥𝜑    &   ⊢ (𝜑 ↔ 𝜓)    ⇒   ⊢ ∃𝑥𝜓
Theorem	sbtd 43087*	A true statement is true upon substitution (deduction). A similar proof is possible for icht 48360. (Contributed by SN, 4-May-2024.)
⊢ (𝜑 → 𝜓)    ⇒   ⊢ (𝜑 → [𝑡 / 𝑥]𝜓)
Theorem	sbor2 43088	One direction of sbor 2341, using fewer axioms. Compare 19.33 1917. (Contributed by Steven Nguyen, 18-Aug-2023.)
⊢ (([𝑡 / 𝑥]𝜑 ∨ [𝑡 / 𝑥]𝜓) → [𝑡 / 𝑥](𝜑 ∨ 𝜓))
Theorem	sbalexi 43089*	Inference form of sbalex 2280, avoiding ax-10 2178 by using ax-gen 1828. (Contributed by SN, 12-Aug-2025.)
⊢ ∃𝑥(𝑥 = 𝑦 ∧ 𝜑)    ⇒   ⊢ ∀𝑥(𝑥 = 𝑦 → 𝜑)
Theorem	nfalh 43090	Version of nfal 2355 with an 'h' hypothesis, avoiding ax-12 2215. (Contributed by SN, 11-Feb-2026.)
⊢ (𝜑 → ∀𝑥𝜑)    ⇒   ⊢ Ⅎ𝑥∀𝑦𝜑
Theorem	nfe2 43091	An inner existential quantifier's variable is bound. (Contributed by SN, 11-Feb-2026.)
⊢ Ⅎ𝑥∃𝑦∃𝑥𝜑
Theorem	nfale2 43092	An inner existential quantifier's variable is bound. (Contributed by SN, 11-Feb-2026.)
⊢ Ⅎ𝑥∀𝑦∃𝑥𝜑
Theorem	19.9dev 43093*	19.9d 2241 in the case of an existential quantifier, avoiding the ax-10 2178 from nfex 2356 that would be used for the hypothesis of 19.9d 2241, at the cost of an additional DV condition on 𝑦, 𝜑. (Contributed by SN, 26-May-2024.)
⊢ (𝜑 → Ⅎ𝑥𝜓)    ⇒   ⊢ (𝜑 → (∃𝑥∃𝑦𝜓 ↔ ∃𝑦𝜓))
Theorem	3rspcedvd 43094*	Triple application of rspcedvd 3581. (Contributed by Steven Nguyen, 27-Feb-2023.)
⊢ (𝜑 → 𝐴 ∈ 𝐷)    &   ⊢ (𝜑 → 𝐵 ∈ 𝐷)    &   ⊢ (𝜑 → 𝐶 ∈ 𝐷)    &   ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → (𝜓 ↔ 𝜒))    &   ⊢ ((𝜑 ∧ 𝑦 = 𝐵) → (𝜒 ↔ 𝜃))    &   ⊢ ((𝜑 ∧ 𝑧 = 𝐶) → (𝜃 ↔ 𝜏))    &   ⊢ (𝜑 → 𝜏)    ⇒   ⊢ (𝜑 → ∃𝑥 ∈ 𝐷 ∃𝑦 ∈ 𝐷 ∃𝑧 ∈ 𝐷 𝜓)
Theorem	sn-axrep5v 43095*	A condensed form of axrep5 5244. (Contributed by SN, 21-Sep-2023.)
⊢ (∀𝑤 ∈ 𝑥 ∃*𝑧𝜑 → ∃𝑦∀𝑧(𝑧 ∈ 𝑦 ↔ ∃𝑤 ∈ 𝑥 𝜑))
Theorem	sn-axprlem3 43096*	axprlem3 5394 using only Tarski's FOL axiom schemes and ax-rep 5236. (Contributed by SN, 22-Sep-2023.)
⊢ ∃𝑦∀𝑧(𝑧 ∈ 𝑦 ↔ ∃𝑤 ∈ 𝑥 if-(𝜑, 𝑧 = 𝑎, 𝑧 = 𝑏))
Theorem	sn-exelALT 43097*	Alternate proof of exel 5413, avoiding ax-pr 5402 but requiring ax-5 1943, ax-9 2155, and ax-pow 5334. This is similar to how elALT2 5338 uses ax-pow 5334 instead of ax-pr 5402 compared to el 5417. (Contributed by SN, 18-Sep-2023.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ∃𝑦∃𝑥 𝑥 ∈ 𝑦
Theorem	ssabdv 43098*	Deduction of abstraction subclass from implication. (Contributed by SN, 22-Dec-2024.)
⊢ (𝜑 → (𝑥 ∈ 𝐴 → 𝜓))    ⇒   ⊢ (𝜑 → 𝐴 ⊆ {𝑥 ∣ 𝜓})
Theorem	sn-iotalem 43099*	An unused lemma showing that many equivalences involving df-iota 6493 are potentially provable without ax-10 2178, ax-11 2194, ax-12 2215. (Contributed by SN, 6-Nov-2024.)
⊢ {𝑦 ∣ {𝑥 ∣ 𝜑} = {𝑦}} = {𝑧 ∣ {𝑦 ∣ {𝑥 ∣ 𝜑} = {𝑦}} = {𝑧}}
Theorem	sn-iotalemcor 43100*	Corollary of sn-iotalem 43099. Compare sb8iota 6504. (Contributed by SN, 6-Nov-2024.)
⊢ (℩𝑥𝜑) = (℩𝑦{𝑥 ∣ 𝜑} = {𝑦})