Theorem List for Intuitionistic Logic Explorer - 8501-8600 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | xnn0nnn0pnf 8501 |
An extended nonnegative integer which is not a standard nonnegative
integer is positive infinity. (Contributed by AV, 10-Dec-2020.)
|
⊢ ((𝑁 ∈ ℕ0*
∧ ¬ 𝑁 ∈
ℕ0) → 𝑁 = +∞) |
|
3.4.9 Integers (as a subset of complex
numbers)
|
|
Syntax | cz 8502 |
Extend class notation to include the class of integers.
|
class ℤ |
|
Definition | df-z 8503 |
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 8504 |
Membership in the set of integers. (Contributed by NM, 8-Jan-2002.)
|
⊢ (𝑁 ∈ ℤ ↔ (𝑁 ∈ ℝ ∧ (𝑁 = 0 ∨ 𝑁 ∈ ℕ ∨ -𝑁 ∈ ℕ))) |
|
Theorem | nnnegz 8505 |
The negative of a positive integer is an integer. (Contributed by NM,
12-Jan-2002.)
|
⊢ (𝑁 ∈ ℕ → -𝑁 ∈ ℤ) |
|
Theorem | zre 8506 |
An integer is a real. (Contributed by NM, 8-Jan-2002.)
|
⊢ (𝑁 ∈ ℤ → 𝑁 ∈ ℝ) |
|
Theorem | zcn 8507 |
An integer is a complex number. (Contributed by NM, 9-May-2004.)
|
⊢ (𝑁 ∈ ℤ → 𝑁 ∈ ℂ) |
|
Theorem | zrei 8508 |
An integer is a real number. (Contributed by NM, 14-Jul-2005.)
|
⊢ 𝐴 ∈ ℤ
⇒ ⊢ 𝐴 ∈ ℝ |
|
Theorem | zssre 8509 |
The integers are a subset of the reals. (Contributed by NM,
2-Aug-2004.)
|
⊢ ℤ ⊆ ℝ |
|
Theorem | zsscn 8510 |
The integers are a subset of the complex numbers. (Contributed by NM,
2-Aug-2004.)
|
⊢ ℤ ⊆ ℂ |
|
Theorem | zex 8511 |
The set of integers exists. (Contributed by NM, 30-Jul-2004.) (Revised
by Mario Carneiro, 17-Nov-2014.)
|
⊢ ℤ ∈ V |
|
Theorem | elnnz 8512 |
Positive integer property expressed in terms of integers. (Contributed by
NM, 8-Jan-2002.)
|
⊢ (𝑁 ∈ ℕ ↔ (𝑁 ∈ ℤ ∧ 0 < 𝑁)) |
|
Theorem | 0z 8513 |
Zero is an integer. (Contributed by NM, 12-Jan-2002.)
|
⊢ 0 ∈ ℤ |
|
Theorem | 0zd 8514 |
Zero is an integer, deductive form (common case). (Contributed by David
A. Wheeler, 8-Dec-2018.)
|
⊢ (𝜑 → 0 ∈ ℤ) |
|
Theorem | elnn0z 8515 |
Nonnegative integer property expressed in terms of integers. (Contributed
by NM, 9-May-2004.)
|
⊢ (𝑁 ∈ ℕ0 ↔ (𝑁 ∈ ℤ ∧ 0 ≤
𝑁)) |
|
Theorem | elznn0nn 8516 |
Integer property expressed in terms nonnegative integers and positive
integers. (Contributed by NM, 10-May-2004.)
|
⊢ (𝑁 ∈ ℤ ↔ (𝑁 ∈ ℕ0 ∨ (𝑁 ∈ ℝ ∧ -𝑁 ∈
ℕ))) |
|
Theorem | elznn0 8517 |
Integer property expressed in terms of nonnegative integers. (Contributed
by NM, 9-May-2004.)
|
⊢ (𝑁 ∈ ℤ ↔ (𝑁 ∈ ℝ ∧ (𝑁 ∈ ℕ0 ∨ -𝑁 ∈
ℕ0))) |
|
Theorem | elznn 8518 |
Integer property expressed in terms of positive integers and nonnegative
integers. (Contributed by NM, 12-Jul-2005.)
|
⊢ (𝑁 ∈ ℤ ↔ (𝑁 ∈ ℝ ∧ (𝑁 ∈ ℕ ∨ -𝑁 ∈
ℕ0))) |
|
Theorem | nnssz 8519 |
Positive integers are a subset of integers. (Contributed by NM,
9-Jan-2002.)
|
⊢ ℕ ⊆ ℤ |
|
Theorem | nn0ssz 8520 |
Nonnegative integers are a subset of the integers. (Contributed by NM,
9-May-2004.)
|
⊢ ℕ0 ⊆
ℤ |
|
Theorem | nnz 8521 |
A positive integer is an integer. (Contributed by NM, 9-May-2004.)
|
⊢ (𝑁 ∈ ℕ → 𝑁 ∈ ℤ) |
|
Theorem | nn0z 8522 |
A nonnegative integer is an integer. (Contributed by NM, 9-May-2004.)
|
⊢ (𝑁 ∈ ℕ0 → 𝑁 ∈
ℤ) |
|
Theorem | nnzi 8523 |
A positive integer is an integer. (Contributed by Mario Carneiro,
18-Feb-2014.)
|
⊢ 𝑁 ∈ ℕ
⇒ ⊢ 𝑁 ∈ ℤ |
|
Theorem | nn0zi 8524 |
A nonnegative integer is an integer. (Contributed by Mario Carneiro,
18-Feb-2014.)
|
⊢ 𝑁 ∈
ℕ0 ⇒ ⊢ 𝑁 ∈ ℤ |
|
Theorem | elnnz1 8525 |
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 8526 |
Positive integers expressed as a subset of integers. (Contributed by NM,
3-Oct-2004.)
|
⊢ ℕ = {𝑥 ∈ ℤ ∣ 1 ≤ 𝑥} |
|
Theorem | nn0zrab 8527 |
Nonnegative integers expressed as a subset of integers. (Contributed by
NM, 3-Oct-2004.)
|
⊢ ℕ0 = {𝑥 ∈ ℤ ∣ 0 ≤ 𝑥} |
|
Theorem | 1z 8528 |
One is an integer. (Contributed by NM, 10-May-2004.)
|
⊢ 1 ∈ ℤ |
|
Theorem | 1zzd 8529 |
1 is an integer, deductive form (common case). (Contributed by David A.
Wheeler, 6-Dec-2018.)
|
⊢ (𝜑 → 1 ∈ ℤ) |
|
Theorem | 2z 8530 |
Two is an integer. (Contributed by NM, 10-May-2004.)
|
⊢ 2 ∈ ℤ |
|
Theorem | 3z 8531 |
3 is an integer. (Contributed by David A. Wheeler, 8-Dec-2018.)
|
⊢ 3 ∈ ℤ |
|
Theorem | 4z 8532 |
4 is an integer. (Contributed by BJ, 26-Mar-2020.)
|
⊢ 4 ∈ ℤ |
|
Theorem | znegcl 8533 |
Closure law for negative integers. (Contributed by NM, 9-May-2004.)
|
⊢ (𝑁 ∈ ℤ → -𝑁 ∈ ℤ) |
|
Theorem | neg1z 8534 |
-1 is an integer (common case). (Contributed by David A. Wheeler,
5-Dec-2018.)
|
⊢ -1 ∈ ℤ |
|
Theorem | znegclb 8535 |
A number is an integer iff its negative is. (Contributed by Stefan
O'Rear, 13-Sep-2014.)
|
⊢ (𝐴 ∈ ℂ → (𝐴 ∈ ℤ ↔ -𝐴 ∈ ℤ)) |
|
Theorem | nn0negz 8536 |
The negative of a nonnegative integer is an integer. (Contributed by NM,
9-May-2004.)
|
⊢ (𝑁 ∈ ℕ0 → -𝑁 ∈
ℤ) |
|
Theorem | nn0negzi 8537 |
The negative of a nonnegative integer is an integer. (Contributed by
Mario Carneiro, 18-Feb-2014.)
|
⊢ 𝑁 ∈
ℕ0 ⇒ ⊢ -𝑁 ∈ ℤ |
|
Theorem | peano2z 8538 |
Second Peano postulate generalized to integers. (Contributed by NM,
13-Feb-2005.)
|
⊢ (𝑁 ∈ ℤ → (𝑁 + 1) ∈ ℤ) |
|
Theorem | zaddcllempos 8539 |
Lemma for zaddcl 8542. Special case in which 𝑁 is a
positive integer.
(Contributed by Jim Kingdon, 14-Mar-2020.)
|
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (𝑀 + 𝑁) ∈ ℤ) |
|
Theorem | peano2zm 8540 |
"Reverse" second Peano postulate for integers. (Contributed by NM,
12-Sep-2005.)
|
⊢ (𝑁 ∈ ℤ → (𝑁 − 1) ∈
ℤ) |
|
Theorem | zaddcllemneg 8541 |
Lemma for zaddcl 8542. Special case in which -𝑁 is a
positive
integer. (Contributed by Jim Kingdon, 14-Mar-2020.)
|
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ) → (𝑀 + 𝑁) ∈ ℤ) |
|
Theorem | zaddcl 8542 |
Closure of addition of integers. (Contributed by NM, 9-May-2004.) (Proof
shortened by Mario Carneiro, 16-May-2014.)
|
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 + 𝑁) ∈ ℤ) |
|
Theorem | zsubcl 8543 |
Closure of subtraction of integers. (Contributed by NM, 11-May-2004.)
|
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 − 𝑁) ∈ ℤ) |
|
Theorem | ztri3or0 8544 |
Integer trichotomy (with zero). (Contributed by Jim Kingdon,
14-Mar-2020.)
|
⊢ (𝑁 ∈ ℤ → (𝑁 < 0 ∨ 𝑁 = 0 ∨ 0 < 𝑁)) |
|
Theorem | ztri3or 8545 |
Integer trichotomy. (Contributed by Jim Kingdon, 14-Mar-2020.)
|
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 < 𝑁 ∨ 𝑀 = 𝑁 ∨ 𝑁 < 𝑀)) |
|
Theorem | zletric 8546 |
Trichotomy law. (Contributed by Jim Kingdon, 27-Mar-2020.)
|
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (𝐴 ≤ 𝐵 ∨ 𝐵 ≤ 𝐴)) |
|
Theorem | zlelttric 8547 |
Trichotomy law. (Contributed by Jim Kingdon, 17-Apr-2020.)
|
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (𝐴 ≤ 𝐵 ∨ 𝐵 < 𝐴)) |
|
Theorem | zltnle 8548 |
'Less than' expressed in terms of 'less than or equal to'. (Contributed
by Jim Kingdon, 14-Mar-2020.)
|
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (𝐴 < 𝐵 ↔ ¬ 𝐵 ≤ 𝐴)) |
|
Theorem | zleloe 8549 |
Integer 'Less than or equal to' expressed in terms of 'less than' or
'equals'. (Contributed by Jim Kingdon, 8-Apr-2020.)
|
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (𝐴 ≤ 𝐵 ↔ (𝐴 < 𝐵 ∨ 𝐴 = 𝐵))) |
|
Theorem | znnnlt1 8550 |
An integer is not a positive integer iff it is less than one.
(Contributed by NM, 13-Jul-2005.)
|
⊢ (𝑁 ∈ ℤ → (¬ 𝑁 ∈ ℕ ↔ 𝑁 < 1)) |
|
Theorem | zletr 8551 |
Transitive law of ordering for integers. (Contributed by Alexander van
der Vekens, 3-Apr-2018.)
|
⊢ ((𝐽 ∈ ℤ ∧ 𝐾 ∈ ℤ ∧ 𝐿 ∈ ℤ) → ((𝐽 ≤ 𝐾 ∧ 𝐾 ≤ 𝐿) → 𝐽 ≤ 𝐿)) |
|
Theorem | zrevaddcl 8552 |
Reverse closure law for addition of integers. (Contributed by NM,
11-May-2004.)
|
⊢ (𝑁 ∈ ℤ → ((𝑀 ∈ ℂ ∧ (𝑀 + 𝑁) ∈ ℤ) ↔ 𝑀 ∈ ℤ)) |
|
Theorem | znnsub 8553 |
The positive difference of unequal integers is a positive integer.
(Generalization of nnsub 8214.) (Contributed by NM, 11-May-2004.)
|
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 < 𝑁 ↔ (𝑁 − 𝑀) ∈ ℕ)) |
|
Theorem | nzadd 8554 |
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 8555 |
Closure of multiplication of integers. (Contributed by NM,
30-Jul-2004.)
|
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 · 𝑁) ∈ ℤ) |
|
Theorem | zltp1le 8556 |
Integer ordering relation. (Contributed by NM, 10-May-2004.) (Proof
shortened by Mario Carneiro, 16-May-2014.)
|
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 < 𝑁 ↔ (𝑀 + 1) ≤ 𝑁)) |
|
Theorem | zleltp1 8557 |
Integer ordering relation. (Contributed by NM, 10-May-2004.)
|
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 ≤ 𝑁 ↔ 𝑀 < (𝑁 + 1))) |
|
Theorem | zlem1lt 8558 |
Integer ordering relation. (Contributed by NM, 13-Nov-2004.)
|
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 ≤ 𝑁 ↔ (𝑀 − 1) < 𝑁)) |
|
Theorem | zltlem1 8559 |
Integer ordering relation. (Contributed by NM, 13-Nov-2004.)
|
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 < 𝑁 ↔ 𝑀 ≤ (𝑁 − 1))) |
|
Theorem | zgt0ge1 8560 |
An integer greater than 0 is greater than or equal to
1.
(Contributed by AV, 14-Oct-2018.)
|
⊢ (𝑍 ∈ ℤ → (0 < 𝑍 ↔ 1 ≤ 𝑍)) |
|
Theorem | nnleltp1 8561 |
Positive integer ordering relation. (Contributed by NM, 13-Aug-2001.)
(Proof shortened by Mario Carneiro, 16-May-2014.)
|
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) → (𝐴 ≤ 𝐵 ↔ 𝐴 < (𝐵 + 1))) |
|
Theorem | nnltp1le 8562 |
Positive integer ordering relation. (Contributed by NM, 19-Aug-2001.)
|
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) → (𝐴 < 𝐵 ↔ (𝐴 + 1) ≤ 𝐵)) |
|
Theorem | nnaddm1cl 8563 |
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 8564 |
Nonnegative integer ordering relation. (Contributed by Raph Levien,
10-Dec-2002.) (Proof shortened by Mario Carneiro, 16-May-2014.)
|
⊢ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)
→ (𝑀 < 𝑁 ↔ (𝑀 + 1) ≤ 𝑁)) |
|
Theorem | nn0leltp1 8565 |
Nonnegative integer ordering relation. (Contributed by Raph Levien,
10-Apr-2004.)
|
⊢ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)
→ (𝑀 ≤ 𝑁 ↔ 𝑀 < (𝑁 + 1))) |
|
Theorem | nn0ltlem1 8566 |
Nonnegative integer ordering relation. (Contributed by NM, 10-May-2004.)
(Proof shortened by Mario Carneiro, 16-May-2014.)
|
⊢ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)
→ (𝑀 < 𝑁 ↔ 𝑀 ≤ (𝑁 − 1))) |
|
Theorem | znn0sub 8567 |
The nonnegative difference of integers is a nonnegative integer.
(Generalization of nn0sub 8568.) (Contributed by NM, 14-Jul-2005.)
|
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 ≤ 𝑁 ↔ (𝑁 − 𝑀) ∈
ℕ0)) |
|
Theorem | nn0sub 8568 |
Subtraction of nonnegative integers. (Contributed by NM, 9-May-2004.)
|
⊢ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)
→ (𝑀 ≤ 𝑁 ↔ (𝑁 − 𝑀) ∈
ℕ0)) |
|
Theorem | nn0n0n1ge2 8569 |
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 8570* |
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 8571 |
Alternate definition of the integers, based on elz2 8570.
(Contributed by
Mario Carneiro, 16-May-2014.)
|
⊢ ℤ = ( − “ (ℕ ×
ℕ)) |
|
Theorem | nn0sub2 8572 |
Subtraction of nonnegative integers. (Contributed by NM, 4-Sep-2005.)
|
⊢ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0
∧ 𝑀 ≤ 𝑁) → (𝑁 − 𝑀) ∈
ℕ0) |
|
Theorem | zapne 8573 |
Apartness is equivalent to not equal for integers. (Contributed by Jim
Kingdon, 14-Mar-2020.)
|
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 # 𝑁 ↔ 𝑀 ≠ 𝑁)) |
|
Theorem | zdceq 8574 |
Equality of integers is decidable. (Contributed by Jim Kingdon,
14-Mar-2020.)
|
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) →
DECID 𝐴 =
𝐵) |
|
Theorem | zdcle 8575 |
Integer ≤ is decidable. (Contributed by Jim
Kingdon, 7-Apr-2020.)
|
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) →
DECID 𝐴
≤ 𝐵) |
|
Theorem | zdclt 8576 |
Integer < is decidable. (Contributed by Jim
Kingdon, 1-Jun-2020.)
|
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) →
DECID 𝐴
< 𝐵) |
|
Theorem | zltlen 8577 |
Integer 'Less than' expressed in terms of 'less than or equal to'. Also
see ltleap 7867 which is a similar result for real numbers.
(Contributed by
Jim Kingdon, 14-Mar-2020.)
|
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (𝐴 < 𝐵 ↔ (𝐴 ≤ 𝐵 ∧ 𝐵 ≠ 𝐴))) |
|
Theorem | nn0n0n1ge2b 8578 |
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 8579 |
A nonnegative integer less than 1 is 0. (Contributed by Paul
Chapman, 22-Jun-2011.)
|
⊢ (𝑁 ∈ ℕ0 → (𝑁 < 1 ↔ 𝑁 = 0)) |
|
Theorem | nn0lt2 8580 |
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 8581 |
Nonnegative integer ordering relation. (Contributed by NM,
21-Jun-2005.)
|
⊢ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)
→ (𝑀 ≤ 𝑁 ↔ (𝑀 − 1) < 𝑁)) |
|
Theorem | nnlem1lt 8582 |
Positive integer ordering relation. (Contributed by NM, 21-Jun-2005.)
|
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (𝑀 ≤ 𝑁 ↔ (𝑀 − 1) < 𝑁)) |
|
Theorem | nnltlem1 8583 |
Positive integer ordering relation. (Contributed by NM, 21-Jun-2005.)
|
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (𝑀 < 𝑁 ↔ 𝑀 ≤ (𝑁 − 1))) |
|
Theorem | nnm1ge0 8584 |
A positive integer decreased by 1 is greater than or equal to 0.
(Contributed by AV, 30-Oct-2018.)
|
⊢ (𝑁 ∈ ℕ → 0 ≤ (𝑁 − 1)) |
|
Theorem | nn0ge0div 8585 |
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 8586* |
Two ways to express "𝑀 divides 𝑁. (Contributed by NM,
3-Oct-2008.)
|
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℤ) → (∃𝑘 ∈ ℤ (𝑀 · 𝑘) = 𝑁 ↔ (𝑁 / 𝑀) ∈ ℤ)) |
|
Theorem | zdivadd 8587 |
Property of divisibility: if 𝐷 divides 𝐴 and 𝐵 then it
divides
𝐴 +
𝐵. (Contributed by
NM, 3-Oct-2008.)
|
⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ ((𝐴 / 𝐷) ∈ ℤ ∧ (𝐵 / 𝐷) ∈ ℤ)) → ((𝐴 + 𝐵) / 𝐷) ∈ ℤ) |
|
Theorem | zdivmul 8588 |
Property of divisibility: if 𝐷 divides 𝐴 then it divides
𝐵
· 𝐴.
(Contributed by NM, 3-Oct-2008.)
|
⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ (𝐴 / 𝐷) ∈ ℤ) → ((𝐵 · 𝐴) / 𝐷) ∈ ℤ) |
|
Theorem | zextle 8589* |
An extensionality-like property for integer ordering. (Contributed by
NM, 29-Oct-2005.)
|
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ ∀𝑘 ∈ ℤ (𝑘 ≤ 𝑀 ↔ 𝑘 ≤ 𝑁)) → 𝑀 = 𝑁) |
|
Theorem | zextlt 8590* |
An extensionality-like property for integer ordering. (Contributed by
NM, 29-Oct-2005.)
|
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ ∀𝑘 ∈ ℤ (𝑘 < 𝑀 ↔ 𝑘 < 𝑁)) → 𝑀 = 𝑁) |
|
Theorem | recnz 8591 |
The reciprocal of a number greater than 1 is not an integer. (Contributed
by NM, 3-May-2005.)
|
⊢ ((𝐴 ∈ ℝ ∧ 1 < 𝐴) → ¬ (1 / 𝐴) ∈
ℤ) |
|
Theorem | btwnnz 8592 |
A number between an integer and its successor is not an integer.
(Contributed by NM, 3-May-2005.)
|
⊢ ((𝐴 ∈ ℤ ∧ 𝐴 < 𝐵 ∧ 𝐵 < (𝐴 + 1)) → ¬ 𝐵 ∈ ℤ) |
|
Theorem | gtndiv 8593 |
A larger number does not divide a smaller positive integer. (Contributed
by NM, 3-May-2005.)
|
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℕ ∧ 𝐵 < 𝐴) → ¬ (𝐵 / 𝐴) ∈ ℤ) |
|
Theorem | halfnz 8594 |
One-half is not an integer. (Contributed by NM, 31-Jul-2004.)
|
⊢ ¬ (1 / 2) ∈
ℤ |
|
Theorem | 3halfnz 8595 |
Three halves is not an integer. (Contributed by AV, 2-Jun-2020.)
|
⊢ ¬ (3 / 2) ∈
ℤ |
|
Theorem | suprzclex 8596* |
The supremum of a set of integers is an element of the set.
(Contributed by Jim Kingdon, 20-Dec-2021.)
|
⊢ (𝜑 → ∃𝑥 ∈ ℝ (∀𝑦 ∈ 𝐴 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧 ∈ 𝐴 𝑦 < 𝑧))) & ⊢ (𝜑 → 𝐴 ⊆ ℤ)
⇒ ⊢ (𝜑 → sup(𝐴, ℝ, < ) ∈ 𝐴) |
|
Theorem | prime 8597* |
Two ways to express "𝐴 is a prime number (or 1)."
(Contributed by
NM, 4-May-2005.)
|
⊢ (𝐴 ∈ ℕ → (∀𝑥 ∈ ℕ ((𝐴 / 𝑥) ∈ ℕ → (𝑥 = 1 ∨ 𝑥 = 𝐴)) ↔ ∀𝑥 ∈ ℕ ((1 < 𝑥 ∧ 𝑥 ≤ 𝐴 ∧ (𝐴 / 𝑥) ∈ ℕ) → 𝑥 = 𝐴))) |
|
Theorem | msqznn 8598 |
The square of a nonzero integer is a positive integer. (Contributed by
NM, 2-Aug-2004.)
|
⊢ ((𝐴 ∈ ℤ ∧ 𝐴 ≠ 0) → (𝐴 · 𝐴) ∈ ℕ) |
|
Theorem | zneo 8599 |
No even integer equals an odd integer (i.e. no integer can be both even
and odd). Exercise 10(a) of [Apostol] p.
28. (Contributed by NM,
31-Jul-2004.) (Proof shortened by Mario Carneiro, 18-May-2014.)
|
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (2 · 𝐴) ≠ ((2 · 𝐵) + 1)) |
|
Theorem | nneoor 8600 |
A positive integer is even or odd. (Contributed by Jim Kingdon,
15-Mar-2020.)
|
⊢ (𝑁 ∈ ℕ → ((𝑁 / 2) ∈ ℕ ∨ ((𝑁 + 1) / 2) ∈
ℕ)) |