P. 433 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 43201-43300   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	prjspersym 43201*	The relation in ℙ𝕣𝕠𝕛 is symmetric. (Contributed by Steven Nguyen, 1-May-2023.)
⊢ ∼ = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ ∃𝑙 ∈ 𝐾 𝑥 = (𝑙 · 𝑦))}    &   ⊢ 𝐵 = ((Base‘𝑉) ∖ {(0g‘𝑉)})    &   ⊢ 𝑆 = (Scalar‘𝑉)    &   ⊢ · = ( ·𝑠 ‘𝑉)    &   ⊢ 𝐾 = (Base‘𝑆)    ⇒   ⊢ ((𝑉 ∈ LVec ∧ 𝑋 ∼ 𝑌) → 𝑌 ∼ 𝑋)
Theorem	prjsper 43202*	The relation used to define ℙ𝕣𝕠𝕛 is an equivalence relation. (Contributed by Steven Nguyen, 1-May-2023.)
⊢ ∼ = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ ∃𝑙 ∈ 𝐾 𝑥 = (𝑙 · 𝑦))}    &   ⊢ 𝐵 = ((Base‘𝑉) ∖ {(0g‘𝑉)})    &   ⊢ 𝑆 = (Scalar‘𝑉)    &   ⊢ · = ( ·𝑠 ‘𝑉)    &   ⊢ 𝐾 = (Base‘𝑆)    ⇒   ⊢ (𝑉 ∈ LVec → ∼ Er 𝐵)
Theorem	prjspreln0 43203*	Two nonzero vectors are equivalent by a nonzero scalar. (Contributed by Steven Nguyen, 31-May-2023.)
⊢ ∼ = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ ∃𝑙 ∈ 𝐾 𝑥 = (𝑙 · 𝑦))}    &   ⊢ 𝐵 = ((Base‘𝑉) ∖ {(0g‘𝑉)})    &   ⊢ 𝑆 = (Scalar‘𝑉)    &   ⊢ · = ( ·𝑠 ‘𝑉)    &   ⊢ 𝐾 = (Base‘𝑆)    &   ⊢ 0 = (0g‘𝑆)    ⇒   ⊢ (𝑉 ∈ LVec → (𝑋 ∼ 𝑌 ↔ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ ∃𝑚 ∈ (𝐾 ∖ { 0 })𝑋 = (𝑚 · 𝑌))))
Theorem	prjspvs 43204*	A nonzero multiple of a vector is equivalent to the vector. (Contributed by Steven Nguyen, 6-Jun-2023.)
⊢ ∼ = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ ∃𝑙 ∈ 𝐾 𝑥 = (𝑙 · 𝑦))}    &   ⊢ 𝐵 = ((Base‘𝑉) ∖ {(0g‘𝑉)})    &   ⊢ 𝑆 = (Scalar‘𝑉)    &   ⊢ · = ( ·𝑠 ‘𝑉)    &   ⊢ 𝐾 = (Base‘𝑆)    &   ⊢ 0 = (0g‘𝑆)    ⇒   ⊢ ((𝑉 ∈ LVec ∧ 𝑋 ∈ 𝐵 ∧ 𝑁 ∈ (𝐾 ∖ { 0 })) → (𝑁 · 𝑋) ∼ 𝑋)
Theorem	prjsprellsp 43205*	Two vectors are equivalent iff their spans are equal. (Contributed by Steven Nguyen, 31-May-2023.)
⊢ ∼ = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ ∃𝑙 ∈ 𝐾 𝑥 = (𝑙 · 𝑦))}    &   ⊢ 𝐵 = ((Base‘𝑉) ∖ {(0g‘𝑉)})    &   ⊢ 𝑆 = (Scalar‘𝑉)    &   ⊢ · = ( ·𝑠 ‘𝑉)    &   ⊢ 𝐾 = (Base‘𝑆)    &   ⊢ 𝑁 = (LSpan‘𝑉)    ⇒   ⊢ ((𝑉 ∈ LVec ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → (𝑋 ∼ 𝑌 ↔ (𝑁‘{𝑋}) = (𝑁‘{𝑌})))
Theorem	prjspeclsp 43206*	The vectors equivalent to a vector 𝑋 are the nonzero vectors in the span of 𝑋. (Contributed by Steven Nguyen, 6-Jun-2023.)
⊢ ∼ = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ ∃𝑙 ∈ 𝐾 𝑥 = (𝑙 · 𝑦))}    &   ⊢ 𝐵 = ((Base‘𝑉) ∖ {(0g‘𝑉)})    &   ⊢ 𝑆 = (Scalar‘𝑉)    &   ⊢ · = ( ·𝑠 ‘𝑉)    &   ⊢ 𝐾 = (Base‘𝑆)    &   ⊢ 𝑁 = (LSpan‘𝑉)    ⇒   ⊢ ((𝑉 ∈ LVec ∧ 𝑋 ∈ 𝐵) → [𝑋] ∼ = ((𝑁‘{𝑋}) ∖ {(0g‘𝑉)}))
Theorem	prjspval2 43207*	Alternate definition of projective space. (Contributed by Steven Nguyen, 7-Jun-2023.)
⊢ 0 = (0g‘𝑉)    &   ⊢ 𝐵 = ((Base‘𝑉) ∖ { 0 })    &   ⊢ 𝑁 = (LSpan‘𝑉)    ⇒   ⊢ (𝑉 ∈ LVec → (ℙ𝕣𝕠𝕛‘𝑉) = ∪ 𝑧 ∈ 𝐵 {((𝑁‘{𝑧}) ∖ { 0 })})
Syntax	cprjspn 43208	Extend class notation with the n-dimensional projective space function.
class ℙ𝕣𝕠𝕛n
Definition	df-prjspn 43209*	Define the n-dimensional projective space function. A projective space of dimension 1 is a projective line, and a projective space of dimension 2 is a projective plane. Compare df-ehl 25506. This space is considered n-dimensional because the vector space (𝑘 freeLMod (0...𝑛)) is (n+1)-dimensional and the ℙ𝕣𝕠𝕛 function returns equivalence classes with respect to a linear (1-dimensional) relation. (Contributed by BJ and Steven Nguyen, 29-Apr-2023.)
⊢ ℙ𝕣𝕠𝕛n = (𝑛 ∈ ℕ0, 𝑘 ∈ DivRing ↦ (ℙ𝕣𝕠𝕛‘(𝑘 freeLMod (0...𝑛))))
Theorem	prjspnval 43210	Value of the n-dimensional projective space function. (Contributed by Steven Nguyen, 1-May-2023.)
⊢ ((𝑁 ∈ ℕ0 ∧ 𝐾 ∈ DivRing) → (𝑁ℙ𝕣𝕠𝕛n𝐾) = (ℙ𝕣𝕠𝕛‘(𝐾 freeLMod (0...𝑁))))
Theorem	prjspnerlem 43211*	A lemma showing that the equivalence relation used in prjspnval2 43212 and the equivalence relation used in prjspval 43197 are equal, but only with the antecedent 𝐾 ∈ DivRing. (Contributed by SN, 15-Jul-2023.)
⊢ ∼ = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ ∃𝑙 ∈ 𝑆 𝑥 = (𝑙 · 𝑦))}    &   ⊢ 𝑊 = (𝐾 freeLMod (0...𝑁))    &   ⊢ 𝐵 = ((Base‘𝑊) ∖ {(0g‘𝑊)})    &   ⊢ 𝑆 = (Base‘𝐾)    &   ⊢ · = ( ·𝑠 ‘𝑊)    ⇒   ⊢ (𝐾 ∈ DivRing → ∼ = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ ∃𝑙 ∈ (Base‘(Scalar‘𝑊))𝑥 = (𝑙 · 𝑦))})
Theorem	prjspnval2 43212*	Value of the n-dimensional projective space function, expanded. (Contributed by Steven Nguyen, 15-Jul-2023.)
⊢ ∼ = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ ∃𝑙 ∈ 𝑆 𝑥 = (𝑙 · 𝑦))}    &   ⊢ 𝑊 = (𝐾 freeLMod (0...𝑁))    &   ⊢ 𝐵 = ((Base‘𝑊) ∖ {(0g‘𝑊)})    &   ⊢ 𝑆 = (Base‘𝐾)    &   ⊢ · = ( ·𝑠 ‘𝑊)    ⇒   ⊢ ((𝑁 ∈ ℕ0 ∧ 𝐾 ∈ DivRing) → (𝑁ℙ𝕣𝕠𝕛n𝐾) = (𝐵 / ∼ ))
Theorem	prjspner 43213*	The relation used to define ℙ𝕣𝕠𝕛 (and indirectly ℙ𝕣𝕠𝕛n through df-prjspn 43209) is an equivalence relation. This is a lemma that converts the equivalence relation used in results like prjspertr 43199 and prjspersym 43201 (see prjspnerlem 43211). Several theorems are covered in one thanks to the theorems around df-er 8682. (Contributed by SN, 14-Aug-2023.)
⊢ ∼ = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ ∃𝑙 ∈ 𝑆 𝑥 = (𝑙 · 𝑦))}    &   ⊢ 𝑊 = (𝐾 freeLMod (0...𝑁))    &   ⊢ 𝐵 = ((Base‘𝑊) ∖ {(0g‘𝑊)})    &   ⊢ 𝑆 = (Base‘𝐾)    &   ⊢ · = ( ·𝑠 ‘𝑊)    &   ⊢ (𝜑 → 𝐾 ∈ DivRing)    ⇒   ⊢ (𝜑 → ∼ Er 𝐵)
Theorem	prjspnvs 43214*	A nonzero multiple of a vector is equivalent to the vector. This converts the equivalence relation used in prjspvs 43204 (see prjspnerlem 43211). (Contributed by SN, 8-Aug-2024.)
⊢ ∼ = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ ∃𝑙 ∈ 𝑆 𝑥 = (𝑙 · 𝑦))}    &   ⊢ 𝑊 = (𝐾 freeLMod (0...𝑁))    &   ⊢ 𝐵 = ((Base‘𝑊) ∖ {(0g‘𝑊)})    &   ⊢ 𝑆 = (Base‘𝐾)    &   ⊢ · = ( ·𝑠 ‘𝑊)    &   ⊢ 0 = (0g‘𝐾)    &   ⊢ (𝜑 → 𝐾 ∈ DivRing)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑆)    &   ⊢ (𝜑 → 𝐶 ≠ 0 )    ⇒   ⊢ (𝜑 → (𝐶 · 𝑋) ∼ 𝑋)
Theorem	prjspnssbas 43215	A projective point spans a subset of the (nonzero) affine points. (Contributed by SN, 17-Jan-2025.)
⊢ 𝑃 = (𝑁ℙ𝕣𝕠𝕛n𝐾)    &   ⊢ 𝑊 = (𝐾 freeLMod (0...𝑁))    &   ⊢ 𝐵 = ((Base‘𝑊) ∖ {(0g‘𝑊)})    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    &   ⊢ (𝜑 → 𝐾 ∈ DivRing)    ⇒   ⊢ (𝜑 → 𝑃 ⊆ 𝒫 𝐵)
Theorem	prjspnn0 43216	A projective point is nonempty. (Contributed by SN, 17-Jan-2025.)
⊢ 𝑃 = (𝑁ℙ𝕣𝕠𝕛n𝐾)    &   ⊢ 𝑊 = (𝐾 freeLMod (0...𝑁))    &   ⊢ 𝐵 = ((Base‘𝑊) ∖ {(0g‘𝑊)})    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    &   ⊢ (𝜑 → 𝐾 ∈ DivRing)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑃)    ⇒   ⊢ (𝜑 → 𝐴 ≠ ∅)
Theorem	0prjspnlem 43217	Lemma for 0prjspn 43222. The given unit vector is a nonzero vector. (Contributed by Steven Nguyen, 16-Jul-2023.)
⊢ 𝐵 = ((Base‘𝑊) ∖ {(0g‘𝑊)})    &   ⊢ 𝑊 = (𝐾 freeLMod (0...0))    &   ⊢ 1 = ((𝐾 unitVec (0...0))‘0)    ⇒   ⊢ (𝐾 ∈ DivRing → 1 ∈ 𝐵)
Theorem	prjspnfv01 43218*	Any vector is equivalent to a vector whose zeroth coordinate is 0 or 1 (proof of the value of the zeroth coordinate). (Contributed by SN, 13-Aug-2023.)
⊢ 𝐹 = (𝑏 ∈ 𝐵 ↦ if((𝑏‘0) = 0 , 𝑏, ((𝐼‘(𝑏‘0)) · 𝑏)))    &   ⊢ 𝐵 = ((Base‘𝑊) ∖ {(0g‘𝑊)})    &   ⊢ 𝑊 = (𝐾 freeLMod (0...𝑁))    &   ⊢ · = ( ·𝑠 ‘𝑊)    &   ⊢ 0 = (0g‘𝐾)    &   ⊢ 1 = (1r‘𝐾)    &   ⊢ 𝐼 = (invr‘𝐾)    &   ⊢ (𝜑 → 𝐾 ∈ DivRing)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    ⇒   ⊢ (𝜑 → ((𝐹‘𝑋)‘0) = if((𝑋‘0) = 0 , 0 , 1 ))
Theorem	prjspner01 43219*	Any vector is equivalent to a vector whose zeroth coordinate is 0 or 1 (proof of the equivalence). (Contributed by SN, 13-Aug-2023.)
⊢ ∼ = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ ∃𝑙 ∈ 𝑆 𝑥 = (𝑙 · 𝑦))}    &   ⊢ 𝐹 = (𝑏 ∈ 𝐵 ↦ if((𝑏‘0) = 0 , 𝑏, ((𝐼‘(𝑏‘0)) · 𝑏)))    &   ⊢ 𝐵 = ((Base‘𝑊) ∖ {(0g‘𝑊)})    &   ⊢ 𝑊 = (𝐾 freeLMod (0...𝑁))    &   ⊢ · = ( ·𝑠 ‘𝑊)    &   ⊢ 𝑆 = (Base‘𝐾)    &   ⊢ 0 = (0g‘𝐾)    &   ⊢ 𝐼 = (invr‘𝐾)    &   ⊢ (𝜑 → 𝐾 ∈ DivRing)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    ⇒   ⊢ (𝜑 → 𝑋 ∼ (𝐹‘𝑋))
Theorem	prjspner1 43220*	Two vectors whose zeroth coordinate is nonzero are equivalent if and only if they have the same representative in the (n-1)-dimensional affine subspace { x0 = 1 } . For example, vectors in 3D space whose 𝑥 coordinate is nonzero are equivalent iff they intersect at the plane 𝑥 = 1 at the same point (also see section header). (Contributed by SN, 13-Aug-2023.)
⊢ ∼ = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ ∃𝑙 ∈ 𝑆 𝑥 = (𝑙 · 𝑦))}    &   ⊢ 𝐹 = (𝑏 ∈ 𝐵 ↦ if((𝑏‘0) = 0 , 𝑏, ((𝐼‘(𝑏‘0)) · 𝑏)))    &   ⊢ 𝐵 = ((Base‘𝑊) ∖ {(0g‘𝑊)})    &   ⊢ 𝑊 = (𝐾 freeLMod (0...𝑁))    &   ⊢ · = ( ·𝑠 ‘𝑊)    &   ⊢ 𝑆 = (Base‘𝐾)    &   ⊢ 0 = (0g‘𝐾)    &   ⊢ 𝐼 = (invr‘𝐾)    &   ⊢ (𝜑 → 𝐾 ∈ DivRing)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → (𝑋‘0) ≠ 0 )    &   ⊢ (𝜑 → (𝑌‘0) ≠ 0 )    ⇒   ⊢ (𝜑 → (𝑋 ∼ 𝑌 ↔ (𝐹‘𝑋) = (𝐹‘𝑌)))
Theorem	0prjspnrel 43221*	In the zero-dimensional projective space, all vectors are equivalent to the unit vector. (Contributed by Steven Nguyen, 7-Jun-2023.)
⊢ ∼ = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ ∃𝑙 ∈ 𝑆 𝑥 = (𝑙 · 𝑦))}    &   ⊢ 𝐵 = ((Base‘𝑊) ∖ {(0g‘𝑊)})    &   ⊢ · = ( ·𝑠 ‘𝑊)    &   ⊢ 𝑆 = (Base‘𝐾)    &   ⊢ 𝑊 = (𝐾 freeLMod (0...0))    &   ⊢ 1 = ((𝐾 unitVec (0...0))‘0)    ⇒   ⊢ ((𝐾 ∈ DivRing ∧ 𝑋 ∈ 𝐵) → 𝑋 ∼ 1 )
Theorem	0prjspn 43222	A zero-dimensional projective space has only 1 point. (Contributed by Steven Nguyen, 9-Jun-2023.)
⊢ 𝑊 = (𝐾 freeLMod (0...0))    &   ⊢ 𝐵 = ((Base‘𝑊) ∖ {(0g‘𝑊)})    ⇒   ⊢ (𝐾 ∈ DivRing → (0ℙ𝕣𝕠𝕛n𝐾) = {𝐵})
Syntax	cprjcrv 43223	Extend class notation with the projective curve function.
class ℙ𝕣𝕠𝕛Crv
Definition	df-prjcrv 43224*	Define the projective curve function. This takes a homogeneous polynomial and outputs the homogeneous coordinates where the polynomial evaluates to zero (the "zero set"). (In other words, scalar multiples are collapsed into the same projective point. See mhphf4 43194 and prjspvs 43204). (Contributed by SN, 23-Nov-2024.)
⊢ ℙ𝕣𝕠𝕛Crv = (𝑛 ∈ ℕ0, 𝑘 ∈ Field ↦ (𝑓 ∈ ∪ ran ((0...𝑛) mHomP 𝑘) ↦ {𝑝 ∈ (𝑛ℙ𝕣𝕠𝕛n𝑘) ∣ ((((0...𝑛) eval 𝑘)‘𝑓) “ 𝑝) = {(0g‘𝑘)}}))
Theorem	prjcrvfval 43225*	Value of the projective curve function. (Contributed by SN, 23-Nov-2024.)
⊢ 𝐻 = ((0...𝑁) mHomP 𝐾)    &   ⊢ 𝐸 = ((0...𝑁) eval 𝐾)    &   ⊢ 𝑃 = (𝑁ℙ𝕣𝕠𝕛n𝐾)    &   ⊢ 0 = (0g‘𝐾)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    &   ⊢ (𝜑 → 𝐾 ∈ Field)    ⇒   ⊢ (𝜑 → (𝑁ℙ𝕣𝕠𝕛Crv𝐾) = (𝑓 ∈ ∪ ran 𝐻 ↦ {𝑝 ∈ 𝑃 ∣ ((𝐸‘𝑓) “ 𝑝) = { 0 }}))
Theorem	prjcrvval 43226*	Value of the projective curve function. (Contributed by SN, 23-Nov-2024.)
⊢ 𝐻 = ((0...𝑁) mHomP 𝐾)    &   ⊢ 𝐸 = ((0...𝑁) eval 𝐾)    &   ⊢ 𝑃 = (𝑁ℙ𝕣𝕠𝕛n𝐾)    &   ⊢ 0 = (0g‘𝐾)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    &   ⊢ (𝜑 → 𝐾 ∈ Field)    &   ⊢ (𝜑 → 𝐹 ∈ ∪ ran 𝐻)    ⇒   ⊢ (𝜑 → ((𝑁ℙ𝕣𝕠𝕛Crv𝐾)‘𝐹) = {𝑝 ∈ 𝑃 ∣ ((𝐸‘𝐹) “ 𝑝) = { 0 }})
Theorem	prjcrv0 43227	The "curve" (zero set) corresponding to the zero polynomial contains all coordinates. (Contributed by SN, 23-Nov-2024.)
⊢ 𝑌 = ((0...𝑁) mPoly 𝐾)    &   ⊢ 0 = (0g‘𝑌)    &   ⊢ 𝑃 = (𝑁ℙ𝕣𝕠𝕛n𝐾)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    &   ⊢ (𝜑 → 𝐾 ∈ Field)    ⇒   ⊢ (𝜑 → ((𝑁ℙ𝕣𝕠𝕛Crv𝐾)‘ 0 ) = 𝑃)
21.30.8  Basic reductions for Fermat's Last Theorem
Theorem	dffltz 43228*	Fermat's Last Theorem (FLT) for nonzero integers is equivalent to the original scope of natural numbers. The backwards direction takes (𝑎↑𝑛) + (𝑏↑𝑛) = (𝑐↑𝑛), and adds the negative of any negative term to both sides, thus creating the corresponding equation with only positive integers. There are six combinations of negativity, so the proof is particularly long. (Contributed by Steven Nguyen, 27-Feb-2023.)
⊢ (∀𝑛 ∈ (ℤ≥‘3)∀𝑥 ∈ ℕ ∀𝑦 ∈ ℕ ∀𝑧 ∈ ℕ ((𝑥↑𝑛) + (𝑦↑𝑛)) ≠ (𝑧↑𝑛) ↔ ∀𝑛 ∈ (ℤ≥‘3)∀𝑎 ∈ (ℤ ∖ {0})∀𝑏 ∈ (ℤ ∖ {0})∀𝑐 ∈ (ℤ ∖ {0})((𝑎↑𝑛) + (𝑏↑𝑛)) ≠ (𝑐↑𝑛))
Theorem	fltmul 43229	A counterexample to FLT stays valid when scaled. The hypotheses are more general than they need to be for convenience. (There does not seem to be a standard term for Fermat or Pythagorean triples extended to any 𝑁 ∈ ℕ0, so the label is more about the context in which this theorem is used). (Contributed by SN, 20-Aug-2024.)
⊢ (𝜑 → 𝑆 ∈ ℂ)    &   ⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    &   ⊢ (𝜑 → ((𝐴↑𝑁) + (𝐵↑𝑁)) = (𝐶↑𝑁))    ⇒   ⊢ (𝜑 → (((𝑆 · 𝐴)↑𝑁) + ((𝑆 · 𝐵)↑𝑁)) = ((𝑆 · 𝐶)↑𝑁))
Theorem	fltdiv 43230	A counterexample to FLT stays valid when scaled. The hypotheses are more general than they need to be for convenience. (Contributed by SN, 20-Aug-2024.)
⊢ (𝜑 → 𝑆 ∈ ℂ)    &   ⊢ (𝜑 → 𝑆 ≠ 0)    &   ⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    &   ⊢ (𝜑 → ((𝐴↑𝑁) + (𝐵↑𝑁)) = (𝐶↑𝑁))    ⇒   ⊢ (𝜑 → (((𝐴 / 𝑆)↑𝑁) + ((𝐵 / 𝑆)↑𝑁)) = ((𝐶 / 𝑆)↑𝑁))
Theorem	flt0 43231	A counterexample for FLT does not exist for 𝑁 = 0. (Contributed by SN, 20-Aug-2024.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    &   ⊢ (𝜑 → ((𝐴↑𝑁) + (𝐵↑𝑁)) = (𝐶↑𝑁))    ⇒   ⊢ (𝜑 → 𝑁 ∈ ℕ)
Theorem	fltdvdsabdvdsc 43232	Any factor of both 𝐴 and 𝐵 also divides 𝐶. This establishes the validity of fltabcoprmex 43233. (Contributed by SN, 21-Aug-2024.)
⊢ (𝜑 → 𝐴 ∈ ℕ)    &   ⊢ (𝜑 → 𝐵 ∈ ℕ)    &   ⊢ (𝜑 → 𝐶 ∈ ℕ)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → ((𝐴↑𝑁) + (𝐵↑𝑁)) = (𝐶↑𝑁))    ⇒   ⊢ (𝜑 → (𝐴 gcd 𝐵) ∥ 𝐶)
Theorem	fltabcoprmex 43233	A counterexample to FLT implies a counterexample to FLT with 𝐴, 𝐵 (assigned to 𝐴 / (𝐴 gcd 𝐵) and 𝐵 / (𝐴 gcd 𝐵)) coprime (by divgcdcoprm0 16713). (Contributed by SN, 20-Aug-2024.)
⊢ (𝜑 → 𝐴 ∈ ℕ)    &   ⊢ (𝜑 → 𝐵 ∈ ℕ)    &   ⊢ (𝜑 → 𝐶 ∈ ℕ)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    &   ⊢ (𝜑 → ((𝐴↑𝑁) + (𝐵↑𝑁)) = (𝐶↑𝑁))    ⇒   ⊢ (𝜑 → (((𝐴 / (𝐴 gcd 𝐵))↑𝑁) + ((𝐵 / (𝐴 gcd 𝐵))↑𝑁)) = ((𝐶 / (𝐴 gcd 𝐵))↑𝑁))
Theorem	fltaccoprm 43234	A counterexample to FLT with 𝐴, 𝐵 coprime also has 𝐴, 𝐶 coprime. (Contributed by SN, 20-Aug-2024.)
⊢ (𝜑 → 𝐴 ∈ ℕ)    &   ⊢ (𝜑 → 𝐵 ∈ ℕ)    &   ⊢ (𝜑 → 𝐶 ∈ ℕ)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    &   ⊢ (𝜑 → ((𝐴↑𝑁) + (𝐵↑𝑁)) = (𝐶↑𝑁))    &   ⊢ (𝜑 → (𝐴 gcd 𝐵) = 1)    ⇒   ⊢ (𝜑 → (𝐴 gcd 𝐶) = 1)
Theorem	fltbccoprm 43235	A counterexample to FLT with 𝐴, 𝐵 coprime also has 𝐵, 𝐶 coprime. Proven from fltaccoprm 43234 using commutativity of addition. (Contributed by SN, 20-Aug-2024.)
⊢ (𝜑 → 𝐴 ∈ ℕ)    &   ⊢ (𝜑 → 𝐵 ∈ ℕ)    &   ⊢ (𝜑 → 𝐶 ∈ ℕ)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    &   ⊢ (𝜑 → ((𝐴↑𝑁) + (𝐵↑𝑁)) = (𝐶↑𝑁))    &   ⊢ (𝜑 → (𝐴 gcd 𝐵) = 1)    ⇒   ⊢ (𝜑 → (𝐵 gcd 𝐶) = 1)
Theorem	fltabcoprm 43236	A counterexample to FLT with 𝐴, 𝐶 coprime also has 𝐴, 𝐵 coprime. Converse of fltaccoprm 43234. (Contributed by SN, 22-Aug-2024.)
⊢ (𝜑 → 𝐴 ∈ ℕ)    &   ⊢ (𝜑 → 𝐵 ∈ ℕ)    &   ⊢ (𝜑 → 𝐶 ∈ ℕ)    &   ⊢ (𝜑 → (𝐴 gcd 𝐶) = 1)    &   ⊢ (𝜑 → ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2))    ⇒   ⊢ (𝜑 → (𝐴 gcd 𝐵) = 1)
Theorem	infdesc 43237*	Infinite descent. The hypotheses say that 𝑆 is lower bounded, and that if 𝜓 holds for an integer in 𝑆, it holds for a smaller integer in 𝑆. By infinite descent, eventually we cannot go any smaller, therefore 𝜓 holds for no integer in 𝑆. (Contributed by SN, 20-Aug-2024.)
⊢ (𝑦 = 𝑥 → (𝜓 ↔ 𝜒))    &   ⊢ (𝑦 = 𝑧 → (𝜓 ↔ 𝜃))    &   ⊢ (𝜑 → 𝑆 ⊆ (ℤ≥‘𝑀))    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝜒)) → ∃𝑧 ∈ 𝑆 (𝜃 ∧ 𝑧 < 𝑥))    ⇒   ⊢ (𝜑 → {𝑦 ∈ 𝑆 ∣ 𝜓} = ∅)
Theorem	fltne 43238	If a counterexample to FLT exists, its addends are not equal. (Contributed by SN, 1-Jun-2023.)
⊢ (𝜑 → 𝐴 ∈ ℕ)    &   ⊢ (𝜑 → 𝐵 ∈ ℕ)    &   ⊢ (𝜑 → 𝐶 ∈ ℕ)    &   ⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘2))    &   ⊢ (𝜑 → ((𝐴↑𝑁) + (𝐵↑𝑁)) = (𝐶↑𝑁))    ⇒   ⊢ (𝜑 → 𝐴 ≠ 𝐵)
Theorem	flt4lem 43239	Raising a number to the fourth power is equivalent to squaring it twice. (Contributed by SN, 21-Aug-2024.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    ⇒   ⊢ (𝜑 → (𝐴↑4) = ((𝐴↑2)↑2))
Theorem	flt4lem1 43240	Satisfy the antecedent used in several pythagtrip 16884 lemmas, with 𝐴, 𝐶 coprime rather than 𝐴, 𝐵. (Contributed by SN, 21-Aug-2024.)
⊢ (𝜑 → 𝐴 ∈ ℕ)    &   ⊢ (𝜑 → 𝐵 ∈ ℕ)    &   ⊢ (𝜑 → 𝐶 ∈ ℕ)    &   ⊢ (𝜑 → ¬ 2 ∥ 𝐴)    &   ⊢ (𝜑 → (𝐴 gcd 𝐶) = 1)    &   ⊢ (𝜑 → ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2))    ⇒   ⊢ (𝜑 → ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2) ∧ ((𝐴 gcd 𝐵) = 1 ∧ ¬ 2 ∥ 𝐴)))
Theorem	flt4lem2 43241	If 𝐴 is even, 𝐵 is odd. (Contributed by SN, 22-Aug-2024.)
⊢ (𝜑 → 𝐴 ∈ ℕ)    &   ⊢ (𝜑 → 𝐵 ∈ ℕ)    &   ⊢ (𝜑 → 𝐶 ∈ ℕ)    &   ⊢ (𝜑 → 2 ∥ 𝐴)    &   ⊢ (𝜑 → (𝐴 gcd 𝐶) = 1)    &   ⊢ (𝜑 → ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2))    ⇒   ⊢ (𝜑 → ¬ 2 ∥ 𝐵)
Theorem	flt4lem3 43242	Equivalent to pythagtriplem4 16869. Show that 𝐶 + 𝐴 and 𝐶 − 𝐴 are coprime. (Contributed by SN, 22-Aug-2024.)
⊢ (𝜑 → 𝐴 ∈ ℕ)    &   ⊢ (𝜑 → 𝐵 ∈ ℕ)    &   ⊢ (𝜑 → 𝐶 ∈ ℕ)    &   ⊢ (𝜑 → 2 ∥ 𝐴)    &   ⊢ (𝜑 → (𝐴 gcd 𝐶) = 1)    &   ⊢ (𝜑 → ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2))    ⇒   ⊢ (𝜑 → ((𝐶 + 𝐴) gcd (𝐶 − 𝐴)) = 1)
Theorem	flt4lem4 43243	If the product of two coprime factors is a perfect square, the factors are perfect squares. (Contributed by SN, 22-Aug-2024.)
⊢ (𝜑 → 𝐴 ∈ ℕ)    &   ⊢ (𝜑 → 𝐵 ∈ ℕ)    &   ⊢ (𝜑 → 𝐶 ∈ ℕ)    &   ⊢ (𝜑 → (𝐴 gcd 𝐵) = 1)    &   ⊢ (𝜑 → (𝐴 · 𝐵) = (𝐶↑2))    ⇒   ⊢ (𝜑 → (𝐴 = ((𝐴 gcd 𝐶)↑2) ∧ 𝐵 = ((𝐵 gcd 𝐶)↑2)))
Theorem	flt4lem5 43244	In the context of the lemmas of pythagtrip 16884, 𝑀 and 𝑁 are coprime. (Contributed by SN, 23-Aug-2024.)
⊢ 𝑀 = (((√‘(𝐶 + 𝐵)) + (√‘(𝐶 − 𝐵))) / 2)    &   ⊢ 𝑁 = (((√‘(𝐶 + 𝐵)) − (√‘(𝐶 − 𝐵))) / 2)    ⇒   ⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2) ∧ ((𝐴 gcd 𝐵) = 1 ∧ ¬ 2 ∥ 𝐴)) → (𝑀 gcd 𝑁) = 1)
Theorem	flt4lem5elem 43245	Version of fltaccoprm 43234 and fltbccoprm 43235 where 𝑀 is not squared. This can be proved in general for any polynomial in three variables: using prmdvdsncoprmbd 16776, dvds2addd 16340, and prmdvdsexp 16764, we can show that if two variables are coprime, the third is also coprime to the two. (Contributed by SN, 24-Aug-2024.)
⊢ (𝜑 → 𝑀 ∈ ℕ)    &   ⊢ (𝜑 → 𝑅 ∈ ℕ)    &   ⊢ (𝜑 → 𝑆 ∈ ℕ)    &   ⊢ (𝜑 → 𝑀 = ((𝑅↑2) + (𝑆↑2)))    &   ⊢ (𝜑 → (𝑅 gcd 𝑆) = 1)    ⇒   ⊢ (𝜑 → ((𝑅 gcd 𝑀) = 1 ∧ (𝑆 gcd 𝑀) = 1))
Theorem	flt4lem5a 43246	Part 1 of Equation 1 of https://crypto.stanford.edu/pbc/notes/numberfield/fermatn4.html. (Contributed by SN, 22-Aug-2024.)
⊢ 𝑀 = (((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2)    &   ⊢ 𝑁 = (((√‘(𝐶 + (𝐵↑2))) − (√‘(𝐶 − (𝐵↑2)))) / 2)    &   ⊢ 𝑅 = (((√‘(𝑀 + 𝑁)) + (√‘(𝑀 − 𝑁))) / 2)    &   ⊢ 𝑆 = (((√‘(𝑀 + 𝑁)) − (√‘(𝑀 − 𝑁))) / 2)    &   ⊢ (𝜑 → 𝐴 ∈ ℕ)    &   ⊢ (𝜑 → 𝐵 ∈ ℕ)    &   ⊢ (𝜑 → 𝐶 ∈ ℕ)    &   ⊢ (𝜑 → ¬ 2 ∥ 𝐴)    &   ⊢ (𝜑 → (𝐴 gcd 𝐶) = 1)    &   ⊢ (𝜑 → ((𝐴↑4) + (𝐵↑4)) = (𝐶↑2))    ⇒   ⊢ (𝜑 → ((𝐴↑2) + (𝑁↑2)) = (𝑀↑2))
Theorem	flt4lem5b 43247	Part 2 of Equation 1 of https://crypto.stanford.edu/pbc/notes/numberfield/fermatn4.html. (Contributed by SN, 22-Aug-2024.)
⊢ 𝑀 = (((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2)    &   ⊢ 𝑁 = (((√‘(𝐶 + (𝐵↑2))) − (√‘(𝐶 − (𝐵↑2)))) / 2)    &   ⊢ 𝑅 = (((√‘(𝑀 + 𝑁)) + (√‘(𝑀 − 𝑁))) / 2)    &   ⊢ 𝑆 = (((√‘(𝑀 + 𝑁)) − (√‘(𝑀 − 𝑁))) / 2)    &   ⊢ (𝜑 → 𝐴 ∈ ℕ)    &   ⊢ (𝜑 → 𝐵 ∈ ℕ)    &   ⊢ (𝜑 → 𝐶 ∈ ℕ)    &   ⊢ (𝜑 → ¬ 2 ∥ 𝐴)    &   ⊢ (𝜑 → (𝐴 gcd 𝐶) = 1)    &   ⊢ (𝜑 → ((𝐴↑4) + (𝐵↑4)) = (𝐶↑2))    ⇒   ⊢ (𝜑 → (2 · (𝑀 · 𝑁)) = (𝐵↑2))
Theorem	flt4lem5c 43248	Part 2 of Equation 2 of https://crypto.stanford.edu/pbc/notes/numberfield/fermatn4.html. (Contributed by SN, 22-Aug-2024.)
⊢ 𝑀 = (((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2)    &   ⊢ 𝑁 = (((√‘(𝐶 + (𝐵↑2))) − (√‘(𝐶 − (𝐵↑2)))) / 2)    &   ⊢ 𝑅 = (((√‘(𝑀 + 𝑁)) + (√‘(𝑀 − 𝑁))) / 2)    &   ⊢ 𝑆 = (((√‘(𝑀 + 𝑁)) − (√‘(𝑀 − 𝑁))) / 2)    &   ⊢ (𝜑 → 𝐴 ∈ ℕ)    &   ⊢ (𝜑 → 𝐵 ∈ ℕ)    &   ⊢ (𝜑 → 𝐶 ∈ ℕ)    &   ⊢ (𝜑 → ¬ 2 ∥ 𝐴)    &   ⊢ (𝜑 → (𝐴 gcd 𝐶) = 1)    &   ⊢ (𝜑 → ((𝐴↑4) + (𝐵↑4)) = (𝐶↑2))    ⇒   ⊢ (𝜑 → 𝑁 = (2 · (𝑅 · 𝑆)))
Theorem	flt4lem5d 43249	Part 3 of Equation 2 of https://crypto.stanford.edu/pbc/notes/numberfield/fermatn4.html. (Contributed by SN, 23-Aug-2024.)
⊢ 𝑀 = (((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2)    &   ⊢ 𝑁 = (((√‘(𝐶 + (𝐵↑2))) − (√‘(𝐶 − (𝐵↑2)))) / 2)    &   ⊢ 𝑅 = (((√‘(𝑀 + 𝑁)) + (√‘(𝑀 − 𝑁))) / 2)    &   ⊢ 𝑆 = (((√‘(𝑀 + 𝑁)) − (√‘(𝑀 − 𝑁))) / 2)    &   ⊢ (𝜑 → 𝐴 ∈ ℕ)    &   ⊢ (𝜑 → 𝐵 ∈ ℕ)    &   ⊢ (𝜑 → 𝐶 ∈ ℕ)    &   ⊢ (𝜑 → ¬ 2 ∥ 𝐴)    &   ⊢ (𝜑 → (𝐴 gcd 𝐶) = 1)    &   ⊢ (𝜑 → ((𝐴↑4) + (𝐵↑4)) = (𝐶↑2))    ⇒   ⊢ (𝜑 → 𝑀 = ((𝑅↑2) + (𝑆↑2)))
Theorem	flt4lem5e 43250	Satisfy the hypotheses of flt4lem4 43243. (Contributed by SN, 23-Aug-2024.)
⊢ 𝑀 = (((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2)    &   ⊢ 𝑁 = (((√‘(𝐶 + (𝐵↑2))) − (√‘(𝐶 − (𝐵↑2)))) / 2)    &   ⊢ 𝑅 = (((√‘(𝑀 + 𝑁)) + (√‘(𝑀 − 𝑁))) / 2)    &   ⊢ 𝑆 = (((√‘(𝑀 + 𝑁)) − (√‘(𝑀 − 𝑁))) / 2)    &   ⊢ (𝜑 → 𝐴 ∈ ℕ)    &   ⊢ (𝜑 → 𝐵 ∈ ℕ)    &   ⊢ (𝜑 → 𝐶 ∈ ℕ)    &   ⊢ (𝜑 → ¬ 2 ∥ 𝐴)    &   ⊢ (𝜑 → (𝐴 gcd 𝐶) = 1)    &   ⊢ (𝜑 → ((𝐴↑4) + (𝐵↑4)) = (𝐶↑2))    ⇒   ⊢ (𝜑 → (((𝑅 gcd 𝑆) = 1 ∧ (𝑅 gcd 𝑀) = 1 ∧ (𝑆 gcd 𝑀) = 1) ∧ (𝑅 ∈ ℕ ∧ 𝑆 ∈ ℕ ∧ 𝑀 ∈ ℕ) ∧ ((𝑀 · (𝑅 · 𝑆)) = ((𝐵 / 2)↑2) ∧ (𝐵 / 2) ∈ ℕ)))
Theorem	flt4lem5f 43251	Final equation of https://crypto.stanford.edu/pbc/notes/numberfield/fermatn4.html. Given 𝐴↑4 + 𝐵↑4 = 𝐶↑2, provide a smaller solution. This satisfies the infinite descent condition. (Contributed by SN, 24-Aug-2024.)
⊢ 𝑀 = (((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2)    &   ⊢ 𝑁 = (((√‘(𝐶 + (𝐵↑2))) − (√‘(𝐶 − (𝐵↑2)))) / 2)    &   ⊢ 𝑅 = (((√‘(𝑀 + 𝑁)) + (√‘(𝑀 − 𝑁))) / 2)    &   ⊢ 𝑆 = (((√‘(𝑀 + 𝑁)) − (√‘(𝑀 − 𝑁))) / 2)    &   ⊢ (𝜑 → 𝐴 ∈ ℕ)    &   ⊢ (𝜑 → 𝐵 ∈ ℕ)    &   ⊢ (𝜑 → 𝐶 ∈ ℕ)    &   ⊢ (𝜑 → ¬ 2 ∥ 𝐴)    &   ⊢ (𝜑 → (𝐴 gcd 𝐶) = 1)    &   ⊢ (𝜑 → ((𝐴↑4) + (𝐵↑4)) = (𝐶↑2))    ⇒   ⊢ (𝜑 → ((𝑀 gcd (𝐵 / 2))↑2) = (((𝑅 gcd (𝐵 / 2))↑4) + ((𝑆 gcd (𝐵 / 2))↑4)))
Theorem	flt4lem6 43252	Remove shared factors in a solution to 𝐴↑4 + 𝐵↑4 = 𝐶↑2. (Contributed by SN, 24-Jul-2024.)
⊢ (𝜑 → 𝐴 ∈ ℕ)    &   ⊢ (𝜑 → 𝐵 ∈ ℕ)    &   ⊢ (𝜑 → 𝐶 ∈ ℕ)    &   ⊢ (𝜑 → ((𝐴↑4) + (𝐵↑4)) = (𝐶↑2))    ⇒   ⊢ (𝜑 → (((𝐴 / (𝐴 gcd 𝐵)) ∈ ℕ ∧ (𝐵 / (𝐴 gcd 𝐵)) ∈ ℕ ∧ (𝐶 / ((𝐴 gcd 𝐵)↑2)) ∈ ℕ) ∧ (((𝐴 / (𝐴 gcd 𝐵))↑4) + ((𝐵 / (𝐴 gcd 𝐵))↑4)) = ((𝐶 / ((𝐴 gcd 𝐵)↑2))↑2)))
Theorem	flt4lem7 43253*	Convert flt4lem5f 43251 into a convenient form for nna4b4nsq 43254. TODO-SN: The change to (𝐴 gcd 𝐵) = 1 points at some inefficiency in the lemmas. (Contributed by SN, 25-Aug-2024.)
⊢ (𝜑 → 𝐴 ∈ ℕ)    &   ⊢ (𝜑 → 𝐵 ∈ ℕ)    &   ⊢ (𝜑 → 𝐶 ∈ ℕ)    &   ⊢ (𝜑 → ¬ 2 ∥ 𝐴)    &   ⊢ (𝜑 → (𝐴 gcd 𝐵) = 1)    &   ⊢ (𝜑 → ((𝐴↑4) + (𝐵↑4)) = (𝐶↑2))    ⇒   ⊢ (𝜑 → ∃𝑙 ∈ ℕ (∃𝑔 ∈ ℕ ∃ℎ ∈ ℕ (¬ 2 ∥ 𝑔 ∧ ((𝑔 gcd ℎ) = 1 ∧ ((𝑔↑4) + (ℎ↑4)) = (𝑙↑2))) ∧ 𝑙 < 𝐶))
Theorem	nna4b4nsq 43254	Strengthening of Fermat's last theorem for exponent 4, where the sum is only assumed to be a square. (Contributed by SN, 23-Aug-2024.)
⊢ (𝜑 → 𝐴 ∈ ℕ)    &   ⊢ (𝜑 → 𝐵 ∈ ℕ)    &   ⊢ (𝜑 → 𝐶 ∈ ℕ)    ⇒   ⊢ (𝜑 → ((𝐴↑4) + (𝐵↑4)) ≠ (𝐶↑2))
Theorem	fltltc 43255	(𝐶↑𝑁) is the largest term and therefore 𝐵 < 𝐶. (Contributed by Steven Nguyen, 22-Aug-2023.)
⊢ (𝜑 → 𝐴 ∈ ℕ)    &   ⊢ (𝜑 → 𝐵 ∈ ℕ)    &   ⊢ (𝜑 → 𝐶 ∈ ℕ)    &   ⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘3))    &   ⊢ (𝜑 → ((𝐴↑𝑁) + (𝐵↑𝑁)) = (𝐶↑𝑁))    ⇒   ⊢ (𝜑 → 𝐵 < 𝐶)
Theorem	fltnltalem 43256	Lemma for fltnlta 43257. A lower bound for 𝐴 based on pwdif 15912. (Contributed by Steven Nguyen, 22-Aug-2023.)
⊢ (𝜑 → 𝐴 ∈ ℕ)    &   ⊢ (𝜑 → 𝐵 ∈ ℕ)    &   ⊢ (𝜑 → 𝐶 ∈ ℕ)    &   ⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘3))    &   ⊢ (𝜑 → ((𝐴↑𝑁) + (𝐵↑𝑁)) = (𝐶↑𝑁))    ⇒   ⊢ (𝜑 → ((𝐶 − 𝐵) · ((𝐶↑(𝑁 − 1)) + ((𝑁 − 1) · (𝐵↑(𝑁 − 1))))) < (𝐴↑𝑁))
Theorem	fltnlta 43257	In a Fermat counterexample, the exponent 𝑁 is less than all three numbers (𝐴, 𝐵, and 𝐶). Note that 𝐴 < 𝐵 (hypothesis) and 𝐵 < 𝐶 (fltltc 43255). See https://youtu.be/EymVXkPWxyc 43255 for an outline. (Contributed by SN, 24-Aug-2023.)
⊢ (𝜑 → 𝐴 ∈ ℕ)    &   ⊢ (𝜑 → 𝐵 ∈ ℕ)    &   ⊢ (𝜑 → 𝐶 ∈ ℕ)    &   ⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘3))    &   ⊢ (𝜑 → ((𝐴↑𝑁) + (𝐵↑𝑁)) = (𝐶↑𝑁))    &   ⊢ (𝜑 → 𝐴 < 𝐵)    ⇒   ⊢ (𝜑 → 𝑁 < 𝐴)
21.30.9  Exemplar theorems These theorems were added for illustration or pedagogical purposes without the intention of being used, but some may still be moved to main and used, of course.
Theorem	iddii 43258	Version of a1ii 2 with the hypotheses switched. The first hypothesis is redundant so this theorem should not normally appear in a proof. Inference associated with idd 25. (Contributed by SN, 1-Apr-2025.) (New usage is discouraged.)
⊢ 𝜑    &   ⊢ 𝜓    ⇒   ⊢ 𝜓
Theorem	bicomdALT 43259	Alternate proof of bicomd 226 which is shorter after expanding all parent theorems (as of 8-Aug-2024, bicom 225 depends on bicom1 224 and sylib 221 depends on syl 18). Additionally, the labels bicom1 224 and syl 18 happen to contain fewer characters than bicom 225 and sylib 221. However, neither of these conditions count as a shortening according to conventions 30660. In the first case, the criteria could easily be broken by upstream changes, and in many cases the upstream dependency tree is nontrivial (see orass 934 and pm2.31 935). For the latter case, theorem labels are up to revision, so they are not counted in the size of a proof. (Contributed by SN, 21-May-2022.) (New usage is discouraged.) (Proof modification is discouraged.)
⊢ (𝜑 → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (𝜒 ↔ 𝜓))
Theorem	alan 43260	Alias for 19.26 1893 for easier lookup. (Contributed by SN, 12-Aug-2025.) (New usage is discouraged.)
⊢ (∀𝑥(𝜑 ∧ 𝜓) ↔ (∀𝑥𝜑 ∧ ∀𝑥𝜓))
Theorem	exor 43261	Alias for 19.43 1905 for easier lookup. (Contributed by SN, 5-Jul-2025.) (New usage is discouraged.)
⊢ (∃𝑥(𝜑 ∨ 𝜓) ↔ (∃𝑥𝜑 ∨ ∃𝑥𝜓))
Theorem	rexor 43262	Alias for r19.43 3133 for easier lookup. (Contributed by SN, 5-Jul-2025.) (New usage is discouraged.)
⊢ (∃𝑥 ∈ 𝐴 (𝜑 ∨ 𝜓) ↔ (∃𝑥 ∈ 𝐴 𝜑 ∨ ∃𝑥 ∈ 𝐴 𝜓))
Theorem	ruvALT 43263	Alternate proof of ruv 9558 with one fewer syntax step thanks to using elirrv 9547 instead of elirr 9550. However, it does not change the compressed proof size or the number of symbols in the generated display, so it is not considered a shortening according to conventions 30660. (Contributed by SN, 1-Sep-2024.) (New usage is discouraged.) (Proof modification is discouraged.)
⊢ {𝑥 ∣ 𝑥 ∉ 𝑥} = V
Theorem	sn-wcdeq 43264	Alternative to wcdeq 3729 and df-cdeq 3730. This flattens the syntax representation ( wi ( weq vx vy ) wph ) to ( sn-wcdeq vx vy wph ), illustrating the comment of df-cdeq 3730. (Contributed by SN, 26-Sep-2024.) (New usage is discouraged.)
wff (𝑥 = 𝑦 → 𝜑)
Theorem	sq45 43265	45 squared is 2025. (Contributed by SN, 30-Mar-2025.)
⊢ (;45↑2) = ;;;2025
Theorem	sum9cubes 43266	The sum of the first nine perfect cubes is 2025. (Contributed by SN, 30-Mar-2025.)
⊢ Σ𝑘 ∈ (1...9)(𝑘↑3) = ;;;2025
Theorem	sn-isghm 43267*	Longer proof of isghm 19277, unsuccessfully attempting to simplify isghm 19277 using elovmpo 7645 according to an editorial note (now removed). (Contributed by SN, 7-Jun-2025.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝑋 = (Base‘𝑆)    &   ⊢ 𝑌 = (Base‘𝑇)    &   ⊢ + = (+g‘𝑆)    &   ⊢ ⨣ = (+g‘𝑇)    ⇒   ⊢ (𝐹 ∈ (𝑆 GrpHom 𝑇) ↔ ((𝑆 ∈ Grp ∧ 𝑇 ∈ Grp) ∧ (𝐹:𝑋⟶𝑌 ∧ ∀𝑢 ∈ 𝑋 ∀𝑣 ∈ 𝑋 (𝐹‘(𝑢 + 𝑣)) = ((𝐹‘𝑢) ⨣ (𝐹‘𝑣)))))
Theorem	aprilfools2025 43268	An abuse of notation. (Contributed by Prof. Loof Lirpa, 1-Apr-2025.) (New usage is discouraged.) (Proof modification is discouraged.)
⊢ {⟨“𝐴𝑝𝑟𝑖𝑙”⟩, ⟨“𝑓𝑜𝑜𝑙𝑠!”⟩} ∈ V
21.30.9.1  Standard replacements of ax-10 , ax-11 , ax-12 It is known that ax-10 2178, ax-11 2194, and ax-12 2215 are logically redundant in a weak sense. Practically, they can be replaced with hbn1w 2071, alcomimw 2066, and ax12wlem 2169 as long as you can fully substitute 𝑦 for 𝑥 in the relevant wff (that is, 𝑥 cannot appear in the wff after substituting). This strategy (which I will call a "standard replacement" of axioms) has a lot of potential, for example it works with df-fv 6533 and df-mpt 5187, two very common constructions. But doing a standard replacement of ax-10 2178, ax-11 2194, and ax-12 2215 takes unsatisfyingly long. Usually, if another approach is found, that approach is shorter and better.
Theorem	nfa1w 43269*	Replace ax-10 2178 in nfa1 2188 with a substitution hypothesis. (Contributed by SN, 2-Sep-2025.)
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ Ⅎ𝑥∀𝑥𝜑
Theorem	eu6w 43270*	Replace ax-10 2178, ax-12 2215 in eu6 2604 with substitution hypotheses. (Contributed by SN, 27-May-2025.)
⊢ (𝑥 = 𝑧 → (𝜑 ↔ 𝜓))    &   ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜃))    ⇒   ⊢ (∃!𝑥𝜑 ↔ ∃𝑦∀𝑥(𝜑 ↔ 𝑥 = 𝑦))
Theorem	abbibw 43271*	Replace ax-10 2178, ax-11 2194, ax-12 2215 in abbib 2834 with substitution hypotheses. (Contributed by SN, 27-May-2025.)
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜃))    &   ⊢ (𝑥 = 𝑦 → (𝜓 ↔ 𝜒))    ⇒   ⊢ ({𝑥 ∣ 𝜑} = {𝑥 ∣ 𝜓} ↔ ∀𝑥(𝜑 ↔ 𝜓))
Theorem	absnw 43272*	Replace ax-10 2178, ax-11 2194, ax-12 2215 in absn 4605 with a substitution hypothesis. (Contributed by SN, 27-May-2025.)
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ ({𝑥 ∣ 𝜑} = {𝑌} ↔ ∀𝑥(𝜑 ↔ 𝑥 = 𝑌))
Theorem	euabsn2w 43273*	Replace ax-10 2178, ax-11 2194, ax-12 2215 in euabsn2 4687 with substitution hypotheses. (Contributed by SN, 27-May-2025.)
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    &   ⊢ (𝑥 = 𝑧 → (𝜑 ↔ 𝜃))    ⇒   ⊢ (∃!𝑥𝜑 ↔ ∃𝑦{𝑥 ∣ 𝜑} = {𝑦})
21.31  Mathbox for Igor Ieskov
Theorem	cu3addd 43274	Cube of sum of three numbers. (Contributed by Igor Ieskov, 14-Dec-2023.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    ⇒   ⊢ (𝜑 → (((𝐴 + 𝐵) + 𝐶)↑3) = (((((𝐴↑3) + (3 · ((𝐴↑2) · 𝐵))) + ((3 · (𝐴 · (𝐵↑2))) + (𝐵↑3))) + (((3 · ((𝐴↑2) · 𝐶)) + (((3 · 2) · (𝐴 · 𝐵)) · 𝐶)) + (3 · ((𝐵↑2) · 𝐶)))) + (((3 · (𝐴 · (𝐶↑2))) + (3 · (𝐵 · (𝐶↑2)))) + (𝐶↑3))))
Theorem	negexpidd 43275	The sum of a real number to the power of N and the negative of the number to the power of N equals zero if N is a nonnegative odd integer. (Contributed by Igor Ieskov, 21-Jan-2024.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    &   ⊢ (𝜑 → ¬ 2 ∥ 𝑁)    ⇒   ⊢ (𝜑 → ((𝐴↑𝑁) + (-𝐴↑𝑁)) = 0)
Theorem	rexlimdv3d 43276*	An extended version of rexlimdvv 3221 to include three set variables. (Contributed by Igor Ieskov, 21-Jan-2024.)
⊢ (𝜑 → ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐶) → (𝜓 → 𝜒)))    ⇒   ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 ∃𝑧 ∈ 𝐶 𝜓 → 𝜒))
Theorem	3cubeslem1 43277	Lemma for 3cubes 43283. (Contributed by Igor Ieskov, 22-Jan-2024.)
⊢ (𝜑 → 𝐴 ∈ ℚ)    ⇒   ⊢ (𝜑 → 0 < (((𝐴 + 1)↑2) − 𝐴))
Theorem	3cubeslem2 43278	Lemma for 3cubes 43283. Used to show that the denominators in 3cubeslem4 43282 are nonzero. (Contributed by Igor Ieskov, 22-Jan-2024.)
⊢ (𝜑 → 𝐴 ∈ ℚ)    ⇒   ⊢ (𝜑 → ¬ ((((3↑3) · (𝐴↑2)) + ((3↑2) · 𝐴)) + 3) = 0)
Theorem	3cubeslem3l 43279	Lemma for 3cubes 43283. (Contributed by Igor Ieskov, 22-Jan-2024.)
⊢ (𝜑 → 𝐴 ∈ ℚ)    ⇒   ⊢ (𝜑 → (𝐴 · (((((3↑3) · (𝐴↑2)) + ((3↑2) · 𝐴)) + 3)↑3)) = (((𝐴↑7) · (3↑9)) + (((𝐴↑6) · (3↑9)) + (((𝐴↑5) · ((3↑8) + (3↑8))) + (((𝐴↑4) · (((3↑7) · 2) + (3↑6))) + (((𝐴↑3) · ((3↑6) + (3↑6))) + (((𝐴↑2) · (3↑5)) + (𝐴 · (3↑3)))))))))
Theorem	3cubeslem3r 43280	Lemma for 3cubes 43283. (Contributed by Igor Ieskov, 22-Jan-2024.)
⊢ (𝜑 → 𝐴 ∈ ℚ)    ⇒   ⊢ (𝜑 → ((((((3↑3) · (𝐴↑3)) − 1)↑3) + (((-((3↑3) · (𝐴↑3)) + ((3↑2) · 𝐴)) + 1)↑3)) + ((((3↑3) · (𝐴↑2)) + ((3↑2) · 𝐴))↑3)) = (((𝐴↑7) · (3↑9)) + (((𝐴↑6) · (3↑9)) + (((𝐴↑5) · ((3↑8) + (3↑8))) + (((𝐴↑4) · (((3↑7) · 2) + (3↑6))) + (((𝐴↑3) · ((3↑6) + (3↑6))) + (((𝐴↑2) · (3↑5)) + (𝐴 · (3↑3)))))))))
Theorem	3cubeslem3 43281	Lemma for 3cubes 43283. (Contributed by Igor Ieskov, 22-Jan-2024.)
⊢ (𝜑 → 𝐴 ∈ ℚ)    ⇒   ⊢ (𝜑 → (𝐴 · (((((3↑3) · (𝐴↑2)) + ((3↑2) · 𝐴)) + 3)↑3)) = ((((((3↑3) · (𝐴↑3)) − 1)↑3) + (((-((3↑3) · (𝐴↑3)) + ((3↑2) · 𝐴)) + 1)↑3)) + ((((3↑3) · (𝐴↑2)) + ((3↑2) · 𝐴))↑3)))
Theorem	3cubeslem4 43282	Lemma for 3cubes 43283. This is Ryley's explicit formula for decomposing a rational 𝐴 into a sum of three rational cubes. (Contributed by Igor Ieskov, 22-Jan-2024.)
⊢ (𝜑 → 𝐴 ∈ ℚ)    ⇒   ⊢ (𝜑 → 𝐴 = (((((((3↑3) · (𝐴↑3)) − 1) / ((((3↑3) · (𝐴↑2)) + ((3↑2) · 𝐴)) + 3))↑3) + ((((-((3↑3) · (𝐴↑3)) + ((3↑2) · 𝐴)) + 1) / ((((3↑3) · (𝐴↑2)) + ((3↑2) · 𝐴)) + 3))↑3)) + (((((3↑3) · (𝐴↑2)) + ((3↑2) · 𝐴)) / ((((3↑3) · (𝐴↑2)) + ((3↑2) · 𝐴)) + 3))↑3)))
Theorem	3cubes 43283*	Every rational number is a sum of three rational cubes. See S. Ryley, The Ladies' Diary 122 (1825), 35. (Contributed by Igor Ieskov, 22-Jan-2024.)
⊢ (𝐴 ∈ ℚ ↔ ∃𝑎 ∈ ℚ ∃𝑏 ∈ ℚ ∃𝑐 ∈ ℚ 𝐴 = (((𝑎↑3) + (𝑏↑3)) + (𝑐↑3)))
21.32  Mathbox for OpenAI
Theorem	rntrclfvOAI 43284	The range of the transitive closure is equal to the range of the relation. (Contributed by OpenAI, 7-Jul-2020.)
⊢ (𝑅 ∈ 𝑉 → ran (t+‘𝑅) = ran 𝑅)
21.33  Mathbox for Stefan O'Rear
21.33.1  Additional elementary logic and set theory
Theorem	moxfr 43285*	Transfer at-most-one between related expressions. (Contributed by Stefan O'Rear, 12-Feb-2015.)
⊢ 𝐴 ∈ V    &   ⊢ ∃!𝑦 𝑥 = 𝐴    &   ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∃*𝑥𝜑 ↔ ∃*𝑦𝜓)
21.33.2  Additional theory of functions
Theorem	imaiinfv 43286*	Indexed intersection of an image. (Contributed by Stefan O'Rear, 22-Feb-2015.)
⊢ ((𝐹 Fn 𝐴 ∧ 𝐵 ⊆ 𝐴) → ∩ 𝑥 ∈ 𝐵 (𝐹‘𝑥) = ∩ (𝐹 “ 𝐵))
21.33.3  Additional topology
Theorem	elrfi 43287*	Elementhood in a set of relative finite intersections. (Contributed by Stefan O'Rear, 22-Feb-2015.)
⊢ ((𝐵 ∈ 𝑉 ∧ 𝐶 ⊆ 𝒫 𝐵) → (𝐴 ∈ (fi‘({𝐵} ∪ 𝐶)) ↔ ∃𝑣 ∈ (𝒫 𝐶 ∩ Fin)𝐴 = (𝐵 ∩ ∩ 𝑣)))
Theorem	elrfirn 43288*	Elementhood in a set of relative finite intersections of an indexed family of sets. (Contributed by Stefan O'Rear, 22-Feb-2015.)
⊢ ((𝐵 ∈ 𝑉 ∧ 𝐹:𝐼⟶𝒫 𝐵) → (𝐴 ∈ (fi‘({𝐵} ∪ ran 𝐹)) ↔ ∃𝑣 ∈ (𝒫 𝐼 ∩ Fin)𝐴 = (𝐵 ∩ ∩ 𝑦 ∈ 𝑣 (𝐹‘𝑦))))
Theorem	elrfirn2 43289*	Elementhood in a set of relative finite intersections of an indexed family of sets (implicit). (Contributed by Stefan O'Rear, 22-Feb-2015.)
⊢ ((𝐵 ∈ 𝑉 ∧ ∀𝑦 ∈ 𝐼 𝐶 ⊆ 𝐵) → (𝐴 ∈ (fi‘({𝐵} ∪ ran (𝑦 ∈ 𝐼 ↦ 𝐶))) ↔ ∃𝑣 ∈ (𝒫 𝐼 ∩ Fin)𝐴 = (𝐵 ∩ ∩ 𝑦 ∈ 𝑣 𝐶)))
Theorem	cmpfiiin 43290*	In a compact topology, a system of closed sets with nonempty finite intersections has a nonempty intersection. (Contributed by Stefan O'Rear, 22-Feb-2015.)
⊢ 𝑋 = ∪ 𝐽    &   ⊢ (𝜑 → 𝐽 ∈ Comp)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐼) → 𝑆 ∈ (Clsd‘𝐽))    &   ⊢ ((𝜑 ∧ (𝑙 ⊆ 𝐼 ∧ 𝑙 ∈ Fin)) → (𝑋 ∩ ∩ 𝑘 ∈ 𝑙 𝑆) ≠ ∅)    ⇒   ⊢ (𝜑 → (𝑋 ∩ ∩ 𝑘 ∈ 𝐼 𝑆) ≠ ∅)
21.33.4  Characterization of closure operators. Kuratowski closure axioms
Theorem	ismrcd1 43291*	Any function from the subsets of a set to itself, which is extensive (satisfies mrcssid 17663), isotone (satisfies mrcss 17662), and idempotent (satisfies mrcidm 17665) has a collection of fixed points which is a Moore collection, and itself is the closure operator for that collection. This can be taken as an alternate definition for the closure operators. This is the first half, ismrcd2 43292 is the second. (Contributed by Stefan O'Rear, 1-Feb-2015.)
⊢ (𝜑 → 𝐵 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐹:𝒫 𝐵⟶𝒫 𝐵)    &   ⊢ ((𝜑 ∧ 𝑥 ⊆ 𝐵) → 𝑥 ⊆ (𝐹‘𝑥))    &   ⊢ ((𝜑 ∧ 𝑥 ⊆ 𝐵 ∧ 𝑦 ⊆ 𝑥) → (𝐹‘𝑦) ⊆ (𝐹‘𝑥))    &   ⊢ ((𝜑 ∧ 𝑥 ⊆ 𝐵) → (𝐹‘(𝐹‘𝑥)) = (𝐹‘𝑥))    ⇒   ⊢ (𝜑 → dom (𝐹 ∩ I ) ∈ (Moore‘𝐵))
Theorem	ismrcd2 43292*	Second half of ismrcd1 43291. (Contributed by Stefan O'Rear, 1-Feb-2015.)
⊢ (𝜑 → 𝐵 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐹:𝒫 𝐵⟶𝒫 𝐵)    &   ⊢ ((𝜑 ∧ 𝑥 ⊆ 𝐵) → 𝑥 ⊆ (𝐹‘𝑥))    &   ⊢ ((𝜑 ∧ 𝑥 ⊆ 𝐵 ∧ 𝑦 ⊆ 𝑥) → (𝐹‘𝑦) ⊆ (𝐹‘𝑥))    &   ⊢ ((𝜑 ∧ 𝑥 ⊆ 𝐵) → (𝐹‘(𝐹‘𝑥)) = (𝐹‘𝑥))    ⇒   ⊢ (𝜑 → 𝐹 = (mrCls‘dom (𝐹 ∩ I )))
Theorem	istopclsd 43293*	A closure function which satisfies sscls 23174, clsidm 23185, cls0 23198, and clsun 36701 defines a (unique) topology which it is the closure function on. (Contributed by Stefan O'Rear, 1-Feb-2015.)
⊢ (𝜑 → 𝐵 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐹:𝒫 𝐵⟶𝒫 𝐵)    &   ⊢ ((𝜑 ∧ 𝑥 ⊆ 𝐵) → 𝑥 ⊆ (𝐹‘𝑥))    &   ⊢ ((𝜑 ∧ 𝑥 ⊆ 𝐵) → (𝐹‘(𝐹‘𝑥)) = (𝐹‘𝑥))    &   ⊢ (𝜑 → (𝐹‘∅) = ∅)    &   ⊢ ((𝜑 ∧ 𝑥 ⊆ 𝐵 ∧ 𝑦 ⊆ 𝐵) → (𝐹‘(𝑥 ∪ 𝑦)) = ((𝐹‘𝑥) ∪ (𝐹‘𝑦)))    &   ⊢ 𝐽 = {𝑧 ∈ 𝒫 𝐵 ∣ (𝐹‘(𝐵 ∖ 𝑧)) = (𝐵 ∖ 𝑧)}    ⇒   ⊢ (𝜑 → (𝐽 ∈ (TopOn‘𝐵) ∧ (cls‘𝐽) = 𝐹))
Theorem	ismrc 43294*	A function is a Moore closure operator iff it satisfies mrcssid 17663, mrcss 17662, and mrcidm 17665. (Contributed by Stefan O'Rear, 1-Feb-2015.)
⊢ (𝐹 ∈ (mrCls “ (Moore‘𝐵)) ↔ (𝐵 ∈ V ∧ 𝐹:𝒫 𝐵⟶𝒫 𝐵 ∧ ∀𝑥∀𝑦((𝑥 ⊆ 𝐵 ∧ 𝑦 ⊆ 𝑥) → (𝑥 ⊆ (𝐹‘𝑥) ∧ (𝐹‘𝑦) ⊆ (𝐹‘𝑥) ∧ (𝐹‘(𝐹‘𝑥)) = (𝐹‘𝑥)))))
21.33.5  Algebraic closure systems
Syntax	cnacs 43295	Class of Noetherian closure systems.
class NoeACS
Definition	df-nacs 43296*	Define a closure system of Noetherian type (not standard terminology) as an algebraic system where all closed sets are finitely generated. (Contributed by Stefan O'Rear, 4-Apr-2015.)
⊢ NoeACS = (𝑥 ∈ V ↦ {𝑐 ∈ (ACS‘𝑥) ∣ ∀𝑠 ∈ 𝑐 ∃𝑔 ∈ (𝒫 𝑥 ∩ Fin)𝑠 = ((mrCls‘𝑐)‘𝑔)})
Theorem	isnacs 43297*	Expand definition of Noetherian-type closure system. (Contributed by Stefan O'Rear, 4-Apr-2015.)
⊢ 𝐹 = (mrCls‘𝐶)    ⇒   ⊢ (𝐶 ∈ (NoeACS‘𝑋) ↔ (𝐶 ∈ (ACS‘𝑋) ∧ ∀𝑠 ∈ 𝐶 ∃𝑔 ∈ (𝒫 𝑋 ∩ Fin)𝑠 = (𝐹‘𝑔)))
Theorem	nacsfg 43298*	In a Noetherian-type closure system, all closed sets are finitely generated. (Contributed by Stefan O'Rear, 4-Apr-2015.)
⊢ 𝐹 = (mrCls‘𝐶)    ⇒   ⊢ ((𝐶 ∈ (NoeACS‘𝑋) ∧ 𝑆 ∈ 𝐶) → ∃𝑔 ∈ (𝒫 𝑋 ∩ Fin)𝑆 = (𝐹‘𝑔))
Theorem	isnacs2 43299	Express Noetherian-type closure system with fewer quantifiers. (Contributed by Stefan O'Rear, 4-Apr-2015.)
⊢ 𝐹 = (mrCls‘𝐶)    ⇒   ⊢ (𝐶 ∈ (NoeACS‘𝑋) ↔ (𝐶 ∈ (ACS‘𝑋) ∧ (𝐹 “ (𝒫 𝑋 ∩ Fin)) = 𝐶))
Theorem	mrefg2 43300*	Slight variation on finite generation for closure systems. (Contributed by Stefan O'Rear, 4-Apr-2015.)
⊢ 𝐹 = (mrCls‘𝐶)    ⇒   ⊢ (𝐶 ∈ (Moore‘𝑋) → (∃𝑔 ∈ (𝒫 𝑋 ∩ Fin)𝑆 = (𝐹‘𝑔) ↔ ∃𝑔 ∈ (𝒫 𝑆 ∩ Fin)𝑆 = (𝐹‘𝑔)))