P. 73 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 7201-7300   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	oawordri 7201	Weak ordering property of ordinal addition. Proposition 8.7 of [TakeutiZaring] p. 59. (Contributed by NM, 7-Dec-2004.)
|- ( ( A e. On /\ B e. On /\ C e. On ) -> ( A C_ B -> ( A +o C ) C_ ( B +o C ) ) )
Theorem	oaord1 7202	An ordinal is less than its sum with a nonzero ordinal. Theorem 18 of [Suppes] p. 209 and its converse. (Contributed by NM, 6-Dec-2004.)
|- ( ( A e. On /\ B e. On ) -> ( (/) e. B <-> A e. ( A +o B ) ) )
Theorem	oaword1 7203	An ordinal is less than or equal to its sum with another. Part of Exercise 5 of [TakeutiZaring] p. 62. (For the other part see oaord1 7202.) (Contributed by NM, 6-Dec-2004.)
|- ( ( A e. On /\ B e. On ) -> A C_ ( A +o B ) )
Theorem	oaword2 7204	An ordinal is less than or equal to its sum with another. Theorem 21 of [Suppes] p. 209. (Contributed by NM, 7-Dec-2004.)
|- ( ( A e. On /\ B e. On ) -> A C_ ( B +o A ) )
Theorem	oawordeulem 7205*	Lemma for oawordex 7208. (Contributed by NM, 11-Dec-2004.)
|- A e. On   &    |- B e. On   &    |- S = { y e. On | B C_ ( A +o y ) }   =>    |- ( A C_ B -> E! x e. On ( A +o x ) = B )
Theorem	oawordeu 7206*	Existence theorem for weak ordering of ordinal sum. Proposition 8.8 of [TakeutiZaring] p. 59. (Contributed by NM, 11-Dec-2004.)
|- ( ( ( A e. On /\ B e. On ) /\ A C_ B ) -> E! x e. On ( A +o x ) = B )
Theorem	oawordexr 7207*	Existence theorem for weak ordering of ordinal sum. (Contributed by NM, 12-Dec-2004.)
|- ( ( A e. On /\ E. x e. On ( A +o x ) = B ) -> A C_ B )
Theorem	oawordex 7208*	Existence theorem for weak ordering of ordinal sum. Proposition 8.8 of [TakeutiZaring] p. 59 and its converse. See oawordeu 7206 for uniqueness. (Contributed by NM, 12-Dec-2004.)
|- ( ( A e. On /\ B e. On ) -> ( A C_ B <-> E. x e. On ( A +o x ) = B ) )
Theorem	oaordex 7209*	Existence theorem for ordering of ordinal sum. Similar to Proposition 4.34(f) of [Mendelson] p. 266 and its converse. (Contributed by NM, 12-Dec-2004.)
|- ( ( A e. On /\ B e. On ) -> ( A e. B <-> E. x e. On ( (/) e. x /\ ( A +o x ) = B ) ) )
Theorem	oa00 7210	An ordinal sum is zero iff both of its arguments are zero. (Contributed by NM, 6-Dec-2004.)
|- ( ( A e. On /\ B e. On ) -> ( ( A +o B ) = (/) <-> ( A = (/) /\ B = (/) ) ) )
Theorem	oalimcl 7211	The ordinal sum with a limit ordinal is a limit ordinal. Proposition 8.11 of [TakeutiZaring] p. 60. (Contributed by NM, 8-Dec-2004.)
|- ( ( A e. On /\ ( B e. C /\ Lim B ) ) -> Lim ( A +o B ) )
Theorem	oaass 7212	Ordinal addition is associative. Theorem 25 of [Suppes] p. 211. (Contributed by NM, 10-Dec-2004.)
|- ( ( A e. On /\ B e. On /\ C e. On ) -> ( ( A +o B ) +o C ) = ( A +o ( B +o C ) ) )
Theorem	oarec 7213*	Recursive definition of ordinal addition. Exercise 25 of [Enderton] p. 240. (Contributed by NM, 26-Dec-2004.) (Revised by Mario Carneiro, 30-May-2015.)
|- ( ( A e. On /\ B e. On ) -> ( A +o B ) = ( A u. ran ( x e. B |-> ( A +o x ) ) ) )
Theorem	oaf1o 7214*	Left addition by a constant is a bijection from ordinals to ordinals greater than the constant. (Contributed by Mario Carneiro, 30-May-2015.)
|- ( A e. On -> ( x e. On |-> ( A +o x ) ) : On -1-1-onto-> ( On \ A ) )
Theorem	oacomf1olem 7215*	Lemma for oacomf1o 7216. (Contributed by Mario Carneiro, 30-May-2015.)
|- F = ( x e. A |-> ( B +o x ) )   =>    |- ( ( A e. On /\ B e. On ) -> ( F : A -1-1-onto-> ran F /\ ( ran F i^i B ) = (/) ) )
Theorem	oacomf1o 7216*	Define a bijection from A +o B to B +o A. Thus, the two are equinumerous even if they are not equal (which sometimes occurs, e.g. oancom 8071). (Contributed by Mario Carneiro, 30-May-2015.)
|- F = ( ( x e. A |-> ( B +o x ) ) u. `' ( x e. B |-> ( A +o x ) ) )   =>    |- ( ( A e. On /\ B e. On ) -> F : ( A +o B ) -1-1-onto-> ( B +o A ) )
Theorem	omordi 7217	Ordering property of ordinal multiplication. Half of Proposition 8.19 of [TakeutiZaring] p. 63. (Contributed by NM, 14-Dec-2004.)
|- ( ( ( B e. On /\ C e. On ) /\ (/) e. C ) -> ( A e. B -> ( C .o A ) e. ( C .o B ) ) )
Theorem	omord2 7218	Ordering property of ordinal multiplication. (Contributed by NM, 25-Dec-2004.)
|- ( ( ( A e. On /\ B e. On /\ C e. On ) /\ (/) e. C ) -> ( A e. B <-> ( C .o A ) e. ( C .o B ) ) )
Theorem	omord 7219	Ordering property of ordinal multiplication. Proposition 8.19 of [TakeutiZaring] p. 63. (Contributed by NM, 14-Dec-2004.)
|- ( ( A e. On /\ B e. On /\ C e. On ) -> ( ( A e. B /\ (/) e. C ) <-> ( C .o A ) e. ( C .o B ) ) )
Theorem	omcan 7220	Left cancellation law for ordinal multiplication. Proposition 8.20 of [TakeutiZaring] p. 63 and its converse. (Contributed by NM, 14-Dec-2004.)
|- ( ( ( A e. On /\ B e. On /\ C e. On ) /\ (/) e. A ) -> ( ( A .o B ) = ( A .o C ) <-> B = C ) )
Theorem	omword 7221	Weak ordering property of ordinal multiplication. (Contributed by NM, 21-Dec-2004.)
|- ( ( ( A e. On /\ B e. On /\ C e. On ) /\ (/) e. C ) -> ( A C_ B <-> ( C .o A ) C_ ( C .o B ) ) )
Theorem	omwordi 7222	Weak ordering property of ordinal multiplication. (Contributed by NM, 21-Dec-2004.)
|- ( ( A e. On /\ B e. On /\ C e. On ) -> ( A C_ B -> ( C .o A ) C_ ( C .o B ) ) )
Theorem	omwordri 7223	Weak ordering property of ordinal multiplication. Proposition 8.21 of [TakeutiZaring] p. 63. (Contributed by NM, 20-Dec-2004.)
|- ( ( A e. On /\ B e. On /\ C e. On ) -> ( A C_ B -> ( A .o C ) C_ ( B .o C ) ) )
Theorem	omword1 7224	An ordinal is less than or equal to its product with another. (Contributed by NM, 21-Dec-2004.)
|- ( ( ( A e. On /\ B e. On ) /\ (/) e. B ) -> A C_ ( A .o B ) )
Theorem	omword2 7225	An ordinal is less than or equal to its product with another. (Contributed by NM, 21-Dec-2004.)
|- ( ( ( A e. On /\ B e. On ) /\ (/) e. B ) -> A C_ ( B .o A ) )
Theorem	om00 7226	The product of two ordinal numbers is zero iff at least one of them is zero. Proposition 8.22 of [TakeutiZaring] p. 64. (Contributed by NM, 21-Dec-2004.)
|- ( ( A e. On /\ B e. On ) -> ( ( A .o B ) = (/) <-> ( A = (/) \/ B = (/) ) ) )
Theorem	om00el 7227	The product of two nonzero ordinal numbers is nonzero. (Contributed by NM, 28-Dec-2004.)
|- ( ( A e. On /\ B e. On ) -> ( (/) e. ( A .o B ) <-> ( (/) e. A /\ (/) e. B ) ) )
Theorem	omordlim 7228*	Ordering involving the product of a limit ordinal. Proposition 8.23 of [TakeutiZaring] p. 64. (Contributed by NM, 25-Dec-2004.)
|- ( ( ( A e. On /\ ( B e. D /\ Lim B ) ) /\ C e. ( A .o B ) ) -> E. x e. B C e. ( A .o x ) )
Theorem	omlimcl 7229	The product of any nonzero ordinal with a limit ordinal is a limit ordinal. Proposition 8.24 of [TakeutiZaring] p. 64. (Contributed by NM, 25-Dec-2004.)
|- ( ( ( A e. On /\ ( B e. C /\ Lim B ) ) /\ (/) e. A ) -> Lim ( A .o B ) )
Theorem	odi 7230	Distributive law for ordinal arithmetic (left-distributivity). Proposition 8.25 of [TakeutiZaring] p. 64. (Contributed by NM, 26-Dec-2004.)
|- ( ( A e. On /\ B e. On /\ C e. On ) -> ( A .o ( B +o C ) ) = ( ( A .o B ) +o ( A .o C ) ) )
Theorem	omass 7231	Multiplication of ordinal numbers is associative. Theorem 8.26 of [TakeutiZaring] p. 65. (Contributed by NM, 28-Dec-2004.)
|- ( ( A e. On /\ B e. On /\ C e. On ) -> ( ( A .o B ) .o C ) = ( A .o ( B .o C ) ) )
Theorem	oneo 7232	If an ordinal number is even, its successor is odd. (Contributed by NM, 26-Jan-2006.)
|- ( ( A e. On /\ B e. On /\ C = ( 2o .o A ) ) -> -. suc C = ( 2o .o B ) )
Theorem	omeulem1 7233*	Lemma for omeu 7236: existence part. (Contributed by Mario Carneiro, 28-Feb-2013.)
|- ( ( A e. On /\ B e. On /\ A =/= (/) ) -> E. x e. On E. y e. A ( ( A .o x ) +o y ) = B )
Theorem	omeulem2 7234	Lemma for omeu 7236: uniqueness part. (Contributed by Mario Carneiro, 28-Feb-2013.) (Revised by Mario Carneiro, 29-May-2015.)
|- ( ( ( A e. On /\ A =/= (/) ) /\ ( B e. On /\ C e. A ) /\ ( D e. On /\ E e. A ) ) -> ( ( B e. D \/ ( B = D /\ C e. E ) ) -> ( ( A .o B ) +o C ) e. ( ( A .o D ) +o E ) ) )
Theorem	omopth2 7235	An ordered pair-like theorem for ordinal multiplication. (Contributed by Mario Carneiro, 29-May-2015.)
|- ( ( ( A e. On /\ A =/= (/) ) /\ ( B e. On /\ C e. A ) /\ ( D e. On /\ E e. A ) ) -> ( ( ( A .o B ) +o C ) = ( ( A .o D ) +o E ) <-> ( B = D /\ C = E ) ) )
Theorem	omeu 7236*	The division algorithm for ordinal multiplication. (Contributed by Mario Carneiro, 28-Feb-2013.)
|- ( ( A e. On /\ B e. On /\ A =/= (/) ) -> E! z E. x e. On E. y e. A ( z = <. x , y >. /\ ( ( A .o x ) +o y ) = B ) )
Theorem	oen0 7237	Ordinal exponentiation with a nonzero mantissa is nonzero. Proposition 8.32 of [TakeutiZaring] p. 67. (Contributed by NM, 4-Jan-2005.)
|- ( ( ( A e. On /\ B e. On ) /\ (/) e. A ) -> (/) e. ( A ^o B ) )
Theorem	oeordi 7238	Ordering law for ordinal exponentiation. Proposition 8.33 of [TakeutiZaring] p. 67. (Contributed by NM, 5-Jan-2005.) (Revised by Mario Carneiro, 24-May-2015.)
|- ( ( B e. On /\ C e. ( On \ 2o ) ) -> ( A e. B -> ( C ^o A ) e. ( C ^o B ) ) )
Theorem	oeord 7239	Ordering property of ordinal exponentiation. Corollary 8.34 of [TakeutiZaring] p. 68 and its converse. (Contributed by NM, 6-Jan-2005.) (Revised by Mario Carneiro, 24-May-2015.)
|- ( ( A e. On /\ B e. On /\ C e. ( On \ 2o ) ) -> ( A e. B <-> ( C ^o A ) e. ( C ^o B ) ) )
Theorem	oecan 7240	Left cancellation law for ordinal exponentiation. (Contributed by NM, 6-Jan-2005.) (Revised by Mario Carneiro, 24-May-2015.)
|- ( ( A e. ( On \ 2o ) /\ B e. On /\ C e. On ) -> ( ( A ^o B ) = ( A ^o C ) <-> B = C ) )
Theorem	oeword 7241	Weak ordering property of ordinal exponentiation. (Contributed by NM, 6-Jan-2005.) (Revised by Mario Carneiro, 24-May-2015.)
|- ( ( A e. On /\ B e. On /\ C e. ( On \ 2o ) ) -> ( A C_ B <-> ( C ^o A ) C_ ( C ^o B ) ) )
Theorem	oewordi 7242	Weak ordering property of ordinal exponentiation. (Contributed by NM, 6-Jan-2005.)
|- ( ( ( A e. On /\ B e. On /\ C e. On ) /\ (/) e. C ) -> ( A C_ B -> ( C ^o A ) C_ ( C ^o B ) ) )
Theorem	oewordri 7243	Weak ordering property of ordinal exponentiation. Proposition 8.35 of [TakeutiZaring] p. 68. (Contributed by NM, 6-Jan-2005.)
|- ( ( B e. On /\ C e. On ) -> ( A e. B -> ( A ^o C ) C_ ( B ^o C ) ) )
Theorem	oeworde 7244	Ordinal exponentiation compared to its exponent. Proposition 8.37 of [TakeutiZaring] p. 68. (Contributed by NM, 7-Jan-2005.) (Revised by Mario Carneiro, 24-May-2015.)
|- ( ( A e. ( On \ 2o ) /\ B e. On ) -> B C_ ( A ^o B ) )
Theorem	oeordsuc 7245	Ordering property of ordinal exponentiation with a successor exponent. Corollary 8.36 of [TakeutiZaring] p. 68. (Contributed by NM, 7-Jan-2005.)
|- ( ( B e. On /\ C e. On ) -> ( A e. B -> ( A ^o suc C ) e. ( B ^o suc C ) ) )
Theorem	oelim2 7246*	Ordinal exponentiation with a limit exponent. Part of Exercise 4.36 of [Mendelson] p. 250. (Contributed by NM, 6-Jan-2005.)
|- ( ( A e. On /\ ( B e. C /\ Lim B ) ) -> ( A ^o B ) = U_ x e. ( B \ 1o ) ( A ^o x ) )
Theorem	oeoalem 7247	Lemma for oeoa 7248. (Contributed by Eric Schmidt, 26-May-2009.)
|- A e. On   &    |- (/) e. A   &    |- B e. On   =>    |- ( C e. On -> ( A ^o ( B +o C ) ) = ( ( A ^o B ) .o ( A ^o C ) ) )
Theorem	oeoa 7248	Sum of exponents law for ordinal exponentiation. Theorem 8R of [Enderton] p. 238. Also Proposition 8.41 of [TakeutiZaring] p. 69. (Contributed by Eric Schmidt, 26-May-2009.)
|- ( ( A e. On /\ B e. On /\ C e. On ) -> ( A ^o ( B +o C ) ) = ( ( A ^o B ) .o ( A ^o C ) ) )
Theorem	oeoelem 7249	Lemma for oeoe 7250. (Contributed by Eric Schmidt, 26-May-2009.)
|- A e. On   &    |- (/) e. A   =>    |- ( ( B e. On /\ C e. On ) -> ( ( A ^o B ) ^o C ) = ( A ^o ( B .o C ) ) )
Theorem	oeoe 7250	Product of exponents law for ordinal exponentiation. Theorem 8S of [Enderton] p. 238. Also Proposition 8.42 of [TakeutiZaring] p. 70. (Contributed by Eric Schmidt, 26-May-2009.)
|- ( ( A e. On /\ B e. On /\ C e. On ) -> ( ( A ^o B ) ^o C ) = ( A ^o ( B .o C ) ) )
Theorem	oelimcl 7251	The ordinal exponential with a limit ordinal is a limit ordinal. (Contributed by Mario Carneiro, 29-May-2015.)
|- ( ( A e. ( On \ 2o ) /\ ( B e. C /\ Lim B ) ) -> Lim ( A ^o B ) )
Theorem	oeeulem 7252*	Lemma for oeeu 7254. (Contributed by Mario Carneiro, 28-Feb-2013.)
|- X = U. |^| { x e. On | B e. ( A ^o x ) }   =>    |- ( ( A e. ( On \ 2o ) /\ B e. ( On \ 1o ) ) -> ( X e. On /\ ( A ^o X ) C_ B /\ B e. ( A ^o suc X ) ) )
Theorem	oeeui 7253*	The division algorithm for ordinal exponentiation. (This version of oeeu 7254 gives an explicit expression for the unique solution of the equation, in terms of the solution P to omeu 7236.) (Contributed by Mario Carneiro, 25-May-2015.)
|- X = U. |^| { x e. On | B e. ( A ^o x ) }   &    |- P = ( iota w E. y e. On E. z e. ( A ^o X ) ( w = <. y , z >. /\ ( ( ( A ^o X ) .o y ) +o z ) = B ) )   &    |- Y = ( 1st ` P )   &    |- Z = ( 2nd ` P )   =>    |- ( ( A e. ( On \ 2o ) /\ B e. ( On \ 1o ) ) -> ( ( ( C e. On /\ D e. ( A \ 1o ) /\ E e. ( A ^o C ) ) /\ ( ( ( A ^o C ) .o D ) +o E ) = B ) <-> ( C = X /\ D = Y /\ E = Z ) ) )
Theorem	oeeu 7254*	The division algorithm for ordinal exponentiation. (Contributed by Mario Carneiro, 25-May-2015.)
|- ( ( A e. ( On \ 2o ) /\ B e. ( On \ 1o ) ) -> E! w E. x e. On E. y e. ( A \ 1o ) E. z e. ( A ^o x ) ( w = <. x , y , z >. /\ ( ( ( A ^o x ) .o y ) +o z ) = B ) )
2.4.18  Natural number arithmetic
Theorem	nna0 7255	Addition with zero. Theorem 4I(A1) of [Enderton] p. 79. (Contributed by NM, 20-Sep-1995.)
|- ( A e. om -> ( A +o (/) ) = A )
Theorem	nnm0 7256	Multiplication with zero. Theorem 4J(A1) of [Enderton] p. 80. (Contributed by NM, 20-Sep-1995.)
|- ( A e. om -> ( A .o (/) ) = (/) )
Theorem	nnasuc 7257	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 7258	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	nnesuc 7259	Exponentiation with a successor exponent. Definition 8.30 of [TakeutiZaring] p. 67. (Contributed by Mario Carneiro, 14-Nov-2014.)
|- ( ( A e. om /\ B e. om ) -> ( A ^o suc B ) = ( ( A ^o B ) .o A ) )
Theorem	nna0r 7260	Addition to zero. Remark in proof of Theorem 4K(2) of [Enderton] p. 81. Note: In this and later theorems, we deliberately avoid the more general ordinal versions of these theorems (in this case oa0r 7190) so that we can avoid ax-rep 4548, which is not needed for finite recursive definitions. (Contributed by NM, 20-Sep-1995.) (Revised by Mario Carneiro, 14-Nov-2014.)
|- ( A e. om -> ( (/) +o A ) = A )
Theorem	nnm0r 7261	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 7262	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 7263	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	nnecl 7264	Closure of exponentiation of natural numbers. Proposition 8.17 of [TakeutiZaring] p. 63. (Contributed by NM, 24-Mar-2007.) (Proof shortened by Andrew Salmon, 22-Oct-2011.)
|- ( ( A e. om /\ B e. om ) -> ( A ^o B ) e. om )
Theorem	nnacli 7265	om is closed under addition. Inference form of nnacl 7262. (Contributed by Scott Fenton, 20-Apr-2012.)
|- A e. om   &    |- B e. om   =>    |- ( A +o B ) e. om
Theorem	nnmcli 7266	om is closed under multiplication. Inference form of nnmcl 7263. (Contributed by Scott Fenton, 20-Apr-2012.)
|- A e. om   &    |- B e. om   =>    |- ( A .o B ) e. om
Theorem	nnarcl 7267	Reverse closure law for addition of natural numbers. Exercise 1 of [TakeutiZaring] p. 62 and its converse. (Contributed by NM, 12-Dec-2004.)
|- ( ( A e. On /\ B e. On ) -> ( ( A +o B ) e. om <-> ( A e. om /\ B e. om ) ) )
Theorem	nnacom 7268	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	nnaordi 7269	Ordering property of addition. Proposition 8.4 of [TakeutiZaring] p. 58, limited to natural numbers. (Contributed by NM, 3-Feb-1996.) (Revised by Mario Carneiro, 15-Nov-2014.)
|- ( ( B e. om /\ C e. om ) -> ( A e. B -> ( C +o A ) e. ( C +o B ) ) )
Theorem	nnaord 7270	Ordering property of addition. Proposition 8.4 of [TakeutiZaring] p. 58, limited to natural numbers, and its converse. (Contributed by NM, 7-Mar-1996.) (Revised by Mario Carneiro, 15-Nov-2014.)
|- ( ( A e. om /\ B e. om /\ C e. om ) -> ( A e. B <-> ( C +o A ) e. ( C +o B ) ) )
Theorem	nnaordr 7271	Ordering property of addition of natural numbers. (Contributed by NM, 9-Nov-2002.)
|- ( ( A e. om /\ B e. om /\ C e. om ) -> ( A e. B <-> ( A +o C ) e. ( B +o C ) ) )
Theorem	nnawordi 7272	Adding to both sides of an inequality in om. (Contributed by Scott Fenton, 16-Apr-2012.) (Revised by Mario Carneiro, 12-May-2012.)
|- ( ( A e. om /\ B e. om /\ C e. om ) -> ( A C_ B -> ( A +o C ) C_ ( B +o C ) ) )
Theorem	nnaass 7273	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 7274	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 7275	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 7276	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 7277	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	nnaword 7278	Weak ordering property of addition. (Contributed by NM, 17-Sep-1995.) (Revised by Mario Carneiro, 15-Nov-2014.)
|- ( ( A e. om /\ B e. om /\ C e. om ) -> ( A C_ B <-> ( C +o A ) C_ ( C +o B ) ) )
Theorem	nnacan 7279	Cancellation law for addition of natural numbers. (Contributed by NM, 27-Oct-1995.) (Revised by Mario Carneiro, 15-Nov-2014.)
|- ( ( A e. om /\ B e. om /\ C e. om ) -> ( ( A +o B ) = ( A +o C ) <-> B = C ) )
Theorem	nnaword1 7280	Weak ordering property of addition. (Contributed by NM, 9-Nov-2002.) (Revised by Mario Carneiro, 15-Nov-2014.)
|- ( ( A e. om /\ B e. om ) -> A C_ ( A +o B ) )
Theorem	nnaword2 7281	Weak ordering property of addition. (Contributed by NM, 9-Nov-2002.)
|- ( ( A e. om /\ B e. om ) -> A C_ ( B +o A ) )
Theorem	nnmordi 7282	Ordering property of multiplication. Half of Proposition 8.19 of [TakeutiZaring] p. 63, limited to natural numbers. (Contributed by NM, 18-Sep-1995.) (Revised by Mario Carneiro, 15-Nov-2014.)
|- ( ( ( B e. om /\ C e. om ) /\ (/) e. C ) -> ( A e. B -> ( C .o A ) e. ( C .o B ) ) )
Theorem	nnmord 7283	Ordering property of multiplication. Proposition 8.19 of [TakeutiZaring] p. 63, limited to natural numbers. (Contributed by NM, 22-Jan-1996.) (Revised by Mario Carneiro, 15-Nov-2014.)
|- ( ( A e. om /\ B e. om /\ C e. om ) -> ( ( A e. B /\ (/) e. C ) <-> ( C .o A ) e. ( C .o B ) ) )
Theorem	nnmword 7284	Weak ordering property of ordinal multiplication. (Contributed by Mario Carneiro, 17-Nov-2014.)
|- ( ( ( A e. om /\ B e. om /\ C e. om ) /\ (/) e. C ) -> ( A C_ B <-> ( C .o A ) C_ ( C .o B ) ) )
Theorem	nnmcan 7285	Cancellation law for multiplication of natural numbers. (Contributed by NM, 26-Oct-1995.) (Revised by Mario Carneiro, 15-Nov-2014.)
|- ( ( ( A e. om /\ B e. om /\ C e. om ) /\ (/) e. A ) -> ( ( A .o B ) = ( A .o C ) <-> B = C ) )
Theorem	nnmwordi 7286	Weak ordering property of multiplication. (Contributed by Mario Carneiro, 17-Nov-2014.)
|- ( ( A e. om /\ B e. om /\ C e. om ) -> ( A C_ B -> ( C .o A ) C_ ( C .o B ) ) )
Theorem	nnmwordri 7287	Weak ordering property of ordinal multiplication. Proposition 8.21 of [TakeutiZaring] p. 63, limited to natural numbers. (Contributed by Mario Carneiro, 17-Nov-2014.)
|- ( ( A e. om /\ B e. om /\ C e. om ) -> ( A C_ B -> ( A .o C ) C_ ( B .o C ) ) )
Theorem	nnawordex 7288*	Equivalence for weak ordering of natural numbers. (Contributed by NM, 8-Nov-2002.) (Revised by Mario Carneiro, 15-Nov-2014.)
|- ( ( A e. om /\ B e. om ) -> ( A C_ B <-> E. x e. om ( A +o x ) = B ) )
Theorem	nnaordex 7289*	Equivalence for ordering. Compare Exercise 23 of [Enderton] p. 88. (Contributed by NM, 5-Dec-1995.) (Revised by Mario Carneiro, 15-Nov-2014.)
|- ( ( A e. om /\ B e. om ) -> ( A e. B <-> E. x e. om ( (/) e. x /\ ( A +o x ) = B ) ) )
Theorem	1onn 7290	One is a natural number. (Contributed by NM, 29-Oct-1995.)
|- 1o e. om
Theorem	2onn 7291	The ordinal 2 is a natural number. (Contributed by NM, 28-Sep-2004.)
|- 2o e. om
Theorem	3onn 7292	The ordinal 3 is a natural number. (Contributed by Mario Carneiro, 5-Jan-2016.)
|- 3o e. om
Theorem	4onn 7293	The ordinal 4 is a natural number. (Contributed by Mario Carneiro, 5-Jan-2016.)
|- 4o e. om
Theorem	oaabslem 7294	Lemma for oaabs 7295. (Contributed by NM, 9-Dec-2004.)
|- ( ( om e. On /\ A e. om ) -> ( A +o om ) = om )
Theorem	oaabs 7295	Ordinal addition absorbs a natural number added to the left of a transfinite number. Proposition 8.10 of [TakeutiZaring] p. 59. (Contributed by NM, 9-Dec-2004.) (Proof shortened by Mario Carneiro, 29-May-2015.)
|- ( ( ( A e. om /\ B e. On ) /\ om C_ B ) -> ( A +o B ) = B )
Theorem	oaabs2 7296	The absorption law oaabs 7295 is also a property of higher powers of om. (Contributed by Mario Carneiro, 29-May-2015.)
|- ( ( ( A e. ( om ^o C ) /\ B e. On ) /\ ( om ^o C ) C_ B ) -> ( A +o B ) = B )
Theorem	omabslem 7297	Lemma for omabs 7298. (Contributed by Mario Carneiro, 30-May-2015.)
|- ( ( om e. On /\ A e. om /\ (/) e. A ) -> ( A .o om ) = om )
Theorem	omabs 7298	Ordinal multiplication is also absorbed by powers of om. (Contributed by Mario Carneiro, 30-May-2015.)
|- ( ( ( A e. om /\ (/) e. A ) /\ ( B e. On /\ (/) e. B ) ) -> ( A .o ( om ^o B ) ) = ( om ^o B ) )
Theorem	nnm1 7299	Multiply an element of om by 1o. (Contributed by Mario Carneiro, 17-Nov-2014.)
|- ( A e. om -> ( A .o 1o ) = A )
Theorem	nnm2 7300	Multiply an element of om by 2o. (Contributed by Scott Fenton, 18-Apr-2012.) (Revised by Mario Carneiro, 17-Nov-2014.)
|- ( A e. om -> ( A .o 2o ) = ( A +o A ) )