![]() |
Metamath
Proof Explorer Theorem List (p. 350 of 480) | < 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-30439) |
![]() (30440-31962) |
![]() (31963-47940) |
Type | Label | Description |
---|---|---|
Statement | ||
Syntax | cmdl 34901 | The set of models. |
class mMdl | ||
Syntax | cusyn 34902 | The syntax function applied to elements of the model. |
class mUSyn | ||
Syntax | cgmdl 34903 | The set of models in a grammatical formal system. |
class mGMdl | ||
Syntax | cmitp 34904 | The interpretation function of the model. |
class mItp | ||
Syntax | cmfitp 34905 | The evaluation function derived from the interpretation. |
class mFromItp | ||
Definition | df-muv 34906 | Define the universe of a model. (Contributed by Mario Carneiro, 14-Jul-2016.) |
β’ mUV = Slot 7 | ||
Definition | df-mfsh 34907 | Define the freshness relation of a model. (Contributed by Mario Carneiro, 14-Jul-2016.) |
β’ mFresh = Slot ;19 | ||
Definition | df-mevl 34908 | Define the evaluation function of a model. (Contributed by Mario Carneiro, 14-Jul-2016.) |
β’ mEval = Slot ;20 | ||
Definition | df-mvl 34909* | Define the set of valuations. (Contributed by Mario Carneiro, 14-Jul-2016.) |
β’ mVL = (π‘ β V β¦ Xπ£ β (mVRβπ‘)((mUVβπ‘) β {((mTypeβπ‘)βπ£)})) | ||
Definition | df-mvsb 34910* | Define substitution applied to a valuation. (Contributed by Mario Carneiro, 14-Jul-2016.) |
β’ mVSubst = (π‘ β V β¦ {β¨β¨π , πβ©, π₯β© β£ ((π β ran (mSubstβπ‘) β§ π β (mVLβπ‘)) β§ βπ£ β (mVRβπ‘)πdom (mEvalβπ‘)(π β((mVHβπ‘)βπ£)) β§ π₯ = (π£ β (mVRβπ‘) β¦ (π(mEvalβπ‘)(π β((mVHβπ‘)βπ£)))))}) | ||
Definition | df-mfrel 34911* | Define the set of freshness relations. (Contributed by Mario Carneiro, 14-Jul-2016.) |
β’ mFRel = (π‘ β V β¦ {π β π« ((mUVβπ‘) Γ (mUVβπ‘)) β£ (β‘π = π β§ βπ β (mVTβπ‘)βπ€ β (π« (mUVβπ‘) β© Fin)βπ£ β ((mUVβπ‘) β {π})π€ β (π β {π£}))}) | ||
Definition | df-mdl 34912* | Define the set of models of a formal system. (Contributed by Mario Carneiro, 14-Jul-2016.) |
β’ mMdl = {π‘ β mFS β£ [(mUVβπ‘) / π’][(mExβπ‘) / π₯][(mVLβπ‘) / π£][(mEvalβπ‘) / π][(mFreshβπ‘) / π]((π’ β ((mTCβπ‘) Γ V) β§ π β (mFRelβπ‘) β§ π β (π’ βpm (π£ Γ (mExβπ‘)))) β§ βπ β π£ ((βπ β π₯ (π β {β¨π, πβ©}) β (π’ β {(1st βπ)}) β§ βπ¦ β (mVRβπ‘)β¨π, ((mVHβπ‘)βπ¦)β©π(πβπ¦) β§ βπβββπ(β¨π, β, πβ© β (mAxβπ‘) β ((βπ¦βπ§(π¦ππ§ β (πβπ¦)π(πβπ§)) β§ β β (dom π β {π})) β πdom π π))) β§ (βπ β ran (mSubstβπ‘)βπ β (mExβπ‘)βπ¦(β¨π , πβ©(mVSubstβπ‘)π¦ β (π β {β¨π, (π βπ)β©}) = (π β {β¨π¦, πβ©})) β§ βπ β π£ βπ β π₯ ((π βΎ ((mVarsβπ‘)βπ)) = (π βΎ ((mVarsβπ‘)βπ)) β (π β {β¨π, πβ©}) = (π β {β¨π, πβ©})) β§ βπ¦ β π’ βπ β π₯ ((π β ((mVarsβπ‘)βπ)) β (π β {π¦}) β (π β {β¨π, πβ©}) β (π β {π¦})))))} | ||
Definition | df-musyn 34913* | Define the syntax typecode function for the model universe. (Contributed by Mario Carneiro, 14-Jul-2016.) |
β’ mUSyn = (π‘ β V β¦ (π£ β (mUVβπ‘) β¦ β¨((mSynβπ‘)β(1st βπ£)), (2nd βπ£)β©)) | ||
Definition | df-gmdl 34914* | Define the set of models of a grammatical formal system. (Contributed by Mario Carneiro, 14-Jul-2016.) |
β’ mGMdl = {π‘ β (mGFS β© mMdl) β£ (βπ β (mTCβπ‘)((mUVβπ‘) β {π}) β ((mUVβπ‘) β {((mSynβπ‘)βπ)}) β§ βπ£ β (mUVβπ)βπ€ β (mUVβπ)(π£(mFreshβπ‘)π€ β π£(mFreshβπ‘)((mUSynβπ‘)βπ€)) β§ βπ β (mVLβπ‘)βπ β (mExβπ‘)((mEvalβπ‘) β {β¨π, πβ©}) = (((mEvalβπ‘) β {β¨π, ((mESynβπ‘)βπ)β©}) β© ((mUVβπ‘) β {(1st βπ)})))} | ||
Definition | df-mitp 34915* | Define the interpretation function for a model. (Contributed by Mario Carneiro, 14-Jul-2016.) |
β’ mItp = (π‘ β V β¦ (π β (mSAβπ‘) β¦ (π β Xπ β ((mVarsβπ‘)βπ)((mUVβπ‘) β {((mTypeβπ‘)βπ)}) β¦ (β©π₯βπ β (mVLβπ‘)(π = (π βΎ ((mVarsβπ‘)βπ)) β§ π₯ = (π(mEvalβπ‘)π)))))) | ||
Definition | df-mfitp 34916* | Define a function that produces the evaluation function, given the interpretation function for a model. (Contributed by Mario Carneiro, 14-Jul-2016.) |
β’ mFromItp = (π‘ β V β¦ (π β Xπ β (mSAβπ‘)(((mUVβπ‘) β {((1st βπ‘)βπ)}) βm Xπ β ((mVarsβπ‘)βπ)((mUVβπ‘) β {((mTypeβπ‘)βπ)})) β¦ (β©π β ((mUVβπ‘) βpm ((mVLβπ‘) Γ (mExβπ‘)))βπ β (mVLβπ‘)(βπ£ β (mVRβπ‘)β¨π, ((mVHβπ‘)βπ£)β©π(πβπ£) β§ βπβπβπ(π(mSTβπ‘)β¨π, πβ© β β¨π, πβ©π(πβ(π β ((mVarsβπ‘)βπ) β¦ (ππ(πβ((mVHβπ‘)βπ)))))) β§ βπ β (mExβπ‘)(π β {β¨π, πβ©}) = ((π β {β¨π, ((mESynβπ‘)βπ)β©}) β© ((mUVβπ‘) β {(1st βπ)})))))) | ||
Syntax | ccpms 34917 | Completion of a metric space. |
class cplMetSp | ||
Syntax | chlb 34918 | Embeddings for a direct limit. |
class HomLimB | ||
Syntax | chlim 34919 | Direct limit structure. |
class HomLim | ||
Syntax | cpfl 34920 | Polynomial extension field. |
class polyFld | ||
Syntax | csf1 34921 | Splitting field for a single polynomial (auxiliary). |
class splitFld1 | ||
Syntax | csf 34922 | Splitting field for a finite set of polynomials. |
class splitFld | ||
Syntax | cpsl 34923 | Splitting field for a sequence of polynomials. |
class polySplitLim | ||
Definition | df-cplmet 34924* | A function which completes the given metric space. (Contributed by Mario Carneiro, 2-Dec-2014.) |
β’ cplMetSp = (π€ β V β¦ β¦((π€ βs β) βΎs (Cauβ(distβπ€))) / πβ¦β¦(Baseβπ) / π£β¦β¦{β¨π, πβ© β£ ({π, π} β π£ β§ βπ₯ β β+ βπ β β€ (π βΎ (β€β₯βπ)):(β€β₯βπ)βΆ((πβπ)(ballβ(distβπ€))π₯))} / πβ¦((π /s π) sSet {β¨(distβndx), {β¨β¨π₯, π¦β©, π§β© β£ βπ β π£ βπ β π£ ((π₯ = [π]π β§ π¦ = [π]π) β§ (π βf (distβπ)π) β π§)}β©})) | ||
Definition | df-homlimb 34925* | The input to this function is a sequence (on β) of homomorphisms πΉ(π):π (π)βΆπ (π + 1). The resulting structure is the direct limit of the direct system so defined. This function returns the pair β¨π, πΊβ© where π is the terminal object and πΊ is a sequence of functions such that πΊ(π):π (π)βΆπ and πΊ(π) = πΉ(π) β πΊ(π + 1). (Contributed by Mario Carneiro, 2-Dec-2014.) |
β’ HomLimB = (π β V β¦ β¦βͺ π β β ({π} Γ dom (πβπ)) / π£β¦β¦β© {π β£ (π Er π£ β§ (π₯ β π£ β¦ β¨((1st βπ₯) + 1), ((πβ(1st βπ₯))β(2nd βπ₯))β©) β π )} / πβ¦β¨(π£ / π), (π β β β¦ (π₯ β dom (πβπ) β¦ [β¨π, π₯β©]π))β©) | ||
Definition | df-homlim 34926* | The input to this function is a sequence (on β) of structures π (π) and homomorphisms πΉ(π):π (π)βΆπ (π + 1). The resulting structure is the direct limit of the direct system so defined, and maintains any structures that were present in the original objects. TODO: generalize to directed sets? (Contributed by Mario Carneiro, 2-Dec-2014.) |
β’ HomLim = (π β V, π β V β¦ β¦( HomLimB βπ) / πβ¦β¦(1st βπ) / π£β¦β¦(2nd βπ) / πβ¦({β¨(Baseβndx), π£β©, β¨(+gβndx), βͺ π β β ran (π₯ β dom (πβπ), π¦ β dom (πβπ) β¦ β¨β¨((πβπ)βπ₯), ((πβπ)βπ¦)β©, ((πβπ)β(π₯(+gβ(πβπ))π¦))β©)β©, β¨(.rβndx), βͺ π β β ran (π₯ β dom (πβπ), π¦ β dom (πβπ) β¦ β¨β¨((πβπ)βπ₯), ((πβπ)βπ¦)β©, ((πβπ)β(π₯(.rβ(πβπ))π¦))β©)β©} βͺ {β¨(TopOpenβndx), {π β π« π£ β£ βπ β β (β‘(πβπ) β π ) β (TopOpenβ(πβπ))}β©, β¨(distβndx), βͺ π β β ran (π₯ β dom ((πβπ)βπ), π¦ β dom ((πβπ)βπ) β¦ β¨β¨((πβπ)βπ₯), ((πβπ)βπ¦)β©, (π₯(distβ(πβπ))π¦)β©)β©, β¨(leβndx), βͺ π β β (β‘(πβπ) β ((leβ(πβπ)) β (πβπ)))β©})) | ||
Definition | df-plfl 34927* | Define the field extension that augments a field with the root of the given irreducible polynomial, and extends the norm if one exists and the extension is unique. (Contributed by Mario Carneiro, 2-Dec-2014.) |
β’ polyFld = (π β V, π β V β¦ β¦(Poly1βπ) / π β¦β¦((RSpanβπ )β{π}) / πβ¦β¦(π§ β (Baseβπ) β¦ [(π§( Β·π βπ )(1rβπ ))](π ~QG π)) / πβ¦β¨β¦(π /s (π ~QG π)) / π‘β¦((π‘ toNrmGrp (β©π β (AbsValβπ‘)(π β π) = (normβπ))) sSet β¨(leβndx), β¦(π§ β (Baseβπ‘) β¦ (β©π β π§ (π deg1 π) < (π deg1 π))) / πβ¦(β‘π β ((leβπ ) β π))β©), πβ©) | ||
Definition | df-sfl1 34928* |
Temporary construction for the splitting field of a polynomial. The
inputs are a field π and a polynomial π that we
want to split,
along with a tuple π in the same format as the output.
The output
is a tuple β¨π, πΉβ© where π is the splitting field
and πΉ
is an injective homomorphism from the original field π.
The function works by repeatedly finding the smallest monic irreducible factor, and extending the field by that factor using the polyFld construction. We keep track of a total order in each of the splitting fields so that we can pick an element definably without needing global choice. (Contributed by Mario Carneiro, 2-Dec-2014.) |
β’ splitFld1 = (π β V, π β V β¦ (π β (Poly1βπ) β¦ (rec((π β V, π β V β¦ β¦( mPoly βπ ) / πβ¦β¦{π β ((Monic1pβπ ) β© (Irredβπ)) β£ (π(β₯rβπ)(π β π) β§ 1 < (π deg1 π))} / πβ¦if(((π β π) = (0gβπ) β¨ π = β ), β¨π , πβ©, β¦(glbβπ) / ββ¦β¦(π polyFld β) / π‘β¦β¨(1st βπ‘), (π β (2nd βπ‘))β©)), π)β(cardβ(1...(π deg1 π)))))) | ||
Definition | df-sfl 34929* | Define the splitting field of a finite collection of polynomials, given a total ordered base field. The output is a tuple β¨π, πΉβ© where π is the totally ordered splitting field and πΉ is an injective homomorphism from the original field π. (Contributed by Mario Carneiro, 2-Dec-2014.) |
β’ splitFld = (π β V, π β V β¦ (β©π₯βπ(π Isom < , (ltβπ)((1...(β―βπ)), π) β§ π₯ = (seq0((π β V, π β V β¦ ((π splitFld1 π)βπ)), (π βͺ {β¨0, β¨π, ( I βΎ (Baseβπ))β©β©}))β(β―βπ))))) | ||
Definition | df-psl 34930* | Define the direct limit of an increasing sequence of fields produced by pasting together the splitting fields for each sequence of polynomials. That is, given a ring π, a strict order on π, and a sequence π:ββΆ(π« π β© Fin) of finite sets of polynomials to split, we construct the direct limit system of field extensions by splitting one set at a time and passing the resulting construction to HomLim. (Contributed by Mario Carneiro, 2-Dec-2014.) |
β’ polySplitLim = (π β V, π β ((π« (Baseβπ) β© Fin) βm β) β¦ β¦(1st β seq0((π β V, π β V β¦ β¦(1st βπ) / πβ¦β¦(1st βπ) / π β¦β¦(π splitFld ran (π₯ β π β¦ (π₯ β (2nd βπ)))) / πβ¦β¨π, ((2nd βπ) β (2nd βπ))β©), (π βͺ {β¨0, β¨β¨π, β β©, ( I βΎ (Baseβπ))β©β©}))) / πβ¦((1st β (π shift 1)) HomLim (2nd β π))) | ||
Syntax | czr 34931 | Integral elements of a ring. |
class ZRing | ||
Syntax | cgf 34932 | Galois finite field. |
class GF | ||
Syntax | cgfo 34933 | Galois limit field. |
class GFβ | ||
Syntax | ceqp 34934 | Equivalence relation for df-qp 34945. |
class ~Qp | ||
Syntax | crqp 34935 | Equivalence relation representatives for df-qp 34945. |
class /Qp | ||
Syntax | cqp 34936 | The set of π-adic rational numbers. |
class Qp | ||
Syntax | czp 34937 | The set of π-adic integers. (Not to be confused with czn 21272.) |
class Zp | ||
Syntax | cqpa 34938 | Algebraic completion of the π-adic rational numbers. |
class _Qp | ||
Syntax | ccp 34939 | Metric completion of _Qp. |
class Cp | ||
Definition | df-zrng 34940 | Define the subring of integral elements in a ring. (Contributed by Mario Carneiro, 2-Dec-2014.) |
β’ ZRing = (π β V β¦ (π IntgRing ran (β€RHomβπ))) | ||
Definition | df-gf 34941* | Define the Galois finite field of order πβπ. (Contributed by Mario Carneiro, 2-Dec-2014.) |
β’ GF = (π β β, π β β β¦ β¦(β€/nβ€βπ) / πβ¦(1st β(π splitFld {β¦(Poly1βπ) / π β¦β¦(var1βπ) / π₯β¦(((πβπ)(.gβ(mulGrpβπ ))π₯)(-gβπ )π₯)}))) | ||
Definition | df-gfoo 34942* | Define the Galois field of order πβ+β, as a direct limit of the Galois finite fields. (Contributed by Mario Carneiro, 2-Dec-2014.) |
β’ GFβ = (π β β β¦ β¦(β€/nβ€βπ) / πβ¦(π polySplitLim (π β β β¦ {β¦(Poly1βπ) / π β¦β¦(var1βπ) / π₯β¦(((πβπ)(.gβ(mulGrpβπ ))π₯)(-gβπ )π₯)}))) | ||
Definition | df-eqp 34943* | Define an equivalence relation on β€-indexed sequences of integers such that two sequences are equivalent iff the difference is equivalent to zero, and a sequence is equivalent to zero iff the sum Ξ£π β€ ππ(π)(πβπ) is a multiple of πβ(π + 1) for every π. (Contributed by Mario Carneiro, 2-Dec-2014.) |
β’ ~Qp = (π β β β¦ {β¨π, πβ© β£ ({π, π} β (β€ βm β€) β§ βπ β β€ Ξ£π β (β€β₯β-π)(((πβ-π) β (πβ-π)) / (πβ(π + (π + 1)))) β β€)}) | ||
Definition | df-rqp 34944* | There is a unique element of (β€ βm (0...(π β 1))) ~Qp -equivalent to any element of (β€ βm β€), if the sequences are zero for sufficiently large negative values; this function selects that element. (Contributed by Mario Carneiro, 2-Dec-2014.) |
β’ /Qp = (π β β β¦ (~Qp β© β¦{π β (β€ βm β€) β£ βπ₯ β ran β€β₯(β‘π β (β€ β {0})) β π₯} / π¦β¦(π¦ Γ (π¦ β© (β€ βm (0...(π β 1))))))) | ||
Definition | df-qp 34945* | Define the π-adic completion of the rational numbers, as a normed field structure with a total order (that is not compatible with the operations). (Contributed by Mario Carneiro, 2-Dec-2014.) (Revised by AV, 10-Oct-2021.) |
β’ Qp = (π β β β¦ β¦{β β (β€ βm (0...(π β 1))) β£ βπ₯ β ran β€β₯(β‘β β (β€ β {0})) β π₯} / πβ¦(({β¨(Baseβndx), πβ©, β¨(+gβndx), (π β π, π β π β¦ ((/Qpβπ)β(π βf + π)))β©, β¨(.rβndx), (π β π, π β π β¦ ((/Qpβπ)β(π β β€ β¦ Ξ£π β β€ ((πβπ) Β· (πβ(π β π))))))β©} βͺ {β¨(leβndx), {β¨π, πβ© β£ ({π, π} β π β§ Ξ£π β β€ ((πβ-π) Β· ((π + 1)β-π)) < Ξ£π β β€ ((πβ-π) Β· ((π + 1)β-π)))}β©}) toNrmGrp (π β π β¦ if(π = (β€ Γ {0}), 0, (πβ-inf((β‘π β (β€ β {0})), β, < )))))) | ||
Definition | df-zp 34946 | Define the π-adic integers, as a subset of the π-adic rationals. (Contributed by Mario Carneiro, 2-Dec-2014.) |
β’ Zp = (ZRing β Qp) | ||
Definition | df-qpa 34947* | Define the completion of the π-adic rationals. Here we simply define it as the splitting field of a dense sequence of polynomials (using as the π-th set the collection of polynomials with degree less than π and with coefficients < (πβπ)). Krasner's lemma will then show that all monic polynomials have splitting fields isomorphic to a sufficiently close Eisenstein polynomial from the list, and unramified extensions are generated by the polynomial π₯β(πβπ) β π₯, which is in the list. Thus, every finite extension of Qp is a subfield of this field extension, so it is algebraically closed. (Contributed by Mario Carneiro, 2-Dec-2014.) |
β’ _Qp = (π β β β¦ β¦(Qpβπ) / πβ¦(π polySplitLim (π β β β¦ {π β (Poly1βπ) β£ ((π deg1 π) β€ π β§ βπ β ran (coe1βπ)(β‘π β (β€ β {0})) β (0...π))}))) | ||
Definition | df-cp 34948 | Define the metric completion of the algebraic completion of the π -adic rationals. (Contributed by Mario Carneiro, 2-Dec-2014.) |
β’ Cp = ( cplMetSp β _Qp) | ||
I hope someone will enjoy solving (proving) the simple equations, inequalities, and calculations from this mathbox. I have proved these problems (theorems) using the Milpgame proof assistant. (It can be downloaded from https://us.metamath.org/other/milpgame/milpgame.html.) | ||
Theorem | problem1 34949 | Practice problem 1. Clues: 5p4e9 12375 3p2e5 12368 eqtri 2759 oveq1i 7422. (Contributed by Filip Cernatescu, 16-Mar-2019.) (Proof modification is discouraged.) |
β’ ((3 + 2) + 4) = 9 | ||
Theorem | problem2 34950 | Practice problem 2. Clues: oveq12i 7424 adddiri 11232 add4i 11443 mulcli 11226 recni 11233 2re 12291 3eqtri 2763 10re 12701 5re 12304 1re 11219 4re 12301 eqcomi 2740 5p4e9 12375 oveq1i 7422 df-3 12281. (Contributed by Filip Cernatescu, 16-Mar-2019.) (Revised by AV, 9-Sep-2021.) (Proof modification is discouraged.) |
β’ (((2 Β· ;10) + 5) + ((1 Β· ;10) + 4)) = ((3 Β· ;10) + 9) | ||
Theorem | problem3 34951 | Practice problem 3. Clues: eqcomi 2740 eqtri 2759 subaddrii 11554 recni 11233 4re 12301 3re 12297 1re 11219 df-4 12282 addcomi 11410. (Contributed by Filip Cernatescu, 16-Mar-2019.) (Proof modification is discouraged.) |
β’ π΄ β β & β’ (π΄ + 3) = 4 β β’ π΄ = 1 | ||
Theorem | problem4 34952 | Practice problem 4. Clues: pm3.2i 470 eqcomi 2740 eqtri 2759 subaddrii 11554 recni 11233 7re 12310 6re 12307 ax-1cn 11172 df-7 12285 ax-mp 5 oveq1i 7422 3cn 12298 2cn 12292 df-3 12281 mullidi 11224 subdiri 11669 mp3an 1460 mulcli 11226 subadd23 11477 oveq2i 7423 oveq12i 7424 3t2e6 12383 mulcomi 11227 subcli 11541 biimpri 227 subadd2i 11553. (Contributed by Filip Cernatescu, 16-Mar-2019.) (Proof modification is discouraged.) |
β’ π΄ β β & β’ π΅ β β & β’ (π΄ + π΅) = 3 & β’ ((3 Β· π΄) + (2 Β· π΅)) = 7 β β’ (π΄ = 1 β§ π΅ = 2) | ||
Theorem | problem5 34953 | Practice problem 5. Clues: 3brtr3i 5177 mpbi 229 breqtri 5173 ltaddsubi 11780 remulcli 11235 2re 12291 3re 12297 9re 12316 eqcomi 2740 mvlladdi 11483 3cn 6cn 12308 eqtr3i 2761 6p3e9 12377 addcomi 11410 ltdiv1ii 12148 6re 12307 nngt0i 12256 2nn 12290 divcan3i 11965 recni 11233 2cn 12292 2ne0 12321 mpbir 230 eqtri 2759 mulcomi 11227 3t2e6 12383 divmuli 11973. (Contributed by Filip Cernatescu, 16-Mar-2019.) (Proof modification is discouraged.) |
β’ π΄ β β & β’ ((2 Β· π΄) + 3) < 9 β β’ π΄ < 3 | ||
Theorem | quad3 34954 | Variant of quadratic equation with discriminant expanded. (Contributed by Filip Cernatescu, 19-Oct-2019.) |
β’ π β β & β’ π΄ β β & β’ π΄ β 0 & β’ π΅ β β & β’ πΆ β β & β’ ((π΄ Β· (πβ2)) + ((π΅ Β· π) + πΆ)) = 0 β β’ (π = ((-π΅ + (ββ((π΅β2) β (4 Β· (π΄ Β· πΆ))))) / (2 Β· π΄)) β¨ π = ((-π΅ β (ββ((π΅β2) β (4 Β· (π΄ Β· πΆ))))) / (2 Β· π΄))) | ||
Theorem | climuzcnv 34955* | Utility lemma to convert between π β€ π and π β (β€β₯βπ) in limit theorems. (Contributed by Paul Chapman, 10-Nov-2012.) |
β’ (π β β β ((π β (β€β₯βπ) β π) β (π β β β (π β€ π β π)))) | ||
Theorem | sinccvglem 34956* | ((sinβπ₯) / π₯) β 1 as (real) π₯ β 0. (Contributed by Paul Chapman, 10-Nov-2012.) (Revised by Mario Carneiro, 21-May-2014.) |
β’ (π β πΉ:ββΆ(β β {0})) & β’ (π β πΉ β 0) & β’ πΊ = (π₯ β (β β {0}) β¦ ((sinβπ₯) / π₯)) & β’ π» = (π₯ β β β¦ (1 β ((π₯β2) / 3))) & β’ (π β π β β) & β’ ((π β§ π β (β€β₯βπ)) β (absβ(πΉβπ)) < 1) β β’ (π β (πΊ β πΉ) β 1) | ||
Theorem | sinccvg 34957* | ((sinβπ₯) / π₯) β 1 as (real) π₯ β 0. (Contributed by Paul Chapman, 10-Nov-2012.) (Proof shortened by Mario Carneiro, 21-May-2014.) |
β’ ((πΉ:ββΆ(β β {0}) β§ πΉ β 0) β ((π₯ β (β β {0}) β¦ ((sinβπ₯) / π₯)) β πΉ) β 1) | ||
Theorem | circum 34958* | The circumference of a circle of radius π , defined as the limit as π β +β of the perimeter of an inscribed n-sided isogons, is ((2 Β· Ο) Β· π ). (Contributed by Paul Chapman, 10-Nov-2012.) (Proof shortened by Mario Carneiro, 21-May-2014.) |
β’ π΄ = ((2 Β· Ο) / π) & β’ π = (π β β β¦ ((2 Β· π) Β· (π Β· (sinβ(π΄ / 2))))) & β’ π β β β β’ π β ((2 Β· Ο) Β· π ) | ||
Theorem | elfzm12 34959 | Membership in a curtailed finite sequence of integers. (Contributed by Paul Chapman, 17-Nov-2012.) |
β’ (π β β β (π β (1...(π β 1)) β π β (1...π))) | ||
Theorem | nn0seqcvg 34960* | A strictly-decreasing nonnegative integer sequence with initial term π reaches zero by the π th term. Inference version. (Contributed by Paul Chapman, 31-Mar-2011.) |
β’ πΉ:β0βΆβ0 & β’ π = (πΉβ0) & β’ (π β β0 β ((πΉβ(π + 1)) β 0 β (πΉβ(π + 1)) < (πΉβπ))) β β’ (πΉβπ) = 0 | ||
Theorem | lediv2aALT 34961 | Division of both sides of 'less than or equal to' by a nonnegative number. (Contributed by Paul Chapman, 7-Sep-2007.) (New usage is discouraged.) (Proof modification is discouraged.) |
β’ (((π΄ β β β§ 0 < π΄) β§ (π΅ β β β§ 0 < π΅) β§ (πΆ β β β§ 0 β€ πΆ)) β (π΄ β€ π΅ β (πΆ / π΅) β€ (πΆ / π΄))) | ||
Theorem | abs2sqlei 34962 | The absolute values of two numbers compare as their squares. (Contributed by Paul Chapman, 7-Sep-2007.) |
β’ π΄ β β & β’ π΅ β β β β’ ((absβπ΄) β€ (absβπ΅) β ((absβπ΄)β2) β€ ((absβπ΅)β2)) | ||
Theorem | abs2sqlti 34963 | The absolute values of two numbers compare as their squares. (Contributed by Paul Chapman, 7-Sep-2007.) |
β’ π΄ β β & β’ π΅ β β β β’ ((absβπ΄) < (absβπ΅) β ((absβπ΄)β2) < ((absβπ΅)β2)) | ||
Theorem | abs2sqle 34964 | The absolute values of two numbers compare as their squares. (Contributed by Paul Chapman, 7-Sep-2007.) |
β’ ((π΄ β β β§ π΅ β β) β ((absβπ΄) β€ (absβπ΅) β ((absβπ΄)β2) β€ ((absβπ΅)β2))) | ||
Theorem | abs2sqlt 34965 | The absolute values of two numbers compare as their squares. (Contributed by Paul Chapman, 7-Sep-2007.) |
β’ ((π΄ β β β§ π΅ β β) β ((absβπ΄) < (absβπ΅) β ((absβπ΄)β2) < ((absβπ΅)β2))) | ||
Theorem | abs2difi 34966 | Difference of absolute values. (Contributed by Paul Chapman, 7-Sep-2007.) |
β’ π΄ β β & β’ π΅ β β β β’ ((absβπ΄) β (absβπ΅)) β€ (absβ(π΄ β π΅)) | ||
Theorem | abs2difabsi 34967 | Absolute value of difference of absolute values. (Contributed by Paul Chapman, 7-Sep-2007.) |
β’ π΄ β β & β’ π΅ β β β β’ (absβ((absβπ΄) β (absβπ΅))) β€ (absβ(π΄ β π΅)) | ||
Theorem | currybi 34968 | Biconditional version of Curry's paradox. If some proposition π amounts to the self-referential statement "This very statement is equivalent to π", then π is true. See bj-currypara 35740 in BJ's mathbox for the classical version. (Contributed by Adrian Ducourtial, 18-Mar-2025.) |
β’ ((π β (π β π)) β π) | ||
Syntax | ccloneop 34969 | Syntax for the function of the class of operations on a set. |
class CloneOp | ||
Definition | df-cloneop 34970* | Define the function that sends a set to the class of clone-theoretic operations on the set. For convenience, we take an operation on π to be a function on finite sequences of elements of π (rather than tuples) with values in π. Following line 6 of [Szendrei] p. 11, the arity π of an operation (here, the length of the sequences at which the operation is defined) is always finite and non-zero, whence π is taken to be a non-zero finite ordinal. (Contributed by Adrian Ducourtial, 3-Apr-2025.) |
β’ CloneOp = (π β V β¦ {π₯ β£ βπ β (Ο β 1o)π₯ β (π βm (π βm π))}) | ||
Syntax | cprj 34971 | Syntax for the function of projections on sets. |
class prj | ||
Definition | df-prj 34972* | Define the function that, for a set π, arity π, and index π, returns the π-th π-ary projection on π. This is the π-ary operation on π that, for any sequence of π elements of π, returns the element having index π. (Contributed by Adrian Ducourtial, 3-Apr-2025.) |
β’ prj = (π β V β¦ (π β (Ο β 1o), π β π β¦ (π₯ β (π βm π) β¦ (π₯βπ)))) | ||
Syntax | csuppos 34973 | Syntax for the function of superpositions. |
class suppos | ||
Definition | df-suppos 34974* | Define the function that, when given an π-ary operation π and π many π-ary operations (πββ ), ..., (πββͺ π), returns the superposition of π with the (πβπ), itself another π-ary operation on π. Given π₯ (a sequence of π arguments in π), the superposition effectively applies each of the (πβπ) to π₯, then applies π to the resulting sequence of π function values. This can be seen as a generalized version of function composition; see paragraph 3 of [Szendrei] p. 11. (Contributed by Adrian Ducourtial, 3-Apr-2025.) |
β’ suppos = (π β V β¦ (π β (Ο β 1o), π β (Ο β 1o) β¦ (π β (π βm (π βm π)), π β ((π βm (π βm π)) βm π) β¦ (π₯ β (π βm π) β¦ (πβ(π β π β¦ ((πβπ)βπ₯))))))) | ||
Theorem | axextprim 34975 | ax-ext 2702 without distinct variable conditions or defined symbols. (Contributed by Scott Fenton, 13-Oct-2010.) |
β’ Β¬ βπ₯ Β¬ ((π₯ β π¦ β π₯ β π§) β ((π₯ β π§ β π₯ β π¦) β π¦ = π§)) | ||
Theorem | axrepprim 34976 | ax-rep 5285 without distinct variable conditions or defined symbols. (Contributed by Scott Fenton, 13-Oct-2010.) |
β’ Β¬ βπ₯ Β¬ (Β¬ βπ¦ Β¬ βπ§(π β π§ = π¦) β βπ§ Β¬ ((βπ¦ π§ β π₯ β Β¬ βπ₯(βπ§ π₯ β π¦ β Β¬ βπ¦π)) β Β¬ (Β¬ βπ₯(βπ§ π₯ β π¦ β Β¬ βπ¦π) β βπ¦ π§ β π₯))) | ||
Theorem | axunprim 34977 | ax-un 7729 without distinct variable conditions or defined symbols. (Contributed by Scott Fenton, 13-Oct-2010.) |
β’ Β¬ βπ₯ Β¬ βπ¦(Β¬ βπ₯(π¦ β π₯ β Β¬ π₯ β π§) β π¦ β π₯) | ||
Theorem | axpowprim 34978 | ax-pow 5363 without distinct variable conditions or defined symbols. (Contributed by Scott Fenton, 13-Oct-2010.) |
β’ (βπ₯ Β¬ βπ¦(βπ₯(Β¬ βπ§ Β¬ π₯ β π¦ β βπ¦ π₯ β π§) β π¦ β π₯) β π₯ = π¦) | ||
Theorem | axregprim 34979 | ax-reg 9591 without distinct variable conditions or defined symbols. (Contributed by Scott Fenton, 13-Oct-2010.) |
β’ (π₯ β π¦ β Β¬ βπ₯(π₯ β π¦ β Β¬ βπ§(π§ β π₯ β Β¬ π§ β π¦))) | ||
Theorem | axinfprim 34980 | ax-inf 9637 without distinct variable conditions or defined symbols. (New usage is discouraged.) (Contributed by Scott Fenton, 13-Oct-2010.) |
β’ Β¬ βπ₯ Β¬ (π¦ β π§ β Β¬ (π¦ β π₯ β Β¬ βπ¦(π¦ β π₯ β Β¬ βπ§(π¦ β π§ β Β¬ π§ β π₯)))) | ||
Theorem | axacprim 34981 | ax-ac 10458 without distinct variable conditions or defined symbols. (New usage is discouraged.) (Contributed by Scott Fenton, 26-Oct-2010.) |
β’ Β¬ βπ₯ Β¬ βπ¦βπ§(βπ₯ Β¬ (π¦ β π§ β Β¬ π§ β π€) β Β¬ βπ€ Β¬ βπ¦ Β¬ ((Β¬ βπ€(π¦ β π§ β (π§ β π€ β (π¦ β π€ β Β¬ π€ β π₯))) β π¦ = π€) β Β¬ (π¦ = π€ β Β¬ βπ€(π¦ β π§ β (π§ β π€ β (π¦ β π€ β Β¬ π€ β π₯)))))) | ||
Theorem | untelirr 34982* | We call a class "untanged" if all its members are not members of themselves. The term originates from Isbell (see citation in dfon2 35069). Using this concept, we can avoid a lot of the uses of the Axiom of Regularity. Here, we prove a series of properties of untanged classes. First, we prove that an untangled class is not a member of itself. (Contributed by Scott Fenton, 28-Feb-2011.) |
β’ (βπ₯ β π΄ Β¬ π₯ β π₯ β Β¬ π΄ β π΄) | ||
Theorem | untuni 34983* | The union of a class is untangled iff all its members are untangled. (Contributed by Scott Fenton, 28-Feb-2011.) |
β’ (βπ₯ β βͺ π΄ Β¬ π₯ β π₯ β βπ¦ β π΄ βπ₯ β π¦ Β¬ π₯ β π₯) | ||
Theorem | untsucf 34984* | If a class is untangled, then so is its successor. (Contributed by Scott Fenton, 28-Feb-2011.) (Revised by Mario Carneiro, 11-Dec-2016.) |
β’ β²π¦π΄ β β’ (βπ₯ β π΄ Β¬ π₯ β π₯ β βπ¦ β suc π΄ Β¬ π¦ β π¦) | ||
Theorem | unt0 34985 | The null set is untangled. (Contributed by Scott Fenton, 10-Mar-2011.) (Proof shortened by Andrew Salmon, 27-Aug-2011.) |
β’ βπ₯ β β Β¬ π₯ β π₯ | ||
Theorem | untint 34986* | If there is an untangled element of a class, then the intersection of the class is untangled. (Contributed by Scott Fenton, 1-Mar-2011.) |
β’ (βπ₯ β π΄ βπ¦ β π₯ Β¬ π¦ β π¦ β βπ¦ β β© π΄ Β¬ π¦ β π¦) | ||
Theorem | efrunt 34987* | If π΄ is well-founded by E, then it is untangled. (Contributed by Scott Fenton, 1-Mar-2011.) |
β’ ( E Fr π΄ β βπ₯ β π΄ Β¬ π₯ β π₯) | ||
Theorem | untangtr 34988* | A transitive class is untangled iff its elements are. (Contributed by Scott Fenton, 7-Mar-2011.) |
β’ (Tr π΄ β (βπ₯ β π΄ Β¬ π₯ β π₯ β βπ₯ β π΄ βπ¦ β π₯ Β¬ π¦ β π¦)) | ||
Theorem | 3jaodd 34989 | Double deduction form of 3jaoi 1426. (Contributed by Scott Fenton, 20-Apr-2011.) |
β’ (π β (π β (π β π))) & β’ (π β (π β (π β π))) & β’ (π β (π β (π β π))) β β’ (π β (π β ((π β¨ π β¨ π) β π))) | ||
Theorem | 3orit 34990 | Closed form of 3ori 1423. (Contributed by Scott Fenton, 20-Apr-2011.) |
β’ ((π β¨ π β¨ π) β ((Β¬ π β§ Β¬ π) β π)) | ||
Theorem | biimpexp 34991 | A biconditional in the antecedent is the same as two implications. (Contributed by Scott Fenton, 12-Dec-2010.) |
β’ (((π β π) β π) β ((π β π) β ((π β π) β π))) | ||
Theorem | nepss 34992 | Two classes are unequal iff their intersection is a proper subset of one of them. (Contributed by Scott Fenton, 23-Feb-2011.) |
β’ (π΄ β π΅ β ((π΄ β© π΅) β π΄ β¨ (π΄ β© π΅) β π΅)) | ||
Theorem | 3ccased 34993 | Triple disjunction form of ccased 1036. (Contributed by Scott Fenton, 27-Oct-2013.) (Revised by Mario Carneiro, 19-Apr-2014.) |
β’ (π β ((π β§ π) β π)) & β’ (π β ((π β§ π) β π)) & β’ (π β ((π β§ π) β π)) & β’ (π β ((π β§ π) β π)) & β’ (π β ((π β§ π) β π)) & β’ (π β ((π β§ π) β π)) & β’ (π β ((π β§ π) β π)) & β’ (π β ((π β§ π) β π)) & β’ (π β ((π β§ π) β π)) β β’ (π β (((π β¨ π β¨ π) β§ (π β¨ π β¨ π)) β π)) | ||
Theorem | dfso3 34994* | Expansion of the definition of a strict order. (Contributed by Scott Fenton, 6-Jun-2016.) |
β’ (π Or π΄ β βπ₯ β π΄ βπ¦ β π΄ βπ§ β π΄ (Β¬ π₯π π₯ β§ ((π₯π π¦ β§ π¦π π§) β π₯π π§) β§ (π₯π π¦ β¨ π₯ = π¦ β¨ π¦π π₯))) | ||
Theorem | brtpid1 34995 | A binary relation involving unordered triples. (Contributed by Scott Fenton, 7-Jun-2016.) |
β’ π΄{β¨π΄, π΅β©, πΆ, π·}π΅ | ||
Theorem | brtpid2 34996 | A binary relation involving unordered triples. (Contributed by Scott Fenton, 7-Jun-2016.) |
β’ π΄{πΆ, β¨π΄, π΅β©, π·}π΅ | ||
Theorem | brtpid3 34997 | A binary relation involving unordered triples. (Contributed by Scott Fenton, 7-Jun-2016.) |
β’ π΄{πΆ, π·, β¨π΄, π΅β©}π΅ | ||
Theorem | iota5f 34998* | A method for computing iota. (Contributed by Scott Fenton, 13-Dec-2017.) |
β’ β²π₯π & β’ β²π₯π΄ & β’ ((π β§ π΄ β π) β (π β π₯ = π΄)) β β’ ((π β§ π΄ β π) β (β©π₯π) = π΄) | ||
Theorem | jath 34999 | Closed form of ja 186. Proved using the completeness script. (Proof modification is discouraged.) (Contributed by Scott Fenton, 13-Dec-2021.) |
β’ ((Β¬ π β π) β ((π β π) β ((π β π) β π))) | ||
Theorem | xpab 35000* | Cartesian product of two class abstractions. (Contributed by Scott Fenton, 19-Aug-2024.) |
β’ ({π₯ β£ π} Γ {π¦ β£ π}) = {β¨π₯, π¦β© β£ (π β§ π)} |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |