mmtheorems44 - 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-10700 108 10701-10800 109 10801-10900 110 10901-11000 111 11001-11100 112 11101-11200 113 11201-11300 114 11301-11400 115 11401-11500 116 11501-11600 117 11601-11700 118 11701-11800 119 11801-11900 120 11901-12000 121 12001-12100 122 12101-12200 123 12201-12229

Statement List for Metamath Proof Explorer - 4301-4400 - Page 44 of 123

Type	Label	Description
Statement
Theorem	omsuc 4301	Multiplication with successor. Definition 8.15 of [TakeutiZaring] p. 62.
|- ((A e. On /\ B e. On) -> (A .o suc B) = ((A .o B) +o A))
Theorem	oesuc 4302	Ordinal exponentiation with a successor exponent. Definition 8.30 of [TakeutiZaring] p. 67.
|- ((A e. On /\ B e. On) -> (A ^o suc B) = ((A ^o B) .o A))
Theorem	oalim 4303	Ordinal addition with a limit ordinal. Definition 8.1 of [TakeutiZaring] p. 56.
|- ((A e. On /\ (B e. C /\ Lim B)) -> (A +o B) = U_x e. B (A +o x))
Theorem	omlim 4304	Ordinal multiplication with a limit ordinal. Definition 8.15 of [TakeutiZaring] p. 62.
|- ((A e. On /\ (B e. C /\ Lim B)) -> (A .o B) = U_x e. B (A .o x))
Theorem	oelim 4305	Ordinal exponentiation with a limit exponent and nonzero mantissa. Definition 8.30 of [TakeutiZaring] p. 67.
|- (((A e. On /\ (B e. C /\ Lim B)) /\ (/) e. A) -> (A ^o B) = U_x e. B (A ^o x))
Theorem	oacl 4306	Closure law for ordinal addition. Proposition 8.2 of [TakeutiZaring] p. 57.
|- ((A e. On /\ B e. On) -> (A +o B) e. On)
Theorem	omcl 4307	Closure law for ordinal multiplication. Proposition 8.16 of [TakeutiZaring] p. 57.
|- ((A e. On /\ B e. On) -> (A .o B) e. On)
Theorem	oecl 4308	Closure law for ordinal exponentiation.
|- ((A e. On /\ B e. On) -> (A ^o B) e. On)
Theorem	oa0r 4309	Ordinal addition with zero. Proposition 8.3 of [TakeutiZaring] p. 57.
|- (A e. On -> ((/) +o A) = A)
Theorem	om0r 4310	Ordinal multiplication with zero. Proposition 8.18(1) of [TakeutiZaring] p. 63.
|- (A e. On -> ((/) .o A) = (/))
Theorem	o1p1e2 4311	1 + 1 = 2 for ordinal numbers.
|- (1o +o 1o) = 2o
Theorem	om1 4312	Ordinal multiplication with 1. Proposition 8.18(2) of [TakeutiZaring] p. 63.
|- (A e. On -> (A .o 1o) = A)
Theorem	om1r 4313	Ordinal multiplication with 1. Proposition 8.18(2) of [TakeutiZaring] p. 63.
|- (A e. On -> (1o .o A) = A)
Theorem	oe1 4314	Ordinal exponentiation with an exponent of 1.
|- (A e. On -> (A ^o 1o) = A)
Theorem	oe1m 4315	Ordinal exponentiation with a mantissa of 1. Proposition 8.31(3) of [TakeutiZaring] p. 67.
|- (A e. On -> (1o ^o A) = 1o)
Theorem	oaordi 4316	Ordering property of ordinal addition. Proposition 8.4 of [TakeutiZaring] p. 58.
|- ((B e. On /\ C e. On) -> (A e. B -> (C +o A) e. (C +o B)))
Theorem	oaord 4317	Ordering property of ordinal addition. Proposition 8.4 of [TakeutiZaring] p. 58 and its converse.
|- ((A e. On /\ B e. On /\ C e. On) -> (A e. B <-> (C +o A) e. (C +o B)))
Theorem	oacan 4318	Left cancellation law for ordinal addition. Corollary 8.5 of [TakeutiZaring] p. 58.
|- ((A e. On /\ B e. On /\ C e. On) -> ((A +o B) = (A +o C) <-> B = C))
Theorem	oaword 4319	Weak ordering property of ordinal addition.
|- ((A e. On /\ B e. On /\ C e. On) -> (A (_ B <-> (C +o A) (_ (C +o B)))
Theorem	oawordri 4320	Weak ordering property of ordinal addition. Proposition 8.7 of [TakeutiZaring] p. 59.
|- ((A e. On /\ B e. On /\ C e. On) -> (A (_ B -> (A +o C) (_ (B +o C)))
Theorem	oaord1 4321	An ordinal is less than its sum with a non-zero ordinal. Theorem 18 of [Suppes] p. 209 and its converse.
|- ((A e. On /\ B e. On) -> ((/) e. B <-> A e. (A +o B)))
Theorem	oaword1 4322	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 4321.)
|- ((A e. On /\ B e. On) -> A (_ (A +o B))
Theorem	oaword2 4323	An ordinal is less than or equal to its sum with another. Theorem 21 of [Suppes] p. 209.
|- ((A e. On /\ B e. On) -> A (_ (B +o A))
Theorem	oawordeulem 4324	Lemma for oawordex 4327.
Theorem	oawordeu 4325	Existence theorem for weak ordering of ordinal sum. Proposition 8.8 of [TakeutiZaring] p. 59.
|- (((A e. On /\ B e. On) /\ A (_ B) -> E!x e. On (A +o x) = B)
Theorem	oawordexr 4326	Existence theorem for weak ordering of ordinal sum.
|- ((A e. On /\ E.x e. On (A +o x) = B) -> A (_ B)
Theorem	oawordex 4327	Existence theorem for weak ordering of ordinal sum. Proposition 8.8 of [TakeutiZaring] p. 59 and its converse. See oawordeu 4325 for uniqueness.
|- ((A e. On /\ B e. On) -> (A (_ B <-> E.x e. On (A +o x) = B))
Theorem	oaordex 4328	Existence theorem for ordering of ordinal sum. Similar to Proposition 4.34(f) of [Mendelson] p. 266 and its converse.
|- ((A e. On /\ B e. On) -> (A e. B <-> E.x e. On ((/) e. x /\ (A +o x) = B)))
Theorem	oa00 4329	An ordinal sum is zero iff both of its arguments are zero.
|- ((A e. On /\ B e. On) -> ((A +o B) = (/) <-> (A = (/) /\ B = (/))))
Theorem	oalimcl 4330	The ordinal sum with a limit ordinal is a limit ordinal. Proposition 8.11 of [TakeutiZaring] p. 60.
|- ((A e. On /\ (B e. C /\ Lim B)) -> Lim (A +o B))
Theorem	oaass 4331	Ordinal addition is associative. Theorem 25 of [Suppes] p. 211.
|- ((A e. On /\ B e. On /\ C e. On) -> ((A +o B) +o C) = (A +o (B +o C)))
Theorem	oarec 4332	Recursive definition of ordinal addition. Exercise 25 of [Enderton] p. 240.
|- ((A e. On /\ B e. On) -> (A +o B) = (A u. {x | E.y e. B x = (A +o y)}))
Theorem	omordi 4333	Ordering property of ordinal multiplication. Half of Proposition 8.19 of [TakeutiZaring] p. 63.
|- (((B e. On /\ C e. On) /\ (/) e. C) -> (A e. B -> (C .o A) e. (C .o B)))
Theorem	omord2 4334	Ordering property of ordinal multiplication.
|- (((A e. On /\ B e. On /\ C e. On) /\ (/) e. C) -> (A e. B <-> (C .o A) e. (C .o B)))
Theorem	omord 4335	Ordering property of ordinal multiplication. Proposition 8.19 of [TakeutiZaring] p. 63.
|- ((A e. On /\ B e. On /\ C e. On) -> ((A e. B /\ (/) e. C) <-> (C .o A) e. (C .o B)))
Theorem	omcan 4336	Left cancellation law for ordinal multiplication. Proposition 8.20 of [TakeutiZaring] p. 63 and its converse.
|- (((A e. On /\ B e. On /\ C e. On) /\ (/) e. A) -> ((A .o B) = (A .o C) <-> B = C))
Theorem	omword 4337	Weak ordering property of ordinal multiplication.
|- (((A e. On /\ B e. On /\ C e. On) /\ (/) e. C) -> (A (_ B <-> (C .o A) (_ (C .o B)))
Theorem	omwordi 4338	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 4339	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 4340	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 4341	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 4342	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 4343	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 4344	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 4345	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 4346	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 4347	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 4348	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 4349	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 4350	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 4351	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 4352	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 4353	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 4354	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 4355	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 4356	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 4357	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 4358	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))
Theorem	oeoalem 4359	Lemma for oeoa 4360.
Theorem	oeoa 4360	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 4361	Lemma for oeoe 4362.
Theorem	oeoe 4362	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)))
Natural number arithmetic
Theorem	nna0 4363	Addition with zero. Theorem 4I(A1) of [Enderton] p. 79.
|- (A e. om -> (A +o (/)) = A)
Theorem	nnm0 4364	Multiplication with zero. Theorem 4J(A1) of [Enderton] p. 80.
|- (A e. om -> (A .o (/)) = (/))
Theorem	nnasuc 4365	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 4366	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 4367	Addition to zero. Remark in proof of Theorem 4K(2) of [Enderton] p. 81.
|- (A e. om -> ((/) +o A) = A)
Theorem	nnm0r 4368	Multiplication with zero. Exercise 16 of [Enderton] p. 82.
|- (A e. om -> ((/) .o A) = (/))
Theorem	nnacl 4369	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 4370	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 4371	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 4372	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 4373	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 4374	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 4375	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 4376	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 4377	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 4378	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 4379	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 4380	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 4381	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 4382	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 4383	Weak ordering property of addition.
|- ((A e. om /\ B e. om /\ C e. om) -> (A (_ B <-> (C +o A) (_ (C +o B)))
Theorem	nnaword1 4384	Weak ordering property of addition.
|- ((A e. om /\ B e. om) -> A (_ (A +o B))
Theorem	nnaword2 4385	Weak ordering property of addition.
|- ((A e. om /\ B e. om) -> A (_ (B +o A))
Theorem	nnmordi 4386	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 4387	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 4388	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 4389	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 4390	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 4391	Lemma for oaabs 4392.
Theorem	oaabs 4392	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 4393	One is a natural number.
|- 1o e. om
Theorem	2onn 4394	The ordinal 2 is a natural number.
|- 2o e. om
Theorem	nneob 4395	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 4396	Lemma for omsmo 4397.
Theorem	omsmo 4397	A strictly monotonic ordinal function on the set of natural numbers is one-to-one.
|- (((A (_ On /\ F:om-->A) /\ A.x e. om (F` x) e. (F` suc x)) -> F:om-1-1->A)
Equivalence relations and classes
Syntax	wer 4398	Extend the definition of a wff to include the equivalence predicate.
wff Er R
Syntax	cec 4399	Extend the definition of a class to include equivalence class.
class [A]R
Syntax	cqs 4400	Extend the definition of a class to include quotient set.
class (A/.R)