mmtheorems43 - Metamath Proof Explorer

Jump to page: Contents + 1 1-100 2 101-200 3 201-300 4 301-400 5 401-500 6 501-600 7 601-700 8 701-800 9 801-900 10 901-1000 11 1001-1100 12 1101-1200 13 1201-1300 14 1301-1400 15 1401-1500 16 1501-1600 17 1601-1700 18 1701-1800 19 1801-1900 20 1901-2000 21 2001-2100 22 2101-2200 23 2201-2300 24 2301-2400 25 2401-2500 26 2501-2600 27 2601-2700 28 2701-2800 29 2801-2900 30 2901-3000 31 3001-3100 32 3101-3200 33 3201-3300 34 3301-3400 35 3401-3500 36 3501-3600 37 3601-3700 38 3701-3800 39 3801-3900 40 3901-4000 41 4001-4100 42 4101-4200 43 4201-4300 44 4301-4400 45 4401-4500 46 4501-4600 47 4601-4700 48 4701-4800 49 4801-4900 50 4901-5000 51 5001-5100 52 5101-5200 53 5201-5300 54 5301-5400 55 5401-5500 56 5501-5600 57 5601-5700 58 5701-5800 59 5801-5900 60 5901-6000 61 6001-6100 62 6101-6200 63 6201-6300 64 6301-6400 65 6401-6500 66 6501-6600 67 6601-6700 68 6701-6800 69 6801-6900 70 6901-7000 71 7001-7100 72 7101-7200 73 7201-7300 74 7301-7400 75 7401-7500 76 7501-7600 77 7601-7700 78 7701-7800 79 7801-7900 80 7901-8000 81 8001-8100 82 8101-8200 83 8201-8300 84 8301-8400 85 8401-8500 86 8501-8600 87 8601-8700 88 8701-8800 89 8801-8900 90 8901-9000 91 9001-9100 92 9101-9200 93 9201-9300 94 9301-9400 95 9401-9500 96 9501-9600 97 9601-9700 98 9701-9800 99 9801-9900 100 9901-10000 101 10001-10100 102 10101-10200 103 10201-10300 104 10301-10400 105 10401-10500 106 10501-10600 107 10601-10682

Statement List for Metamath Proof Explorer - 4201-4300 - Page 43 of 107

Type	Label	Description
Statement
Theorem	omwordi 4201	Weak ordering property of ordinal multiplication.
|- ((A e. On /\ B e. On /\ C e. On) -> (A (_ B -> (C .o A) (_ (C .o B)))
Theorem	omwordri 4202	Weak ordering property of ordinal multiplication. Proposition 8.21 of [TakeutiZaring] p. 63.
|- ((A e. On /\ B e. On /\ C e. On) -> (A (_ B -> (A .o C) (_ (B .o C)))
Theorem	omword1 4203	An ordinal is less than or equal to its product with another.
|- (((A e. On /\ B e. On) /\ (/) e. B) -> A (_ (A .o B))
Theorem	omword2 4204	An ordinal is less than or equal to its product with another.
|- (((A e. On /\ B e. On) /\ (/) e. B) -> A (_ (B .o A))
Theorem	om00 4205	The product of two ordinal numbers is zero iff at least one of them is zero. Proposition 8.22 of [TakeutiZaring] p. 64.
|- ((A e. On /\ B e. On) -> ((A .o B) = (/) <-> (A = (/) \/ B = (/))))
Theorem	om00el 4206	The product of two nonzero ordinal numbers is nonzero.
|- ((A e. On /\ B e. On) -> ((/) e. (A .o B) <-> ((/) e. A /\ (/) e. B)))
Theorem	omordlim 4207	Ordering involving the product of a limit ordinal. Proposition 8.23 of [TakeutiZaring] p. 64.
|- (((A e. On /\ (B e. D /\ Lim B)) /\ C e. (A .o B)) -> E.x e. B C e. (A .o x))
Theorem	omlimcl 4208	The product of any nonzero ordinal with a limit ordinal is a limit ordinal. Proposition 8.24 of [TakeutiZaring] p. 64.
|- (((A e. On /\ (B e. C /\ Lim B)) /\ (/) e. A) -> Lim (A .o B))
Theorem	odi 4209	Distributive law for ordinal arithmetic. Proposition 8.25 of [TakeutiZaring] p. 64. Warning: The HTML proof page is 3/4 megabyte in size.
|- ((A e. On /\ B e. On /\ C e. On) -> (A .o (B +o C)) = ((A .o B) +o (A .o C)))
Theorem	omass 4210	Multiplication of ordinal numbers is associative. Theorem 8.26 of [TakeutiZaring] p. 65.
|- ((A e. On /\ B e. On /\ C e. On) -> ((A .o B) .o C) = (A .o (B .o C)))
Theorem	oneo 4211	If an ordinal number is even, its successor is odd.
|- ((A e. On /\ B e. On /\ C = (2o .o A)) -> -. suc C = (2o .o B))
Theorem	oen0 4212	Ordinal exponentiation with a nonzero mantissa is nonzero. Proposition 8.32 of [TakeutiZaring] p. 67.
|- (((A e. On /\ B e. On) /\ (/) e. A) -> (/) e. (A ^o B))
Theorem	oeordi 4213	Ordering law for ordinal exponentiation. Proposition 8.33 of [TakeutiZaring] p. 67.
|- (((B e. On /\ C e. On) /\ 1o e. C) -> (A e. B -> (C ^o A) e. (C ^o B)))
Theorem	oeord 4214	Ordering property of ordinal exponentiation. Corollary 8.34 of [TakeutiZaring] p. 68 and its converse.
|- (((A e. On /\ B e. On /\ C e. On) /\ 1o e. C) -> (A e. B <-> (C ^o A) e. (C ^o B)))
Theorem	oecan 4215	Left cancellation law for ordinal exponentiation.
|- (((A e. On /\ B e. On /\ C e. On) /\ 1o e. A) -> ((A ^o B) = (A ^o C) <-> B = C))
Theorem	oeword 4216	Weak ordering property of ordinal exponentiation.
|- (((A e. On /\ B e. On /\ C e. On) /\ 1o e. C) -> (A (_ B <-> (C ^o A) (_ (C ^o B)))
Theorem	oewordi 4217	Weak ordering property of ordinal exponentiation.
|- (((A e. On /\ B e. On /\ C e. On) /\ (/) e. C) -> (A (_ B -> (C ^o A) (_ (C ^o B)))
Theorem	oewordri 4218	Weak ordering property of ordinal exponentiation. Proposition 8.35 of [TakeutiZaring] p. 68.
|- ((B e. On /\ C e. On) -> (A e. B -> (A ^o C) (_ (B ^o C)))
Theorem	oeworde 4219	Ordinal exponentiation compared to its exponent. Proposition 8.37 of [TakeutiZaring] p. 68.
|- (((A e. On /\ B e. On) /\ 1o e. A) -> B (_ (A ^o B))
Theorem	oeordsuc 4220	Ordering property of ordinal exponentiation with a successor exponent. Corollary 8.36 of [TakeutiZaring] p. 68.
|- ((B e. On /\ C e. On) -> (A e. B -> (A ^o suc C) e. (B ^o suc C)))
Theorem	oelim2 4221	Ordinal exponentiation with a limit exponent. Part of Exercise 4.36 of [Mendelson] p. 250.
|- ((A e. On /\ (B e. C /\ Lim B)) -> (A ^o B) = U_x e. (B \ 1o)(A ^o x))
Natural number arithmetic
Theorem	nna0 4222	Addition with zero. Theorem 4I(A1) of [Enderton] p. 79.
|- (A e. om -> (A +o (/)) = A)
Theorem	nnm0 4223	Multiplication with zero. Theorem 4J(A1) of [Enderton] p. 80.
|- (A e. om -> (A .o (/)) = (/))
Theorem	nnasuc 4224	Addition with successor. Theorem 4I(A2) of [Enderton] p. 79.
|- ((A e. om /\ B e. om) -> (A +o suc B) = suc (A +o B))
Theorem	nnmsuc 4225	Multiplication with successor. Theorem 4J(A2) of [Enderton] p. 80.
|- ((A e. om /\ B e. om) -> (A .o suc B) = ((A .o B) +o A))
Theorem	nna0r 4226	Addition to zero. Remark in proof of Theorem 4K(2) of [Enderton] p. 81.
|- (A e. om -> ((/) +o A) = A)
Theorem	nnm0r 4227	Multiplication with zero. Exercise 16 of [Enderton] p. 82.
|- (A e. om -> ((/) .o A) = (/))
Theorem	nnacl 4228	Closure of addition of natural numbers. Proposition 8.9 of [TakeutiZaring] p. 59.
|- ((A e. om /\ B e. om) -> (A +o B) e. om)
Theorem	nnmcl 4229	Closure of multiplication of natural numbers. Proposition 8.17 of [TakeutiZaring] p. 63.
|- ((A e. om /\ B e. om) -> (A .o B) e. om)
Theorem	nnecl 4230	Closure of exponentiation of natural numbers. Proposition 8.17 of [TakeutiZaring] p. 63.
|- ((A e. om /\ B e. om) -> (A ^o B) e. om)
Theorem	nnarcl 4231	Reverse closure law for addition of natural numbers. Exercise 1 of [TakeutiZaring] p. 62 and its converse.
|- ((A e. On /\ B e. On) -> ((A +o B) e. om <-> (A e. om /\ B e. om)))
Theorem	nnacom 4232	Addition of natural numbers is commutative. Theorem 4K(2) of [Enderton] p. 81.
|- ((A e. om /\ B e. om) -> (A +o B) = (B +o A))
Theorem	nnaordi 4233	Ordering property of addition. Proposition 8.4 of [TakeutiZaring] p. 58, limited to natural numbers.
|- ((B e. om /\ C e. om) -> (A e. B -> (C +o A) e. (C +o B)))
Theorem	nnaord 4234	Ordering property of addition. Proposition 8.4 of [TakeutiZaring] p. 58, limited to natural numbers, and its converse.
|- ((A e. om /\ B e. om /\ C e. om) -> (A e. B <-> (C +o A) e. (C +o B)))
Theorem	nnaordr 4235	Ordering property of addition of natural numbers.
|- ((A e. om /\ B e. om /\ C e. om) -> (A e. B <-> (A +o C) e. (B +o C)))
Theorem	nnaass 4236	Addition of natural numbers is associative. (For brevity, this is just a special case of the proof for ordinals. A direct proof would be about 1/3 the size of the ordinal proof, since it would use finite induction and not require the limit ordinal case..) Theorem 4K(1) of [Enderton] p. 81.
|- ((A e. om /\ B e. om /\ C e. om) -> ((A +o B) +o C) = (A +o (B +o C)))
Theorem	nndi 4237	Distributive law for natural numbers. (For brevity, this is just a special case of the proof for ordinals. A direct proof would be about 1/4 the size of the ordinal proof, since it would use finite induction and not require the limit ordinal case.) Theorem 4K(3) of [Enderton] p. 81.
|- ((A e. om /\ B e. om /\ C e. om) -> (A .o (B +o C)) = ((A .o B) +o (A .o C)))
Theorem	nnmass 4238	Multiplication of natural numbers is associative. (For brevity, this is just a special case of the proof for ordinals. A direct proof would be about 1/3 the size of the ordinal proof, since it would use finite induction and not require the limit ordinal case..) Theorem 4K(4) of [Enderton] p. 81.
|- ((A e. om /\ B e. om /\ C e. om) -> ((A .o B) .o C) = (A .o (B .o C)))
Theorem	nnmsucr 4239	Multiplication with successor. Exercise 16 of [Enderton] p. 82.
|- ((A e. om /\ B e. om) -> (suc A .o B) = ((A .o B) +o B))
Theorem	nnmcom 4240	Multiplication of natural numbers is commutative. Theorem 4K(5) of [Enderton] p. 81.
|- ((A e. om /\ B e. om) -> (A .o B) = (B .o A))
Theorem	nnacan 4241	Cancellation law for addition of natural numbers.
|- ((A e. om /\ B e. om /\ C e. om) -> ((A +o B) = (A +o C) <-> B = C))
Theorem	nnaword 4242	Weak ordering property of addition.
|- ((A e. om /\ B e. om /\ C e. om) -> (A (_ B <-> (C +o A) (_ (C +o B)))
Theorem	nnaword1 4243	Weak ordering property of addition.
|- ((A e. om /\ B e. om) -> A (_ (A +o B))
Theorem	nnaword2 4244	Weak ordering property of addition.
|- ((A e. om /\ B e. om) -> A (_ (B +o A))
Theorem	nnmordi 4245	Ordering property of multiplication. Half of Proposition 8.19 of [TakeutiZaring] p. 63, limited to natural numbers.
|- ((A e. om /\ B e. om /\ C e. om) -> ((A e. B /\ (/) e. C) -> (C .o A) e. (C .o B)))
Theorem	nnmord 4246	Ordering property of multiplication. Proposition 8.19 of [TakeutiZaring] p. 63, limited to natural numbers.
|- ((A e. om /\ B e. om /\ C e. om) -> ((A e. B /\ (/) e. C) <-> (C .o A) e. (C .o B)))
Theorem	nnmcan 4247	Cancellation law for multiplication of natural numbers.
|- (((A e. om /\ B e. om /\ C e. om) /\ (/) e. A) -> ((A .o B) = (A .o C) <-> B = C))
Theorem	nnaordex 4248	Equivalence for ordering. Compare Exercise 23 of [Enderton] p. 88.
|- ((A e. om /\ B e. om) -> (A e. B <-> E.x e. om ((/) e. x /\ (A +o x) = B)))
Theorem	nnawordex 4249	Equivalence for weak ordering of natural numbers.
|- ((A e. om /\ B e. om) -> (A (_ B <-> E.x e. om (A +o x) = B))
Theorem	oaabslem 4250	Lemma for oaabs 4251.
Theorem	oaabs 4251	Ordinal addition absorbs a natural number added to the left of a transfinite number. Proposition 8.10 of [TakeutiZaring] p. 59.
|- (((A e. om /\ B e. On) /\ om (_ B) -> (A +o B) = B)
Theorem	1onn 4252	One is a natural number.
|- 1o e. om
Theorem	2onn 4253	The ordinal 2 is a natural number.
|- 2o e. om
Theorem	nneob 4254	A natural number is even iff its successor is odd.
|- (A e. om -> (E.x e. om A = (2o .o x) <-> -. E.x e. om suc A = (2o .o x)))
Theorem	omsmolem 4255	Lemma for omsmo 4256.
Theorem	omsmo 4256	A strictly monotonic ordinal function on the set of natural numbers is one-to-one.
|- (((A (_