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