Theorem List for Intuitionistic Logic Explorer - 9201-9300 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | nn0ssxnn0 9201 |
The standard nonnegative integers are a subset of the extended nonnegative
integers. (Contributed by AV, 10-Dec-2020.)
|
⊢ ℕ0 ⊆
ℕ0* |
|
Theorem | nn0xnn0 9202 |
A standard nonnegative integer is an extended nonnegative integer.
(Contributed by AV, 10-Dec-2020.)
|
⊢ (𝐴 ∈ ℕ0 → 𝐴 ∈
ℕ0*) |
|
Theorem | xnn0xr 9203 |
An extended nonnegative integer is an extended real. (Contributed by AV,
10-Dec-2020.)
|
⊢ (𝐴 ∈ ℕ0*
→ 𝐴 ∈
ℝ*) |
|
Theorem | 0xnn0 9204 |
Zero is an extended nonnegative integer. (Contributed by AV,
10-Dec-2020.)
|
⊢ 0 ∈
ℕ0* |
|
Theorem | pnf0xnn0 9205 |
Positive infinity is an extended nonnegative integer. (Contributed by AV,
10-Dec-2020.)
|
⊢ +∞ ∈
ℕ0* |
|
Theorem | nn0nepnf 9206 |
No standard nonnegative integer equals positive infinity. (Contributed by
AV, 10-Dec-2020.)
|
⊢ (𝐴 ∈ ℕ0 → 𝐴 ≠
+∞) |
|
Theorem | nn0xnn0d 9207 |
A standard nonnegative integer is an extended nonnegative integer,
deduction form. (Contributed by AV, 10-Dec-2020.)
|
⊢ (𝜑 → 𝐴 ∈
ℕ0) ⇒ ⊢ (𝜑 → 𝐴 ∈
ℕ0*) |
|
Theorem | nn0nepnfd 9208 |
No standard nonnegative integer equals positive infinity, deduction
form. (Contributed by AV, 10-Dec-2020.)
|
⊢ (𝜑 → 𝐴 ∈
ℕ0) ⇒ ⊢ (𝜑 → 𝐴 ≠ +∞) |
|
Theorem | xnn0nemnf 9209 |
No extended nonnegative integer equals negative infinity. (Contributed by
AV, 10-Dec-2020.)
|
⊢ (𝐴 ∈ ℕ0*
→ 𝐴 ≠
-∞) |
|
Theorem | xnn0xrnemnf 9210 |
The extended nonnegative integers are extended reals without negative
infinity. (Contributed by AV, 10-Dec-2020.)
|
⊢ (𝐴 ∈ ℕ0*
→ (𝐴 ∈
ℝ* ∧ 𝐴 ≠ -∞)) |
|
Theorem | xnn0nnn0pnf 9211 |
An extended nonnegative integer which is not a standard nonnegative
integer is positive infinity. (Contributed by AV, 10-Dec-2020.)
|
⊢ ((𝑁 ∈ ℕ0*
∧ ¬ 𝑁 ∈
ℕ0) → 𝑁 = +∞) |
|
4.4.9 Integers (as a subset of complex
numbers)
|
|
Syntax | cz 9212 |
Extend class notation to include the class of integers.
|
class ℤ |
|
Definition | df-z 9213 |
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 9214 |
Membership in the set of integers. (Contributed by NM, 8-Jan-2002.)
|
⊢ (𝑁 ∈ ℤ ↔ (𝑁 ∈ ℝ ∧ (𝑁 = 0 ∨ 𝑁 ∈ ℕ ∨ -𝑁 ∈ ℕ))) |
|
Theorem | nnnegz 9215 |
The negative of a positive integer is an integer. (Contributed by NM,
12-Jan-2002.)
|
⊢ (𝑁 ∈ ℕ → -𝑁 ∈ ℤ) |
|
Theorem | zre 9216 |
An integer is a real. (Contributed by NM, 8-Jan-2002.)
|
⊢ (𝑁 ∈ ℤ → 𝑁 ∈ ℝ) |
|
Theorem | zcn 9217 |
An integer is a complex number. (Contributed by NM, 9-May-2004.)
|
⊢ (𝑁 ∈ ℤ → 𝑁 ∈ ℂ) |
|
Theorem | zrei 9218 |
An integer is a real number. (Contributed by NM, 14-Jul-2005.)
|
⊢ 𝐴 ∈ ℤ
⇒ ⊢ 𝐴 ∈ ℝ |
|
Theorem | zssre 9219 |
The integers are a subset of the reals. (Contributed by NM,
2-Aug-2004.)
|
⊢ ℤ ⊆ ℝ |
|
Theorem | zsscn 9220 |
The integers are a subset of the complex numbers. (Contributed by NM,
2-Aug-2004.)
|
⊢ ℤ ⊆ ℂ |
|
Theorem | zex 9221 |
The set of integers exists. (Contributed by NM, 30-Jul-2004.) (Revised
by Mario Carneiro, 17-Nov-2014.)
|
⊢ ℤ ∈ V |
|
Theorem | elnnz 9222 |
Positive integer property expressed in terms of integers. (Contributed by
NM, 8-Jan-2002.)
|
⊢ (𝑁 ∈ ℕ ↔ (𝑁 ∈ ℤ ∧ 0 < 𝑁)) |
|
Theorem | 0z 9223 |
Zero is an integer. (Contributed by NM, 12-Jan-2002.)
|
⊢ 0 ∈ ℤ |
|
Theorem | 0zd 9224 |
Zero is an integer, deductive form (common case). (Contributed by David
A. Wheeler, 8-Dec-2018.)
|
⊢ (𝜑 → 0 ∈ ℤ) |
|
Theorem | elnn0z 9225 |
Nonnegative integer property expressed in terms of integers. (Contributed
by NM, 9-May-2004.)
|
⊢ (𝑁 ∈ ℕ0 ↔ (𝑁 ∈ ℤ ∧ 0 ≤
𝑁)) |
|
Theorem | elznn0nn 9226 |
Integer property expressed in terms nonnegative integers and positive
integers. (Contributed by NM, 10-May-2004.)
|
⊢ (𝑁 ∈ ℤ ↔ (𝑁 ∈ ℕ0 ∨ (𝑁 ∈ ℝ ∧ -𝑁 ∈
ℕ))) |
|
Theorem | elznn0 9227 |
Integer property expressed in terms of nonnegative integers. (Contributed
by NM, 9-May-2004.)
|
⊢ (𝑁 ∈ ℤ ↔ (𝑁 ∈ ℝ ∧ (𝑁 ∈ ℕ0 ∨ -𝑁 ∈
ℕ0))) |
|
Theorem | elznn 9228 |
Integer property expressed in terms of positive integers and nonnegative
integers. (Contributed by NM, 12-Jul-2005.)
|
⊢ (𝑁 ∈ ℤ ↔ (𝑁 ∈ ℝ ∧ (𝑁 ∈ ℕ ∨ -𝑁 ∈
ℕ0))) |
|
Theorem | nnssz 9229 |
Positive integers are a subset of integers. (Contributed by NM,
9-Jan-2002.)
|
⊢ ℕ ⊆ ℤ |
|
Theorem | nn0ssz 9230 |
Nonnegative integers are a subset of the integers. (Contributed by NM,
9-May-2004.)
|
⊢ ℕ0 ⊆
ℤ |
|
Theorem | nnz 9231 |
A positive integer is an integer. (Contributed by NM, 9-May-2004.)
|
⊢ (𝑁 ∈ ℕ → 𝑁 ∈ ℤ) |
|
Theorem | nn0z 9232 |
A nonnegative integer is an integer. (Contributed by NM, 9-May-2004.)
|
⊢ (𝑁 ∈ ℕ0 → 𝑁 ∈
ℤ) |
|
Theorem | nnzi 9233 |
A positive integer is an integer. (Contributed by Mario Carneiro,
18-Feb-2014.)
|
⊢ 𝑁 ∈ ℕ
⇒ ⊢ 𝑁 ∈ ℤ |
|
Theorem | nn0zi 9234 |
A nonnegative integer is an integer. (Contributed by Mario Carneiro,
18-Feb-2014.)
|
⊢ 𝑁 ∈
ℕ0 ⇒ ⊢ 𝑁 ∈ ℤ |
|
Theorem | elnnz1 9235 |
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 9236 |
Positive integers expressed as a subset of integers. (Contributed by NM,
3-Oct-2004.)
|
⊢ ℕ = {𝑥 ∈ ℤ ∣ 1 ≤ 𝑥} |
|
Theorem | nn0zrab 9237 |
Nonnegative integers expressed as a subset of integers. (Contributed by
NM, 3-Oct-2004.)
|
⊢ ℕ0 = {𝑥 ∈ ℤ ∣ 0 ≤ 𝑥} |
|
Theorem | 1z 9238 |
One is an integer. (Contributed by NM, 10-May-2004.)
|
⊢ 1 ∈ ℤ |
|
Theorem | 1zzd 9239 |
1 is an integer, deductive form (common case). (Contributed by David A.
Wheeler, 6-Dec-2018.)
|
⊢ (𝜑 → 1 ∈ ℤ) |
|
Theorem | 2z 9240 |
Two is an integer. (Contributed by NM, 10-May-2004.)
|
⊢ 2 ∈ ℤ |
|
Theorem | 3z 9241 |
3 is an integer. (Contributed by David A. Wheeler, 8-Dec-2018.)
|
⊢ 3 ∈ ℤ |
|
Theorem | 4z 9242 |
4 is an integer. (Contributed by BJ, 26-Mar-2020.)
|
⊢ 4 ∈ ℤ |
|
Theorem | znegcl 9243 |
Closure law for negative integers. (Contributed by NM, 9-May-2004.)
|
⊢ (𝑁 ∈ ℤ → -𝑁 ∈ ℤ) |
|
Theorem | neg1z 9244 |
-1 is an integer (common case). (Contributed by David A. Wheeler,
5-Dec-2018.)
|
⊢ -1 ∈ ℤ |
|
Theorem | znegclb 9245 |
A number is an integer iff its negative is. (Contributed by Stefan
O'Rear, 13-Sep-2014.)
|
⊢ (𝐴 ∈ ℂ → (𝐴 ∈ ℤ ↔ -𝐴 ∈ ℤ)) |
|
Theorem | nn0negz 9246 |
The negative of a nonnegative integer is an integer. (Contributed by NM,
9-May-2004.)
|
⊢ (𝑁 ∈ ℕ0 → -𝑁 ∈
ℤ) |
|
Theorem | nn0negzi 9247 |
The negative of a nonnegative integer is an integer. (Contributed by
Mario Carneiro, 18-Feb-2014.)
|
⊢ 𝑁 ∈
ℕ0 ⇒ ⊢ -𝑁 ∈ ℤ |
|
Theorem | peano2z 9248 |
Second Peano postulate generalized to integers. (Contributed by NM,
13-Feb-2005.)
|
⊢ (𝑁 ∈ ℤ → (𝑁 + 1) ∈ ℤ) |
|
Theorem | zaddcllempos 9249 |
Lemma for zaddcl 9252. Special case in which 𝑁 is a
positive integer.
(Contributed by Jim Kingdon, 14-Mar-2020.)
|
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (𝑀 + 𝑁) ∈ ℤ) |
|
Theorem | peano2zm 9250 |
"Reverse" second Peano postulate for integers. (Contributed by NM,
12-Sep-2005.)
|
⊢ (𝑁 ∈ ℤ → (𝑁 − 1) ∈
ℤ) |
|
Theorem | zaddcllemneg 9251 |
Lemma for zaddcl 9252. Special case in which -𝑁 is a
positive
integer. (Contributed by Jim Kingdon, 14-Mar-2020.)
|
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ) → (𝑀 + 𝑁) ∈ ℤ) |
|
Theorem | zaddcl 9252 |
Closure of addition of integers. (Contributed by NM, 9-May-2004.) (Proof
shortened by Mario Carneiro, 16-May-2014.)
|
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 + 𝑁) ∈ ℤ) |
|
Theorem | zsubcl 9253 |
Closure of subtraction of integers. (Contributed by NM, 11-May-2004.)
|
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 − 𝑁) ∈ ℤ) |
|
Theorem | ztri3or0 9254 |
Integer trichotomy (with zero). (Contributed by Jim Kingdon,
14-Mar-2020.)
|
⊢ (𝑁 ∈ ℤ → (𝑁 < 0 ∨ 𝑁 = 0 ∨ 0 < 𝑁)) |
|
Theorem | ztri3or 9255 |
Integer trichotomy. (Contributed by Jim Kingdon, 14-Mar-2020.)
|
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 < 𝑁 ∨ 𝑀 = 𝑁 ∨ 𝑁 < 𝑀)) |
|
Theorem | zletric 9256 |
Trichotomy law. (Contributed by Jim Kingdon, 27-Mar-2020.)
|
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (𝐴 ≤ 𝐵 ∨ 𝐵 ≤ 𝐴)) |
|
Theorem | zlelttric 9257 |
Trichotomy law. (Contributed by Jim Kingdon, 17-Apr-2020.)
|
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (𝐴 ≤ 𝐵 ∨ 𝐵 < 𝐴)) |
|
Theorem | zltnle 9258 |
'Less than' expressed in terms of 'less than or equal to'. (Contributed
by Jim Kingdon, 14-Mar-2020.)
|
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (𝐴 < 𝐵 ↔ ¬ 𝐵 ≤ 𝐴)) |
|
Theorem | zleloe 9259 |
Integer 'Less than or equal to' expressed in terms of 'less than' or
'equals'. (Contributed by Jim Kingdon, 8-Apr-2020.)
|
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (𝐴 ≤ 𝐵 ↔ (𝐴 < 𝐵 ∨ 𝐴 = 𝐵))) |
|
Theorem | znnnlt1 9260 |
An integer is not a positive integer iff it is less than one.
(Contributed by NM, 13-Jul-2005.)
|
⊢ (𝑁 ∈ ℤ → (¬ 𝑁 ∈ ℕ ↔ 𝑁 < 1)) |
|
Theorem | zletr 9261 |
Transitive law of ordering for integers. (Contributed by Alexander van
der Vekens, 3-Apr-2018.)
|
⊢ ((𝐽 ∈ ℤ ∧ 𝐾 ∈ ℤ ∧ 𝐿 ∈ ℤ) → ((𝐽 ≤ 𝐾 ∧ 𝐾 ≤ 𝐿) → 𝐽 ≤ 𝐿)) |
|
Theorem | zrevaddcl 9262 |
Reverse closure law for addition of integers. (Contributed by NM,
11-May-2004.)
|
⊢ (𝑁 ∈ ℤ → ((𝑀 ∈ ℂ ∧ (𝑀 + 𝑁) ∈ ℤ) ↔ 𝑀 ∈ ℤ)) |
|
Theorem | znnsub 9263 |
The positive difference of unequal integers is a positive integer.
(Generalization of nnsub 8917.) (Contributed by NM, 11-May-2004.)
|
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 < 𝑁 ↔ (𝑁 − 𝑀) ∈ ℕ)) |
|
Theorem | nzadd 9264 |
The sum of a real number not being an integer and an integer is not an
integer. Note that "not being an integer" in this case means
"the
negation of is an integer" rather than "is apart from any
integer" (given
excluded middle, those two would be equivalent). (Contributed by AV,
19-Jul-2021.)
|
⊢ ((𝐴 ∈ (ℝ ∖ ℤ) ∧
𝐵 ∈ ℤ) →
(𝐴 + 𝐵) ∈ (ℝ ∖
ℤ)) |
|
Theorem | zmulcl 9265 |
Closure of multiplication of integers. (Contributed by NM,
30-Jul-2004.)
|
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 · 𝑁) ∈ ℤ) |
|
Theorem | zltp1le 9266 |
Integer ordering relation. (Contributed by NM, 10-May-2004.) (Proof
shortened by Mario Carneiro, 16-May-2014.)
|
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 < 𝑁 ↔ (𝑀 + 1) ≤ 𝑁)) |
|
Theorem | zleltp1 9267 |
Integer ordering relation. (Contributed by NM, 10-May-2004.)
|
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 ≤ 𝑁 ↔ 𝑀 < (𝑁 + 1))) |
|
Theorem | zlem1lt 9268 |
Integer ordering relation. (Contributed by NM, 13-Nov-2004.)
|
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 ≤ 𝑁 ↔ (𝑀 − 1) < 𝑁)) |
|
Theorem | zltlem1 9269 |
Integer ordering relation. (Contributed by NM, 13-Nov-2004.)
|
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 < 𝑁 ↔ 𝑀 ≤ (𝑁 − 1))) |
|
Theorem | zgt0ge1 9270 |
An integer greater than 0 is greater than or equal to
1.
(Contributed by AV, 14-Oct-2018.)
|
⊢ (𝑍 ∈ ℤ → (0 < 𝑍 ↔ 1 ≤ 𝑍)) |
|
Theorem | nnleltp1 9271 |
Positive integer ordering relation. (Contributed by NM, 13-Aug-2001.)
(Proof shortened by Mario Carneiro, 16-May-2014.)
|
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) → (𝐴 ≤ 𝐵 ↔ 𝐴 < (𝐵 + 1))) |
|
Theorem | nnltp1le 9272 |
Positive integer ordering relation. (Contributed by NM, 19-Aug-2001.)
|
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) → (𝐴 < 𝐵 ↔ (𝐴 + 1) ≤ 𝐵)) |
|
Theorem | nnaddm1cl 9273 |
Closure of addition of positive integers minus one. (Contributed by NM,
6-Aug-2003.) (Proof shortened by Mario Carneiro, 16-May-2014.)
|
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) → ((𝐴 + 𝐵) − 1) ∈
ℕ) |
|
Theorem | nn0ltp1le 9274 |
Nonnegative integer ordering relation. (Contributed by Raph Levien,
10-Dec-2002.) (Proof shortened by Mario Carneiro, 16-May-2014.)
|
⊢ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)
→ (𝑀 < 𝑁 ↔ (𝑀 + 1) ≤ 𝑁)) |
|
Theorem | nn0leltp1 9275 |
Nonnegative integer ordering relation. (Contributed by Raph Levien,
10-Apr-2004.)
|
⊢ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)
→ (𝑀 ≤ 𝑁 ↔ 𝑀 < (𝑁 + 1))) |
|
Theorem | nn0ltlem1 9276 |
Nonnegative integer ordering relation. (Contributed by NM, 10-May-2004.)
(Proof shortened by Mario Carneiro, 16-May-2014.)
|
⊢ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)
→ (𝑀 < 𝑁 ↔ 𝑀 ≤ (𝑁 − 1))) |
|
Theorem | znn0sub 9277 |
The nonnegative difference of integers is a nonnegative integer.
(Generalization of nn0sub 9278.) (Contributed by NM, 14-Jul-2005.)
|
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 ≤ 𝑁 ↔ (𝑁 − 𝑀) ∈
ℕ0)) |
|
Theorem | nn0sub 9278 |
Subtraction of nonnegative integers. (Contributed by NM, 9-May-2004.)
|
⊢ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)
→ (𝑀 ≤ 𝑁 ↔ (𝑁 − 𝑀) ∈
ℕ0)) |
|
Theorem | ltsubnn0 9279 |
Subtracting a nonnegative integer from a nonnegative integer which is
greater than the first one results in a nonnegative integer. (Contributed
by Alexander van der Vekens, 6-Apr-2018.)
|
⊢ ((𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ0)
→ (𝐵 < 𝐴 → (𝐴 − 𝐵) ∈
ℕ0)) |
|
Theorem | nn0negleid 9280 |
A nonnegative integer is greater than or equal to its negative.
(Contributed by AV, 13-Aug-2021.)
|
⊢ (𝐴 ∈ ℕ0 → -𝐴 ≤ 𝐴) |
|
Theorem | difgtsumgt 9281 |
If the difference of a real number and a nonnegative integer is greater
than another real number, the sum of the real number and the nonnegative
integer is also greater than the other real number. (Contributed by AV,
13-Aug-2021.)
|
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℕ0 ∧ 𝐶 ∈ ℝ) → (𝐶 < (𝐴 − 𝐵) → 𝐶 < (𝐴 + 𝐵))) |
|
Theorem | nn0n0n1ge2 9282 |
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 9283* |
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.)
|
⊢ (𝑁 ∈ ℤ ↔ ∃𝑥 ∈ ℕ ∃𝑦 ∈ ℕ 𝑁 = (𝑥 − 𝑦)) |
|
Theorem | dfz2 9284 |
Alternate definition of the integers, based on elz2 9283.
(Contributed by
Mario Carneiro, 16-May-2014.)
|
⊢ ℤ = ( − “ (ℕ ×
ℕ)) |
|
Theorem | nn0sub2 9285 |
Subtraction of nonnegative integers. (Contributed by NM, 4-Sep-2005.)
|
⊢ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0
∧ 𝑀 ≤ 𝑁) → (𝑁 − 𝑀) ∈
ℕ0) |
|
Theorem | zapne 9286 |
Apartness is equivalent to not equal for integers. (Contributed by Jim
Kingdon, 14-Mar-2020.)
|
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 # 𝑁 ↔ 𝑀 ≠ 𝑁)) |
|
Theorem | zdceq 9287 |
Equality of integers is decidable. (Contributed by Jim Kingdon,
14-Mar-2020.)
|
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) →
DECID 𝐴 =
𝐵) |
|
Theorem | zdcle 9288 |
Integer ≤ is decidable. (Contributed by Jim
Kingdon, 7-Apr-2020.)
|
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) →
DECID 𝐴
≤ 𝐵) |
|
Theorem | zdclt 9289 |
Integer < is decidable. (Contributed by Jim
Kingdon, 1-Jun-2020.)
|
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) →
DECID 𝐴
< 𝐵) |
|
Theorem | zltlen 9290 |
Integer 'Less than' expressed in terms of 'less than or equal to'. Also
see ltleap 8551 which is a similar result for real numbers.
(Contributed by
Jim Kingdon, 14-Mar-2020.)
|
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (𝐴 < 𝐵 ↔ (𝐴 ≤ 𝐵 ∧ 𝐵 ≠ 𝐴))) |
|
Theorem | nn0n0n1ge2b 9291 |
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 9292 |
A nonnegative integer less than 1 is 0. (Contributed by Paul
Chapman, 22-Jun-2011.)
|
⊢ (𝑁 ∈ ℕ0 → (𝑁 < 1 ↔ 𝑁 = 0)) |
|
Theorem | nn0lt2 9293 |
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 | nn0le2is012 9294 |
A nonnegative integer which is less than or equal to 2 is either 0 or 1 or
2. (Contributed by AV, 16-Mar-2019.)
|
⊢ ((𝑁 ∈ ℕ0 ∧ 𝑁 ≤ 2) → (𝑁 = 0 ∨ 𝑁 = 1 ∨ 𝑁 = 2)) |
|
Theorem | nn0lem1lt 9295 |
Nonnegative integer ordering relation. (Contributed by NM,
21-Jun-2005.)
|
⊢ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)
→ (𝑀 ≤ 𝑁 ↔ (𝑀 − 1) < 𝑁)) |
|
Theorem | nnlem1lt 9296 |
Positive integer ordering relation. (Contributed by NM, 21-Jun-2005.)
|
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (𝑀 ≤ 𝑁 ↔ (𝑀 − 1) < 𝑁)) |
|
Theorem | nnltlem1 9297 |
Positive integer ordering relation. (Contributed by NM, 21-Jun-2005.)
|
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (𝑀 < 𝑁 ↔ 𝑀 ≤ (𝑁 − 1))) |
|
Theorem | nnm1ge0 9298 |
A positive integer decreased by 1 is greater than or equal to 0.
(Contributed by AV, 30-Oct-2018.)
|
⊢ (𝑁 ∈ ℕ → 0 ≤ (𝑁 − 1)) |
|
Theorem | nn0ge0div 9299 |
Division of a nonnegative integer by a positive number is not negative.
(Contributed by Alexander van der Vekens, 14-Apr-2018.)
|
⊢ ((𝐾 ∈ ℕ0 ∧ 𝐿 ∈ ℕ) → 0 ≤
(𝐾 / 𝐿)) |
|
Theorem | zdiv 9300* |
Two ways to express "𝑀 divides 𝑁. (Contributed by NM,
3-Oct-2008.)
|
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℤ) → (∃𝑘 ∈ ℤ (𝑀 · 𝑘) = 𝑁 ↔ (𝑁 / 𝑀) ∈ ℤ)) |