P. 77 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 7601-7700   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	oe0m1 7601	Ordinal exponentiation with zero mantissa and nonzero exponent. Proposition 8.31(2) of [TakeutiZaring] p. 67 and its converse. (Contributed by NM, 5-Jan-2005.)
|- ( A e. On -> ( (/) e. A <-> ( (/) ^o A ) = (/) ) )
Theorem	oe0 7602	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 ^o (/) ) = 1o )
Theorem	oev2 7603*	Alternate value of ordinal exponentiation. Compare oev 7594. (Contributed by NM, 2-Jan-2004.) (Revised by Mario Carneiro, 8-Sep-2013.)
|- ( ( A e. On /\ B e. On ) -> ( A ^o B ) = ( ( rec ( ( x e. _V |-> ( x .o A ) ) , 1o ) ` B ) i^i ( ( _V \ |^| A ) u. |^| B ) ) )
Theorem	oasuc 7604	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	oesuclem 7605*	Lemma for oesuc 7607. (Contributed by NM, 31-Dec-2004.) (Revised by Mario Carneiro, 15-Nov-2014.)
|- Lim X   &    |- ( B e. X -> ( rec ( ( x e. _V |-> ( x .o A ) ) , 1o ) ` suc B ) = ( ( x e. _V |-> ( x .o A ) ) ` ( rec ( ( x e. _V |-> ( x .o A ) ) , 1o ) ` B ) ) )   =>    |- ( ( A e. On /\ B e. X ) -> ( A ^o suc B ) = ( ( A ^o B ) .o A ) )
Theorem	omsuc 7606	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	oesuc 7607	Ordinal exponentiation with a successor exponent. Definition 8.30 of [TakeutiZaring] p. 67. (Contributed by NM, 31-Dec-2004.) (Revised by Mario Carneiro, 8-Sep-2013.)
|- ( ( A e. On /\ B e. On ) -> ( A ^o suc B ) = ( ( A ^o B ) .o A ) )
Theorem	onasuc 7608	Addition with successor. Theorem 4I(A2) of [Enderton] p. 79. (Note that this version of oasuc 7604 does not need Replacement.) (Contributed by Mario Carneiro, 16-Nov-2014.)
|- ( ( A e. On /\ B e. om ) -> ( A +o suc B ) = suc ( A +o B ) )
Theorem	onmsuc 7609	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 ) )
Theorem	onesuc 7610	Exponentiation with a successor exponent. Definition 8.30 of [TakeutiZaring] p. 67. (Contributed by Mario Carneiro, 14-Nov-2014.)
|- ( ( A e. On /\ B e. om ) -> ( A ^o suc B ) = ( ( A ^o B ) .o A ) )
Theorem	oa1suc 7611	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	oalim 7612*	Ordinal addition with a limit ordinal. Definition 8.1 of [TakeutiZaring] p. 56. (Contributed by NM, 3-Aug-2004.) (Revised by Mario Carneiro, 8-Sep-2013.)
|- ( ( A e. On /\ ( B e. C /\ Lim B ) ) -> ( A +o B ) = U_ x e. B ( A +o x ) )
Theorem	omlim 7613*	Ordinal multiplication with a limit ordinal. Definition 8.15 of [TakeutiZaring] p. 62. (Contributed by NM, 3-Aug-2004.) (Revised by Mario Carneiro, 8-Sep-2013.)
|- ( ( A e. On /\ ( B e. C /\ Lim B ) ) -> ( A .o B ) = U_ x e. B ( A .o x ) )
Theorem	oelim 7614*	Ordinal exponentiation with a limit exponent and nonzero mantissa. Definition 8.30 of [TakeutiZaring] p. 67. (Contributed by NM, 1-Jan-2005.) (Revised by Mario Carneiro, 8-Sep-2013.)
|- ( ( ( A e. On /\ ( B e. C /\ Lim B ) ) /\ (/) e. A ) -> ( A ^o B ) = U_ x e. B ( A ^o x ) )
Theorem	oacl 7615	Closure law for ordinal addition. Proposition 8.2 of [TakeutiZaring] p. 57. (Contributed by NM, 5-May-1995.)
|- ( ( A e. On /\ B e. On ) -> ( A +o B ) e. On )
Theorem	omcl 7616	Closure law for ordinal multiplication. Proposition 8.16 of [TakeutiZaring] p. 57. (Contributed by NM, 3-Aug-2004.) (Proof shortened by Andrew Salmon, 22-Oct-2011.)
|- ( ( A e. On /\ B e. On ) -> ( A .o B ) e. On )
Theorem	oecl 7617	Closure law for ordinal exponentiation. (Contributed by NM, 1-Jan-2005.) (Proof shortened by Andrew Salmon, 22-Oct-2011.)
|- ( ( A e. On /\ B e. On ) -> ( A ^o B ) e. On )
Theorem	oa0r 7618	Ordinal addition with zero. Proposition 8.3 of [TakeutiZaring] p. 57. (Contributed by NM, 5-May-1995.)
|- ( A e. On -> ( (/) +o A ) = A )
Theorem	om0r 7619	Ordinal multiplication with zero. Proposition 8.18(1) of [TakeutiZaring] p. 63. (Contributed by NM, 3-Aug-2004.)
|- ( A e. On -> ( (/) .o A ) = (/) )
Theorem	o1p1e2 7620	1 + 1 = 2 for ordinal numbers. (Contributed by NM, 18-Feb-2004.)
|- ( 1o +o 1o ) = 2o
Theorem	o2p2e4 7621	2 + 2 = 4 for ordinal numbers. Ordinal numbers are modeled as Von Neumann ordinals; see df-suc 5729. For the usual proof using complex numbers, see 2p2e4 11144. (Contributed by NM, 18-Aug-2021.)
|- ( 2o +o 2o ) = 4o
Theorem	om1 7622	Ordinal multiplication with 1. Proposition 8.18(2) of [TakeutiZaring] p. 63. (Contributed by NM, 29-Oct-1995.)
|- ( A e. On -> ( A .o 1o ) = A )
Theorem	om1r 7623	Ordinal multiplication with 1. Proposition 8.18(2) of [TakeutiZaring] p. 63. (Contributed by NM, 3-Aug-2004.)
|- ( A e. On -> ( 1o .o A ) = A )
Theorem	oe1 7624	Ordinal exponentiation with an exponent of 1. (Contributed by NM, 2-Jan-2005.)
|- ( A e. On -> ( A ^o 1o ) = A )
Theorem	oe1m 7625	Ordinal exponentiation with a mantissa of 1. Proposition 8.31(3) of [TakeutiZaring] p. 67. (Contributed by NM, 2-Jan-2005.)
|- ( A e. On -> ( 1o ^o A ) = 1o )
Theorem	oaordi 7626	Ordering property of ordinal addition. Proposition 8.4 of [TakeutiZaring] p. 58. (Contributed by NM, 5-Dec-2004.)
|- ( ( B e. On /\ C e. On ) -> ( A e. B -> ( C +o A ) e. ( C +o B ) ) )
Theorem	oaord 7627	Ordering property of ordinal addition. Proposition 8.4 of [TakeutiZaring] p. 58 and its converse. (Contributed by NM, 5-Dec-2004.)
|- ( ( A e. On /\ B e. On /\ C e. On ) -> ( A e. B <-> ( C +o A ) e. ( C +o B ) ) )
Theorem	oacan 7628	Left cancellation law for ordinal addition. Corollary 8.5 of [TakeutiZaring] p. 58. (Contributed by NM, 5-Dec-2004.)
|- ( ( A e. On /\ B e. On /\ C e. On ) -> ( ( A +o B ) = ( A +o C ) <-> B = C ) )
Theorem	oaword 7629	Weak ordering property of ordinal addition. (Contributed by NM, 6-Dec-2004.) (Proof shortened by Andrew Salmon, 22-Oct-2011.)
|- ( ( A e. On /\ B e. On /\ C e. On ) -> ( A C_ B <-> ( C +o A ) C_ ( C +o B ) ) )
Theorem	oawordri 7630	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 7631	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 7632	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 7631.) (Contributed by NM, 6-Dec-2004.)
|- ( ( A e. On /\ B e. On ) -> A C_ ( A +o B ) )
Theorem	oaword2 7633	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 7634*	Lemma for oawordex 7637. (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 7635*	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 7636*	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 7637*	Existence theorem for weak ordering of ordinal sum. Proposition 8.8 of [TakeutiZaring] p. 59 and its converse. See oawordeu 7635 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 7638*	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 7639	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 7640	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 7641	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 7642*	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 7643*	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 7644*	Lemma for oacomf1o 7645. (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 7645*	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 8548). (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 7646	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 7647	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 7648	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 7649	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 7650	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 7651	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 7652	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 7653	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 7654	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 7655	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 7656	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 7657*	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 7658	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 7659	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 7660	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 7661	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 7662*	Lemma for omeu 7665: 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 7663	Lemma for omeu 7665: 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 7664	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 7665*	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 7666	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 7667	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 7668	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 7669	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 7670	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 7671	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 7672	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 7673	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 7674	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 7675*	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 7676	Lemma for oeoa 7677. (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 7677	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 7678	Lemma for oeoe 7679. (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 7679	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 7680	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 7681*	Lemma for oeeu 7683. (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 7682*	The division algorithm for ordinal exponentiation. (This version of oeeu 7683 gives an explicit expression for the unique solution of the equation, in terms of the solution P to omeu 7665.) (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 7683*	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.19  Natural number arithmetic
Theorem	nna0 7684	Addition with zero. Theorem 4I(A1) of [Enderton] p. 79. (Contributed by NM, 20-Sep-1995.)
|- ( A e. om -> ( A +o (/) ) = A )
Theorem	nnm0 7685	Multiplication with zero. Theorem 4J(A1) of [Enderton] p. 80. (Contributed by NM, 20-Sep-1995.)
|- ( A e. om -> ( A .o (/) ) = (/) )
Theorem	nnasuc 7686	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 7687	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 7688	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 7689	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 7618) so that we can avoid ax-rep 4771, 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 7690	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 7691	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 7692	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 7693	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 7694	om is closed under addition. Inference form of nnacl 7691. (Contributed by Scott Fenton, 20-Apr-2012.)
|- A e. om   &    |- B e. om   =>    |- ( A +o B ) e. om
Theorem	nnmcli 7695	om is closed under multiplication. Inference form of nnmcl 7692. (Contributed by Scott Fenton, 20-Apr-2012.)
|- A e. om   &    |- B e. om   =>    |- ( A .o B ) e. om
Theorem	nnarcl 7696	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 7697	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 7698	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 7699	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 7700	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 ) ) )