Home | Intuitionistic Logic Explorer Theorem List (p. 64 of 135) | < 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 | nffrec 6301 | Bound-variable hypothesis builder for the finite recursive definition generator. (Contributed by Jim Kingdon, 30-May-2020.) |
⊢ Ⅎ𝑥𝐹 & ⊢ Ⅎ𝑥𝐴 ⇒ ⊢ Ⅎ𝑥frec(𝐹, 𝐴) | ||
Theorem | frec0g 6302 | The initial value resulting from finite recursive definition generation. (Contributed by Jim Kingdon, 7-May-2020.) |
⊢ (𝐴 ∈ 𝑉 → (frec(𝐹, 𝐴)‘∅) = 𝐴) | ||
Theorem | frecabex 6303* | The class abstraction from df-frec 6296 exists. This is a lemma for other finite recursion proofs. (Contributed by Jim Kingdon, 13-May-2020.) |
⊢ (𝜑 → 𝑆 ∈ 𝑉) & ⊢ (𝜑 → ∀𝑦(𝐹‘𝑦) ∈ V) & ⊢ (𝜑 → 𝐴 ∈ 𝑊) ⇒ ⊢ (𝜑 → {𝑥 ∣ (∃𝑚 ∈ ω (dom 𝑆 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝑆‘𝑚))) ∨ (dom 𝑆 = ∅ ∧ 𝑥 ∈ 𝐴))} ∈ V) | ||
Theorem | frecabcl 6304* | The class abstraction from df-frec 6296 exists. Unlike frecabex 6303 the function 𝐹 only needs to be defined on 𝑆, not all sets. This is a lemma for other finite recursion proofs. (Contributed by Jim Kingdon, 21-Mar-2022.) |
⊢ (𝜑 → 𝑁 ∈ ω) & ⊢ (𝜑 → 𝐺:𝑁⟶𝑆) & ⊢ (𝜑 → ∀𝑦 ∈ 𝑆 (𝐹‘𝑦) ∈ 𝑆) & ⊢ (𝜑 → 𝐴 ∈ 𝑆) ⇒ ⊢ (𝜑 → {𝑥 ∣ (∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑚))) ∨ (dom 𝐺 = ∅ ∧ 𝑥 ∈ 𝐴))} ∈ 𝑆) | ||
Theorem | frectfr 6305* |
Lemma to connect transfinite recursion theorems with finite recursion.
That is, given the conditions 𝐹 Fn V and 𝐴 ∈ 𝑉 on
frec(𝐹, 𝐴), we want to be able to apply tfri1d 6240 or tfri2d 6241,
and this lemma lets us satisfy hypotheses of those theorems.
(Contributed by Jim Kingdon, 15-Aug-2019.) |
⊢ 𝐺 = (𝑔 ∈ V ↦ {𝑥 ∣ (∃𝑚 ∈ ω (dom 𝑔 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝑔‘𝑚))) ∨ (dom 𝑔 = ∅ ∧ 𝑥 ∈ 𝐴))}) ⇒ ⊢ ((∀𝑧(𝐹‘𝑧) ∈ V ∧ 𝐴 ∈ 𝑉) → ∀𝑦(Fun 𝐺 ∧ (𝐺‘𝑦) ∈ V)) | ||
Theorem | frecfnom 6306* | The function generated by finite recursive definition generation is a function on omega. (Contributed by Jim Kingdon, 13-May-2020.) |
⊢ ((∀𝑧(𝐹‘𝑧) ∈ V ∧ 𝐴 ∈ 𝑉) → frec(𝐹, 𝐴) Fn ω) | ||
Theorem | freccllem 6307* | Lemma for freccl 6308. Just giving a name to a common expression to simplify the proof. (Contributed by Jim Kingdon, 27-Mar-2022.) |
⊢ (𝜑 → 𝐴 ∈ 𝑆) & ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑆) → (𝐹‘𝑧) ∈ 𝑆) & ⊢ (𝜑 → 𝐵 ∈ ω) & ⊢ 𝐺 = recs((𝑔 ∈ V ↦ {𝑥 ∣ (∃𝑚 ∈ ω (dom 𝑔 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝑔‘𝑚))) ∨ (dom 𝑔 = ∅ ∧ 𝑥 ∈ 𝐴))})) ⇒ ⊢ (𝜑 → (frec(𝐹, 𝐴)‘𝐵) ∈ 𝑆) | ||
Theorem | freccl 6308* | Closure for finite recursion. (Contributed by Jim Kingdon, 27-Mar-2022.) |
⊢ (𝜑 → 𝐴 ∈ 𝑆) & ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑆) → (𝐹‘𝑧) ∈ 𝑆) & ⊢ (𝜑 → 𝐵 ∈ ω) ⇒ ⊢ (𝜑 → (frec(𝐹, 𝐴)‘𝐵) ∈ 𝑆) | ||
Theorem | frecfcllem 6309* | Lemma for frecfcl 6310. 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 6310* | Finite recursion yields a function on the natural numbers. (Contributed by Jim Kingdon, 30-Mar-2022.) |
⊢ ((∀𝑧 ∈ 𝑆 (𝐹‘𝑧) ∈ 𝑆 ∧ 𝐴 ∈ 𝑆) → frec(𝐹, 𝐴):ω⟶𝑆) | ||
Theorem | frecsuclem 6311* | Lemma for frecsuc 6312. 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 6312* | The successor value resulting from finite recursive definition generation. (Contributed by Jim Kingdon, 31-Mar-2022.) |
⊢ ((∀𝑧 ∈ 𝑆 (𝐹‘𝑧) ∈ 𝑆 ∧ 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ ω) → (frec(𝐹, 𝐴)‘suc 𝐵) = (𝐹‘(frec(𝐹, 𝐴)‘𝐵))) | ||
Theorem | frecrdg 6313* |
Transfinite recursion restricted to omega.
Given a suitable characteristic function, df-frec 6296 produces the same results as df-irdg 6275 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 6314 | Extend the definition of a class to include the ordinal number 1. |
class 1o | ||
Syntax | c2o 6315 | Extend the definition of a class to include the ordinal number 2. |
class 2o | ||
Syntax | c3o 6316 | Extend the definition of a class to include the ordinal number 3. |
class 3o | ||
Syntax | c4o 6317 | Extend the definition of a class to include the ordinal number 4. |
class 4o | ||
Syntax | coa 6318 | Extend the definition of a class to include the ordinal addition operation. |
class +o | ||
Syntax | comu 6319 | Extend the definition of a class to include the ordinal multiplication operation. |
class ·o | ||
Syntax | coei 6320 | Extend the definition of a class to include the ordinal exponentiation operation. |
class ↑o | ||
Definition | df-1o 6321 | Define the ordinal number 1. (Contributed by NM, 29-Oct-1995.) |
⊢ 1o = suc ∅ | ||
Definition | df-2o 6322 | Define the ordinal number 2. (Contributed by NM, 18-Feb-2004.) |
⊢ 2o = suc 1o | ||
Definition | df-3o 6323 | Define the ordinal number 3. (Contributed by Mario Carneiro, 14-Jul-2013.) |
⊢ 3o = suc 2o | ||
Definition | df-4o 6324 | Define the ordinal number 4. (Contributed by Mario Carneiro, 14-Jul-2013.) |
⊢ 4o = suc 3o | ||
Definition | df-oadd 6325* | Define the ordinal addition operation. (Contributed by NM, 3-May-1995.) |
⊢ +o = (𝑥 ∈ On, 𝑦 ∈ On ↦ (rec((𝑧 ∈ V ↦ suc 𝑧), 𝑥)‘𝑦)) | ||
Definition | df-omul 6326* | Define the ordinal multiplication operation. (Contributed by NM, 26-Aug-1995.) |
⊢ ·o = (𝑥 ∈ On, 𝑦 ∈ On ↦ (rec((𝑧 ∈ V ↦ (𝑧 +o 𝑥)), ∅)‘𝑦)) | ||
Definition | df-oexpi 6327* |
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 6328 | Ordinal 1 is an ordinal number. (Contributed by NM, 29-Oct-1995.) |
⊢ 1o ∈ On | ||
Theorem | 1oex 6329 | Ordinal 1 is a set. (Contributed by BJ, 4-Jul-2022.) |
⊢ 1o ∈ V | ||
Theorem | 2on 6330 | Ordinal 2 is an ordinal number. (Contributed by NM, 18-Feb-2004.) (Proof shortened by Andrew Salmon, 12-Aug-2011.) |
⊢ 2o ∈ On | ||
Theorem | 2on0 6331 | Ordinal two is not zero. (Contributed by Scott Fenton, 17-Jun-2011.) |
⊢ 2o ≠ ∅ | ||
Theorem | 3on 6332 | Ordinal 3 is an ordinal number. (Contributed by Mario Carneiro, 5-Jan-2016.) |
⊢ 3o ∈ On | ||
Theorem | 4on 6333 | Ordinal 3 is an ordinal number. (Contributed by Mario Carneiro, 5-Jan-2016.) |
⊢ 4o ∈ On | ||
Theorem | df1o2 6334 | Expanded value of the ordinal number 1. (Contributed by NM, 4-Nov-2002.) |
⊢ 1o = {∅} | ||
Theorem | df2o3 6335 | Expanded value of the ordinal number 2. (Contributed by Mario Carneiro, 14-Aug-2015.) |
⊢ 2o = {∅, 1o} | ||
Theorem | df2o2 6336 | Expanded value of the ordinal number 2. (Contributed by NM, 29-Jan-2004.) |
⊢ 2o = {∅, {∅}} | ||
Theorem | 1n0 6337 | Ordinal one is not equal to ordinal zero. (Contributed by NM, 26-Dec-2004.) |
⊢ 1o ≠ ∅ | ||
Theorem | xp01disj 6338 | Cartesian products with the singletons of ordinals 0 and 1 are disjoint. (Contributed by NM, 2-Jun-2007.) |
⊢ ((𝐴 × {∅}) ∩ (𝐶 × {1o})) = ∅ | ||
Theorem | xp01disjl 6339 | Cartesian products with the singletons of ordinals 0 and 1 are disjoint. (Contributed by Jim Kingdon, 11-Jul-2023.) |
⊢ (({∅} × 𝐴) ∩ ({1o} × 𝐶)) = ∅ | ||
Theorem | ordgt0ge1 6340 | Two ways to express that an ordinal class is positive. (Contributed by NM, 21-Dec-2004.) |
⊢ (Ord 𝐴 → (∅ ∈ 𝐴 ↔ 1o ⊆ 𝐴)) | ||
Theorem | ordge1n0im 6341 | An ordinal greater than or equal to 1 is nonzero. (Contributed by Jim Kingdon, 26-Jun-2019.) |
⊢ (Ord 𝐴 → (1o ⊆ 𝐴 → 𝐴 ≠ ∅)) | ||
Theorem | el1o 6342 | Membership in ordinal one. (Contributed by NM, 5-Jan-2005.) |
⊢ (𝐴 ∈ 1o ↔ 𝐴 = ∅) | ||
Theorem | dif1o 6343 | Two ways to say that 𝐴 is a nonzero number of the set 𝐵. (Contributed by Mario Carneiro, 21-May-2015.) |
⊢ (𝐴 ∈ (𝐵 ∖ 1o) ↔ (𝐴 ∈ 𝐵 ∧ 𝐴 ≠ ∅)) | ||
Theorem | 2oconcl 6344 | Closure of the pair swapping function on 2o. (Contributed by Mario Carneiro, 27-Sep-2015.) |
⊢ (𝐴 ∈ 2o → (1o ∖ 𝐴) ∈ 2o) | ||
Theorem | 0lt1o 6345 | Ordinal zero is less than ordinal one. (Contributed by NM, 5-Jan-2005.) |
⊢ ∅ ∈ 1o | ||
Theorem | 0lt2o 6346 | Ordinal zero is less than ordinal two. (Contributed by Jim Kingdon, 31-Jul-2022.) |
⊢ ∅ ∈ 2o | ||
Theorem | 1lt2o 6347 | Ordinal one is less than ordinal two. (Contributed by Jim Kingdon, 31-Jul-2022.) |
⊢ 1o ∈ 2o | ||
Theorem | oafnex 6348 | The characteristic function for ordinal addition is defined everywhere. (Contributed by Jim Kingdon, 27-Jul-2019.) |
⊢ (𝑥 ∈ V ↦ suc 𝑥) Fn V | ||
Theorem | sucinc 6349* | Successor is increasing. (Contributed by Jim Kingdon, 25-Jun-2019.) |
⊢ 𝐹 = (𝑧 ∈ V ↦ suc 𝑧) ⇒ ⊢ ∀𝑥 𝑥 ⊆ (𝐹‘𝑥) | ||
Theorem | sucinc2 6350* | Successor is increasing. (Contributed by Jim Kingdon, 14-Jul-2019.) |
⊢ 𝐹 = (𝑧 ∈ V ↦ suc 𝑧) ⇒ ⊢ ((𝐵 ∈ On ∧ 𝐴 ∈ 𝐵) → (𝐹‘𝐴) ⊆ (𝐹‘𝐵)) | ||
Theorem | fnoa 6351 | 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 6352 | Ordinal addition is a set. (Contributed by Mario Carneiro, 3-Jul-2019.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 +o 𝐵) ∈ V) | ||
Theorem | omfnex 6353* | The characteristic function for ordinal multiplication is defined everywhere. (Contributed by Jim Kingdon, 23-Aug-2019.) |
⊢ (𝐴 ∈ 𝑉 → (𝑥 ∈ V ↦ (𝑥 +o 𝐴)) Fn V) | ||
Theorem | fnom 6354 | 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 6355 | Ordinal multiplication is a set. (Contributed by Mario Carneiro, 3-Jul-2019.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 ·o 𝐵) ∈ V) | ||
Theorem | fnoei 6356 | 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 6357 | Ordinal exponentiation is a set. (Contributed by Mario Carneiro, 3-Jul-2019.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 ↑o 𝐵) ∈ V) | ||
Theorem | oav 6358* | 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 6359* | 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 6360* | Value of ordinal exponentiation. (Contributed by Jim Kingdon, 9-Jul-2019.) |
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 ↑o 𝐵) = (rec((𝑥 ∈ V ↦ (𝑥 ·o 𝐴)), 1o)‘𝐵)) | ||
Theorem | oa0 6361 | 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 6362 | 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 6363 | 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 6364 | 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 6365 | 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 6366 | Closure law for ordinal exponentiation. (Contributed by Jim Kingdon, 26-Jul-2019.) |
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 ↑o 𝐵) ∈ On) | ||
Theorem | oav2 6367* | Value of ordinal addition. (Contributed by Mario Carneiro and Jim Kingdon, 12-Aug-2019.) |
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 +o 𝐵) = (𝐴 ∪ ∪ 𝑥 ∈ 𝐵 suc (𝐴 +o 𝑥))) | ||
Theorem | oasuc 6368 | 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 6369* | Value of ordinal multiplication. (Contributed by Jim Kingdon, 23-Aug-2019.) |
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 ·o 𝐵) = ∪ 𝑥 ∈ 𝐵 ((𝐴 ·o 𝑥) +o 𝐴)) | ||
Theorem | onasuc 6370 | Addition with successor. Theorem 4I(A2) of [Enderton] p. 79. (Contributed by Mario Carneiro, 16-Nov-2014.) |
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ ω) → (𝐴 +o suc 𝐵) = suc (𝐴 +o 𝐵)) | ||
Theorem | oa1suc 6371 | 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 6372 | 1 + 1 = 2 for ordinal numbers. (Contributed by NM, 18-Feb-2004.) |
⊢ (1o +o 1o) = 2o | ||
Theorem | oawordi 6373 | Weak ordering property of ordinal addition. (Contributed by Jim Kingdon, 27-Jul-2019.) |
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On) → (𝐴 ⊆ 𝐵 → (𝐶 +o 𝐴) ⊆ (𝐶 +o 𝐵))) | ||
Theorem | oawordriexmid 6374* | A weak ordering property of ordinal addition which implies excluded middle. The property is proposition 8.7 of [TakeutiZaring] p. 59. Compare with oawordi 6373. (Contributed by Jim Kingdon, 15-May-2022.) |
⊢ ((𝑎 ∈ On ∧ 𝑏 ∈ On ∧ 𝑐 ∈ On) → (𝑎 ⊆ 𝑏 → (𝑎 +o 𝑐) ⊆ (𝑏 +o 𝑐))) ⇒ ⊢ (𝜑 ∨ ¬ 𝜑) | ||
Theorem | oaword1 6375 | 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 6376 | 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 6377 | 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 6378 | Addition with zero. Theorem 4I(A1) of [Enderton] p. 79. (Contributed by NM, 20-Sep-1995.) |
⊢ (𝐴 ∈ ω → (𝐴 +o ∅) = 𝐴) | ||
Theorem | nnm0 6379 | Multiplication with zero. Theorem 4J(A1) of [Enderton] p. 80. (Contributed by NM, 20-Sep-1995.) |
⊢ (𝐴 ∈ ω → (𝐴 ·o ∅) = ∅) | ||
Theorem | nnasuc 6380 | 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 6381 | 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 6382 | 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 6383 | 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 6384 | 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 6385 | 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 6386 | ω is closed under addition. Inference form of nnacl 6384. (Contributed by Scott Fenton, 20-Apr-2012.) |
⊢ 𝐴 ∈ ω & ⊢ 𝐵 ∈ ω ⇒ ⊢ (𝐴 +o 𝐵) ∈ ω | ||
Theorem | nnmcli 6387 | ω is closed under multiplication. Inference form of nnmcl 6385. (Contributed by Scott Fenton, 20-Apr-2012.) |
⊢ 𝐴 ∈ ω & ⊢ 𝐵 ∈ ω ⇒ ⊢ (𝐴 ·o 𝐵) ∈ ω | ||
Theorem | nnacom 6388 | 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 6389 | 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 6390 | 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 6391 | 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 6392 | 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 6393 | 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 6394 | Distributive law for natural numbers (right-distributivity). (Contributed by Jim Kingdon, 3-Dec-2019.) |
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω ∧ 𝐶 ∈ ω) → ((𝐴 +o 𝐵) ·o 𝐶) = ((𝐴 ·o 𝐶) +o (𝐵 ·o 𝐶))) | ||
Theorem | nnsucelsuc 6395 | Membership is inherited by successors. The reverse direction holds for all ordinals, as seen at onsucelsucr 4432, but the forward direction, for all ordinals, implies excluded middle as seen as onsucelsucexmid 4453. (Contributed by Jim Kingdon, 25-Aug-2019.) |
⊢ (𝐵 ∈ ω → (𝐴 ∈ 𝐵 ↔ suc 𝐴 ∈ suc 𝐵)) | ||
Theorem | nnsucsssuc 6396 | Membership is inherited by successors. The reverse direction holds for all ordinals, as seen at onsucsssucr 4433, but the forward direction, for all ordinals, implies excluded middle as seen as onsucsssucexmid 4450. (Contributed by Jim Kingdon, 25-Aug-2019.) |
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω) → (𝐴 ⊆ 𝐵 ↔ suc 𝐴 ⊆ suc 𝐵)) | ||
Theorem | nntri3or 6397 | Trichotomy for natural numbers. (Contributed by Jim Kingdon, 25-Aug-2019.) |
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω) → (𝐴 ∈ 𝐵 ∨ 𝐴 = 𝐵 ∨ 𝐵 ∈ 𝐴)) | ||
Theorem | nntri2 6398 | A trichotomy law for natural numbers. (Contributed by Jim Kingdon, 28-Aug-2019.) |
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω) → (𝐴 ∈ 𝐵 ↔ ¬ (𝐴 = 𝐵 ∨ 𝐵 ∈ 𝐴))) | ||
Theorem | nnsucuniel 6399 | Given an element 𝐴 of the union of a natural number 𝐵, suc 𝐴 is an element of 𝐵 itself. The reverse direction holds for all ordinals (sucunielr 4434). The forward direction for all ordinals implies excluded middle (ordsucunielexmid 4454). (Contributed by Jim Kingdon, 13-Mar-2022.) |
⊢ (𝐵 ∈ ω → (𝐴 ∈ ∪ 𝐵 ↔ suc 𝐴 ∈ 𝐵)) | ||
Theorem | nntri1 6400 | A trichotomy law for natural numbers. (Contributed by Jim Kingdon, 28-Aug-2019.) |
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω) → (𝐴 ⊆ 𝐵 ↔ ¬ 𝐵 ∈ 𝐴)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |