P. 410 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 40901-41000   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	sn-addlt0d 40901	The sum of negative numbers is negative. (Contributed by SN, 25-Jan-2025.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 < 0)    &   ⊢ (𝜑 → 𝐵 < 0)    ⇒   ⊢ (𝜑 → (𝐴 + 𝐵) < 0)
Theorem	sn-addgt0d 40902	The sum of positive numbers is positive. Proof of addgt0d 11730 without ax-mulcom 11115. (Contributed by SN, 25-Jan-2025.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 0 < 𝐴)    &   ⊢ (𝜑 → 0 < 𝐵)    ⇒   ⊢ (𝜑 → 0 < (𝐴 + 𝐵))
Theorem	sn-nnne0 40903	nnne0 12187 without ax-mulcom 11115. (Contributed by SN, 25-Jan-2025.)
⊢ (𝐴 ∈ ℕ → 𝐴 ≠ 0)
Theorem	reelznn0nn 40904	elznn0nn 12513 restated using df-resub 40821. (Contributed by SN, 25-Jan-2025.)
⊢ (𝑁 ∈ ℤ ↔ (𝑁 ∈ ℕ0 ∨ (𝑁 ∈ ℝ ∧ (0 −ℝ 𝑁) ∈ ℕ)))
Theorem	nn0addcom 40905	Addition is commutative for nonnegative integers. Proven without ax-mulcom 11115. (Contributed by SN, 1-Feb-2025.)
⊢ ((𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ0) → (𝐴 + 𝐵) = (𝐵 + 𝐴))
Theorem	zaddcomlem 40906	Lemma for zaddcom 40907. (Contributed by SN, 1-Feb-2025.)
⊢ (((𝐴 ∈ ℝ ∧ (0 −ℝ 𝐴) ∈ ℕ) ∧ 𝐵 ∈ ℕ0) → (𝐴 + 𝐵) = (𝐵 + 𝐴))
Theorem	zaddcom 40907	Addition is commutative for integers. Proven without ax-mulcom 11115. (Contributed by SN, 25-Jan-2025.)
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (𝐴 + 𝐵) = (𝐵 + 𝐴))
Theorem	renegmulnnass 40908	Move multiplication by a natural number inside and outside negation. (Contributed by SN, 25-Jan-2025.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    ⇒   ⊢ (𝜑 → ((0 −ℝ 𝐴) · 𝑁) = (0 −ℝ (𝐴 · 𝑁)))
Theorem	nn0mulcom 40909	Multiplication is commutative for nonnegative integers. Proven without ax-mulcom 11115. (Contributed by SN, 25-Jan-2025.)
⊢ ((𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ0) → (𝐴 · 𝐵) = (𝐵 · 𝐴))
Theorem	zmulcomlem 40910	Lemma for zmulcom 40911. (Contributed by SN, 25-Jan-2025.)
⊢ (((𝐴 ∈ ℝ ∧ (0 −ℝ 𝐴) ∈ ℕ) ∧ 𝐵 ∈ ℕ0) → (𝐴 · 𝐵) = (𝐵 · 𝐴))
Theorem	zmulcom 40911	Multiplication is commutative for integers. Proven without ax-mulcom 11115. From this result and grpcominv1 40687, we can show that rationals commute under multiplication without using ax-mulcom 11115. (Contributed by SN, 25-Jan-2025.)
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (𝐴 · 𝐵) = (𝐵 · 𝐴))
Theorem	mulgt0con1dlem 40912	Lemma for mulgt0con1d 40913. Contraposes a positive deduction to a negative deduction. (Contributed by SN, 26-Jun-2024.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → (0 < 𝐴 → 0 < 𝐵))    &   ⊢ (𝜑 → (𝐴 = 0 → 𝐵 = 0))    ⇒   ⊢ (𝜑 → (𝐵 < 0 → 𝐴 < 0))
Theorem	mulgt0con1d 40913	Counterpart to mulgt0con2d 40914, though not a lemma of anything. This is the first use of ax-pre-mulgt0 11128. (Contributed by SN, 26-Jun-2024.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 0 < 𝐵)    &   ⊢ (𝜑 → (𝐴 · 𝐵) < 0)    ⇒   ⊢ (𝜑 → 𝐴 < 0)
Theorem	mulgt0con2d 40914	Lemma for mulgt0b2d 40915 and contrapositive of mulgt0 11232. (Contributed by SN, 26-Jun-2024.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 0 < 𝐴)    &   ⊢ (𝜑 → (𝐴 · 𝐵) < 0)    ⇒   ⊢ (𝜑 → 𝐵 < 0)
Theorem	mulgt0b2d 40915	Biconditional, deductive form of mulgt0 11232. The second factor is positive iff the product is. Note that the commuted form cannot be proven since resubdi 40851 does not have a commuted form. (Contributed by SN, 26-Jun-2024.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 0 < 𝐴)    ⇒   ⊢ (𝜑 → (0 < 𝐵 ↔ 0 < (𝐴 · 𝐵)))
Theorem	sn-ltmul2d 40916	ltmul2d 12999 without ax-mulcom 11115. (Contributed by SN, 26-Jun-2024.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ)    &   ⊢ (𝜑 → 0 < 𝐶)    ⇒   ⊢ (𝜑 → ((𝐶 · 𝐴) < (𝐶 · 𝐵) ↔ 𝐴 < 𝐵))
Theorem	sn-0lt1 40917	0lt1 11677 without ax-mulcom 11115. (Contributed by SN, 13-Feb-2024.)
⊢ 0 < 1
Theorem	sn-ltp1 40918	ltp1 11995 without ax-mulcom 11115. (Contributed by SN, 13-Feb-2024.)
⊢ (𝐴 ∈ ℝ → 𝐴 < (𝐴 + 1))
Theorem	reneg1lt0 40919	Lemma for sn-inelr 40920. (Contributed by SN, 1-Jun-2024.)
⊢ (0 −ℝ 1) < 0
Theorem	sn-inelr 40920	inelr 12143 without ax-mulcom 11115. (Contributed by SN, 1-Jun-2024.)
⊢ ¬ i ∈ ℝ
Theorem	itrere 40921	i times a real is real iff the real is zero. (Contributed by SN, 27-Jun-2024.)
⊢ (𝑅 ∈ ℝ → ((i · 𝑅) ∈ ℝ ↔ 𝑅 = 0))
Theorem	retire 40922	Commuted version of itrere 40921. (Contributed by SN, 27-Jun-2024.)
⊢ (𝑅 ∈ ℝ → ((𝑅 · i) ∈ ℝ ↔ 𝑅 = 0))
Theorem	cnreeu 40923	The reals in the expression given by cnre 11152 uniquely define a complex number. (Contributed by SN, 27-Jun-2024.)
⊢ (𝜑 → 𝑟 ∈ ℝ)    &   ⊢ (𝜑 → 𝑠 ∈ ℝ)    &   ⊢ (𝜑 → 𝑡 ∈ ℝ)    &   ⊢ (𝜑 → 𝑢 ∈ ℝ)    ⇒   ⊢ (𝜑 → ((𝑟 + (i · 𝑠)) = (𝑡 + (i · 𝑢)) ↔ (𝑟 = 𝑡 ∧ 𝑠 = 𝑢)))
Theorem	sn-sup2 40924*	sup2 12111 with exactly the same proof except for using sn-ltp1 40918 instead of ltp1 11995, saving ax-mulcom 11115. (Contributed by SN, 26-Jun-2024.)
⊢ ((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 (𝑦 < 𝑥 ∨ 𝑦 = 𝑥)) → ∃𝑥 ∈ ℝ (∀𝑦 ∈ 𝐴 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧 ∈ 𝐴 𝑦 < 𝑧)))
21.26.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 40925	Extend class notation with the projective space function.
class ℙ𝕣𝕠𝕛
Definition	df-prjsp 40926*	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, equivocating rational multiples of real numbers). Compare df-lsatoms 37438. (Contributed by BJ and SN, 29-Apr-2023.)
⊢ ℙ𝕣𝕠𝕛 = (𝑣 ∈ LVec ↦ ⦋((Base‘𝑣) ∖ {(0g‘𝑣)}) / 𝑏⦌(𝑏 / {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ 𝑏 ∧ 𝑦 ∈ 𝑏) ∧ ∃𝑙 ∈ (Base‘(Scalar‘𝑣))𝑥 = (𝑙( ·𝑠 ‘𝑣)𝑦))}))
Theorem	prjspval 40927*	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 40928*	Utility theorem regarding the relation used in ℙ𝕣𝕠𝕛. (Contributed by Steven Nguyen, 29-Apr-2023.)
⊢ ∼ = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ ∃𝑙 ∈ 𝐾 𝑥 = (𝑙 · 𝑦))}    ⇒   ⊢ (𝑋 ∼ 𝑌 ↔ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ ∃𝑚 ∈ 𝐾 𝑋 = (𝑚 · 𝑌)))
Theorem	prjspertr 40929*	The relation in ℙ𝕣𝕠𝕛 is transitive. (Contributed by Steven Nguyen, 1-May-2023.)
⊢ ∼ = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ ∃𝑙 ∈ 𝐾 𝑥 = (𝑙 · 𝑦))}    &   ⊢ 𝐵 = ((Base‘𝑉) ∖ {(0g‘𝑉)})    &   ⊢ 𝑆 = (Scalar‘𝑉)    &   ⊢ · = ( ·𝑠 ‘𝑉)    &   ⊢ 𝐾 = (Base‘𝑆)    ⇒   ⊢ ((𝑉 ∈ LMod ∧ (𝑋 ∼ 𝑌 ∧ 𝑌 ∼ 𝑍)) → 𝑋 ∼ 𝑍)
Theorem	prjsperref 40930*	The relation in ℙ𝕣𝕠𝕛 is reflexive. (Contributed by Steven Nguyen, 30-Apr-2023.)
⊢ ∼ = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ ∃𝑙 ∈ 𝐾 𝑥 = (𝑙 · 𝑦))}    &   ⊢ 𝐵 = ((Base‘𝑉) ∖ {(0g‘𝑉)})    &   ⊢ 𝑆 = (Scalar‘𝑉)    &   ⊢ · = ( ·𝑠 ‘𝑉)    &   ⊢ 𝐾 = (Base‘𝑆)    ⇒   ⊢ (𝑉 ∈ LMod → (𝑋 ∈ 𝐵 ↔ 𝑋 ∼ 𝑋))
Theorem	prjspersym 40931*	The relation in ℙ𝕣𝕠𝕛 is symmetric. (Contributed by Steven Nguyen, 1-May-2023.)
⊢ ∼ = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ ∃𝑙 ∈ 𝐾 𝑥 = (𝑙 · 𝑦))}    &   ⊢ 𝐵 = ((Base‘𝑉) ∖ {(0g‘𝑉)})    &   ⊢ 𝑆 = (Scalar‘𝑉)    &   ⊢ · = ( ·𝑠 ‘𝑉)    &   ⊢ 𝐾 = (Base‘𝑆)    ⇒   ⊢ ((𝑉 ∈ LVec ∧ 𝑋 ∼ 𝑌) → 𝑌 ∼ 𝑋)
Theorem	prjsper 40932*	The relation used to define ℙ𝕣𝕠𝕛 is an equivalence relation. (Contributed by Steven Nguyen, 1-May-2023.)
⊢ ∼ = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ ∃𝑙 ∈ 𝐾 𝑥 = (𝑙 · 𝑦))}    &   ⊢ 𝐵 = ((Base‘𝑉) ∖ {(0g‘𝑉)})    &   ⊢ 𝑆 = (Scalar‘𝑉)    &   ⊢ · = ( ·𝑠 ‘𝑉)    &   ⊢ 𝐾 = (Base‘𝑆)    ⇒   ⊢ (𝑉 ∈ LVec → ∼ Er 𝐵)
Theorem	prjspreln0 40933*	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 40934*	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 40935*	Two vectors are equivalent iff their spans are equal. (Contributed by Steven Nguyen, 31-May-2023.)
⊢ ∼ = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ ∃𝑙 ∈ 𝐾 𝑥 = (𝑙 · 𝑦))}    &   ⊢ 𝐵 = ((Base‘𝑉) ∖ {(0g‘𝑉)})    &   ⊢ 𝑆 = (Scalar‘𝑉)    &   ⊢ · = ( ·𝑠 ‘𝑉)    &   ⊢ 𝐾 = (Base‘𝑆)    &   ⊢ 𝑁 = (LSpan‘𝑉)    ⇒   ⊢ ((𝑉 ∈ LVec ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → (𝑋 ∼ 𝑌 ↔ (𝑁‘{𝑋}) = (𝑁‘{𝑌})))
Theorem	prjspeclsp 40936*	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 40937*	Alternate definition of projective space. (Contributed by Steven Nguyen, 7-Jun-2023.)
⊢ 0 = (0g‘𝑉)    &   ⊢ 𝐵 = ((Base‘𝑉) ∖ { 0 })    &   ⊢ 𝑁 = (LSpan‘𝑉)    ⇒   ⊢ (𝑉 ∈ LVec → (ℙ𝕣𝕠𝕛‘𝑉) = ∪ 𝑧 ∈ 𝐵 {((𝑁‘{𝑧}) ∖ { 0 })})
Syntax	cprjspn 40938	Extend class notation with the n-dimensional projective space function.
class ℙ𝕣𝕠𝕛n
Definition	df-prjspn 40939*	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 24750. 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 40940	Value of the n-dimensional projective space function. (Contributed by Steven Nguyen, 1-May-2023.)
⊢ ((𝑁 ∈ ℕ0 ∧ 𝐾 ∈ DivRing) → (𝑁ℙ𝕣𝕠𝕛n𝐾) = (ℙ𝕣𝕠𝕛‘(𝐾 freeLMod (0...𝑁))))
Theorem	prjspnerlem 40941*	A lemma showing that the equivalence relation used in prjspnval2 40942 and the equivalence relation used in prjspval 40927 are equal, but only with the antecedent 𝐾 ∈ DivRing. (Contributed by SN, 15-Jul-2023.)
⊢ ∼ = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ ∃𝑙 ∈ 𝑆 𝑥 = (𝑙 · 𝑦))}    &   ⊢ 𝑊 = (𝐾 freeLMod (0...𝑁))    &   ⊢ 𝐵 = ((Base‘𝑊) ∖ {(0g‘𝑊)})    &   ⊢ 𝑆 = (Base‘𝐾)    &   ⊢ · = ( ·𝑠 ‘𝑊)    ⇒   ⊢ (𝐾 ∈ DivRing → ∼ = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ ∃𝑙 ∈ (Base‘(Scalar‘𝑊))𝑥 = (𝑙 · 𝑦))})
Theorem	prjspnval2 40942*	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 40943*	The relation used to define ℙ𝕣𝕠𝕛 (and indirectly ℙ𝕣𝕠𝕛n through df-prjspn 40939) is an equivalence relation. This is a lemma that converts the equivalence relation used in results like prjspertr 40929 and prjspersym 40931 (see prjspnerlem 40941). Several theorems are covered in one thanks to the theorems around df-er 8648. (Contributed by SN, 14-Aug-2023.)
⊢ ∼ = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ ∃𝑙 ∈ 𝑆 𝑥 = (𝑙 · 𝑦))}    &   ⊢ 𝑊 = (𝐾 freeLMod (0...𝑁))    &   ⊢ 𝐵 = ((Base‘𝑊) ∖ {(0g‘𝑊)})    &   ⊢ 𝑆 = (Base‘𝐾)    &   ⊢ · = ( ·𝑠 ‘𝑊)    &   ⊢ (𝜑 → 𝐾 ∈ DivRing)    ⇒   ⊢ (𝜑 → ∼ Er 𝐵)
Theorem	prjspnvs 40944*	A nonzero multiple of a vector is equivalent to the vector. This converts the equivalence relation used in prjspvs 40934 (see prjspnerlem 40941). (Contributed by SN, 8-Aug-2024.)
⊢ ∼ = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ ∃𝑙 ∈ 𝑆 𝑥 = (𝑙 · 𝑦))}    &   ⊢ 𝑊 = (𝐾 freeLMod (0...𝑁))    &   ⊢ 𝐵 = ((Base‘𝑊) ∖ {(0g‘𝑊)})    &   ⊢ 𝑆 = (Base‘𝐾)    &   ⊢ · = ( ·𝑠 ‘𝑊)    &   ⊢ 0 = (0g‘𝐾)    &   ⊢ (𝜑 → 𝐾 ∈ DivRing)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑆)    &   ⊢ (𝜑 → 𝐶 ≠ 0 )    ⇒   ⊢ (𝜑 → (𝐶 · 𝑋) ∼ 𝑋)
Theorem	prjspnssbas 40945	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 40946	A projective point is nonempty. (Contributed by SN, 17-Jan-2025.)
⊢ 𝑃 = (𝑁ℙ𝕣𝕠𝕛n𝐾)    &   ⊢ 𝑊 = (𝐾 freeLMod (0...𝑁))    &   ⊢ 𝐵 = ((Base‘𝑊) ∖ {(0g‘𝑊)})    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    &   ⊢ (𝜑 → 𝐾 ∈ DivRing)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑃)    ⇒   ⊢ (𝜑 → 𝐴 ≠ ∅)
Theorem	0prjspnlem 40947	Lemma for 0prjspn 40952. 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 40948*	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 40949*	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 40950*	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 40951*	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 40952	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 40953	Extend class notation with the projective curve function.
class ℙ𝕣𝕠𝕛Crv
Definition	df-prjcrv 40954*	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 40760 and prjspvs 40934). (Contributed by SN, 23-Nov-2024.)
⊢ ℙ𝕣𝕠𝕛Crv = (𝑛 ∈ ℕ0, 𝑘 ∈ Field ↦ (𝑓 ∈ ∪ ran ((0...𝑛) mHomP 𝑘) ↦ {𝑝 ∈ (𝑛ℙ𝕣𝕠𝕛n𝑘) ∣ ((((0...𝑛) eval 𝑘)‘𝑓) “ 𝑝) = {(0g‘𝑘)}}))
Theorem	prjcrvfval 40955*	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 40956*	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 40957	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.26.8  Basic reductions for Fermat's Last Theorem
Theorem	dffltz 40958*	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 40959	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 40960	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 40961	A counterexample for FLT does not exist for 𝑁 = 0. (Contributed by SN, 20-Aug-2024.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    &   ⊢ (𝜑 → ((𝐴↑𝑁) + (𝐵↑𝑁)) = (𝐶↑𝑁))    ⇒   ⊢ (𝜑 → 𝑁 ∈ ℕ)
Theorem	fltdvdsabdvdsc 40962	Any factor of both 𝐴 and 𝐵 also divides 𝐶. This establishes the validity of fltabcoprmex 40963. (Contributed by SN, 21-Aug-2024.)
⊢ (𝜑 → 𝐴 ∈ ℕ)    &   ⊢ (𝜑 → 𝐵 ∈ ℕ)    &   ⊢ (𝜑 → 𝐶 ∈ ℕ)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → ((𝐴↑𝑁) + (𝐵↑𝑁)) = (𝐶↑𝑁))    ⇒   ⊢ (𝜑 → (𝐴 gcd 𝐵) ∥ 𝐶)
Theorem	fltabcoprmex 40963	A counterexample to FLT implies a counterexample to FLT with 𝐴, 𝐵 (assigned to 𝐴 / (𝐴 gcd 𝐵) and 𝐵 / (𝐴 gcd 𝐵)) coprime (by divgcdcoprm0 16541). (Contributed by SN, 20-Aug-2024.)
⊢ (𝜑 → 𝐴 ∈ ℕ)    &   ⊢ (𝜑 → 𝐵 ∈ ℕ)    &   ⊢ (𝜑 → 𝐶 ∈ ℕ)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    &   ⊢ (𝜑 → ((𝐴↑𝑁) + (𝐵↑𝑁)) = (𝐶↑𝑁))    ⇒   ⊢ (𝜑 → (((𝐴 / (𝐴 gcd 𝐵))↑𝑁) + ((𝐵 / (𝐴 gcd 𝐵))↑𝑁)) = ((𝐶 / (𝐴 gcd 𝐵))↑𝑁))
Theorem	fltaccoprm 40964	A counterexample to FLT with 𝐴, 𝐵 coprime also has 𝐴, 𝐶 coprime. (Contributed by SN, 20-Aug-2024.)
⊢ (𝜑 → 𝐴 ∈ ℕ)    &   ⊢ (𝜑 → 𝐵 ∈ ℕ)    &   ⊢ (𝜑 → 𝐶 ∈ ℕ)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    &   ⊢ (𝜑 → ((𝐴↑𝑁) + (𝐵↑𝑁)) = (𝐶↑𝑁))    &   ⊢ (𝜑 → (𝐴 gcd 𝐵) = 1)    ⇒   ⊢ (𝜑 → (𝐴 gcd 𝐶) = 1)
Theorem	fltbccoprm 40965	A counterexample to FLT with 𝐴, 𝐵 coprime also has 𝐵, 𝐶 coprime. Proven from fltaccoprm 40964 using commutativity of addition. (Contributed by SN, 20-Aug-2024.)
⊢ (𝜑 → 𝐴 ∈ ℕ)    &   ⊢ (𝜑 → 𝐵 ∈ ℕ)    &   ⊢ (𝜑 → 𝐶 ∈ ℕ)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    &   ⊢ (𝜑 → ((𝐴↑𝑁) + (𝐵↑𝑁)) = (𝐶↑𝑁))    &   ⊢ (𝜑 → (𝐴 gcd 𝐵) = 1)    ⇒   ⊢ (𝜑 → (𝐵 gcd 𝐶) = 1)
Theorem	fltabcoprm 40966	A counterexample to FLT with 𝐴, 𝐶 coprime also has 𝐴, 𝐵 coprime. Converse of fltaccoprm 40964. (Contributed by SN, 22-Aug-2024.)
⊢ (𝜑 → 𝐴 ∈ ℕ)    &   ⊢ (𝜑 → 𝐵 ∈ ℕ)    &   ⊢ (𝜑 → 𝐶 ∈ ℕ)    &   ⊢ (𝜑 → (𝐴 gcd 𝐶) = 1)    &   ⊢ (𝜑 → ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2))    ⇒   ⊢ (𝜑 → (𝐴 gcd 𝐵) = 1)
Theorem	infdesc 40967*	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 40968	If a counterexample to FLT exists, its addends are not equal. (Contributed by SN, 1-Jun-2023.)
⊢ (𝜑 → 𝐴 ∈ ℕ)    &   ⊢ (𝜑 → 𝐵 ∈ ℕ)    &   ⊢ (𝜑 → 𝐶 ∈ ℕ)    &   ⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘2))    &   ⊢ (𝜑 → ((𝐴↑𝑁) + (𝐵↑𝑁)) = (𝐶↑𝑁))    ⇒   ⊢ (𝜑 → 𝐴 ≠ 𝐵)
Theorem	flt4lem 40969	Raising a number to the fourth power is equivalent to squaring it twice. (Contributed by SN, 21-Aug-2024.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    ⇒   ⊢ (𝜑 → (𝐴↑4) = ((𝐴↑2)↑2))
Theorem	flt4lem1 40970	Satisfy the antecedent used in several pythagtrip 16706 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 40971	If 𝐴 is even, 𝐵 is odd. (Contributed by SN, 22-Aug-2024.)
⊢ (𝜑 → 𝐴 ∈ ℕ)    &   ⊢ (𝜑 → 𝐵 ∈ ℕ)    &   ⊢ (𝜑 → 𝐶 ∈ ℕ)    &   ⊢ (𝜑 → 2 ∥ 𝐴)    &   ⊢ (𝜑 → (𝐴 gcd 𝐶) = 1)    &   ⊢ (𝜑 → ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2))    ⇒   ⊢ (𝜑 → ¬ 2 ∥ 𝐵)
Theorem	flt4lem3 40972	Equivalent to pythagtriplem4 16691. Show that 𝐶 + 𝐴 and 𝐶 − 𝐴 are coprime. (Contributed by SN, 22-Aug-2024.)
⊢ (𝜑 → 𝐴 ∈ ℕ)    &   ⊢ (𝜑 → 𝐵 ∈ ℕ)    &   ⊢ (𝜑 → 𝐶 ∈ ℕ)    &   ⊢ (𝜑 → 2 ∥ 𝐴)    &   ⊢ (𝜑 → (𝐴 gcd 𝐶) = 1)    &   ⊢ (𝜑 → ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2))    ⇒   ⊢ (𝜑 → ((𝐶 + 𝐴) gcd (𝐶 − 𝐴)) = 1)
Theorem	flt4lem4 40973	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 40974	In the context of the lemmas of pythagtrip 16706, 𝑀 and 𝑁 are coprime. (Contributed by SN, 23-Aug-2024.)
⊢ 𝑀 = (((√‘(𝐶 + 𝐵)) + (√‘(𝐶 − 𝐵))) / 2)    &   ⊢ 𝑁 = (((√‘(𝐶 + 𝐵)) − (√‘(𝐶 − 𝐵))) / 2)    ⇒   ⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2) ∧ ((𝐴 gcd 𝐵) = 1 ∧ ¬ 2 ∥ 𝐴)) → (𝑀 gcd 𝑁) = 1)
Theorem	flt4lem5elem 40975	Version of fltaccoprm 40964 and fltbccoprm 40965 where 𝑀 is not squared. This can be proved in general for any polynomial in three variables: using prmdvdsncoprmbd 16602, dvds2addd 16174, and prmdvdsexp 16591, 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 40976	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 40977	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 40978	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 40979	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 40980	Satisfy the hypotheses of flt4lem4 40973. (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 40981	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 40982	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 40983*	Convert flt4lem5f 40981 into a convenient form for nna4b4nsq 40984. 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 40984	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 40985	(𝐶↑𝑁) is the largest term and therefore 𝐵 < 𝐶. (Contributed by Steven Nguyen, 22-Aug-2023.)
⊢ (𝜑 → 𝐴 ∈ ℕ)    &   ⊢ (𝜑 → 𝐵 ∈ ℕ)    &   ⊢ (𝜑 → 𝐶 ∈ ℕ)    &   ⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘3))    &   ⊢ (𝜑 → ((𝐴↑𝑁) + (𝐵↑𝑁)) = (𝐶↑𝑁))    ⇒   ⊢ (𝜑 → 𝐵 < 𝐶)
Theorem	fltnltalem 40986	Lemma for fltnlta 40987. A lower bound for 𝐴 based on pwdif 15753. (Contributed by Steven Nguyen, 22-Aug-2023.)
⊢ (𝜑 → 𝐴 ∈ ℕ)    &   ⊢ (𝜑 → 𝐵 ∈ ℕ)    &   ⊢ (𝜑 → 𝐶 ∈ ℕ)    &   ⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘3))    &   ⊢ (𝜑 → ((𝐴↑𝑁) + (𝐵↑𝑁)) = (𝐶↑𝑁))    ⇒   ⊢ (𝜑 → ((𝐶 − 𝐵) · ((𝐶↑(𝑁 − 1)) + ((𝑁 − 1) · (𝐵↑(𝑁 − 1))))) < (𝐴↑𝑁))
Theorem	fltnlta 40987	In a Fermat counterexample, the exponent 𝑁 is less than all three numbers (𝐴, 𝐵, and 𝐶). Note that 𝐴 < 𝐵 (hypothesis) and 𝐵 < 𝐶 (fltltc 40985). See https://youtu.be/EymVXkPWxyc 40985 for an outline. (Contributed by SN, 24-Aug-2023.)
⊢ (𝜑 → 𝐴 ∈ ℕ)    &   ⊢ (𝜑 → 𝐵 ∈ ℕ)    &   ⊢ (𝜑 → 𝐶 ∈ ℕ)    &   ⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘3))    &   ⊢ (𝜑 → ((𝐴↑𝑁) + (𝐵↑𝑁)) = (𝐶↑𝑁))    &   ⊢ (𝜑 → 𝐴 < 𝐵)    ⇒   ⊢ (𝜑 → 𝑁 < 𝐴)
21.27  Mathbox for Igor Ieskov
Theorem	binom2d 40988	Deduction form of binom2. (Contributed by Igor Ieskov, 14-Dec-2023.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    ⇒   ⊢ (𝜑 → ((𝐴 + 𝐵)↑2) = (((𝐴↑2) + (2 · (𝐴 · 𝐵))) + (𝐵↑2)))
Theorem	cu3addd 40989	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	sqnegd 40990	The square of the negative of a number. (Contributed by Igor Ieskov, 21-Jan-2024.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    ⇒   ⊢ (𝜑 → (-𝐴↑2) = (𝐴↑2))
Theorem	negexpidd 40991	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 40992*	An extended version of rexlimdvv 3204 to include three set variables. (Contributed by Igor Ieskov, 21-Jan-2024.)
⊢ (𝜑 → ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐶) → (𝜓 → 𝜒)))    ⇒   ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 ∃𝑧 ∈ 𝐶 𝜓 → 𝜒))
Theorem	3cubeslem1 40993	Lemma for 3cubes 40999. (Contributed by Igor Ieskov, 22-Jan-2024.)
⊢ (𝜑 → 𝐴 ∈ ℚ)    ⇒   ⊢ (𝜑 → 0 < (((𝐴 + 1)↑2) − 𝐴))
Theorem	3cubeslem2 40994	Lemma for 3cubes 40999. Used to show that the denominators in 3cubeslem4 40998 are nonzero. (Contributed by Igor Ieskov, 22-Jan-2024.)
⊢ (𝜑 → 𝐴 ∈ ℚ)    ⇒   ⊢ (𝜑 → ¬ ((((3↑3) · (𝐴↑2)) + ((3↑2) · 𝐴)) + 3) = 0)
Theorem	3cubeslem3l 40995	Lemma for 3cubes 40999. (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 40996	Lemma for 3cubes 40999. (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 40997	Lemma for 3cubes 40999. (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 40998	Lemma for 3cubes 40999. 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 40999*	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.28  Mathbox for OpenAI
Theorem	rntrclfvOAI 41000	The range of the transitive closure is equal to the range of the relation. (Contributed by OpenAI, 7-Jul-2020.)
⊢ (𝑅 ∈ 𝑉 → ran (t+‘𝑅) = ran 𝑅)