![]() |
Metamath
Proof Explorer Theorem List (p. 347 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 | ||
Syntax | cmevl 34601 | The evaluation function of a model. |
class mEval | ||
Syntax | cmdl 34602 | The set of models. |
class mMdl | ||
Syntax | cusyn 34603 | The syntax function applied to elements of the model. |
class mUSyn | ||
Syntax | cgmdl 34604 | The set of models in a grammatical formal system. |
class mGMdl | ||
Syntax | cmitp 34605 | The interpretation function of the model. |
class mItp | ||
Syntax | cmfitp 34606 | The evaluation function derived from the interpretation. |
class mFromItp | ||
Definition | df-muv 34607 | Define the universe of a model. (Contributed by Mario Carneiro, 14-Jul-2016.) |
β’ mUV = Slot 7 | ||
Definition | df-mfsh 34608 | Define the freshness relation of a model. (Contributed by Mario Carneiro, 14-Jul-2016.) |
β’ mFresh = Slot ;19 | ||
Definition | df-mevl 34609 | Define the evaluation function of a model. (Contributed by Mario Carneiro, 14-Jul-2016.) |
β’ mEval = Slot ;20 | ||
Definition | df-mvl 34610* | Define the set of valuations. (Contributed by Mario Carneiro, 14-Jul-2016.) |
β’ mVL = (π‘ β V β¦ Xπ£ β (mVRβπ‘)((mUVβπ‘) β {((mTypeβπ‘)βπ£)})) | ||
Definition | df-mvsb 34611* | 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 34612* | Define the set of freshness relations. (Contributed by Mario Carneiro, 14-Jul-2016.) |
β’ mFRel = (π‘ β V β¦ {π β π« ((mUVβπ‘) Γ (mUVβπ‘)) β£ (β‘π = π β§ βπ β (mVTβπ‘)βπ€ β (π« (mUVβπ‘) β© Fin)βπ£ β ((mUVβπ‘) β {π})π€ β (π β {π£}))}) | ||
Definition | df-mdl 34613* | 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 34614* | 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 34615* | 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 34616* | 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 34617* | 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 34618 | Completion of a metric space. |
class cplMetSp | ||
Syntax | chlb 34619 | Embeddings for a direct limit. |
class HomLimB | ||
Syntax | chlim 34620 | Direct limit structure. |
class HomLim | ||
Syntax | cpfl 34621 | Polynomial extension field. |
class polyFld | ||
Syntax | csf1 34622 | Splitting field for a single polynomial (auxiliary). |
class splitFld1 | ||
Syntax | csf 34623 | Splitting field for a finite set of polynomials. |
class splitFld | ||
Syntax | cpsl 34624 | Splitting field for a sequence of polynomials. |
class polySplitLim | ||
Definition | df-cplmet 34625* | 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 34626* | 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 34627* | 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 34628* | 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 34629* |
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 34630* | 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 34631* | 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 34632 | Integral elements of a ring. |
class ZRing | ||
Syntax | cgf 34633 | Galois finite field. |
class GF | ||
Syntax | cgfo 34634 | Galois limit field. |
class GFβ | ||
Syntax | ceqp 34635 | Equivalence relation for df-qp 34646. |
class ~Qp | ||
Syntax | crqp 34636 | Equivalence relation representatives for df-qp 34646. |
class /Qp | ||
Syntax | cqp 34637 | The set of π-adic rational numbers. |
class Qp | ||
Syntax | czp 34638 | The set of π-adic integers. (Not to be confused with czn 21052.) |
class Zp | ||
Syntax | cqpa 34639 | Algebraic completion of the π-adic rational numbers. |
class _Qp | ||
Syntax | ccp 34640 | Metric completion of _Qp. |
class Cp | ||
Definition | df-zrng 34641 | Define the subring of integral elements in a ring. (Contributed by Mario Carneiro, 2-Dec-2014.) |
β’ ZRing = (π β V β¦ (π IntgRing ran (β€RHomβπ))) | ||
Definition | df-gf 34642* | 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 34643* | 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 34644* | 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 34645* | 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 34646* | 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 34647 | Define the π-adic integers, as a subset of the π-adic rationals. (Contributed by Mario Carneiro, 2-Dec-2014.) |
β’ Zp = (ZRing β Qp) | ||
Definition | df-qpa 34648* | 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 34649 | 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 34650 | Practice problem 1. Clues: 5p4e9 12370 3p2e5 12363 eqtri 2761 oveq1i 7419. (Contributed by Filip Cernatescu, 16-Mar-2019.) (Proof modification is discouraged.) |
β’ ((3 + 2) + 4) = 9 | ||
Theorem | problem2 34651 | Practice problem 2. Clues: oveq12i 7421 adddiri 11227 add4i 11438 mulcli 11221 recni 11228 2re 12286 3eqtri 2765 10re 12696 5re 12299 1re 11214 4re 12296 eqcomi 2742 5p4e9 12370 oveq1i 7419 df-3 12276. (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 34652 | Practice problem 3. Clues: eqcomi 2742 eqtri 2761 subaddrii 11549 recni 11228 4re 12296 3re 12292 1re 11214 df-4 12277 addcomi 11405. (Contributed by Filip Cernatescu, 16-Mar-2019.) (Proof modification is discouraged.) |
β’ π΄ β β & β’ (π΄ + 3) = 4 β β’ π΄ = 1 | ||
Theorem | problem4 34653 | Practice problem 4. Clues: pm3.2i 472 eqcomi 2742 eqtri 2761 subaddrii 11549 recni 11228 7re 12305 6re 12302 ax-1cn 11168 df-7 12280 ax-mp 5 oveq1i 7419 3cn 12293 2cn 12287 df-3 12276 mullidi 11219 subdiri 11664 mp3an 1462 mulcli 11221 subadd23 11472 oveq2i 7420 oveq12i 7421 3t2e6 12378 mulcomi 11222 subcli 11536 biimpri 227 subadd2i 11548. (Contributed by Filip Cernatescu, 16-Mar-2019.) (Proof modification is discouraged.) |
β’ π΄ β β & β’ π΅ β β & β’ (π΄ + π΅) = 3 & β’ ((3 Β· π΄) + (2 Β· π΅)) = 7 β β’ (π΄ = 1 β§ π΅ = 2) | ||
Theorem | problem5 34654 | Practice problem 5. Clues: 3brtr3i 5178 mpbi 229 breqtri 5174 ltaddsubi 11775 remulcli 11230 2re 12286 3re 12292 9re 12311 eqcomi 2742 mvlladdi 11478 3cn 6cn 12303 eqtr3i 2763 6p3e9 12372 addcomi 11405 ltdiv1ii 12143 6re 12302 nngt0i 12251 2nn 12285 divcan3i 11960 recni 11228 2cn 12287 2ne0 12316 mpbir 230 eqtri 2761 mulcomi 11222 3t2e6 12378 divmuli 11968. (Contributed by Filip Cernatescu, 16-Mar-2019.) (Proof modification is discouraged.) |
β’ π΄ β β & β’ ((2 Β· π΄) + 3) < 9 β β’ π΄ < 3 | ||
Theorem | quad3 34655 | 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 34656* | Utility lemma to convert between π β€ π and π β (β€β₯βπ) in limit theorems. (Contributed by Paul Chapman, 10-Nov-2012.) |
β’ (π β β β ((π β (β€β₯βπ) β π) β (π β β β (π β€ π β π)))) | ||
Theorem | sinccvglem 34657* | ((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 34658* | ((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 34659* | 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 34660 | Membership in a curtailed finite sequence of integers. (Contributed by Paul Chapman, 17-Nov-2012.) |
β’ (π β β β (π β (1...(π β 1)) β π β (1...π))) | ||
Theorem | nn0seqcvg 34661* | 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 34662 | 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 34663 | 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 34664 | 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 34665 | 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 34666 | 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 34667 | Difference of absolute values. (Contributed by Paul Chapman, 7-Sep-2007.) |
β’ π΄ β β & β’ π΅ β β β β’ ((absβπ΄) β (absβπ΅)) β€ (absβ(π΄ β π΅)) | ||
Theorem | abs2difabsi 34668 | Absolute value of difference of absolute values. (Contributed by Paul Chapman, 7-Sep-2007.) |
β’ π΄ β β & β’ π΅ β β β β’ (absβ((absβπ΄) β (absβπ΅))) β€ (absβ(π΄ β π΅)) | ||
Theorem | currybi 34669 | 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 35436 in BJ's mathbox for the classical version. (Contributed by Adrian Ducourtial, 18-Mar-2025.) |
β’ ((π β (π β π)) β π) | ||
Theorem | axextprim 34670 | ax-ext 2704 without distinct variable conditions or defined symbols. (Contributed by Scott Fenton, 13-Oct-2010.) |
β’ Β¬ βπ₯ Β¬ ((π₯ β π¦ β π₯ β π§) β ((π₯ β π§ β π₯ β π¦) β π¦ = π§)) | ||
Theorem | axrepprim 34671 | ax-rep 5286 without distinct variable conditions or defined symbols. (Contributed by Scott Fenton, 13-Oct-2010.) |
β’ Β¬ βπ₯ Β¬ (Β¬ βπ¦ Β¬ βπ§(π β π§ = π¦) β βπ§ Β¬ ((βπ¦ π§ β π₯ β Β¬ βπ₯(βπ§ π₯ β π¦ β Β¬ βπ¦π)) β Β¬ (Β¬ βπ₯(βπ§ π₯ β π¦ β Β¬ βπ¦π) β βπ¦ π§ β π₯))) | ||
Theorem | axunprim 34672 | ax-un 7725 without distinct variable conditions or defined symbols. (Contributed by Scott Fenton, 13-Oct-2010.) |
β’ Β¬ βπ₯ Β¬ βπ¦(Β¬ βπ₯(π¦ β π₯ β Β¬ π₯ β π§) β π¦ β π₯) | ||
Theorem | axpowprim 34673 | ax-pow 5364 without distinct variable conditions or defined symbols. (Contributed by Scott Fenton, 13-Oct-2010.) |
β’ (βπ₯ Β¬ βπ¦(βπ₯(Β¬ βπ§ Β¬ π₯ β π¦ β βπ¦ π₯ β π§) β π¦ β π₯) β π₯ = π¦) | ||
Theorem | axregprim 34674 | ax-reg 9587 without distinct variable conditions or defined symbols. (Contributed by Scott Fenton, 13-Oct-2010.) |
β’ (π₯ β π¦ β Β¬ βπ₯(π₯ β π¦ β Β¬ βπ§(π§ β π₯ β Β¬ π§ β π¦))) | ||
Theorem | axinfprim 34675 | ax-inf 9633 without distinct variable conditions or defined symbols. (New usage is discouraged.) (Contributed by Scott Fenton, 13-Oct-2010.) |
β’ Β¬ βπ₯ Β¬ (π¦ β π§ β Β¬ (π¦ β π₯ β Β¬ βπ¦(π¦ β π₯ β Β¬ βπ§(π¦ β π§ β Β¬ π§ β π₯)))) | ||
Theorem | axacprim 34676 | ax-ac 10454 without distinct variable conditions or defined symbols. (New usage is discouraged.) (Contributed by Scott Fenton, 26-Oct-2010.) |
β’ Β¬ βπ₯ Β¬ βπ¦βπ§(βπ₯ Β¬ (π¦ β π§ β Β¬ π§ β π€) β Β¬ βπ€ Β¬ βπ¦ Β¬ ((Β¬ βπ€(π¦ β π§ β (π§ β π€ β (π¦ β π€ β Β¬ π€ β π₯))) β π¦ = π€) β Β¬ (π¦ = π€ β Β¬ βπ€(π¦ β π§ β (π§ β π€ β (π¦ β π€ β Β¬ π€ β π₯)))))) | ||
Theorem | untelirr 34677* | We call a class "untanged" if all its members are not members of themselves. The term originates from Isbell (see citation in dfon2 34764). 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 34678* | The union of a class is untangled iff all its members are untangled. (Contributed by Scott Fenton, 28-Feb-2011.) |
β’ (βπ₯ β βͺ π΄ Β¬ π₯ β π₯ β βπ¦ β π΄ βπ₯ β π¦ Β¬ π₯ β π₯) | ||
Theorem | untsucf 34679* | 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 34680 | The null set is untangled. (Contributed by Scott Fenton, 10-Mar-2011.) (Proof shortened by Andrew Salmon, 27-Aug-2011.) |
β’ βπ₯ β β Β¬ π₯ β π₯ | ||
Theorem | untint 34681* | 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 34682* | If π΄ is well-founded by E, then it is untangled. (Contributed by Scott Fenton, 1-Mar-2011.) |
β’ ( E Fr π΄ β βπ₯ β π΄ Β¬ π₯ β π₯) | ||
Theorem | untangtr 34683* | A transitive class is untangled iff its elements are. (Contributed by Scott Fenton, 7-Mar-2011.) |
β’ (Tr π΄ β (βπ₯ β π΄ Β¬ π₯ β π₯ β βπ₯ β π΄ βπ¦ β π₯ Β¬ π¦ β π¦)) | ||
Theorem | 3jaodd 34684 | Double deduction form of 3jaoi 1428. (Contributed by Scott Fenton, 20-Apr-2011.) |
β’ (π β (π β (π β π))) & β’ (π β (π β (π β π))) & β’ (π β (π β (π β π))) β β’ (π β (π β ((π β¨ π β¨ π) β π))) | ||
Theorem | 3orit 34685 | Closed form of 3ori 1425. (Contributed by Scott Fenton, 20-Apr-2011.) |
β’ ((π β¨ π β¨ π) β ((Β¬ π β§ Β¬ π) β π)) | ||
Theorem | biimpexp 34686 | A biconditional in the antecedent is the same as two implications. (Contributed by Scott Fenton, 12-Dec-2010.) |
β’ (((π β π) β π) β ((π β π) β ((π β π) β π))) | ||
Theorem | nepss 34687 | Two classes are unequal iff their intersection is a proper subset of one of them. (Contributed by Scott Fenton, 23-Feb-2011.) |
β’ (π΄ β π΅ β ((π΄ β© π΅) β π΄ β¨ (π΄ β© π΅) β π΅)) | ||
Theorem | 3ccased 34688 | Triple disjunction form of ccased 1038. (Contributed by Scott Fenton, 27-Oct-2013.) (Revised by Mario Carneiro, 19-Apr-2014.) |
β’ (π β ((π β§ π) β π)) & β’ (π β ((π β§ π) β π)) & β’ (π β ((π β§ π) β π)) & β’ (π β ((π β§ π) β π)) & β’ (π β ((π β§ π) β π)) & β’ (π β ((π β§ π) β π)) & β’ (π β ((π β§ π) β π)) & β’ (π β ((π β§ π) β π)) & β’ (π β ((π β§ π) β π)) β β’ (π β (((π β¨ π β¨ π) β§ (π β¨ π β¨ π)) β π)) | ||
Theorem | dfso3 34689* | Expansion of the definition of a strict order. (Contributed by Scott Fenton, 6-Jun-2016.) |
β’ (π Or π΄ β βπ₯ β π΄ βπ¦ β π΄ βπ§ β π΄ (Β¬ π₯π π₯ β§ ((π₯π π¦ β§ π¦π π§) β π₯π π§) β§ (π₯π π¦ β¨ π₯ = π¦ β¨ π¦π π₯))) | ||
Theorem | brtpid1 34690 | A binary relation involving unordered triples. (Contributed by Scott Fenton, 7-Jun-2016.) |
β’ π΄{β¨π΄, π΅β©, πΆ, π·}π΅ | ||
Theorem | brtpid2 34691 | A binary relation involving unordered triples. (Contributed by Scott Fenton, 7-Jun-2016.) |
β’ π΄{πΆ, β¨π΄, π΅β©, π·}π΅ | ||
Theorem | brtpid3 34692 | A binary relation involving unordered triples. (Contributed by Scott Fenton, 7-Jun-2016.) |
β’ π΄{πΆ, π·, β¨π΄, π΅β©}π΅ | ||
Theorem | iota5f 34693* | A method for computing iota. (Contributed by Scott Fenton, 13-Dec-2017.) |
β’ β²π₯π & β’ β²π₯π΄ & β’ ((π β§ π΄ β π) β (π β π₯ = π΄)) β β’ ((π β§ π΄ β π) β (β©π₯π) = π΄) | ||
Theorem | jath 34694 | Closed form of ja 186. Proved using the completeness script. (Proof modification is discouraged.) (Contributed by Scott Fenton, 13-Dec-2021.) |
β’ ((Β¬ π β π) β ((π β π) β ((π β π) β π))) | ||
Theorem | xpab 34695* | Cartesian product of two class abstractions. (Contributed by Scott Fenton, 19-Aug-2024.) |
β’ ({π₯ β£ π} Γ {π¦ β£ π}) = {β¨π₯, π¦β© β£ (π β§ π)} | ||
Theorem | nnuni 34696 | The union of a finite ordinal is a finite ordinal. (Contributed by Scott Fenton, 17-Oct-2024.) |
β’ (π΄ β Ο β βͺ π΄ β Ο) | ||
Theorem | sqdivzi 34697 | Distribution of square over division. (Contributed by Scott Fenton, 7-Jun-2013.) |
β’ π΄ β β & β’ π΅ β β β β’ (π΅ β 0 β ((π΄ / π΅)β2) = ((π΄β2) / (π΅β2))) | ||
Theorem | supfz 34698 | The supremum of a finite sequence of integers. (Contributed by Scott Fenton, 8-Aug-2013.) |
β’ (π β (β€β₯βπ) β sup((π...π), β€, < ) = π) | ||
Theorem | inffz 34699 | The infimum of a finite sequence of integers. (Contributed by Scott Fenton, 8-Aug-2013.) (Revised by AV, 10-Oct-2021.) |
β’ (π β (β€β₯βπ) β inf((π...π), β€, < ) = π) | ||
Theorem | fz0n 34700 | The sequence (0...(π β 1)) is empty iff π is zero. (Contributed by Scott Fenton, 16-May-2014.) |
β’ (π β β0 β ((0...(π β 1)) = β β π = 0)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |