Home Metamath Proof ExplorerTheorem List (p. 400 of 457) < Previous  Next > Bad symbols? Try the GIF version. Mirrors  >  Metamath Home Page  >  MPE Home Page  >  Theorem List Contents  >  Recent Proofs       This page: Page List

 Color key: Metamath Proof Explorer (1-28790) Hilbert Space Explorer (28791-30313) Users' Mathboxes (30314-45688)

Theorem List for Metamath Proof Explorer - 39901-40000   *Has distinct variable group(s)
TypeLabelDescription
Statement

Theoremremulinvcom 39901 A left multiplicative inverse is a right multiplicative inverse. Proven without ax-mulcom 10629. (Contributed by SN, 5-Feb-2024.)
(𝜑𝐴 ∈ ℝ)    &   (𝜑𝐵 ∈ ℝ)    &   (𝜑 → (𝐴 · 𝐵) = 1)       (𝜑 → (𝐵 · 𝐴) = 1)

Theoremremulid2 39902 Commuted version of ax-1rid 10635 without ax-mulcom 10629. (Contributed by SN, 5-Feb-2024.)
(𝐴 ∈ ℝ → (1 · 𝐴) = 𝐴)

Theoremsn-1ticom 39903 Lemma for sn-mulid2 39904 and it1ei 39905. (Contributed by SN, 27-May-2024.)
(1 · i) = (i · 1)

Theoremsn-mulid2 39904 mulid2 10668 without ax-mulcom 10629. (Contributed by SN, 27-May-2024.)
(𝐴 ∈ ℂ → (1 · 𝐴) = 𝐴)

Theoremit1ei 39905 1 is a multiplicative identity for i (see sn-mulid2 39904 for commuted version). (Contributed by SN, 1-Jun-2024.)
(i · 1) = i

Theoremipiiie0 39906 The multiplicative inverse of i (per i4 13607) is also its additive inverse. (Contributed by SN, 30-Jun-2024.)
(i + (i · (i · i))) = 0

Theoremremulcand 39907 Commuted version of remulcan2d 39785 without ax-mulcom 10629. (Contributed by SN, 21-Feb-2024.)
(𝜑𝐴 ∈ ℝ)    &   (𝜑𝐵 ∈ ℝ)    &   (𝜑𝐶 ∈ ℝ)    &   (𝜑𝐶 ≠ 0)       (𝜑 → ((𝐶 · 𝐴) = (𝐶 · 𝐵) ↔ 𝐴 = 𝐵))

Theoremsn-0tie0 39908 Lemma for sn-mul02 39909. Commuted version of sn-it0e0 39884. (Contributed by SN, 30-Jun-2024.)
(0 · i) = 0

Theoremsn-mul02 39909 mul02 10846 without ax-mulcom 10629. See https://github.com/icecream17/Stuff/blob/main/math/0A%3D0.md 10629 for an outline. (Contributed by SN, 30-Jun-2024.)
(𝐴 ∈ ℂ → (0 · 𝐴) = 0)

((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (0 < 𝐴𝐵 < (𝐵 + 𝐴)))

Theoremreposdif 39911 Comparison of two numbers whose difference is positive. Compare posdif 11161. (Contributed by SN, 13-Feb-2024.)
((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 < 𝐵 ↔ 0 < (𝐵 𝐴)))

Theoremrelt0neg1 39912 Comparison of a real and its negative to zero. Compare lt0neg1 11174. (Contributed by SN, 13-Feb-2024.)
(𝐴 ∈ ℝ → (𝐴 < 0 ↔ 0 < (0 − 𝐴)))

Theoremrelt0neg2 39913 Comparison of a real and its negative to zero. Compare lt0neg2 11175. (Contributed by SN, 13-Feb-2024.)
(𝐴 ∈ ℝ → (0 < 𝐴 ↔ (0 − 𝐴) < 0))

Theoremmulgt0con1dlem 39914 Lemma for mulgt0con1d 39915. Contraposes a positive deduction to a negative deduction. (Contributed by SN, 26-Jun-2024.)
(𝜑𝐴 ∈ ℝ)    &   (𝜑𝐵 ∈ ℝ)    &   (𝜑 → (0 < 𝐴 → 0 < 𝐵))    &   (𝜑 → (𝐴 = 0 → 𝐵 = 0))       (𝜑 → (𝐵 < 0 → 𝐴 < 0))

Theoremmulgt0con1d 39915 Counterpart to mulgt0con2d 39916, though not a lemma of anything. This is the first use of ax-pre-mulgt0 10642. (Contributed by SN, 26-Jun-2024.)
(𝜑𝐴 ∈ ℝ)    &   (𝜑𝐵 ∈ ℝ)    &   (𝜑 → 0 < 𝐵)    &   (𝜑 → (𝐴 · 𝐵) < 0)       (𝜑𝐴 < 0)

Theoremmulgt0con2d 39916 Lemma for mulgt0b2d 39917 and contrapositive of mulgt0 10746. (Contributed by SN, 26-Jun-2024.)
(𝜑𝐴 ∈ ℝ)    &   (𝜑𝐵 ∈ ℝ)    &   (𝜑 → 0 < 𝐴)    &   (𝜑 → (𝐴 · 𝐵) < 0)       (𝜑𝐵 < 0)

Theoremmulgt0b2d 39917 Biconditional, deductive form of mulgt0 10746. The second factor is positive iff the product is. Note that the commuted form cannot be proven since resubdi 39866 does not have a commuted form. (Contributed by SN, 26-Jun-2024.)
(𝜑𝐴 ∈ ℝ)    &   (𝜑𝐵 ∈ ℝ)    &   (𝜑 → 0 < 𝐴)       (𝜑 → (0 < 𝐵 ↔ 0 < (𝐴 · 𝐵)))

Theoremsn-ltmul2d 39918 ltmul2d 12504 without ax-mulcom 10629. (Contributed by SN, 26-Jun-2024.)
(𝜑𝐴 ∈ ℝ)    &   (𝜑𝐵 ∈ ℝ)    &   (𝜑𝐶 ∈ ℝ)    &   (𝜑 → 0 < 𝐶)       (𝜑 → ((𝐶 · 𝐴) < (𝐶 · 𝐵) ↔ 𝐴 < 𝐵))

Theoremsn-0lt1 39919 0lt1 11190 without ax-mulcom 10629. (Contributed by SN, 13-Feb-2024.)
0 < 1

Theoremsn-ltp1 39920 ltp1 11508 without ax-mulcom 10629. (Contributed by SN, 13-Feb-2024.)
(𝐴 ∈ ℝ → 𝐴 < (𝐴 + 1))

Theoremreneg1lt0 39921 Lemma for sn-inelr 39922. (Contributed by SN, 1-Jun-2024.)
(0 − 1) < 0

Theoremsn-inelr 39922 inelr 11654 without ax-mulcom 10629. (Contributed by SN, 1-Jun-2024.)
¬ i ∈ ℝ

Theoremitrere 39923 i times a real is real iff the real is zero. (Contributed by SN, 27-Jun-2024.)
(𝑅 ∈ ℝ → ((i · 𝑅) ∈ ℝ ↔ 𝑅 = 0))

Theoremretire 39924 Commuted version of itrere 39923. (Contributed by SN, 27-Jun-2024.)
(𝑅 ∈ ℝ → ((𝑅 · i) ∈ ℝ ↔ 𝑅 = 0))

Theoremcnreeu 39925 The reals in the expression given by cnre 10666 uniquely define a complex number. (Contributed by SN, 27-Jun-2024.)
(𝜑𝑟 ∈ ℝ)    &   (𝜑𝑠 ∈ ℝ)    &   (𝜑𝑡 ∈ ℝ)    &   (𝜑𝑢 ∈ ℝ)       (𝜑 → ((𝑟 + (i · 𝑠)) = (𝑡 + (i · 𝑢)) ↔ (𝑟 = 𝑡𝑠 = 𝑢)))

Theoremsn-sup2 39926* sup2 11623 with exactly the same proof except for using sn-ltp1 39920 instead of ltp1 11508, saving ax-mulcom 10629. (Contributed by SN, 26-Jun-2024.)
((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦𝐴 (𝑦 < 𝑥𝑦 = 𝑥)) → ∃𝑥 ∈ ℝ (∀𝑦𝐴 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧𝐴 𝑦 < 𝑧)))

20.26.6  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.

Syntaxcprjsp 39927 Extend class notation with the projective space function.
class ℙ𝕣𝕠𝕛

Definitiondf-prjsp 39928* 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). (Contributed by BJ and Steven Nguyen, 29-Apr-2023.)
ℙ𝕣𝕠𝕛 = (𝑣 ∈ LVec ↦ ((Base‘𝑣) ∖ {(0g𝑣)}) / 𝑏(𝑏 / {⟨𝑥, 𝑦⟩ ∣ ((𝑥𝑏𝑦𝑏) ∧ ∃𝑙 ∈ (Base‘(Scalar‘𝑣))𝑥 = (𝑙( ·𝑠𝑣)𝑦))}))

Theoremprjspval 39929* 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 → (ℙ𝕣𝕠𝕛‘𝑉) = (𝐵 / {⟨𝑥, 𝑦⟩ ∣ ((𝑥𝐵𝑦𝐵) ∧ ∃𝑙𝐾 𝑥 = (𝑙 · 𝑦))}))

Theoremprjsprel 39930* Utility theorem regarding the relation used in ℙ𝕣𝕠𝕛. (Contributed by Steven Nguyen, 29-Apr-2023.)
= {⟨𝑥, 𝑦⟩ ∣ ((𝑥𝐵𝑦𝐵) ∧ ∃𝑙𝐾 𝑥 = (𝑙 · 𝑦))}       (𝑋 𝑌 ↔ ((𝑋𝐵𝑌𝐵) ∧ ∃𝑚𝐾 𝑋 = (𝑚 · 𝑌)))

Theoremprjspertr 39931* The relation in ℙ𝕣𝕠𝕛 is transitive. (Contributed by Steven Nguyen, 1-May-2023.)
= {⟨𝑥, 𝑦⟩ ∣ ((𝑥𝐵𝑦𝐵) ∧ ∃𝑙𝐾 𝑥 = (𝑙 · 𝑦))}    &   𝐵 = ((Base‘𝑉) ∖ {(0g𝑉)})    &   𝑆 = (Scalar‘𝑉)    &    · = ( ·𝑠𝑉)    &   𝐾 = (Base‘𝑆)       ((𝑉 ∈ LMod ∧ (𝑋 𝑌𝑌 𝑍)) → 𝑋 𝑍)

Theoremprjsperref 39932* The relation in ℙ𝕣𝕠𝕛 is reflexive. (Contributed by Steven Nguyen, 30-Apr-2023.)
= {⟨𝑥, 𝑦⟩ ∣ ((𝑥𝐵𝑦𝐵) ∧ ∃𝑙𝐾 𝑥 = (𝑙 · 𝑦))}    &   𝐵 = ((Base‘𝑉) ∖ {(0g𝑉)})    &   𝑆 = (Scalar‘𝑉)    &    · = ( ·𝑠𝑉)    &   𝐾 = (Base‘𝑆)       (𝑉 ∈ LMod → (𝑋𝐵𝑋 𝑋))

Theoremprjspersym 39933* The relation in ℙ𝕣𝕠𝕛 is symmetric. (Contributed by Steven Nguyen, 1-May-2023.)
= {⟨𝑥, 𝑦⟩ ∣ ((𝑥𝐵𝑦𝐵) ∧ ∃𝑙𝐾 𝑥 = (𝑙 · 𝑦))}    &   𝐵 = ((Base‘𝑉) ∖ {(0g𝑉)})    &   𝑆 = (Scalar‘𝑉)    &    · = ( ·𝑠𝑉)    &   𝐾 = (Base‘𝑆)       ((𝑉 ∈ LVec ∧ 𝑋 𝑌) → 𝑌 𝑋)

Theoremprjsper 39934* The relation used to define ℙ𝕣𝕠𝕛 is an equivalence relation. (Contributed by Steven Nguyen, 1-May-2023.)
= {⟨𝑥, 𝑦⟩ ∣ ((𝑥𝐵𝑦𝐵) ∧ ∃𝑙𝐾 𝑥 = (𝑙 · 𝑦))}    &   𝐵 = ((Base‘𝑉) ∖ {(0g𝑉)})    &   𝑆 = (Scalar‘𝑉)    &    · = ( ·𝑠𝑉)    &   𝐾 = (Base‘𝑆)       (𝑉 ∈ LVec → Er 𝐵)

Theoremprjspreln0 39935* Two nonzero vectors are equivalent by a nonzero scalar. (Contributed by Steven Nguyen, 31-May-2023.)
= {⟨𝑥, 𝑦⟩ ∣ ((𝑥𝐵𝑦𝐵) ∧ ∃𝑙𝐾 𝑥 = (𝑙 · 𝑦))}    &   𝐵 = ((Base‘𝑉) ∖ {(0g𝑉)})    &   𝑆 = (Scalar‘𝑉)    &    · = ( ·𝑠𝑉)    &   𝐾 = (Base‘𝑆)    &    0 = (0g𝑆)       (𝑉 ∈ LVec → (𝑋 𝑌 ↔ ((𝑋𝐵𝑌𝐵) ∧ ∃𝑚 ∈ (𝐾 ∖ { 0 })𝑋 = (𝑚 · 𝑌))))

Theoremprjspvs 39936* 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 })) → (𝑁 · 𝑋) 𝑋)

Theoremprjsprellsp 39937* Two vectors are equivalent iff their spans are equal. (Contributed by Steven Nguyen, 31-May-2023.)
= {⟨𝑥, 𝑦⟩ ∣ ((𝑥𝐵𝑦𝐵) ∧ ∃𝑙𝐾 𝑥 = (𝑙 · 𝑦))}    &   𝐵 = ((Base‘𝑉) ∖ {(0g𝑉)})    &   𝑆 = (Scalar‘𝑉)    &    · = ( ·𝑠𝑉)    &   𝐾 = (Base‘𝑆)    &   𝑁 = (LSpan‘𝑉)       ((𝑉 ∈ LVec ∧ (𝑋𝐵𝑌𝐵)) → (𝑋 𝑌 ↔ (𝑁‘{𝑋}) = (𝑁‘{𝑌})))

Theoremprjspeclsp 39938* 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𝑉)}))

Theoremprjspval2 39939* Alternate definition of projective space. (Contributed by Steven Nguyen, 7-Jun-2023.)
0 = (0g𝑉)    &   𝐵 = ((Base‘𝑉) ∖ { 0 })    &   𝑁 = (LSpan‘𝑉)       (𝑉 ∈ LVec → (ℙ𝕣𝕠𝕛‘𝑉) = 𝑧𝐵 {((𝑁‘{𝑧}) ∖ { 0 })})

Syntaxcprjspn 39940 Extend class notation with the n-dimensional projective space function.
class ℙ𝕣𝕠𝕛n

Definitiondf-prjspn 39941* 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 24076. 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...𝑛))))

Theoremprjspnval 39942 Value of the n-dimensional projective space function. (Contributed by Steven Nguyen, 1-May-2023.)
((𝑁 ∈ ℕ0𝐾 ∈ DivRing) → (𝑁ℙ𝕣𝕠𝕛n𝐾) = (ℙ𝕣𝕠𝕛‘(𝐾 freeLMod (0...𝑁))))

Theoremprjspnerlem 39943* A lemma showing that the equivalence relation used in prjspnval2 39944 and the equivalence relation used in prjspval 39929 are equal, but only with the antecedent 𝐾 ∈ DivRing. (Contributed by SN, 15-Jul-2023.)
= {⟨𝑥, 𝑦⟩ ∣ ((𝑥𝐵𝑦𝐵) ∧ ∃𝑙𝑆 𝑥 = (𝑙 · 𝑦))}    &   𝑊 = (𝐾 freeLMod (0...𝑁))    &   𝐵 = ((Base‘𝑊) ∖ {(0g𝑊)})    &   𝑆 = (Base‘𝐾)    &    · = ( ·𝑠𝑊)       (𝐾 ∈ DivRing → = {⟨𝑥, 𝑦⟩ ∣ ((𝑥𝐵𝑦𝐵) ∧ ∃𝑙 ∈ (Base‘(Scalar‘𝑊))𝑥 = (𝑙 · 𝑦))})

Theoremprjspnval2 39944* Value of the n-dimensional projective space function, expanded. (Contributed by Steven Nguyen, 15-Jul-2023.)
= {⟨𝑥, 𝑦⟩ ∣ ((𝑥𝐵𝑦𝐵) ∧ ∃𝑙𝑆 𝑥 = (𝑙 · 𝑦))}    &   𝑊 = (𝐾 freeLMod (0...𝑁))    &   𝐵 = ((Base‘𝑊) ∖ {(0g𝑊)})    &   𝑆 = (Base‘𝐾)    &    · = ( ·𝑠𝑊)       ((𝑁 ∈ ℕ0𝐾 ∈ DivRing) → (𝑁ℙ𝕣𝕠𝕛n𝐾) = (𝐵 / ))

Theoremprjspner 39945* The relation used to define ℙ𝕣𝕠𝕛 (and indirectly ℙ𝕣𝕠𝕛n through df-prjspn 39941) is an equivalence relation. This is a lemma that converts the equivalence relation used in results like prjspertr 39931 and prjspersym 39933 (see prjspnerlem 39943). Several theorems are covered in one thanks to the theorems around df-er 8297. (Contributed by SN, 14-Aug-2023.)
= {⟨𝑥, 𝑦⟩ ∣ ((𝑥𝐵𝑦𝐵) ∧ ∃𝑙𝑆 𝑥 = (𝑙 · 𝑦))}    &   𝑊 = (𝐾 freeLMod (0...𝑁))    &   𝐵 = ((Base‘𝑊) ∖ {(0g𝑊)})    &   𝑆 = (Base‘𝐾)    &    · = ( ·𝑠𝑊)    &   (𝜑𝐾 ∈ DivRing)       (𝜑 Er 𝐵)

Theoremprjspnvs 39946* A nonzero multiple of a vector is equivalent to the vector. This converts the equivalence relation used in prjspvs 39936 (see prjspnerlem 39943). (Contributed by SN, 8-Aug-2024.)
= {⟨𝑥, 𝑦⟩ ∣ ((𝑥𝐵𝑦𝐵) ∧ ∃𝑙𝑆 𝑥 = (𝑙 · 𝑦))}    &   𝑊 = (𝐾 freeLMod (0...𝑁))    &   𝐵 = ((Base‘𝑊) ∖ {(0g𝑊)})    &   𝑆 = (Base‘𝐾)    &    · = ( ·𝑠𝑊)    &    0 = (0g𝐾)    &   (𝜑𝐾 ∈ DivRing)    &   (𝜑𝑋𝐵)    &   (𝜑𝐶𝑆)    &   (𝜑𝐶0 )       (𝜑 → (𝐶 · 𝑋) 𝑋)

Theorem0prjspnlem 39947 Lemma for 0prjspn 39952. 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𝐵)

Theoremprjspnfv01 39948* 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 ))

Theoremprjspner01 39949* 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)    &   (𝜑𝑋𝐵)       (𝜑𝑋 (𝐹𝑋))

Theoremprjspner1 39950* 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 )       (𝜑 → (𝑋 𝑌 ↔ (𝐹𝑋) = (𝐹𝑌)))

Theorem0prjspnrel 39951* 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 )

Theorem0prjspn 39952 A zero-dimensional projective space has only 1 point. (Contributed by Steven Nguyen, 9-Jun-2023.)
𝑊 = (𝐾 freeLMod (0...0))    &   𝐵 = ((Base‘𝑊) ∖ {(0g𝑊)})       (𝐾 ∈ DivRing → (0ℙ𝕣𝕠𝕛n𝐾) = {𝐵})

20.26.7  Basic reductions for Fermat's Last Theorem

Theoremdffltz 39953* 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})((𝑎𝑛) + (𝑏𝑛)) ≠ (𝑐𝑛))

Theoremfltmul 39954 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, hence the label is more about the context in which this theorem is used). (Contributed by SN, 20-Aug-2024.)
(𝜑𝑆 ∈ ℂ)    &   (𝜑𝐴 ∈ ℂ)    &   (𝜑𝐵 ∈ ℂ)    &   (𝜑𝐶 ∈ ℂ)    &   (𝜑𝑁 ∈ ℕ0)    &   (𝜑 → ((𝐴𝑁) + (𝐵𝑁)) = (𝐶𝑁))       (𝜑 → (((𝑆 · 𝐴)↑𝑁) + ((𝑆 · 𝐵)↑𝑁)) = ((𝑆 · 𝐶)↑𝑁))

Theoremfltdiv 39955 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)    &   (𝜑 → ((𝐴𝑁) + (𝐵𝑁)) = (𝐶𝑁))       (𝜑 → (((𝐴 / 𝑆)↑𝑁) + ((𝐵 / 𝑆)↑𝑁)) = ((𝐶 / 𝑆)↑𝑁))

Theoremflt0 39956 A counterexample for FLT does not exist for 𝑁 = 0. (Contributed by SN, 20-Aug-2024.)
(𝜑𝐴 ∈ ℂ)    &   (𝜑𝐵 ∈ ℂ)    &   (𝜑𝐶 ∈ ℂ)    &   (𝜑𝑁 ∈ ℕ0)    &   (𝜑 → ((𝐴𝑁) + (𝐵𝑁)) = (𝐶𝑁))       (𝜑𝑁 ∈ ℕ)

Theoremfltdvdsabdvdsc 39957 Any factor of both 𝐴 and 𝐵 also divides 𝐶. This establishes the validity of fltabcoprmex 39958. (Contributed by SN, 21-Aug-2024.)
(𝜑𝐴 ∈ ℕ)    &   (𝜑𝐵 ∈ ℕ)    &   (𝜑𝐶 ∈ ℕ)    &   (𝜑𝑁 ∈ ℕ)    &   (𝜑 → ((𝐴𝑁) + (𝐵𝑁)) = (𝐶𝑁))       (𝜑 → (𝐴 gcd 𝐵) ∥ 𝐶)

Theoremfltabcoprmex 39958 A counterexample to FLT implies a counterexample to FLT with 𝐴, 𝐵 (assigned to 𝐴 / (𝐴 gcd 𝐵) and 𝐵 / (𝐴 gcd 𝐵)) coprime (by divgcdcoprm0 16051). (Contributed by SN, 20-Aug-2024.)
(𝜑𝐴 ∈ ℕ)    &   (𝜑𝐵 ∈ ℕ)    &   (𝜑𝐶 ∈ ℕ)    &   (𝜑𝑁 ∈ ℕ0)    &   (𝜑 → ((𝐴𝑁) + (𝐵𝑁)) = (𝐶𝑁))       (𝜑 → (((𝐴 / (𝐴 gcd 𝐵))↑𝑁) + ((𝐵 / (𝐴 gcd 𝐵))↑𝑁)) = ((𝐶 / (𝐴 gcd 𝐵))↑𝑁))

Theoremfltaccoprm 39959 A counterexample to FLT with 𝐴, 𝐵 coprime also has 𝐴, 𝐶 coprime. (Contributed by SN, 20-Aug-2024.)
(𝜑𝐴 ∈ ℕ)    &   (𝜑𝐵 ∈ ℕ)    &   (𝜑𝐶 ∈ ℕ)    &   (𝜑𝑁 ∈ ℕ0)    &   (𝜑 → ((𝐴𝑁) + (𝐵𝑁)) = (𝐶𝑁))    &   (𝜑 → (𝐴 gcd 𝐵) = 1)       (𝜑 → (𝐴 gcd 𝐶) = 1)

Theoremfltbccoprm 39960 A counterexample to FLT with 𝐴, 𝐵 coprime also has 𝐵, 𝐶 coprime. Proven from fltaccoprm 39959 using commutativity of addition. (Contributed by SN, 20-Aug-2024.)
(𝜑𝐴 ∈ ℕ)    &   (𝜑𝐵 ∈ ℕ)    &   (𝜑𝐶 ∈ ℕ)    &   (𝜑𝑁 ∈ ℕ0)    &   (𝜑 → ((𝐴𝑁) + (𝐵𝑁)) = (𝐶𝑁))    &   (𝜑 → (𝐴 gcd 𝐵) = 1)       (𝜑 → (𝐵 gcd 𝐶) = 1)

Theoremfltabcoprm 39961 A counterexample to FLT with 𝐴, 𝐶 coprime also has 𝐴, 𝐵 coprime. Converse of fltaccoprm 39959. (Contributed by SN, 22-Aug-2024.)
(𝜑𝐴 ∈ ℕ)    &   (𝜑𝐵 ∈ ℕ)    &   (𝜑𝐶 ∈ ℕ)    &   (𝜑 → (𝐴 gcd 𝐶) = 1)    &   (𝜑 → ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2))       (𝜑 → (𝐴 gcd 𝐵) = 1)

Theoreminfdesc 39962* 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.)
(𝑦 = 𝑥 → (𝜓𝜒))    &   (𝑦 = 𝑧 → (𝜓𝜃))    &   (𝜑𝑆 ⊆ (ℤ𝑀))    &   ((𝜑 ∧ (𝑥𝑆𝜒)) → ∃𝑧𝑆 (𝜃𝑧 < 𝑥))       (𝜑 → {𝑦𝑆𝜓} = ∅)

Theoremfltne 39963 If a counterexample to FLT exists, its addends are not equal. (Contributed by SN, 1-Jun-2023.)
(𝜑𝐴 ∈ ℕ)    &   (𝜑𝐵 ∈ ℕ)    &   (𝜑𝐶 ∈ ℕ)    &   (𝜑𝑁 ∈ (ℤ‘2))    &   (𝜑 → ((𝐴𝑁) + (𝐵𝑁)) = (𝐶𝑁))       (𝜑𝐴𝐵)

Theoremflt4lem 39964 Raising a number to the fourth power is equivalent to squaring it twice. (Contributed by SN, 21-Aug-2024.)
(𝜑𝐴 ∈ ℂ)       (𝜑 → (𝐴↑4) = ((𝐴↑2)↑2))

Theoremflt4lem1 39965 Satisfy the antecedent used in several pythagtrip 16216 lemmas, with 𝐴, 𝐶 coprime rather than 𝐴, 𝐵. (Contributed by SN, 21-Aug-2024.)
(𝜑𝐴 ∈ ℕ)    &   (𝜑𝐵 ∈ ℕ)    &   (𝜑𝐶 ∈ ℕ)    &   (𝜑 → ¬ 2 ∥ 𝐴)    &   (𝜑 → (𝐴 gcd 𝐶) = 1)    &   (𝜑 → ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2))       (𝜑 → ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2) ∧ ((𝐴 gcd 𝐵) = 1 ∧ ¬ 2 ∥ 𝐴)))

Theoremflt4lem2 39966 If 𝐴 is even, 𝐵 is odd. (Contributed by SN, 22-Aug-2024.)
(𝜑𝐴 ∈ ℕ)    &   (𝜑𝐵 ∈ ℕ)    &   (𝜑𝐶 ∈ ℕ)    &   (𝜑 → 2 ∥ 𝐴)    &   (𝜑 → (𝐴 gcd 𝐶) = 1)    &   (𝜑 → ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2))       (𝜑 → ¬ 2 ∥ 𝐵)

Theoremflt4lem3 39967 Equivalent to pythagtriplem4 16201. Show that 𝐶 + 𝐴 and 𝐶𝐴 are coprime. (Contributed by SN, 22-Aug-2024.)
(𝜑𝐴 ∈ ℕ)    &   (𝜑𝐵 ∈ ℕ)    &   (𝜑𝐶 ∈ ℕ)    &   (𝜑 → 2 ∥ 𝐴)    &   (𝜑 → (𝐴 gcd 𝐶) = 1)    &   (𝜑 → ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2))       (𝜑 → ((𝐶 + 𝐴) gcd (𝐶𝐴)) = 1)

Theoremflt4lem4 39968 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)))

Theoremflt4lem5 39969 In the context of the lemmas of pythagtrip 16216, 𝑀 and 𝑁 are coprime. (Contributed by SN, 23-Aug-2024.)
𝑀 = (((√‘(𝐶 + 𝐵)) + (√‘(𝐶𝐵))) / 2)    &   𝑁 = (((√‘(𝐶 + 𝐵)) − (√‘(𝐶𝐵))) / 2)       (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2) ∧ ((𝐴 gcd 𝐵) = 1 ∧ ¬ 2 ∥ 𝐴)) → (𝑀 gcd 𝑁) = 1)

Theoremflt4lem5elem 39970 Version of fltaccoprm 39959 and fltbccoprm 39960 where 𝑀 is not squared. This can be proved in general for any polynomial in three variables: using prmdvdsncoprmbd 16112, dvds2addd 15683, and prmdvdsexp 16101, 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))

Theoremflt4lem5a 39971 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))

Theoremflt4lem5b 39972 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))

Theoremflt4lem5c 39973 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 · (𝑅 · 𝑆)))

Theoremflt4lem5d 39974 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)))

Theoremflt4lem5e 39975 Satisfy the hypotheses of flt4lem4 39968. EDITORIAL: This is not minimized! (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) ∈ ℕ)))

Theoremflt4lem5f 39976 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)))

Theoremflt4lem6 39977 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)))

Theoremflt4lem7 39978* Convert flt4lem5f 39976 into a convenient form for nna4b4nsq 39979. TODO-SN: The change to (𝐴 gcd 𝐵) = 1 points at some inefficiency in the lemmas. EDITORIAL: This is not minimized! (Contributed by SN, 25-Aug-2024.)
(𝜑𝐴 ∈ ℕ)    &   (𝜑𝐵 ∈ ℕ)    &   (𝜑𝐶 ∈ ℕ)    &   (𝜑 → ¬ 2 ∥ 𝐴)    &   (𝜑 → (𝐴 gcd 𝐵) = 1)    &   (𝜑 → ((𝐴↑4) + (𝐵↑4)) = (𝐶↑2))       (𝜑 → ∃𝑙 ∈ ℕ (∃𝑔 ∈ ℕ ∃ ∈ ℕ (¬ 2 ∥ 𝑔 ∧ ((𝑔 gcd ) = 1 ∧ ((𝑔↑4) + (↑4)) = (𝑙↑2))) ∧ 𝑙 < 𝐶))

Theoremnna4b4nsq 39979 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))

Theoremfltltc 39980 (𝐶𝑁) is the largest term and therefore 𝐵 < 𝐶. (Contributed by Steven Nguyen, 22-Aug-2023.)
(𝜑𝐴 ∈ ℕ)    &   (𝜑𝐵 ∈ ℕ)    &   (𝜑𝐶 ∈ ℕ)    &   (𝜑𝑁 ∈ (ℤ‘3))    &   (𝜑 → ((𝐴𝑁) + (𝐵𝑁)) = (𝐶𝑁))       (𝜑𝐵 < 𝐶)

Theoremfltnltalem 39981 Lemma for fltnlta 39982. A lower bound for 𝐴 based on pwdif 15261. (Contributed by Steven Nguyen, 22-Aug-2023.)
(𝜑𝐴 ∈ ℕ)    &   (𝜑𝐵 ∈ ℕ)    &   (𝜑𝐶 ∈ ℕ)    &   (𝜑𝑁 ∈ (ℤ‘3))    &   (𝜑 → ((𝐴𝑁) + (𝐵𝑁)) = (𝐶𝑁))       (𝜑 → ((𝐶𝐵) · ((𝐶↑(𝑁 − 1)) + ((𝑁 − 1) · (𝐵↑(𝑁 − 1))))) < (𝐴𝑁))

Theoremfltnlta 39982 𝑁 is less than 𝐴. See https://www.youtu.be/EymVXkPWxyc for an outline. (Contributed by Steven Nguyen, 24-Aug-2023.)
(𝜑𝐴 ∈ ℕ)    &   (𝜑𝐵 ∈ ℕ)    &   (𝜑𝐶 ∈ ℕ)    &   (𝜑𝑁 ∈ (ℤ‘3))    &   (𝜑 → ((𝐴𝑁) + (𝐵𝑁)) = (𝐶𝑁))    &   (𝜑𝐴 < 𝐵)       (𝜑𝑁 < 𝐴)

20.27  Mathbox for Igor Ieskov

Theorembinom2d 39983 Deduction form of binom2. (Contributed by Igor Ieskov, 14-Dec-2023.)
(𝜑𝐴 ∈ ℂ)    &   (𝜑𝐵 ∈ ℂ)       (𝜑 → ((𝐴 + 𝐵)↑2) = (((𝐴↑2) + (2 · (𝐴 · 𝐵))) + (𝐵↑2)))

Theoremcu3addd 39984 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))))

Theoremsqnegd 39985 The square of the negative of a number. (Contributed by Igor Ieskov, 21-Jan-2024.)
(𝜑𝐴 ∈ ℂ)       (𝜑 → (-𝐴↑2) = (𝐴↑2))

Theoremnegexpidd 39986 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)

Theoremrexlimdv3d 39987* An extended version of rexlimdvv 3218 to include three set variables. (Contributed by Igor Ieskov, 21-Jan-2024.)
(𝜑 → ((𝑥𝐴𝑦𝐵𝑧𝐶) → (𝜓𝜒)))       (𝜑 → (∃𝑥𝐴𝑦𝐵𝑧𝐶 𝜓𝜒))

Theorem3cubeslem1 39988 Lemma for 3cubes 39994. (Contributed by Igor Ieskov, 22-Jan-2024.)
(𝜑𝐴 ∈ ℚ)       (𝜑 → 0 < (((𝐴 + 1)↑2) − 𝐴))

Theorem3cubeslem2 39989 Lemma for 3cubes 39994. Used to show that the denominators in 3cubeslem4 39993 are nonzero. (Contributed by Igor Ieskov, 22-Jan-2024.)
(𝜑𝐴 ∈ ℚ)       (𝜑 → ¬ ((((3↑3) · (𝐴↑2)) + ((3↑2) · 𝐴)) + 3) = 0)

Theorem3cubeslem3l 39990 Lemma for 3cubes 39994. (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)))))))))

Theorem3cubeslem3r 39991 Lemma for 3cubes 39994. (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)))))))))

Theorem3cubeslem3 39992 Lemma for 3cubes 39994. (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)))

Theorem3cubeslem4 39993 Lemma for 3cubes 39994. 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)))

Theorem3cubes 39994* 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)))

20.28  Mathbox for OpenAI

TheoremrntrclfvOAI 39995 The range of the transitive closure is equal to the range of the relation. (Contributed by OpenAI, 7-Jul-2020.)
(𝑅𝑉 → ran (t+‘𝑅) = ran 𝑅)

20.29  Mathbox for Stefan O'Rear

20.29.1  Additional elementary logic and set theory

Theoremmoxfr 39996* Transfer at-most-one between related expressions. (Contributed by Stefan O'Rear, 12-Feb-2015.)
𝐴 ∈ V    &   ∃!𝑦 𝑥 = 𝐴    &   (𝑥 = 𝐴 → (𝜑𝜓))       (∃*𝑥𝜑 ↔ ∃*𝑦𝜓)

Theoremimaiinfv 39997* Indexed intersection of an image. (Contributed by Stefan O'Rear, 22-Feb-2015.)
((𝐹 Fn 𝐴𝐵𝐴) → 𝑥𝐵 (𝐹𝑥) = (𝐹𝐵))