Home | Intuitionistic Logic Explorer Theorem List (p. 64 of 133) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > ILE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | frecfcllem 6301* | Lemma for frecfcl 6302. Just giving a name to a common expression to simplify the proof. (Contributed by Jim Kingdon, 30-Mar-2022.) |
⊢ 𝐺 = recs((𝑔 ∈ V ↦ {𝑥 ∣ (∃𝑚 ∈ ω (dom 𝑔 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝑔‘𝑚))) ∨ (dom 𝑔 = ∅ ∧ 𝑥 ∈ 𝐴))})) ⇒ ⊢ ((∀𝑧 ∈ 𝑆 (𝐹‘𝑧) ∈ 𝑆 ∧ 𝐴 ∈ 𝑆) → frec(𝐹, 𝐴):ω⟶𝑆) | ||
Theorem | frecfcl 6302* | Finite recursion yields a function on the natural numbers. (Contributed by Jim Kingdon, 30-Mar-2022.) |
⊢ ((∀𝑧 ∈ 𝑆 (𝐹‘𝑧) ∈ 𝑆 ∧ 𝐴 ∈ 𝑆) → frec(𝐹, 𝐴):ω⟶𝑆) | ||
Theorem | frecsuclem 6303* | Lemma for frecsuc 6304. Just giving a name to a common expression to simplify the proof. (Contributed by Jim Kingdon, 29-Mar-2022.) |
⊢ 𝐺 = (𝑔 ∈ V ↦ {𝑥 ∣ (∃𝑚 ∈ ω (dom 𝑔 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝑔‘𝑚))) ∨ (dom 𝑔 = ∅ ∧ 𝑥 ∈ 𝐴))}) ⇒ ⊢ ((∀𝑧 ∈ 𝑆 (𝐹‘𝑧) ∈ 𝑆 ∧ 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ ω) → (frec(𝐹, 𝐴)‘suc 𝐵) = (𝐹‘(frec(𝐹, 𝐴)‘𝐵))) | ||
Theorem | frecsuc 6304* | The successor value resulting from finite recursive definition generation. (Contributed by Jim Kingdon, 31-Mar-2022.) |
⊢ ((∀𝑧 ∈ 𝑆 (𝐹‘𝑧) ∈ 𝑆 ∧ 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ ω) → (frec(𝐹, 𝐴)‘suc 𝐵) = (𝐹‘(frec(𝐹, 𝐴)‘𝐵))) | ||
Theorem | frecrdg 6305* |
Transfinite recursion restricted to omega.
Given a suitable characteristic function, df-frec 6288 produces the same results as df-irdg 6267 restricted to ω. Presumably the theorem would also hold if 𝐹 Fn V were changed to ∀𝑧(𝐹‘𝑧) ∈ V. (Contributed by Jim Kingdon, 29-Aug-2019.) |
⊢ (𝜑 → 𝐹 Fn V) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → ∀𝑥 𝑥 ⊆ (𝐹‘𝑥)) ⇒ ⊢ (𝜑 → frec(𝐹, 𝐴) = (rec(𝐹, 𝐴) ↾ ω)) | ||
Syntax | c1o 6306 | Extend the definition of a class to include the ordinal number 1. |
class 1o | ||
Syntax | c2o 6307 | Extend the definition of a class to include the ordinal number 2. |
class 2o | ||
Syntax | c3o 6308 | Extend the definition of a class to include the ordinal number 3. |
class 3o | ||
Syntax | c4o 6309 | Extend the definition of a class to include the ordinal number 4. |
class 4o | ||
Syntax | coa 6310 | Extend the definition of a class to include the ordinal addition operation. |
class +o | ||
Syntax | comu 6311 | Extend the definition of a class to include the ordinal multiplication operation. |
class ·o | ||
Syntax | coei 6312 | Extend the definition of a class to include the ordinal exponentiation operation. |
class ↑o | ||
Definition | df-1o 6313 | Define the ordinal number 1. (Contributed by NM, 29-Oct-1995.) |
⊢ 1o = suc ∅ | ||
Definition | df-2o 6314 | Define the ordinal number 2. (Contributed by NM, 18-Feb-2004.) |
⊢ 2o = suc 1o | ||
Definition | df-3o 6315 | Define the ordinal number 3. (Contributed by Mario Carneiro, 14-Jul-2013.) |
⊢ 3o = suc 2o | ||
Definition | df-4o 6316 | Define the ordinal number 4. (Contributed by Mario Carneiro, 14-Jul-2013.) |
⊢ 4o = suc 3o | ||
Definition | df-oadd 6317* | Define the ordinal addition operation. (Contributed by NM, 3-May-1995.) |
⊢ +o = (𝑥 ∈ On, 𝑦 ∈ On ↦ (rec((𝑧 ∈ V ↦ suc 𝑧), 𝑥)‘𝑦)) | ||
Definition | df-omul 6318* | Define the ordinal multiplication operation. (Contributed by NM, 26-Aug-1995.) |
⊢ ·o = (𝑥 ∈ On, 𝑦 ∈ On ↦ (rec((𝑧 ∈ V ↦ (𝑧 +o 𝑥)), ∅)‘𝑦)) | ||
Definition | df-oexpi 6319* |
Define the ordinal exponentiation operation.
This definition is similar to a conventional definition of exponentiation except that it defines ∅ ↑o 𝐴 to be 1o for all 𝐴 ∈ On, in order to avoid having different cases for whether the base is ∅ or not. (Contributed by Mario Carneiro, 4-Jul-2019.) |
⊢ ↑o = (𝑥 ∈ On, 𝑦 ∈ On ↦ (rec((𝑧 ∈ V ↦ (𝑧 ·o 𝑥)), 1o)‘𝑦)) | ||
Theorem | 1on 6320 | Ordinal 1 is an ordinal number. (Contributed by NM, 29-Oct-1995.) |
⊢ 1o ∈ On | ||
Theorem | 1oex 6321 | Ordinal 1 is a set. (Contributed by BJ, 4-Jul-2022.) |
⊢ 1o ∈ V | ||
Theorem | 2on 6322 | Ordinal 2 is an ordinal number. (Contributed by NM, 18-Feb-2004.) (Proof shortened by Andrew Salmon, 12-Aug-2011.) |
⊢ 2o ∈ On | ||
Theorem | 2on0 6323 | Ordinal two is not zero. (Contributed by Scott Fenton, 17-Jun-2011.) |
⊢ 2o ≠ ∅ | ||
Theorem | 3on 6324 | Ordinal 3 is an ordinal number. (Contributed by Mario Carneiro, 5-Jan-2016.) |
⊢ 3o ∈ On | ||
Theorem | 4on 6325 | Ordinal 3 is an ordinal number. (Contributed by Mario Carneiro, 5-Jan-2016.) |
⊢ 4o ∈ On | ||
Theorem | df1o2 6326 | Expanded value of the ordinal number 1. (Contributed by NM, 4-Nov-2002.) |
⊢ 1o = {∅} | ||
Theorem | df2o3 6327 | Expanded value of the ordinal number 2. (Contributed by Mario Carneiro, 14-Aug-2015.) |
⊢ 2o = {∅, 1o} | ||
Theorem | df2o2 6328 | Expanded value of the ordinal number 2. (Contributed by NM, 29-Jan-2004.) |
⊢ 2o = {∅, {∅}} | ||
Theorem | 1n0 6329 | Ordinal one is not equal to ordinal zero. (Contributed by NM, 26-Dec-2004.) |
⊢ 1o ≠ ∅ | ||
Theorem | xp01disj 6330 | Cartesian products with the singletons of ordinals 0 and 1 are disjoint. (Contributed by NM, 2-Jun-2007.) |
⊢ ((𝐴 × {∅}) ∩ (𝐶 × {1o})) = ∅ | ||
Theorem | xp01disjl 6331 | Cartesian products with the singletons of ordinals 0 and 1 are disjoint. (Contributed by Jim Kingdon, 11-Jul-2023.) |
⊢ (({∅} × 𝐴) ∩ ({1o} × 𝐶)) = ∅ | ||
Theorem | ordgt0ge1 6332 | Two ways to express that an ordinal class is positive. (Contributed by NM, 21-Dec-2004.) |
⊢ (Ord 𝐴 → (∅ ∈ 𝐴 ↔ 1o ⊆ 𝐴)) | ||
Theorem | ordge1n0im 6333 | An ordinal greater than or equal to 1 is nonzero. (Contributed by Jim Kingdon, 26-Jun-2019.) |
⊢ (Ord 𝐴 → (1o ⊆ 𝐴 → 𝐴 ≠ ∅)) | ||
Theorem | el1o 6334 | Membership in ordinal one. (Contributed by NM, 5-Jan-2005.) |
⊢ (𝐴 ∈ 1o ↔ 𝐴 = ∅) | ||
Theorem | dif1o 6335 | Two ways to say that 𝐴 is a nonzero number of the set 𝐵. (Contributed by Mario Carneiro, 21-May-2015.) |
⊢ (𝐴 ∈ (𝐵 ∖ 1o) ↔ (𝐴 ∈ 𝐵 ∧ 𝐴 ≠ ∅)) | ||
Theorem | 2oconcl 6336 | Closure of the pair swapping function on 2o. (Contributed by Mario Carneiro, 27-Sep-2015.) |
⊢ (𝐴 ∈ 2o → (1o ∖ 𝐴) ∈ 2o) | ||
Theorem | 0lt1o 6337 | Ordinal zero is less than ordinal one. (Contributed by NM, 5-Jan-2005.) |
⊢ ∅ ∈ 1o | ||
Theorem | 0lt2o 6338 | Ordinal zero is less than ordinal two. (Contributed by Jim Kingdon, 31-Jul-2022.) |
⊢ ∅ ∈ 2o | ||
Theorem | 1lt2o 6339 | Ordinal one is less than ordinal two. (Contributed by Jim Kingdon, 31-Jul-2022.) |
⊢ 1o ∈ 2o | ||
Theorem | oafnex 6340 | The characteristic function for ordinal addition is defined everywhere. (Contributed by Jim Kingdon, 27-Jul-2019.) |
⊢ (𝑥 ∈ V ↦ suc 𝑥) Fn V | ||
Theorem | sucinc 6341* | Successor is increasing. (Contributed by Jim Kingdon, 25-Jun-2019.) |
⊢ 𝐹 = (𝑧 ∈ V ↦ suc 𝑧) ⇒ ⊢ ∀𝑥 𝑥 ⊆ (𝐹‘𝑥) | ||
Theorem | sucinc2 6342* | Successor is increasing. (Contributed by Jim Kingdon, 14-Jul-2019.) |
⊢ 𝐹 = (𝑧 ∈ V ↦ suc 𝑧) ⇒ ⊢ ((𝐵 ∈ On ∧ 𝐴 ∈ 𝐵) → (𝐹‘𝐴) ⊆ (𝐹‘𝐵)) | ||
Theorem | fnoa 6343 | Functionality and domain of ordinal addition. (Contributed by NM, 26-Aug-1995.) (Proof shortened by Mario Carneiro, 3-Jul-2019.) |
⊢ +o Fn (On × On) | ||
Theorem | oaexg 6344 | Ordinal addition is a set. (Contributed by Mario Carneiro, 3-Jul-2019.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 +o 𝐵) ∈ V) | ||
Theorem | omfnex 6345* | The characteristic function for ordinal multiplication is defined everywhere. (Contributed by Jim Kingdon, 23-Aug-2019.) |
⊢ (𝐴 ∈ 𝑉 → (𝑥 ∈ V ↦ (𝑥 +o 𝐴)) Fn V) | ||
Theorem | fnom 6346 | Functionality and domain of ordinal multiplication. (Contributed by NM, 26-Aug-1995.) (Revised by Mario Carneiro, 3-Jul-2019.) |
⊢ ·o Fn (On × On) | ||
Theorem | omexg 6347 | Ordinal multiplication is a set. (Contributed by Mario Carneiro, 3-Jul-2019.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 ·o 𝐵) ∈ V) | ||
Theorem | fnoei 6348 | Functionality and domain of ordinal exponentiation. (Contributed by Mario Carneiro, 29-May-2015.) (Revised by Mario Carneiro, 3-Jul-2019.) |
⊢ ↑o Fn (On × On) | ||
Theorem | oeiexg 6349 | Ordinal exponentiation is a set. (Contributed by Mario Carneiro, 3-Jul-2019.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 ↑o 𝐵) ∈ V) | ||
Theorem | oav 6350* | Value of ordinal addition. (Contributed by NM, 3-May-1995.) (Revised by Mario Carneiro, 8-Sep-2013.) |
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 +o 𝐵) = (rec((𝑥 ∈ V ↦ suc 𝑥), 𝐴)‘𝐵)) | ||
Theorem | omv 6351* | Value of ordinal multiplication. (Contributed by NM, 17-Sep-1995.) (Revised by Mario Carneiro, 23-Aug-2014.) |
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 ·o 𝐵) = (rec((𝑥 ∈ V ↦ (𝑥 +o 𝐴)), ∅)‘𝐵)) | ||
Theorem | oeiv 6352* | Value of ordinal exponentiation. (Contributed by Jim Kingdon, 9-Jul-2019.) |
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 ↑o 𝐵) = (rec((𝑥 ∈ V ↦ (𝑥 ·o 𝐴)), 1o)‘𝐵)) | ||
Theorem | oa0 6353 | Addition with zero. Proposition 8.3 of [TakeutiZaring] p. 57. (Contributed by NM, 3-May-1995.) (Revised by Mario Carneiro, 8-Sep-2013.) |
⊢ (𝐴 ∈ On → (𝐴 +o ∅) = 𝐴) | ||
Theorem | om0 6354 | Ordinal multiplication with zero. Definition 8.15 of [TakeutiZaring] p. 62. (Contributed by NM, 17-Sep-1995.) (Revised by Mario Carneiro, 8-Sep-2013.) |
⊢ (𝐴 ∈ On → (𝐴 ·o ∅) = ∅) | ||
Theorem | oei0 6355 | 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.) |
⊢ (𝐴 ∈ On → (𝐴 ↑o ∅) = 1o) | ||
Theorem | oacl 6356 | 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.) |
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 +o 𝐵) ∈ On) | ||
Theorem | omcl 6357 | 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.) |
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 ·o 𝐵) ∈ On) | ||
Theorem | oeicl 6358 | Closure law for ordinal exponentiation. (Contributed by Jim Kingdon, 26-Jul-2019.) |
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 ↑o 𝐵) ∈ On) | ||
Theorem | oav2 6359* | Value of ordinal addition. (Contributed by Mario Carneiro and Jim Kingdon, 12-Aug-2019.) |
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 +o 𝐵) = (𝐴 ∪ ∪ 𝑥 ∈ 𝐵 suc (𝐴 +o 𝑥))) | ||
Theorem | oasuc 6360 | Addition with successor. Definition 8.1 of [TakeutiZaring] p. 56. (Contributed by NM, 3-May-1995.) (Revised by Mario Carneiro, 8-Sep-2013.) |
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 +o suc 𝐵) = suc (𝐴 +o 𝐵)) | ||
Theorem | omv2 6361* | Value of ordinal multiplication. (Contributed by Jim Kingdon, 23-Aug-2019.) |
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 ·o 𝐵) = ∪ 𝑥 ∈ 𝐵 ((𝐴 ·o 𝑥) +o 𝐴)) | ||
Theorem | onasuc 6362 | Addition with successor. Theorem 4I(A2) of [Enderton] p. 79. (Contributed by Mario Carneiro, 16-Nov-2014.) |
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ ω) → (𝐴 +o suc 𝐵) = suc (𝐴 +o 𝐵)) | ||
Theorem | oa1suc 6363 | 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.) |
⊢ (𝐴 ∈ On → (𝐴 +o 1o) = suc 𝐴) | ||
Theorem | o1p1e2 6364 | 1 + 1 = 2 for ordinal numbers. (Contributed by NM, 18-Feb-2004.) |
⊢ (1o +o 1o) = 2o | ||
Theorem | oawordi 6365 | Weak ordering property of ordinal addition. (Contributed by Jim Kingdon, 27-Jul-2019.) |
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On) → (𝐴 ⊆ 𝐵 → (𝐶 +o 𝐴) ⊆ (𝐶 +o 𝐵))) | ||
Theorem | oawordriexmid 6366* | A weak ordering property of ordinal addition which implies excluded middle. The property is proposition 8.7 of [TakeutiZaring] p. 59. Compare with oawordi 6365. (Contributed by Jim Kingdon, 15-May-2022.) |
⊢ ((𝑎 ∈ On ∧ 𝑏 ∈ On ∧ 𝑐 ∈ On) → (𝑎 ⊆ 𝑏 → (𝑎 +o 𝑐) ⊆ (𝑏 +o 𝑐))) ⇒ ⊢ (𝜑 ∨ ¬ 𝜑) | ||
Theorem | oaword1 6367 | 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.) |
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → 𝐴 ⊆ (𝐴 +o 𝐵)) | ||
Theorem | omsuc 6368 | Multiplication with successor. Definition 8.15 of [TakeutiZaring] p. 62. (Contributed by NM, 17-Sep-1995.) (Revised by Mario Carneiro, 8-Sep-2013.) |
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 ·o suc 𝐵) = ((𝐴 ·o 𝐵) +o 𝐴)) | ||
Theorem | onmsuc 6369 | Multiplication with successor. Theorem 4J(A2) of [Enderton] p. 80. (Contributed by NM, 20-Sep-1995.) (Revised by Mario Carneiro, 14-Nov-2014.) |
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ ω) → (𝐴 ·o suc 𝐵) = ((𝐴 ·o 𝐵) +o 𝐴)) | ||
Theorem | nna0 6370 | Addition with zero. Theorem 4I(A1) of [Enderton] p. 79. (Contributed by NM, 20-Sep-1995.) |
⊢ (𝐴 ∈ ω → (𝐴 +o ∅) = 𝐴) | ||
Theorem | nnm0 6371 | Multiplication with zero. Theorem 4J(A1) of [Enderton] p. 80. (Contributed by NM, 20-Sep-1995.) |
⊢ (𝐴 ∈ ω → (𝐴 ·o ∅) = ∅) | ||
Theorem | nnasuc 6372 | Addition with successor. Theorem 4I(A2) of [Enderton] p. 79. (Contributed by NM, 20-Sep-1995.) (Revised by Mario Carneiro, 14-Nov-2014.) |
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω) → (𝐴 +o suc 𝐵) = suc (𝐴 +o 𝐵)) | ||
Theorem | nnmsuc 6373 | Multiplication with successor. Theorem 4J(A2) of [Enderton] p. 80. (Contributed by NM, 20-Sep-1995.) (Revised by Mario Carneiro, 14-Nov-2014.) |
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω) → (𝐴 ·o suc 𝐵) = ((𝐴 ·o 𝐵) +o 𝐴)) | ||
Theorem | nna0r 6374 | 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.) |
⊢ (𝐴 ∈ ω → (∅ +o 𝐴) = 𝐴) | ||
Theorem | nnm0r 6375 | Multiplication with zero. Exercise 16 of [Enderton] p. 82. (Contributed by NM, 20-Sep-1995.) (Revised by Mario Carneiro, 15-Nov-2014.) |
⊢ (𝐴 ∈ ω → (∅ ·o 𝐴) = ∅) | ||
Theorem | nnacl 6376 | 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.) |
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω) → (𝐴 +o 𝐵) ∈ ω) | ||
Theorem | nnmcl 6377 | 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.) |
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω) → (𝐴 ·o 𝐵) ∈ ω) | ||
Theorem | nnacli 6378 | ω is closed under addition. Inference form of nnacl 6376. (Contributed by Scott Fenton, 20-Apr-2012.) |
⊢ 𝐴 ∈ ω & ⊢ 𝐵 ∈ ω ⇒ ⊢ (𝐴 +o 𝐵) ∈ ω | ||
Theorem | nnmcli 6379 | ω is closed under multiplication. Inference form of nnmcl 6377. (Contributed by Scott Fenton, 20-Apr-2012.) |
⊢ 𝐴 ∈ ω & ⊢ 𝐵 ∈ ω ⇒ ⊢ (𝐴 ·o 𝐵) ∈ ω | ||
Theorem | nnacom 6380 | 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.) |
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω) → (𝐴 +o 𝐵) = (𝐵 +o 𝐴)) | ||
Theorem | nnaass 6381 | 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.) |
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω ∧ 𝐶 ∈ ω) → ((𝐴 +o 𝐵) +o 𝐶) = (𝐴 +o (𝐵 +o 𝐶))) | ||
Theorem | nndi 6382 | 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.) |
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω ∧ 𝐶 ∈ ω) → (𝐴 ·o (𝐵 +o 𝐶)) = ((𝐴 ·o 𝐵) +o (𝐴 ·o 𝐶))) | ||
Theorem | nnmass 6383 | 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.) |
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω ∧ 𝐶 ∈ ω) → ((𝐴 ·o 𝐵) ·o 𝐶) = (𝐴 ·o (𝐵 ·o 𝐶))) | ||
Theorem | nnmsucr 6384 | Multiplication with successor. Exercise 16 of [Enderton] p. 82. (Contributed by NM, 21-Sep-1995.) (Proof shortened by Andrew Salmon, 22-Oct-2011.) |
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω) → (suc 𝐴 ·o 𝐵) = ((𝐴 ·o 𝐵) +o 𝐵)) | ||
Theorem | nnmcom 6385 | 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.) |
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω) → (𝐴 ·o 𝐵) = (𝐵 ·o 𝐴)) | ||
Theorem | nndir 6386 | Distributive law for natural numbers (right-distributivity). (Contributed by Jim Kingdon, 3-Dec-2019.) |
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω ∧ 𝐶 ∈ ω) → ((𝐴 +o 𝐵) ·o 𝐶) = ((𝐴 ·o 𝐶) +o (𝐵 ·o 𝐶))) | ||
Theorem | nnsucelsuc 6387 | Membership is inherited by successors. The reverse direction holds for all ordinals, as seen at onsucelsucr 4424, but the forward direction, for all ordinals, implies excluded middle as seen as onsucelsucexmid 4445. (Contributed by Jim Kingdon, 25-Aug-2019.) |
⊢ (𝐵 ∈ ω → (𝐴 ∈ 𝐵 ↔ suc 𝐴 ∈ suc 𝐵)) | ||
Theorem | nnsucsssuc 6388 | Membership is inherited by successors. The reverse direction holds for all ordinals, as seen at onsucsssucr 4425, but the forward direction, for all ordinals, implies excluded middle as seen as onsucsssucexmid 4442. (Contributed by Jim Kingdon, 25-Aug-2019.) |
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω) → (𝐴 ⊆ 𝐵 ↔ suc 𝐴 ⊆ suc 𝐵)) | ||
Theorem | nntri3or 6389 | Trichotomy for natural numbers. (Contributed by Jim Kingdon, 25-Aug-2019.) |
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω) → (𝐴 ∈ 𝐵 ∨ 𝐴 = 𝐵 ∨ 𝐵 ∈ 𝐴)) | ||
Theorem | nntri2 6390 | A trichotomy law for natural numbers. (Contributed by Jim Kingdon, 28-Aug-2019.) |
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω) → (𝐴 ∈ 𝐵 ↔ ¬ (𝐴 = 𝐵 ∨ 𝐵 ∈ 𝐴))) | ||
Theorem | nnsucuniel 6391 | Given an element 𝐴 of the union of a natural number 𝐵, suc 𝐴 is an element of 𝐵 itself. The reverse direction holds for all ordinals (sucunielr 4426). The forward direction for all ordinals implies excluded middle (ordsucunielexmid 4446). (Contributed by Jim Kingdon, 13-Mar-2022.) |
⊢ (𝐵 ∈ ω → (𝐴 ∈ ∪ 𝐵 ↔ suc 𝐴 ∈ 𝐵)) | ||
Theorem | nntri1 6392 | A trichotomy law for natural numbers. (Contributed by Jim Kingdon, 28-Aug-2019.) |
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω) → (𝐴 ⊆ 𝐵 ↔ ¬ 𝐵 ∈ 𝐴)) | ||
Theorem | nntri3 6393 | A trichotomy law for natural numbers. (Contributed by Jim Kingdon, 15-May-2020.) |
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω) → (𝐴 = 𝐵 ↔ (¬ 𝐴 ∈ 𝐵 ∧ ¬ 𝐵 ∈ 𝐴))) | ||
Theorem | nntri2or2 6394 | A trichotomy law for natural numbers. (Contributed by Jim Kingdon, 15-Sep-2021.) |
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω) → (𝐴 ⊆ 𝐵 ∨ 𝐵 ⊆ 𝐴)) | ||
Theorem | nndceq 6395 | Equality of natural numbers is decidable. Theorem 7.2.6 of [HoTT], p. (varies). For the specific case where 𝐵 is zero, see nndceq0 4531. (Contributed by Jim Kingdon, 31-Aug-2019.) |
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω) → DECID 𝐴 = 𝐵) | ||
Theorem | nndcel 6396 | Set membership between two natural numbers is decidable. (Contributed by Jim Kingdon, 6-Sep-2019.) |
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω) → DECID 𝐴 ∈ 𝐵) | ||
Theorem | nnsseleq 6397 | For natural numbers, inclusion is equivalent to membership or equality. (Contributed by Jim Kingdon, 16-Sep-2021.) |
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω) → (𝐴 ⊆ 𝐵 ↔ (𝐴 ∈ 𝐵 ∨ 𝐴 = 𝐵))) | ||
Theorem | nnsssuc 6398 | A natural number is a subset of another natural number if and only if it belongs to its successor. (Contributed by Jim Kingdon, 22-Jul-2023.) |
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω) → (𝐴 ⊆ 𝐵 ↔ 𝐴 ∈ suc 𝐵)) | ||
Theorem | nntr2 6399 | Transitive law for natural numbers. (Contributed by Jim Kingdon, 22-Jul-2023.) |
⊢ ((𝐴 ∈ ω ∧ 𝐶 ∈ ω) → ((𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝐶) → 𝐴 ∈ 𝐶)) | ||
Theorem | dcdifsnid 6400* | If we remove a single element from a set with decidable equality then put it back in, we end up with the original set. This strengthens difsnss 3666 from subset to equality but the proof relies on equality being decidable. (Contributed by Jim Kingdon, 17-Jun-2022.) |
⊢ ((∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 DECID 𝑥 = 𝑦 ∧ 𝐵 ∈ 𝐴) → ((𝐴 ∖ {𝐵}) ∪ {𝐵}) = 𝐴) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |