P. 316 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 31501-31600   *Has distinct variable group(s)

Type	Label	Description
Statement
Syntax	cmvl 31501	The set of valuations.
class mVL
Syntax	cmvsb 31502	Substitution for a valuation.
class mVSubst
Syntax	cmfsh 31503	The freshness relation of a model.
class mFresh
Syntax	cmfr 31504	The set of freshness relations.
class mFRel
Syntax	cmevl 31505	The evaluation function of a model.
class mEval
Syntax	cmdl 31506	The set of models.
class mMdl
Syntax	cusyn 31507	The syntax function applied to elements of the model.
class mUSyn
Syntax	cgmdl 31508	The set of models in a grammatical formal system.
class mGMdl
Syntax	cmitp 31509	The interpretation function of the model.
class mItp
Syntax	cmfitp 31510	The evaluation function derived from the interpretation.
class mFromItp
Definition	df-muv 31511	Define the universe of a model. (Contributed by Mario Carneiro, 14-Jul-2016.)
|- mUV = Slot 7
Definition	df-mfsh 31512	Define the freshness relation of a model. (Contributed by Mario Carneiro, 14-Jul-2016.)
|- mFresh = Slot 8
Definition	df-mevl 31513	Define the evaluation function of a model. (Contributed by Mario Carneiro, 14-Jul-2016.)
|- mEval = Slot 9
Definition	df-mvl 31514*	Define the set of valuations. (Contributed by Mario Carneiro, 14-Jul-2016.)
|- mVL = ( t e. _V |-> X_ v e. (mVR ` t ) ( (mUV ` t ) " { ( (mType ` t ) ` v ) } ) )
Definition	df-mvsb 31515*	Define substitution applied to a valuation. (Contributed by Mario Carneiro, 14-Jul-2016.)
|- mVSubst = ( t e. _V |-> { <. <. s , m >. , x >. | ( ( s e. ran (mSubst ` t ) /\ m e. (mVL ` t ) ) /\ A. v e. (mVR ` t ) m dom (mEval ` t ) ( s ` ( (mVH ` t ) ` v ) ) /\ x = ( v e. (mVR ` t ) |-> ( m (mEval ` t ) ( s ` ( (mVH ` t ) ` v ) ) ) ) ) } )
Definition	df-mfrel 31516*	Define the set of freshness relations. (Contributed by Mario Carneiro, 14-Jul-2016.)
|- mFRel = ( t e. _V |-> { r e. ~P ( (mUV ` t ) X. (mUV ` t ) ) | ( `' r = r /\ A. c e. (mVT ` t ) A. w e. ( ~P (mUV ` t ) i^i Fin ) E. v e. ( (mUV ` t ) " { c } ) w C_ ( r " { v } ) ) } )
Definition	df-mdl 31517*	Define the set of models of a formal system. (Contributed by Mario Carneiro, 14-Jul-2016.)
|- mMdl = { t e. mFS | [. (mUV ` t ) / u ]. [. (mEx ` t ) / x ]. [. (mVL ` t ) / v ]. [. (mEval ` t ) / n ]. [. (mFresh ` t ) / f ]. ( ( u C_ ( (mTC ` t ) X. _V ) /\ f e. (mFRel ` t ) /\ n e. ( u ^pm ( v X. (mEx ` t ) ) ) ) /\ A. m e. v ( ( A. e e. x ( n " { <. m , e >. } ) C_ ( u " { ( 1st ` e ) } ) /\ A. y e. (mVR ` t ) <. m , ( (mVH ` t ) ` y ) >. n ( m ` y ) /\ A. d A. h A. a ( <. d , h , a >. e. (mAx ` t ) -> ( ( A. y A. z ( y d z -> ( m ` y ) f ( m ` z ) ) /\ h C_ ( dom n " { m } ) ) -> m dom n a ) ) ) /\ ( A. s e. ran (mSubst ` t ) A. e e. (mEx ` t ) A. y ( <. s , m >. (mVSubst ` t ) y -> ( n " { <. m , ( s ` e ) >. } ) = ( n " { <. y , e >. } ) ) /\ A. p e. v A. e e. x ( ( m |` ( (mVars ` t ) ` e ) ) = ( p |` ( (mVars ` t ) ` e ) ) -> ( n " { <. m , e >. } ) = ( n " { <. p , e >. } ) ) /\ A. y e. u A. e e. x ( ( m " ( (mVars ` t ) ` e ) ) C_ ( f " { y } ) -> ( n " { <. m , e >. } ) C_ ( f " { y } ) ) ) ) ) }
Definition	df-musyn 31518*	Define the syntax typecode function for the model universe. (Contributed by Mario Carneiro, 14-Jul-2016.)
|- mUSyn = ( t e. _V |-> ( v e. (mUV ` t ) |-> <. ( (mSyn ` t ) ` ( 1st ` v ) ) , ( 2nd ` v ) >. ) )
Definition	df-gmdl 31519*	Define the set of models of a grammatical formal system. (Contributed by Mario Carneiro, 14-Jul-2016.)
|- mGMdl = { t e. (mGFS i^i mMdl ) | ( A. c e. (mTC ` t ) ( (mUV ` t ) " { c } ) C_ ( (mUV ` t ) " { ( (mSyn ` t ) ` c ) } ) /\ A. v e. (mUV ` c ) A. w e. (mUV ` c ) ( v (mFresh ` t ) w <-> v (mFresh ` t ) ( (mUSyn ` t ) ` w ) ) /\ A. m e. (mVL ` t ) A. e e. (mEx ` t ) ( (mEval ` t ) " { <. m , e >. } ) = ( ( (mEval ` t ) " { <. m , ( (mESyn ` t ) ` e ) >. } ) i^i ( (mUV ` t ) " { ( 1st ` e ) } ) ) ) }
Definition	df-mitp 31520*	Define the interpretation function for a model. (Contributed by Mario Carneiro, 14-Jul-2016.)
|- mItp = ( t e. _V |-> ( a e. (mSA ` t ) |-> ( g e. X_ i e. ( (mVars ` t ) ` a ) ( (mUV ` t ) " { ( (mType ` t ) ` i ) } ) |-> ( iota x E. m e. (mVL ` t ) ( g = ( m |` ( (mVars ` t ) ` a ) ) /\ x = ( m (mEval ` t ) a ) ) ) ) ) )
Definition	df-mfitp 31521*	Define a function that produces the evaluation function, given the interpretation function for a model. (Contributed by Mario Carneiro, 14-Jul-2016.)
|- mFromItp = ( t e. _V |-> ( f e. X_ a e. (mSA ` t ) ( ( (mUV ` t ) " { ( ( 1st ` t ) ` a ) } ) ^m X_ i e. ( (mVars ` t ) ` a ) ( (mUV ` t ) " { ( (mType ` t ) ` i ) } ) ) |-> ( iota_ n e. ( (mUV ` t ) ^pm ( (mVL ` t ) X. (mEx ` t ) ) ) A. m e. (mVL ` t ) ( A. v e. (mVR ` t ) <. m , ( (mVH ` t ) ` v ) >. n ( m ` v ) /\ A. e A. a A. g ( e (mST ` t ) <. a , g >. -> <. m , e >. n ( f ` ( i e. ( (mVars ` t ) ` a ) |-> ( m n ( g ` ( (mVH ` t ) ` i ) ) ) ) ) ) /\ A. e e. (mEx ` t ) ( n " { <. m , e >. } ) = ( ( n " { <. m , ( (mESyn ` t ) ` e ) >. } ) i^i ( (mUV ` t ) " { ( 1st ` e ) } ) ) ) ) ) )
20.5.15  Splitting fields
Syntax	citr 31522	Integral subring of a ring.
class IntgRing
Syntax	ccpms 31523	Completion of a metric space.
class cplMetSp
Syntax	chlb 31524	Embeddings for a direct limit.
class HomLimB
Syntax	chlim 31525	Direct limit structure.
class HomLim
Syntax	cpfl 31526	Polynomial extension field.
class polyFld
Syntax	csf1 31527	Splitting field for a single polynomial (auxiliary).
class splitFld1
Syntax	csf 31528	Splitting field for a finite set of polynomials.
class splitFld
Syntax	cpsl 31529	Splitting field for a sequence of polynomials.
class polySplitLim
Definition	df-irng 31530*	Define the subring of elements of r integral over s in a ring. (Contributed by Mario Carneiro, 2-Dec-2014.)
|- IntgRing = ( r e. _V , s e. _V |-> U_ f e. (Monic1p ` ( r ↾s s ) ) ( `' f " { ( 0g ` r ) } ) )
Definition	df-cplmet 31531*	A function which completes the given metric space. (Contributed by Mario Carneiro, 2-Dec-2014.)
|- cplMetSp = ( w e. _V |-> [_ ( ( w ^s NN ) ↾s ( Cau ` ( dist ` w ) ) ) / r ]_ [_ ( Base ` r ) / v ]_ [_ { <. f , g >. | ( { f , g } C_ v /\ A. x e. RR+ E. j e. ZZ ( f |` ( ZZ>= ` j ) ) : ( ZZ>= ` j ) --> ( ( g ` j ) ( ball ` ( dist ` w ) ) x ) ) } / e ]_ ( ( r /.s e ) sSet { <. ( dist ` ndx ) , { <. <. x , y >. , z >. | E. p e. v E. q e. v ( ( x = [ p ] e /\ y = [ q ] e ) /\ ( p oF ( dist ` r ) q ) ~~> z ) } >. } ) )
Definition	df-homlimb 31532*	The input to this function is a sequence (on NN) of homomorphisms F ( n ) : R ( n ) --> R ( n + 1 ). The resulting structure is the direct limit of the direct system so defined. This function returns the pair <. S , G >. where S is the terminal object and G is a sequence of functions such that G ( n ) : R ( n ) --> S and G ( n ) = F ( n ) o. G ( n + 1 ). (Contributed by Mario Carneiro, 2-Dec-2014.)
|- HomLimB = ( f e. _V |-> [_ U_ n e. NN ( { n } X. dom ( f ` n ) ) / v ]_ [_ |^| { s | ( s Er v /\ ( x e. v |-> <. ( ( 1st ` x ) + 1 ) , ( ( f ` ( 1st ` x ) ) ` ( 2nd ` x ) ) >. ) C_ s ) } / e ]_ <. ( v /. e ) , ( n e. NN |-> ( x e. dom ( f ` n ) |-> [ <. n , x >. ] e ) ) >. )
Definition	df-homlim 31533*	The input to this function is a sequence (on NN) of structures R ( n ) and homomorphisms F ( n ) : R ( n ) --> R ( n + 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 = ( r e. _V , f e. _V |-> [_ ( HomLimB ` f ) / e ]_ [_ ( 1st ` e ) / v ]_ [_ ( 2nd ` e ) / g ]_ ( { <. ( Base ` ndx ) , v >. , <. ( +g ` ndx ) , U_ n e. NN ran ( x e. dom ( g ` n ) , y e. dom ( g ` n ) |-> <. <. ( ( g ` n ) ` x ) , ( ( g ` n ) ` y ) >. , ( ( g ` n ) ` ( x ( +g ` ( r ` n ) ) y ) ) >. ) >. , <. ( .r ` ndx ) , U_ n e. NN ran ( x e. dom ( g ` n ) , y e. dom ( g ` n ) |-> <. <. ( ( g ` n ) ` x ) , ( ( g ` n ) ` y ) >. , ( ( g ` n ) ` ( x ( .r ` ( r ` n ) ) y ) ) >. ) >. } u. { <. ( TopOpen ` ndx ) , { s e. ~P v | A. n e. NN ( `' ( g ` n ) " s ) e. ( TopOpen ` ( r ` n ) ) } >. , <. ( dist ` ndx ) , U_ n e. NN ran ( x e. dom ( ( g ` n ) ` n ) , y e. dom ( ( g ` n ) ` n ) |-> <. <. ( ( g ` n ) ` x ) , ( ( g ` n ) ` y ) >. , ( x ( dist ` ( r ` n ) ) y ) >. ) >. , <. ( le ` ndx ) , U_ n e. NN ( `' ( g ` n ) o. ( ( le ` ( r ` n ) ) o. ( g ` n ) ) ) >. } ) )
Definition	df-plfl 31534*	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 = ( r e. _V , p e. _V |-> [_ (Poly1 ` r ) / s ]_ [_ ( (RSpan ` s ) ` { p } ) / i ]_ [_ ( z e. ( Base ` r ) |-> [ ( z ( .s ` s ) ( 1r ` s ) ) ] ( s ~QG i ) ) / f ]_ <. [_ ( s /.s ( s ~QG i ) ) / t ]_ ( ( t toNrmGrp ( iota_ n e. (AbsVal ` t ) ( n o. f ) = ( norm ` r ) ) ) sSet <. ( le ` ndx ) , [_ ( z e. ( Base ` t ) |-> ( iota_ q e. z ( r deg1 q ) < ( r deg1 p ) ) ) / g ]_ ( `' g o. ( ( le ` s ) o. g ) ) >. ) , f >. )
Definition	df-sfl1 31535*	Temporary construction for the splitting field of a polynomial. The inputs are a field r and a polynomial p that we want to split, along with a tuple j in the same format as the output. The output is a tuple <. S , F >. where S is the splitting field and F is an injective homomorphism from the original field r. 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 = ( r e. _V , j e. _V |-> ( p e. (Poly1 ` r ) |-> ( rec ( ( s e. _V , f e. _V |-> [_ ( mPoly ` s ) / m ]_ [_ { g e. ( (Monic1p ` s ) i^i (Irred ` m ) ) | ( g ( ||r ` m ) ( p o. f ) /\ 1 < ( s deg1 g ) ) } / b ]_ if ( ( ( p o. f ) = ( 0g ` m ) \/ b = (/) ) , <. s , f >. , [_ ( glb ` b ) / h ]_ [_ ( s polyFld h ) / t ]_ <. ( 1st ` t ) , ( f o. ( 2nd ` t ) ) >. ) ) , j ) ` ( card ` ( 1 ... ( r deg1 p ) ) ) ) ) )
Definition	df-sfl 31536*	Define the splitting field of a finite collection of polynomials, given a total ordered base field. The output is a tuple <. S , F >. where S is the totally ordered splitting field and F is an injective homomorphism from the original field r. (Contributed by Mario Carneiro, 2-Dec-2014.)
|- splitFld = ( r e. _V , p e. _V |-> ( iota x E. f ( f Isom < , ( lt ` r ) ( ( 1 ... ( # ` p ) ) , p ) /\ x = ( seq 0 ( ( e e. _V , g e. _V |-> ( ( r splitFld1 e ) ` g ) ) , ( f u. { <. 0 , <. r , ( _I |` ( Base ` r ) ) >. >. } ) ) ` ( # ` p ) ) ) ) )
Definition	df-psl 31537*	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 r, a strict order on r, and a sequence p : NN --> ( ~P r i^i 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 = ( r e. _V , p e. ( ( ~P ( Base ` r ) i^i Fin ) ^m NN ) |-> [_ ( 1st o. seq 0 ( ( g e. _V , q e. _V |-> [_ ( 1st ` g ) / e ]_ [_ ( 1st ` e ) / s ]_ [_ ( s splitFld ran ( x e. q |-> ( x o. ( 2nd ` g ) ) ) ) / f ]_ <. f , ( ( 2nd ` g ) o. ( 2nd ` f ) ) >. ) , ( p u. { <. 0 , <. <. r , (/) >. , ( _I |` ( Base ` r ) ) >. >. } ) ) ) / f ]_ ( ( 1st o. ( f shift 1 ) ) HomLim ( 2nd o. f ) ) )
20.5.16  p-adic number fields
Syntax	czr 31538	Integral elements of a ring.
class ZRing
Syntax	cgf 31539	Galois finite field.
class GF
Syntax	cgfo 31540	Galois limit field.
class GF∞
Syntax	ceqp 31541	Equivalence relation for df-qp 31553.
class ~Qp
Syntax	crqp 31542	Equivalence relation representatives for df-qp 31553.
class /Qp
Syntax	cqp 31543	The set of p-adic rational numbers.
class Qp
Syntax	cqpOLD 31544	The set of p-adic rational numbers. (New usage is discouraged.)
class QpOLD
Syntax	czp 31545	The set of p-adic integers. (Not to be confused with czn 19851.)
class Zp
Syntax	cqpa 31546	Algebraic completion of the p-adic rational numbers.
class _Qp
Syntax	ccp 31547	Metric completion of _Qp.
class Cp
Definition	df-zrng 31548	Define the subring of integral elements in a ring. (Contributed by Mario Carneiro, 2-Dec-2014.)
|- ZRing = ( r e. _V |-> ( r IntgRing ran ( ZRHom ` r ) ) )
Definition	df-gf 31549*	Define the Galois finite field of order p ^ n. (Contributed by Mario Carneiro, 2-Dec-2014.)
|- GF = ( p e. Prime , n e. NN |-> [_ (ℤ/nℤ ` p ) / r ]_ ( 1st ` ( r splitFld { [_ (Poly1 ` r ) / s ]_ [_ (var1 ` r ) / x ]_ ( ( ( p ^ n ) (.g ` (mulGrp ` s ) ) x ) ( -g ` s ) x ) } ) ) )
Definition	df-gfoo 31550*	Define the Galois field of order p ^ +oo, as a direct limit of the Galois finite fields. (Contributed by Mario Carneiro, 2-Dec-2014.)
|- GF∞ = ( p e. Prime |-> [_ (ℤ/nℤ ` p ) / r ]_ ( r polySplitLim ( n e. NN |-> { [_ (Poly1 ` r ) / s ]_ [_ (var1 ` r ) / x ]_ ( ( ( p ^ n ) (.g ` (mulGrp ` s ) ) x ) ( -g ` s ) x ) } ) ) )
Definition	df-eqp 31551*	Define an equivalence relation on ZZ-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 sum_ k <_ n f ( k ) ( p ^ k ) is a multiple of p ^ ( n + 1 ) for every n. (Contributed by Mario Carneiro, 2-Dec-2014.)
|- ~Qp = ( p e. Prime |-> { <. f , g >. | ( { f , g } C_ ( ZZ ^m ZZ ) /\ A. n e. ZZ sum_ k e. ( ZZ>= ` -u n ) ( ( ( f ` -u k ) - ( g ` -u k ) ) / ( p ^ ( k + ( n + 1 ) ) ) ) e. ZZ ) } )
Definition	df-rqp 31552*	There is a unique element of ( ZZ ^m ( 0 ... ( p - 1 ) ) ) ~Qp -equivalent to any element of ( ZZ ^m ZZ ), if the sequences are zero for sufficiently large negative values; this function selects that element. (Contributed by Mario Carneiro, 2-Dec-2014.)
|- /Qp = ( p e. Prime |-> (~Qp i^i [_ { f e. ( ZZ ^m ZZ ) | E. x e. ran ZZ>= ( `' f " ( ZZ \ { 0 } ) ) C_ x } / y ]_ ( y X. ( y i^i ( ZZ ^m ( 0 ... ( p - 1 ) ) ) ) ) ) )
Definition	df-qp 31553*	Define the p-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 = ( p e. Prime |-> [_ { h e. ( ZZ ^m ( 0 ... ( p - 1 ) ) ) | E. x e. ran ZZ>= ( `' h " ( ZZ \ { 0 } ) ) C_ x } / b ]_ ( ( { <. ( Base ` ndx ) , b >. , <. ( +g ` ndx ) , ( f e. b , g e. b |-> ( (/Qp ` p ) ` ( f oF + g ) ) ) >. , <. ( .r ` ndx ) , ( f e. b , g e. b |-> ( (/Qp ` p ) ` ( n e. ZZ |-> sum_ k e. ZZ ( ( f ` k ) x. ( g ` ( n - k ) ) ) ) ) ) >. } u. { <. ( le ` ndx ) , { <. f , g >. | ( { f , g } C_ b /\ sum_ k e. ZZ ( ( f ` -u k ) x. ( ( p + 1 ) ^ -u k ) ) < sum_ k e. ZZ ( ( g ` -u k ) x. ( ( p + 1 ) ^ -u k ) ) ) } >. } ) toNrmGrp ( f e. b |-> if ( f = ( ZZ X. { 0 } ) , 0 , ( p ^ -uinf ( ( `' f " ( ZZ \ { 0 } ) ) , RR , < ) ) ) ) ) )
Definition	df-qpOLD 31554*	Define the p-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.) Obsolete version of df-qp 31553 as of 10-Oct-2021. (New usage is discouraged.)
|- QpOLD = ( p e. Prime |-> [_ { h e. ( ZZ ^m ( 0 ... ( p - 1 ) ) ) | E. x e. ran ZZ>= ( `' h " ( ZZ \ { 0 } ) ) C_ x } / b ]_ ( ( { <. ( Base ` ndx ) , b >. , <. ( +g ` ndx ) , ( f e. b , g e. b |-> ( (/Qp ` p ) ` ( f oF + g ) ) ) >. , <. ( .r ` ndx ) , ( f e. b , g e. b |-> ( (/Qp ` p ) ` ( n e. ZZ |-> sum_ k e. ZZ ( ( f ` k ) x. ( g ` ( n - k ) ) ) ) ) ) >. } u. { <. ( le ` ndx ) , { <. f , g >. | ( { f , g } C_ b /\ sum_ k e. ZZ ( ( f ` -u k ) x. ( ( p + 1 ) ^ -u k ) ) < sum_ k e. ZZ ( ( g ` -u k ) x. ( ( p + 1 ) ^ -u k ) ) ) } >. } ) toNrmGrp ( f e. b |-> if ( f = ( ZZ X. { 0 } ) , 0 , ( p ^ -u sup ( ( `' f " ( ZZ \ { 0 } ) ) , RR , `' < ) ) ) ) ) )
Definition	df-zp 31555	Define the p-adic integers, as a subset of the p-adic rationals. (Contributed by Mario Carneiro, 2-Dec-2014.)
|- Zp = (ZRing o. Qp )
Definition	df-qpa 31556*	Define the completion of the p-adic rationals. Here we simply define it as the splitting field of a dense sequence of polynomials (using as the n-th set the collection of polynomials with degree less than n and with coefficients < ( p ^ n )). 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 x ^ ( p ^ n ) - x, 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 = ( p e. Prime |-> [_ (Qp ` p ) / r ]_ ( r polySplitLim ( n e. NN |-> { f e. (Poly1 ` r ) | ( ( r deg1 f ) <_ n /\ A. d e. ran (coe1 ` f ) ( `' d " ( ZZ \ { 0 } ) ) C_ ( 0 ... n ) ) } ) ) )
Definition	df-cp 31557	Define the metric completion of the algebraic completion of the p -adic rationals. (Contributed by Mario Carneiro, 2-Dec-2014.)
|- Cp = ( cplMetSp o. _Qp )
20.6  Mathbox for Filip Cernatescu 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 http://us.metamath.org/other/milpgame/milpgame.html.)
Theorem	problem1 31558	Practice problem 1. Clues: 5p4e9 11167 3p2e5 11160 eqtri 2644 oveq1i 6660. (Contributed by Filip Cernatescu, 16-Mar-2019.) (Proof modification is discouraged.)
|- ( ( 3 + 2 ) + 4 ) = 9
Theorem	problem2 31559	Practice problem 2. Clues: oveq12i 6662 adddiri 10051 add4i 10260 mulcli 10045 recni 10052 2re 11090 3eqtri 2648 10re 11517 5re 11099 1re 10039 4re 11097 eqcomi 2631 5p4e9 11167 oveq1i 6660 df-3 11080. (Contributed by Filip Cernatescu, 16-Mar-2019.) (Revised by AV, 9-Sep-2021.) (Proof modification is discouraged.)
|- ( ( ( 2 x. ; 1 0 ) + 5 ) + ( ( 1 x. ; 1 0 ) + 4 ) ) = ( ( 3 x. ; 1 0 ) + 9 )
Theorem	problem2OLD 31560	Practice problem 2. Clues: oveq12i 6662 adddiri 10051 add4i 10260 mulcli 10045 recni 10052 2re 11090 3eqtri 2648 10re 11517 5re 11099 1re 10039 4re 11097 eqcomi 2631 5p4e9 11167 oveq1i 6660 df-3 11080. (Contributed by Filip Cernatescu, 16-Mar-2019.) Obsolete version of problem2 31559 as of 9-Sep-2021. (Proof modification is discouraged.) (New usage is discouraged.)
|- ( ( ( 2 x. 10 ) + 5 ) + ( ( 1 x. 10 ) + 4 ) ) = ( ( 3 x. 10 ) + 9 )
Theorem	problem3 31561	Practice problem 3. Clues: eqcomi 2631 eqtri 2644 subaddrii 10370 recni 10052 4re 11097 3re 11094 1re 10039 df-4 11081 addcomi 10227. (Contributed by Filip Cernatescu, 16-Mar-2019.) (Proof modification is discouraged.)
|- A e. CC   &    |- ( A + 3 ) = 4   =>    |- A = 1
Theorem	problem4 31562	Practice problem 4. Clues: pm3.2i 471 eqcomi 2631 eqtri 2644 subaddrii 10370 recni 10052 7re 11103 6re 11101 ax-1cn 9994 df-7 11084 ax-mp 5 oveq1i 6660 3cn 11095 2cn 11091 df-3 11080 mulid2i 10043 subdiri 10480 mp3an 1424 mulcli 10045 subadd23 10293 oveq2i 6661 oveq12i 6662 3t2e6 11179 mulcomi 10046 subcli 10357 biimpri 218 subadd2i 10369. (Contributed by Filip Cernatescu, 16-Mar-2019.) (Proof modification is discouraged.)
|- A e. CC   &    |- B e. CC   &    |- ( A + B ) = 3   &    |- ( ( 3 x. A ) + ( 2 x. B ) ) = 7   =>    |- ( A = 1 /\ B = 2 )
Theorem	problem5 31563	Practice problem 5. Clues: 3brtr3i 4682 mpbi 220 breqtri 4678 ltaddsubi 10589 remulcli 10054 2re 11090 3re 11094 9re 11107 eqcomi 2631 mvlladdi 10299 3cn 6cn 11102 eqtr3i 2646 6p3e9 11170 addcomi 10227 ltdiv1ii 10953 6re 11101 nngt0i 11054 2nn 11185 divcan3i 10771 recni 10052 2cn 11091 2ne0 11113 mpbir 221 eqtri 2644 mulcomi 10046 3t2e6 11179 divmuli 10779. (Contributed by Filip Cernatescu, 16-Mar-2019.) (Proof modification is discouraged.)
|- A e. RR   &    |- ( ( 2 x. A ) + 3 ) < 9   =>    |- A < 3
Theorem	quad3 31564	Variant of quadratic equation with discriminant expanded. (Contributed by Filip Cernatescu, 19-Oct-2019.)
|- X e. CC   &    |- A e. CC   &    |- A =/= 0   &    |- B e. CC   &    |- C e. CC   &    |- ( ( A x. ( X ^ 2 ) ) + ( ( B x. X ) + C ) ) = 0   =>    |- ( X = ( ( -u B + ( sqr ` ( ( B ^ 2 ) - ( 4 x. ( A x. C ) ) ) ) ) / ( 2 x. A ) ) \/ X = ( ( -u B - ( sqr ` ( ( B ^ 2 ) - ( 4 x. ( A x. C ) ) ) ) ) / ( 2 x. A ) ) )
20.7  Mathbox for Paul Chapman
20.7.1  Real and complex numbers (cont.)
Theorem	climuzcnv 31565*	Utility lemma to convert between m <_ k and k e. ( ZZ>= ` m ) in limit theorems. (Contributed by Paul Chapman, 10-Nov-2012.)
|- ( m e. NN -> ( ( k e. ( ZZ>= ` m ) -> ph ) <-> ( k e. NN -> ( m <_ k -> ph ) ) ) )
Theorem	sinccvglem 31566*	( ( sin ` x ) / x ) ~~> 1 as (real) x ~~> 0. (Contributed by Paul Chapman, 10-Nov-2012.) (Revised by Mario Carneiro, 21-May-2014.)
|- ( ph -> F : NN --> ( RR \ { 0 } ) )   &    |- ( ph -> F ~~> 0 )   &    |- G = ( x e. ( RR \ { 0 } ) |-> ( ( sin ` x ) / x ) )   &    |- H = ( x e. CC |-> ( 1 - ( ( x ^ 2 ) / 3 ) ) )   &    |- ( ph -> M e. NN )   &    |- ( ( ph /\ k e. ( ZZ>= ` M ) ) -> ( abs ` ( F ` k ) ) < 1 )   =>    |- ( ph -> ( G o. F ) ~~> 1 )
Theorem	sinccvg 31567*	( ( sin ` x ) / x ) ~~> 1 as (real) x ~~> 0. (Contributed by Paul Chapman, 10-Nov-2012.) (Proof shortened by Mario Carneiro, 21-May-2014.)
|- ( ( F : NN --> ( RR \ { 0 } ) /\ F ~~> 0 ) -> ( ( x e. ( RR \ { 0 } ) |-> ( ( sin ` x ) / x ) ) o. F ) ~~> 1 )
Theorem	circum 31568*	The circumference of a circle of radius R, defined as the limit as n ~~> +oo of the perimeter of an inscribed n-sided isogons, is ( ( 2 x. pi ) x. R ). (Contributed by Paul Chapman, 10-Nov-2012.) (Proof shortened by Mario Carneiro, 21-May-2014.)
|- A = ( ( 2 x. pi ) / n )   &    |- P = ( n e. NN |-> ( ( 2 x. n ) x. ( R x. ( sin ` ( A / 2 ) ) ) ) )   &    |- R e. RR   =>    |- P ~~> ( ( 2 x. pi ) x. R )
20.7.2  Miscellaneous theorems
Theorem	elfzm12 31569	Membership in a curtailed finite sequence of integers. (Contributed by Paul Chapman, 17-Nov-2012.)
|- ( N e. NN -> ( M e. ( 1 ... ( N - 1 ) ) -> M e. ( 1 ... N ) ) )
Theorem	nn0seqcvg 31570*	A strictly-decreasing nonnegative integer sequence with initial term N reaches zero by the N th term. Inference version. (Contributed by Paul Chapman, 31-Mar-2011.)
|- F : NN0 --> NN0   &    |- N = ( F ` 0 )   &    |- ( k e. NN0 -> ( ( F ` ( k + 1 ) ) =/= 0 -> ( F ` ( k + 1 ) ) < ( F ` k ) ) )   =>    |- ( F ` N ) = 0
Theorem	lediv2aALT 31571	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.)
|- ( ( ( A e. RR /\ 0 < A ) /\ ( B e. RR /\ 0 < B ) /\ ( C e. RR /\ 0 <_ C ) ) -> ( A <_ B -> ( C / B ) <_ ( C / A ) ) )
Theorem	abs2sqlei 31572	The absolute values of two numbers compare as their squares. (Contributed by Paul Chapman, 7-Sep-2007.)
|- A e. CC   &    |- B e. CC   =>    |- ( ( abs ` A ) <_ ( abs ` B ) <-> ( ( abs ` A ) ^ 2 ) <_ ( ( abs ` B ) ^ 2 ) )
Theorem	abs2sqlti 31573	The absolute values of two numbers compare as their squares. (Contributed by Paul Chapman, 7-Sep-2007.)
|- A e. CC   &    |- B e. CC   =>    |- ( ( abs ` A ) < ( abs ` B ) <-> ( ( abs ` A ) ^ 2 ) < ( ( abs ` B ) ^ 2 ) )
Theorem	abs2sqle 31574	The absolute values of two numbers compare as their squares. (Contributed by Paul Chapman, 7-Sep-2007.)
|- ( ( A e. CC /\ B e. CC ) -> ( ( abs ` A ) <_ ( abs ` B ) <-> ( ( abs ` A ) ^ 2 ) <_ ( ( abs ` B ) ^ 2 ) ) )
Theorem	abs2sqlt 31575	The absolute values of two numbers compare as their squares. (Contributed by Paul Chapman, 7-Sep-2007.)
|- ( ( A e. CC /\ B e. CC ) -> ( ( abs ` A ) < ( abs ` B ) <-> ( ( abs ` A ) ^ 2 ) < ( ( abs ` B ) ^ 2 ) ) )
Theorem	abs2difi 31576	Difference of absolute values. (Contributed by Paul Chapman, 7-Sep-2007.)
|- A e. CC   &    |- B e. CC   =>    |- ( ( abs ` A ) - ( abs ` B ) ) <_ ( abs ` ( A - B ) )
Theorem	abs2difabsi 31577	Absolute value of difference of absolute values. (Contributed by Paul Chapman, 7-Sep-2007.)
|- A e. CC   &    |- B e. CC   =>    |- ( abs ` ( ( abs ` A ) - ( abs ` B ) ) ) <_ ( abs ` ( A - B ) )
20.8  Mathbox for Scott Fenton
20.8.1  ZFC Axioms in primitive form
Theorem	axextprim 31578	ax-ext 2602 without distinct variable conditions or defined symbols. (Contributed by Scott Fenton, 13-Oct-2010.)
|- -. A. x -. ( ( x e. y -> x e. z ) -> ( ( x e. z -> x e. y ) -> y = z ) )
Theorem	axrepprim 31579	ax-rep 4771 without distinct variable conditions or defined symbols. (Contributed by Scott Fenton, 13-Oct-2010.)
|- -. A. x -. ( -. A. y -. A. z ( ph -> z = y ) -> A. z -. ( ( A. y z e. x -> -. A. x ( A. z x e. y -> -. A. y ph ) ) -> -. ( -. A. x ( A. z x e. y -> -. A. y ph ) -> A. y z e. x ) ) )
Theorem	axunprim 31580	ax-un 6949 without distinct variable conditions or defined symbols. (Contributed by Scott Fenton, 13-Oct-2010.)
|- -. A. x -. A. y ( -. A. x ( y e. x -> -. x e. z ) -> y e. x )
Theorem	axpowprim 31581	ax-pow 4843 without distinct variable conditions or defined symbols. (Contributed by Scott Fenton, 13-Oct-2010.)
|- ( A. x -. A. y ( A. x ( -. A. z -. x e. y -> A. y x e. z ) -> y e. x ) -> x = y )
Theorem	axregprim 31582	ax-reg 8497 without distinct variable conditions or defined symbols. (Contributed by Scott Fenton, 13-Oct-2010.)
|- ( x e. y -> -. A. x ( x e. y -> -. A. z ( z e. x -> -. z e. y ) ) )
Theorem	axinfprim 31583	ax-inf 8535 without distinct variable conditions or defined symbols. (New usage is discouraged.) (Contributed by Scott Fenton, 13-Oct-2010.)
|- -. A. x -. ( y e. z -> -. ( y e. x -> -. A. y ( y e. x -> -. A. z ( y e. z -> -. z e. x ) ) ) )
Theorem	axacprim 31584	ax-ac 9281 without distinct variable conditions or defined symbols. (New usage is discouraged.) (Contributed by Scott Fenton, 26-Oct-2010.)
|- -. A. x -. A. y A. z ( A. x -. ( y e. z -> -. z e. w ) -> -. A. w -. A. y -. ( ( -. A. w ( y e. z -> ( z e. w -> ( y e. w -> -. w e. x ) ) ) -> y = w ) -> -. ( y = w -> -. A. w ( y e. z -> ( z e. w -> ( y e. w -> -. w e. x ) ) ) ) ) )
20.8.2  Untangled classes
Theorem	untelirr 31585*	We call a class "untanged" if all its members are not members of themselves. The term originates from Isbell (see citation in dfon2 31697). 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.)
|- ( A. x e. A -. x e. x -> -. A e. A )
Theorem	untuni 31586*	The union of a class is untangled iff all its members are untangled. (Contributed by Scott Fenton, 28-Feb-2011.)
|- ( A. x e. U. A -. x e. x <-> A. y e. A A. x e. y -. x e. x )
Theorem	untsucf 31587*	If a class is untangled, then so is its successor. (Contributed by Scott Fenton, 28-Feb-2011.) (Revised by Mario Carneiro, 11-Dec-2016.)
|- F/_ y A   =>    |- ( A. x e. A -. x e. x -> A. y e. suc A -. y e. y )
Theorem	unt0 31588	The null set is untangled. (Contributed by Scott Fenton, 10-Mar-2011.) (Proof shortened by Andrew Salmon, 27-Aug-2011.)
|- A. x e. (/) -. x e. x
Theorem	untint 31589*	If there is an untangled element of a class, then the intersection of the class is untangled. (Contributed by Scott Fenton, 1-Mar-2011.)
|- ( E. x e. A A. y e. x -. y e. y -> A. y e. |^| A -. y e. y )
Theorem	efrunt 31590*	If A is well-founded by _E, then it is untangled. (Contributed by Scott Fenton, 1-Mar-2011.)
|- ( _E Fr A -> A. x e. A -. x e. x )
Theorem	untangtr 31591*	A transitive class is untangled iff its elements are. (Contributed by Scott Fenton, 7-Mar-2011.)
|- ( Tr A -> ( A. x e. A -. x e. x <-> A. x e. A A. y e. x -. y e. y ) )
20.8.3  Extra propositional calculus theorems
Theorem	3orel2 31592	Partial elimination of a triple disjunction by denial of a disjunct. (Contributed by Scott Fenton, 26-Mar-2011.) (Proof shortened by Andrew Salmon, 25-May-2011.)
|- ( -. ps -> ( ( ph \/ ps \/ ch ) -> ( ph \/ ch ) ) )
Theorem	3orel3 31593	Partial elimination of a triple disjunction by denial of a disjunct. (Contributed by Scott Fenton, 26-Mar-2011.)
|- ( -. ch -> ( ( ph \/ ps \/ ch ) -> ( ph \/ ps ) ) )
Theorem	3pm3.2ni 31594	Triple negated disjunction introduction. (Contributed by Scott Fenton, 20-Apr-2011.)
|- -. ph   &    |- -. ps   &    |- -. ch   =>    |- -. ( ph \/ ps \/ ch )
Theorem	3jaodd 31595	Double deduction form of 3jaoi 1391. (Contributed by Scott Fenton, 20-Apr-2011.)
|- ( ph -> ( ps -> ( ch -> et ) ) )   &    |- ( ph -> ( ps -> ( th -> et ) ) )   &    |- ( ph -> ( ps -> ( ta -> et ) ) )   =>    |- ( ph -> ( ps -> ( ( ch \/ th \/ ta ) -> et ) ) )
Theorem	3orit 31596	Closed form of 3ori 1388. (Contributed by Scott Fenton, 20-Apr-2011.)
|- ( ( ph \/ ps \/ ch ) <-> ( ( -. ph /\ -. ps ) -> ch ) )
Theorem	biimpexp 31597	A biconditional in the antecedent is the same as two implications. (Contributed by Scott Fenton, 12-Dec-2010.)
|- ( ( ( ph <-> ps ) -> ch ) <-> ( ( ph -> ps ) -> ( ( ps -> ph ) -> ch ) ) )
Theorem	3orel13 31598	Elimination of two disjuncts in a triple disjunction. (Contributed by Scott Fenton, 9-Jun-2011.)
|- ( ( -. ph /\ -. ch ) -> ( ( ph \/ ps \/ ch ) -> ps ) )
20.8.4  Misc. Useful Theorems
Theorem	nepss 31599	Two classes are inequal iff their intersection is a proper subset of one of them. (Contributed by Scott Fenton, 23-Feb-2011.)
|- ( A =/= B <-> ( ( A i^i B ) C. A \/ ( A i^i B ) C. B ) )
Theorem	3ccased 31600	Triple disjunction form of ccased 988. (Contributed by Scott Fenton, 27-Oct-2013.) (Revised by Mario Carneiro, 19-Apr-2014.)
|- ( ph -> ( ( ch /\ et ) -> ps ) )   &    |- ( ph -> ( ( ch /\ ze ) -> ps ) )   &    |- ( ph -> ( ( ch /\ si ) -> ps ) )   &    |- ( ph -> ( ( th /\ et ) -> ps ) )   &    |- ( ph -> ( ( th /\ ze ) -> ps ) )   &    |- ( ph -> ( ( th /\ si ) -> ps ) )   &    |- ( ph -> ( ( ta /\ et ) -> ps ) )   &    |- ( ph -> ( ( ta /\ ze ) -> ps ) )   &    |- ( ph -> ( ( ta /\ si ) -> ps ) )   =>    |- ( ph -> ( ( ( ch \/ th \/ ta ) /\ ( et \/ ze \/ si ) ) -> ps ) )