![]() |
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-30438) |
![]() (30439-31961) |
![]() (31962-47939) |
Type | Label | Description |
---|---|---|
Statement | ||
Syntax | cusyn 34901 | The syntax function applied to elements of the model. |
class mUSyn | ||
Syntax | cgmdl 34902 | The set of models in a grammatical formal system. |
class mGMdl | ||
Syntax | cmitp 34903 | The interpretation function of the model. |
class mItp | ||
Syntax | cmfitp 34904 | The evaluation function derived from the interpretation. |
class mFromItp | ||
Definition | df-muv 34905 | Define the universe of a model. (Contributed by Mario Carneiro, 14-Jul-2016.) |
β’ mUV = Slot 7 | ||
Definition | df-mfsh 34906 | Define the freshness relation of a model. (Contributed by Mario Carneiro, 14-Jul-2016.) |
β’ mFresh = Slot ;19 | ||
Definition | df-mevl 34907 | Define the evaluation function of a model. (Contributed by Mario Carneiro, 14-Jul-2016.) |
β’ mEval = Slot ;20 | ||
Definition | df-mvl 34908* | Define the set of valuations. (Contributed by Mario Carneiro, 14-Jul-2016.) |
β’ mVL = (π‘ β V β¦ Xπ£ β (mVRβπ‘)((mUVβπ‘) β {((mTypeβπ‘)βπ£)})) | ||
Definition | df-mvsb 34909* | 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 34910* | Define the set of freshness relations. (Contributed by Mario Carneiro, 14-Jul-2016.) |
β’ mFRel = (π‘ β V β¦ {π β π« ((mUVβπ‘) Γ (mUVβπ‘)) β£ (β‘π = π β§ βπ β (mVTβπ‘)βπ€ β (π« (mUVβπ‘) β© Fin)βπ£ β ((mUVβπ‘) β {π})π€ β (π β {π£}))}) | ||
Definition | df-mdl 34911* | 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 34912* | 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 34913* | 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 34914* | 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 34915* | 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 34916 | Completion of a metric space. |
class cplMetSp | ||
Syntax | chlb 34917 | Embeddings for a direct limit. |
class HomLimB | ||
Syntax | chlim 34918 | Direct limit structure. |
class HomLim | ||
Syntax | cpfl 34919 | Polynomial extension field. |
class polyFld | ||
Syntax | csf1 34920 | Splitting field for a single polynomial (auxiliary). |
class splitFld1 | ||
Syntax | csf 34921 | Splitting field for a finite set of polynomials. |
class splitFld | ||
Syntax | cpsl 34922 | Splitting field for a sequence of polynomials. |
class polySplitLim | ||
Definition | df-cplmet 34923* | 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 34924* | 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 34925* | 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 34926* | 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 34927* |
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 34928* | 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 34929* | 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 34930 | Integral elements of a ring. |
class ZRing | ||
Syntax | cgf 34931 | Galois finite field. |
class GF | ||
Syntax | cgfo 34932 | Galois limit field. |
class GFβ | ||
Syntax | ceqp 34933 | Equivalence relation for df-qp 34944. |
class ~Qp | ||
Syntax | crqp 34934 | Equivalence relation representatives for df-qp 34944. |
class /Qp | ||
Syntax | cqp 34935 | The set of π-adic rational numbers. |
class Qp | ||
Syntax | czp 34936 | The set of π-adic integers. (Not to be confused with czn 21271.) |
class Zp | ||
Syntax | cqpa 34937 | Algebraic completion of the π-adic rational numbers. |
class _Qp | ||
Syntax | ccp 34938 | Metric completion of _Qp. |
class Cp | ||
Definition | df-zrng 34939 | Define the subring of integral elements in a ring. (Contributed by Mario Carneiro, 2-Dec-2014.) |
β’ ZRing = (π β V β¦ (π IntgRing ran (β€RHomβπ))) | ||
Definition | df-gf 34940* | 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 34941* | 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 34942* | 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 34943* | 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 34944* | 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 34945 | Define the π-adic integers, as a subset of the π-adic rationals. (Contributed by Mario Carneiro, 2-Dec-2014.) |
β’ Zp = (ZRing β Qp) | ||
Definition | df-qpa 34946* | 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 34947 | 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 34948 | Practice problem 1. Clues: 5p4e9 12374 3p2e5 12367 eqtri 2758 oveq1i 7421. (Contributed by Filip Cernatescu, 16-Mar-2019.) (Proof modification is discouraged.) |
β’ ((3 + 2) + 4) = 9 | ||
Theorem | problem2 34949 | Practice problem 2. Clues: oveq12i 7423 adddiri 11231 add4i 11442 mulcli 11225 recni 11232 2re 12290 3eqtri 2762 10re 12700 5re 12303 1re 11218 4re 12300 eqcomi 2739 5p4e9 12374 oveq1i 7421 df-3 12280. (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 34950 | Practice problem 3. Clues: eqcomi 2739 eqtri 2758 subaddrii 11553 recni 11232 4re 12300 3re 12296 1re 11218 df-4 12281 addcomi 11409. (Contributed by Filip Cernatescu, 16-Mar-2019.) (Proof modification is discouraged.) |
β’ π΄ β β & β’ (π΄ + 3) = 4 β β’ π΄ = 1 | ||
Theorem | problem4 34951 | Practice problem 4. Clues: pm3.2i 469 eqcomi 2739 eqtri 2758 subaddrii 11553 recni 11232 7re 12309 6re 12306 ax-1cn 11170 df-7 12284 ax-mp 5 oveq1i 7421 3cn 12297 2cn 12291 df-3 12280 mullidi 11223 subdiri 11668 mp3an 1459 mulcli 11225 subadd23 11476 oveq2i 7422 oveq12i 7423 3t2e6 12382 mulcomi 11226 subcli 11540 biimpri 227 subadd2i 11552. (Contributed by Filip Cernatescu, 16-Mar-2019.) (Proof modification is discouraged.) |
β’ π΄ β β & β’ π΅ β β & β’ (π΄ + π΅) = 3 & β’ ((3 Β· π΄) + (2 Β· π΅)) = 7 β β’ (π΄ = 1 β§ π΅ = 2) | ||
Theorem | problem5 34952 | Practice problem 5. Clues: 3brtr3i 5176 mpbi 229 breqtri 5172 ltaddsubi 11779 remulcli 11234 2re 12290 3re 12296 9re 12315 eqcomi 2739 mvlladdi 11482 3cn 6cn 12307 eqtr3i 2760 6p3e9 12376 addcomi 11409 ltdiv1ii 12147 6re 12306 nngt0i 12255 2nn 12289 divcan3i 11964 recni 11232 2cn 12291 2ne0 12320 mpbir 230 eqtri 2758 mulcomi 11226 3t2e6 12382 divmuli 11972. (Contributed by Filip Cernatescu, 16-Mar-2019.) (Proof modification is discouraged.) |
β’ π΄ β β & β’ ((2 Β· π΄) + 3) < 9 β β’ π΄ < 3 | ||
Theorem | quad3 34953 | 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 34954* | Utility lemma to convert between π β€ π and π β (β€β₯βπ) in limit theorems. (Contributed by Paul Chapman, 10-Nov-2012.) |
β’ (π β β β ((π β (β€β₯βπ) β π) β (π β β β (π β€ π β π)))) | ||
Theorem | sinccvglem 34955* | ((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 34956* | ((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 34957* | 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 34958 | Membership in a curtailed finite sequence of integers. (Contributed by Paul Chapman, 17-Nov-2012.) |
β’ (π β β β (π β (1...(π β 1)) β π β (1...π))) | ||
Theorem | nn0seqcvg 34959* | 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 34960 | 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 34961 | 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 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 | abs2sqle 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 | abs2sqlt 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 | abs2difi 34965 | Difference of absolute values. (Contributed by Paul Chapman, 7-Sep-2007.) |
β’ π΄ β β & β’ π΅ β β β β’ ((absβπ΄) β (absβπ΅)) β€ (absβ(π΄ β π΅)) | ||
Theorem | abs2difabsi 34966 | Absolute value of difference of absolute values. (Contributed by Paul Chapman, 7-Sep-2007.) |
β’ π΄ β β & β’ π΅ β β β β’ (absβ((absβπ΄) β (absβπ΅))) β€ (absβ(π΄ β π΅)) | ||
Theorem | currybi 34967 | 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 35739 in BJ's mathbox for the classical version. (Contributed by Adrian Ducourtial, 18-Mar-2025.) |
β’ ((π β (π β π)) β π) | ||
Syntax | ccloneop 34968 | Syntax for the function of the class of operations on a set. |
class CloneOp | ||
Definition | df-cloneop 34969* | 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 34970 | Syntax for the function of projections on sets. |
class prj | ||
Definition | df-prj 34971* | 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 34972 | Syntax for the function of superpositions. |
class suppos | ||
Definition | df-suppos 34973* | 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 34974 | ax-ext 2701 without distinct variable conditions or defined symbols. (Contributed by Scott Fenton, 13-Oct-2010.) |
β’ Β¬ βπ₯ Β¬ ((π₯ β π¦ β π₯ β π§) β ((π₯ β π§ β π₯ β π¦) β π¦ = π§)) | ||
Theorem | axrepprim 34975 | ax-rep 5284 without distinct variable conditions or defined symbols. (Contributed by Scott Fenton, 13-Oct-2010.) |
β’ Β¬ βπ₯ Β¬ (Β¬ βπ¦ Β¬ βπ§(π β π§ = π¦) β βπ§ Β¬ ((βπ¦ π§ β π₯ β Β¬ βπ₯(βπ§ π₯ β π¦ β Β¬ βπ¦π)) β Β¬ (Β¬ βπ₯(βπ§ π₯ β π¦ β Β¬ βπ¦π) β βπ¦ π§ β π₯))) | ||
Theorem | axunprim 34976 | ax-un 7727 without distinct variable conditions or defined symbols. (Contributed by Scott Fenton, 13-Oct-2010.) |
β’ Β¬ βπ₯ Β¬ βπ¦(Β¬ βπ₯(π¦ β π₯ β Β¬ π₯ β π§) β π¦ β π₯) | ||
Theorem | axpowprim 34977 | ax-pow 5362 without distinct variable conditions or defined symbols. (Contributed by Scott Fenton, 13-Oct-2010.) |
β’ (βπ₯ Β¬ βπ¦(βπ₯(Β¬ βπ§ Β¬ π₯ β π¦ β βπ¦ π₯ β π§) β π¦ β π₯) β π₯ = π¦) | ||
Theorem | axregprim 34978 | ax-reg 9589 without distinct variable conditions or defined symbols. (Contributed by Scott Fenton, 13-Oct-2010.) |
β’ (π₯ β π¦ β Β¬ βπ₯(π₯ β π¦ β Β¬ βπ§(π§ β π₯ β Β¬ π§ β π¦))) | ||
Theorem | axinfprim 34979 | ax-inf 9635 without distinct variable conditions or defined symbols. (New usage is discouraged.) (Contributed by Scott Fenton, 13-Oct-2010.) |
β’ Β¬ βπ₯ Β¬ (π¦ β π§ β Β¬ (π¦ β π₯ β Β¬ βπ¦(π¦ β π₯ β Β¬ βπ§(π¦ β π§ β Β¬ π§ β π₯)))) | ||
Theorem | axacprim 34980 | ax-ac 10456 without distinct variable conditions or defined symbols. (New usage is discouraged.) (Contributed by Scott Fenton, 26-Oct-2010.) |
β’ Β¬ βπ₯ Β¬ βπ¦βπ§(βπ₯ Β¬ (π¦ β π§ β Β¬ π§ β π€) β Β¬ βπ€ Β¬ βπ¦ Β¬ ((Β¬ βπ€(π¦ β π§ β (π§ β π€ β (π¦ β π€ β Β¬ π€ β π₯))) β π¦ = π€) β Β¬ (π¦ = π€ β Β¬ βπ€(π¦ β π§ β (π§ β π€ β (π¦ β π€ β Β¬ π€ β π₯)))))) | ||
Theorem | untelirr 34981* | We call a class "untanged" if all its members are not members of themselves. The term originates from Isbell (see citation in dfon2 35068). 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 34982* | The union of a class is untangled iff all its members are untangled. (Contributed by Scott Fenton, 28-Feb-2011.) |
β’ (βπ₯ β βͺ π΄ Β¬ π₯ β π₯ β βπ¦ β π΄ βπ₯ β π¦ Β¬ π₯ β π₯) | ||
Theorem | untsucf 34983* | 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 34984 | The null set is untangled. (Contributed by Scott Fenton, 10-Mar-2011.) (Proof shortened by Andrew Salmon, 27-Aug-2011.) |
β’ βπ₯ β β Β¬ π₯ β π₯ | ||
Theorem | untint 34985* | 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 34986* | If π΄ is well-founded by E, then it is untangled. (Contributed by Scott Fenton, 1-Mar-2011.) |
β’ ( E Fr π΄ β βπ₯ β π΄ Β¬ π₯ β π₯) | ||
Theorem | untangtr 34987* | A transitive class is untangled iff its elements are. (Contributed by Scott Fenton, 7-Mar-2011.) |
β’ (Tr π΄ β (βπ₯ β π΄ Β¬ π₯ β π₯ β βπ₯ β π΄ βπ¦ β π₯ Β¬ π¦ β π¦)) | ||
Theorem | 3jaodd 34988 | Double deduction form of 3jaoi 1425. (Contributed by Scott Fenton, 20-Apr-2011.) |
β’ (π β (π β (π β π))) & β’ (π β (π β (π β π))) & β’ (π β (π β (π β π))) β β’ (π β (π β ((π β¨ π β¨ π) β π))) | ||
Theorem | 3orit 34989 | Closed form of 3ori 1422. (Contributed by Scott Fenton, 20-Apr-2011.) |
β’ ((π β¨ π β¨ π) β ((Β¬ π β§ Β¬ π) β π)) | ||
Theorem | biimpexp 34990 | A biconditional in the antecedent is the same as two implications. (Contributed by Scott Fenton, 12-Dec-2010.) |
β’ (((π β π) β π) β ((π β π) β ((π β π) β π))) | ||
Theorem | nepss 34991 | Two classes are unequal iff their intersection is a proper subset of one of them. (Contributed by Scott Fenton, 23-Feb-2011.) |
β’ (π΄ β π΅ β ((π΄ β© π΅) β π΄ β¨ (π΄ β© π΅) β π΅)) | ||
Theorem | 3ccased 34992 | Triple disjunction form of ccased 1035. (Contributed by Scott Fenton, 27-Oct-2013.) (Revised by Mario Carneiro, 19-Apr-2014.) |
β’ (π β ((π β§ π) β π)) & β’ (π β ((π β§ π) β π)) & β’ (π β ((π β§ π) β π)) & β’ (π β ((π β§ π) β π)) & β’ (π β ((π β§ π) β π)) & β’ (π β ((π β§ π) β π)) & β’ (π β ((π β§ π) β π)) & β’ (π β ((π β§ π) β π)) & β’ (π β ((π β§ π) β π)) β β’ (π β (((π β¨ π β¨ π) β§ (π β¨ π β¨ π)) β π)) | ||
Theorem | dfso3 34993* | Expansion of the definition of a strict order. (Contributed by Scott Fenton, 6-Jun-2016.) |
β’ (π Or π΄ β βπ₯ β π΄ βπ¦ β π΄ βπ§ β π΄ (Β¬ π₯π π₯ β§ ((π₯π π¦ β§ π¦π π§) β π₯π π§) β§ (π₯π π¦ β¨ π₯ = π¦ β¨ π¦π π₯))) | ||
Theorem | brtpid1 34994 | A binary relation involving unordered triples. (Contributed by Scott Fenton, 7-Jun-2016.) |
β’ π΄{β¨π΄, π΅β©, πΆ, π·}π΅ | ||
Theorem | brtpid2 34995 | A binary relation involving unordered triples. (Contributed by Scott Fenton, 7-Jun-2016.) |
β’ π΄{πΆ, β¨π΄, π΅β©, π·}π΅ | ||
Theorem | brtpid3 34996 | A binary relation involving unordered triples. (Contributed by Scott Fenton, 7-Jun-2016.) |
β’ π΄{πΆ, π·, β¨π΄, π΅β©}π΅ | ||
Theorem | iota5f 34997* | A method for computing iota. (Contributed by Scott Fenton, 13-Dec-2017.) |
β’ β²π₯π & β’ β²π₯π΄ & β’ ((π β§ π΄ β π) β (π β π₯ = π΄)) β β’ ((π β§ π΄ β π) β (β©π₯π) = π΄) | ||
Theorem | jath 34998 | Closed form of ja 186. Proved using the completeness script. (Proof modification is discouraged.) (Contributed by Scott Fenton, 13-Dec-2021.) |
β’ ((Β¬ π β π) β ((π β π) β ((π β π) β π))) | ||
Theorem | xpab 34999* | Cartesian product of two class abstractions. (Contributed by Scott Fenton, 19-Aug-2024.) |
β’ ({π₯ β£ π} Γ {π¦ β£ π}) = {β¨π₯, π¦β© β£ (π β§ π)} | ||
Theorem | nnuni 35000 | The union of a finite ordinal is a finite ordinal. (Contributed by Scott Fenton, 17-Oct-2024.) |
β’ (π΄ β Ο β βͺ π΄ β Ο) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |