Home | Intuitionistic Logic Explorer Theorem List (p. 61 of 102) | < Previous Next > |
Browser slow? Try the
Unicode version. |
||
Mirrors > Metamath Home Page > ILE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Type | Label | Description |
---|---|---|
Statement | ||
Definition | df-1o 6001 | Define the ordinal number 1. (Contributed by NM, 29-Oct-1995.) |
Definition | df-2o 6002 | Define the ordinal number 2. (Contributed by NM, 18-Feb-2004.) |
Definition | df-3o 6003 | Define the ordinal number 3. (Contributed by Mario Carneiro, 14-Jul-2013.) |
Definition | df-4o 6004 | Define the ordinal number 4. (Contributed by Mario Carneiro, 14-Jul-2013.) |
Definition | df-oadd 6005* | Define the ordinal addition operation. (Contributed by NM, 3-May-1995.) |
Definition | df-omul 6006* | Define the ordinal multiplication operation. (Contributed by NM, 26-Aug-1995.) |
Definition | df-oexpi 6007* |
Define the ordinal exponentiation operation.
This definition is similar to a conventional definition of exponentiation except that it defines ↑𝑜 to be for all , in order to avoid having different cases for whether the base is or not. (Contributed by Mario Carneiro, 4-Jul-2019.) |
↑𝑜 | ||
Theorem | 1on 6008 | Ordinal 1 is an ordinal number. (Contributed by NM, 29-Oct-1995.) |
Theorem | 2on 6009 | Ordinal 2 is an ordinal number. (Contributed by NM, 18-Feb-2004.) (Proof shortened by Andrew Salmon, 12-Aug-2011.) |
Theorem | 2on0 6010 | Ordinal two is not zero. (Contributed by Scott Fenton, 17-Jun-2011.) |
Theorem | 3on 6011 | Ordinal 3 is an ordinal number. (Contributed by Mario Carneiro, 5-Jan-2016.) |
Theorem | 4on 6012 | Ordinal 3 is an ordinal number. (Contributed by Mario Carneiro, 5-Jan-2016.) |
Theorem | df1o2 6013 | Expanded value of the ordinal number 1. (Contributed by NM, 4-Nov-2002.) |
Theorem | df2o3 6014 | Expanded value of the ordinal number 2. (Contributed by Mario Carneiro, 14-Aug-2015.) |
Theorem | df2o2 6015 | Expanded value of the ordinal number 2. (Contributed by NM, 29-Jan-2004.) |
Theorem | 1n0 6016 | Ordinal one is not equal to ordinal zero. (Contributed by NM, 26-Dec-2004.) |
Theorem | xp01disj 6017 | Cartesian products with the singletons of ordinals 0 and 1 are disjoint. (Contributed by NM, 2-Jun-2007.) |
Theorem | ordgt0ge1 6018 | Two ways to express that an ordinal class is positive. (Contributed by NM, 21-Dec-2004.) |
Theorem | ordge1n0im 6019 | An ordinal greater than or equal to 1 is nonzero. (Contributed by Jim Kingdon, 26-Jun-2019.) |
Theorem | el1o 6020 | Membership in ordinal one. (Contributed by NM, 5-Jan-2005.) |
Theorem | dif1o 6021 | Two ways to say that is a nonzero number of the set . (Contributed by Mario Carneiro, 21-May-2015.) |
Theorem | 2oconcl 6022 | Closure of the pair swapping function on . (Contributed by Mario Carneiro, 27-Sep-2015.) |
Theorem | 0lt1o 6023 | Ordinal zero is less than ordinal one. (Contributed by NM, 5-Jan-2005.) |
Theorem | oafnex 6024 | The characteristic function for ordinal addition is defined everywhere. (Contributed by Jim Kingdon, 27-Jul-2019.) |
Theorem | sucinc 6025* | Successor is increasing. (Contributed by Jim Kingdon, 25-Jun-2019.) |
Theorem | sucinc2 6026* | Successor is increasing. (Contributed by Jim Kingdon, 14-Jul-2019.) |
Theorem | fnoa 6027 | Functionality and domain of ordinal addition. (Contributed by NM, 26-Aug-1995.) (Proof shortened by Mario Carneiro, 3-Jul-2019.) |
Theorem | oaexg 6028 | Ordinal addition is a set. (Contributed by Mario Carneiro, 3-Jul-2019.) |
Theorem | omfnex 6029* | The characteristic function for ordinal multiplication is defined everywhere. (Contributed by Jim Kingdon, 23-Aug-2019.) |
Theorem | fnom 6030 | Functionality and domain of ordinal multiplication. (Contributed by NM, 26-Aug-1995.) (Revised by Mario Carneiro, 3-Jul-2019.) |
Theorem | omexg 6031 | Ordinal multiplication is a set. (Contributed by Mario Carneiro, 3-Jul-2019.) |
Theorem | fnoei 6032 | Functionality and domain of ordinal exponentiation. (Contributed by Mario Carneiro, 29-May-2015.) (Revised by Mario Carneiro, 3-Jul-2019.) |
↑𝑜 | ||
Theorem | oeiexg 6033 | Ordinal exponentiation is a set. (Contributed by Mario Carneiro, 3-Jul-2019.) |
↑𝑜 | ||
Theorem | oav 6034* | Value of ordinal addition. (Contributed by NM, 3-May-1995.) (Revised by Mario Carneiro, 8-Sep-2013.) |
Theorem | omv 6035* | Value of ordinal multiplication. (Contributed by NM, 17-Sep-1995.) (Revised by Mario Carneiro, 23-Aug-2014.) |
Theorem | oeiv 6036* | Value of ordinal exponentiation. (Contributed by Jim Kingdon, 9-Jul-2019.) |
↑𝑜 | ||
Theorem | oa0 6037 | Addition with zero. Proposition 8.3 of [TakeutiZaring] p. 57. (Contributed by NM, 3-May-1995.) (Revised by Mario Carneiro, 8-Sep-2013.) |
Theorem | om0 6038 | Ordinal multiplication with zero. Definition 8.15 of [TakeutiZaring] p. 62. (Contributed by NM, 17-Sep-1995.) (Revised by Mario Carneiro, 8-Sep-2013.) |
Theorem | oei0 6039 | 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.) |
↑𝑜 | ||
Theorem | oacl 6040 | 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.) |
Theorem | omcl 6041 | 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.) |
Theorem | oeicl 6042 | Closure law for ordinal exponentiation. (Contributed by Jim Kingdon, 26-Jul-2019.) |
↑𝑜 | ||
Theorem | oav2 6043* | Value of ordinal addition. (Contributed by Mario Carneiro and Jim Kingdon, 12-Aug-2019.) |
Theorem | oasuc 6044 | Addition with successor. Definition 8.1 of [TakeutiZaring] p. 56. (Contributed by NM, 3-May-1995.) (Revised by Mario Carneiro, 8-Sep-2013.) |
Theorem | omv2 6045* | Value of ordinal multiplication. (Contributed by Jim Kingdon, 23-Aug-2019.) |
Theorem | onasuc 6046 | Addition with successor. Theorem 4I(A2) of [Enderton] p. 79. (Contributed by Mario Carneiro, 16-Nov-2014.) |
Theorem | oa1suc 6047 | 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.) |
Theorem | o1p1e2 6048 | 1 + 1 = 2 for ordinal numbers. (Contributed by NM, 18-Feb-2004.) |
Theorem | oawordi 6049 | Weak ordering property of ordinal addition. (Contributed by Jim Kingdon, 27-Jul-2019.) |
Theorem | oaword1 6050 | 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.) |
Theorem | omsuc 6051 | Multiplication with successor. Definition 8.15 of [TakeutiZaring] p. 62. (Contributed by NM, 17-Sep-1995.) (Revised by Mario Carneiro, 8-Sep-2013.) |
Theorem | onmsuc 6052 | Multiplication with successor. Theorem 4J(A2) of [Enderton] p. 80. (Contributed by NM, 20-Sep-1995.) (Revised by Mario Carneiro, 14-Nov-2014.) |
Theorem | nna0 6053 | Addition with zero. Theorem 4I(A1) of [Enderton] p. 79. (Contributed by NM, 20-Sep-1995.) |
Theorem | nnm0 6054 | Multiplication with zero. Theorem 4J(A1) of [Enderton] p. 80. (Contributed by NM, 20-Sep-1995.) |
Theorem | nnasuc 6055 | Addition with successor. Theorem 4I(A2) of [Enderton] p. 79. (Contributed by NM, 20-Sep-1995.) (Revised by Mario Carneiro, 14-Nov-2014.) |
Theorem | nnmsuc 6056 | Multiplication with successor. Theorem 4J(A2) of [Enderton] p. 80. (Contributed by NM, 20-Sep-1995.) (Revised by Mario Carneiro, 14-Nov-2014.) |
Theorem | nna0r 6057 | 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.) |
Theorem | nnm0r 6058 | Multiplication with zero. Exercise 16 of [Enderton] p. 82. (Contributed by NM, 20-Sep-1995.) (Revised by Mario Carneiro, 15-Nov-2014.) |
Theorem | nnacl 6059 | 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.) |
Theorem | nnmcl 6060 | 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.) |
Theorem | nnacli 6061 | is closed under addition. Inference form of nnacl 6059. (Contributed by Scott Fenton, 20-Apr-2012.) |
Theorem | nnmcli 6062 | is closed under multiplication. Inference form of nnmcl 6060. (Contributed by Scott Fenton, 20-Apr-2012.) |
Theorem | nnacom 6063 | 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.) |
Theorem | nnaass 6064 | 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.) |
Theorem | nndi 6065 | 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.) |
Theorem | nnmass 6066 | 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.) |
Theorem | nnmsucr 6067 | Multiplication with successor. Exercise 16 of [Enderton] p. 82. (Contributed by NM, 21-Sep-1995.) (Proof shortened by Andrew Salmon, 22-Oct-2011.) |
Theorem | nnmcom 6068 | 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.) |
Theorem | nndir 6069 | Distributive law for natural numbers (right-distributivity). (Contributed by Jim Kingdon, 3-Dec-2019.) |
Theorem | nnsucelsuc 6070 | Membership is inherited by successors. The reverse direction holds for all ordinals, as seen at onsucelsucr 4234, but the forward direction, for all ordinals, implies excluded middle as seen as onsucelsucexmid 4255. (Contributed by Jim Kingdon, 25-Aug-2019.) |
Theorem | nnsucsssuc 6071 | Membership is inherited by successors. The reverse direction holds for all ordinals, as seen at onsucsssucr 4235, but the forward direction, for all ordinals, implies excluded middle as seen as onsucsssucexmid 4252. (Contributed by Jim Kingdon, 25-Aug-2019.) |
Theorem | nntri3or 6072 | Trichotomy for natural numbers. (Contributed by Jim Kingdon, 25-Aug-2019.) |
Theorem | nntri2 6073 | A trichotomy law for natural numbers. (Contributed by Jim Kingdon, 28-Aug-2019.) |
Theorem | nntri1 6074 | A trichotomy law for natural numbers. (Contributed by Jim Kingdon, 28-Aug-2019.) |
Theorem | nntri3 6075 | A trichotomy law for natural numbers. (Contributed by Jim Kingdon, 15-May-2020.) |
Theorem | nntri2or2 6076 | A trichotomy law for natural numbers. (Contributed by Jim Kingdon, 15-Sep-2021.) |
Theorem | nndceq 6077 | Equality of natural numbers is decidable. Theorem 7.2.6 of [HoTT], p. (varies). For the specific case where is zero, see nndceq0 4339. (Contributed by Jim Kingdon, 31-Aug-2019.) |
DECID | ||
Theorem | nndcel 6078 | Set membership between two natural numbers is decidable. (Contributed by Jim Kingdon, 6-Sep-2019.) |
DECID | ||
Theorem | nnsseleq 6079 | For natural numbers, inclusion is equivalent to membership or equality. (Contributed by Jim Kingdon, 16-Sep-2021.) |
Theorem | nndifsnid 6080 | If we remove a single element from a natural number then put it back in, we end up with the original natural number. This strengthens difsnss 3510 from subset to equality but the proof relies on equality being decidable. (Contributed by Jim Kingdon, 31-Aug-2021.) |
Theorem | nnaordi 6081 | 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.) |
Theorem | nnaord 6082 | 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.) |
Theorem | nnaordr 6083 | Ordering property of addition of natural numbers. (Contributed by NM, 9-Nov-2002.) |
Theorem | nnaword 6084 | Weak ordering property of addition. (Contributed by NM, 17-Sep-1995.) (Revised by Mario Carneiro, 15-Nov-2014.) |
Theorem | nnacan 6085 | Cancellation law for addition of natural numbers. (Contributed by NM, 27-Oct-1995.) (Revised by Mario Carneiro, 15-Nov-2014.) |
Theorem | nnaword1 6086 | Weak ordering property of addition. (Contributed by NM, 9-Nov-2002.) (Revised by Mario Carneiro, 15-Nov-2014.) |
Theorem | nnaword2 6087 | Weak ordering property of addition. (Contributed by NM, 9-Nov-2002.) |
Theorem | nnawordi 6088 | Adding to both sides of an inequality in (Contributed by Scott Fenton, 16-Apr-2012.) (Revised by Mario Carneiro, 12-May-2012.) |
Theorem | nnmordi 6089 | 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.) |
Theorem | nnmord 6090 | 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.) |
Theorem | nnmword 6091 | Weak ordering property of ordinal multiplication. (Contributed by Mario Carneiro, 17-Nov-2014.) |
Theorem | nnmcan 6092 | Cancellation law for multiplication of natural numbers. (Contributed by NM, 26-Oct-1995.) (Revised by Mario Carneiro, 15-Nov-2014.) |
Theorem | 1onn 6093 | One is a natural number. (Contributed by NM, 29-Oct-1995.) |
Theorem | 2onn 6094 | The ordinal 2 is a natural number. (Contributed by NM, 28-Sep-2004.) |
Theorem | 3onn 6095 | The ordinal 3 is a natural number. (Contributed by Mario Carneiro, 5-Jan-2016.) |
Theorem | 4onn 6096 | The ordinal 4 is a natural number. (Contributed by Mario Carneiro, 5-Jan-2016.) |
Theorem | nnm1 6097 | Multiply an element of by . (Contributed by Mario Carneiro, 17-Nov-2014.) |
Theorem | nnm2 6098 | Multiply an element of by (Contributed by Scott Fenton, 18-Apr-2012.) (Revised by Mario Carneiro, 17-Nov-2014.) |
Theorem | nn2m 6099 | Multiply an element of by (Contributed by Scott Fenton, 16-Apr-2012.) (Revised by Mario Carneiro, 17-Nov-2014.) |
Theorem | nnaordex 6100* | Equivalence for ordering. Compare Exercise 23 of [Enderton] p. 88. (Contributed by NM, 5-Dec-1995.) (Revised by Mario Carneiro, 15-Nov-2014.) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |