![]() |
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-30166) |
![]() (30167-31689) |
![]() (31690-47842) |
Type | Label | Description |
---|---|---|
Statement | ||
Syntax | cmfitp 34601 | The evaluation function derived from the interpretation. |
class mFromItp | ||
Definition | df-muv 34602 | Define the universe of a model. (Contributed by Mario Carneiro, 14-Jul-2016.) |
β’ mUV = Slot 7 | ||
Definition | df-mfsh 34603 | Define the freshness relation of a model. (Contributed by Mario Carneiro, 14-Jul-2016.) |
β’ mFresh = Slot ;19 | ||
Definition | df-mevl 34604 | Define the evaluation function of a model. (Contributed by Mario Carneiro, 14-Jul-2016.) |
β’ mEval = Slot ;20 | ||
Definition | df-mvl 34605* | Define the set of valuations. (Contributed by Mario Carneiro, 14-Jul-2016.) |
β’ mVL = (π‘ β V β¦ Xπ£ β (mVRβπ‘)((mUVβπ‘) β {((mTypeβπ‘)βπ£)})) | ||
Definition | df-mvsb 34606* | 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 34607* | Define the set of freshness relations. (Contributed by Mario Carneiro, 14-Jul-2016.) |
β’ mFRel = (π‘ β V β¦ {π β π« ((mUVβπ‘) Γ (mUVβπ‘)) β£ (β‘π = π β§ βπ β (mVTβπ‘)βπ€ β (π« (mUVβπ‘) β© Fin)βπ£ β ((mUVβπ‘) β {π})π€ β (π β {π£}))}) | ||
Definition | df-mdl 34608* | 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 34609* | 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 34610* | 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 34611* | 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 34612* | 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 34613 | Completion of a metric space. |
class cplMetSp | ||
Syntax | chlb 34614 | Embeddings for a direct limit. |
class HomLimB | ||
Syntax | chlim 34615 | Direct limit structure. |
class HomLim | ||
Syntax | cpfl 34616 | Polynomial extension field. |
class polyFld | ||
Syntax | csf1 34617 | Splitting field for a single polynomial (auxiliary). |
class splitFld1 | ||
Syntax | csf 34618 | Splitting field for a finite set of polynomials. |
class splitFld | ||
Syntax | cpsl 34619 | Splitting field for a sequence of polynomials. |
class polySplitLim | ||
Definition | df-cplmet 34620* | 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 34621* | 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 34622* | 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 34623* | 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 34624* |
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 34625* | 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 34626* | 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 34627 | Integral elements of a ring. |
class ZRing | ||
Syntax | cgf 34628 | Galois finite field. |
class GF | ||
Syntax | cgfo 34629 | Galois limit field. |
class GFβ | ||
Syntax | ceqp 34630 | Equivalence relation for df-qp 34641. |
class ~Qp | ||
Syntax | crqp 34631 | Equivalence relation representatives for df-qp 34641. |
class /Qp | ||
Syntax | cqp 34632 | The set of π-adic rational numbers. |
class Qp | ||
Syntax | czp 34633 | The set of π-adic integers. (Not to be confused with czn 21051.) |
class Zp | ||
Syntax | cqpa 34634 | Algebraic completion of the π-adic rational numbers. |
class _Qp | ||
Syntax | ccp 34635 | Metric completion of _Qp. |
class Cp | ||
Definition | df-zrng 34636 | Define the subring of integral elements in a ring. (Contributed by Mario Carneiro, 2-Dec-2014.) |
β’ ZRing = (π β V β¦ (π IntgRing ran (β€RHomβπ))) | ||
Definition | df-gf 34637* | 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 34638* | 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 34639* | 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 34640* | 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 34641* | 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 34642 | Define the π-adic integers, as a subset of the π-adic rationals. (Contributed by Mario Carneiro, 2-Dec-2014.) |
β’ Zp = (ZRing β Qp) | ||
Definition | df-qpa 34643* | 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 34644 | 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 34645 | Practice problem 1. Clues: 5p4e9 12369 3p2e5 12362 eqtri 2760 oveq1i 7418. (Contributed by Filip Cernatescu, 16-Mar-2019.) (Proof modification is discouraged.) |
β’ ((3 + 2) + 4) = 9 | ||
Theorem | problem2 34646 | Practice problem 2. Clues: oveq12i 7420 adddiri 11226 add4i 11437 mulcli 11220 recni 11227 2re 12285 3eqtri 2764 10re 12695 5re 12298 1re 11213 4re 12295 eqcomi 2741 5p4e9 12369 oveq1i 7418 df-3 12275. (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 34647 | Practice problem 3. Clues: eqcomi 2741 eqtri 2760 subaddrii 11548 recni 11227 4re 12295 3re 12291 1re 11213 df-4 12276 addcomi 11404. (Contributed by Filip Cernatescu, 16-Mar-2019.) (Proof modification is discouraged.) |
β’ π΄ β β & β’ (π΄ + 3) = 4 β β’ π΄ = 1 | ||
Theorem | problem4 34648 | Practice problem 4. Clues: pm3.2i 471 eqcomi 2741 eqtri 2760 subaddrii 11548 recni 11227 7re 12304 6re 12301 ax-1cn 11167 df-7 12279 ax-mp 5 oveq1i 7418 3cn 12292 2cn 12286 df-3 12275 mullidi 11218 subdiri 11663 mp3an 1461 mulcli 11220 subadd23 11471 oveq2i 7419 oveq12i 7420 3t2e6 12377 mulcomi 11221 subcli 11535 biimpri 227 subadd2i 11547. (Contributed by Filip Cernatescu, 16-Mar-2019.) (Proof modification is discouraged.) |
β’ π΄ β β & β’ π΅ β β & β’ (π΄ + π΅) = 3 & β’ ((3 Β· π΄) + (2 Β· π΅)) = 7 β β’ (π΄ = 1 β§ π΅ = 2) | ||
Theorem | problem5 34649 | Practice problem 5. Clues: 3brtr3i 5177 mpbi 229 breqtri 5173 ltaddsubi 11774 remulcli 11229 2re 12285 3re 12291 9re 12310 eqcomi 2741 mvlladdi 11477 3cn 6cn 12302 eqtr3i 2762 6p3e9 12371 addcomi 11404 ltdiv1ii 12142 6re 12301 nngt0i 12250 2nn 12284 divcan3i 11959 recni 11227 2cn 12286 2ne0 12315 mpbir 230 eqtri 2760 mulcomi 11221 3t2e6 12377 divmuli 11967. (Contributed by Filip Cernatescu, 16-Mar-2019.) (Proof modification is discouraged.) |
β’ π΄ β β & β’ ((2 Β· π΄) + 3) < 9 β β’ π΄ < 3 | ||
Theorem | quad3 34650 | 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 34651* | Utility lemma to convert between π β€ π and π β (β€β₯βπ) in limit theorems. (Contributed by Paul Chapman, 10-Nov-2012.) |
β’ (π β β β ((π β (β€β₯βπ) β π) β (π β β β (π β€ π β π)))) | ||
Theorem | sinccvglem 34652* | ((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 34653* | ((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 34654* | 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 34655 | Membership in a curtailed finite sequence of integers. (Contributed by Paul Chapman, 17-Nov-2012.) |
β’ (π β β β (π β (1...(π β 1)) β π β (1...π))) | ||
Theorem | nn0seqcvg 34656* | 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 34657 | 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 34658 | 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 34659 | 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 34660 | 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 34661 | 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 34662 | Difference of absolute values. (Contributed by Paul Chapman, 7-Sep-2007.) |
β’ π΄ β β & β’ π΅ β β β β’ ((absβπ΄) β (absβπ΅)) β€ (absβ(π΄ β π΅)) | ||
Theorem | abs2difabsi 34663 | Absolute value of difference of absolute values. (Contributed by Paul Chapman, 7-Sep-2007.) |
β’ π΄ β β & β’ π΅ β β β β’ (absβ((absβπ΄) β (absβπ΅))) β€ (absβ(π΄ β π΅)) | ||
Theorem | currybi 34664 | 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 35431 in BJ's mathbox for the classical version. (Contributed by Adrian Ducourtial, 18-Mar-2025.) |
β’ ((π β (π β π)) β π) | ||
Theorem | axextprim 34665 | ax-ext 2703 without distinct variable conditions or defined symbols. (Contributed by Scott Fenton, 13-Oct-2010.) |
β’ Β¬ βπ₯ Β¬ ((π₯ β π¦ β π₯ β π§) β ((π₯ β π§ β π₯ β π¦) β π¦ = π§)) | ||
Theorem | axrepprim 34666 | ax-rep 5285 without distinct variable conditions or defined symbols. (Contributed by Scott Fenton, 13-Oct-2010.) |
β’ Β¬ βπ₯ Β¬ (Β¬ βπ¦ Β¬ βπ§(π β π§ = π¦) β βπ§ Β¬ ((βπ¦ π§ β π₯ β Β¬ βπ₯(βπ§ π₯ β π¦ β Β¬ βπ¦π)) β Β¬ (Β¬ βπ₯(βπ§ π₯ β π¦ β Β¬ βπ¦π) β βπ¦ π§ β π₯))) | ||
Theorem | axunprim 34667 | ax-un 7724 without distinct variable conditions or defined symbols. (Contributed by Scott Fenton, 13-Oct-2010.) |
β’ Β¬ βπ₯ Β¬ βπ¦(Β¬ βπ₯(π¦ β π₯ β Β¬ π₯ β π§) β π¦ β π₯) | ||
Theorem | axpowprim 34668 | ax-pow 5363 without distinct variable conditions or defined symbols. (Contributed by Scott Fenton, 13-Oct-2010.) |
β’ (βπ₯ Β¬ βπ¦(βπ₯(Β¬ βπ§ Β¬ π₯ β π¦ β βπ¦ π₯ β π§) β π¦ β π₯) β π₯ = π¦) | ||
Theorem | axregprim 34669 | ax-reg 9586 without distinct variable conditions or defined symbols. (Contributed by Scott Fenton, 13-Oct-2010.) |
β’ (π₯ β π¦ β Β¬ βπ₯(π₯ β π¦ β Β¬ βπ§(π§ β π₯ β Β¬ π§ β π¦))) | ||
Theorem | axinfprim 34670 | ax-inf 9632 without distinct variable conditions or defined symbols. (New usage is discouraged.) (Contributed by Scott Fenton, 13-Oct-2010.) |
β’ Β¬ βπ₯ Β¬ (π¦ β π§ β Β¬ (π¦ β π₯ β Β¬ βπ¦(π¦ β π₯ β Β¬ βπ§(π¦ β π§ β Β¬ π§ β π₯)))) | ||
Theorem | axacprim 34671 | ax-ac 10453 without distinct variable conditions or defined symbols. (New usage is discouraged.) (Contributed by Scott Fenton, 26-Oct-2010.) |
β’ Β¬ βπ₯ Β¬ βπ¦βπ§(βπ₯ Β¬ (π¦ β π§ β Β¬ π§ β π€) β Β¬ βπ€ Β¬ βπ¦ Β¬ ((Β¬ βπ€(π¦ β π§ β (π§ β π€ β (π¦ β π€ β Β¬ π€ β π₯))) β π¦ = π€) β Β¬ (π¦ = π€ β Β¬ βπ€(π¦ β π§ β (π§ β π€ β (π¦ β π€ β Β¬ π€ β π₯)))))) | ||
Theorem | untelirr 34672* | We call a class "untanged" if all its members are not members of themselves. The term originates from Isbell (see citation in dfon2 34759). 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 34673* | The union of a class is untangled iff all its members are untangled. (Contributed by Scott Fenton, 28-Feb-2011.) |
β’ (βπ₯ β βͺ π΄ Β¬ π₯ β π₯ β βπ¦ β π΄ βπ₯ β π¦ Β¬ π₯ β π₯) | ||
Theorem | untsucf 34674* | 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 34675 | The null set is untangled. (Contributed by Scott Fenton, 10-Mar-2011.) (Proof shortened by Andrew Salmon, 27-Aug-2011.) |
β’ βπ₯ β β Β¬ π₯ β π₯ | ||
Theorem | untint 34676* | 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 34677* | If π΄ is well-founded by E, then it is untangled. (Contributed by Scott Fenton, 1-Mar-2011.) |
β’ ( E Fr π΄ β βπ₯ β π΄ Β¬ π₯ β π₯) | ||
Theorem | untangtr 34678* | A transitive class is untangled iff its elements are. (Contributed by Scott Fenton, 7-Mar-2011.) |
β’ (Tr π΄ β (βπ₯ β π΄ Β¬ π₯ β π₯ β βπ₯ β π΄ βπ¦ β π₯ Β¬ π¦ β π¦)) | ||
Theorem | 3jaodd 34679 | Double deduction form of 3jaoi 1427. (Contributed by Scott Fenton, 20-Apr-2011.) |
β’ (π β (π β (π β π))) & β’ (π β (π β (π β π))) & β’ (π β (π β (π β π))) β β’ (π β (π β ((π β¨ π β¨ π) β π))) | ||
Theorem | 3orit 34680 | Closed form of 3ori 1424. (Contributed by Scott Fenton, 20-Apr-2011.) |
β’ ((π β¨ π β¨ π) β ((Β¬ π β§ Β¬ π) β π)) | ||
Theorem | biimpexp 34681 | A biconditional in the antecedent is the same as two implications. (Contributed by Scott Fenton, 12-Dec-2010.) |
β’ (((π β π) β π) β ((π β π) β ((π β π) β π))) | ||
Theorem | nepss 34682 | Two classes are unequal iff their intersection is a proper subset of one of them. (Contributed by Scott Fenton, 23-Feb-2011.) |
β’ (π΄ β π΅ β ((π΄ β© π΅) β π΄ β¨ (π΄ β© π΅) β π΅)) | ||
Theorem | 3ccased 34683 | Triple disjunction form of ccased 1037. (Contributed by Scott Fenton, 27-Oct-2013.) (Revised by Mario Carneiro, 19-Apr-2014.) |
β’ (π β ((π β§ π) β π)) & β’ (π β ((π β§ π) β π)) & β’ (π β ((π β§ π) β π)) & β’ (π β ((π β§ π) β π)) & β’ (π β ((π β§ π) β π)) & β’ (π β ((π β§ π) β π)) & β’ (π β ((π β§ π) β π)) & β’ (π β ((π β§ π) β π)) & β’ (π β ((π β§ π) β π)) β β’ (π β (((π β¨ π β¨ π) β§ (π β¨ π β¨ π)) β π)) | ||
Theorem | dfso3 34684* | Expansion of the definition of a strict order. (Contributed by Scott Fenton, 6-Jun-2016.) |
β’ (π Or π΄ β βπ₯ β π΄ βπ¦ β π΄ βπ§ β π΄ (Β¬ π₯π π₯ β§ ((π₯π π¦ β§ π¦π π§) β π₯π π§) β§ (π₯π π¦ β¨ π₯ = π¦ β¨ π¦π π₯))) | ||
Theorem | brtpid1 34685 | A binary relation involving unordered triples. (Contributed by Scott Fenton, 7-Jun-2016.) |
β’ π΄{β¨π΄, π΅β©, πΆ, π·}π΅ | ||
Theorem | brtpid2 34686 | A binary relation involving unordered triples. (Contributed by Scott Fenton, 7-Jun-2016.) |
β’ π΄{πΆ, β¨π΄, π΅β©, π·}π΅ | ||
Theorem | brtpid3 34687 | A binary relation involving unordered triples. (Contributed by Scott Fenton, 7-Jun-2016.) |
β’ π΄{πΆ, π·, β¨π΄, π΅β©}π΅ | ||
Theorem | iota5f 34688* | A method for computing iota. (Contributed by Scott Fenton, 13-Dec-2017.) |
β’ β²π₯π & β’ β²π₯π΄ & β’ ((π β§ π΄ β π) β (π β π₯ = π΄)) β β’ ((π β§ π΄ β π) β (β©π₯π) = π΄) | ||
Theorem | jath 34689 | Closed form of ja 186. Proved using the completeness script. (Proof modification is discouraged.) (Contributed by Scott Fenton, 13-Dec-2021.) |
β’ ((Β¬ π β π) β ((π β π) β ((π β π) β π))) | ||
Theorem | xpab 34690* | Cartesian product of two class abstractions. (Contributed by Scott Fenton, 19-Aug-2024.) |
β’ ({π₯ β£ π} Γ {π¦ β£ π}) = {β¨π₯, π¦β© β£ (π β§ π)} | ||
Theorem | nnuni 34691 | The union of a finite ordinal is a finite ordinal. (Contributed by Scott Fenton, 17-Oct-2024.) |
β’ (π΄ β Ο β βͺ π΄ β Ο) | ||
Theorem | sqdivzi 34692 | Distribution of square over division. (Contributed by Scott Fenton, 7-Jun-2013.) |
β’ π΄ β β & β’ π΅ β β β β’ (π΅ β 0 β ((π΄ / π΅)β2) = ((π΄β2) / (π΅β2))) | ||
Theorem | supfz 34693 | The supremum of a finite sequence of integers. (Contributed by Scott Fenton, 8-Aug-2013.) |
β’ (π β (β€β₯βπ) β sup((π...π), β€, < ) = π) | ||
Theorem | inffz 34694 | The infimum of a finite sequence of integers. (Contributed by Scott Fenton, 8-Aug-2013.) (Revised by AV, 10-Oct-2021.) |
β’ (π β (β€β₯βπ) β inf((π...π), β€, < ) = π) | ||
Theorem | fz0n 34695 | The sequence (0...(π β 1)) is empty iff π is zero. (Contributed by Scott Fenton, 16-May-2014.) |
β’ (π β β0 β ((0...(π β 1)) = β β π = 0)) | ||
Theorem | shftvalg 34696 | Value of a sequence shifted by π΄. (Contributed by Scott Fenton, 16-Dec-2017.) |
β’ ((πΉ β π β§ π΄ β β β§ π΅ β β) β ((πΉ shift π΄)βπ΅) = (πΉβ(π΅ β π΄))) | ||
Theorem | divcnvlin 34697* | Limit of the ratio of two linear functions. (Contributed by Scott Fenton, 17-Dec-2017.) |
β’ π = (β€β₯βπ) & β’ (π β π β β€) & β’ (π β π΄ β β) & β’ (π β π΅ β β€) & β’ (π β πΉ β π) & β’ ((π β§ π β π) β (πΉβπ) = ((π + π΄) / (π + π΅))) β β’ (π β πΉ β 1) | ||
Theorem | climlec3 34698* | Comparison of a constant to the limit of a sequence. (Contributed by Scott Fenton, 5-Jan-2018.) |
β’ π = (β€β₯βπ) & β’ (π β π β β€) & β’ (π β π΅ β β) & β’ (π β πΉ β π΄) & β’ ((π β§ π β π) β (πΉβπ) β β) & β’ ((π β§ π β π) β (πΉβπ) β€ π΅) β β’ (π β π΄ β€ π΅) | ||
Theorem | logi 34699 | Calculate the logarithm of i. (Contributed by Scott Fenton, 13-Apr-2020.) |
β’ (logβi) = (i Β· (Ο / 2)) | ||
Theorem | iexpire 34700 | i raised to itself is real. (Contributed by Scott Fenton, 13-Apr-2020.) |
β’ (iβπi) β β |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |