Home | Metamath
Proof Explorer Theorem List (p. 402 of 462) | < 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-28971) |
Hilbert Space Explorer
(28972-30494) |
Users' Mathboxes
(30495-46134) |
Type | Label | Description |
---|---|---|
Statement | ||
Definition | df-prjsp 40101* | 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‘𝑣))𝑥 = (𝑙( ·𝑠 ‘𝑣)𝑦))})) | ||
Theorem | prjspval 40102* | 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 40103* | Utility theorem regarding the relation used in ℙ𝕣𝕠𝕛. (Contributed by Steven Nguyen, 29-Apr-2023.) |
⊢ ∼ = {〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ ∃𝑙 ∈ 𝐾 𝑥 = (𝑙 · 𝑦))} ⇒ ⊢ (𝑋 ∼ 𝑌 ↔ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ ∃𝑚 ∈ 𝐾 𝑋 = (𝑚 · 𝑌))) | ||
Theorem | prjspertr 40104* | The relation in ℙ𝕣𝕠𝕛 is transitive. (Contributed by Steven Nguyen, 1-May-2023.) |
⊢ ∼ = {〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ ∃𝑙 ∈ 𝐾 𝑥 = (𝑙 · 𝑦))} & ⊢ 𝐵 = ((Base‘𝑉) ∖ {(0g‘𝑉)}) & ⊢ 𝑆 = (Scalar‘𝑉) & ⊢ · = ( ·𝑠 ‘𝑉) & ⊢ 𝐾 = (Base‘𝑆) ⇒ ⊢ ((𝑉 ∈ LMod ∧ (𝑋 ∼ 𝑌 ∧ 𝑌 ∼ 𝑍)) → 𝑋 ∼ 𝑍) | ||
Theorem | prjsperref 40105* | The relation in ℙ𝕣𝕠𝕛 is reflexive. (Contributed by Steven Nguyen, 30-Apr-2023.) |
⊢ ∼ = {〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ ∃𝑙 ∈ 𝐾 𝑥 = (𝑙 · 𝑦))} & ⊢ 𝐵 = ((Base‘𝑉) ∖ {(0g‘𝑉)}) & ⊢ 𝑆 = (Scalar‘𝑉) & ⊢ · = ( ·𝑠 ‘𝑉) & ⊢ 𝐾 = (Base‘𝑆) ⇒ ⊢ (𝑉 ∈ LMod → (𝑋 ∈ 𝐵 ↔ 𝑋 ∼ 𝑋)) | ||
Theorem | prjspersym 40106* | The relation in ℙ𝕣𝕠𝕛 is symmetric. (Contributed by Steven Nguyen, 1-May-2023.) |
⊢ ∼ = {〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ ∃𝑙 ∈ 𝐾 𝑥 = (𝑙 · 𝑦))} & ⊢ 𝐵 = ((Base‘𝑉) ∖ {(0g‘𝑉)}) & ⊢ 𝑆 = (Scalar‘𝑉) & ⊢ · = ( ·𝑠 ‘𝑉) & ⊢ 𝐾 = (Base‘𝑆) ⇒ ⊢ ((𝑉 ∈ LVec ∧ 𝑋 ∼ 𝑌) → 𝑌 ∼ 𝑋) | ||
Theorem | prjsper 40107* | The relation used to define ℙ𝕣𝕠𝕛 is an equivalence relation. (Contributed by Steven Nguyen, 1-May-2023.) |
⊢ ∼ = {〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ ∃𝑙 ∈ 𝐾 𝑥 = (𝑙 · 𝑦))} & ⊢ 𝐵 = ((Base‘𝑉) ∖ {(0g‘𝑉)}) & ⊢ 𝑆 = (Scalar‘𝑉) & ⊢ · = ( ·𝑠 ‘𝑉) & ⊢ 𝐾 = (Base‘𝑆) ⇒ ⊢ (𝑉 ∈ LVec → ∼ Er 𝐵) | ||
Theorem | prjspreln0 40108* | 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 40109* | 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 40110* | Two vectors are equivalent iff their spans are equal. (Contributed by Steven Nguyen, 31-May-2023.) |
⊢ ∼ = {〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ ∃𝑙 ∈ 𝐾 𝑥 = (𝑙 · 𝑦))} & ⊢ 𝐵 = ((Base‘𝑉) ∖ {(0g‘𝑉)}) & ⊢ 𝑆 = (Scalar‘𝑉) & ⊢ · = ( ·𝑠 ‘𝑉) & ⊢ 𝐾 = (Base‘𝑆) & ⊢ 𝑁 = (LSpan‘𝑉) ⇒ ⊢ ((𝑉 ∈ LVec ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → (𝑋 ∼ 𝑌 ↔ (𝑁‘{𝑋}) = (𝑁‘{𝑌}))) | ||
Theorem | prjspeclsp 40111* | 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 40112* | Alternate definition of projective space. (Contributed by Steven Nguyen, 7-Jun-2023.) |
⊢ 0 = (0g‘𝑉) & ⊢ 𝐵 = ((Base‘𝑉) ∖ { 0 }) & ⊢ 𝑁 = (LSpan‘𝑉) ⇒ ⊢ (𝑉 ∈ LVec → (ℙ𝕣𝕠𝕛‘𝑉) = ∪ 𝑧 ∈ 𝐵 {((𝑁‘{𝑧}) ∖ { 0 })}) | ||
Syntax | cprjspn 40113 | Extend class notation with the n-dimensional projective space function. |
class ℙ𝕣𝕠𝕛n | ||
Definition | df-prjspn 40114* | 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 24255. 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 40115 | Value of the n-dimensional projective space function. (Contributed by Steven Nguyen, 1-May-2023.) |
⊢ ((𝑁 ∈ ℕ0 ∧ 𝐾 ∈ DivRing) → (𝑁ℙ𝕣𝕠𝕛n𝐾) = (ℙ𝕣𝕠𝕛‘(𝐾 freeLMod (0...𝑁)))) | ||
Theorem | prjspnerlem 40116* | A lemma showing that the equivalence relation used in prjspnval2 40117 and the equivalence relation used in prjspval 40102 are equal, but only with the antecedent 𝐾 ∈ DivRing. (Contributed by SN, 15-Jul-2023.) |
⊢ ∼ = {〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ ∃𝑙 ∈ 𝑆 𝑥 = (𝑙 · 𝑦))} & ⊢ 𝑊 = (𝐾 freeLMod (0...𝑁)) & ⊢ 𝐵 = ((Base‘𝑊) ∖ {(0g‘𝑊)}) & ⊢ 𝑆 = (Base‘𝐾) & ⊢ · = ( ·𝑠 ‘𝑊) ⇒ ⊢ (𝐾 ∈ DivRing → ∼ = {〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ ∃𝑙 ∈ (Base‘(Scalar‘𝑊))𝑥 = (𝑙 · 𝑦))}) | ||
Theorem | prjspnval2 40117* | 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 40118* | The relation used to define ℙ𝕣𝕠𝕛 (and indirectly ℙ𝕣𝕠𝕛n through df-prjspn 40114) is an equivalence relation. This is a lemma that converts the equivalence relation used in results like prjspertr 40104 and prjspersym 40106 (see prjspnerlem 40116). Several theorems are covered in one thanks to the theorems around df-er 8380. (Contributed by SN, 14-Aug-2023.) |
⊢ ∼ = {〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ ∃𝑙 ∈ 𝑆 𝑥 = (𝑙 · 𝑦))} & ⊢ 𝑊 = (𝐾 freeLMod (0...𝑁)) & ⊢ 𝐵 = ((Base‘𝑊) ∖ {(0g‘𝑊)}) & ⊢ 𝑆 = (Base‘𝐾) & ⊢ · = ( ·𝑠 ‘𝑊) & ⊢ (𝜑 → 𝐾 ∈ DivRing) ⇒ ⊢ (𝜑 → ∼ Er 𝐵) | ||
Theorem | prjspnvs 40119* | A nonzero multiple of a vector is equivalent to the vector. This converts the equivalence relation used in prjspvs 40109 (see prjspnerlem 40116). (Contributed by SN, 8-Aug-2024.) |
⊢ ∼ = {〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ ∃𝑙 ∈ 𝑆 𝑥 = (𝑙 · 𝑦))} & ⊢ 𝑊 = (𝐾 freeLMod (0...𝑁)) & ⊢ 𝐵 = ((Base‘𝑊) ∖ {(0g‘𝑊)}) & ⊢ 𝑆 = (Base‘𝐾) & ⊢ · = ( ·𝑠 ‘𝑊) & ⊢ 0 = (0g‘𝐾) & ⊢ (𝜑 → 𝐾 ∈ DivRing) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝐶 ∈ 𝑆) & ⊢ (𝜑 → 𝐶 ≠ 0 ) ⇒ ⊢ (𝜑 → (𝐶 · 𝑋) ∼ 𝑋) | ||
Theorem | 0prjspnlem 40120 | Lemma for 0prjspn 40125. 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 40121* | 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 40122* | 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 40123* | 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 40124* | 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 40125 | A zero-dimensional projective space has only 1 point. (Contributed by Steven Nguyen, 9-Jun-2023.) |
⊢ 𝑊 = (𝐾 freeLMod (0...0)) & ⊢ 𝐵 = ((Base‘𝑊) ∖ {(0g‘𝑊)}) ⇒ ⊢ (𝐾 ∈ DivRing → (0ℙ𝕣𝕠𝕛n𝐾) = {𝐵}) | ||
Theorem | dffltz 40126* | 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 40127 | 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) & ⊢ (𝜑 → ((𝐴↑𝑁) + (𝐵↑𝑁)) = (𝐶↑𝑁)) ⇒ ⊢ (𝜑 → (((𝑆 · 𝐴)↑𝑁) + ((𝑆 · 𝐵)↑𝑁)) = ((𝑆 · 𝐶)↑𝑁)) | ||
Theorem | fltdiv 40128 | 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 40129 | A counterexample for FLT does not exist for 𝑁 = 0. (Contributed by SN, 20-Aug-2024.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ) & ⊢ (𝜑 → 𝑁 ∈ ℕ0) & ⊢ (𝜑 → ((𝐴↑𝑁) + (𝐵↑𝑁)) = (𝐶↑𝑁)) ⇒ ⊢ (𝜑 → 𝑁 ∈ ℕ) | ||
Theorem | fltdvdsabdvdsc 40130 | Any factor of both 𝐴 and 𝐵 also divides 𝐶. This establishes the validity of fltabcoprmex 40131. (Contributed by SN, 21-Aug-2024.) |
⊢ (𝜑 → 𝐴 ∈ ℕ) & ⊢ (𝜑 → 𝐵 ∈ ℕ) & ⊢ (𝜑 → 𝐶 ∈ ℕ) & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → ((𝐴↑𝑁) + (𝐵↑𝑁)) = (𝐶↑𝑁)) ⇒ ⊢ (𝜑 → (𝐴 gcd 𝐵) ∥ 𝐶) | ||
Theorem | fltabcoprmex 40131 | A counterexample to FLT implies a counterexample to FLT with 𝐴, 𝐵 (assigned to 𝐴 / (𝐴 gcd 𝐵) and 𝐵 / (𝐴 gcd 𝐵)) coprime (by divgcdcoprm0 16203). (Contributed by SN, 20-Aug-2024.) |
⊢ (𝜑 → 𝐴 ∈ ℕ) & ⊢ (𝜑 → 𝐵 ∈ ℕ) & ⊢ (𝜑 → 𝐶 ∈ ℕ) & ⊢ (𝜑 → 𝑁 ∈ ℕ0) & ⊢ (𝜑 → ((𝐴↑𝑁) + (𝐵↑𝑁)) = (𝐶↑𝑁)) ⇒ ⊢ (𝜑 → (((𝐴 / (𝐴 gcd 𝐵))↑𝑁) + ((𝐵 / (𝐴 gcd 𝐵))↑𝑁)) = ((𝐶 / (𝐴 gcd 𝐵))↑𝑁)) | ||
Theorem | fltaccoprm 40132 | A counterexample to FLT with 𝐴, 𝐵 coprime also has 𝐴, 𝐶 coprime. (Contributed by SN, 20-Aug-2024.) |
⊢ (𝜑 → 𝐴 ∈ ℕ) & ⊢ (𝜑 → 𝐵 ∈ ℕ) & ⊢ (𝜑 → 𝐶 ∈ ℕ) & ⊢ (𝜑 → 𝑁 ∈ ℕ0) & ⊢ (𝜑 → ((𝐴↑𝑁) + (𝐵↑𝑁)) = (𝐶↑𝑁)) & ⊢ (𝜑 → (𝐴 gcd 𝐵) = 1) ⇒ ⊢ (𝜑 → (𝐴 gcd 𝐶) = 1) | ||
Theorem | fltbccoprm 40133 | A counterexample to FLT with 𝐴, 𝐵 coprime also has 𝐵, 𝐶 coprime. Proven from fltaccoprm 40132 using commutativity of addition. (Contributed by SN, 20-Aug-2024.) |
⊢ (𝜑 → 𝐴 ∈ ℕ) & ⊢ (𝜑 → 𝐵 ∈ ℕ) & ⊢ (𝜑 → 𝐶 ∈ ℕ) & ⊢ (𝜑 → 𝑁 ∈ ℕ0) & ⊢ (𝜑 → ((𝐴↑𝑁) + (𝐵↑𝑁)) = (𝐶↑𝑁)) & ⊢ (𝜑 → (𝐴 gcd 𝐵) = 1) ⇒ ⊢ (𝜑 → (𝐵 gcd 𝐶) = 1) | ||
Theorem | fltabcoprm 40134 | A counterexample to FLT with 𝐴, 𝐶 coprime also has 𝐴, 𝐵 coprime. Converse of fltaccoprm 40132. (Contributed by SN, 22-Aug-2024.) |
⊢ (𝜑 → 𝐴 ∈ ℕ) & ⊢ (𝜑 → 𝐵 ∈ ℕ) & ⊢ (𝜑 → 𝐶 ∈ ℕ) & ⊢ (𝜑 → (𝐴 gcd 𝐶) = 1) & ⊢ (𝜑 → ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2)) ⇒ ⊢ (𝜑 → (𝐴 gcd 𝐵) = 1) | ||
Theorem | infdesc 40135* | 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 40136 | If a counterexample to FLT exists, its addends are not equal. (Contributed by SN, 1-Jun-2023.) |
⊢ (𝜑 → 𝐴 ∈ ℕ) & ⊢ (𝜑 → 𝐵 ∈ ℕ) & ⊢ (𝜑 → 𝐶 ∈ ℕ) & ⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘2)) & ⊢ (𝜑 → ((𝐴↑𝑁) + (𝐵↑𝑁)) = (𝐶↑𝑁)) ⇒ ⊢ (𝜑 → 𝐴 ≠ 𝐵) | ||
Theorem | flt4lem 40137 | Raising a number to the fourth power is equivalent to squaring it twice. (Contributed by SN, 21-Aug-2024.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) ⇒ ⊢ (𝜑 → (𝐴↑4) = ((𝐴↑2)↑2)) | ||
Theorem | flt4lem1 40138 | Satisfy the antecedent used in several pythagtrip 16368 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 40139 | If 𝐴 is even, 𝐵 is odd. (Contributed by SN, 22-Aug-2024.) |
⊢ (𝜑 → 𝐴 ∈ ℕ) & ⊢ (𝜑 → 𝐵 ∈ ℕ) & ⊢ (𝜑 → 𝐶 ∈ ℕ) & ⊢ (𝜑 → 2 ∥ 𝐴) & ⊢ (𝜑 → (𝐴 gcd 𝐶) = 1) & ⊢ (𝜑 → ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2)) ⇒ ⊢ (𝜑 → ¬ 2 ∥ 𝐵) | ||
Theorem | flt4lem3 40140 | Equivalent to pythagtriplem4 16353. Show that 𝐶 + 𝐴 and 𝐶 − 𝐴 are coprime. (Contributed by SN, 22-Aug-2024.) |
⊢ (𝜑 → 𝐴 ∈ ℕ) & ⊢ (𝜑 → 𝐵 ∈ ℕ) & ⊢ (𝜑 → 𝐶 ∈ ℕ) & ⊢ (𝜑 → 2 ∥ 𝐴) & ⊢ (𝜑 → (𝐴 gcd 𝐶) = 1) & ⊢ (𝜑 → ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2)) ⇒ ⊢ (𝜑 → ((𝐶 + 𝐴) gcd (𝐶 − 𝐴)) = 1) | ||
Theorem | flt4lem4 40141 | 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 40142 | In the context of the lemmas of pythagtrip 16368, 𝑀 and 𝑁 are coprime. (Contributed by SN, 23-Aug-2024.) |
⊢ 𝑀 = (((√‘(𝐶 + 𝐵)) + (√‘(𝐶 − 𝐵))) / 2) & ⊢ 𝑁 = (((√‘(𝐶 + 𝐵)) − (√‘(𝐶 − 𝐵))) / 2) ⇒ ⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2) ∧ ((𝐴 gcd 𝐵) = 1 ∧ ¬ 2 ∥ 𝐴)) → (𝑀 gcd 𝑁) = 1) | ||
Theorem | flt4lem5elem 40143 | Version of fltaccoprm 40132 and fltbccoprm 40133 where 𝑀 is not squared. This can be proved in general for any polynomial in three variables: using prmdvdsncoprmbd 16264, dvds2addd 15834, and prmdvdsexp 16253, 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 40144 | 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 40145 | 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 40146 | 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 40147 | 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 40148 | Satisfy the hypotheses of flt4lem4 40141. 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) ∈ ℕ))) | ||
Theorem | flt4lem5f 40149 | 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 40150 | 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 40151* | Convert flt4lem5f 40149 into a convenient form for nna4b4nsq 40152. 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))) ∧ 𝑙 < 𝐶)) | ||
Theorem | nna4b4nsq 40152 | 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 40153 | (𝐶↑𝑁) is the largest term and therefore 𝐵 < 𝐶. (Contributed by Steven Nguyen, 22-Aug-2023.) |
⊢ (𝜑 → 𝐴 ∈ ℕ) & ⊢ (𝜑 → 𝐵 ∈ ℕ) & ⊢ (𝜑 → 𝐶 ∈ ℕ) & ⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘3)) & ⊢ (𝜑 → ((𝐴↑𝑁) + (𝐵↑𝑁)) = (𝐶↑𝑁)) ⇒ ⊢ (𝜑 → 𝐵 < 𝐶) | ||
Theorem | fltnltalem 40154 | Lemma for fltnlta 40155. A lower bound for 𝐴 based on pwdif 15413. (Contributed by Steven Nguyen, 22-Aug-2023.) |
⊢ (𝜑 → 𝐴 ∈ ℕ) & ⊢ (𝜑 → 𝐵 ∈ ℕ) & ⊢ (𝜑 → 𝐶 ∈ ℕ) & ⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘3)) & ⊢ (𝜑 → ((𝐴↑𝑁) + (𝐵↑𝑁)) = (𝐶↑𝑁)) ⇒ ⊢ (𝜑 → ((𝐶 − 𝐵) · ((𝐶↑(𝑁 − 1)) + ((𝑁 − 1) · (𝐵↑(𝑁 − 1))))) < (𝐴↑𝑁)) | ||
Theorem | fltnlta 40155 | 𝑁 is less than 𝐴. See https://www.youtu.be/EymVXkPWxyc for an outline. (Contributed by Steven Nguyen, 24-Aug-2023.) |
⊢ (𝜑 → 𝐴 ∈ ℕ) & ⊢ (𝜑 → 𝐵 ∈ ℕ) & ⊢ (𝜑 → 𝐶 ∈ ℕ) & ⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘3)) & ⊢ (𝜑 → ((𝐴↑𝑁) + (𝐵↑𝑁)) = (𝐶↑𝑁)) & ⊢ (𝜑 → 𝐴 < 𝐵) ⇒ ⊢ (𝜑 → 𝑁 < 𝐴) | ||
Theorem | binom2d 40156 | Deduction form of binom2. (Contributed by Igor Ieskov, 14-Dec-2023.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) ⇒ ⊢ (𝜑 → ((𝐴 + 𝐵)↑2) = (((𝐴↑2) + (2 · (𝐴 · 𝐵))) + (𝐵↑2))) | ||
Theorem | cu3addd 40157 | 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 40158 | The square of the negative of a number. (Contributed by Igor Ieskov, 21-Jan-2024.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) ⇒ ⊢ (𝜑 → (-𝐴↑2) = (𝐴↑2)) | ||
Theorem | negexpidd 40159 | 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 40160* | An extended version of rexlimdvv 3205 to include three set variables. (Contributed by Igor Ieskov, 21-Jan-2024.) |
⊢ (𝜑 → ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐶) → (𝜓 → 𝜒))) ⇒ ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 ∃𝑧 ∈ 𝐶 𝜓 → 𝜒)) | ||
Theorem | 3cubeslem1 40161 | Lemma for 3cubes 40167. (Contributed by Igor Ieskov, 22-Jan-2024.) |
⊢ (𝜑 → 𝐴 ∈ ℚ) ⇒ ⊢ (𝜑 → 0 < (((𝐴 + 1)↑2) − 𝐴)) | ||
Theorem | 3cubeslem2 40162 | Lemma for 3cubes 40167. Used to show that the denominators in 3cubeslem4 40166 are nonzero. (Contributed by Igor Ieskov, 22-Jan-2024.) |
⊢ (𝜑 → 𝐴 ∈ ℚ) ⇒ ⊢ (𝜑 → ¬ ((((3↑3) · (𝐴↑2)) + ((3↑2) · 𝐴)) + 3) = 0) | ||
Theorem | 3cubeslem3l 40163 | Lemma for 3cubes 40167. (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 40164 | Lemma for 3cubes 40167. (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 40165 | Lemma for 3cubes 40167. (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 40166 | Lemma for 3cubes 40167. 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 40167* | 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))) | ||
Theorem | rntrclfvOAI 40168 | The range of the transitive closure is equal to the range of the relation. (Contributed by OpenAI, 7-Jul-2020.) |
⊢ (𝑅 ∈ 𝑉 → ran (t+‘𝑅) = ran 𝑅) | ||
Theorem | moxfr 40169* | Transfer at-most-one between related expressions. (Contributed by Stefan O'Rear, 12-Feb-2015.) |
⊢ 𝐴 ∈ V & ⊢ ∃!𝑦 𝑥 = 𝐴 & ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∃*𝑥𝜑 ↔ ∃*𝑦𝜓) | ||
Theorem | imaiinfv 40170* | Indexed intersection of an image. (Contributed by Stefan O'Rear, 22-Feb-2015.) |
⊢ ((𝐹 Fn 𝐴 ∧ 𝐵 ⊆ 𝐴) → ∩ 𝑥 ∈ 𝐵 (𝐹‘𝑥) = ∩ (𝐹 “ 𝐵)) | ||
Theorem | elrfi 40171* | Elementhood in a set of relative finite intersections. (Contributed by Stefan O'Rear, 22-Feb-2015.) |
⊢ ((𝐵 ∈ 𝑉 ∧ 𝐶 ⊆ 𝒫 𝐵) → (𝐴 ∈ (fi‘({𝐵} ∪ 𝐶)) ↔ ∃𝑣 ∈ (𝒫 𝐶 ∩ Fin)𝐴 = (𝐵 ∩ ∩ 𝑣))) | ||
Theorem | elrfirn 40172* | Elementhood in a set of relative finite intersections of an indexed family of sets. (Contributed by Stefan O'Rear, 22-Feb-2015.) |
⊢ ((𝐵 ∈ 𝑉 ∧ 𝐹:𝐼⟶𝒫 𝐵) → (𝐴 ∈ (fi‘({𝐵} ∪ ran 𝐹)) ↔ ∃𝑣 ∈ (𝒫 𝐼 ∩ Fin)𝐴 = (𝐵 ∩ ∩ 𝑦 ∈ 𝑣 (𝐹‘𝑦)))) | ||
Theorem | elrfirn2 40173* | Elementhood in a set of relative finite intersections of an indexed family of sets (implicit). (Contributed by Stefan O'Rear, 22-Feb-2015.) |
⊢ ((𝐵 ∈ 𝑉 ∧ ∀𝑦 ∈ 𝐼 𝐶 ⊆ 𝐵) → (𝐴 ∈ (fi‘({𝐵} ∪ ran (𝑦 ∈ 𝐼 ↦ 𝐶))) ↔ ∃𝑣 ∈ (𝒫 𝐼 ∩ Fin)𝐴 = (𝐵 ∩ ∩ 𝑦 ∈ 𝑣 𝐶))) | ||
Theorem | cmpfiiin 40174* | In a compact topology, a system of closed sets with nonempty finite intersections has a nonempty intersection. (Contributed by Stefan O'Rear, 22-Feb-2015.) |
⊢ 𝑋 = ∪ 𝐽 & ⊢ (𝜑 → 𝐽 ∈ Comp) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐼) → 𝑆 ∈ (Clsd‘𝐽)) & ⊢ ((𝜑 ∧ (𝑙 ⊆ 𝐼 ∧ 𝑙 ∈ Fin)) → (𝑋 ∩ ∩ 𝑘 ∈ 𝑙 𝑆) ≠ ∅) ⇒ ⊢ (𝜑 → (𝑋 ∩ ∩ 𝑘 ∈ 𝐼 𝑆) ≠ ∅) | ||
Theorem | ismrcd1 40175* | Any function from the subsets of a set to itself, which is extensive (satisfies mrcssid 17092), isotone (satisfies mrcss 17091), and idempotent (satisfies mrcidm 17094) has a collection of fixed points which is a Moore collection, and itself is the closure operator for that collection. This can be taken as an alternate definition for the closure operators. This is the first half, ismrcd2 40176 is the second. (Contributed by Stefan O'Rear, 1-Feb-2015.) |
⊢ (𝜑 → 𝐵 ∈ 𝑉) & ⊢ (𝜑 → 𝐹:𝒫 𝐵⟶𝒫 𝐵) & ⊢ ((𝜑 ∧ 𝑥 ⊆ 𝐵) → 𝑥 ⊆ (𝐹‘𝑥)) & ⊢ ((𝜑 ∧ 𝑥 ⊆ 𝐵 ∧ 𝑦 ⊆ 𝑥) → (𝐹‘𝑦) ⊆ (𝐹‘𝑥)) & ⊢ ((𝜑 ∧ 𝑥 ⊆ 𝐵) → (𝐹‘(𝐹‘𝑥)) = (𝐹‘𝑥)) ⇒ ⊢ (𝜑 → dom (𝐹 ∩ I ) ∈ (Moore‘𝐵)) | ||
Theorem | ismrcd2 40176* | Second half of ismrcd1 40175. (Contributed by Stefan O'Rear, 1-Feb-2015.) |
⊢ (𝜑 → 𝐵 ∈ 𝑉) & ⊢ (𝜑 → 𝐹:𝒫 𝐵⟶𝒫 𝐵) & ⊢ ((𝜑 ∧ 𝑥 ⊆ 𝐵) → 𝑥 ⊆ (𝐹‘𝑥)) & ⊢ ((𝜑 ∧ 𝑥 ⊆ 𝐵 ∧ 𝑦 ⊆ 𝑥) → (𝐹‘𝑦) ⊆ (𝐹‘𝑥)) & ⊢ ((𝜑 ∧ 𝑥 ⊆ 𝐵) → (𝐹‘(𝐹‘𝑥)) = (𝐹‘𝑥)) ⇒ ⊢ (𝜑 → 𝐹 = (mrCls‘dom (𝐹 ∩ I ))) | ||
Theorem | istopclsd 40177* | A closure function which satisfies sscls 21925, clsidm 21936, cls0 21949, and clsun 34211 defines a (unique) topology which it is the closure function on. (Contributed by Stefan O'Rear, 1-Feb-2015.) |
⊢ (𝜑 → 𝐵 ∈ 𝑉) & ⊢ (𝜑 → 𝐹:𝒫 𝐵⟶𝒫 𝐵) & ⊢ ((𝜑 ∧ 𝑥 ⊆ 𝐵) → 𝑥 ⊆ (𝐹‘𝑥)) & ⊢ ((𝜑 ∧ 𝑥 ⊆ 𝐵) → (𝐹‘(𝐹‘𝑥)) = (𝐹‘𝑥)) & ⊢ (𝜑 → (𝐹‘∅) = ∅) & ⊢ ((𝜑 ∧ 𝑥 ⊆ 𝐵 ∧ 𝑦 ⊆ 𝐵) → (𝐹‘(𝑥 ∪ 𝑦)) = ((𝐹‘𝑥) ∪ (𝐹‘𝑦))) & ⊢ 𝐽 = {𝑧 ∈ 𝒫 𝐵 ∣ (𝐹‘(𝐵 ∖ 𝑧)) = (𝐵 ∖ 𝑧)} ⇒ ⊢ (𝜑 → (𝐽 ∈ (TopOn‘𝐵) ∧ (cls‘𝐽) = 𝐹)) | ||
Theorem | ismrc 40178* | A function is a Moore closure operator iff it satisfies mrcssid 17092, mrcss 17091, and mrcidm 17094. (Contributed by Stefan O'Rear, 1-Feb-2015.) |
⊢ (𝐹 ∈ (mrCls “ (Moore‘𝐵)) ↔ (𝐵 ∈ V ∧ 𝐹:𝒫 𝐵⟶𝒫 𝐵 ∧ ∀𝑥∀𝑦((𝑥 ⊆ 𝐵 ∧ 𝑦 ⊆ 𝑥) → (𝑥 ⊆ (𝐹‘𝑥) ∧ (𝐹‘𝑦) ⊆ (𝐹‘𝑥) ∧ (𝐹‘(𝐹‘𝑥)) = (𝐹‘𝑥))))) | ||
Syntax | cnacs 40179 | Class of Noetherian closure systems. |
class NoeACS | ||
Definition | df-nacs 40180* | Define a closure system of Noetherian type (not standard terminology) as an algebraic system where all closed sets are finitely generated. (Contributed by Stefan O'Rear, 4-Apr-2015.) |
⊢ NoeACS = (𝑥 ∈ V ↦ {𝑐 ∈ (ACS‘𝑥) ∣ ∀𝑠 ∈ 𝑐 ∃𝑔 ∈ (𝒫 𝑥 ∩ Fin)𝑠 = ((mrCls‘𝑐)‘𝑔)}) | ||
Theorem | isnacs 40181* | Expand definition of Noetherian-type closure system. (Contributed by Stefan O'Rear, 4-Apr-2015.) |
⊢ 𝐹 = (mrCls‘𝐶) ⇒ ⊢ (𝐶 ∈ (NoeACS‘𝑋) ↔ (𝐶 ∈ (ACS‘𝑋) ∧ ∀𝑠 ∈ 𝐶 ∃𝑔 ∈ (𝒫 𝑋 ∩ Fin)𝑠 = (𝐹‘𝑔))) | ||
Theorem | nacsfg 40182* | In a Noetherian-type closure system, all closed sets are finitely generated. (Contributed by Stefan O'Rear, 4-Apr-2015.) |
⊢ 𝐹 = (mrCls‘𝐶) ⇒ ⊢ ((𝐶 ∈ (NoeACS‘𝑋) ∧ 𝑆 ∈ 𝐶) → ∃𝑔 ∈ (𝒫 𝑋 ∩ Fin)𝑆 = (𝐹‘𝑔)) | ||
Theorem | isnacs2 40183 | Express Noetherian-type closure system with fewer quantifiers. (Contributed by Stefan O'Rear, 4-Apr-2015.) |
⊢ 𝐹 = (mrCls‘𝐶) ⇒ ⊢ (𝐶 ∈ (NoeACS‘𝑋) ↔ (𝐶 ∈ (ACS‘𝑋) ∧ (𝐹 “ (𝒫 𝑋 ∩ Fin)) = 𝐶)) | ||
Theorem | mrefg2 40184* | Slight variation on finite generation for closure systems. (Contributed by Stefan O'Rear, 4-Apr-2015.) |
⊢ 𝐹 = (mrCls‘𝐶) ⇒ ⊢ (𝐶 ∈ (Moore‘𝑋) → (∃𝑔 ∈ (𝒫 𝑋 ∩ Fin)𝑆 = (𝐹‘𝑔) ↔ ∃𝑔 ∈ (𝒫 𝑆 ∩ Fin)𝑆 = (𝐹‘𝑔))) | ||
Theorem | mrefg3 40185* | Slight variation on finite generation for closure systems. (Contributed by Stefan O'Rear, 4-Apr-2015.) |
⊢ 𝐹 = (mrCls‘𝐶) ⇒ ⊢ ((𝐶 ∈ (Moore‘𝑋) ∧ 𝑆 ∈ 𝐶) → (∃𝑔 ∈ (𝒫 𝑋 ∩ Fin)𝑆 = (𝐹‘𝑔) ↔ ∃𝑔 ∈ (𝒫 𝑆 ∩ Fin)𝑆 ⊆ (𝐹‘𝑔))) | ||
Theorem | nacsacs 40186 | A closure system of Noetherian type is algebraic. (Contributed by Stefan O'Rear, 4-Apr-2015.) |
⊢ (𝐶 ∈ (NoeACS‘𝑋) → 𝐶 ∈ (ACS‘𝑋)) | ||
Theorem | isnacs3 40187* | A choice-free order equivalent to the Noetherian condition on a closure system. (Contributed by Stefan O'Rear, 4-Apr-2015.) |
⊢ (𝐶 ∈ (NoeACS‘𝑋) ↔ (𝐶 ∈ (Moore‘𝑋) ∧ ∀𝑠 ∈ 𝒫 𝐶((toInc‘𝑠) ∈ Dirset → ∪ 𝑠 ∈ 𝑠))) | ||
Theorem | incssnn0 40188* | Transitivity induction of subsets, lemma for nacsfix 40189. (Contributed by Stefan O'Rear, 4-Apr-2015.) |
⊢ ((∀𝑥 ∈ ℕ0 (𝐹‘𝑥) ⊆ (𝐹‘(𝑥 + 1)) ∧ 𝐴 ∈ ℕ0 ∧ 𝐵 ∈ (ℤ≥‘𝐴)) → (𝐹‘𝐴) ⊆ (𝐹‘𝐵)) | ||
Theorem | nacsfix 40189* | An increasing sequence of closed sets in a Noetherian-type closure system eventually fixates. (Contributed by Stefan O'Rear, 4-Apr-2015.) |
⊢ ((𝐶 ∈ (NoeACS‘𝑋) ∧ 𝐹:ℕ0⟶𝐶 ∧ ∀𝑥 ∈ ℕ0 (𝐹‘𝑥) ⊆ (𝐹‘(𝑥 + 1))) → ∃𝑦 ∈ ℕ0 ∀𝑧 ∈ (ℤ≥‘𝑦)(𝐹‘𝑧) = (𝐹‘𝑦)) | ||
Theorem | constmap 40190 |
A constant (represented without dummy variables) is an element of a
function set.
Note: In the following development, we will be quite often quantifying over functions and points in N-dimensional space (which are equivalent to functions from an "index set"). Many of the following theorems exist to transfer standard facts about functions to elements of function sets. (Contributed by Stefan O'Rear, 30-Aug-2014.) (Revised by Stefan O'Rear, 5-May-2015.) |
⊢ 𝐴 ∈ V & ⊢ 𝐶 ∈ V ⇒ ⊢ (𝐵 ∈ 𝐶 → (𝐴 × {𝐵}) ∈ (𝐶 ↑m 𝐴)) | ||
Theorem | mapco2g 40191 | Renaming indices in a tuple, with sethood as antecedents. (Contributed by Stefan O'Rear, 9-Oct-2014.) (Revised by Mario Carneiro, 5-May-2015.) |
⊢ ((𝐸 ∈ V ∧ 𝐴 ∈ (𝐵 ↑m 𝐶) ∧ 𝐷:𝐸⟶𝐶) → (𝐴 ∘ 𝐷) ∈ (𝐵 ↑m 𝐸)) | ||
Theorem | mapco2 40192 | Post-composition (renaming indices) of a mapping viewed as a point. (Contributed by Stefan O'Rear, 5-Oct-2014.) (Revised by Stefan O'Rear, 5-May-2015.) |
⊢ 𝐸 ∈ V ⇒ ⊢ ((𝐴 ∈ (𝐵 ↑m 𝐶) ∧ 𝐷:𝐸⟶𝐶) → (𝐴 ∘ 𝐷) ∈ (𝐵 ↑m 𝐸)) | ||
Theorem | mapfzcons 40193 | Extending a one-based mapping by adding a tuple at the end results in another mapping. (Contributed by Stefan O'Rear, 10-Oct-2014.) (Revised by Stefan O'Rear, 5-May-2015.) |
⊢ 𝑀 = (𝑁 + 1) ⇒ ⊢ ((𝑁 ∈ ℕ0 ∧ 𝐴 ∈ (𝐵 ↑m (1...𝑁)) ∧ 𝐶 ∈ 𝐵) → (𝐴 ∪ {〈𝑀, 𝐶〉}) ∈ (𝐵 ↑m (1...𝑀))) | ||
Theorem | mapfzcons1 40194 | Recover prefix mapping from an extended mapping. (Contributed by Stefan O'Rear, 10-Oct-2014.) (Revised by Stefan O'Rear, 5-May-2015.) |
⊢ 𝑀 = (𝑁 + 1) ⇒ ⊢ (𝐴 ∈ (𝐵 ↑m (1...𝑁)) → ((𝐴 ∪ {〈𝑀, 𝐶〉}) ↾ (1...𝑁)) = 𝐴) | ||
Theorem | mapfzcons1cl 40195 | A nonempty mapping has a prefix. (Contributed by Stefan O'Rear, 10-Oct-2014.) (Revised by Stefan O'Rear, 5-May-2015.) |
⊢ 𝑀 = (𝑁 + 1) ⇒ ⊢ (𝐴 ∈ (𝐵 ↑m (1...𝑀)) → (𝐴 ↾ (1...𝑁)) ∈ (𝐵 ↑m (1...𝑁))) | ||
Theorem | mapfzcons2 40196 | Recover added element from an extended mapping. (Contributed by Stefan O'Rear, 10-Oct-2014.) (Revised by Stefan O'Rear, 5-May-2015.) |
⊢ 𝑀 = (𝑁 + 1) ⇒ ⊢ ((𝐴 ∈ (𝐵 ↑m (1...𝑁)) ∧ 𝐶 ∈ 𝐵) → ((𝐴 ∪ {〈𝑀, 𝐶〉})‘𝑀) = 𝐶) | ||
Theorem | mptfcl 40197* | Interpret range of a maps-to notation as a constraint on the definition. (Contributed by Stefan O'Rear, 10-Oct-2014.) |
⊢ ((𝑡 ∈ 𝐴 ↦ 𝐵):𝐴⟶𝐶 → (𝑡 ∈ 𝐴 → 𝐵 ∈ 𝐶)) | ||
Syntax | cmzpcl 40198 | Extend class notation to include pre-polynomial rings. |
class mzPolyCld | ||
Syntax | cmzp 40199 | Extend class notation to include polynomial rings. |
class mzPoly | ||
Definition | df-mzpcl 40200* | Define the polynomially closed function rings over an arbitrary index set 𝑣. The set (mzPolyCld‘𝑣) contains all sets of functions from (ℤ ↑m 𝑣) to ℤ which include all constants and projections and are closed under addition and multiplication. This is a "temporary" set used to define the polynomial function ring itself (mzPoly‘𝑣); see df-mzp 40201. (Contributed by Stefan O'Rear, 4-Oct-2014.) |
⊢ mzPolyCld = (𝑣 ∈ V ↦ {𝑝 ∈ 𝒫 (ℤ ↑m (ℤ ↑m 𝑣)) ∣ ((∀𝑖 ∈ ℤ ((ℤ ↑m 𝑣) × {𝑖}) ∈ 𝑝 ∧ ∀𝑗 ∈ 𝑣 (𝑥 ∈ (ℤ ↑m 𝑣) ↦ (𝑥‘𝑗)) ∈ 𝑝) ∧ ∀𝑓 ∈ 𝑝 ∀𝑔 ∈ 𝑝 ((𝑓 ∘f + 𝑔) ∈ 𝑝 ∧ (𝑓 ∘f · 𝑔) ∈ 𝑝))}) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |