P. 434 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 43301-43400   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	evlselv 43301	Evaluating a selection of variable assignments, then evaluating the rest of the variables, is the same as evaluating with all assignments. (Contributed by SN, 10-Mar-2025.)
⊢ 𝑃 = (𝐼 mPoly 𝑅)    &   ⊢ 𝐾 = (Base‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑃)    &   ⊢ 𝑈 = ((𝐼 ∖ 𝐽) mPoly 𝑅)    &   ⊢ 𝑇 = (𝐽 mPoly 𝑈)    &   ⊢ 𝐿 = (algSc‘𝑈)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑅 ∈ CRing)    &   ⊢ (𝜑 → 𝐽 ⊆ 𝐼)    &   ⊢ (𝜑 → 𝐹 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐴 ∈ (𝐾 ↑m 𝐼))    ⇒   ⊢ (𝜑 → ((((𝐼 ∖ 𝐽) eval 𝑅)‘(((𝐽 eval 𝑈)‘(((𝐼 selectVars 𝑅)‘𝐽)‘𝐹))‘(𝐿 ∘ (𝐴 ↾ 𝐽))))‘(𝐴 ↾ (𝐼 ∖ 𝐽))) = (((𝐼 eval 𝑅)‘𝐹)‘𝐴))
Theorem	fsuppind 43302*	Induction on functions 𝐹:𝐴⟶𝐵 with finite support, or in other words the base set of the free module (see frlmelbas 21887 and frlmplusgval 21895). This theorem is structurally general for polynomial proof usage (see mplelbas 22121 and mpladd 22139). Note that hypothesis 0 is redundant when 𝐼 is nonempty. (Contributed by SN, 18-May-2024.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 0 = (0g‘𝐺)    &   ⊢ + = (+g‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ Grp)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → (𝐼 × { 0 }) ∈ 𝐻)    &   ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 𝐵)) → (𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑎, 𝑏, 0 )) ∈ 𝐻)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐻 ∧ 𝑦 ∈ 𝐻)) → (𝑥 ∘f + 𝑦) ∈ 𝐻)    ⇒   ⊢ ((𝜑 ∧ (𝑋:𝐼⟶𝐵 ∧ 𝑋 finSupp 0 )) → 𝑋 ∈ 𝐻)
Theorem	fsuppssindlem1 43303*	Lemma for fsuppssind 43305. Functions are zero outside of their support. (Contributed by SN, 15-Jul-2024.)
⊢ (𝜑 → 0 ∈ 𝑊)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐹:𝐼⟶𝐵)    &   ⊢ (𝜑 → (𝐹 supp 0 ) ⊆ 𝑆)    ⇒   ⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐼 ↦ if(𝑥 ∈ 𝑆, ((𝐹 ↾ 𝑆)‘𝑥), 0 )))
Theorem	fsuppssindlem2 43304*	Lemma for fsuppssind 43305. Write a function as a union. (Contributed by SN, 15-Jul-2024.)
⊢ (𝜑 → 𝐵 ∈ 𝑊)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑆 ⊆ 𝐼)    ⇒   ⊢ (𝜑 → (𝐹 ∈ {𝑓 ∈ (𝐵 ↑m 𝑆) ∣ (𝑥 ∈ 𝐼 ↦ if(𝑥 ∈ 𝑆, (𝑓‘𝑥), 0 )) ∈ 𝐻} ↔ (𝐹:𝑆⟶𝐵 ∧ (𝐹 ∪ ((𝐼 ∖ 𝑆) × { 0 })) ∈ 𝐻)))
Theorem	fsuppssind 43305*	Induction on functions 𝐹:𝐴⟶𝐵 with finite support (see fsuppind 43302) whose supports are subsets of 𝑆. (Contributed by SN, 15-Jun-2024.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 0 = (0g‘𝐺)    &   ⊢ + = (+g‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ Grp)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑆 ⊆ 𝐼)    &   ⊢ (𝜑 → (𝐼 × { 0 }) ∈ 𝐻)    &   ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝐵)) → (𝑠 ∈ 𝐼 ↦ if(𝑠 = 𝑎, 𝑏, 0 )) ∈ 𝐻)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐻 ∧ 𝑦 ∈ 𝐻)) → (𝑥 ∘f + 𝑦) ∈ 𝐻)    &   ⊢ (𝜑 → 𝑋:𝐼⟶𝐵)    &   ⊢ (𝜑 → 𝑋 finSupp 0 )    &   ⊢ (𝜑 → (𝑋 supp 0 ) ⊆ 𝑆)    ⇒   ⊢ (𝜑 → 𝑋 ∈ 𝐻)
Theorem	mhpind 43306*	The homogeneous polynomials of degree 𝑁 are generated by the terms of degree 𝑁 and addition. (Contributed by SN, 28-Jul-2024.)
⊢ 𝐻 = (𝐼 mHomP 𝑅)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 𝑃 = (𝐼 mPoly 𝑅)    &   ⊢ + = (+g‘𝑃)    &   ⊢ 𝐷 = {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin}    &   ⊢ 𝑆 = {𝑔 ∈ 𝐷 ∣ ((ℂfld ↾s ℕ0) Σg 𝑔) = 𝑁}    &   ⊢ (𝜑 → 𝑅 ∈ Grp)    &   ⊢ (𝜑 → 𝑋 ∈ (𝐻‘𝑁))    &   ⊢ (𝜑 → (𝐷 × { 0 }) ∈ 𝐺)    &   ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝐵)) → (𝑠 ∈ 𝐷 ↦ if(𝑠 = 𝑎, 𝑏, 0 )) ∈ 𝐺)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ ((𝐻‘𝑁) ∩ 𝐺) ∧ 𝑦 ∈ ((𝐻‘𝑁) ∩ 𝐺))) → (𝑥 + 𝑦) ∈ 𝐺)    ⇒   ⊢ (𝜑 → 𝑋 ∈ 𝐺)
Theorem	evlsmhpvvval 43307*	Give a formula for the evaluation of a homogeneous polynomial given assignments from variables to values. The difference between this and evlsvvval 22225 is that 𝑏 ∈ 𝐷 is restricted to 𝑏 ∈ 𝐺, that is, we can evaluate an 𝑁-th degree homogeneous polynomial over just the terms where the sum of all variable degrees is 𝑁. (Contributed by SN, 5-Mar-2025.)
⊢ 𝑄 = ((𝐼 evalSub 𝑆)‘𝑅)    &   ⊢ 𝐻 = (𝐼 mHomP 𝑈)    &   ⊢ 𝑈 = (𝑆 ↾s 𝑅)    &   ⊢ 𝐷 = {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin}    &   ⊢ 𝐺 = {𝑔 ∈ 𝐷 ∣ ((ℂfld ↾s ℕ0) Σg 𝑔) = 𝑁}    &   ⊢ 𝐾 = (Base‘𝑆)    &   ⊢ 𝑀 = (mulGrp‘𝑆)    &   ⊢ ↑ = (.g‘𝑀)    &   ⊢ · = (.r‘𝑆)    &   ⊢ (𝜑 → 𝑆 ∈ CRing)    &   ⊢ (𝜑 → 𝑅 ∈ (SubRing‘𝑆))    &   ⊢ (𝜑 → 𝐹 ∈ (𝐻‘𝑁))    &   ⊢ (𝜑 → 𝐴 ∈ (𝐾 ↑m 𝐼))    ⇒   ⊢ (𝜑 → ((𝑄‘𝐹)‘𝐴) = (𝑆 Σg (𝑏 ∈ 𝐺 ↦ ((𝐹‘𝑏) · (𝑀 Σg (𝑖 ∈ 𝐼 ↦ ((𝑏‘𝑖) ↑ (𝐴‘𝑖))))))))
Theorem	mhphflem 43308*	Lemma for mhphf 43309. Add several multiples of 𝐿 together, in a case where the total amount of multiplies is 𝑁. (Contributed by SN, 30-Jul-2024.)
⊢ 𝐷 = {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin}    &   ⊢ 𝐻 = {𝑔 ∈ 𝐷 ∣ ((ℂfld ↾s ℕ0) Σg 𝑔) = 𝑁}    &   ⊢ 𝐵 = (Base‘𝐺)    &   ⊢ · = (.g‘𝐺)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐺 ∈ Mnd)    &   ⊢ (𝜑 → 𝐿 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    ⇒   ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐻) → (𝐺 Σg (𝑣 ∈ 𝐼 ↦ ((𝑎‘𝑣) · 𝐿))) = (𝑁 · 𝐿))
Theorem	mhphf 43309	A homogeneous polynomial defines a homogeneous function. Equivalently, an algebraic form is a homogeneous function. (An algebraic form is the function corresponding to a homogeneous polynomial, which in this case is the (𝑄‘𝑋) which corresponds to 𝑋). (Contributed by SN, 28-Jul-2024.) (Proof shortened by SN, 8-Mar-2025.)
⊢ 𝑄 = ((𝐼 evalSub 𝑆)‘𝑅)    &   ⊢ 𝐻 = (𝐼 mHomP 𝑈)    &   ⊢ 𝑈 = (𝑆 ↾s 𝑅)    &   ⊢ 𝐾 = (Base‘𝑆)    &   ⊢ · = (.r‘𝑆)    &   ⊢ ↑ = (.g‘(mulGrp‘𝑆))    &   ⊢ (𝜑 → 𝑆 ∈ CRing)    &   ⊢ (𝜑 → 𝑅 ∈ (SubRing‘𝑆))    &   ⊢ (𝜑 → 𝐿 ∈ 𝑅)    &   ⊢ (𝜑 → 𝑋 ∈ (𝐻‘𝑁))    &   ⊢ (𝜑 → 𝐴 ∈ (𝐾 ↑m 𝐼))    ⇒   ⊢ (𝜑 → ((𝑄‘𝑋)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑋)‘𝐴)))
Theorem	mhphf2 43310	A homogeneous polynomial defines a homogeneous function; this is mhphf 43309 with simpler notation in the conclusion in exchange for a complex definition of ∙, which is based on frlmvscafval 21897 but without the finite support restriction (frlmpws 21881, frlmbas 21886) on the assignments 𝐴 from variables to values. TODO?: Polynomials (df-mpl 22042) are defined to have a finite amount of terms (of finite degree). As such, any assignment may be replaced by an assignment with finite support (as only a finite amount of variables matter in a given polynomial, even if the set of variables is infinite). So the finite support restriction can be assumed without loss of generality. (Contributed by SN, 11-Nov-2024.)
⊢ 𝑄 = ((𝐼 evalSub 𝑆)‘𝑅)    &   ⊢ 𝐻 = (𝐼 mHomP 𝑈)    &   ⊢ 𝑈 = (𝑆 ↾s 𝑅)    &   ⊢ 𝐾 = (Base‘𝑆)    &   ⊢ ∙ = ( ·𝑠 ‘((ringLMod‘𝑆) ↑s 𝐼))    &   ⊢ · = (.r‘𝑆)    &   ⊢ ↑ = (.g‘(mulGrp‘𝑆))    &   ⊢ (𝜑 → 𝑆 ∈ CRing)    &   ⊢ (𝜑 → 𝑅 ∈ (SubRing‘𝑆))    &   ⊢ (𝜑 → 𝐿 ∈ 𝑅)    &   ⊢ (𝜑 → 𝑋 ∈ (𝐻‘𝑁))    &   ⊢ (𝜑 → 𝐴 ∈ (𝐾 ↑m 𝐼))    ⇒   ⊢ (𝜑 → ((𝑄‘𝑋)‘(𝐿 ∙ 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑋)‘𝐴)))
Theorem	mhphf3 43311	A homogeneous polynomial defines a homogeneous function; this is mhphf2 43310 with the finite support restriction (frlmpws 21881, frlmbas 21886) on the assignments 𝐴 from variables to values. See comment of mhphf2 43310. (Contributed by SN, 23-Nov-2024.)
⊢ 𝑄 = ((𝐼 evalSub 𝑆)‘𝑅)    &   ⊢ 𝐻 = (𝐼 mHomP 𝑈)    &   ⊢ 𝑈 = (𝑆 ↾s 𝑅)    &   ⊢ 𝐾 = (Base‘𝑆)    &   ⊢ 𝐹 = (𝑆 freeLMod 𝐼)    &   ⊢ 𝑀 = (Base‘𝐹)    &   ⊢ ∙ = ( ·𝑠 ‘𝐹)    &   ⊢ · = (.r‘𝑆)    &   ⊢ ↑ = (.g‘(mulGrp‘𝑆))    &   ⊢ (𝜑 → 𝑆 ∈ CRing)    &   ⊢ (𝜑 → 𝑅 ∈ (SubRing‘𝑆))    &   ⊢ (𝜑 → 𝐿 ∈ 𝑅)    &   ⊢ (𝜑 → 𝑋 ∈ (𝐻‘𝑁))    &   ⊢ (𝜑 → 𝐴 ∈ 𝑀)    ⇒   ⊢ (𝜑 → ((𝑄‘𝑋)‘(𝐿 ∙ 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑋)‘𝐴)))
Theorem	mhphf4 43312	A homogeneous polynomial defines a homogeneous function; this is mhphf3 43311 with evalSub collapsed to eval. (Contributed by SN, 23-Nov-2024.)
⊢ 𝑄 = (𝐼 eval 𝑆)    &   ⊢ 𝐻 = (𝐼 mHomP 𝑆)    &   ⊢ 𝐾 = (Base‘𝑆)    &   ⊢ 𝐹 = (𝑆 freeLMod 𝐼)    &   ⊢ 𝑀 = (Base‘𝐹)    &   ⊢ ∙ = ( ·𝑠 ‘𝐹)    &   ⊢ · = (.r‘𝑆)    &   ⊢ ↑ = (.g‘(mulGrp‘𝑆))    &   ⊢ (𝜑 → 𝑆 ∈ CRing)    &   ⊢ (𝜑 → 𝐿 ∈ 𝐾)    &   ⊢ (𝜑 → 𝑋 ∈ (𝐻‘𝑁))    &   ⊢ (𝜑 → 𝐴 ∈ 𝑀)    ⇒   ⊢ (𝜑 → ((𝑄‘𝑋)‘(𝐿 ∙ 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑋)‘𝐴)))
21.31.7  Projective spaces Looking at a corner in 3D space, one can see three right angles. It is impossible to draw three lines in 2D space such that any two of these lines are perpendicular, but a good enough representation is made by casting lines from the 2D surface. Points along the same cast line are collapsed into one point on the 2D surface. In many cases, the 2D surface is smaller than whatever needs to be represented. If the lines cast were perpendicular to the 2D surface, then only areas as small as the 2D surface could be represented. To fix this, the lines need to get further apart as they go farther from the 2D surface. On the other side of the 2D surface the lines will get closer together and intersect at a point (because it's defined that way). From this perspective, two parallel lines in 3D space will be represented by two lines that seem to intersect at a point "at infinity". Considering all maximal classes of parallel lines on a 2D plane in 3D space, these classes will all appear to intersect at different points at infinity, forming a line at infinity. Therefore the real projective plane can be thought of as the real affine plane together with the line at infinity. The projective plane takes care of some exceptions that may be found in the affine plane. For example, consider the curve that is the zeroes of 𝑦 = 𝑥↑2. Any line connecting the point (0, 1) to the x-axis intersects with the curve twice, except for the vertical line between (0, 1) and (0, 0). In the projective plane, the curve becomes an ellipse and there is no exception. While it may not seem like it, points at infinity and points corresponding to the affine plane are the same type of point. Consider a line going through the origin in 3D (affine) space. Either it intersects the plane 𝑧 = 1 once, or it is entirely within the plane 𝑧 = 0. If it is entirely within the plane 𝑧 = 0, then it corresponds to the point at infinity intersecting all lines on the plane 𝑧 = 1 with the same slope. Else it corresponds to the point in the 2D plane 𝑧 = 1 that it intersects. So there is a bijection between 3D lines through the origin and points on the real projective plane. The concept of projective spaces generalizes the projective plane to any dimension.
Syntax	cprjsp 43313	Extend class notation with the projective space function.
class ℙ𝕣𝕠𝕛
Definition	df-prjsp 43314*	Define the projective space function. In the bijection between 3D lines through the origin and points in the projective plane (see section comment), this is equivalent to making any two 3D points (excluding the origin) equivalent iff one is a multiple of another. This definition does not quite give all the properties needed, since the scalars of a left vector space can be "less dense" than the vectors (for example, making equivalent rational multiples of real numbers). Compare df-lsatoms 39728. (Contributed by BJ and SN, 29-Apr-2023.)
⊢ ℙ𝕣𝕠𝕛 = (𝑣 ∈ LVec ↦ ⦋((Base‘𝑣) ∖ {(0g‘𝑣)}) / 𝑏⦌(𝑏 / {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ 𝑏 ∧ 𝑦 ∈ 𝑏) ∧ ∃𝑙 ∈ (Base‘(Scalar‘𝑣))𝑥 = (𝑙( ·𝑠 ‘𝑣)𝑦))}))
Theorem	prjspval 43315*	Value of the projective space function, which is also known as the projectivization of 𝑉. (Contributed by Steven Nguyen, 29-Apr-2023.)
⊢ 𝐵 = ((Base‘𝑉) ∖ {(0g‘𝑉)})    &   ⊢ · = ( ·𝑠 ‘𝑉)    &   ⊢ 𝑆 = (Scalar‘𝑉)    &   ⊢ 𝐾 = (Base‘𝑆)    ⇒   ⊢ (𝑉 ∈ LVec → (ℙ𝕣𝕠𝕛‘𝑉) = (𝐵 / {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ ∃𝑙 ∈ 𝐾 𝑥 = (𝑙 · 𝑦))}))
Theorem	prjsprel 43316*	Utility theorem regarding the relation used in ℙ𝕣𝕠𝕛. (Contributed by Steven Nguyen, 29-Apr-2023.)
⊢ ∼ = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ ∃𝑙 ∈ 𝐾 𝑥 = (𝑙 · 𝑦))}    ⇒   ⊢ (𝑋 ∼ 𝑌 ↔ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ ∃𝑚 ∈ 𝐾 𝑋 = (𝑚 · 𝑌)))
Theorem	prjspertr 43317*	The relation in ℙ𝕣𝕠𝕛 is transitive. (Contributed by Steven Nguyen, 1-May-2023.)
⊢ ∼ = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ ∃𝑙 ∈ 𝐾 𝑥 = (𝑙 · 𝑦))}    &   ⊢ 𝐵 = ((Base‘𝑉) ∖ {(0g‘𝑉)})    &   ⊢ 𝑆 = (Scalar‘𝑉)    &   ⊢ · = ( ·𝑠 ‘𝑉)    &   ⊢ 𝐾 = (Base‘𝑆)    ⇒   ⊢ ((𝑉 ∈ LMod ∧ (𝑋 ∼ 𝑌 ∧ 𝑌 ∼ 𝑍)) → 𝑋 ∼ 𝑍)
Theorem	prjsperref 43318*	The relation in ℙ𝕣𝕠𝕛 is reflexive. (Contributed by Steven Nguyen, 30-Apr-2023.)
⊢ ∼ = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ ∃𝑙 ∈ 𝐾 𝑥 = (𝑙 · 𝑦))}    &   ⊢ 𝐵 = ((Base‘𝑉) ∖ {(0g‘𝑉)})    &   ⊢ 𝑆 = (Scalar‘𝑉)    &   ⊢ · = ( ·𝑠 ‘𝑉)    &   ⊢ 𝐾 = (Base‘𝑆)    ⇒   ⊢ (𝑉 ∈ LMod → (𝑋 ∈ 𝐵 ↔ 𝑋 ∼ 𝑋))
Theorem	prjspersym 43319*	The relation in ℙ𝕣𝕠𝕛 is symmetric. (Contributed by Steven Nguyen, 1-May-2023.)
⊢ ∼ = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ ∃𝑙 ∈ 𝐾 𝑥 = (𝑙 · 𝑦))}    &   ⊢ 𝐵 = ((Base‘𝑉) ∖ {(0g‘𝑉)})    &   ⊢ 𝑆 = (Scalar‘𝑉)    &   ⊢ · = ( ·𝑠 ‘𝑉)    &   ⊢ 𝐾 = (Base‘𝑆)    ⇒   ⊢ ((𝑉 ∈ LVec ∧ 𝑋 ∼ 𝑌) → 𝑌 ∼ 𝑋)
Theorem	prjsper 43320*	The relation used to define ℙ𝕣𝕠𝕛 is an equivalence relation. (Contributed by Steven Nguyen, 1-May-2023.)
⊢ ∼ = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ ∃𝑙 ∈ 𝐾 𝑥 = (𝑙 · 𝑦))}    &   ⊢ 𝐵 = ((Base‘𝑉) ∖ {(0g‘𝑉)})    &   ⊢ 𝑆 = (Scalar‘𝑉)    &   ⊢ · = ( ·𝑠 ‘𝑉)    &   ⊢ 𝐾 = (Base‘𝑆)    ⇒   ⊢ (𝑉 ∈ LVec → ∼ Er 𝐵)
Theorem	prjspreln0 43321*	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 43322*	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 43323*	Two vectors are equivalent iff their spans are equal. (Contributed by Steven Nguyen, 31-May-2023.)
⊢ ∼ = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ ∃𝑙 ∈ 𝐾 𝑥 = (𝑙 · 𝑦))}    &   ⊢ 𝐵 = ((Base‘𝑉) ∖ {(0g‘𝑉)})    &   ⊢ 𝑆 = (Scalar‘𝑉)    &   ⊢ · = ( ·𝑠 ‘𝑉)    &   ⊢ 𝐾 = (Base‘𝑆)    &   ⊢ 𝑁 = (LSpan‘𝑉)    ⇒   ⊢ ((𝑉 ∈ LVec ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → (𝑋 ∼ 𝑌 ↔ (𝑁‘{𝑋}) = (𝑁‘{𝑌})))
Theorem	prjspeclsp 43324*	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 43325*	Alternate definition of projective space. (Contributed by Steven Nguyen, 7-Jun-2023.)
⊢ 0 = (0g‘𝑉)    &   ⊢ 𝐵 = ((Base‘𝑉) ∖ { 0 })    &   ⊢ 𝑁 = (LSpan‘𝑉)    ⇒   ⊢ (𝑉 ∈ LVec → (ℙ𝕣𝕠𝕛‘𝑉) = ∪ 𝑧 ∈ 𝐵 {((𝑁‘{𝑧}) ∖ { 0 })})
Syntax	cprjspn 43326	Extend class notation with the n-dimensional projective space function.
class ℙ𝕣𝕠𝕛n
Definition	df-prjspn 43327*	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 25526. 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 43328	Value of the n-dimensional projective space function. (Contributed by Steven Nguyen, 1-May-2023.)
⊢ ((𝑁 ∈ ℕ0 ∧ 𝐾 ∈ DivRing) → (𝑁ℙ𝕣𝕠𝕛n𝐾) = (ℙ𝕣𝕠𝕛‘(𝐾 freeLMod (0...𝑁))))
Theorem	prjspnerlem 43329*	A lemma showing that the equivalence relation used in prjspnval2 43330 and the equivalence relation used in prjspval 43315 are equal, but only with the antecedent 𝐾 ∈ DivRing. (Contributed by SN, 15-Jul-2023.)
⊢ ∼ = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ ∃𝑙 ∈ 𝑆 𝑥 = (𝑙 · 𝑦))}    &   ⊢ 𝑊 = (𝐾 freeLMod (0...𝑁))    &   ⊢ 𝐵 = ((Base‘𝑊) ∖ {(0g‘𝑊)})    &   ⊢ 𝑆 = (Base‘𝐾)    &   ⊢ · = ( ·𝑠 ‘𝑊)    ⇒   ⊢ (𝐾 ∈ DivRing → ∼ = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ ∃𝑙 ∈ (Base‘(Scalar‘𝑊))𝑥 = (𝑙 · 𝑦))})
Theorem	prjspnval2 43330*	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 43331*	The relation used to define ℙ𝕣𝕠𝕛 (and indirectly ℙ𝕣𝕠𝕛n through df-prjspn 43327) is an equivalence relation. This is a lemma that converts the equivalence relation used in results like prjspertr 43317 and prjspersym 43319 (see prjspnerlem 43329). Several theorems are covered in one thanks to the theorems around df-er 8695. (Contributed by SN, 14-Aug-2023.)
⊢ ∼ = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ ∃𝑙 ∈ 𝑆 𝑥 = (𝑙 · 𝑦))}    &   ⊢ 𝑊 = (𝐾 freeLMod (0...𝑁))    &   ⊢ 𝐵 = ((Base‘𝑊) ∖ {(0g‘𝑊)})    &   ⊢ 𝑆 = (Base‘𝐾)    &   ⊢ · = ( ·𝑠 ‘𝑊)    &   ⊢ (𝜑 → 𝐾 ∈ DivRing)    ⇒   ⊢ (𝜑 → ∼ Er 𝐵)
Theorem	prjspnvs 43332*	A nonzero multiple of a vector is equivalent to the vector. This converts the equivalence relation used in prjspvs 43322 (see prjspnerlem 43329). (Contributed by SN, 8-Aug-2024.)
⊢ ∼ = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ ∃𝑙 ∈ 𝑆 𝑥 = (𝑙 · 𝑦))}    &   ⊢ 𝑊 = (𝐾 freeLMod (0...𝑁))    &   ⊢ 𝐵 = ((Base‘𝑊) ∖ {(0g‘𝑊)})    &   ⊢ 𝑆 = (Base‘𝐾)    &   ⊢ · = ( ·𝑠 ‘𝑊)    &   ⊢ 0 = (0g‘𝐾)    &   ⊢ (𝜑 → 𝐾 ∈ DivRing)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑆)    &   ⊢ (𝜑 → 𝐶 ≠ 0 )    ⇒   ⊢ (𝜑 → (𝐶 · 𝑋) ∼ 𝑋)
Theorem	prjspnssbas 43333	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 43334	A projective point is nonempty. (Contributed by SN, 17-Jan-2025.)
⊢ 𝑃 = (𝑁ℙ𝕣𝕠𝕛n𝐾)    &   ⊢ 𝑊 = (𝐾 freeLMod (0...𝑁))    &   ⊢ 𝐵 = ((Base‘𝑊) ∖ {(0g‘𝑊)})    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    &   ⊢ (𝜑 → 𝐾 ∈ DivRing)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑃)    ⇒   ⊢ (𝜑 → 𝐴 ≠ ∅)
Theorem	0prjspnlem 43335	Lemma for 0prjspn 43340. 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 43336*	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 43337*	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 43338*	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 43339*	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 43340	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 43341	Extend class notation with the projective curve function.
class ℙ𝕣𝕠𝕛Crv
Definition	df-prjcrv 43342*	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 43312 and prjspvs 43322). (Contributed by SN, 23-Nov-2024.)
⊢ ℙ𝕣𝕠𝕛Crv = (𝑛 ∈ ℕ0, 𝑘 ∈ Field ↦ (𝑓 ∈ ∪ ran ((0...𝑛) mHomP 𝑘) ↦ {𝑝 ∈ (𝑛ℙ𝕣𝕠𝕛n𝑘) ∣ ((((0...𝑛) eval 𝑘)‘𝑓) “ 𝑝) = {(0g‘𝑘)}}))
Theorem	prjcrvfval 43343*	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 43344*	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 43345	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.31.8  Basic reductions for Fermat's Last Theorem
Theorem	dffltz 43346*	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 43347	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 43348	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 43349	A counterexample for FLT does not exist for 𝑁 = 0. (Contributed by SN, 20-Aug-2024.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    &   ⊢ (𝜑 → ((𝐴↑𝑁) + (𝐵↑𝑁)) = (𝐶↑𝑁))    ⇒   ⊢ (𝜑 → 𝑁 ∈ ℕ)
Theorem	fltdvdsabdvdsc 43350	Any factor of both 𝐴 and 𝐵 also divides 𝐶. This establishes the validity of fltabcoprmex 43351. (Contributed by SN, 21-Aug-2024.)
⊢ (𝜑 → 𝐴 ∈ ℕ)    &   ⊢ (𝜑 → 𝐵 ∈ ℕ)    &   ⊢ (𝜑 → 𝐶 ∈ ℕ)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → ((𝐴↑𝑁) + (𝐵↑𝑁)) = (𝐶↑𝑁))    ⇒   ⊢ (𝜑 → (𝐴 gcd 𝐵) ∥ 𝐶)
Theorem	fltabcoprmex 43351	A counterexample to FLT implies a counterexample to FLT with 𝐴, 𝐵 (assigned to 𝐴 / (𝐴 gcd 𝐵) and 𝐵 / (𝐴 gcd 𝐵)) coprime (by divgcdcoprm0 16724). (Contributed by SN, 20-Aug-2024.)
⊢ (𝜑 → 𝐴 ∈ ℕ)    &   ⊢ (𝜑 → 𝐵 ∈ ℕ)    &   ⊢ (𝜑 → 𝐶 ∈ ℕ)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    &   ⊢ (𝜑 → ((𝐴↑𝑁) + (𝐵↑𝑁)) = (𝐶↑𝑁))    ⇒   ⊢ (𝜑 → (((𝐴 / (𝐴 gcd 𝐵))↑𝑁) + ((𝐵 / (𝐴 gcd 𝐵))↑𝑁)) = ((𝐶 / (𝐴 gcd 𝐵))↑𝑁))
Theorem	fltaccoprm 43352	A counterexample to FLT with 𝐴, 𝐵 coprime also has 𝐴, 𝐶 coprime. (Contributed by SN, 20-Aug-2024.)
⊢ (𝜑 → 𝐴 ∈ ℕ)    &   ⊢ (𝜑 → 𝐵 ∈ ℕ)    &   ⊢ (𝜑 → 𝐶 ∈ ℕ)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    &   ⊢ (𝜑 → ((𝐴↑𝑁) + (𝐵↑𝑁)) = (𝐶↑𝑁))    &   ⊢ (𝜑 → (𝐴 gcd 𝐵) = 1)    ⇒   ⊢ (𝜑 → (𝐴 gcd 𝐶) = 1)
Theorem	fltbccoprm 43353	A counterexample to FLT with 𝐴, 𝐵 coprime also has 𝐵, 𝐶 coprime. Proven from fltaccoprm 43352 using commutativity of addition. (Contributed by SN, 20-Aug-2024.)
⊢ (𝜑 → 𝐴 ∈ ℕ)    &   ⊢ (𝜑 → 𝐵 ∈ ℕ)    &   ⊢ (𝜑 → 𝐶 ∈ ℕ)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    &   ⊢ (𝜑 → ((𝐴↑𝑁) + (𝐵↑𝑁)) = (𝐶↑𝑁))    &   ⊢ (𝜑 → (𝐴 gcd 𝐵) = 1)    ⇒   ⊢ (𝜑 → (𝐵 gcd 𝐶) = 1)
Theorem	fltabcoprm 43354	A counterexample to FLT with 𝐴, 𝐶 coprime also has 𝐴, 𝐵 coprime. Converse of fltaccoprm 43352. (Contributed by SN, 22-Aug-2024.)
⊢ (𝜑 → 𝐴 ∈ ℕ)    &   ⊢ (𝜑 → 𝐵 ∈ ℕ)    &   ⊢ (𝜑 → 𝐶 ∈ ℕ)    &   ⊢ (𝜑 → (𝐴 gcd 𝐶) = 1)    &   ⊢ (𝜑 → ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2))    ⇒   ⊢ (𝜑 → (𝐴 gcd 𝐵) = 1)
Theorem	infdesc 43355*	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 43356	If a counterexample to FLT exists, its addends are not equal. (Contributed by SN, 1-Jun-2023.)
⊢ (𝜑 → 𝐴 ∈ ℕ)    &   ⊢ (𝜑 → 𝐵 ∈ ℕ)    &   ⊢ (𝜑 → 𝐶 ∈ ℕ)    &   ⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘2))    &   ⊢ (𝜑 → ((𝐴↑𝑁) + (𝐵↑𝑁)) = (𝐶↑𝑁))    ⇒   ⊢ (𝜑 → 𝐴 ≠ 𝐵)
Theorem	flt4lem 43357	Raising a number to the fourth power is equivalent to squaring it twice. (Contributed by SN, 21-Aug-2024.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    ⇒   ⊢ (𝜑 → (𝐴↑4) = ((𝐴↑2)↑2))
Theorem	flt4lem1 43358	Satisfy the antecedent used in several pythagtrip 16895 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 43359	If 𝐴 is even, 𝐵 is odd. (Contributed by SN, 22-Aug-2024.)
⊢ (𝜑 → 𝐴 ∈ ℕ)    &   ⊢ (𝜑 → 𝐵 ∈ ℕ)    &   ⊢ (𝜑 → 𝐶 ∈ ℕ)    &   ⊢ (𝜑 → 2 ∥ 𝐴)    &   ⊢ (𝜑 → (𝐴 gcd 𝐶) = 1)    &   ⊢ (𝜑 → ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2))    ⇒   ⊢ (𝜑 → ¬ 2 ∥ 𝐵)
Theorem	flt4lem3 43360	Equivalent to pythagtriplem4 16880. Show that 𝐶 + 𝐴 and 𝐶 − 𝐴 are coprime. (Contributed by SN, 22-Aug-2024.)
⊢ (𝜑 → 𝐴 ∈ ℕ)    &   ⊢ (𝜑 → 𝐵 ∈ ℕ)    &   ⊢ (𝜑 → 𝐶 ∈ ℕ)    &   ⊢ (𝜑 → 2 ∥ 𝐴)    &   ⊢ (𝜑 → (𝐴 gcd 𝐶) = 1)    &   ⊢ (𝜑 → ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2))    ⇒   ⊢ (𝜑 → ((𝐶 + 𝐴) gcd (𝐶 − 𝐴)) = 1)
Theorem	flt4lem4 43361	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 43362	In the context of the lemmas of pythagtrip 16895, 𝑀 and 𝑁 are coprime. (Contributed by SN, 23-Aug-2024.)
⊢ 𝑀 = (((√‘(𝐶 + 𝐵)) + (√‘(𝐶 − 𝐵))) / 2)    &   ⊢ 𝑁 = (((√‘(𝐶 + 𝐵)) − (√‘(𝐶 − 𝐵))) / 2)    ⇒   ⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2) ∧ ((𝐴 gcd 𝐵) = 1 ∧ ¬ 2 ∥ 𝐴)) → (𝑀 gcd 𝑁) = 1)
Theorem	flt4lem5elem 43363	Version of fltaccoprm 43352 and fltbccoprm 43353 where 𝑀 is not squared. This can be proved in general for any polynomial in three variables: using prmdvdsncoprmbd 16787, dvds2addd 16351, and prmdvdsexp 16775, 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 43364	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 43365	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 43366	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 43367	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 43368	Satisfy the hypotheses of flt4lem4 43361. (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 43369	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 43370	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 43371*	Convert flt4lem5f 43369 into a convenient form for nna4b4nsq 43372. 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 43372	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 43373	(𝐶↑𝑁) is the largest term and therefore 𝐵 < 𝐶. (Contributed by Steven Nguyen, 22-Aug-2023.)
⊢ (𝜑 → 𝐴 ∈ ℕ)    &   ⊢ (𝜑 → 𝐵 ∈ ℕ)    &   ⊢ (𝜑 → 𝐶 ∈ ℕ)    &   ⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘3))    &   ⊢ (𝜑 → ((𝐴↑𝑁) + (𝐵↑𝑁)) = (𝐶↑𝑁))    ⇒   ⊢ (𝜑 → 𝐵 < 𝐶)
Theorem	fltnltalem 43374	Lemma for fltnlta 43375. A lower bound for 𝐴 based on pwdif 15924. (Contributed by Steven Nguyen, 22-Aug-2023.)
⊢ (𝜑 → 𝐴 ∈ ℕ)    &   ⊢ (𝜑 → 𝐵 ∈ ℕ)    &   ⊢ (𝜑 → 𝐶 ∈ ℕ)    &   ⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘3))    &   ⊢ (𝜑 → ((𝐴↑𝑁) + (𝐵↑𝑁)) = (𝐶↑𝑁))    ⇒   ⊢ (𝜑 → ((𝐶 − 𝐵) · ((𝐶↑(𝑁 − 1)) + ((𝑁 − 1) · (𝐵↑(𝑁 − 1))))) < (𝐴↑𝑁))
Theorem	fltnlta 43375	In a Fermat counterexample, the exponent 𝑁 is less than all three numbers (𝐴, 𝐵, and 𝐶). Note that 𝐴 < 𝐵 (hypothesis) and 𝐵 < 𝐶 (fltltc 43373). See https://youtu.be/EymVXkPWxyc 43373 for an outline. (Contributed by SN, 24-Aug-2023.)
⊢ (𝜑 → 𝐴 ∈ ℕ)    &   ⊢ (𝜑 → 𝐵 ∈ ℕ)    &   ⊢ (𝜑 → 𝐶 ∈ ℕ)    &   ⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘3))    &   ⊢ (𝜑 → ((𝐴↑𝑁) + (𝐵↑𝑁)) = (𝐶↑𝑁))    &   ⊢ (𝜑 → 𝐴 < 𝐵)    ⇒   ⊢ (𝜑 → 𝑁 < 𝐴)
21.31.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 43376	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 43377	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 30729. 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 43378	Alias for 19.26 1900 for easier lookup. (Contributed by SN, 12-Aug-2025.) (New usage is discouraged.)
⊢ (∀𝑥(𝜑 ∧ 𝜓) ↔ (∀𝑥𝜑 ∧ ∀𝑥𝜓))
Theorem	exor 43379	Alias for 19.43 1912 for easier lookup. (Contributed by SN, 5-Jul-2025.) (New usage is discouraged.)
⊢ (∃𝑥(𝜑 ∨ 𝜓) ↔ (∃𝑥𝜑 ∨ ∃𝑥𝜓))
Theorem	rexor 43380	Alias for r19.43 3133 for easier lookup. (Contributed by SN, 5-Jul-2025.) (New usage is discouraged.)
⊢ (∃𝑥 ∈ 𝐴 (𝜑 ∨ 𝜓) ↔ (∃𝑥 ∈ 𝐴 𝜑 ∨ ∃𝑥 ∈ 𝐴 𝜓))
Theorem	ruvALT 43381	Alternate proof of ruv 9571 with one fewer syntax step thanks to using elirrv 9560 instead of elirr 9563. 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 30729. (Contributed by SN, 1-Sep-2024.) (New usage is discouraged.) (Proof modification is discouraged.)
⊢ {𝑥 ∣ 𝑥 ∉ 𝑥} = V
Theorem	sn-wcdeq 43382	Alternative to wcdeq 3727 and df-cdeq 3728. This flattens the syntax representation ( wi ( weq vx vy ) wph ) to ( sn-wcdeq vx vy wph ), illustrating the comment of df-cdeq 3728. (Contributed by SN, 26-Sep-2024.) (New usage is discouraged.)
wff (𝑥 = 𝑦 → 𝜑)
Theorem	sq45 43383	45 squared is 2025. (Contributed by SN, 30-Mar-2025.)
⊢ (;45↑2) = ;;;2025
Theorem	sum9cubes 43384	The sum of the first nine perfect cubes is 2025. (Contributed by SN, 30-Mar-2025.)
⊢ Σ𝑘 ∈ (1...9)(𝑘↑3) = ;;;2025
Theorem	sn-isghm 43385*	Longer proof of isghm 19287, unsuccessfully attempting to simplify isghm 19287 using elovmpo 7657 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 43386	An abuse of notation. (Contributed by Prof. Loof Lirpa, 1-Apr-2025.) (New usage is discouraged.) (Proof modification is discouraged.)
⊢ {⟨“𝐴𝑝𝑟𝑖𝑙”⟩, ⟨“𝑓𝑜𝑜𝑙𝑠!”⟩} ∈ V
21.31.9.1  Standard replacements of ax-10 , ax-11 , ax-12 It is known that ax-10 2176, ax-11 2192, and ax-12 2213 are logically redundant in a weak sense. Practically, they can be replaced with hbn1w 2078, alcomimw 2073, and ax12wlem 2167 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 6546 and df-mpt 5194, two very common constructions. But doing a standard replacement of ax-10 2176, ax-11 2192, and ax-12 2213 takes unsatisfyingly long. Usually, if another approach is found, that approach is shorter and better.
Theorem	nfa1w 43387*	Replace ax-10 2176 in nfa1 2186 with a substitution hypothesis. (Contributed by SN, 2-Sep-2025.)
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ Ⅎ𝑥∀𝑥𝜑
Theorem	eu6w 43388*	Replace ax-10 2176, ax-12 2213 in eu6 2602 with substitution hypotheses. (Contributed by SN, 27-May-2025.)
⊢ (𝑥 = 𝑧 → (𝜑 ↔ 𝜓))    &   ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜃))    ⇒   ⊢ (∃!𝑥𝜑 ↔ ∃𝑦∀𝑥(𝜑 ↔ 𝑥 = 𝑦))
Theorem	abbibw 43389*	Replace ax-10 2176, ax-11 2192, ax-12 2213 in abbib 2832 with substitution hypotheses. (Contributed by SN, 27-May-2025.)
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜃))    &   ⊢ (𝑥 = 𝑦 → (𝜓 ↔ 𝜒))    ⇒   ⊢ ({𝑥 ∣ 𝜑} = {𝑥 ∣ 𝜓} ↔ ∀𝑥(𝜑 ↔ 𝜓))
Theorem	absnw 43390*	Replace ax-10 2176, ax-11 2192, ax-12 2213 in absn 4610 with a substitution hypothesis. (Contributed by SN, 27-May-2025.)
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ ({𝑥 ∣ 𝜑} = {𝑌} ↔ ∀𝑥(𝜑 ↔ 𝑥 = 𝑌))
Theorem	euabsn2w 43391*	Replace ax-10 2176, ax-11 2192, ax-12 2213 in euabsn2 4692 with substitution hypotheses. (Contributed by SN, 27-May-2025.)
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    &   ⊢ (𝑥 = 𝑧 → (𝜑 ↔ 𝜃))    ⇒   ⊢ (∃!𝑥𝜑 ↔ ∃𝑦{𝑥 ∣ 𝜑} = {𝑦})
21.32  Mathbox for Igor Ieskov
Theorem	cu3addd 43392	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 43393	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 43394*	An extended version of rexlimdvv 3221 to include three set variables. (Contributed by Igor Ieskov, 21-Jan-2024.)
⊢ (𝜑 → ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐶) → (𝜓 → 𝜒)))    ⇒   ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 ∃𝑧 ∈ 𝐶 𝜓 → 𝜒))
Theorem	3cubeslem1 43395	Lemma for 3cubes 43401. (Contributed by Igor Ieskov, 22-Jan-2024.)
⊢ (𝜑 → 𝐴 ∈ ℚ)    ⇒   ⊢ (𝜑 → 0 < (((𝐴 + 1)↑2) − 𝐴))
Theorem	3cubeslem2 43396	Lemma for 3cubes 43401. Used to show that the denominators in 3cubeslem4 43400 are nonzero. (Contributed by Igor Ieskov, 22-Jan-2024.)
⊢ (𝜑 → 𝐴 ∈ ℚ)    ⇒   ⊢ (𝜑 → ¬ ((((3↑3) · (𝐴↑2)) + ((3↑2) · 𝐴)) + 3) = 0)
Theorem	3cubeslem3l 43397	Lemma for 3cubes 43401. (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 43398	Lemma for 3cubes 43401. (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 43399	Lemma for 3cubes 43401. (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 43400	Lemma for 3cubes 43401. 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)))