Theorem List for Intuitionistic Logic Explorer - 8201-8300 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | 5nn0 8201 |
5 is a nonnegative integer. (Contributed by Mario Carneiro,
19-Apr-2015.)
|
⊢ 5 ∈
ℕ0 |
|
Theorem | 6nn0 8202 |
6 is a nonnegative integer. (Contributed by Mario Carneiro,
19-Apr-2015.)
|
⊢ 6 ∈
ℕ0 |
|
Theorem | 7nn0 8203 |
7 is a nonnegative integer. (Contributed by Mario Carneiro,
19-Apr-2015.)
|
⊢ 7 ∈
ℕ0 |
|
Theorem | 8nn0 8204 |
8 is a nonnegative integer. (Contributed by Mario Carneiro,
19-Apr-2015.)
|
⊢ 8 ∈
ℕ0 |
|
Theorem | 9nn0 8205 |
9 is a nonnegative integer. (Contributed by Mario Carneiro,
19-Apr-2015.)
|
⊢ 9 ∈
ℕ0 |
|
Theorem | 10nn0 8206 |
10 is a nonnegative integer. (Contributed by Mario Carneiro,
19-Apr-2015.)
|
⊢ 10 ∈
ℕ0 |
|
Theorem | nn0ge0 8207 |
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 8208 |
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 8209 |
Nonnegative integers are nonnegative. (Contributed by Raph Levien,
10-Dec-2002.)
|
⊢ 𝑁 ∈
ℕ0 ⇒ ⊢ 0 ≤ 𝑁 |
|
Theorem | nn0le0eq0 8210 |
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 8211 |
A nonnegative integer increased by 1 is greater than 0. (Contributed by
Alexander van der Vekens, 3-Oct-2018.)
|
⊢ (𝑁 ∈ ℕ0 → 0 <
(𝑁 + 1)) |
|
Theorem | nnnn0addcl 8212 |
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 8213 |
A nonnegative integer plus a positive integer is a positive integer.
(Contributed by NM, 22-Dec-2005.)
|
⊢ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ) → (𝑀 + 𝑁) ∈ ℕ) |
|
Theorem | 0mnnnnn0 8214 |
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 8215 |
If 𝑆 is closed under addition, then so is
𝑆 ∪
{0}.
(Contributed by Mario Carneiro, 17-Jul-2014.)
|
⊢ (𝜑 → 𝑆 ⊆ ℂ) & ⊢ 𝑇 = (𝑆 ∪ {0}) & ⊢ ((𝜑 ∧ (𝑀 ∈ 𝑆 ∧ 𝑁 ∈ 𝑆)) → (𝑀 + 𝑁) ∈ 𝑆) ⇒ ⊢ ((𝜑 ∧ (𝑀 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇)) → (𝑀 + 𝑁) ∈ 𝑇) |
|
Theorem | un0mulcl 8216 |
If 𝑆 is closed under multiplication, then
so is 𝑆
∪ {0}.
(Contributed by Mario Carneiro, 17-Jul-2014.)
|
⊢ (𝜑 → 𝑆 ⊆ ℂ) & ⊢ 𝑇 = (𝑆 ∪ {0}) & ⊢ ((𝜑 ∧ (𝑀 ∈ 𝑆 ∧ 𝑁 ∈ 𝑆)) → (𝑀 · 𝑁) ∈ 𝑆) ⇒ ⊢ ((𝜑 ∧ (𝑀 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇)) → (𝑀 · 𝑁) ∈ 𝑇) |
|
Theorem | nn0addcl 8217 |
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 8218 |
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 8219 |
Closure of addition of nonnegative integers, inference form.
(Contributed by Raph Levien, 10-Dec-2002.)
|
⊢ 𝑀 ∈ ℕ0 & ⊢ 𝑁 ∈
ℕ0 ⇒ ⊢ (𝑀 + 𝑁) ∈
ℕ0 |
|
Theorem | nn0mulcli 8220 |
Closure of multiplication of nonnegative integers, inference form.
(Contributed by Raph Levien, 10-Dec-2002.)
|
⊢ 𝑀 ∈ ℕ0 & ⊢ 𝑁 ∈
ℕ0 ⇒ ⊢ (𝑀 · 𝑁) ∈
ℕ0 |
|
Theorem | nn0p1nn 8221 |
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 8222 |
Second Peano postulate for nonnegative integers. (Contributed by NM,
9-May-2004.)
|
⊢ (𝑁 ∈ ℕ0 → (𝑁 + 1) ∈
ℕ0) |
|
Theorem | nnm1nn0 8223 |
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 8224 |
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 8225 |
The positive integer property expressed in terms of nonnegative integers.
(Contributed by NM, 10-May-2004.)
|
⊢ (𝑁 ∈ ℕ ↔ (𝑁 ∈ ℂ ∧ (𝑁 − 1) ∈
ℕ0)) |
|
Theorem | elnnnn0b 8226 |
The positive integer property expressed in terms of nonnegative integers.
(Contributed by NM, 1-Sep-2005.)
|
⊢ (𝑁 ∈ ℕ ↔ (𝑁 ∈ ℕ0 ∧ 0 <
𝑁)) |
|
Theorem | elnnnn0c 8227 |
The positive integer property expressed in terms of nonnegative integers.
(Contributed by NM, 10-Jan-2006.)
|
⊢ (𝑁 ∈ ℕ ↔ (𝑁 ∈ ℕ0 ∧ 1 ≤
𝑁)) |
|
Theorem | nn0addge1 8228 |
A number is less than or equal to itself plus a nonnegative integer.
(Contributed by NM, 10-Mar-2005.)
|
⊢ ((𝐴 ∈ ℝ ∧ 𝑁 ∈ ℕ0) → 𝐴 ≤ (𝐴 + 𝑁)) |
|
Theorem | nn0addge2 8229 |
A number is less than or equal to itself plus a nonnegative integer.
(Contributed by NM, 10-Mar-2005.)
|
⊢ ((𝐴 ∈ ℝ ∧ 𝑁 ∈ ℕ0) → 𝐴 ≤ (𝑁 + 𝐴)) |
|
Theorem | nn0addge1i 8230 |
A number is less than or equal to itself plus a nonnegative integer.
(Contributed by NM, 10-Mar-2005.)
|
⊢ 𝐴 ∈ ℝ & ⊢ 𝑁 ∈
ℕ0 ⇒ ⊢ 𝐴 ≤ (𝐴 + 𝑁) |
|
Theorem | nn0addge2i 8231 |
A number is less than or equal to itself plus a nonnegative integer.
(Contributed by NM, 10-Mar-2005.)
|
⊢ 𝐴 ∈ ℝ & ⊢ 𝑁 ∈
ℕ0 ⇒ ⊢ 𝐴 ≤ (𝑁 + 𝐴) |
|
Theorem | nn0le2xi 8232 |
A nonnegative integer is less than or equal to twice itself.
(Contributed by Raph Levien, 10-Dec-2002.)
|
⊢ 𝑁 ∈
ℕ0 ⇒ ⊢ 𝑁 ≤ (2 · 𝑁) |
|
Theorem | nn0lele2xi 8233 |
'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 8234 |
Two ways to write the support of a function on ℕ0. (Contributed by
Mario Carneiro, 29-Dec-2014.)
|
⊢ (𝐹:𝐼⟶ℕ0 → (◡𝐹 “ (V ∖ {0})) = (◡𝐹 “ ℕ)) |
|
Theorem | nnnn0d 8235 |
A positive integer is a nonnegative integer. (Contributed by Mario
Carneiro, 27-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℕ)
⇒ ⊢ (𝜑 → 𝐴 ∈
ℕ0) |
|
Theorem | nn0red 8236 |
A nonnegative integer is a real number. (Contributed by Mario Carneiro,
27-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈
ℕ0) ⇒ ⊢ (𝜑 → 𝐴 ∈ ℝ) |
|
Theorem | nn0cnd 8237 |
A nonnegative integer is a complex number. (Contributed by Mario
Carneiro, 27-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈
ℕ0) ⇒ ⊢ (𝜑 → 𝐴 ∈ ℂ) |
|
Theorem | nn0ge0d 8238 |
A nonnegative integer is greater than or equal to zero. (Contributed by
Mario Carneiro, 27-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈
ℕ0) ⇒ ⊢ (𝜑 → 0 ≤ 𝐴) |
|
Theorem | nn0addcld 8239 |
Closure of addition of nonnegative integers, inference form.
(Contributed by Mario Carneiro, 27-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℕ0) & ⊢ (𝜑 → 𝐵 ∈
ℕ0) ⇒ ⊢ (𝜑 → (𝐴 + 𝐵) ∈
ℕ0) |
|
Theorem | nn0mulcld 8240 |
Closure of multiplication of nonnegative integers, inference form.
(Contributed by Mario Carneiro, 27-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℕ0) & ⊢ (𝜑 → 𝐵 ∈
ℕ0) ⇒ ⊢ (𝜑 → (𝐴 · 𝐵) ∈
ℕ0) |
|
Theorem | nn0readdcl 8241 |
Closure law for addition of reals, restricted to nonnegative integers.
(Contributed by Alexander van der Vekens, 6-Apr-2018.)
|
⊢ ((𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ0)
→ (𝐴 + 𝐵) ∈
ℝ) |
|
Theorem | nn0ge2m1nn 8242 |
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 8243 |
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 8244 |
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 8245 |
Extend class notation to include the class of integers.
|
class ℤ |
|
Definition | df-z 8246 |
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 8247 |
Membership in the set of integers. (Contributed by NM, 8-Jan-2002.)
|
⊢ (𝑁 ∈ ℤ ↔ (𝑁 ∈ ℝ ∧ (𝑁 = 0 ∨ 𝑁 ∈ ℕ ∨ -𝑁 ∈ ℕ))) |
|
Theorem | nnnegz 8248 |
The negative of a positive integer is an integer. (Contributed by NM,
12-Jan-2002.)
|
⊢ (𝑁 ∈ ℕ → -𝑁 ∈ ℤ) |
|
Theorem | zre 8249 |
An integer is a real. (Contributed by NM, 8-Jan-2002.)
|
⊢ (𝑁 ∈ ℤ → 𝑁 ∈ ℝ) |
|
Theorem | zcn 8250 |
An integer is a complex number. (Contributed by NM, 9-May-2004.)
|
⊢ (𝑁 ∈ ℤ → 𝑁 ∈ ℂ) |
|
Theorem | zrei 8251 |
An integer is a real number. (Contributed by NM, 14-Jul-2005.)
|
⊢ 𝐴 ∈ ℤ
⇒ ⊢ 𝐴 ∈ ℝ |
|
Theorem | zssre 8252 |
The integers are a subset of the reals. (Contributed by NM,
2-Aug-2004.)
|
⊢ ℤ ⊆ ℝ |
|
Theorem | zsscn 8253 |
The integers are a subset of the complex numbers. (Contributed by NM,
2-Aug-2004.)
|
⊢ ℤ ⊆ ℂ |
|
Theorem | zex 8254 |
The set of integers exists. (Contributed by NM, 30-Jul-2004.) (Revised
by Mario Carneiro, 17-Nov-2014.)
|
⊢ ℤ ∈ V |
|
Theorem | elnnz 8255 |
Positive integer property expressed in terms of integers. (Contributed by
NM, 8-Jan-2002.)
|
⊢ (𝑁 ∈ ℕ ↔ (𝑁 ∈ ℤ ∧ 0 < 𝑁)) |
|
Theorem | 0z 8256 |
Zero is an integer. (Contributed by NM, 12-Jan-2002.)
|
⊢ 0 ∈ ℤ |
|
Theorem | 0zd 8257 |
Zero is an integer, deductive form (common case). (Contributed by David
A. Wheeler, 8-Dec-2018.)
|
⊢ (𝜑 → 0 ∈ ℤ) |
|
Theorem | elnn0z 8258 |
Nonnegative integer property expressed in terms of integers. (Contributed
by NM, 9-May-2004.)
|
⊢ (𝑁 ∈ ℕ0 ↔ (𝑁 ∈ ℤ ∧ 0 ≤
𝑁)) |
|
Theorem | elznn0nn 8259 |
Integer property expressed in terms nonnegative integers and positive
integers. (Contributed by NM, 10-May-2004.)
|
⊢ (𝑁 ∈ ℤ ↔ (𝑁 ∈ ℕ0 ∨ (𝑁 ∈ ℝ ∧ -𝑁 ∈
ℕ))) |
|
Theorem | elznn0 8260 |
Integer property expressed in terms of nonnegative integers. (Contributed
by NM, 9-May-2004.)
|
⊢ (𝑁 ∈ ℤ ↔ (𝑁 ∈ ℝ ∧ (𝑁 ∈ ℕ0 ∨ -𝑁 ∈
ℕ0))) |
|
Theorem | elznn 8261 |
Integer property expressed in terms of positive integers and nonnegative
integers. (Contributed by NM, 12-Jul-2005.)
|
⊢ (𝑁 ∈ ℤ ↔ (𝑁 ∈ ℝ ∧ (𝑁 ∈ ℕ ∨ -𝑁 ∈
ℕ0))) |
|
Theorem | nnssz 8262 |
Positive integers are a subset of integers. (Contributed by NM,
9-Jan-2002.)
|
⊢ ℕ ⊆ ℤ |
|
Theorem | nn0ssz 8263 |
Nonnegative integers are a subset of the integers. (Contributed by NM,
9-May-2004.)
|
⊢ ℕ0 ⊆
ℤ |
|
Theorem | nnz 8264 |
A positive integer is an integer. (Contributed by NM, 9-May-2004.)
|
⊢ (𝑁 ∈ ℕ → 𝑁 ∈ ℤ) |
|
Theorem | nn0z 8265 |
A nonnegative integer is an integer. (Contributed by NM, 9-May-2004.)
|
⊢ (𝑁 ∈ ℕ0 → 𝑁 ∈
ℤ) |
|
Theorem | nnzi 8266 |
A positive integer is an integer. (Contributed by Mario Carneiro,
18-Feb-2014.)
|
⊢ 𝑁 ∈ ℕ
⇒ ⊢ 𝑁 ∈ ℤ |
|
Theorem | nn0zi 8267 |
A nonnegative integer is an integer. (Contributed by Mario Carneiro,
18-Feb-2014.)
|
⊢ 𝑁 ∈
ℕ0 ⇒ ⊢ 𝑁 ∈ ℤ |
|
Theorem | elnnz1 8268 |
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 8269 |
Positive integers expressed as a subset of integers. (Contributed by NM,
3-Oct-2004.)
|
⊢ ℕ = {𝑥 ∈ ℤ ∣ 1 ≤ 𝑥} |
|
Theorem | nn0zrab 8270 |
Nonnegative integers expressed as a subset of integers. (Contributed by
NM, 3-Oct-2004.)
|
⊢ ℕ0 = {𝑥 ∈ ℤ ∣ 0 ≤ 𝑥} |
|
Theorem | 1z 8271 |
One is an integer. (Contributed by NM, 10-May-2004.)
|
⊢ 1 ∈ ℤ |
|
Theorem | 1zzd 8272 |
1 is an integer, deductive form (common case). (Contributed by David A.
Wheeler, 6-Dec-2018.)
|
⊢ (𝜑 → 1 ∈ ℤ) |
|
Theorem | 2z 8273 |
Two is an integer. (Contributed by NM, 10-May-2004.)
|
⊢ 2 ∈ ℤ |
|
Theorem | 3z 8274 |
3 is an integer. (Contributed by David A. Wheeler, 8-Dec-2018.)
|
⊢ 3 ∈ ℤ |
|
Theorem | 4z 8275 |
4 is an integer. (Contributed by BJ, 26-Mar-2020.)
|
⊢ 4 ∈ ℤ |
|
Theorem | znegcl 8276 |
Closure law for negative integers. (Contributed by NM, 9-May-2004.)
|
⊢ (𝑁 ∈ ℤ → -𝑁 ∈ ℤ) |
|
Theorem | neg1z 8277 |
-1 is an integer (common case). (Contributed by David A. Wheeler,
5-Dec-2018.)
|
⊢ -1 ∈ ℤ |
|
Theorem | znegclb 8278 |
A number is an integer iff its negative is. (Contributed by Stefan
O'Rear, 13-Sep-2014.)
|
⊢ (𝐴 ∈ ℂ → (𝐴 ∈ ℤ ↔ -𝐴 ∈ ℤ)) |
|
Theorem | nn0negz 8279 |
The negative of a nonnegative integer is an integer. (Contributed by NM,
9-May-2004.)
|
⊢ (𝑁 ∈ ℕ0 → -𝑁 ∈
ℤ) |
|
Theorem | nn0negzi 8280 |
The negative of a nonnegative integer is an integer. (Contributed by
Mario Carneiro, 18-Feb-2014.)
|
⊢ 𝑁 ∈
ℕ0 ⇒ ⊢ -𝑁 ∈ ℤ |
|
Theorem | peano2z 8281 |
Second Peano postulate generalized to integers. (Contributed by NM,
13-Feb-2005.)
|
⊢ (𝑁 ∈ ℤ → (𝑁 + 1) ∈ ℤ) |
|
Theorem | zaddcllempos 8282 |
Lemma for zaddcl 8285. Special case in which 𝑁 is a
positive integer.
(Contributed by Jim Kingdon, 14-Mar-2020.)
|
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (𝑀 + 𝑁) ∈ ℤ) |
|
Theorem | peano2zm 8283 |
"Reverse" second Peano postulate for integers. (Contributed by NM,
12-Sep-2005.)
|
⊢ (𝑁 ∈ ℤ → (𝑁 − 1) ∈
ℤ) |
|
Theorem | zaddcllemneg 8284 |
Lemma for zaddcl 8285. Special case in which -𝑁 is a
positive
integer. (Contributed by Jim Kingdon, 14-Mar-2020.)
|
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ) → (𝑀 + 𝑁) ∈ ℤ) |
|
Theorem | zaddcl 8285 |
Closure of addition of integers. (Contributed by NM, 9-May-2004.) (Proof
shortened by Mario Carneiro, 16-May-2014.)
|
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 + 𝑁) ∈ ℤ) |
|
Theorem | zsubcl 8286 |
Closure of subtraction of integers. (Contributed by NM, 11-May-2004.)
|
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 − 𝑁) ∈ ℤ) |
|
Theorem | ztri3or0 8287 |
Integer trichotomy (with zero). (Contributed by Jim Kingdon,
14-Mar-2020.)
|
⊢ (𝑁 ∈ ℤ → (𝑁 < 0 ∨ 𝑁 = 0 ∨ 0 < 𝑁)) |
|
Theorem | ztri3or 8288 |
Integer trichotomy. (Contributed by Jim Kingdon, 14-Mar-2020.)
|
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 < 𝑁 ∨ 𝑀 = 𝑁 ∨ 𝑁 < 𝑀)) |
|
Theorem | zletric 8289 |
Trichotomy law. (Contributed by Jim Kingdon, 27-Mar-2020.)
|
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (𝐴 ≤ 𝐵 ∨ 𝐵 ≤ 𝐴)) |
|
Theorem | zlelttric 8290 |
Trichotomy law. (Contributed by Jim Kingdon, 17-Apr-2020.)
|
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (𝐴 ≤ 𝐵 ∨ 𝐵 < 𝐴)) |
|
Theorem | zltnle 8291 |
'Less than' expressed in terms of 'less than or equal to'. (Contributed
by Jim Kingdon, 14-Mar-2020.)
|
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (𝐴 < 𝐵 ↔ ¬ 𝐵 ≤ 𝐴)) |
|
Theorem | zleloe 8292 |
Integer 'Less than or equal to' expressed in terms of 'less than' or
'equals'. (Contributed by Jim Kingdon, 8-Apr-2020.)
|
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (𝐴 ≤ 𝐵 ↔ (𝐴 < 𝐵 ∨ 𝐴 = 𝐵))) |
|
Theorem | znnnlt1 8293 |
An integer is not a positive integer iff it is less than one.
(Contributed by NM, 13-Jul-2005.)
|
⊢ (𝑁 ∈ ℤ → (¬ 𝑁 ∈ ℕ ↔ 𝑁 < 1)) |
|
Theorem | zletr 8294 |
Transitive law of ordering for integers. (Contributed by Alexander van
der Vekens, 3-Apr-2018.)
|
⊢ ((𝐽 ∈ ℤ ∧ 𝐾 ∈ ℤ ∧ 𝐿 ∈ ℤ) → ((𝐽 ≤ 𝐾 ∧ 𝐾 ≤ 𝐿) → 𝐽 ≤ 𝐿)) |
|
Theorem | zrevaddcl 8295 |
Reverse closure law for addition of integers. (Contributed by NM,
11-May-2004.)
|
⊢ (𝑁 ∈ ℤ → ((𝑀 ∈ ℂ ∧ (𝑀 + 𝑁) ∈ ℤ) ↔ 𝑀 ∈ ℤ)) |
|
Theorem | znnsub 8296 |
The positive difference of unequal integers is a positive integer.
(Generalization of nnsub 7952.) (Contributed by NM, 11-May-2004.)
|
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 < 𝑁 ↔ (𝑁 − 𝑀) ∈ ℕ)) |
|
Theorem | zmulcl 8297 |
Closure of multiplication of integers. (Contributed by NM,
30-Jul-2004.)
|
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 · 𝑁) ∈ ℤ) |
|
Theorem | zltp1le 8298 |
Integer ordering relation. (Contributed by NM, 10-May-2004.) (Proof
shortened by Mario Carneiro, 16-May-2014.)
|
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 < 𝑁 ↔ (𝑀 + 1) ≤ 𝑁)) |
|
Theorem | zleltp1 8299 |
Integer ordering relation. (Contributed by NM, 10-May-2004.)
|
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 ≤ 𝑁 ↔ 𝑀 < (𝑁 + 1))) |
|
Theorem | zlem1lt 8300 |
Integer ordering relation. (Contributed by NM, 13-Nov-2004.)
|
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 ≤ 𝑁 ↔ (𝑀 − 1) < 𝑁)) |