Theorem List for Intuitionistic Logic Explorer - 8001-8100 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | elnnnn0 8001 |
The positive integer property expressed in terms of nonnegative integers.
(Contributed by NM, 10-May-2004.)
|
⊢ (𝑁 ∈
ℕ ↔ (𝑁 ∈ ℂ ∧
(𝑁 − 1) ∈ ℕ0)) |
|
Theorem | elnnnn0b 8002 |
The positive integer property expressed in terms of nonnegative integers.
(Contributed by NM, 1-Sep-2005.)
|
⊢ (𝑁 ∈
ℕ ↔ (𝑁 ∈ ℕ0 ∧ 0 < 𝑁)) |
|
Theorem | elnnnn0c 8003 |
The positive integer property expressed in terms of nonnegative integers.
(Contributed by NM, 10-Jan-2006.)
|
⊢ (𝑁 ∈
ℕ ↔ (𝑁 ∈ ℕ0 ∧ 1 ≤ 𝑁)) |
|
Theorem | nn0addge1 8004 |
A number is less than or equal to itself plus a nonnegative integer.
(Contributed by NM, 10-Mar-2005.)
|
⊢ ((A ∈ ℝ ∧ 𝑁 ∈ ℕ0) → A ≤ (A +
𝑁)) |
|
Theorem | nn0addge2 8005 |
A number is less than or equal to itself plus a nonnegative integer.
(Contributed by NM, 10-Mar-2005.)
|
⊢ ((A ∈ ℝ ∧ 𝑁 ∈ ℕ0) → A ≤ (𝑁 + A)) |
|
Theorem | nn0addge1i 8006 |
A number is less than or equal to itself plus a nonnegative integer.
(Contributed by NM, 10-Mar-2005.)
|
⊢ A ∈ ℝ & ⊢ 𝑁 ∈ ℕ0
⇒ ⊢ A ≤ (A +
𝑁) |
|
Theorem | nn0addge2i 8007 |
A number is less than or equal to itself plus a nonnegative integer.
(Contributed by NM, 10-Mar-2005.)
|
⊢ A ∈ ℝ & ⊢ 𝑁 ∈ ℕ0
⇒ ⊢ A ≤ (𝑁 + A) |
|
Theorem | nn0le2xi 8008 |
A nonnegative integer is less than or equal to twice itself.
(Contributed by Raph Levien, 10-Dec-2002.)
|
⊢ 𝑁 ∈
ℕ0 ⇒ ⊢ 𝑁 ≤ (2 · 𝑁) |
|
Theorem | nn0lele2xi 8009 |
'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 8010 |
Two ways to write the support of a function on ℕ0. (Contributed by
Mario Carneiro, 29-Dec-2014.)
|
⊢ (𝐹:𝐼⟶ℕ0 → (◡𝐹 “ (V ∖ {0})) = (◡𝐹 “ ℕ)) |
|
Theorem | nnnn0d 8011 |
A positive integer is a nonnegative integer. (Contributed by Mario
Carneiro, 27-May-2016.)
|
⊢ (φ
→ A ∈ ℕ) ⇒ ⊢ (φ → A ∈
ℕ0) |
|
Theorem | nn0red 8012 |
A nonnegative integer is a real number. (Contributed by Mario Carneiro,
27-May-2016.)
|
⊢ (φ
→ A ∈ ℕ0)
⇒ ⊢ (φ → A ∈
ℝ) |
|
Theorem | nn0cnd 8013 |
A nonnegative integer is a complex number. (Contributed by Mario
Carneiro, 27-May-2016.)
|
⊢ (φ
→ A ∈ ℕ0)
⇒ ⊢ (φ → A ∈
ℂ) |
|
Theorem | nn0ge0d 8014 |
A nonnegative integer is greater than or equal to zero. (Contributed by
Mario Carneiro, 27-May-2016.)
|
⊢ (φ
→ A ∈ ℕ0)
⇒ ⊢ (φ → 0 ≤ A) |
|
Theorem | nn0addcld 8015 |
Closure of addition of nonnegative integers, inference form.
(Contributed by Mario Carneiro, 27-May-2016.)
|
⊢ (φ
→ A ∈ ℕ0) & ⊢ (φ → B ∈
ℕ0) ⇒ ⊢ (φ → (A + B) ∈ ℕ0) |
|
Theorem | nn0mulcld 8016 |
Closure of multiplication of nonnegative integers, inference form.
(Contributed by Mario Carneiro, 27-May-2016.)
|
⊢ (φ
→ A ∈ ℕ0) & ⊢ (φ → B ∈
ℕ0) ⇒ ⊢ (φ → (A · B)
∈ ℕ0) |
|
Theorem | nn0readdcl 8017 |
Closure law for addition of reals, restricted to nonnegative integers.
(Contributed by Alexander van der Vekens, 6-Apr-2018.)
|
⊢ ((A ∈ ℕ0 ∧ B ∈ ℕ0) → (A + B) ∈ ℝ) |
|
Theorem | nn0ge2m1nn 8018 |
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 8019 |
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 8020 |
Closure law for dividing of a nonnegative integer by a positive integer.
(Contributed by Alexander van der Vekens, 14-Apr-2018.)
|
⊢ ((𝐾 ∈
ℕ0 ∧ 𝐿 ∈
ℕ) → (𝐾 / 𝐿) ∈ ℝ) |
|
3.4.8 Integers (as a subset of complex
numbers)
|
|
Syntax | cz 8021 |
Extend class notation to include the class of integers.
|
class ℤ |
|
Definition | df-z 8022 |
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 8023 |
Membership in the set of integers. (Contributed by NM, 8-Jan-2002.)
|
⊢ (𝑁 ∈
ℤ ↔ (𝑁 ∈ ℝ ∧
(𝑁 = 0 ∨ 𝑁 ∈
ℕ ∨ -𝑁 ∈
ℕ))) |
|
Theorem | nnnegz 8024 |
The negative of a positive integer is an integer. (Contributed by NM,
12-Jan-2002.)
|
⊢ (𝑁 ∈
ℕ → -𝑁 ∈ ℤ) |
|
Theorem | zre 8025 |
An integer is a real. (Contributed by NM, 8-Jan-2002.)
|
⊢ (𝑁 ∈
ℤ → 𝑁 ∈ ℝ) |
|
Theorem | zcn 8026 |
An integer is a complex number. (Contributed by NM, 9-May-2004.)
|
⊢ (𝑁 ∈
ℤ → 𝑁 ∈ ℂ) |
|
Theorem | zrei 8027 |
An integer is a real number. (Contributed by NM, 14-Jul-2005.)
|
⊢ A ∈ ℤ ⇒ ⊢ A ∈
ℝ |
|
Theorem | zssre 8028 |
The integers are a subset of the reals. (Contributed by NM,
2-Aug-2004.)
|
⊢ ℤ ⊆ ℝ |
|
Theorem | zsscn 8029 |
The integers are a subset of the complex numbers. (Contributed by NM,
2-Aug-2004.)
|
⊢ ℤ ⊆ ℂ |
|
Theorem | zex 8030 |
The set of integers exists. (Contributed by NM, 30-Jul-2004.) (Revised
by Mario Carneiro, 17-Nov-2014.)
|
⊢ ℤ ∈
V |
|
Theorem | elnnz 8031 |
Positive integer property expressed in terms of integers. (Contributed by
NM, 8-Jan-2002.)
|
⊢ (𝑁 ∈
ℕ ↔ (𝑁 ∈ ℤ ∧ 0
< 𝑁)) |
|
Theorem | 0z 8032 |
Zero is an integer. (Contributed by NM, 12-Jan-2002.)
|
⊢ 0 ∈
ℤ |
|
Theorem | 0zd 8033 |
Zero is an integer, deductive form (common case). (Contributed by David
A. Wheeler, 8-Dec-2018.)
|
⊢ (φ
→ 0 ∈ ℤ) |
|
Theorem | elnn0z 8034 |
Nonnegative integer property expressed in terms of integers. (Contributed
by NM, 9-May-2004.)
|
⊢ (𝑁 ∈
ℕ0 ↔ (𝑁 ∈
ℤ ∧ 0 ≤ 𝑁)) |
|
Theorem | elznn0nn 8035 |
Integer property expressed in terms nonnegative integers and positive
integers. (Contributed by NM, 10-May-2004.)
|
⊢ (𝑁 ∈
ℤ ↔ (𝑁 ∈ ℕ0
∨ (𝑁 ∈ ℝ ∧
-𝑁 ∈ ℕ))) |
|
Theorem | elznn0 8036 |
Integer property expressed in terms of nonnegative integers. (Contributed
by NM, 9-May-2004.)
|
⊢ (𝑁 ∈
ℤ ↔ (𝑁 ∈ ℝ ∧
(𝑁 ∈ ℕ0
∨ -𝑁 ∈ ℕ0))) |
|
Theorem | elznn 8037 |
Integer property expressed in terms of positive integers and nonnegative
integers. (Contributed by NM, 12-Jul-2005.)
|
⊢ (𝑁 ∈
ℤ ↔ (𝑁 ∈ ℝ ∧
(𝑁 ∈ ℕ ∨
-𝑁 ∈ ℕ0))) |
|
Theorem | nnssz 8038 |
Positive integers are a subset of integers. (Contributed by NM,
9-Jan-2002.)
|
⊢ ℕ ⊆ ℤ |
|
Theorem | nn0ssz 8039 |
Nonnegative integers are a subset of the integers. (Contributed by NM,
9-May-2004.)
|
⊢ ℕ0 ⊆
ℤ |
|
Theorem | nnz 8040 |
A positive integer is an integer. (Contributed by NM, 9-May-2004.)
|
⊢ (𝑁 ∈
ℕ → 𝑁 ∈ ℤ) |
|
Theorem | nn0z 8041 |
A nonnegative integer is an integer. (Contributed by NM, 9-May-2004.)
|
⊢ (𝑁 ∈
ℕ0 → 𝑁 ∈
ℤ) |
|
Theorem | nnzi 8042 |
A positive integer is an integer. (Contributed by Mario Carneiro,
18-Feb-2014.)
|
⊢ 𝑁 ∈
ℕ ⇒ ⊢ 𝑁 ∈
ℤ |
|
Theorem | nn0zi 8043 |
A nonnegative integer is an integer. (Contributed by Mario Carneiro,
18-Feb-2014.)
|
⊢ 𝑁 ∈
ℕ0 ⇒ ⊢ 𝑁 ∈
ℤ |
|
Theorem | elnnz1 8044 |
Positive integer property expressed in terms of integers. (Contributed by
NM, 10-May-2004.) (Proof shortened by Mario Carneiro, 16-May-2014.)
|
⊢ (𝑁 ∈
ℕ ↔ (𝑁 ∈ ℤ ∧ 1
≤ 𝑁)) |
|
Theorem | nnzrab 8045 |
Positive integers expressed as a subset of integers. (Contributed by NM,
3-Oct-2004.)
|
⊢ ℕ = {x ∈ ℤ
∣ 1 ≤ x} |
|
Theorem | nn0zrab 8046 |
Nonnegative integers expressed as a subset of integers. (Contributed by
NM, 3-Oct-2004.)
|
⊢ ℕ0 = {x ∈ ℤ
∣ 0 ≤ x} |
|
Theorem | 1z 8047 |
One is an integer. (Contributed by NM, 10-May-2004.)
|
⊢ 1 ∈
ℤ |
|
Theorem | 1zzd 8048 |
1 is an integer, deductive form (common case). (Contributed by David A.
Wheeler, 6-Dec-2018.)
|
⊢ (φ
→ 1 ∈ ℤ) |
|
Theorem | 2z 8049 |
Two is an integer. (Contributed by NM, 10-May-2004.)
|
⊢ 2 ∈
ℤ |
|
Theorem | 3z 8050 |
3 is an integer. (Contributed by David A. Wheeler, 8-Dec-2018.)
|
⊢ 3 ∈
ℤ |
|
Theorem | 4z 8051 |
4 is an integer. (Contributed by BJ, 26-Mar-2020.)
|
⊢ 4 ∈
ℤ |
|
Theorem | znegcl 8052 |
Closure law for negative integers. (Contributed by NM, 9-May-2004.)
|
⊢ (𝑁 ∈
ℤ → -𝑁 ∈ ℤ) |
|
Theorem | neg1z 8053 |
-1 is an integer (common case). (Contributed by David A. Wheeler,
5-Dec-2018.)
|
⊢ -1 ∈
ℤ |
|
Theorem | znegclb 8054 |
A number is an integer iff its negative is. (Contributed by Stefan
O'Rear, 13-Sep-2014.)
|
⊢ (A ∈ ℂ → (A ∈ ℤ
↔ -A ∈ ℤ)) |
|
Theorem | nn0negz 8055 |
The negative of a nonnegative integer is an integer. (Contributed by NM,
9-May-2004.)
|
⊢ (𝑁 ∈
ℕ0 → -𝑁 ∈
ℤ) |
|
Theorem | nn0negzi 8056 |
The negative of a nonnegative integer is an integer. (Contributed by
Mario Carneiro, 18-Feb-2014.)
|
⊢ 𝑁 ∈
ℕ0 ⇒ ⊢ -𝑁 ∈
ℤ |
|
Theorem | peano2z 8057 |
Second Peano postulate generalized to integers. (Contributed by NM,
13-Feb-2005.)
|
⊢ (𝑁 ∈
ℤ → (𝑁 + 1)
∈ ℤ) |
|
Theorem | zaddcllempos 8058 |
Lemma for zaddcl 8061. Special case in which 𝑁 is a
positive
integer. (Contributed by Jim Kingdon, 14-Mar-2020.)
|
⊢ ((𝑀 ∈
ℤ ∧ 𝑁 ∈
ℕ) → (𝑀 + 𝑁) ∈ ℤ) |
|
Theorem | peano2zm 8059 |
"Reverse" second Peano postulate for integers. (Contributed by NM,
12-Sep-2005.)
|
⊢ (𝑁 ∈
ℤ → (𝑁 −
1) ∈ ℤ) |
|
Theorem | zaddcllemneg 8060 |
Lemma for zaddcl 8061. Special case in which -𝑁 is a
positive
integer. (Contributed by Jim Kingdon, 14-Mar-2020.)
|
⊢ ((𝑀 ∈
ℤ ∧ 𝑁 ∈
ℝ ∧ -𝑁 ∈
ℕ) → (𝑀 + 𝑁) ∈ ℤ) |
|
Theorem | zaddcl 8061 |
Closure of addition of integers. (Contributed by NM, 9-May-2004.) (Proof
shortened by Mario Carneiro, 16-May-2014.)
|
⊢ ((𝑀 ∈
ℤ ∧ 𝑁 ∈
ℤ) → (𝑀 + 𝑁) ∈ ℤ) |
|
Theorem | zsubcl 8062 |
Closure of subtraction of integers. (Contributed by NM, 11-May-2004.)
|
⊢ ((𝑀 ∈
ℤ ∧ 𝑁 ∈
ℤ) → (𝑀 −
𝑁) ∈ ℤ) |
|
Theorem | ztri3or0 8063 |
Integer trichotomy (with zero). (Contributed by Jim Kingdon,
14-Mar-2020.)
|
⊢ (𝑁 ∈
ℤ → (𝑁 < 0
∨ 𝑁 = 0 ∨ 0
< 𝑁)) |
|
Theorem | ztri3or 8064 |
Integer trichotomy. (Contributed by Jim Kingdon, 14-Mar-2020.)
|
⊢ ((𝑀 ∈
ℤ ∧ 𝑁 ∈
ℤ) → (𝑀 <
𝑁
∨ 𝑀 = 𝑁
∨ 𝑁 < 𝑀)) |
|
Theorem | zletric 8065 |
Trichotomy law. (Contributed by Jim Kingdon, 27-Mar-2020.)
|
⊢ ((A ∈ ℤ ∧
B ∈
ℤ) → (A ≤ B ∨ B ≤ A)) |
|
Theorem | zlelttric 8066 |
Trichotomy law. (Contributed by Jim Kingdon, 17-Apr-2020.)
|
⊢ ((A ∈ ℤ ∧
B ∈
ℤ) → (A ≤ B ∨ B < A)) |
|
Theorem | zltnle 8067 |
'Less than' expressed in terms of 'less than or equal to'. (Contributed
by Jim Kingdon, 14-Mar-2020.)
|
⊢ ((A ∈ ℤ ∧
B ∈
ℤ) → (A < B ↔ ¬ B ≤ A)) |
|
Theorem | zleloe 8068 |
Integer 'Less than or equal to' expressed in terms of 'less than' or
'equals'. (Contributed by Jim Kingdon, 8-Apr-2020.)
|
⊢ ((A ∈ ℤ ∧
B ∈
ℤ) → (A ≤ B ↔ (A
< B ∨
A = B))) |
|
Theorem | znnnlt1 8069 |
An integer is not a positive integer iff it is less than one.
(Contributed by NM, 13-Jul-2005.)
|
⊢ (𝑁 ∈
ℤ → (¬ 𝑁
∈ ℕ ↔ 𝑁 < 1)) |
|
Theorem | zletr 8070 |
Transitive law of ordering for integers. (Contributed by Alexander van
der Vekens, 3-Apr-2018.)
|
⊢ ((𝐽 ∈
ℤ ∧ 𝐾 ∈
ℤ ∧ 𝐿 ∈
ℤ) → ((𝐽 ≤
𝐾 ∧ 𝐾 ≤ 𝐿) → 𝐽 ≤ 𝐿)) |
|
Theorem | zrevaddcl 8071 |
Reverse closure law for addition of integers. (Contributed by NM,
11-May-2004.)
|
⊢ (𝑁 ∈
ℤ → ((𝑀 ∈ ℂ ∧
(𝑀 + 𝑁) ∈
ℤ) ↔ 𝑀 ∈ ℤ)) |
|
Theorem | znnsub 8072 |
The positive difference of unequal integers is a positive integer.
(Generalization of nnsub 7733.) (Contributed by NM, 11-May-2004.)
|
⊢ ((𝑀 ∈
ℤ ∧ 𝑁 ∈
ℤ) → (𝑀 <
𝑁 ↔ (𝑁 − 𝑀) ∈
ℕ)) |
|
Theorem | zmulcl 8073 |
Closure of multiplication of integers. (Contributed by NM,
30-Jul-2004.)
|
⊢ ((𝑀 ∈
ℤ ∧ 𝑁 ∈
ℤ) → (𝑀
· 𝑁) ∈ ℤ) |
|
Theorem | zltp1le 8074 |
Integer ordering relation. (Contributed by NM, 10-May-2004.) (Proof
shortened by Mario Carneiro, 16-May-2014.)
|
⊢ ((𝑀 ∈
ℤ ∧ 𝑁 ∈
ℤ) → (𝑀 <
𝑁 ↔ (𝑀 + 1) ≤ 𝑁)) |
|
Theorem | zleltp1 8075 |
Integer ordering relation. (Contributed by NM, 10-May-2004.)
|
⊢ ((𝑀 ∈
ℤ ∧ 𝑁 ∈
ℤ) → (𝑀 ≤
𝑁 ↔ 𝑀 < (𝑁 + 1))) |
|
Theorem | zlem1lt 8076 |
Integer ordering relation. (Contributed by NM, 13-Nov-2004.)
|
⊢ ((𝑀 ∈
ℤ ∧ 𝑁 ∈
ℤ) → (𝑀 ≤
𝑁 ↔ (𝑀 − 1) < 𝑁)) |
|
Theorem | zltlem1 8077 |
Integer ordering relation. (Contributed by NM, 13-Nov-2004.)
|
⊢ ((𝑀 ∈
ℤ ∧ 𝑁 ∈
ℤ) → (𝑀 <
𝑁 ↔ 𝑀 ≤ (𝑁 − 1))) |
|
Theorem | zgt0ge1 8078 |
An integer greater than 0 is greater than or equal to
1.
(Contributed by AV, 14-Oct-2018.)
|
⊢ (𝑍 ∈
ℤ → (0 < 𝑍
↔ 1 ≤ 𝑍)) |
|
Theorem | nnleltp1 8079 |
Positive integer ordering relation. (Contributed by NM, 13-Aug-2001.)
(Proof shortened by Mario Carneiro, 16-May-2014.)
|
⊢ ((A ∈ ℕ ∧
B ∈
ℕ) → (A ≤ B ↔ A <
(B + 1))) |
|
Theorem | nnltp1le 8080 |
Positive integer ordering relation. (Contributed by NM, 19-Aug-2001.)
|
⊢ ((A ∈ ℕ ∧
B ∈
ℕ) → (A < B ↔ (A +
1) ≤ B)) |
|
Theorem | nnaddm1cl 8081 |
Closure of addition of positive integers minus one. (Contributed by NM,
6-Aug-2003.) (Proof shortened by Mario Carneiro, 16-May-2014.)
|
⊢ ((A ∈ ℕ ∧
B ∈
ℕ) → ((A + B) − 1) ∈
ℕ) |
|
Theorem | nn0ltp1le 8082 |
Nonnegative integer ordering relation. (Contributed by Raph Levien,
10-Dec-2002.) (Proof shortened by Mario Carneiro, 16-May-2014.)
|
⊢ ((𝑀 ∈
ℕ0 ∧ 𝑁 ∈
ℕ0) → (𝑀 < 𝑁 ↔ (𝑀 + 1) ≤ 𝑁)) |
|
Theorem | nn0leltp1 8083 |
Nonnegative integer ordering relation. (Contributed by Raph Levien,
10-Apr-2004.)
|
⊢ ((𝑀 ∈
ℕ0 ∧ 𝑁 ∈
ℕ0) → (𝑀 ≤ 𝑁 ↔ 𝑀 < (𝑁 + 1))) |
|
Theorem | nn0ltlem1 8084 |
Nonnegative integer ordering relation. (Contributed by NM, 10-May-2004.)
(Proof shortened by Mario Carneiro, 16-May-2014.)
|
⊢ ((𝑀 ∈
ℕ0 ∧ 𝑁 ∈
ℕ0) → (𝑀 < 𝑁 ↔ 𝑀 ≤ (𝑁 − 1))) |
|
Theorem | znn0sub 8085 |
The nonnegative difference of integers is a nonnegative integer.
(Generalization of nn0sub 8086.) (Contributed by NM, 14-Jul-2005.)
|
⊢ ((𝑀 ∈
ℤ ∧ 𝑁 ∈
ℤ) → (𝑀 ≤
𝑁 ↔ (𝑁 − 𝑀) ∈
ℕ0)) |
|
Theorem | nn0sub 8086 |
Subtraction of nonnegative integers. (Contributed by NM, 9-May-2004.)
|
⊢ ((𝑀 ∈
ℕ0 ∧ 𝑁 ∈
ℕ0) → (𝑀 ≤ 𝑁 ↔ (𝑁 − 𝑀) ∈
ℕ0)) |
|
Theorem | nn0n0n1ge2 8087 |
A nonnegative integer which is neither 0 nor 1 is greater than or equal to
2. (Contributed by Alexander van der Vekens, 6-Dec-2017.)
|
⊢ ((𝑁 ∈
ℕ0 ∧ 𝑁 ≠ 0 ∧
𝑁 ≠ 1) → 2 ≤
𝑁) |
|
Theorem | elz2 8088* |
Membership in the set of integers. Commonly used in constructions of
the integers as equivalence classes under subtraction of the positive
integers. (Contributed by Mario Carneiro, 16-May-2014.)
|
⊢ (𝑁 ∈
ℤ ↔ ∃x ∈ ℕ ∃y ∈ ℕ 𝑁 = (x
− y)) |
|
Theorem | dfz2 8089 |
Alternative definition of the integers, based on elz2 8088.
(Contributed
by Mario Carneiro, 16-May-2014.)
|
⊢ ℤ = ( − “ (ℕ ×
ℕ)) |
|
Theorem | nn0sub2 8090 |
Subtraction of nonnegative integers. (Contributed by NM, 4-Sep-2005.)
|
⊢ ((𝑀 ∈
ℕ0 ∧ 𝑁 ∈
ℕ0 ∧ 𝑀 ≤ 𝑁) → (𝑁 − 𝑀) ∈
ℕ0) |
|
Theorem | zapne 8091 |
Apartness is equivalent to not equal for integers. (Contributed by Jim
Kingdon, 14-Mar-2020.)
|
⊢ ((𝑀 ∈
ℤ ∧ 𝑁 ∈
ℤ) → (𝑀 # 𝑁 ↔ 𝑀 ≠ 𝑁)) |
|
Theorem | zdceq 8092 |
Equality of integers is decidable. (Contributed by Jim Kingdon,
14-Mar-2020.)
|
⊢ ((A ∈ ℤ ∧
B ∈
ℤ) → DECID A =
B) |
|
Theorem | zdcle 8093 |
Integer ≤ is decidable. (Contributed by Jim
Kingdon, 7-Apr-2020.)
|
⊢ ((A ∈ ℤ ∧
B ∈
ℤ) → DECID A
≤ B) |
|
Theorem | zdclt 8094 |
Integer < is decidable. (Contributed by Jim
Kingdon, 1-Jun-2020.)
|
⊢ ((A ∈ ℤ ∧
B ∈
ℤ) → DECID A
< B) |
|
Theorem | zltlen 8095 |
Integer 'Less than' expressed in terms of 'less than or equal to'. Also
see ltleap 7413 which is a similar result for complex
numbers. (Contributed
by Jim Kingdon, 14-Mar-2020.)
|
⊢ ((A ∈ ℤ ∧
B ∈
ℤ) → (A < B ↔ (A
≤ B ∧
B ≠ A))) |
|
Theorem | nn0n0n1ge2b 8096 |
A nonnegative integer is neither 0 nor 1 if and only if it is greater than
or equal to 2. (Contributed by Alexander van der Vekens, 17-Jan-2018.)
|
⊢ (𝑁 ∈
ℕ0 → ((𝑁 ≠ 0 ∧
𝑁 ≠ 1) ↔ 2 ≤
𝑁)) |
|
Theorem | nn0lt10b 8097 |
A nonnegative integer less than 1 is 0. (Contributed by Paul
Chapman, 22-Jun-2011.)
|
⊢ (𝑁 ∈
ℕ0 → (𝑁 < 1 ↔ 𝑁 = 0)) |
|
Theorem | nn0lt2 8098 |
A nonnegative integer less than 2 must be 0 or 1. (Contributed by
Alexander van der Vekens, 16-Sep-2018.)
|
⊢ ((𝑁 ∈
ℕ0 ∧ 𝑁 < 2) → (𝑁 = 0 ∨
𝑁 = 1)) |
|
Theorem | nn0lem1lt 8099 |
Nonnegative integer ordering relation. (Contributed by NM,
21-Jun-2005.)
|
⊢ ((𝑀 ∈
ℕ0 ∧ 𝑁 ∈
ℕ0) → (𝑀 ≤ 𝑁 ↔ (𝑀 − 1) < 𝑁)) |
|
Theorem | nnlem1lt 8100 |
Positive integer ordering relation. (Contributed by NM, 21-Jun-2005.)
|
⊢ ((𝑀 ∈
ℕ ∧ 𝑁 ∈
ℕ) → (𝑀 ≤
𝑁 ↔ (𝑀 − 1) < 𝑁)) |