![]() |
Metamath
Proof Explorer Theorem List (p. 427 of 491) | < 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: | ![]() (1-30946) |
![]() (30947-32469) |
![]() (32470-49035) |
Type | Label | Description |
---|---|---|
Statement | ||
Definition | df-prjspn 42601* | 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 25433. 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 42602 | Value of the n-dimensional projective space function. (Contributed by Steven Nguyen, 1-May-2023.) |
⊢ ((𝑁 ∈ ℕ0 ∧ 𝐾 ∈ DivRing) → (𝑁ℙ𝕣𝕠𝕛n𝐾) = (ℙ𝕣𝕠𝕛‘(𝐾 freeLMod (0...𝑁)))) | ||
Theorem | prjspnerlem 42603* | A lemma showing that the equivalence relation used in prjspnval2 42604 and the equivalence relation used in prjspval 42589 are equal, but only with the antecedent 𝐾 ∈ DivRing. (Contributed by SN, 15-Jul-2023.) |
⊢ ∼ = {〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ ∃𝑙 ∈ 𝑆 𝑥 = (𝑙 · 𝑦))} & ⊢ 𝑊 = (𝐾 freeLMod (0...𝑁)) & ⊢ 𝐵 = ((Base‘𝑊) ∖ {(0g‘𝑊)}) & ⊢ 𝑆 = (Base‘𝐾) & ⊢ · = ( ·𝑠 ‘𝑊) ⇒ ⊢ (𝐾 ∈ DivRing → ∼ = {〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ ∃𝑙 ∈ (Base‘(Scalar‘𝑊))𝑥 = (𝑙 · 𝑦))}) | ||
Theorem | prjspnval2 42604* | 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 42605* | The relation used to define ℙ𝕣𝕠𝕛 (and indirectly ℙ𝕣𝕠𝕛n through df-prjspn 42601) is an equivalence relation. This is a lemma that converts the equivalence relation used in results like prjspertr 42591 and prjspersym 42593 (see prjspnerlem 42603). Several theorems are covered in one thanks to the theorems around df-er 8743. (Contributed by SN, 14-Aug-2023.) |
⊢ ∼ = {〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ ∃𝑙 ∈ 𝑆 𝑥 = (𝑙 · 𝑦))} & ⊢ 𝑊 = (𝐾 freeLMod (0...𝑁)) & ⊢ 𝐵 = ((Base‘𝑊) ∖ {(0g‘𝑊)}) & ⊢ 𝑆 = (Base‘𝐾) & ⊢ · = ( ·𝑠 ‘𝑊) & ⊢ (𝜑 → 𝐾 ∈ DivRing) ⇒ ⊢ (𝜑 → ∼ Er 𝐵) | ||
Theorem | prjspnvs 42606* | A nonzero multiple of a vector is equivalent to the vector. This converts the equivalence relation used in prjspvs 42596 (see prjspnerlem 42603). (Contributed by SN, 8-Aug-2024.) |
⊢ ∼ = {〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ ∃𝑙 ∈ 𝑆 𝑥 = (𝑙 · 𝑦))} & ⊢ 𝑊 = (𝐾 freeLMod (0...𝑁)) & ⊢ 𝐵 = ((Base‘𝑊) ∖ {(0g‘𝑊)}) & ⊢ 𝑆 = (Base‘𝐾) & ⊢ · = ( ·𝑠 ‘𝑊) & ⊢ 0 = (0g‘𝐾) & ⊢ (𝜑 → 𝐾 ∈ DivRing) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝐶 ∈ 𝑆) & ⊢ (𝜑 → 𝐶 ≠ 0 ) ⇒ ⊢ (𝜑 → (𝐶 · 𝑋) ∼ 𝑋) | ||
Theorem | prjspnssbas 42607 | 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 42608 | A projective point is nonempty. (Contributed by SN, 17-Jan-2025.) |
⊢ 𝑃 = (𝑁ℙ𝕣𝕠𝕛n𝐾) & ⊢ 𝑊 = (𝐾 freeLMod (0...𝑁)) & ⊢ 𝐵 = ((Base‘𝑊) ∖ {(0g‘𝑊)}) & ⊢ (𝜑 → 𝑁 ∈ ℕ0) & ⊢ (𝜑 → 𝐾 ∈ DivRing) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) ⇒ ⊢ (𝜑 → 𝐴 ≠ ∅) | ||
Theorem | 0prjspnlem 42609 | Lemma for 0prjspn 42614. 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 42610* | 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 42611* | 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 42612* | 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 42613* | 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 42614 | 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 42615 | Extend class notation with the projective curve function. |
class ℙ𝕣𝕠𝕛Crv | ||
Definition | df-prjcrv 42616* | 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 42586 and prjspvs 42596). (Contributed by SN, 23-Nov-2024.) |
⊢ ℙ𝕣𝕠𝕛Crv = (𝑛 ∈ ℕ0, 𝑘 ∈ Field ↦ (𝑓 ∈ ∪ ran ((0...𝑛) mHomP 𝑘) ↦ {𝑝 ∈ (𝑛ℙ𝕣𝕠𝕛n𝑘) ∣ ((((0...𝑛) eval 𝑘)‘𝑓) “ 𝑝) = {(0g‘𝑘)}})) | ||
Theorem | prjcrvfval 42617* | 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 42618* | 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 42619 | 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 ) = 𝑃) | ||
Theorem | dffltz 42620* | 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 42621 | 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 42622 | 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 42623 | A counterexample for FLT does not exist for 𝑁 = 0. (Contributed by SN, 20-Aug-2024.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ) & ⊢ (𝜑 → 𝑁 ∈ ℕ0) & ⊢ (𝜑 → ((𝐴↑𝑁) + (𝐵↑𝑁)) = (𝐶↑𝑁)) ⇒ ⊢ (𝜑 → 𝑁 ∈ ℕ) | ||
Theorem | fltdvdsabdvdsc 42624 | Any factor of both 𝐴 and 𝐵 also divides 𝐶. This establishes the validity of fltabcoprmex 42625. (Contributed by SN, 21-Aug-2024.) |
⊢ (𝜑 → 𝐴 ∈ ℕ) & ⊢ (𝜑 → 𝐵 ∈ ℕ) & ⊢ (𝜑 → 𝐶 ∈ ℕ) & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → ((𝐴↑𝑁) + (𝐵↑𝑁)) = (𝐶↑𝑁)) ⇒ ⊢ (𝜑 → (𝐴 gcd 𝐵) ∥ 𝐶) | ||
Theorem | fltabcoprmex 42625 | A counterexample to FLT implies a counterexample to FLT with 𝐴, 𝐵 (assigned to 𝐴 / (𝐴 gcd 𝐵) and 𝐵 / (𝐴 gcd 𝐵)) coprime (by divgcdcoprm0 16698). (Contributed by SN, 20-Aug-2024.) |
⊢ (𝜑 → 𝐴 ∈ ℕ) & ⊢ (𝜑 → 𝐵 ∈ ℕ) & ⊢ (𝜑 → 𝐶 ∈ ℕ) & ⊢ (𝜑 → 𝑁 ∈ ℕ0) & ⊢ (𝜑 → ((𝐴↑𝑁) + (𝐵↑𝑁)) = (𝐶↑𝑁)) ⇒ ⊢ (𝜑 → (((𝐴 / (𝐴 gcd 𝐵))↑𝑁) + ((𝐵 / (𝐴 gcd 𝐵))↑𝑁)) = ((𝐶 / (𝐴 gcd 𝐵))↑𝑁)) | ||
Theorem | fltaccoprm 42626 | A counterexample to FLT with 𝐴, 𝐵 coprime also has 𝐴, 𝐶 coprime. (Contributed by SN, 20-Aug-2024.) |
⊢ (𝜑 → 𝐴 ∈ ℕ) & ⊢ (𝜑 → 𝐵 ∈ ℕ) & ⊢ (𝜑 → 𝐶 ∈ ℕ) & ⊢ (𝜑 → 𝑁 ∈ ℕ0) & ⊢ (𝜑 → ((𝐴↑𝑁) + (𝐵↑𝑁)) = (𝐶↑𝑁)) & ⊢ (𝜑 → (𝐴 gcd 𝐵) = 1) ⇒ ⊢ (𝜑 → (𝐴 gcd 𝐶) = 1) | ||
Theorem | fltbccoprm 42627 | A counterexample to FLT with 𝐴, 𝐵 coprime also has 𝐵, 𝐶 coprime. Proven from fltaccoprm 42626 using commutativity of addition. (Contributed by SN, 20-Aug-2024.) |
⊢ (𝜑 → 𝐴 ∈ ℕ) & ⊢ (𝜑 → 𝐵 ∈ ℕ) & ⊢ (𝜑 → 𝐶 ∈ ℕ) & ⊢ (𝜑 → 𝑁 ∈ ℕ0) & ⊢ (𝜑 → ((𝐴↑𝑁) + (𝐵↑𝑁)) = (𝐶↑𝑁)) & ⊢ (𝜑 → (𝐴 gcd 𝐵) = 1) ⇒ ⊢ (𝜑 → (𝐵 gcd 𝐶) = 1) | ||
Theorem | fltabcoprm 42628 | A counterexample to FLT with 𝐴, 𝐶 coprime also has 𝐴, 𝐵 coprime. Converse of fltaccoprm 42626. (Contributed by SN, 22-Aug-2024.) |
⊢ (𝜑 → 𝐴 ∈ ℕ) & ⊢ (𝜑 → 𝐵 ∈ ℕ) & ⊢ (𝜑 → 𝐶 ∈ ℕ) & ⊢ (𝜑 → (𝐴 gcd 𝐶) = 1) & ⊢ (𝜑 → ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2)) ⇒ ⊢ (𝜑 → (𝐴 gcd 𝐵) = 1) | ||
Theorem | infdesc 42629* | 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 42630 | If a counterexample to FLT exists, its addends are not equal. (Contributed by SN, 1-Jun-2023.) |
⊢ (𝜑 → 𝐴 ∈ ℕ) & ⊢ (𝜑 → 𝐵 ∈ ℕ) & ⊢ (𝜑 → 𝐶 ∈ ℕ) & ⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘2)) & ⊢ (𝜑 → ((𝐴↑𝑁) + (𝐵↑𝑁)) = (𝐶↑𝑁)) ⇒ ⊢ (𝜑 → 𝐴 ≠ 𝐵) | ||
Theorem | flt4lem 42631 | Raising a number to the fourth power is equivalent to squaring it twice. (Contributed by SN, 21-Aug-2024.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) ⇒ ⊢ (𝜑 → (𝐴↑4) = ((𝐴↑2)↑2)) | ||
Theorem | flt4lem1 42632 | Satisfy the antecedent used in several pythagtrip 16867 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 42633 | If 𝐴 is even, 𝐵 is odd. (Contributed by SN, 22-Aug-2024.) |
⊢ (𝜑 → 𝐴 ∈ ℕ) & ⊢ (𝜑 → 𝐵 ∈ ℕ) & ⊢ (𝜑 → 𝐶 ∈ ℕ) & ⊢ (𝜑 → 2 ∥ 𝐴) & ⊢ (𝜑 → (𝐴 gcd 𝐶) = 1) & ⊢ (𝜑 → ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2)) ⇒ ⊢ (𝜑 → ¬ 2 ∥ 𝐵) | ||
Theorem | flt4lem3 42634 | Equivalent to pythagtriplem4 16852. Show that 𝐶 + 𝐴 and 𝐶 − 𝐴 are coprime. (Contributed by SN, 22-Aug-2024.) |
⊢ (𝜑 → 𝐴 ∈ ℕ) & ⊢ (𝜑 → 𝐵 ∈ ℕ) & ⊢ (𝜑 → 𝐶 ∈ ℕ) & ⊢ (𝜑 → 2 ∥ 𝐴) & ⊢ (𝜑 → (𝐴 gcd 𝐶) = 1) & ⊢ (𝜑 → ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2)) ⇒ ⊢ (𝜑 → ((𝐶 + 𝐴) gcd (𝐶 − 𝐴)) = 1) | ||
Theorem | flt4lem4 42635 | 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 42636 | In the context of the lemmas of pythagtrip 16867, 𝑀 and 𝑁 are coprime. (Contributed by SN, 23-Aug-2024.) |
⊢ 𝑀 = (((√‘(𝐶 + 𝐵)) + (√‘(𝐶 − 𝐵))) / 2) & ⊢ 𝑁 = (((√‘(𝐶 + 𝐵)) − (√‘(𝐶 − 𝐵))) / 2) ⇒ ⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2) ∧ ((𝐴 gcd 𝐵) = 1 ∧ ¬ 2 ∥ 𝐴)) → (𝑀 gcd 𝑁) = 1) | ||
Theorem | flt4lem5elem 42637 | Version of fltaccoprm 42626 and fltbccoprm 42627 where 𝑀 is not squared. This can be proved in general for any polynomial in three variables: using prmdvdsncoprmbd 16760, dvds2addd 16325, and prmdvdsexp 16748, 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 42638 | 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 42639 | 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 42640 | 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 42641 | 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 42642 | Satisfy the hypotheses of flt4lem4 42635. (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 42643 | 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 42644 | 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 42645* | Convert flt4lem5f 42643 into a convenient form for nna4b4nsq 42646. 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 42646 | 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 42647 | (𝐶↑𝑁) is the largest term and therefore 𝐵 < 𝐶. (Contributed by Steven Nguyen, 22-Aug-2023.) |
⊢ (𝜑 → 𝐴 ∈ ℕ) & ⊢ (𝜑 → 𝐵 ∈ ℕ) & ⊢ (𝜑 → 𝐶 ∈ ℕ) & ⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘3)) & ⊢ (𝜑 → ((𝐴↑𝑁) + (𝐵↑𝑁)) = (𝐶↑𝑁)) ⇒ ⊢ (𝜑 → 𝐵 < 𝐶) | ||
Theorem | fltnltalem 42648 | Lemma for fltnlta 42649. A lower bound for 𝐴 based on pwdif 15900. (Contributed by Steven Nguyen, 22-Aug-2023.) |
⊢ (𝜑 → 𝐴 ∈ ℕ) & ⊢ (𝜑 → 𝐵 ∈ ℕ) & ⊢ (𝜑 → 𝐶 ∈ ℕ) & ⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘3)) & ⊢ (𝜑 → ((𝐴↑𝑁) + (𝐵↑𝑁)) = (𝐶↑𝑁)) ⇒ ⊢ (𝜑 → ((𝐶 − 𝐵) · ((𝐶↑(𝑁 − 1)) + ((𝑁 − 1) · (𝐵↑(𝑁 − 1))))) < (𝐴↑𝑁)) | ||
Theorem | fltnlta 42649 | In a Fermat counterexample, the exponent 𝑁 is less than all three numbers (𝐴, 𝐵, and 𝐶). Note that 𝐴 < 𝐵 (hypothesis) and 𝐵 < 𝐶 (fltltc 42647). See https://youtu.be/EymVXkPWxyc 42647 for an outline. (Contributed by SN, 24-Aug-2023.) |
⊢ (𝜑 → 𝐴 ∈ ℕ) & ⊢ (𝜑 → 𝐵 ∈ ℕ) & ⊢ (𝜑 → 𝐶 ∈ ℕ) & ⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘3)) & ⊢ (𝜑 → ((𝐴↑𝑁) + (𝐵↑𝑁)) = (𝐶↑𝑁)) & ⊢ (𝜑 → 𝐴 < 𝐵) ⇒ ⊢ (𝜑 → 𝑁 < 𝐴) | ||
These theorems were added for illustration or pedagogical purposes without the intention of being used, but some may still be moved to main and used, of course. | ||
Theorem | iddii 42650 | Version of a1ii 2 with the hypotheses switched. The first hypothesis is redundant so this theorem should not normally appear in a proof. Inference associated with idd 24. (Contributed by SN, 1-Apr-2025.) (New usage is discouraged.) |
⊢ 𝜑 & ⊢ 𝜓 ⇒ ⊢ 𝜓 | ||
Theorem | bicomdALT 42651 | Alternate proof of bicomd 223 which is shorter after expanding all parent theorems (as of 8-Aug-2024, bicom 222 depends on bicom1 221 and sylib 218 depends on syl 17). Additionally, the labels bicom1 221 and syl 17 happen to contain fewer characters than bicom 222 and sylib 218. However, neither of these conditions count as a shortening according to conventions 30428. In the first case, the criteria could easily be broken by upstream changes, and in many cases the upstream dependency tree is nontrivial (see orass 921 and pm2.31 922). For the latter case, theorem labels are up to revision, so they are not counted in the size of a proof. (Contributed by SN, 21-May-2022.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ (𝜑 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (𝜒 ↔ 𝜓)) | ||
Theorem | alan 42652 | Alias for 19.26 1867 for easier lookup. (Contributed by SN, 12-Aug-2025.) (New usage is discouraged.) |
⊢ (∀𝑥(𝜑 ∧ 𝜓) ↔ (∀𝑥𝜑 ∧ ∀𝑥𝜓)) | ||
Theorem | exor 42653 | Alias for 19.43 1879 for easier lookup. (Contributed by SN, 5-Jul-2025.) (New usage is discouraged.) |
⊢ (∃𝑥(𝜑 ∨ 𝜓) ↔ (∃𝑥𝜑 ∨ ∃𝑥𝜓)) | ||
Theorem | rexor 42654 | Alias for r19.43 3119 for easier lookup. (Contributed by SN, 5-Jul-2025.) (New usage is discouraged.) |
⊢ (∃𝑥 ∈ 𝐴 (𝜑 ∨ 𝜓) ↔ (∃𝑥 ∈ 𝐴 𝜑 ∨ ∃𝑥 ∈ 𝐴 𝜓)) | ||
Theorem | ruvALT 42655 | Alternate proof of ruv 9639 with one fewer syntax step thanks to using elirrv 9633 instead of elirr 9634. However, it does not change the compressed proof size or the number of symbols in the generated display, so it is not considered a shortening according to conventions 30428. (Contributed by SN, 1-Sep-2024.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ {𝑥 ∣ 𝑥 ∉ 𝑥} = V | ||
Theorem | sn-wcdeq 42656 | Alternative to wcdeq 3771 and df-cdeq 3772. This flattens the syntax representation ( wi ( weq vx vy ) wph ) to ( sn-wcdeq vx vy wph ), illustrating the comment of df-cdeq 3772. (Contributed by SN, 26-Sep-2024.) (New usage is discouraged.) |
wff (𝑥 = 𝑦 → 𝜑) | ||
Theorem | sq45 42657 | 45 squared is 2025. (Contributed by SN, 30-Mar-2025.) |
⊢ (;45↑2) = ;;;2025 | ||
Theorem | sum9cubes 42658 | The sum of the first nine perfect cubes is 2025. (Contributed by SN, 30-Mar-2025.) |
⊢ Σ𝑘 ∈ (1...9)(𝑘↑3) = ;;;2025 | ||
Theorem | sn-isghm 42659* | Longer proof of isghm 19245, unsuccessfully attempting to simplify isghm 19245 using elovmpo 7677 according to an editorial note (now removed). (Contributed by SN, 7-Jun-2025.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ 𝑋 = (Base‘𝑆) & ⊢ 𝑌 = (Base‘𝑇) & ⊢ + = (+g‘𝑆) & ⊢ ⨣ = (+g‘𝑇) ⇒ ⊢ (𝐹 ∈ (𝑆 GrpHom 𝑇) ↔ ((𝑆 ∈ Grp ∧ 𝑇 ∈ Grp) ∧ (𝐹:𝑋⟶𝑌 ∧ ∀𝑢 ∈ 𝑋 ∀𝑣 ∈ 𝑋 (𝐹‘(𝑢 + 𝑣)) = ((𝐹‘𝑢) ⨣ (𝐹‘𝑣))))) | ||
Theorem | aprilfools2025 42660 | An abuse of notation. (Contributed by Prof. Loof Lirpa, 1-Apr-2025.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ {〈“𝐴𝑝𝑟𝑖𝑙”〉, 〈“𝑓𝑜𝑜𝑙𝑠!”〉} ∈ V | ||
It is known that ax-10 2138, ax-11 2154, and ax-12 2174 are logically redundant in a weak sense. Practically, they can be replaced with hbn1w 2043, alcomimw 2039, and ax12wlem 2129 as long as you can fully substitute 𝑦 for 𝑥 in the relevant wff (that is, 𝑥 cannot appear in the wff after substituting). This strategy (which I will call a "standard replacement" of axioms) has a lot of potential, for example it works with df-fv 6570 and df-mpt 5231, two very common constructions. But doing a standard replacement of ax-10 2138, ax-11 2154, and ax-12 2174 takes unsatisfyingly long. Usually, if another approach is found, that approach is shorter and better. | ||
Theorem | nfa1w 42661* | Replace ax-10 2138 in nfa1 2148 with a substitution hypothesis. (Contributed by SN, 2-Sep-2025.) |
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ Ⅎ𝑥∀𝑥𝜑 | ||
Theorem | eu6w 42662* | Replace ax-10 2138, ax-12 2174 in eu6 2571 with substitution hypotheses. (Contributed by SN, 27-May-2025.) |
⊢ (𝑥 = 𝑧 → (𝜑 ↔ 𝜓)) & ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜃)) ⇒ ⊢ (∃!𝑥𝜑 ↔ ∃𝑦∀𝑥(𝜑 ↔ 𝑥 = 𝑦)) | ||
Theorem | abbibw 42663* | Replace ax-10 2138, ax-11 2154, ax-12 2174 in abbib 2808 with substitution hypotheses. (Contributed by SN, 27-May-2025.) |
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜃)) & ⊢ (𝑥 = 𝑦 → (𝜓 ↔ 𝜒)) ⇒ ⊢ ({𝑥 ∣ 𝜑} = {𝑥 ∣ 𝜓} ↔ ∀𝑥(𝜑 ↔ 𝜓)) | ||
Theorem | absnw 42664* | Replace ax-10 2138, ax-11 2154, ax-12 2174 in absn 4649 with a substitution hypothesis. (Contributed by SN, 27-May-2025.) |
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ ({𝑥 ∣ 𝜑} = {𝑌} ↔ ∀𝑥(𝜑 ↔ 𝑥 = 𝑌)) | ||
Theorem | euabsn2w 42665* | Replace ax-10 2138, ax-11 2154, ax-12 2174 in euabsn2 4729 with substitution hypotheses. (Contributed by SN, 27-May-2025.) |
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) & ⊢ (𝑥 = 𝑧 → (𝜑 ↔ 𝜃)) ⇒ ⊢ (∃!𝑥𝜑 ↔ ∃𝑦{𝑥 ∣ 𝜑} = {𝑦}) | ||
Theorem | sn-tz6.12-2 42666* | tz6.12-2 6894 without ax-10 2138, ax-11 2154, ax-12 2174. Improves 118 theorems. (Contributed by SN, 27-May-2025.) |
⊢ (¬ ∃!𝑥 𝐴𝐹𝑥 → (𝐹‘𝐴) = ∅) | ||
Theorem | cu3addd 42667 | 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 42668 | The square of the negative of a number. (Contributed by Igor Ieskov, 21-Jan-2024.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) ⇒ ⊢ (𝜑 → (-𝐴↑2) = (𝐴↑2)) | ||
Theorem | negexpidd 42669 | 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 42670* | An extended version of rexlimdvv 3209 to include three set variables. (Contributed by Igor Ieskov, 21-Jan-2024.) |
⊢ (𝜑 → ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐶) → (𝜓 → 𝜒))) ⇒ ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 ∃𝑧 ∈ 𝐶 𝜓 → 𝜒)) | ||
Theorem | 3cubeslem1 42671 | Lemma for 3cubes 42677. (Contributed by Igor Ieskov, 22-Jan-2024.) |
⊢ (𝜑 → 𝐴 ∈ ℚ) ⇒ ⊢ (𝜑 → 0 < (((𝐴 + 1)↑2) − 𝐴)) | ||
Theorem | 3cubeslem2 42672 | Lemma for 3cubes 42677. Used to show that the denominators in 3cubeslem4 42676 are nonzero. (Contributed by Igor Ieskov, 22-Jan-2024.) |
⊢ (𝜑 → 𝐴 ∈ ℚ) ⇒ ⊢ (𝜑 → ¬ ((((3↑3) · (𝐴↑2)) + ((3↑2) · 𝐴)) + 3) = 0) | ||
Theorem | 3cubeslem3l 42673 | Lemma for 3cubes 42677. (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 42674 | Lemma for 3cubes 42677. (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 42675 | Lemma for 3cubes 42677. (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 42676 | Lemma for 3cubes 42677. 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 42677* | 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 42678 | 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 42679* | Transfer at-most-one between related expressions. (Contributed by Stefan O'Rear, 12-Feb-2015.) |
⊢ 𝐴 ∈ V & ⊢ ∃!𝑦 𝑥 = 𝐴 & ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∃*𝑥𝜑 ↔ ∃*𝑦𝜓) | ||
Theorem | imaiinfv 42680* | Indexed intersection of an image. (Contributed by Stefan O'Rear, 22-Feb-2015.) |
⊢ ((𝐹 Fn 𝐴 ∧ 𝐵 ⊆ 𝐴) → ∩ 𝑥 ∈ 𝐵 (𝐹‘𝑥) = ∩ (𝐹 “ 𝐵)) | ||
Theorem | elrfi 42681* | Elementhood in a set of relative finite intersections. (Contributed by Stefan O'Rear, 22-Feb-2015.) |
⊢ ((𝐵 ∈ 𝑉 ∧ 𝐶 ⊆ 𝒫 𝐵) → (𝐴 ∈ (fi‘({𝐵} ∪ 𝐶)) ↔ ∃𝑣 ∈ (𝒫 𝐶 ∩ Fin)𝐴 = (𝐵 ∩ ∩ 𝑣))) | ||
Theorem | elrfirn 42682* | 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 42683* | 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 42684* | 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 42685* | Any function from the subsets of a set to itself, which is extensive (satisfies mrcssid 17661), isotone (satisfies mrcss 17660), and idempotent (satisfies mrcidm 17663) 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 42686 is the second. (Contributed by Stefan O'Rear, 1-Feb-2015.) |
⊢ (𝜑 → 𝐵 ∈ 𝑉) & ⊢ (𝜑 → 𝐹:𝒫 𝐵⟶𝒫 𝐵) & ⊢ ((𝜑 ∧ 𝑥 ⊆ 𝐵) → 𝑥 ⊆ (𝐹‘𝑥)) & ⊢ ((𝜑 ∧ 𝑥 ⊆ 𝐵 ∧ 𝑦 ⊆ 𝑥) → (𝐹‘𝑦) ⊆ (𝐹‘𝑥)) & ⊢ ((𝜑 ∧ 𝑥 ⊆ 𝐵) → (𝐹‘(𝐹‘𝑥)) = (𝐹‘𝑥)) ⇒ ⊢ (𝜑 → dom (𝐹 ∩ I ) ∈ (Moore‘𝐵)) | ||
Theorem | ismrcd2 42686* | Second half of ismrcd1 42685. (Contributed by Stefan O'Rear, 1-Feb-2015.) |
⊢ (𝜑 → 𝐵 ∈ 𝑉) & ⊢ (𝜑 → 𝐹:𝒫 𝐵⟶𝒫 𝐵) & ⊢ ((𝜑 ∧ 𝑥 ⊆ 𝐵) → 𝑥 ⊆ (𝐹‘𝑥)) & ⊢ ((𝜑 ∧ 𝑥 ⊆ 𝐵 ∧ 𝑦 ⊆ 𝑥) → (𝐹‘𝑦) ⊆ (𝐹‘𝑥)) & ⊢ ((𝜑 ∧ 𝑥 ⊆ 𝐵) → (𝐹‘(𝐹‘𝑥)) = (𝐹‘𝑥)) ⇒ ⊢ (𝜑 → 𝐹 = (mrCls‘dom (𝐹 ∩ I ))) | ||
Theorem | istopclsd 42687* | A closure function which satisfies sscls 23079, clsidm 23090, cls0 23103, and clsun 36310 defines a (unique) topology which it is the closure function on. (Contributed by Stefan O'Rear, 1-Feb-2015.) |
⊢ (𝜑 → 𝐵 ∈ 𝑉) & ⊢ (𝜑 → 𝐹:𝒫 𝐵⟶𝒫 𝐵) & ⊢ ((𝜑 ∧ 𝑥 ⊆ 𝐵) → 𝑥 ⊆ (𝐹‘𝑥)) & ⊢ ((𝜑 ∧ 𝑥 ⊆ 𝐵) → (𝐹‘(𝐹‘𝑥)) = (𝐹‘𝑥)) & ⊢ (𝜑 → (𝐹‘∅) = ∅) & ⊢ ((𝜑 ∧ 𝑥 ⊆ 𝐵 ∧ 𝑦 ⊆ 𝐵) → (𝐹‘(𝑥 ∪ 𝑦)) = ((𝐹‘𝑥) ∪ (𝐹‘𝑦))) & ⊢ 𝐽 = {𝑧 ∈ 𝒫 𝐵 ∣ (𝐹‘(𝐵 ∖ 𝑧)) = (𝐵 ∖ 𝑧)} ⇒ ⊢ (𝜑 → (𝐽 ∈ (TopOn‘𝐵) ∧ (cls‘𝐽) = 𝐹)) | ||
Theorem | ismrc 42688* | A function is a Moore closure operator iff it satisfies mrcssid 17661, mrcss 17660, and mrcidm 17663. (Contributed by Stefan O'Rear, 1-Feb-2015.) |
⊢ (𝐹 ∈ (mrCls “ (Moore‘𝐵)) ↔ (𝐵 ∈ V ∧ 𝐹:𝒫 𝐵⟶𝒫 𝐵 ∧ ∀𝑥∀𝑦((𝑥 ⊆ 𝐵 ∧ 𝑦 ⊆ 𝑥) → (𝑥 ⊆ (𝐹‘𝑥) ∧ (𝐹‘𝑦) ⊆ (𝐹‘𝑥) ∧ (𝐹‘(𝐹‘𝑥)) = (𝐹‘𝑥))))) | ||
Syntax | cnacs 42689 | Class of Noetherian closure systems. |
class NoeACS | ||
Definition | df-nacs 42690* | 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 42691* | Expand definition of Noetherian-type closure system. (Contributed by Stefan O'Rear, 4-Apr-2015.) |
⊢ 𝐹 = (mrCls‘𝐶) ⇒ ⊢ (𝐶 ∈ (NoeACS‘𝑋) ↔ (𝐶 ∈ (ACS‘𝑋) ∧ ∀𝑠 ∈ 𝐶 ∃𝑔 ∈ (𝒫 𝑋 ∩ Fin)𝑠 = (𝐹‘𝑔))) | ||
Theorem | nacsfg 42692* | 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 42693 | Express Noetherian-type closure system with fewer quantifiers. (Contributed by Stefan O'Rear, 4-Apr-2015.) |
⊢ 𝐹 = (mrCls‘𝐶) ⇒ ⊢ (𝐶 ∈ (NoeACS‘𝑋) ↔ (𝐶 ∈ (ACS‘𝑋) ∧ (𝐹 “ (𝒫 𝑋 ∩ Fin)) = 𝐶)) | ||
Theorem | mrefg2 42694* | Slight variation on finite generation for closure systems. (Contributed by Stefan O'Rear, 4-Apr-2015.) |
⊢ 𝐹 = (mrCls‘𝐶) ⇒ ⊢ (𝐶 ∈ (Moore‘𝑋) → (∃𝑔 ∈ (𝒫 𝑋 ∩ Fin)𝑆 = (𝐹‘𝑔) ↔ ∃𝑔 ∈ (𝒫 𝑆 ∩ Fin)𝑆 = (𝐹‘𝑔))) | ||
Theorem | mrefg3 42695* | Slight variation on finite generation for closure systems. (Contributed by Stefan O'Rear, 4-Apr-2015.) |
⊢ 𝐹 = (mrCls‘𝐶) ⇒ ⊢ ((𝐶 ∈ (Moore‘𝑋) ∧ 𝑆 ∈ 𝐶) → (∃𝑔 ∈ (𝒫 𝑋 ∩ Fin)𝑆 = (𝐹‘𝑔) ↔ ∃𝑔 ∈ (𝒫 𝑆 ∩ Fin)𝑆 ⊆ (𝐹‘𝑔))) | ||
Theorem | nacsacs 42696 | A closure system of Noetherian type is algebraic. (Contributed by Stefan O'Rear, 4-Apr-2015.) |
⊢ (𝐶 ∈ (NoeACS‘𝑋) → 𝐶 ∈ (ACS‘𝑋)) | ||
Theorem | isnacs3 42697* | 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 42698* | Transitivity induction of subsets, lemma for nacsfix 42699. (Contributed by Stefan O'Rear, 4-Apr-2015.) |
⊢ ((∀𝑥 ∈ ℕ0 (𝐹‘𝑥) ⊆ (𝐹‘(𝑥 + 1)) ∧ 𝐴 ∈ ℕ0 ∧ 𝐵 ∈ (ℤ≥‘𝐴)) → (𝐹‘𝐴) ⊆ (𝐹‘𝐵)) | ||
Theorem | nacsfix 42699* | 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 42700 |
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 𝐴)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |