Home | Metamath
Proof Explorer Theorem List (p. 409 of 470) | < 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-29646) |
Hilbert Space Explorer
(29647-31169) |
Users' Mathboxes
(31170-46966) |
Type | Label | Description |
---|---|---|
Statement | ||
Syntax | cprjcrv 40801 | Extend class notation with the projective curve function. |
class โ๐ฃ๐ ๐Crv | ||
Definition | df-prjcrv 40802* | 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 40621 and prjspvs 40782). (Contributed by SN, 23-Nov-2024.) |
โข โ๐ฃ๐ ๐Crv = (๐ โ โ0, ๐ โ Field โฆ (๐ โ โช ran ((0...๐) mHomP ๐) โฆ {๐ โ (๐โ๐ฃ๐ ๐n๐) โฃ ((((0...๐) eval ๐)โ๐) โ ๐) = {(0gโ๐)}})) | ||
Theorem | prjcrvfval 40803* | 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 40804* | 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 40805 | 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 40806* | 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 40807 | 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 40808 | 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 40809 | A counterexample for FLT does not exist for ๐ = 0. (Contributed by SN, 20-Aug-2024.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ โ) & โข (๐ โ ๐ถ โ โ) & โข (๐ โ ๐ โ โ0) & โข (๐ โ ((๐ดโ๐) + (๐ตโ๐)) = (๐ถโ๐)) โ โข (๐ โ ๐ โ โ) | ||
Theorem | fltdvdsabdvdsc 40810 | Any factor of both ๐ด and ๐ต also divides ๐ถ. This establishes the validity of fltabcoprmex 40811. (Contributed by SN, 21-Aug-2024.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ โ) & โข (๐ โ ๐ถ โ โ) & โข (๐ โ ๐ โ โ) & โข (๐ โ ((๐ดโ๐) + (๐ตโ๐)) = (๐ถโ๐)) โ โข (๐ โ (๐ด gcd ๐ต) โฅ ๐ถ) | ||
Theorem | fltabcoprmex 40811 | A counterexample to FLT implies a counterexample to FLT with ๐ด, ๐ต (assigned to ๐ด / (๐ด gcd ๐ต) and ๐ต / (๐ด gcd ๐ต)) coprime (by divgcdcoprm0 16476). (Contributed by SN, 20-Aug-2024.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ โ) & โข (๐ โ ๐ถ โ โ) & โข (๐ โ ๐ โ โ0) & โข (๐ โ ((๐ดโ๐) + (๐ตโ๐)) = (๐ถโ๐)) โ โข (๐ โ (((๐ด / (๐ด gcd ๐ต))โ๐) + ((๐ต / (๐ด gcd ๐ต))โ๐)) = ((๐ถ / (๐ด gcd ๐ต))โ๐)) | ||
Theorem | fltaccoprm 40812 | A counterexample to FLT with ๐ด, ๐ต coprime also has ๐ด, ๐ถ coprime. (Contributed by SN, 20-Aug-2024.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ โ) & โข (๐ โ ๐ถ โ โ) & โข (๐ โ ๐ โ โ0) & โข (๐ โ ((๐ดโ๐) + (๐ตโ๐)) = (๐ถโ๐)) & โข (๐ โ (๐ด gcd ๐ต) = 1) โ โข (๐ โ (๐ด gcd ๐ถ) = 1) | ||
Theorem | fltbccoprm 40813 | A counterexample to FLT with ๐ด, ๐ต coprime also has ๐ต, ๐ถ coprime. Proven from fltaccoprm 40812 using commutativity of addition. (Contributed by SN, 20-Aug-2024.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ โ) & โข (๐ โ ๐ถ โ โ) & โข (๐ โ ๐ โ โ0) & โข (๐ โ ((๐ดโ๐) + (๐ตโ๐)) = (๐ถโ๐)) & โข (๐ โ (๐ด gcd ๐ต) = 1) โ โข (๐ โ (๐ต gcd ๐ถ) = 1) | ||
Theorem | fltabcoprm 40814 | A counterexample to FLT with ๐ด, ๐ถ coprime also has ๐ด, ๐ต coprime. Converse of fltaccoprm 40812. (Contributed by SN, 22-Aug-2024.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ โ) & โข (๐ โ ๐ถ โ โ) & โข (๐ โ (๐ด gcd ๐ถ) = 1) & โข (๐ โ ((๐ดโ2) + (๐ตโ2)) = (๐ถโ2)) โ โข (๐ โ (๐ด gcd ๐ต) = 1) | ||
Theorem | infdesc 40815* | 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 40816 | If a counterexample to FLT exists, its addends are not equal. (Contributed by SN, 1-Jun-2023.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ โ) & โข (๐ โ ๐ถ โ โ) & โข (๐ โ ๐ โ (โคโฅโ2)) & โข (๐ โ ((๐ดโ๐) + (๐ตโ๐)) = (๐ถโ๐)) โ โข (๐ โ ๐ด โ ๐ต) | ||
Theorem | flt4lem 40817 | Raising a number to the fourth power is equivalent to squaring it twice. (Contributed by SN, 21-Aug-2024.) |
โข (๐ โ ๐ด โ โ) โ โข (๐ โ (๐ดโ4) = ((๐ดโ2)โ2)) | ||
Theorem | flt4lem1 40818 | Satisfy the antecedent used in several pythagtrip 16641 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 40819 | If ๐ด is even, ๐ต is odd. (Contributed by SN, 22-Aug-2024.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ โ) & โข (๐ โ ๐ถ โ โ) & โข (๐ โ 2 โฅ ๐ด) & โข (๐ โ (๐ด gcd ๐ถ) = 1) & โข (๐ โ ((๐ดโ2) + (๐ตโ2)) = (๐ถโ2)) โ โข (๐ โ ยฌ 2 โฅ ๐ต) | ||
Theorem | flt4lem3 40820 | Equivalent to pythagtriplem4 16626. Show that ๐ถ + ๐ด and ๐ถ โ ๐ด are coprime. (Contributed by SN, 22-Aug-2024.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ โ) & โข (๐ โ ๐ถ โ โ) & โข (๐ โ 2 โฅ ๐ด) & โข (๐ โ (๐ด gcd ๐ถ) = 1) & โข (๐ โ ((๐ดโ2) + (๐ตโ2)) = (๐ถโ2)) โ โข (๐ โ ((๐ถ + ๐ด) gcd (๐ถ โ ๐ด)) = 1) | ||
Theorem | flt4lem4 40821 | 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 40822 | In the context of the lemmas of pythagtrip 16641, ๐ and ๐ are coprime. (Contributed by SN, 23-Aug-2024.) |
โข ๐ = (((โโ(๐ถ + ๐ต)) + (โโ(๐ถ โ ๐ต))) / 2) & โข ๐ = (((โโ(๐ถ + ๐ต)) โ (โโ(๐ถ โ ๐ต))) / 2) โ โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง ((๐ดโ2) + (๐ตโ2)) = (๐ถโ2) โง ((๐ด gcd ๐ต) = 1 โง ยฌ 2 โฅ ๐ด)) โ (๐ gcd ๐) = 1) | ||
Theorem | flt4lem5elem 40823 | Version of fltaccoprm 40812 and fltbccoprm 40813 where ๐ is not squared. This can be proved in general for any polynomial in three variables: using prmdvdsncoprmbd 16537, dvds2addd 16109, and prmdvdsexp 16526, 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 40824 | 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 40825 | 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 40826 | 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 40827 | 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 40828 | Satisfy the hypotheses of flt4lem4 40821. (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 40829 | 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 40830 | 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 40831* | Convert flt4lem5f 40829 into a convenient form for nna4b4nsq 40832. 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 40832 | 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 40833 | (๐ถโ๐) is the largest term and therefore ๐ต < ๐ถ. (Contributed by Steven Nguyen, 22-Aug-2023.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ โ) & โข (๐ โ ๐ถ โ โ) & โข (๐ โ ๐ โ (โคโฅโ3)) & โข (๐ โ ((๐ดโ๐) + (๐ตโ๐)) = (๐ถโ๐)) โ โข (๐ โ ๐ต < ๐ถ) | ||
Theorem | fltnltalem 40834 | Lemma for fltnlta 40835. A lower bound for ๐ด based on pwdif 15688. (Contributed by Steven Nguyen, 22-Aug-2023.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ โ) & โข (๐ โ ๐ถ โ โ) & โข (๐ โ ๐ โ (โคโฅโ3)) & โข (๐ โ ((๐ดโ๐) + (๐ตโ๐)) = (๐ถโ๐)) โ โข (๐ โ ((๐ถ โ ๐ต) ยท ((๐ถโ(๐ โ 1)) + ((๐ โ 1) ยท (๐ตโ(๐ โ 1))))) < (๐ดโ๐)) | ||
Theorem | fltnlta 40835 | In a Fermat counterexample, the exponent ๐ is less than all three numbers (๐ด, ๐ต, and ๐ถ). Note that ๐ด < ๐ต (hypothesis) and ๐ต < ๐ถ (fltltc 40833). See https://youtu.be/EymVXkPWxyc 40833 for an outline. (Contributed by SN, 24-Aug-2023.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ โ) & โข (๐ โ ๐ถ โ โ) & โข (๐ โ ๐ โ (โคโฅโ3)) & โข (๐ โ ((๐ดโ๐) + (๐ตโ๐)) = (๐ถโ๐)) & โข (๐ โ ๐ด < ๐ต) โ โข (๐ โ ๐ < ๐ด) | ||
Theorem | binom2d 40836 | Deduction form of binom2. (Contributed by Igor Ieskov, 14-Dec-2023.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ โ) โ โข (๐ โ ((๐ด + ๐ต)โ2) = (((๐ดโ2) + (2 ยท (๐ด ยท ๐ต))) + (๐ตโ2))) | ||
Theorem | cu3addd 40837 | 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 40838 | The square of the negative of a number. (Contributed by Igor Ieskov, 21-Jan-2024.) |
โข (๐ โ ๐ด โ โ) โ โข (๐ โ (-๐ดโ2) = (๐ดโ2)) | ||
Theorem | negexpidd 40839 | 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 40840* | An extended version of rexlimdvv 3203 to include three set variables. (Contributed by Igor Ieskov, 21-Jan-2024.) |
โข (๐ โ ((๐ฅ โ ๐ด โง ๐ฆ โ ๐ต โง ๐ง โ ๐ถ) โ (๐ โ ๐))) โ โข (๐ โ (โ๐ฅ โ ๐ด โ๐ฆ โ ๐ต โ๐ง โ ๐ถ ๐ โ ๐)) | ||
Theorem | 3cubeslem1 40841 | Lemma for 3cubes 40847. (Contributed by Igor Ieskov, 22-Jan-2024.) |
โข (๐ โ ๐ด โ โ) โ โข (๐ โ 0 < (((๐ด + 1)โ2) โ ๐ด)) | ||
Theorem | 3cubeslem2 40842 | Lemma for 3cubes 40847. Used to show that the denominators in 3cubeslem4 40846 are nonzero. (Contributed by Igor Ieskov, 22-Jan-2024.) |
โข (๐ โ ๐ด โ โ) โ โข (๐ โ ยฌ ((((3โ3) ยท (๐ดโ2)) + ((3โ2) ยท ๐ด)) + 3) = 0) | ||
Theorem | 3cubeslem3l 40843 | Lemma for 3cubes 40847. (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 40844 | Lemma for 3cubes 40847. (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 40845 | Lemma for 3cubes 40847. (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 40846 | Lemma for 3cubes 40847. 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 40847* | 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 40848 | 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 40849* | Transfer at-most-one between related expressions. (Contributed by Stefan O'Rear, 12-Feb-2015.) |
โข ๐ด โ V & โข โ!๐ฆ ๐ฅ = ๐ด & โข (๐ฅ = ๐ด โ (๐ โ ๐)) โ โข (โ*๐ฅ๐ โ โ*๐ฆ๐) | ||
Theorem | imaiinfv 40850* | Indexed intersection of an image. (Contributed by Stefan O'Rear, 22-Feb-2015.) |
โข ((๐น Fn ๐ด โง ๐ต โ ๐ด) โ โฉ ๐ฅ โ ๐ต (๐นโ๐ฅ) = โฉ (๐น โ ๐ต)) | ||
Theorem | elrfi 40851* | Elementhood in a set of relative finite intersections. (Contributed by Stefan O'Rear, 22-Feb-2015.) |
โข ((๐ต โ ๐ โง ๐ถ โ ๐ซ ๐ต) โ (๐ด โ (fiโ({๐ต} โช ๐ถ)) โ โ๐ฃ โ (๐ซ ๐ถ โฉ Fin)๐ด = (๐ต โฉ โฉ ๐ฃ))) | ||
Theorem | elrfirn 40852* | 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 40853* | 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 40854* | 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 40855* | Any function from the subsets of a set to itself, which is extensive (satisfies mrcssid 17432), isotone (satisfies mrcss 17431), and idempotent (satisfies mrcidm 17434) 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 40856 is the second. (Contributed by Stefan O'Rear, 1-Feb-2015.) |
โข (๐ โ ๐ต โ ๐) & โข (๐ โ ๐น:๐ซ ๐ตโถ๐ซ ๐ต) & โข ((๐ โง ๐ฅ โ ๐ต) โ ๐ฅ โ (๐นโ๐ฅ)) & โข ((๐ โง ๐ฅ โ ๐ต โง ๐ฆ โ ๐ฅ) โ (๐นโ๐ฆ) โ (๐นโ๐ฅ)) & โข ((๐ โง ๐ฅ โ ๐ต) โ (๐นโ(๐นโ๐ฅ)) = (๐นโ๐ฅ)) โ โข (๐ โ dom (๐น โฉ I ) โ (Mooreโ๐ต)) | ||
Theorem | ismrcd2 40856* | Second half of ismrcd1 40855. (Contributed by Stefan O'Rear, 1-Feb-2015.) |
โข (๐ โ ๐ต โ ๐) & โข (๐ โ ๐น:๐ซ ๐ตโถ๐ซ ๐ต) & โข ((๐ โง ๐ฅ โ ๐ต) โ ๐ฅ โ (๐นโ๐ฅ)) & โข ((๐ โง ๐ฅ โ ๐ต โง ๐ฆ โ ๐ฅ) โ (๐นโ๐ฆ) โ (๐นโ๐ฅ)) & โข ((๐ โง ๐ฅ โ ๐ต) โ (๐นโ(๐นโ๐ฅ)) = (๐นโ๐ฅ)) โ โข (๐ โ ๐น = (mrClsโdom (๐น โฉ I ))) | ||
Theorem | istopclsd 40857* | A closure function which satisfies sscls 22329, clsidm 22340, cls0 22353, and clsun 34686 defines a (unique) topology which it is the closure function on. (Contributed by Stefan O'Rear, 1-Feb-2015.) |
โข (๐ โ ๐ต โ ๐) & โข (๐ โ ๐น:๐ซ ๐ตโถ๐ซ ๐ต) & โข ((๐ โง ๐ฅ โ ๐ต) โ ๐ฅ โ (๐นโ๐ฅ)) & โข ((๐ โง ๐ฅ โ ๐ต) โ (๐นโ(๐นโ๐ฅ)) = (๐นโ๐ฅ)) & โข (๐ โ (๐นโโ ) = โ ) & โข ((๐ โง ๐ฅ โ ๐ต โง ๐ฆ โ ๐ต) โ (๐นโ(๐ฅ โช ๐ฆ)) = ((๐นโ๐ฅ) โช (๐นโ๐ฆ))) & โข ๐ฝ = {๐ง โ ๐ซ ๐ต โฃ (๐นโ(๐ต โ ๐ง)) = (๐ต โ ๐ง)} โ โข (๐ โ (๐ฝ โ (TopOnโ๐ต) โง (clsโ๐ฝ) = ๐น)) | ||
Theorem | ismrc 40858* | A function is a Moore closure operator iff it satisfies mrcssid 17432, mrcss 17431, and mrcidm 17434. (Contributed by Stefan O'Rear, 1-Feb-2015.) |
โข (๐น โ (mrCls โ (Mooreโ๐ต)) โ (๐ต โ V โง ๐น:๐ซ ๐ตโถ๐ซ ๐ต โง โ๐ฅโ๐ฆ((๐ฅ โ ๐ต โง ๐ฆ โ ๐ฅ) โ (๐ฅ โ (๐นโ๐ฅ) โง (๐นโ๐ฆ) โ (๐นโ๐ฅ) โง (๐นโ(๐นโ๐ฅ)) = (๐นโ๐ฅ))))) | ||
Syntax | cnacs 40859 | Class of Noetherian closure systems. |
class NoeACS | ||
Definition | df-nacs 40860* | 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 40861* | Expand definition of Noetherian-type closure system. (Contributed by Stefan O'Rear, 4-Apr-2015.) |
โข ๐น = (mrClsโ๐ถ) โ โข (๐ถ โ (NoeACSโ๐) โ (๐ถ โ (ACSโ๐) โง โ๐ โ ๐ถ โ๐ โ (๐ซ ๐ โฉ Fin)๐ = (๐นโ๐))) | ||
Theorem | nacsfg 40862* | 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 40863 | Express Noetherian-type closure system with fewer quantifiers. (Contributed by Stefan O'Rear, 4-Apr-2015.) |
โข ๐น = (mrClsโ๐ถ) โ โข (๐ถ โ (NoeACSโ๐) โ (๐ถ โ (ACSโ๐) โง (๐น โ (๐ซ ๐ โฉ Fin)) = ๐ถ)) | ||
Theorem | mrefg2 40864* | Slight variation on finite generation for closure systems. (Contributed by Stefan O'Rear, 4-Apr-2015.) |
โข ๐น = (mrClsโ๐ถ) โ โข (๐ถ โ (Mooreโ๐) โ (โ๐ โ (๐ซ ๐ โฉ Fin)๐ = (๐นโ๐) โ โ๐ โ (๐ซ ๐ โฉ Fin)๐ = (๐นโ๐))) | ||
Theorem | mrefg3 40865* | Slight variation on finite generation for closure systems. (Contributed by Stefan O'Rear, 4-Apr-2015.) |
โข ๐น = (mrClsโ๐ถ) โ โข ((๐ถ โ (Mooreโ๐) โง ๐ โ ๐ถ) โ (โ๐ โ (๐ซ ๐ โฉ Fin)๐ = (๐นโ๐) โ โ๐ โ (๐ซ ๐ โฉ Fin)๐ โ (๐นโ๐))) | ||
Theorem | nacsacs 40866 | A closure system of Noetherian type is algebraic. (Contributed by Stefan O'Rear, 4-Apr-2015.) |
โข (๐ถ โ (NoeACSโ๐) โ ๐ถ โ (ACSโ๐)) | ||
Theorem | isnacs3 40867* | 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 40868* | Transitivity induction of subsets, lemma for nacsfix 40869. (Contributed by Stefan O'Rear, 4-Apr-2015.) |
โข ((โ๐ฅ โ โ0 (๐นโ๐ฅ) โ (๐นโ(๐ฅ + 1)) โง ๐ด โ โ0 โง ๐ต โ (โคโฅโ๐ด)) โ (๐นโ๐ด) โ (๐นโ๐ต)) | ||
Theorem | nacsfix 40869* | 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 40870 |
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 40871 | 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 40872 | 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 40873 | 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 40874 | 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 40875 | 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 40876 | 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 40877* | Interpret range of a maps-to notation as a constraint on the definition. (Contributed by Stefan O'Rear, 10-Oct-2014.) |
โข ((๐ก โ ๐ด โฆ ๐ต):๐ดโถ๐ถ โ (๐ก โ ๐ด โ ๐ต โ ๐ถ)) | ||
Syntax | cmzpcl 40878 | Extend class notation to include pre-polynomial rings. |
class mzPolyCld | ||
Syntax | cmzp 40879 | Extend class notation to include polynomial rings. |
class mzPoly | ||
Definition | df-mzpcl 40880* | 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 40881. (Contributed by Stefan O'Rear, 4-Oct-2014.) |
โข mzPolyCld = (๐ฃ โ V โฆ {๐ โ ๐ซ (โค โm (โค โm ๐ฃ)) โฃ ((โ๐ โ โค ((โค โm ๐ฃ) ร {๐}) โ ๐ โง โ๐ โ ๐ฃ (๐ฅ โ (โค โm ๐ฃ) โฆ (๐ฅโ๐)) โ ๐) โง โ๐ โ ๐ โ๐ โ ๐ ((๐ โf + ๐) โ ๐ โง (๐ โf ยท ๐) โ ๐))}) | ||
Definition | df-mzp 40881 | Polynomials over โค with an arbitrary index set, that is, the smallest ring of functions containing all constant functions and all projections. This is almost the most general reasonable definition; to reach full generality, we would need to be able to replace ZZ with an arbitrary (semi)ring (and a coordinate subring), but rings have not been defined yet. (Contributed by Stefan O'Rear, 4-Oct-2014.) |
โข mzPoly = (๐ฃ โ V โฆ โฉ (mzPolyCldโ๐ฃ)) | ||
Theorem | mzpclval 40882* | Substitution lemma for mzPolyCld. (Contributed by Stefan O'Rear, 4-Oct-2014.) |
โข (๐ โ V โ (mzPolyCldโ๐) = {๐ โ ๐ซ (โค โm (โค โm ๐)) โฃ ((โ๐ โ โค ((โค โm ๐) ร {๐}) โ ๐ โง โ๐ โ ๐ (๐ฅ โ (โค โm ๐) โฆ (๐ฅโ๐)) โ ๐) โง โ๐ โ ๐ โ๐ โ ๐ ((๐ โf + ๐) โ ๐ โง (๐ โf ยท ๐) โ ๐))}) | ||
Theorem | elmzpcl 40883* | Double substitution lemma for mzPolyCld. (Contributed by Stefan O'Rear, 4-Oct-2014.) |
โข (๐ โ V โ (๐ โ (mzPolyCldโ๐) โ (๐ โ (โค โm (โค โm ๐)) โง ((โ๐ โ โค ((โค โm ๐) ร {๐}) โ ๐ โง โ๐ โ ๐ (๐ฅ โ (โค โm ๐) โฆ (๐ฅโ๐)) โ ๐) โง โ๐ โ ๐ โ๐ โ ๐ ((๐ โf + ๐) โ ๐ โง (๐ โf ยท ๐) โ ๐))))) | ||
Theorem | mzpclall 40884 | The set of all functions with the signature of a polynomial is a polynomially closed set. This is a lemma to show that the intersection in df-mzp 40881 is well-defined. (Contributed by Stefan O'Rear, 4-Oct-2014.) |
โข (๐ โ V โ (โค โm (โค โm ๐)) โ (mzPolyCldโ๐)) | ||
Theorem | mzpcln0 40885 | Corollary of mzpclall 40884: polynomially closed function sets are not empty. (Contributed by Stefan O'Rear, 4-Oct-2014.) |
โข (๐ โ V โ (mzPolyCldโ๐) โ โ ) | ||
Theorem | mzpcl1 40886 | Defining property 1 of a polynomially closed function set ๐: it contains all constant functions. (Contributed by Stefan O'Rear, 4-Oct-2014.) |
โข ((๐ โ (mzPolyCldโ๐) โง ๐น โ โค) โ ((โค โm ๐) ร {๐น}) โ ๐) | ||
Theorem | mzpcl2 40887* | Defining property 2 of a polynomially closed function set ๐: it contains all projections. (Contributed by Stefan O'Rear, 4-Oct-2014.) |
โข ((๐ โ (mzPolyCldโ๐) โง ๐น โ ๐) โ (๐ โ (โค โm ๐) โฆ (๐โ๐น)) โ ๐) | ||
Theorem | mzpcl34 40888 | Defining properties 3 and 4 of a polynomially closed function set ๐: it is closed under pointwise addition and multiplication. (Contributed by Stefan O'Rear, 4-Oct-2014.) |
โข ((๐ โ (mzPolyCldโ๐) โง ๐น โ ๐ โง ๐บ โ ๐) โ ((๐น โf + ๐บ) โ ๐ โง (๐น โf ยท ๐บ) โ ๐)) | ||
Theorem | mzpval 40889 | Value of the mzPoly function. (Contributed by Stefan O'Rear, 4-Oct-2014.) |
โข (๐ โ V โ (mzPolyโ๐) = โฉ (mzPolyCldโ๐)) | ||
Theorem | dmmzp 40890 | mzPoly is defined for all index sets which are sets. This is used with elfvdm 6875 to eliminate sethood antecedents. (Contributed by Stefan O'Rear, 4-Oct-2014.) |
โข dom mzPoly = V | ||
Theorem | mzpincl 40891 | Polynomial closedness is a universal first-order property and passes to intersections. This is where the closure properties of the polynomial ring itself are proved. (Contributed by Stefan O'Rear, 4-Oct-2014.) |
โข (๐ โ V โ (mzPolyโ๐) โ (mzPolyCldโ๐)) | ||
Theorem | mzpconst 40892 | Constant functions are polynomial. See also mzpconstmpt 40897. (Contributed by Stefan O'Rear, 4-Oct-2014.) |
โข ((๐ โ V โง ๐ถ โ โค) โ ((โค โm ๐) ร {๐ถ}) โ (mzPolyโ๐)) | ||
Theorem | mzpf 40893 | A polynomial function is a function from the coordinate space to the integers. (Contributed by Stefan O'Rear, 5-Oct-2014.) |
โข (๐น โ (mzPolyโ๐) โ ๐น:(โค โm ๐)โถโค) | ||
Theorem | mzpproj 40894* | A projection function is polynomial. (Contributed by Stefan O'Rear, 4-Oct-2014.) |
โข ((๐ โ V โง ๐ โ ๐) โ (๐ โ (โค โm ๐) โฆ (๐โ๐)) โ (mzPolyโ๐)) | ||
Theorem | mzpadd 40895 | The pointwise sum of two polynomial functions is a polynomial function. See also mzpaddmpt 40898. (Contributed by Stefan O'Rear, 4-Oct-2014.) |
โข ((๐ด โ (mzPolyโ๐) โง ๐ต โ (mzPolyโ๐)) โ (๐ด โf + ๐ต) โ (mzPolyโ๐)) | ||
Theorem | mzpmul 40896 | The pointwise product of two polynomial functions is a polynomial function. See also mzpmulmpt 40899. (Contributed by Stefan O'Rear, 4-Oct-2014.) |
โข ((๐ด โ (mzPolyโ๐) โง ๐ต โ (mzPolyโ๐)) โ (๐ด โf ยท ๐ต) โ (mzPolyโ๐)) | ||
Theorem | mzpconstmpt 40897* | A constant function expressed in maps-to notation is polynomial. This theorem and the several that follow (mzpaddmpt 40898, mzpmulmpt 40899, mzpnegmpt 40901, mzpsubmpt 40900, mzpexpmpt 40902) can be used to build proofs that functions which are "manifestly polynomial", in the sense of being a maps-to containing constants, projections, and simple arithmetic operations, are actually polynomial functions. There is no mzpprojmpt because mzpproj 40894 is already expressed using maps-to notation. (Contributed by Stefan O'Rear, 5-Oct-2014.) |
โข ((๐ โ V โง ๐ถ โ โค) โ (๐ฅ โ (โค โm ๐) โฆ ๐ถ) โ (mzPolyโ๐)) | ||
Theorem | mzpaddmpt 40898* | Sum of polynomial functions is polynomial. Maps-to version of mzpadd 40895. (Contributed by Stefan O'Rear, 5-Oct-2014.) |
โข (((๐ฅ โ (โค โm ๐) โฆ ๐ด) โ (mzPolyโ๐) โง (๐ฅ โ (โค โm ๐) โฆ ๐ต) โ (mzPolyโ๐)) โ (๐ฅ โ (โค โm ๐) โฆ (๐ด + ๐ต)) โ (mzPolyโ๐)) | ||
Theorem | mzpmulmpt 40899* | Product of polynomial functions is polynomial. Maps-to version of mzpmulmpt 40899. (Contributed by Stefan O'Rear, 5-Oct-2014.) |
โข (((๐ฅ โ (โค โm ๐) โฆ ๐ด) โ (mzPolyโ๐) โง (๐ฅ โ (โค โm ๐) โฆ ๐ต) โ (mzPolyโ๐)) โ (๐ฅ โ (โค โm ๐) โฆ (๐ด ยท ๐ต)) โ (mzPolyโ๐)) | ||
Theorem | mzpsubmpt 40900* | The difference of two polynomial functions is polynomial. (Contributed by Stefan O'Rear, 10-Oct-2014.) |
โข (((๐ฅ โ (โค โm ๐) โฆ ๐ด) โ (mzPolyโ๐) โง (๐ฅ โ (โค โm ๐) โฆ ๐ต) โ (mzPolyโ๐)) โ (๐ฅ โ (โค โm ๐) โฆ (๐ด โ ๐ต)) โ (mzPolyโ๐)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |