![]() |
Metamath
Proof Explorer Theorem List (p. 415 of 479) | < 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-30171) |
![]() (30172-31694) |
![]() (31695-47852) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | flt4lem7 41401* | Convert flt4lem5f 41399 into a convenient form for nna4b4nsq 41402. 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 41402 | 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 41403 | (πΆβπ) is the largest term and therefore π΅ < πΆ. (Contributed by Steven Nguyen, 22-Aug-2023.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β πΆ β β) & β’ (π β π β (β€β₯β3)) & β’ (π β ((π΄βπ) + (π΅βπ)) = (πΆβπ)) β β’ (π β π΅ < πΆ) | ||
Theorem | fltnltalem 41404 | Lemma for fltnlta 41405. A lower bound for π΄ based on pwdif 15814. (Contributed by Steven Nguyen, 22-Aug-2023.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β πΆ β β) & β’ (π β π β (β€β₯β3)) & β’ (π β ((π΄βπ) + (π΅βπ)) = (πΆβπ)) β β’ (π β ((πΆ β π΅) Β· ((πΆβ(π β 1)) + ((π β 1) Β· (π΅β(π β 1))))) < (π΄βπ)) | ||
Theorem | fltnlta 41405 | In a Fermat counterexample, the exponent π is less than all three numbers (π΄, π΅, and πΆ). Note that π΄ < π΅ (hypothesis) and π΅ < πΆ (fltltc 41403). See https://youtu.be/EymVXkPWxyc 41403 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 41406 | 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 41407 | Alternate proof of bicomd 222 which is shorter after expanding all parent theorems (as of 8-Aug-2024, bicom 221 depends on bicom1 220 and sylib 217 depends on syl 17). Additionally, the labels bicom1 220 and syl 17 happen to contain fewer characters than bicom 221 and sylib 217. However, neither of these conditions count as a shortening according to conventions 29653. 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 | elabgw 41408* | Membership in a class abstraction, using two substitution hypotheses to avoid a disjoint variable condition on π₯ and π΄. This is to elabg 3667 what sbievw2 2100 is to sbievw 2096. (Contributed by SN, 20-Apr-2024.) |
β’ (π₯ = π¦ β (π β π)) & β’ (π¦ = π΄ β (π β π)) β β’ (π΄ β π β (π΄ β {π₯ β£ π} β π)) | ||
Theorem | elab2gw 41409* | Membership in a class abstraction, using two substitution hypotheses to avoid a disjoint variable condition on π₯ and π΄, which is not usually significant since π΅ is usually a constant. (Contributed by SN, 16-May-2024.) |
β’ (π₯ = π¦ β (π β π)) & β’ (π¦ = π΄ β (π β π)) & β’ π΅ = {π₯ β£ π} β β’ (π΄ β π β (π΄ β π΅ β π)) | ||
Theorem | elrab2w 41410* | Membership in a restricted class abstraction. This is to elrab2 3687 what elab2gw 41409 is to elab2g 3671. (Contributed by SN, 2-Sep-2024.) |
β’ (π₯ = π¦ β (π β π)) & β’ (π¦ = π΄ β (π β π)) & β’ πΆ = {π₯ β π΅ β£ π} β β’ (π΄ β πΆ β (π΄ β π΅ β§ π)) | ||
Theorem | ruvALT 41411 | Alternate proof of ruv 9597 with one fewer syntax step thanks to using elirrv 9591 instead of elirr 9592. 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 29653. (Contributed by SN, 1-Sep-2024.) (New usage is discouraged.) (Proof modification is discouraged.) |
β’ {π₯ β£ π₯ β π₯} = V | ||
Theorem | sn-wcdeq 41412 | Alternative to wcdeq 3760 and df-cdeq 3761. This flattens the syntax representation ( wi ( weq vx vy ) wph ) to ( sn-wcdeq vx vy wph ), illustrating the comment of df-cdeq 3761. (Contributed by SN, 26-Sep-2024.) (New usage is discouraged.) |
wff (π₯ = π¦ β π) | ||
Theorem | sq45 41413 | 45 squared is 2025. (Contributed by SN, 30-Mar-2025.) |
β’ (;45β2) = ;;;2025 | ||
Theorem | sum9cubes 41414 | The sum of the first nine perfect cubes is 2025. (Contributed by SN, 30-Mar-2025.) |
β’ Ξ£π β (1...9)(πβ3) = ;;;2025 | ||
Theorem | acos1half 41415 | The arccosine of 1 / 2 is Ο / 3. (Contributed by SN, 31-Aug-2024.) |
β’ (arccosβ(1 / 2)) = (Ο / 3) | ||
Theorem | aprilfools2025 41416 | An abuse of notation. (Contributed by Prof. Loof Lirpa, 1-Apr-2025.) (New usage is discouraged.) (Proof modification is discouraged.) |
β’ {β¨βπ΄ππππββ©, β¨βπππππ !ββ©} β V | ||
Theorem | binom2d 41417 | Deduction form of binom2. (Contributed by Igor Ieskov, 14-Dec-2023.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) β β’ (π β ((π΄ + π΅)β2) = (((π΄β2) + (2 Β· (π΄ Β· π΅))) + (π΅β2))) | ||
Theorem | cu3addd 41418 | 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 41419 | The square of the negative of a number. (Contributed by Igor Ieskov, 21-Jan-2024.) |
β’ (π β π΄ β β) β β’ (π β (-π΄β2) = (π΄β2)) | ||
Theorem | negexpidd 41420 | 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 41421* | An extended version of rexlimdvv 3211 to include three set variables. (Contributed by Igor Ieskov, 21-Jan-2024.) |
β’ (π β ((π₯ β π΄ β§ π¦ β π΅ β§ π§ β πΆ) β (π β π))) β β’ (π β (βπ₯ β π΄ βπ¦ β π΅ βπ§ β πΆ π β π)) | ||
Theorem | 3cubeslem1 41422 | Lemma for 3cubes 41428. (Contributed by Igor Ieskov, 22-Jan-2024.) |
β’ (π β π΄ β β) β β’ (π β 0 < (((π΄ + 1)β2) β π΄)) | ||
Theorem | 3cubeslem2 41423 | Lemma for 3cubes 41428. Used to show that the denominators in 3cubeslem4 41427 are nonzero. (Contributed by Igor Ieskov, 22-Jan-2024.) |
β’ (π β π΄ β β) β β’ (π β Β¬ ((((3β3) Β· (π΄β2)) + ((3β2) Β· π΄)) + 3) = 0) | ||
Theorem | 3cubeslem3l 41424 | Lemma for 3cubes 41428. (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 41425 | Lemma for 3cubes 41428. (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 41426 | Lemma for 3cubes 41428. (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 41427 | Lemma for 3cubes 41428. 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 41428* | 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 41429 | 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 41430* | Transfer at-most-one between related expressions. (Contributed by Stefan O'Rear, 12-Feb-2015.) |
β’ π΄ β V & β’ β!π¦ π₯ = π΄ & β’ (π₯ = π΄ β (π β π)) β β’ (β*π₯π β β*π¦π) | ||
Theorem | imaiinfv 41431* | Indexed intersection of an image. (Contributed by Stefan O'Rear, 22-Feb-2015.) |
β’ ((πΉ Fn π΄ β§ π΅ β π΄) β β© π₯ β π΅ (πΉβπ₯) = β© (πΉ β π΅)) | ||
Theorem | elrfi 41432* | Elementhood in a set of relative finite intersections. (Contributed by Stefan O'Rear, 22-Feb-2015.) |
β’ ((π΅ β π β§ πΆ β π« π΅) β (π΄ β (fiβ({π΅} βͺ πΆ)) β βπ£ β (π« πΆ β© Fin)π΄ = (π΅ β© β© π£))) | ||
Theorem | elrfirn 41433* | 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 41434* | 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 41435* | 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 41436* | Any function from the subsets of a set to itself, which is extensive (satisfies mrcssid 17561), isotone (satisfies mrcss 17560), and idempotent (satisfies mrcidm 17563) 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 41437 is the second. (Contributed by Stefan O'Rear, 1-Feb-2015.) |
β’ (π β π΅ β π) & β’ (π β πΉ:π« π΅βΆπ« π΅) & β’ ((π β§ π₯ β π΅) β π₯ β (πΉβπ₯)) & β’ ((π β§ π₯ β π΅ β§ π¦ β π₯) β (πΉβπ¦) β (πΉβπ₯)) & β’ ((π β§ π₯ β π΅) β (πΉβ(πΉβπ₯)) = (πΉβπ₯)) β β’ (π β dom (πΉ β© I ) β (Mooreβπ΅)) | ||
Theorem | ismrcd2 41437* | Second half of ismrcd1 41436. (Contributed by Stefan O'Rear, 1-Feb-2015.) |
β’ (π β π΅ β π) & β’ (π β πΉ:π« π΅βΆπ« π΅) & β’ ((π β§ π₯ β π΅) β π₯ β (πΉβπ₯)) & β’ ((π β§ π₯ β π΅ β§ π¦ β π₯) β (πΉβπ¦) β (πΉβπ₯)) & β’ ((π β§ π₯ β π΅) β (πΉβ(πΉβπ₯)) = (πΉβπ₯)) β β’ (π β πΉ = (mrClsβdom (πΉ β© I ))) | ||
Theorem | istopclsd 41438* | A closure function which satisfies sscls 22560, clsidm 22571, cls0 22584, and clsun 35213 defines a (unique) topology which it is the closure function on. (Contributed by Stefan O'Rear, 1-Feb-2015.) |
β’ (π β π΅ β π) & β’ (π β πΉ:π« π΅βΆπ« π΅) & β’ ((π β§ π₯ β π΅) β π₯ β (πΉβπ₯)) & β’ ((π β§ π₯ β π΅) β (πΉβ(πΉβπ₯)) = (πΉβπ₯)) & β’ (π β (πΉββ ) = β ) & β’ ((π β§ π₯ β π΅ β§ π¦ β π΅) β (πΉβ(π₯ βͺ π¦)) = ((πΉβπ₯) βͺ (πΉβπ¦))) & β’ π½ = {π§ β π« π΅ β£ (πΉβ(π΅ β π§)) = (π΅ β π§)} β β’ (π β (π½ β (TopOnβπ΅) β§ (clsβπ½) = πΉ)) | ||
Theorem | ismrc 41439* | A function is a Moore closure operator iff it satisfies mrcssid 17561, mrcss 17560, and mrcidm 17563. (Contributed by Stefan O'Rear, 1-Feb-2015.) |
β’ (πΉ β (mrCls β (Mooreβπ΅)) β (π΅ β V β§ πΉ:π« π΅βΆπ« π΅ β§ βπ₯βπ¦((π₯ β π΅ β§ π¦ β π₯) β (π₯ β (πΉβπ₯) β§ (πΉβπ¦) β (πΉβπ₯) β§ (πΉβ(πΉβπ₯)) = (πΉβπ₯))))) | ||
Syntax | cnacs 41440 | Class of Noetherian closure systems. |
class NoeACS | ||
Definition | df-nacs 41441* | 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 41442* | Expand definition of Noetherian-type closure system. (Contributed by Stefan O'Rear, 4-Apr-2015.) |
β’ πΉ = (mrClsβπΆ) β β’ (πΆ β (NoeACSβπ) β (πΆ β (ACSβπ) β§ βπ β πΆ βπ β (π« π β© Fin)π = (πΉβπ))) | ||
Theorem | nacsfg 41443* | 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 41444 | Express Noetherian-type closure system with fewer quantifiers. (Contributed by Stefan O'Rear, 4-Apr-2015.) |
β’ πΉ = (mrClsβπΆ) β β’ (πΆ β (NoeACSβπ) β (πΆ β (ACSβπ) β§ (πΉ β (π« π β© Fin)) = πΆ)) | ||
Theorem | mrefg2 41445* | Slight variation on finite generation for closure systems. (Contributed by Stefan O'Rear, 4-Apr-2015.) |
β’ πΉ = (mrClsβπΆ) β β’ (πΆ β (Mooreβπ) β (βπ β (π« π β© Fin)π = (πΉβπ) β βπ β (π« π β© Fin)π = (πΉβπ))) | ||
Theorem | mrefg3 41446* | Slight variation on finite generation for closure systems. (Contributed by Stefan O'Rear, 4-Apr-2015.) |
β’ πΉ = (mrClsβπΆ) β β’ ((πΆ β (Mooreβπ) β§ π β πΆ) β (βπ β (π« π β© Fin)π = (πΉβπ) β βπ β (π« π β© Fin)π β (πΉβπ))) | ||
Theorem | nacsacs 41447 | A closure system of Noetherian type is algebraic. (Contributed by Stefan O'Rear, 4-Apr-2015.) |
β’ (πΆ β (NoeACSβπ) β πΆ β (ACSβπ)) | ||
Theorem | isnacs3 41448* | 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 41449* | Transitivity induction of subsets, lemma for nacsfix 41450. (Contributed by Stefan O'Rear, 4-Apr-2015.) |
β’ ((βπ₯ β β0 (πΉβπ₯) β (πΉβ(π₯ + 1)) β§ π΄ β β0 β§ π΅ β (β€β₯βπ΄)) β (πΉβπ΄) β (πΉβπ΅)) | ||
Theorem | nacsfix 41450* | 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 41451 |
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 41452 | 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 41453 | 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 41454 | 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 41455 | 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 41456 | 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 41457 | 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 41458* | Interpret range of a maps-to notation as a constraint on the definition. (Contributed by Stefan O'Rear, 10-Oct-2014.) |
β’ ((π‘ β π΄ β¦ π΅):π΄βΆπΆ β (π‘ β π΄ β π΅ β πΆ)) | ||
Syntax | cmzpcl 41459 | Extend class notation to include pre-polynomial rings. |
class mzPolyCld | ||
Syntax | cmzp 41460 | Extend class notation to include polynomial rings. |
class mzPoly | ||
Definition | df-mzpcl 41461* | 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 41462. (Contributed by Stefan O'Rear, 4-Oct-2014.) |
β’ mzPolyCld = (π£ β V β¦ {π β π« (β€ βm (β€ βm π£)) β£ ((βπ β β€ ((β€ βm π£) Γ {π}) β π β§ βπ β π£ (π₯ β (β€ βm π£) β¦ (π₯βπ)) β π) β§ βπ β π βπ β π ((π βf + π) β π β§ (π βf Β· π) β π))}) | ||
Definition | df-mzp 41462 | 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 41463* | Substitution lemma for mzPolyCld. (Contributed by Stefan O'Rear, 4-Oct-2014.) |
β’ (π β V β (mzPolyCldβπ) = {π β π« (β€ βm (β€ βm π)) β£ ((βπ β β€ ((β€ βm π) Γ {π}) β π β§ βπ β π (π₯ β (β€ βm π) β¦ (π₯βπ)) β π) β§ βπ β π βπ β π ((π βf + π) β π β§ (π βf Β· π) β π))}) | ||
Theorem | elmzpcl 41464* | Double substitution lemma for mzPolyCld. (Contributed by Stefan O'Rear, 4-Oct-2014.) |
β’ (π β V β (π β (mzPolyCldβπ) β (π β (β€ βm (β€ βm π)) β§ ((βπ β β€ ((β€ βm π) Γ {π}) β π β§ βπ β π (π₯ β (β€ βm π) β¦ (π₯βπ)) β π) β§ βπ β π βπ β π ((π βf + π) β π β§ (π βf Β· π) β π))))) | ||
Theorem | mzpclall 41465 | 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 41462 is well-defined. (Contributed by Stefan O'Rear, 4-Oct-2014.) |
β’ (π β V β (β€ βm (β€ βm π)) β (mzPolyCldβπ)) | ||
Theorem | mzpcln0 41466 | Corollary of mzpclall 41465: polynomially closed function sets are not empty. (Contributed by Stefan O'Rear, 4-Oct-2014.) |
β’ (π β V β (mzPolyCldβπ) β β ) | ||
Theorem | mzpcl1 41467 | 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 41468* | 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 41469 | 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 41470 | Value of the mzPoly function. (Contributed by Stefan O'Rear, 4-Oct-2014.) |
β’ (π β V β (mzPolyβπ) = β© (mzPolyCldβπ)) | ||
Theorem | dmmzp 41471 | mzPoly is defined for all index sets which are sets. This is used with elfvdm 6929 to eliminate sethood antecedents. (Contributed by Stefan O'Rear, 4-Oct-2014.) |
β’ dom mzPoly = V | ||
Theorem | mzpincl 41472 | 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 41473 | Constant functions are polynomial. See also mzpconstmpt 41478. (Contributed by Stefan O'Rear, 4-Oct-2014.) |
β’ ((π β V β§ πΆ β β€) β ((β€ βm π) Γ {πΆ}) β (mzPolyβπ)) | ||
Theorem | mzpf 41474 | 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 41475* | A projection function is polynomial. (Contributed by Stefan O'Rear, 4-Oct-2014.) |
β’ ((π β V β§ π β π) β (π β (β€ βm π) β¦ (πβπ)) β (mzPolyβπ)) | ||
Theorem | mzpadd 41476 | The pointwise sum of two polynomial functions is a polynomial function. See also mzpaddmpt 41479. (Contributed by Stefan O'Rear, 4-Oct-2014.) |
β’ ((π΄ β (mzPolyβπ) β§ π΅ β (mzPolyβπ)) β (π΄ βf + π΅) β (mzPolyβπ)) | ||
Theorem | mzpmul 41477 | The pointwise product of two polynomial functions is a polynomial function. See also mzpmulmpt 41480. (Contributed by Stefan O'Rear, 4-Oct-2014.) |
β’ ((π΄ β (mzPolyβπ) β§ π΅ β (mzPolyβπ)) β (π΄ βf Β· π΅) β (mzPolyβπ)) | ||
Theorem | mzpconstmpt 41478* | A constant function expressed in maps-to notation is polynomial. This theorem and the several that follow (mzpaddmpt 41479, mzpmulmpt 41480, mzpnegmpt 41482, mzpsubmpt 41481, mzpexpmpt 41483) 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 41475 is already expressed using maps-to notation. (Contributed by Stefan O'Rear, 5-Oct-2014.) |
β’ ((π β V β§ πΆ β β€) β (π₯ β (β€ βm π) β¦ πΆ) β (mzPolyβπ)) | ||
Theorem | mzpaddmpt 41479* | Sum of polynomial functions is polynomial. Maps-to version of mzpadd 41476. (Contributed by Stefan O'Rear, 5-Oct-2014.) |
β’ (((π₯ β (β€ βm π) β¦ π΄) β (mzPolyβπ) β§ (π₯ β (β€ βm π) β¦ π΅) β (mzPolyβπ)) β (π₯ β (β€ βm π) β¦ (π΄ + π΅)) β (mzPolyβπ)) | ||
Theorem | mzpmulmpt 41480* | Product of polynomial functions is polynomial. Maps-to version of mzpmulmpt 41480. (Contributed by Stefan O'Rear, 5-Oct-2014.) |
β’ (((π₯ β (β€ βm π) β¦ π΄) β (mzPolyβπ) β§ (π₯ β (β€ βm π) β¦ π΅) β (mzPolyβπ)) β (π₯ β (β€ βm π) β¦ (π΄ Β· π΅)) β (mzPolyβπ)) | ||
Theorem | mzpsubmpt 41481* | The difference of two polynomial functions is polynomial. (Contributed by Stefan O'Rear, 10-Oct-2014.) |
β’ (((π₯ β (β€ βm π) β¦ π΄) β (mzPolyβπ) β§ (π₯ β (β€ βm π) β¦ π΅) β (mzPolyβπ)) β (π₯ β (β€ βm π) β¦ (π΄ β π΅)) β (mzPolyβπ)) | ||
Theorem | mzpnegmpt 41482* | Negation of a polynomial function. (Contributed by Stefan O'Rear, 11-Oct-2014.) |
β’ ((π₯ β (β€ βm π) β¦ π΄) β (mzPolyβπ) β (π₯ β (β€ βm π) β¦ -π΄) β (mzPolyβπ)) | ||
Theorem | mzpexpmpt 41483* | Raise a polynomial function to a (fixed) exponent. (Contributed by Stefan O'Rear, 5-Oct-2014.) |
β’ (((π₯ β (β€ βm π) β¦ π΄) β (mzPolyβπ) β§ π· β β0) β (π₯ β (β€ βm π) β¦ (π΄βπ·)) β (mzPolyβπ)) | ||
Theorem | mzpindd 41484* | "Structural" induction to prove properties of all polynomial functions. (Contributed by Stefan O'Rear, 4-Oct-2014.) |
β’ ((π β§ π β β€) β π) & β’ ((π β§ π β π) β π) & β’ ((π β§ (π:(β€ βm π)βΆβ€ β§ π) β§ (π:(β€ βm π)βΆβ€ β§ π)) β π) & β’ ((π β§ (π:(β€ βm π)βΆβ€ β§ π) β§ (π:(β€ βm π)βΆβ€ β§ π)) β π) & β’ (π₯ = ((β€ βm π) Γ {π}) β (π β π)) & β’ (π₯ = (π β (β€ βm π) β¦ (πβπ)) β (π β π)) & β’ (π₯ = π β (π β π)) & β’ (π₯ = π β (π β π)) & β’ (π₯ = (π βf + π) β (π β π)) & β’ (π₯ = (π βf Β· π) β (π β π)) & β’ (π₯ = π΄ β (π β π)) β β’ ((π β§ π΄ β (mzPolyβπ)) β π) | ||
Theorem | mzpmfp 41485 | Relationship between multivariate Z-polynomials and general multivariate polynomial functions. (Contributed by Stefan O'Rear, 20-Mar-2015.) (Revised by AV, 13-Jun-2019.) |
β’ (mzPolyβπΌ) = ran (πΌ eval β€ring) | ||
Theorem | mzpsubst 41486* | Substituting polynomials for the variables of a polynomial results in a polynomial. πΊ is expected to depend on π¦ and provide the polynomials which are being substituted. (Contributed by Stefan O'Rear, 5-Oct-2014.) |
β’ ((π β V β§ πΉ β (mzPolyβπ) β§ βπ¦ β π πΊ β (mzPolyβπ)) β (π₯ β (β€ βm π) β¦ (πΉβ(π¦ β π β¦ (πΊβπ₯)))) β (mzPolyβπ)) | ||
Theorem | mzprename 41487* | Simplified version of mzpsubst 41486 to simply relabel variables in a polynomial. (Contributed by Stefan O'Rear, 5-Oct-2014.) |
β’ ((π β V β§ πΉ β (mzPolyβπ) β§ π :πβΆπ) β (π₯ β (β€ βm π) β¦ (πΉβ(π₯ β π ))) β (mzPolyβπ)) | ||
Theorem | mzpresrename 41488* | A polynomial is a polynomial over all larger index sets. (Contributed by Stefan O'Rear, 5-Oct-2014.) (Revised by Stefan O'Rear, 5-Jun-2015.) |
β’ ((π β V β§ π β π β§ πΉ β (mzPolyβπ)) β (π₯ β (β€ βm π) β¦ (πΉβ(π₯ βΎ π))) β (mzPolyβπ)) | ||
Theorem | mzpcompact2lem 41489* | Lemma for mzpcompact2 41490. (Contributed by Stefan O'Rear, 9-Oct-2014.) |
β’ π΅ β V β β’ (π΄ β (mzPolyβπ΅) β βπ β Fin βπ β (mzPolyβπ)(π β π΅ β§ π΄ = (π β (β€ βm π΅) β¦ (πβ(π βΎ π))))) | ||
Theorem | mzpcompact2 41490* | Polynomials are finitary objects and can only reference a finite number of variables, even if the index set is infinite. Thus, every polynomial can be expressed as a (uniquely minimal, although we do not prove that) polynomial on a finite number of variables, which is then extended by adding an arbitrary set of ignored variables. (Contributed by Stefan O'Rear, 9-Oct-2014.) |
β’ (π΄ β (mzPolyβπ΅) β βπ β Fin βπ β (mzPolyβπ)(π β π΅ β§ π΄ = (π β (β€ βm π΅) β¦ (πβ(π βΎ π))))) | ||
Theorem | coeq0i 41491 | coeq0 6255 but without explicitly introducing domain and range symbols. (Contributed by Stefan O'Rear, 16-Oct-2014.) |
β’ ((π΄:πΆβΆπ· β§ π΅:πΈβΆπΉ β§ (πΆ β© πΉ) = β ) β (π΄ β π΅) = β ) | ||
Theorem | fzsplit1nn0 41492 | Split a finite 1-based set of integers in the middle, allowing either end to be empty ((1...0)). (Contributed by Stefan O'Rear, 8-Oct-2014.) |
β’ ((π΄ β β0 β§ π΅ β β0 β§ π΄ β€ π΅) β (1...π΅) = ((1...π΄) βͺ ((π΄ + 1)...π΅))) | ||
Syntax | cdioph 41493 | Extend class notation to include the family of Diophantine sets. |
class Dioph | ||
Definition | df-dioph 41494* | A Diophantine set is a set of positive integers which is a projection of the zero set of some polynomial. This definition somewhat awkwardly mixes β€ (via mzPoly) and β0 (to define the zero sets); the former could be avoided by considering coincidence sets of β0 polynomials at the cost of requiring two, and the second is driven by consistency with our mu-recursive functions and the requirements of the Davis-Putnam-Robinson-Matiyasevich proof. Both are avoidable at a complexity cost. In particular, it is a consequence of 4sq 16897 that implicitly restricting variables to β0 adds no expressive power over allowing them to range over β€. While this definition stipulates a specific index set for the polynomials, there is actually flexibility here, see eldioph2b 41501. (Contributed by Stefan O'Rear, 5-Oct-2014.) |
β’ Dioph = (π β β0 β¦ ran (π β (β€β₯βπ), π β (mzPolyβ(1...π)) β¦ {π‘ β£ βπ’ β (β0 βm (1...π))(π‘ = (π’ βΎ (1...π)) β§ (πβπ’) = 0)})) | ||
Theorem | eldiophb 41495* | Initial expression of Diophantine property of a set. (Contributed by Stefan O'Rear, 5-Oct-2014.) (Revised by Mario Carneiro, 22-Sep-2015.) |
β’ (π· β (Diophβπ) β (π β β0 β§ βπ β (β€β₯βπ)βπ β (mzPolyβ(1...π))π· = {π‘ β£ βπ’ β (β0 βm (1...π))(π‘ = (π’ βΎ (1...π)) β§ (πβπ’) = 0)})) | ||
Theorem | eldioph 41496* | Condition for a set to be Diophantine (unpacking existential quantifier). (Contributed by Stefan O'Rear, 5-Oct-2014.) |
β’ ((π β β0 β§ πΎ β (β€β₯βπ) β§ π β (mzPolyβ(1...πΎ))) β {π‘ β£ βπ’ β (β0 βm (1...πΎ))(π‘ = (π’ βΎ (1...π)) β§ (πβπ’) = 0)} β (Diophβπ)) | ||
Theorem | diophrw 41497* | Renaming and adding unused witness variables does not change the Diophantine set coded by a polynomial. (Contributed by Stefan O'Rear, 7-Oct-2014.) |
β’ ((π β V β§ π:πβ1-1βπ β§ (π βΎ π) = ( I βΎ π)) β {π β£ βπ β (β0 βm π)(π = (π βΎ π) β§ ((π β (β€ βm π) β¦ (πβ(π β π)))βπ) = 0)} = {π β£ βπ β (β0 βm π)(π = (π βΎ π) β§ (πβπ) = 0)}) | ||
Theorem | eldioph2lem1 41498* | Lemma for eldioph2 41500. Construct necessary renaming function for one direction. (Contributed by Stefan O'Rear, 8-Oct-2014.) |
β’ ((π β β0 β§ π΄ β Fin β§ (1...π) β π΄) β βπ β (β€β₯βπ)βπ β V (π:(1...π)β1-1-ontoβπ΄ β§ (π βΎ (1...π)) = ( I βΎ (1...π)))) | ||
Theorem | eldioph2lem2 41499* | Lemma for eldioph2 41500. Construct necessary renaming function for one direction. (Contributed by Stefan O'Rear, 8-Oct-2014.) |
β’ (((π β β0 β§ Β¬ π β Fin) β§ ((1...π) β π β§ π΄ β (β€β₯βπ))) β βπ(π:(1...π΄)β1-1βπ β§ (π βΎ (1...π)) = ( I βΎ (1...π)))) | ||
Theorem | eldioph2 41500* | Construct a Diophantine set from a polynomial with witness variables drawn from any set whatsoever, via mzpcompact2 41490. (Contributed by Stefan O'Rear, 8-Oct-2014.) (Revised by Stefan O'Rear, 5-Jun-2015.) |
β’ ((π β β0 β§ (π β V β§ (1...π) β π) β§ π β (mzPolyβπ)) β {π‘ β£ βπ’ β (β0 βm π)(π‘ = (π’ βΎ (1...π)) β§ (πβπ’) = 0)} β (Diophβπ)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |