![]() |
Intuitionistic Logic Explorer Theorem List (p. 91 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 | ||
Syntax | cn0 9001 | Extend class notation to include the class of nonnegative integers. |
class ℕ0 | ||
Definition | df-n0 9002 | Define the set of nonnegative integers. (Contributed by Raph Levien, 10-Dec-2002.) |
⊢ ℕ0 = (ℕ ∪ {0}) | ||
Theorem | elnn0 9003 | Nonnegative integers expressed in terms of naturals and zero. (Contributed by Raph Levien, 10-Dec-2002.) |
⊢ (𝐴 ∈ ℕ0 ↔ (𝐴 ∈ ℕ ∨ 𝐴 = 0)) | ||
Theorem | nnssnn0 9004 | Positive naturals are a subset of nonnegative integers. (Contributed by Raph Levien, 10-Dec-2002.) |
⊢ ℕ ⊆ ℕ0 | ||
Theorem | nn0ssre 9005 | Nonnegative integers are a subset of the reals. (Contributed by Raph Levien, 10-Dec-2002.) |
⊢ ℕ0 ⊆ ℝ | ||
Theorem | nn0sscn 9006 | Nonnegative integers are a subset of the complex numbers.) (Contributed by NM, 9-May-2004.) |
⊢ ℕ0 ⊆ ℂ | ||
Theorem | nn0ex 9007 | The set of nonnegative integers exists. (Contributed by NM, 18-Jul-2004.) |
⊢ ℕ0 ∈ V | ||
Theorem | nnnn0 9008 | A positive integer is a nonnegative integer. (Contributed by NM, 9-May-2004.) |
⊢ (𝐴 ∈ ℕ → 𝐴 ∈ ℕ0) | ||
Theorem | nnnn0i 9009 | A positive integer is a nonnegative integer. (Contributed by NM, 20-Jun-2005.) |
⊢ 𝑁 ∈ ℕ ⇒ ⊢ 𝑁 ∈ ℕ0 | ||
Theorem | nn0re 9010 | A nonnegative integer is a real number. (Contributed by NM, 9-May-2004.) |
⊢ (𝐴 ∈ ℕ0 → 𝐴 ∈ ℝ) | ||
Theorem | nn0cn 9011 | A nonnegative integer is a complex number. (Contributed by NM, 9-May-2004.) |
⊢ (𝐴 ∈ ℕ0 → 𝐴 ∈ ℂ) | ||
Theorem | nn0rei 9012 | A nonnegative integer is a real number. (Contributed by NM, 14-May-2003.) |
⊢ 𝐴 ∈ ℕ0 ⇒ ⊢ 𝐴 ∈ ℝ | ||
Theorem | nn0cni 9013 | A nonnegative integer is a complex number. (Contributed by NM, 14-May-2003.) |
⊢ 𝐴 ∈ ℕ0 ⇒ ⊢ 𝐴 ∈ ℂ | ||
Theorem | dfn2 9014 | The set of positive integers defined in terms of nonnegative integers. (Contributed by NM, 23-Sep-2007.) (Proof shortened by Mario Carneiro, 13-Feb-2013.) |
⊢ ℕ = (ℕ0 ∖ {0}) | ||
Theorem | elnnne0 9015 | The positive integer property expressed in terms of difference from zero. (Contributed by Stefan O'Rear, 12-Sep-2015.) |
⊢ (𝑁 ∈ ℕ ↔ (𝑁 ∈ ℕ0 ∧ 𝑁 ≠ 0)) | ||
Theorem | 0nn0 9016 | 0 is a nonnegative integer. (Contributed by Raph Levien, 10-Dec-2002.) |
⊢ 0 ∈ ℕ0 | ||
Theorem | 1nn0 9017 | 1 is a nonnegative integer. (Contributed by Raph Levien, 10-Dec-2002.) |
⊢ 1 ∈ ℕ0 | ||
Theorem | 2nn0 9018 | 2 is a nonnegative integer. (Contributed by Raph Levien, 10-Dec-2002.) |
⊢ 2 ∈ ℕ0 | ||
Theorem | 3nn0 9019 | 3 is a nonnegative integer. (Contributed by Mario Carneiro, 18-Feb-2014.) |
⊢ 3 ∈ ℕ0 | ||
Theorem | 4nn0 9020 | 4 is a nonnegative integer. (Contributed by Mario Carneiro, 18-Feb-2014.) |
⊢ 4 ∈ ℕ0 | ||
Theorem | 5nn0 9021 | 5 is a nonnegative integer. (Contributed by Mario Carneiro, 19-Apr-2015.) |
⊢ 5 ∈ ℕ0 | ||
Theorem | 6nn0 9022 | 6 is a nonnegative integer. (Contributed by Mario Carneiro, 19-Apr-2015.) |
⊢ 6 ∈ ℕ0 | ||
Theorem | 7nn0 9023 | 7 is a nonnegative integer. (Contributed by Mario Carneiro, 19-Apr-2015.) |
⊢ 7 ∈ ℕ0 | ||
Theorem | 8nn0 9024 | 8 is a nonnegative integer. (Contributed by Mario Carneiro, 19-Apr-2015.) |
⊢ 8 ∈ ℕ0 | ||
Theorem | 9nn0 9025 | 9 is a nonnegative integer. (Contributed by Mario Carneiro, 19-Apr-2015.) |
⊢ 9 ∈ ℕ0 | ||
Theorem | nn0ge0 9026 | A nonnegative integer is greater than or equal to zero. (Contributed by NM, 9-May-2004.) (Revised by Mario Carneiro, 16-May-2014.) |
⊢ (𝑁 ∈ ℕ0 → 0 ≤ 𝑁) | ||
Theorem | nn0nlt0 9027 | A nonnegative integer is not less than zero. (Contributed by NM, 9-May-2004.) (Revised by Mario Carneiro, 27-May-2016.) |
⊢ (𝐴 ∈ ℕ0 → ¬ 𝐴 < 0) | ||
Theorem | nn0ge0i 9028 | Nonnegative integers are nonnegative. (Contributed by Raph Levien, 10-Dec-2002.) |
⊢ 𝑁 ∈ ℕ0 ⇒ ⊢ 0 ≤ 𝑁 | ||
Theorem | nn0le0eq0 9029 | A nonnegative integer is less than or equal to zero iff it is equal to zero. (Contributed by NM, 9-Dec-2005.) |
⊢ (𝑁 ∈ ℕ0 → (𝑁 ≤ 0 ↔ 𝑁 = 0)) | ||
Theorem | nn0p1gt0 9030 | A nonnegative integer increased by 1 is greater than 0. (Contributed by Alexander van der Vekens, 3-Oct-2018.) |
⊢ (𝑁 ∈ ℕ0 → 0 < (𝑁 + 1)) | ||
Theorem | nnnn0addcl 9031 | A positive integer plus a nonnegative integer is a positive integer. (Contributed by NM, 20-Apr-2005.) (Proof shortened by Mario Carneiro, 16-May-2014.) |
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ0) → (𝑀 + 𝑁) ∈ ℕ) | ||
Theorem | nn0nnaddcl 9032 | A nonnegative integer plus a positive integer is a positive integer. (Contributed by NM, 22-Dec-2005.) |
⊢ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ) → (𝑀 + 𝑁) ∈ ℕ) | ||
Theorem | 0mnnnnn0 9033 | The result of subtracting a positive integer from 0 is not a nonnegative integer. (Contributed by Alexander van der Vekens, 19-Mar-2018.) |
⊢ (𝑁 ∈ ℕ → (0 − 𝑁) ∉ ℕ0) | ||
Theorem | un0addcl 9034 | If 𝑆 is closed under addition, then so is 𝑆 ∪ {0}. (Contributed by Mario Carneiro, 17-Jul-2014.) |
⊢ (𝜑 → 𝑆 ⊆ ℂ) & ⊢ 𝑇 = (𝑆 ∪ {0}) & ⊢ ((𝜑 ∧ (𝑀 ∈ 𝑆 ∧ 𝑁 ∈ 𝑆)) → (𝑀 + 𝑁) ∈ 𝑆) ⇒ ⊢ ((𝜑 ∧ (𝑀 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇)) → (𝑀 + 𝑁) ∈ 𝑇) | ||
Theorem | un0mulcl 9035 | If 𝑆 is closed under multiplication, then so is 𝑆 ∪ {0}. (Contributed by Mario Carneiro, 17-Jul-2014.) |
⊢ (𝜑 → 𝑆 ⊆ ℂ) & ⊢ 𝑇 = (𝑆 ∪ {0}) & ⊢ ((𝜑 ∧ (𝑀 ∈ 𝑆 ∧ 𝑁 ∈ 𝑆)) → (𝑀 · 𝑁) ∈ 𝑆) ⇒ ⊢ ((𝜑 ∧ (𝑀 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇)) → (𝑀 · 𝑁) ∈ 𝑇) | ||
Theorem | nn0addcl 9036 | Closure of addition of nonnegative integers. (Contributed by Raph Levien, 10-Dec-2002.) (Proof shortened by Mario Carneiro, 17-Jul-2014.) |
⊢ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) → (𝑀 + 𝑁) ∈ ℕ0) | ||
Theorem | nn0mulcl 9037 | Closure of multiplication of nonnegative integers. (Contributed by NM, 22-Jul-2004.) (Proof shortened by Mario Carneiro, 17-Jul-2014.) |
⊢ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) → (𝑀 · 𝑁) ∈ ℕ0) | ||
Theorem | nn0addcli 9038 | Closure of addition of nonnegative integers, inference form. (Contributed by Raph Levien, 10-Dec-2002.) |
⊢ 𝑀 ∈ ℕ0 & ⊢ 𝑁 ∈ ℕ0 ⇒ ⊢ (𝑀 + 𝑁) ∈ ℕ0 | ||
Theorem | nn0mulcli 9039 | Closure of multiplication of nonnegative integers, inference form. (Contributed by Raph Levien, 10-Dec-2002.) |
⊢ 𝑀 ∈ ℕ0 & ⊢ 𝑁 ∈ ℕ0 ⇒ ⊢ (𝑀 · 𝑁) ∈ ℕ0 | ||
Theorem | nn0p1nn 9040 | A nonnegative integer plus 1 is a positive integer. (Contributed by Raph Levien, 30-Jun-2006.) (Revised by Mario Carneiro, 16-May-2014.) |
⊢ (𝑁 ∈ ℕ0 → (𝑁 + 1) ∈ ℕ) | ||
Theorem | peano2nn0 9041 | Second Peano postulate for nonnegative integers. (Contributed by NM, 9-May-2004.) |
⊢ (𝑁 ∈ ℕ0 → (𝑁 + 1) ∈ ℕ0) | ||
Theorem | nnm1nn0 9042 | A positive integer minus 1 is a nonnegative integer. (Contributed by Jason Orendorff, 24-Jan-2007.) (Revised by Mario Carneiro, 16-May-2014.) |
⊢ (𝑁 ∈ ℕ → (𝑁 − 1) ∈ ℕ0) | ||
Theorem | elnn0nn 9043 | The nonnegative integer property expressed in terms of positive integers. (Contributed by NM, 10-May-2004.) (Proof shortened by Mario Carneiro, 16-May-2014.) |
⊢ (𝑁 ∈ ℕ0 ↔ (𝑁 ∈ ℂ ∧ (𝑁 + 1) ∈ ℕ)) | ||
Theorem | elnnnn0 9044 | The positive integer property expressed in terms of nonnegative integers. (Contributed by NM, 10-May-2004.) |
⊢ (𝑁 ∈ ℕ ↔ (𝑁 ∈ ℂ ∧ (𝑁 − 1) ∈ ℕ0)) | ||
Theorem | elnnnn0b 9045 | The positive integer property expressed in terms of nonnegative integers. (Contributed by NM, 1-Sep-2005.) |
⊢ (𝑁 ∈ ℕ ↔ (𝑁 ∈ ℕ0 ∧ 0 < 𝑁)) | ||
Theorem | elnnnn0c 9046 | The positive integer property expressed in terms of nonnegative integers. (Contributed by NM, 10-Jan-2006.) |
⊢ (𝑁 ∈ ℕ ↔ (𝑁 ∈ ℕ0 ∧ 1 ≤ 𝑁)) | ||
Theorem | nn0addge1 9047 | A number is less than or equal to itself plus a nonnegative integer. (Contributed by NM, 10-Mar-2005.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝑁 ∈ ℕ0) → 𝐴 ≤ (𝐴 + 𝑁)) | ||
Theorem | nn0addge2 9048 | A number is less than or equal to itself plus a nonnegative integer. (Contributed by NM, 10-Mar-2005.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝑁 ∈ ℕ0) → 𝐴 ≤ (𝑁 + 𝐴)) | ||
Theorem | nn0addge1i 9049 | A number is less than or equal to itself plus a nonnegative integer. (Contributed by NM, 10-Mar-2005.) |
⊢ 𝐴 ∈ ℝ & ⊢ 𝑁 ∈ ℕ0 ⇒ ⊢ 𝐴 ≤ (𝐴 + 𝑁) | ||
Theorem | nn0addge2i 9050 | A number is less than or equal to itself plus a nonnegative integer. (Contributed by NM, 10-Mar-2005.) |
⊢ 𝐴 ∈ ℝ & ⊢ 𝑁 ∈ ℕ0 ⇒ ⊢ 𝐴 ≤ (𝑁 + 𝐴) | ||
Theorem | nn0le2xi 9051 | A nonnegative integer is less than or equal to twice itself. (Contributed by Raph Levien, 10-Dec-2002.) |
⊢ 𝑁 ∈ ℕ0 ⇒ ⊢ 𝑁 ≤ (2 · 𝑁) | ||
Theorem | nn0lele2xi 9052 | 'Less than or equal to' implies 'less than or equal to twice' for nonnegative integers. (Contributed by Raph Levien, 10-Dec-2002.) |
⊢ 𝑀 ∈ ℕ0 & ⊢ 𝑁 ∈ ℕ0 ⇒ ⊢ (𝑁 ≤ 𝑀 → 𝑁 ≤ (2 · 𝑀)) | ||
Theorem | nn0supp 9053 | Two ways to write the support of a function on ℕ0. (Contributed by Mario Carneiro, 29-Dec-2014.) |
⊢ (𝐹:𝐼⟶ℕ0 → (◡𝐹 “ (V ∖ {0})) = (◡𝐹 “ ℕ)) | ||
Theorem | nnnn0d 9054 | A positive integer is a nonnegative integer. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℕ) ⇒ ⊢ (𝜑 → 𝐴 ∈ ℕ0) | ||
Theorem | nn0red 9055 | A nonnegative integer is a real number. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℕ0) ⇒ ⊢ (𝜑 → 𝐴 ∈ ℝ) | ||
Theorem | nn0cnd 9056 | A nonnegative integer is a complex number. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℕ0) ⇒ ⊢ (𝜑 → 𝐴 ∈ ℂ) | ||
Theorem | nn0ge0d 9057 | A nonnegative integer is greater than or equal to zero. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℕ0) ⇒ ⊢ (𝜑 → 0 ≤ 𝐴) | ||
Theorem | nn0addcld 9058 | Closure of addition of nonnegative integers, inference form. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℕ0) & ⊢ (𝜑 → 𝐵 ∈ ℕ0) ⇒ ⊢ (𝜑 → (𝐴 + 𝐵) ∈ ℕ0) | ||
Theorem | nn0mulcld 9059 | Closure of multiplication of nonnegative integers, inference form. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℕ0) & ⊢ (𝜑 → 𝐵 ∈ ℕ0) ⇒ ⊢ (𝜑 → (𝐴 · 𝐵) ∈ ℕ0) | ||
Theorem | nn0readdcl 9060 | Closure law for addition of reals, restricted to nonnegative integers. (Contributed by Alexander van der Vekens, 6-Apr-2018.) |
⊢ ((𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ0) → (𝐴 + 𝐵) ∈ ℝ) | ||
Theorem | nn0ge2m1nn 9061 | If a nonnegative integer is greater than or equal to two, the integer decreased by 1 is a positive integer. (Contributed by Alexander van der Vekens, 1-Aug-2018.) (Revised by AV, 4-Jan-2020.) |
⊢ ((𝑁 ∈ ℕ0 ∧ 2 ≤ 𝑁) → (𝑁 − 1) ∈ ℕ) | ||
Theorem | nn0ge2m1nn0 9062 | If a nonnegative integer is greater than or equal to two, the integer decreased by 1 is also a nonnegative integer. (Contributed by Alexander van der Vekens, 1-Aug-2018.) |
⊢ ((𝑁 ∈ ℕ0 ∧ 2 ≤ 𝑁) → (𝑁 − 1) ∈ ℕ0) | ||
Theorem | nn0nndivcl 9063 | Closure law for dividing of a nonnegative integer by a positive integer. (Contributed by Alexander van der Vekens, 14-Apr-2018.) |
⊢ ((𝐾 ∈ ℕ0 ∧ 𝐿 ∈ ℕ) → (𝐾 / 𝐿) ∈ ℝ) | ||
The function values of the hash (set size) function are either nonnegative integers or positive infinity. To avoid the need to distinguish between finite and infinite sets (and therefore if the set size is a nonnegative integer or positive infinity), it is useful to provide a definition of the set of nonnegative integers extended by positive infinity, analogously to the extension of the real numbers ℝ*, see df-xr 7828. | ||
Syntax | cxnn0 9064 | The set of extended nonnegative integers. |
class ℕ0* | ||
Definition | df-xnn0 9065 | Define the set of extended nonnegative integers that includes positive infinity. Analogue of the extension of the real numbers ℝ*, see df-xr 7828. If we assumed excluded middle, this would be essentially the same as ℕ∞ as defined at df-nninf 7015 but in its absence the relationship between the two is more complicated. (Contributed by AV, 10-Dec-2020.) |
⊢ ℕ0* = (ℕ0 ∪ {+∞}) | ||
Theorem | elxnn0 9066 | An extended nonnegative integer is either a standard nonnegative integer or positive infinity. (Contributed by AV, 10-Dec-2020.) |
⊢ (𝐴 ∈ ℕ0* ↔ (𝐴 ∈ ℕ0 ∨ 𝐴 = +∞)) | ||
Theorem | nn0ssxnn0 9067 | The standard nonnegative integers are a subset of the extended nonnegative integers. (Contributed by AV, 10-Dec-2020.) |
⊢ ℕ0 ⊆ ℕ0* | ||
Theorem | nn0xnn0 9068 | A standard nonnegative integer is an extended nonnegative integer. (Contributed by AV, 10-Dec-2020.) |
⊢ (𝐴 ∈ ℕ0 → 𝐴 ∈ ℕ0*) | ||
Theorem | xnn0xr 9069 | An extended nonnegative integer is an extended real. (Contributed by AV, 10-Dec-2020.) |
⊢ (𝐴 ∈ ℕ0* → 𝐴 ∈ ℝ*) | ||
Theorem | 0xnn0 9070 | Zero is an extended nonnegative integer. (Contributed by AV, 10-Dec-2020.) |
⊢ 0 ∈ ℕ0* | ||
Theorem | pnf0xnn0 9071 | Positive infinity is an extended nonnegative integer. (Contributed by AV, 10-Dec-2020.) |
⊢ +∞ ∈ ℕ0* | ||
Theorem | nn0nepnf 9072 | No standard nonnegative integer equals positive infinity. (Contributed by AV, 10-Dec-2020.) |
⊢ (𝐴 ∈ ℕ0 → 𝐴 ≠ +∞) | ||
Theorem | nn0xnn0d 9073 | A standard nonnegative integer is an extended nonnegative integer, deduction form. (Contributed by AV, 10-Dec-2020.) |
⊢ (𝜑 → 𝐴 ∈ ℕ0) ⇒ ⊢ (𝜑 → 𝐴 ∈ ℕ0*) | ||
Theorem | nn0nepnfd 9074 | No standard nonnegative integer equals positive infinity, deduction form. (Contributed by AV, 10-Dec-2020.) |
⊢ (𝜑 → 𝐴 ∈ ℕ0) ⇒ ⊢ (𝜑 → 𝐴 ≠ +∞) | ||
Theorem | xnn0nemnf 9075 | No extended nonnegative integer equals negative infinity. (Contributed by AV, 10-Dec-2020.) |
⊢ (𝐴 ∈ ℕ0* → 𝐴 ≠ -∞) | ||
Theorem | xnn0xrnemnf 9076 | The extended nonnegative integers are extended reals without negative infinity. (Contributed by AV, 10-Dec-2020.) |
⊢ (𝐴 ∈ ℕ0* → (𝐴 ∈ ℝ* ∧ 𝐴 ≠ -∞)) | ||
Theorem | xnn0nnn0pnf 9077 | An extended nonnegative integer which is not a standard nonnegative integer is positive infinity. (Contributed by AV, 10-Dec-2020.) |
⊢ ((𝑁 ∈ ℕ0* ∧ ¬ 𝑁 ∈ ℕ0) → 𝑁 = +∞) | ||
Syntax | cz 9078 | Extend class notation to include the class of integers. |
class ℤ | ||
Definition | df-z 9079 | Define the set of integers, which are the positive and negative integers together with zero. Definition of integers in [Apostol] p. 22. The letter Z abbreviates the German word Zahlen meaning "numbers." (Contributed by NM, 8-Jan-2002.) |
⊢ ℤ = {𝑛 ∈ ℝ ∣ (𝑛 = 0 ∨ 𝑛 ∈ ℕ ∨ -𝑛 ∈ ℕ)} | ||
Theorem | elz 9080 | Membership in the set of integers. (Contributed by NM, 8-Jan-2002.) |
⊢ (𝑁 ∈ ℤ ↔ (𝑁 ∈ ℝ ∧ (𝑁 = 0 ∨ 𝑁 ∈ ℕ ∨ -𝑁 ∈ ℕ))) | ||
Theorem | nnnegz 9081 | The negative of a positive integer is an integer. (Contributed by NM, 12-Jan-2002.) |
⊢ (𝑁 ∈ ℕ → -𝑁 ∈ ℤ) | ||
Theorem | zre 9082 | An integer is a real. (Contributed by NM, 8-Jan-2002.) |
⊢ (𝑁 ∈ ℤ → 𝑁 ∈ ℝ) | ||
Theorem | zcn 9083 | An integer is a complex number. (Contributed by NM, 9-May-2004.) |
⊢ (𝑁 ∈ ℤ → 𝑁 ∈ ℂ) | ||
Theorem | zrei 9084 | An integer is a real number. (Contributed by NM, 14-Jul-2005.) |
⊢ 𝐴 ∈ ℤ ⇒ ⊢ 𝐴 ∈ ℝ | ||
Theorem | zssre 9085 | The integers are a subset of the reals. (Contributed by NM, 2-Aug-2004.) |
⊢ ℤ ⊆ ℝ | ||
Theorem | zsscn 9086 | The integers are a subset of the complex numbers. (Contributed by NM, 2-Aug-2004.) |
⊢ ℤ ⊆ ℂ | ||
Theorem | zex 9087 | The set of integers exists. (Contributed by NM, 30-Jul-2004.) (Revised by Mario Carneiro, 17-Nov-2014.) |
⊢ ℤ ∈ V | ||
Theorem | elnnz 9088 | Positive integer property expressed in terms of integers. (Contributed by NM, 8-Jan-2002.) |
⊢ (𝑁 ∈ ℕ ↔ (𝑁 ∈ ℤ ∧ 0 < 𝑁)) | ||
Theorem | 0z 9089 | Zero is an integer. (Contributed by NM, 12-Jan-2002.) |
⊢ 0 ∈ ℤ | ||
Theorem | 0zd 9090 | Zero is an integer, deductive form (common case). (Contributed by David A. Wheeler, 8-Dec-2018.) |
⊢ (𝜑 → 0 ∈ ℤ) | ||
Theorem | elnn0z 9091 | Nonnegative integer property expressed in terms of integers. (Contributed by NM, 9-May-2004.) |
⊢ (𝑁 ∈ ℕ0 ↔ (𝑁 ∈ ℤ ∧ 0 ≤ 𝑁)) | ||
Theorem | elznn0nn 9092 | Integer property expressed in terms nonnegative integers and positive integers. (Contributed by NM, 10-May-2004.) |
⊢ (𝑁 ∈ ℤ ↔ (𝑁 ∈ ℕ0 ∨ (𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ))) | ||
Theorem | elznn0 9093 | Integer property expressed in terms of nonnegative integers. (Contributed by NM, 9-May-2004.) |
⊢ (𝑁 ∈ ℤ ↔ (𝑁 ∈ ℝ ∧ (𝑁 ∈ ℕ0 ∨ -𝑁 ∈ ℕ0))) | ||
Theorem | elznn 9094 | Integer property expressed in terms of positive integers and nonnegative integers. (Contributed by NM, 12-Jul-2005.) |
⊢ (𝑁 ∈ ℤ ↔ (𝑁 ∈ ℝ ∧ (𝑁 ∈ ℕ ∨ -𝑁 ∈ ℕ0))) | ||
Theorem | nnssz 9095 | Positive integers are a subset of integers. (Contributed by NM, 9-Jan-2002.) |
⊢ ℕ ⊆ ℤ | ||
Theorem | nn0ssz 9096 | Nonnegative integers are a subset of the integers. (Contributed by NM, 9-May-2004.) |
⊢ ℕ0 ⊆ ℤ | ||
Theorem | nnz 9097 | A positive integer is an integer. (Contributed by NM, 9-May-2004.) |
⊢ (𝑁 ∈ ℕ → 𝑁 ∈ ℤ) | ||
Theorem | nn0z 9098 | A nonnegative integer is an integer. (Contributed by NM, 9-May-2004.) |
⊢ (𝑁 ∈ ℕ0 → 𝑁 ∈ ℤ) | ||
Theorem | nnzi 9099 | A positive integer is an integer. (Contributed by Mario Carneiro, 18-Feb-2014.) |
⊢ 𝑁 ∈ ℕ ⇒ ⊢ 𝑁 ∈ ℤ | ||
Theorem | nn0zi 9100 | A nonnegative integer is an integer. (Contributed by Mario Carneiro, 18-Feb-2014.) |
⊢ 𝑁 ∈ ℕ0 ⇒ ⊢ 𝑁 ∈ ℤ |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |