P. 61 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 6001-6100   *Has distinct variable group(s)

Type	Label	Description
Statement
Definition	df-frec 6001*	Define a recursive definition generator on om (the class of finite ordinals) with characteristic function F and initial value I. This rather amazing operation allows us to define, with compact direct definitions, functions that are usually defined in textbooks only with indirect self-referencing recursive definitions. A recursive definition requires advanced metalogic to justify - in particular, eliminating a recursive definition is very difficult and often not even shown in textbooks. On the other hand, the elimination of a direct definition is a matter of simple mechanical substitution. The price paid is the daunting complexity of our frec operation (especially when df-recs 5943 that it is built on is also eliminated). But once we get past this hurdle, definitions that would otherwise be recursive become relatively simple; see frec0g 6006 and frecsuc 6014. Unlike with transfinite recursion, finite recurson can readily divide definitions and proofs into zero and successor cases, because even without excluded middle we have theorems such as nn0suc 4345. The analogous situation with transfinite recursion - being able to say that an ordinal is zero, successor, or limit - is enabled by excluded middle and thus is not available to us. For the characteristic functions which satisfy the conditions given at frecrdg 6015, this definition and df-irdg 5980 restricted to om produce the same result. Note: We introduce frec with the philosophical goal of being able to eliminate all definitions with direct mechanical substitution and to verify easily the soundness of definitions. Metamath itself has no built-in technical limitation that prevents multiple-part recursive definitions in the traditional textbook style. (Contributed by Mario Carneiro and Jim Kingdon, 10-Aug-2019.)
|- frec ( F , I ) = (recs ( ( g e. _V |-> { x | ( E. m e. om ( dom g = suc m /\ x e. ( F ` ( g ` m ) ) ) \/ ( dom g = (/) /\ x e. I ) ) } ) ) |` om )
Theorem	freceq1 6002	Equality theorem for the finite recursive definition generator. (Contributed by Jim Kingdon, 30-May-2020.)
|- ( F = G -> frec ( F , A ) = frec ( G , A ) )
Theorem	freceq2 6003	Equality theorem for the finite recursive definition generator. (Contributed by Jim Kingdon, 30-May-2020.)
|- ( A = B -> frec ( F , A ) = frec ( F , B ) )
Theorem	frecex 6004	Finite recursion produces a set. (Contributed by Jim Kingdon, 20-Aug-2021.)
|- frec ( F , A ) e. _V
Theorem	nffrec 6005	Bound-variable hypothesis builder for the finite recursive definition generator. (Contributed by Jim Kingdon, 30-May-2020.)
|- F/_ x F   &    |- F/_ x A   =>    |- F/_ xfrec ( F , A )
Theorem	frec0g 6006	The initial value resulting from finite recursive definition generation. (Contributed by Jim Kingdon, 7-May-2020.)
|- ( A e. V -> (frec ( F , A ) ` (/) ) = A )
Theorem	frecabex 6007*	The class abstraction from df-frec 6001 exists. This is a lemma for other finite recursion proofs. (Contributed by Jim Kingdon, 13-May-2020.)
|- ( ph -> S e. V )   &    |- ( ph -> A. y ( F ` y ) e. _V )   &    |- ( ph -> A e. W )   =>    |- ( ph -> { x | ( E. m e. om ( dom S = suc m /\ x e. ( F ` ( S ` m ) ) ) \/ ( dom S = (/) /\ x e. A ) ) } e. _V )
Theorem	frectfr 6008*	Lemma to connect transfinite recursion theorems with finite recursion. That is, given the conditions F Fn _V and A e. V on frec ( F , A ), we want to be able to apply tfri1d 5972 or tfri2d 5973, and this lemma lets us satisfy hypotheses of those theorems. (Contributed by Jim Kingdon, 15-Aug-2019.)
|- G = ( g e. _V |-> { x | ( E. m e. om ( dom g = suc m /\ x e. ( F ` ( g ` m ) ) ) \/ ( dom g = (/) /\ x e. A ) ) } )   =>    |- ( ( A. z ( F ` z ) e. _V /\ A e. V ) -> A. y ( Fun G /\ ( G ` y ) e. _V ) )
Theorem	frecfnom 6009*	The function generated by finite recursive definition generation is a function on omega. (Contributed by Jim Kingdon, 13-May-2020.)
|- ( ( A. z ( F ` z ) e. _V /\ A e. V ) -> frec ( F , A ) Fn om )
Theorem	frecsuclem1 6010*	Lemma for frecsuc 6014. (Contributed by Jim Kingdon, 13-Aug-2019.)
|- G = ( g e. _V |-> { x | ( E. m e. om ( dom g = suc m /\ x e. ( F ` ( g ` m ) ) ) \/ ( dom g = (/) /\ x e. A ) ) } )   =>    |- ( ( A. z ( F ` z ) e. _V /\ A e. V /\ B e. om ) -> (frec ( F , A ) ` suc B ) = ( G ` (recs ( G ) |` suc B ) ) )
Theorem	frecsuclemdm 6011*	Lemma for frecsuc 6014. (Contributed by Jim Kingdon, 15-Aug-2019.)
|- G = ( g e. _V |-> { x | ( E. m e. om ( dom g = suc m /\ x e. ( F ` ( g ` m ) ) ) \/ ( dom g = (/) /\ x e. A ) ) } )   =>    |- ( ( A. z ( F ` z ) e. _V /\ A e. V /\ B e. om ) -> dom (recs ( G ) |` suc B ) = suc B )
Theorem	frecsuclem2 6012*	Lemma for frecsuc 6014. (Contributed by Jim Kingdon, 15-Aug-2019.)
|- G = ( g e. _V |-> { x | ( E. m e. om ( dom g = suc m /\ x e. ( F ` ( g ` m ) ) ) \/ ( dom g = (/) /\ x e. A ) ) } )   =>    |- ( ( A. z ( F ` z ) e. _V /\ A e. V /\ B e. om ) -> ( (recs ( G ) |` suc B ) ` B ) = (frec ( F , A ) ` B ) )
Theorem	frecsuclem3 6013*	Lemma for frecsuc 6014. (Contributed by Jim Kingdon, 15-Aug-2019.)
|- G = ( g e. _V |-> { x | ( E. m e. om ( dom g = suc m /\ x e. ( F ` ( g ` m ) ) ) \/ ( dom g = (/) /\ x e. A ) ) } )   =>    |- ( ( A. z ( F ` z ) e. _V /\ A e. V /\ B e. om ) -> (frec ( F , A ) ` suc B ) = ( F ` (frec ( F , A ) ` B ) ) )
Theorem	frecsuc 6014*	The successor value resulting from finite recursive definition generation. (Contributed by Jim Kingdon, 15-Aug-2019.)
|- ( ( A. z ( F ` z ) e. _V /\ A e. V /\ B e. om ) -> (frec ( F , A ) ` suc B ) = ( F ` (frec ( F , A ) ` B ) ) )
Theorem	frecrdg 6015*	Transfinite recursion restricted to omega. Given a suitable characteristic function, df-frec 6001 produces the same results as df-irdg 5980 restricted to om. Presumably the theorem would also hold if F Fn _V were changed to A. z ( F ` z ) e. _V. (Contributed by Jim Kingdon, 29-Aug-2019.)
|- ( ph -> F Fn _V )   &    |- ( ph -> A e. V )   &    |- ( ph -> A. x x C_ ( F ` x ) )   =>    |- ( ph -> frec ( F , A ) = ( rec ( F , A ) |` om ) )
Theorem	freccl 6016*	Closure for finite recursion. (Contributed by Jim Kingdon, 25-May-2020.)
|- ( ph -> A. z ( F ` z ) e. _V )   &    |- ( ph -> A e. S )   &    |- ( ( ph /\ z e. S ) -> ( F ` z ) e. S )   &    |- ( ph -> B e. om )   =>    |- ( ph -> (frec ( F , A ) ` B ) e. S )
2.6.22  Ordinal arithmetic
Syntax	c1o 6017	Extend the definition of a class to include the ordinal number 1.
class 1o
Syntax	c2o 6018	Extend the definition of a class to include the ordinal number 2.
class 2o
Syntax	c3o 6019	Extend the definition of a class to include the ordinal number 3.
class 3o
Syntax	c4o 6020	Extend the definition of a class to include the ordinal number 4.
class 4o
Syntax	coa 6021	Extend the definition of a class to include the ordinal addition operation.
class +o
Syntax	comu 6022	Extend the definition of a class to include the ordinal multiplication operation.
class .o
Syntax	coei 6023	Extend the definition of a class to include the ordinal exponentiation operation.
class ↑𝑜
Definition	df-1o 6024	Define the ordinal number 1. (Contributed by NM, 29-Oct-1995.)
|- 1o = suc (/)
Definition	df-2o 6025	Define the ordinal number 2. (Contributed by NM, 18-Feb-2004.)
|- 2o = suc 1o
Definition	df-3o 6026	Define the ordinal number 3. (Contributed by Mario Carneiro, 14-Jul-2013.)
|- 3o = suc 2o
Definition	df-4o 6027	Define the ordinal number 4. (Contributed by Mario Carneiro, 14-Jul-2013.)
|- 4o = suc 3o
Definition	df-oadd 6028*	Define the ordinal addition operation. (Contributed by NM, 3-May-1995.)
|- +o = ( x e. On , y e. On |-> ( rec ( ( z e. _V |-> suc z ) , x ) ` y ) )
Definition	df-omul 6029*	Define the ordinal multiplication operation. (Contributed by NM, 26-Aug-1995.)
|- .o = ( x e. On , y e. On |-> ( rec ( ( z e. _V |-> ( z +o x ) ) , (/) ) ` y ) )
Definition	df-oexpi 6030*	Define the ordinal exponentiation operation. This definition is similar to a conventional definition of exponentiation except that it defines (/) ↑𝑜 A to be 1o for all A e. On, in order to avoid having different cases for whether the base is (/) or not. (Contributed by Mario Carneiro, 4-Jul-2019.)
|- ↑𝑜 = ( x e. On , y e. On |-> ( rec ( ( z e. _V |-> ( z .o x ) ) , 1o ) ` y ) )
Theorem	1on 6031	Ordinal 1 is an ordinal number. (Contributed by NM, 29-Oct-1995.)
|- 1o e. On
Theorem	2on 6032	Ordinal 2 is an ordinal number. (Contributed by NM, 18-Feb-2004.) (Proof shortened by Andrew Salmon, 12-Aug-2011.)
|- 2o e. On
Theorem	2on0 6033	Ordinal two is not zero. (Contributed by Scott Fenton, 17-Jun-2011.)
|- 2o =/= (/)
Theorem	3on 6034	Ordinal 3 is an ordinal number. (Contributed by Mario Carneiro, 5-Jan-2016.)
|- 3o e. On
Theorem	4on 6035	Ordinal 3 is an ordinal number. (Contributed by Mario Carneiro, 5-Jan-2016.)
|- 4o e. On
Theorem	df1o2 6036	Expanded value of the ordinal number 1. (Contributed by NM, 4-Nov-2002.)
|- 1o = { (/) }
Theorem	df2o3 6037	Expanded value of the ordinal number 2. (Contributed by Mario Carneiro, 14-Aug-2015.)
|- 2o = { (/) , 1o }
Theorem	df2o2 6038	Expanded value of the ordinal number 2. (Contributed by NM, 29-Jan-2004.)
|- 2o = { (/) , { (/) } }
Theorem	1n0 6039	Ordinal one is not equal to ordinal zero. (Contributed by NM, 26-Dec-2004.)
|- 1o =/= (/)
Theorem	xp01disj 6040	Cartesian products with the singletons of ordinals 0 and 1 are disjoint. (Contributed by NM, 2-Jun-2007.)
|- ( ( A X. { (/) } ) i^i ( C X. { 1o } ) ) = (/)
Theorem	ordgt0ge1 6041	Two ways to express that an ordinal class is positive. (Contributed by NM, 21-Dec-2004.)
|- ( Ord A -> ( (/) e. A <-> 1o C_ A ) )
Theorem	ordge1n0im 6042	An ordinal greater than or equal to 1 is nonzero. (Contributed by Jim Kingdon, 26-Jun-2019.)
|- ( Ord A -> ( 1o C_ A -> A =/= (/) ) )
Theorem	el1o 6043	Membership in ordinal one. (Contributed by NM, 5-Jan-2005.)
|- ( A e. 1o <-> A = (/) )
Theorem	dif1o 6044	Two ways to say that A is a nonzero number of the set B. (Contributed by Mario Carneiro, 21-May-2015.)
|- ( A e. ( B \ 1o ) <-> ( A e. B /\ A =/= (/) ) )
Theorem	2oconcl 6045	Closure of the pair swapping function on 2o. (Contributed by Mario Carneiro, 27-Sep-2015.)
|- ( A e. 2o -> ( 1o \ A ) e. 2o )
Theorem	0lt1o 6046	Ordinal zero is less than ordinal one. (Contributed by NM, 5-Jan-2005.)
|- (/) e. 1o
Theorem	oafnex 6047	The characteristic function for ordinal addition is defined everywhere. (Contributed by Jim Kingdon, 27-Jul-2019.)
|- ( x e. _V |-> suc x ) Fn _V
Theorem	sucinc 6048*	Successor is increasing. (Contributed by Jim Kingdon, 25-Jun-2019.)
|- F = ( z e. _V |-> suc z )   =>    |- A. x x C_ ( F ` x )
Theorem	sucinc2 6049*	Successor is increasing. (Contributed by Jim Kingdon, 14-Jul-2019.)
|- F = ( z e. _V |-> suc z )   =>    |- ( ( B e. On /\ A e. B ) -> ( F ` A ) C_ ( F ` B ) )
Theorem	fnoa 6050	Functionality and domain of ordinal addition. (Contributed by NM, 26-Aug-1995.) (Proof shortened by Mario Carneiro, 3-Jul-2019.)
|- +o Fn ( On X. On )
Theorem	oaexg 6051	Ordinal addition is a set. (Contributed by Mario Carneiro, 3-Jul-2019.)
|- ( ( A e. V /\ B e. W ) -> ( A +o B ) e. _V )
Theorem	omfnex 6052*	The characteristic function for ordinal multiplication is defined everywhere. (Contributed by Jim Kingdon, 23-Aug-2019.)
|- ( A e. V -> ( x e. _V |-> ( x +o A ) ) Fn _V )
Theorem	fnom 6053	Functionality and domain of ordinal multiplication. (Contributed by NM, 26-Aug-1995.) (Revised by Mario Carneiro, 3-Jul-2019.)
|- .o Fn ( On X. On )
Theorem	omexg 6054	Ordinal multiplication is a set. (Contributed by Mario Carneiro, 3-Jul-2019.)
|- ( ( A e. V /\ B e. W ) -> ( A .o B ) e. _V )
Theorem	fnoei 6055	Functionality and domain of ordinal exponentiation. (Contributed by Mario Carneiro, 29-May-2015.) (Revised by Mario Carneiro, 3-Jul-2019.)
|- ↑𝑜 Fn ( On X. On )
Theorem	oeiexg 6056	Ordinal exponentiation is a set. (Contributed by Mario Carneiro, 3-Jul-2019.)
|- ( ( A e. V /\ B e. W ) -> ( A ↑𝑜 B ) e. _V )
Theorem	oav 6057*	Value of ordinal addition. (Contributed by NM, 3-May-1995.) (Revised by Mario Carneiro, 8-Sep-2013.)
|- ( ( A e. On /\ B e. On ) -> ( A +o B ) = ( rec ( ( x e. _V |-> suc x ) , A ) ` B ) )
Theorem	omv 6058*	Value of ordinal multiplication. (Contributed by NM, 17-Sep-1995.) (Revised by Mario Carneiro, 23-Aug-2014.)
|- ( ( A e. On /\ B e. On ) -> ( A .o B ) = ( rec ( ( x e. _V |-> ( x +o A ) ) , (/) ) ` B ) )
Theorem	oeiv 6059*	Value of ordinal exponentiation. (Contributed by Jim Kingdon, 9-Jul-2019.)
|- ( ( A e. On /\ B e. On ) -> ( A ↑𝑜 B ) = ( rec ( ( x e. _V |-> ( x .o A ) ) , 1o ) ` B ) )
Theorem	oa0 6060	Addition with zero. Proposition 8.3 of [TakeutiZaring] p. 57. (Contributed by NM, 3-May-1995.) (Revised by Mario Carneiro, 8-Sep-2013.)
|- ( A e. On -> ( A +o (/) ) = A )
Theorem	om0 6061	Ordinal multiplication with zero. Definition 8.15 of [TakeutiZaring] p. 62. (Contributed by NM, 17-Sep-1995.) (Revised by Mario Carneiro, 8-Sep-2013.)
|- ( A e. On -> ( A .o (/) ) = (/) )
Theorem	oei0 6062	Ordinal exponentiation with zero exponent. Definition 8.30 of [TakeutiZaring] p. 67. (Contributed by NM, 31-Dec-2004.) (Revised by Mario Carneiro, 8-Sep-2013.)
|- ( A e. On -> ( A ↑𝑜 (/) ) = 1o )
Theorem	oacl 6063	Closure law for ordinal addition. Proposition 8.2 of [TakeutiZaring] p. 57. (Contributed by NM, 5-May-1995.) (Constructive proof by Jim Kingdon, 26-Jul-2019.)
|- ( ( A e. On /\ B e. On ) -> ( A +o B ) e. On )
Theorem	omcl 6064	Closure law for ordinal multiplication. Proposition 8.16 of [TakeutiZaring] p. 57. (Contributed by NM, 3-Aug-2004.) (Constructive proof by Jim Kingdon, 26-Jul-2019.)
|- ( ( A e. On /\ B e. On ) -> ( A .o B ) e. On )
Theorem	oeicl 6065	Closure law for ordinal exponentiation. (Contributed by Jim Kingdon, 26-Jul-2019.)
|- ( ( A e. On /\ B e. On ) -> ( A ↑𝑜 B ) e. On )
Theorem	oav2 6066*	Value of ordinal addition. (Contributed by Mario Carneiro and Jim Kingdon, 12-Aug-2019.)
|- ( ( A e. On /\ B e. On ) -> ( A +o B ) = ( A u. U_ x e. B suc ( A +o x ) ) )
Theorem	oasuc 6067	Addition with successor. Definition 8.1 of [TakeutiZaring] p. 56. (Contributed by NM, 3-May-1995.) (Revised by Mario Carneiro, 8-Sep-2013.)
|- ( ( A e. On /\ B e. On ) -> ( A +o suc B ) = suc ( A +o B ) )
Theorem	omv2 6068*	Value of ordinal multiplication. (Contributed by Jim Kingdon, 23-Aug-2019.)
|- ( ( A e. On /\ B e. On ) -> ( A .o B ) = U_ x e. B ( ( A .o x ) +o A ) )
Theorem	onasuc 6069	Addition with successor. Theorem 4I(A2) of [Enderton] p. 79. (Contributed by Mario Carneiro, 16-Nov-2014.)
|- ( ( A e. On /\ B e. om ) -> ( A +o suc B ) = suc ( A +o B ) )
Theorem	oa1suc 6070	Addition with 1 is same as successor. Proposition 4.34(a) of [Mendelson] p. 266. (Contributed by NM, 29-Oct-1995.) (Revised by Mario Carneiro, 16-Nov-2014.)
|- ( A e. On -> ( A +o 1o ) = suc A )
Theorem	o1p1e2 6071	1 + 1 = 2 for ordinal numbers. (Contributed by NM, 18-Feb-2004.)
|- ( 1o +o 1o ) = 2o
Theorem	oawordi 6072	Weak ordering property of ordinal addition. (Contributed by Jim Kingdon, 27-Jul-2019.)
|- ( ( A e. On /\ B e. On /\ C e. On ) -> ( A C_ B -> ( C +o A ) C_ ( C +o B ) ) )
Theorem	oaword1 6073	An ordinal is less than or equal to its sum with another. Part of Exercise 5 of [TakeutiZaring] p. 62. (Contributed by NM, 6-Dec-2004.)
|- ( ( A e. On /\ B e. On ) -> A C_ ( A +o B ) )
Theorem	omsuc 6074	Multiplication with successor. Definition 8.15 of [TakeutiZaring] p. 62. (Contributed by NM, 17-Sep-1995.) (Revised by Mario Carneiro, 8-Sep-2013.)
|- ( ( A e. On /\ B e. On ) -> ( A .o suc B ) = ( ( A .o B ) +o A ) )
Theorem	onmsuc 6075	Multiplication with successor. Theorem 4J(A2) of [Enderton] p. 80. (Contributed by NM, 20-Sep-1995.) (Revised by Mario Carneiro, 14-Nov-2014.)
|- ( ( A e. On /\ B e. om ) -> ( A .o suc B ) = ( ( A .o B ) +o A ) )
2.6.23  Natural number arithmetic
Theorem	nna0 6076	Addition with zero. Theorem 4I(A1) of [Enderton] p. 79. (Contributed by NM, 20-Sep-1995.)
|- ( A e. om -> ( A +o (/) ) = A )
Theorem	nnm0 6077	Multiplication with zero. Theorem 4J(A1) of [Enderton] p. 80. (Contributed by NM, 20-Sep-1995.)
|- ( A e. om -> ( A .o (/) ) = (/) )
Theorem	nnasuc 6078	Addition with successor. Theorem 4I(A2) of [Enderton] p. 79. (Contributed by NM, 20-Sep-1995.) (Revised by Mario Carneiro, 14-Nov-2014.)
|- ( ( A e. om /\ B e. om ) -> ( A +o suc B ) = suc ( A +o B ) )
Theorem	nnmsuc 6079	Multiplication with successor. Theorem 4J(A2) of [Enderton] p. 80. (Contributed by NM, 20-Sep-1995.) (Revised by Mario Carneiro, 14-Nov-2014.)
|- ( ( A e. om /\ B e. om ) -> ( A .o suc B ) = ( ( A .o B ) +o A ) )
Theorem	nna0r 6080	Addition to zero. Remark in proof of Theorem 4K(2) of [Enderton] p. 81. (Contributed by NM, 20-Sep-1995.) (Revised by Mario Carneiro, 14-Nov-2014.)
|- ( A e. om -> ( (/) +o A ) = A )
Theorem	nnm0r 6081	Multiplication with zero. Exercise 16 of [Enderton] p. 82. (Contributed by NM, 20-Sep-1995.) (Revised by Mario Carneiro, 15-Nov-2014.)
|- ( A e. om -> ( (/) .o A ) = (/) )
Theorem	nnacl 6082	Closure of addition of natural numbers. Proposition 8.9 of [TakeutiZaring] p. 59. (Contributed by NM, 20-Sep-1995.) (Proof shortened by Andrew Salmon, 22-Oct-2011.)
|- ( ( A e. om /\ B e. om ) -> ( A +o B ) e. om )
Theorem	nnmcl 6083	Closure of multiplication of natural numbers. Proposition 8.17 of [TakeutiZaring] p. 63. (Contributed by NM, 20-Sep-1995.) (Proof shortened by Andrew Salmon, 22-Oct-2011.)
|- ( ( A e. om /\ B e. om ) -> ( A .o B ) e. om )
Theorem	nnacli 6084	om is closed under addition. Inference form of nnacl 6082. (Contributed by Scott Fenton, 20-Apr-2012.)
|- A e. om   &    |- B e. om   =>    |- ( A +o B ) e. om
Theorem	nnmcli 6085	om is closed under multiplication. Inference form of nnmcl 6083. (Contributed by Scott Fenton, 20-Apr-2012.)
|- A e. om   &    |- B e. om   =>    |- ( A .o B ) e. om
Theorem	nnacom 6086	Addition of natural numbers is commutative. Theorem 4K(2) of [Enderton] p. 81. (Contributed by NM, 6-May-1995.) (Revised by Mario Carneiro, 15-Nov-2014.)
|- ( ( A e. om /\ B e. om ) -> ( A +o B ) = ( B +o A ) )
Theorem	nnaass 6087	Addition of natural numbers is associative. Theorem 4K(1) of [Enderton] p. 81. (Contributed by NM, 20-Sep-1995.) (Revised by Mario Carneiro, 15-Nov-2014.)
|- ( ( A e. om /\ B e. om /\ C e. om ) -> ( ( A +o B ) +o C ) = ( A +o ( B +o C ) ) )
Theorem	nndi 6088	Distributive law for natural numbers (left-distributivity). Theorem 4K(3) of [Enderton] p. 81. (Contributed by NM, 20-Sep-1995.) (Revised by Mario Carneiro, 15-Nov-2014.)
|- ( ( A e. om /\ B e. om /\ C e. om ) -> ( A .o ( B +o C ) ) = ( ( A .o B ) +o ( A .o C ) ) )
Theorem	nnmass 6089	Multiplication of natural numbers is associative. Theorem 4K(4) of [Enderton] p. 81. (Contributed by NM, 20-Sep-1995.) (Revised by Mario Carneiro, 15-Nov-2014.)
|- ( ( A e. om /\ B e. om /\ C e. om ) -> ( ( A .o B ) .o C ) = ( A .o ( B .o C ) ) )
Theorem	nnmsucr 6090	Multiplication with successor. Exercise 16 of [Enderton] p. 82. (Contributed by NM, 21-Sep-1995.) (Proof shortened by Andrew Salmon, 22-Oct-2011.)
|- ( ( A e. om /\ B e. om ) -> ( suc A .o B ) = ( ( A .o B ) +o B ) )
Theorem	nnmcom 6091	Multiplication of natural numbers is commutative. Theorem 4K(5) of [Enderton] p. 81. (Contributed by NM, 21-Sep-1995.) (Proof shortened by Andrew Salmon, 22-Oct-2011.)
|- ( ( A e. om /\ B e. om ) -> ( A .o B ) = ( B .o A ) )
Theorem	nndir 6092	Distributive law for natural numbers (right-distributivity). (Contributed by Jim Kingdon, 3-Dec-2019.)
|- ( ( A e. om /\ B e. om /\ C e. om ) -> ( ( A +o B ) .o C ) = ( ( A .o C ) +o ( B .o C ) ) )
Theorem	nnsucelsuc 6093	Membership is inherited by successors. The reverse direction holds for all ordinals, as seen at onsucelsucr 4252, but the forward direction, for all ordinals, implies excluded middle as seen as onsucelsucexmid 4273. (Contributed by Jim Kingdon, 25-Aug-2019.)
|- ( B e. om -> ( A e. B <-> suc A e. suc B ) )
Theorem	nnsucsssuc 6094	Membership is inherited by successors. The reverse direction holds for all ordinals, as seen at onsucsssucr 4253, but the forward direction, for all ordinals, implies excluded middle as seen as onsucsssucexmid 4270. (Contributed by Jim Kingdon, 25-Aug-2019.)
|- ( ( A e. om /\ B e. om ) -> ( A C_ B <-> suc A C_ suc B ) )
Theorem	nntri3or 6095	Trichotomy for natural numbers. (Contributed by Jim Kingdon, 25-Aug-2019.)
|- ( ( A e. om /\ B e. om ) -> ( A e. B \/ A = B \/ B e. A ) )
Theorem	nntri2 6096	A trichotomy law for natural numbers. (Contributed by Jim Kingdon, 28-Aug-2019.)
|- ( ( A e. om /\ B e. om ) -> ( A e. B <-> -. ( A = B \/ B e. A ) ) )
Theorem	nntri1 6097	A trichotomy law for natural numbers. (Contributed by Jim Kingdon, 28-Aug-2019.)
|- ( ( A e. om /\ B e. om ) -> ( A C_ B <-> -. B e. A ) )
Theorem	nntri3 6098	A trichotomy law for natural numbers. (Contributed by Jim Kingdon, 15-May-2020.)
|- ( ( A e. om /\ B e. om ) -> ( A = B <-> ( -. A e. B /\ -. B e. A ) ) )
Theorem	nntri2or2 6099	A trichotomy law for natural numbers. (Contributed by Jim Kingdon, 15-Sep-2021.)
|- ( ( A e. om /\ B e. om ) -> ( A C_ B \/ B C_ A ) )
Theorem	nndceq 6100	Equality of natural numbers is decidable. Theorem 7.2.6 of [HoTT], p. (varies). For the specific case where B is zero, see nndceq0 4357. (Contributed by Jim Kingdon, 31-Aug-2019.)
|- ( ( A e. om /\ B e. om ) -> DECID A = B )