| Metamath
Proof Explorer Theorem List (p. 127 of 494) | < Previous Next > | |
| Bad symbols? Try the
GIF version. |
||
|
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
||
| Color key: | (1-30937) |
(30938-32460) |
(32461-49324) |
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Theorem | elxnn0 12601 | An extended nonnegative integer is either a standard nonnegative integer or positive infinity. (Contributed by AV, 10-Dec-2020.) |
| ⊢ (𝐴 ∈ ℕ0* ↔ (𝐴 ∈ ℕ0 ∨ 𝐴 = +∞)) | ||
| Theorem | nn0ssxnn0 12602 | The standard nonnegative integers are a subset of the extended nonnegative integers. (Contributed by AV, 10-Dec-2020.) |
| ⊢ ℕ0 ⊆ ℕ0* | ||
| Theorem | nn0xnn0 12603 | A standard nonnegative integer is an extended nonnegative integer. (Contributed by AV, 10-Dec-2020.) |
| ⊢ (𝐴 ∈ ℕ0 → 𝐴 ∈ ℕ0*) | ||
| Theorem | xnn0xr 12604 | An extended nonnegative integer is an extended real. (Contributed by AV, 10-Dec-2020.) |
| ⊢ (𝐴 ∈ ℕ0* → 𝐴 ∈ ℝ*) | ||
| Theorem | 0xnn0 12605 | Zero is an extended nonnegative integer. (Contributed by AV, 10-Dec-2020.) |
| ⊢ 0 ∈ ℕ0* | ||
| Theorem | pnf0xnn0 12606 | Positive infinity is an extended nonnegative integer. (Contributed by AV, 10-Dec-2020.) |
| ⊢ +∞ ∈ ℕ0* | ||
| Theorem | nn0nepnf 12607 | No standard nonnegative integer equals positive infinity. (Contributed by AV, 10-Dec-2020.) |
| ⊢ (𝐴 ∈ ℕ0 → 𝐴 ≠ +∞) | ||
| Theorem | nn0xnn0d 12608 | A standard nonnegative integer is an extended nonnegative integer, deduction form. (Contributed by AV, 10-Dec-2020.) |
| ⊢ (𝜑 → 𝐴 ∈ ℕ0) ⇒ ⊢ (𝜑 → 𝐴 ∈ ℕ0*) | ||
| Theorem | nn0nepnfd 12609 | No standard nonnegative integer equals positive infinity, deduction form. (Contributed by AV, 10-Dec-2020.) |
| ⊢ (𝜑 → 𝐴 ∈ ℕ0) ⇒ ⊢ (𝜑 → 𝐴 ≠ +∞) | ||
| Theorem | xnn0nemnf 12610 | No extended nonnegative integer equals negative infinity. (Contributed by AV, 10-Dec-2020.) |
| ⊢ (𝐴 ∈ ℕ0* → 𝐴 ≠ -∞) | ||
| Theorem | xnn0xrnemnf 12611 | The extended nonnegative integers are extended reals without negative infinity. (Contributed by AV, 10-Dec-2020.) |
| ⊢ (𝐴 ∈ ℕ0* → (𝐴 ∈ ℝ* ∧ 𝐴 ≠ -∞)) | ||
| Theorem | xnn0nnn0pnf 12612 | An extended nonnegative integer which is not a standard nonnegative integer is positive infinity. (Contributed by AV, 10-Dec-2020.) |
| ⊢ ((𝑁 ∈ ℕ0* ∧ ¬ 𝑁 ∈ ℕ0) → 𝑁 = +∞) | ||
| Syntax | cz 12613 | Extend class notation to include the class of integers. |
| class ℤ | ||
| Definition | df-z 12614 | 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 12615 | Membership in the set of integers. (Contributed by NM, 8-Jan-2002.) |
| ⊢ (𝑁 ∈ ℤ ↔ (𝑁 ∈ ℝ ∧ (𝑁 = 0 ∨ 𝑁 ∈ ℕ ∨ -𝑁 ∈ ℕ))) | ||
| Theorem | nnnegz 12616 | The negative of a positive integer is an integer. (Contributed by NM, 12-Jan-2002.) |
| ⊢ (𝑁 ∈ ℕ → -𝑁 ∈ ℤ) | ||
| Theorem | zre 12617 | An integer is a real. (Contributed by NM, 8-Jan-2002.) |
| ⊢ (𝑁 ∈ ℤ → 𝑁 ∈ ℝ) | ||
| Theorem | zcn 12618 | An integer is a complex number. (Contributed by NM, 9-May-2004.) |
| ⊢ (𝑁 ∈ ℤ → 𝑁 ∈ ℂ) | ||
| Theorem | zrei 12619 | An integer is a real number. (Contributed by NM, 14-Jul-2005.) |
| ⊢ 𝐴 ∈ ℤ ⇒ ⊢ 𝐴 ∈ ℝ | ||
| Theorem | zssre 12620 | The integers are a subset of the reals. (Contributed by NM, 2-Aug-2004.) |
| ⊢ ℤ ⊆ ℝ | ||
| Theorem | zsscn 12621 | The integers are a subset of the complex numbers. (Contributed by NM, 2-Aug-2004.) |
| ⊢ ℤ ⊆ ℂ | ||
| Theorem | zex 12622 | The set of integers exists. See also zexALT 12633. (Contributed by NM, 30-Jul-2004.) (Revised by Mario Carneiro, 17-Nov-2014.) |
| ⊢ ℤ ∈ V | ||
| Theorem | elnnz 12623 | Positive integer property expressed in terms of integers. (Contributed by NM, 8-Jan-2002.) |
| ⊢ (𝑁 ∈ ℕ ↔ (𝑁 ∈ ℤ ∧ 0 < 𝑁)) | ||
| Theorem | 0z 12624 | Zero is an integer. (Contributed by NM, 12-Jan-2002.) |
| ⊢ 0 ∈ ℤ | ||
| Theorem | 0zd 12625 | Zero is an integer, deduction form. (Contributed by David A. Wheeler, 8-Dec-2018.) |
| ⊢ (𝜑 → 0 ∈ ℤ) | ||
| Theorem | elnn0z 12626 | Nonnegative integer property expressed in terms of integers. (Contributed by NM, 9-May-2004.) |
| ⊢ (𝑁 ∈ ℕ0 ↔ (𝑁 ∈ ℤ ∧ 0 ≤ 𝑁)) | ||
| Theorem | elznn0nn 12627 | Integer property expressed in terms nonnegative integers and positive integers. (Contributed by NM, 10-May-2004.) |
| ⊢ (𝑁 ∈ ℤ ↔ (𝑁 ∈ ℕ0 ∨ (𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ))) | ||
| Theorem | elznn0 12628 | Integer property expressed in terms of nonnegative integers. (Contributed by NM, 9-May-2004.) |
| ⊢ (𝑁 ∈ ℤ ↔ (𝑁 ∈ ℝ ∧ (𝑁 ∈ ℕ0 ∨ -𝑁 ∈ ℕ0))) | ||
| Theorem | elznn 12629 | Integer property expressed in terms of positive integers and nonnegative integers. (Contributed by NM, 12-Jul-2005.) |
| ⊢ (𝑁 ∈ ℤ ↔ (𝑁 ∈ ℝ ∧ (𝑁 ∈ ℕ ∨ -𝑁 ∈ ℕ0))) | ||
| Theorem | zle0orge1 12630 | There is no integer in the open unit interval, i.e., an integer is either less than or equal to 0 or greater than or equal to 1. (Contributed by AV, 4-Jun-2023.) |
| ⊢ (𝑍 ∈ ℤ → (𝑍 ≤ 0 ∨ 1 ≤ 𝑍)) | ||
| Theorem | elz2 12631* | 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 12632 | Alternative definition of the integers, based on elz2 12631. (Contributed by Mario Carneiro, 16-May-2014.) |
| ⊢ ℤ = ( − “ (ℕ × ℕ)) | ||
| Theorem | zexALT 12633 | Alternate proof of zex 12622. (Contributed by NM, 30-Jul-2004.) (Revised by Mario Carneiro, 16-May-2014.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ ℤ ∈ V | ||
| Theorem | nnz 12634 | A positive integer is an integer. (Contributed by NM, 9-May-2004.) Reduce dependencies on axioms. (Revised by Steven Nguyen, 29-Nov-2022.) |
| ⊢ (𝑁 ∈ ℕ → 𝑁 ∈ ℤ) | ||
| Theorem | nnssz 12635 | Positive integers are a subset of integers. (Contributed by NM, 9-Jan-2002.) |
| ⊢ ℕ ⊆ ℤ | ||
| Theorem | nn0ssz 12636 | Nonnegative integers are a subset of the integers. (Contributed by NM, 9-May-2004.) |
| ⊢ ℕ0 ⊆ ℤ | ||
| Theorem | nnzOLD 12637 | Obsolete version of nnz 12634 as of 1-Feb-2025. (Contributed by NM, 9-May-2004.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ (𝑁 ∈ ℕ → 𝑁 ∈ ℤ) | ||
| Theorem | nn0z 12638 | A nonnegative integer is an integer. (Contributed by NM, 9-May-2004.) |
| ⊢ (𝑁 ∈ ℕ0 → 𝑁 ∈ ℤ) | ||
| Theorem | nn0zd 12639 | A nonnegative integer is an integer. (Contributed by Mario Carneiro, 28-May-2016.) |
| ⊢ (𝜑 → 𝐴 ∈ ℕ0) ⇒ ⊢ (𝜑 → 𝐴 ∈ ℤ) | ||
| Theorem | nnzd 12640 | A positive integer is an integer. (Contributed by Mario Carneiro, 28-May-2016.) |
| ⊢ (𝜑 → 𝐴 ∈ ℕ) ⇒ ⊢ (𝜑 → 𝐴 ∈ ℤ) | ||
| Theorem | nnzi 12641 | A positive integer is an integer. (Contributed by Mario Carneiro, 18-Feb-2014.) |
| ⊢ 𝑁 ∈ ℕ ⇒ ⊢ 𝑁 ∈ ℤ | ||
| Theorem | nn0zi 12642 | A nonnegative integer is an integer. (Contributed by Mario Carneiro, 18-Feb-2014.) |
| ⊢ 𝑁 ∈ ℕ0 ⇒ ⊢ 𝑁 ∈ ℤ | ||
| Theorem | elnnz1 12643 | Positive integer property expressed in terms of integers. (Contributed by NM, 10-May-2004.) (Proof shortened by Mario Carneiro, 16-May-2014.) |
| ⊢ (𝑁 ∈ ℕ ↔ (𝑁 ∈ ℤ ∧ 1 ≤ 𝑁)) | ||
| Theorem | znnnlt1 12644 | An integer is not a positive integer iff it is less than one. (Contributed by NM, 13-Jul-2005.) |
| ⊢ (𝑁 ∈ ℤ → (¬ 𝑁 ∈ ℕ ↔ 𝑁 < 1)) | ||
| Theorem | nnzrab 12645 | Positive integers expressed as a subset of integers. (Contributed by NM, 3-Oct-2004.) |
| ⊢ ℕ = {𝑥 ∈ ℤ ∣ 1 ≤ 𝑥} | ||
| Theorem | nn0zrab 12646 | Nonnegative integers expressed as a subset of integers. (Contributed by NM, 3-Oct-2004.) |
| ⊢ ℕ0 = {𝑥 ∈ ℤ ∣ 0 ≤ 𝑥} | ||
| Theorem | 1z 12647 | One is an integer. (Contributed by NM, 10-May-2004.) |
| ⊢ 1 ∈ ℤ | ||
| Theorem | 1zzd 12648 | One is an integer, deduction form. (Contributed by David A. Wheeler, 6-Dec-2018.) |
| ⊢ (𝜑 → 1 ∈ ℤ) | ||
| Theorem | 2z 12649 | 2 is an integer. (Contributed by NM, 10-May-2004.) |
| ⊢ 2 ∈ ℤ | ||
| Theorem | 3z 12650 | 3 is an integer. (Contributed by David A. Wheeler, 8-Dec-2018.) |
| ⊢ 3 ∈ ℤ | ||
| Theorem | 4z 12651 | 4 is an integer. (Contributed by BJ, 26-Mar-2020.) |
| ⊢ 4 ∈ ℤ | ||
| Theorem | znegcl 12652 | Closure law for negative integers. (Contributed by NM, 9-May-2004.) |
| ⊢ (𝑁 ∈ ℤ → -𝑁 ∈ ℤ) | ||
| Theorem | neg1z 12653 | -1 is an integer. (Contributed by David A. Wheeler, 5-Dec-2018.) |
| ⊢ -1 ∈ ℤ | ||
| Theorem | znegclb 12654 | A complex number is an integer iff its negative is. (Contributed by Stefan O'Rear, 13-Sep-2014.) |
| ⊢ (𝐴 ∈ ℂ → (𝐴 ∈ ℤ ↔ -𝐴 ∈ ℤ)) | ||
| Theorem | nn0negz 12655 | The negative of a nonnegative integer is an integer. (Contributed by NM, 9-May-2004.) |
| ⊢ (𝑁 ∈ ℕ0 → -𝑁 ∈ ℤ) | ||
| Theorem | nn0negzi 12656 | The negative of a nonnegative integer is an integer. (Contributed by Mario Carneiro, 18-Feb-2014.) |
| ⊢ 𝑁 ∈ ℕ0 ⇒ ⊢ -𝑁 ∈ ℤ | ||
| Theorem | zaddcl 12657 | Closure of addition of integers. (Contributed by NM, 9-May-2004.) (Proof shortened by Mario Carneiro, 16-May-2014.) |
| ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 + 𝑁) ∈ ℤ) | ||
| Theorem | peano2z 12658 | Second Peano postulate generalized to integers. (Contributed by NM, 13-Feb-2005.) |
| ⊢ (𝑁 ∈ ℤ → (𝑁 + 1) ∈ ℤ) | ||
| Theorem | zsubcl 12659 | Closure of subtraction of integers. (Contributed by NM, 11-May-2004.) |
| ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 − 𝑁) ∈ ℤ) | ||
| Theorem | peano2zm 12660 | "Reverse" second Peano postulate for integers. (Contributed by NM, 12-Sep-2005.) |
| ⊢ (𝑁 ∈ ℤ → (𝑁 − 1) ∈ ℤ) | ||
| Theorem | zletr 12661 | Transitive law of ordering for integers. (Contributed by Alexander van der Vekens, 3-Apr-2018.) |
| ⊢ ((𝐽 ∈ ℤ ∧ 𝐾 ∈ ℤ ∧ 𝐿 ∈ ℤ) → ((𝐽 ≤ 𝐾 ∧ 𝐾 ≤ 𝐿) → 𝐽 ≤ 𝐿)) | ||
| Theorem | zrevaddcl 12662 | Reverse closure law for addition of integers. (Contributed by NM, 11-May-2004.) |
| ⊢ (𝑁 ∈ ℤ → ((𝑀 ∈ ℂ ∧ (𝑀 + 𝑁) ∈ ℤ) ↔ 𝑀 ∈ ℤ)) | ||
| Theorem | znnsub 12663 | The positive difference of unequal integers is a positive integer. (Generalization of nnsub 12310.) (Contributed by NM, 11-May-2004.) |
| ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 < 𝑁 ↔ (𝑁 − 𝑀) ∈ ℕ)) | ||
| Theorem | znn0sub 12664 | The nonnegative difference of integers is a nonnegative integer. (Generalization of nn0sub 12576.) (Contributed by NM, 14-Jul-2005.) |
| ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 ≤ 𝑁 ↔ (𝑁 − 𝑀) ∈ ℕ0)) | ||
| Theorem | nzadd 12665 | The sum of a real number not being an integer and an integer is not an integer. (Contributed by AV, 19-Jul-2021.) |
| ⊢ ((𝐴 ∈ (ℝ ∖ ℤ) ∧ 𝐵 ∈ ℤ) → (𝐴 + 𝐵) ∈ (ℝ ∖ ℤ)) | ||
| Theorem | zmulcl 12666 | Closure of multiplication of integers. (Contributed by NM, 30-Jul-2004.) |
| ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 · 𝑁) ∈ ℤ) | ||
| Theorem | zltp1le 12667 | Integer ordering relation. (Contributed by NM, 10-May-2004.) (Proof shortened by Mario Carneiro, 16-May-2014.) |
| ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 < 𝑁 ↔ (𝑀 + 1) ≤ 𝑁)) | ||
| Theorem | zleltp1 12668 | Integer ordering relation. (Contributed by NM, 10-May-2004.) |
| ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 ≤ 𝑁 ↔ 𝑀 < (𝑁 + 1))) | ||
| Theorem | zlem1lt 12669 | Integer ordering relation. (Contributed by NM, 13-Nov-2004.) |
| ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 ≤ 𝑁 ↔ (𝑀 − 1) < 𝑁)) | ||
| Theorem | zltlem1 12670 | Integer ordering relation. (Contributed by NM, 13-Nov-2004.) |
| ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 < 𝑁 ↔ 𝑀 ≤ (𝑁 − 1))) | ||
| Theorem | zltlem1d 12671 | Integer ordering relation, a deduction version. (Contributed by metakunt, 23-May-2024.) |
| ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝑁 ∈ ℤ) ⇒ ⊢ (𝜑 → (𝑀 < 𝑁 ↔ 𝑀 ≤ (𝑁 − 1))) | ||
| Theorem | zgt0ge1 12672 | An integer greater than 0 is greater than or equal to 1. (Contributed by AV, 14-Oct-2018.) |
| ⊢ (𝑍 ∈ ℤ → (0 < 𝑍 ↔ 1 ≤ 𝑍)) | ||
| Theorem | nnleltp1 12673 | Positive integer ordering relation. (Contributed by NM, 13-Aug-2001.) (Proof shortened by Mario Carneiro, 16-May-2014.) |
| ⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) → (𝐴 ≤ 𝐵 ↔ 𝐴 < (𝐵 + 1))) | ||
| Theorem | nnltp1le 12674 | Positive integer ordering relation. (Contributed by NM, 19-Aug-2001.) |
| ⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) → (𝐴 < 𝐵 ↔ (𝐴 + 1) ≤ 𝐵)) | ||
| Theorem | nnaddm1cl 12675 | 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 12676 | Nonnegative integer ordering relation. (Contributed by Raph Levien, 10-Dec-2002.) (Proof shortened by Mario Carneiro, 16-May-2014.) |
| ⊢ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) → (𝑀 < 𝑁 ↔ (𝑀 + 1) ≤ 𝑁)) | ||
| Theorem | nn0leltp1 12677 | Nonnegative integer ordering relation. (Contributed by Raph Levien, 10-Apr-2004.) |
| ⊢ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) → (𝑀 ≤ 𝑁 ↔ 𝑀 < (𝑁 + 1))) | ||
| Theorem | nn0ltlem1 12678 | Nonnegative integer ordering relation. (Contributed by NM, 10-May-2004.) (Proof shortened by Mario Carneiro, 16-May-2014.) |
| ⊢ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) → (𝑀 < 𝑁 ↔ 𝑀 ≤ (𝑁 − 1))) | ||
| Theorem | nn0sub2 12679 | Subtraction of nonnegative integers. (Contributed by NM, 4-Sep-2005.) |
| ⊢ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ 𝑀 ≤ 𝑁) → (𝑁 − 𝑀) ∈ ℕ0) | ||
| Theorem | nn0lt10b 12680 | A nonnegative integer less than 1 is 0. (Contributed by Paul Chapman, 22-Jun-2011.) (Proof shortened by OpenAI, 25-Mar-2020.) |
| ⊢ (𝑁 ∈ ℕ0 → (𝑁 < 1 ↔ 𝑁 = 0)) | ||
| Theorem | nn0lt2 12681 | 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 12682 | 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 12683 | Nonnegative integer ordering relation. (Contributed by NM, 21-Jun-2005.) |
| ⊢ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) → (𝑀 ≤ 𝑁 ↔ (𝑀 − 1) < 𝑁)) | ||
| Theorem | nnlem1lt 12684 | Positive integer ordering relation. (Contributed by NM, 21-Jun-2005.) |
| ⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (𝑀 ≤ 𝑁 ↔ (𝑀 − 1) < 𝑁)) | ||
| Theorem | nnltlem1 12685 | Positive integer ordering relation. (Contributed by NM, 21-Jun-2005.) |
| ⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (𝑀 < 𝑁 ↔ 𝑀 ≤ (𝑁 − 1))) | ||
| Theorem | nnm1ge0 12686 | A positive integer decreased by 1 is greater than or equal to 0. (Contributed by AV, 30-Oct-2018.) |
| ⊢ (𝑁 ∈ ℕ → 0 ≤ (𝑁 − 1)) | ||
| Theorem | nn0ge0div 12687 | 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 12688* | Two ways to express "𝑀 divides 𝑁". (Contributed by NM, 3-Oct-2008.) |
| ⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℤ) → (∃𝑘 ∈ ℤ (𝑀 · 𝑘) = 𝑁 ↔ (𝑁 / 𝑀) ∈ ℤ)) | ||
| Theorem | zdivadd 12689 | Property of divisibility: if 𝐷 divides 𝐴 and 𝐵 then it divides 𝐴 + 𝐵. (Contributed by NM, 3-Oct-2008.) |
| ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ ((𝐴 / 𝐷) ∈ ℤ ∧ (𝐵 / 𝐷) ∈ ℤ)) → ((𝐴 + 𝐵) / 𝐷) ∈ ℤ) | ||
| Theorem | zdivmul 12690 | Property of divisibility: if 𝐷 divides 𝐴 then it divides 𝐵 · 𝐴. (Contributed by NM, 3-Oct-2008.) |
| ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ (𝐴 / 𝐷) ∈ ℤ) → ((𝐵 · 𝐴) / 𝐷) ∈ ℤ) | ||
| Theorem | zextle 12691* | An extensionality-like property for integer ordering. (Contributed by NM, 29-Oct-2005.) |
| ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ ∀𝑘 ∈ ℤ (𝑘 ≤ 𝑀 ↔ 𝑘 ≤ 𝑁)) → 𝑀 = 𝑁) | ||
| Theorem | zextlt 12692* | An extensionality-like property for integer ordering. (Contributed by NM, 29-Oct-2005.) |
| ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ ∀𝑘 ∈ ℤ (𝑘 < 𝑀 ↔ 𝑘 < 𝑁)) → 𝑀 = 𝑁) | ||
| Theorem | recnz 12693 | The reciprocal of a number greater than 1 is not an integer. (Contributed by NM, 3-May-2005.) |
| ⊢ ((𝐴 ∈ ℝ ∧ 1 < 𝐴) → ¬ (1 / 𝐴) ∈ ℤ) | ||
| Theorem | btwnnz 12694 | A number between an integer and its successor is not an integer. (Contributed by NM, 3-May-2005.) |
| ⊢ ((𝐴 ∈ ℤ ∧ 𝐴 < 𝐵 ∧ 𝐵 < (𝐴 + 1)) → ¬ 𝐵 ∈ ℤ) | ||
| Theorem | gtndiv 12695 | A larger number does not divide a smaller positive integer. (Contributed by NM, 3-May-2005.) |
| ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℕ ∧ 𝐵 < 𝐴) → ¬ (𝐵 / 𝐴) ∈ ℤ) | ||
| Theorem | halfnz 12696 | One-half is not an integer. (Contributed by NM, 31-Jul-2004.) |
| ⊢ ¬ (1 / 2) ∈ ℤ | ||
| Theorem | 3halfnz 12697 | Three halves is not an integer. (Contributed by AV, 2-Jun-2020.) |
| ⊢ ¬ (3 / 2) ∈ ℤ | ||
| Theorem | suprzcl 12698* | The supremum of a bounded-above set of integers is a member of the set. (Contributed by Paul Chapman, 21-Mar-2011.) (Revised by Mario Carneiro, 26-Jun-2015.) |
| ⊢ ((𝐴 ⊆ ℤ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥) → sup(𝐴, ℝ, < ) ∈ 𝐴) | ||
| Theorem | prime 12699* | Two ways to express "𝐴 is a prime number (or 1)". See also isprm 16710. (Contributed by NM, 4-May-2005.) |
| ⊢ (𝐴 ∈ ℕ → (∀𝑥 ∈ ℕ ((𝐴 / 𝑥) ∈ ℕ → (𝑥 = 1 ∨ 𝑥 = 𝐴)) ↔ ∀𝑥 ∈ ℕ ((1 < 𝑥 ∧ 𝑥 ≤ 𝐴 ∧ (𝐴 / 𝑥) ∈ ℕ) → 𝑥 = 𝐴))) | ||
| Theorem | msqznn 12700 | The square of a nonzero integer is a positive integer. (Contributed by NM, 2-Aug-2004.) |
| ⊢ ((𝐴 ∈ ℤ ∧ 𝐴 ≠ 0) → (𝐴 · 𝐴) ∈ ℕ) | ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |