![]() |
Intuitionistic Logic Explorer Theorem List (p. 78 of 95) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > ILE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | nnex 7701 | The set of positive integers exists. (Contributed by NM, 3-Oct-1999.) (Revised by Mario Carneiro, 17-Nov-2014.) |
⊢ ℕ ∈ V | ||
Theorem | nnre 7702 | A positive integer is a real number. (Contributed by NM, 18-Aug-1999.) |
⊢ (A ∈ ℕ → A ∈ ℝ) | ||
Theorem | nncn 7703 | A positive integer is a complex number. (Contributed by NM, 18-Aug-1999.) |
⊢ (A ∈ ℕ → A ∈ ℂ) | ||
Theorem | nnrei 7704 | A positive integer is a real number. (Contributed by NM, 18-Aug-1999.) |
⊢ A ∈ ℕ ⇒ ⊢ A ∈ ℝ | ||
Theorem | nncni 7705 | A positive integer is a complex number. (Contributed by NM, 18-Aug-1999.) |
⊢ A ∈ ℕ ⇒ ⊢ A ∈ ℂ | ||
Theorem | 1nn 7706 | Peano postulate: 1 is a positive integer. (Contributed by NM, 11-Jan-1997.) |
⊢ 1 ∈ ℕ | ||
Theorem | peano2nn 7707 | Peano postulate: a successor of a positive integer is a positive integer. (Contributed by NM, 11-Jan-1997.) (Revised by Mario Carneiro, 17-Nov-2014.) |
⊢ (A ∈ ℕ → (A + 1) ∈ ℕ) | ||
Theorem | nnred 7708 | A positive integer is a real number. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (φ → A ∈ ℕ) ⇒ ⊢ (φ → A ∈ ℝ) | ||
Theorem | nncnd 7709 | A positive integer is a complex number. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (φ → A ∈ ℕ) ⇒ ⊢ (φ → A ∈ ℂ) | ||
Theorem | peano2nnd 7710 | Peano postulate: a successor of a positive integer is a positive integer. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (φ → A ∈ ℕ) ⇒ ⊢ (φ → (A + 1) ∈ ℕ) | ||
Theorem | nnind 7711* | Principle of Mathematical Induction (inference schema). The first four hypotheses give us the substitution instances we need; the last two are the basis and the induction step. See nnaddcl 7715 for an example of its use. This is an alternative for Metamath 100 proof #74. (Contributed by NM, 10-Jan-1997.) (Revised by Mario Carneiro, 16-Jun-2013.) |
⊢ (x = 1 → (φ ↔ ψ)) & ⊢ (x = y → (φ ↔ χ)) & ⊢ (x = (y + 1) → (φ ↔ θ)) & ⊢ (x = A → (φ ↔ τ)) & ⊢ ψ & ⊢ (y ∈ ℕ → (χ → θ)) ⇒ ⊢ (A ∈ ℕ → τ) | ||
Theorem | nnindALT 7712* |
Principle of Mathematical Induction (inference schema). The last four
hypotheses give us the substitution instances we need; the first two are
the induction step and the basis.
This ALT version of nnind 7711 has a different hypothesis order. It may be easier to use with the metamath program's Proof Assistant, because "MM-PA> assign last" will be applied to the substitution instances first. We may eventually use this one as the official version. You may use either version. After the proof is complete, the ALT version can be changed to the non-ALT version with "MM-PA> minimize nnind /allow". (Contributed by NM, 7-Dec-2005.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ (y ∈ ℕ → (χ → θ)) & ⊢ ψ & ⊢ (x = 1 → (φ ↔ ψ)) & ⊢ (x = y → (φ ↔ χ)) & ⊢ (x = (y + 1) → (φ ↔ θ)) & ⊢ (x = A → (φ ↔ τ)) ⇒ ⊢ (A ∈ ℕ → τ) | ||
Theorem | nn1m1nn 7713 | Every positive integer is one or a successor. (Contributed by Mario Carneiro, 16-May-2014.) |
⊢ (A ∈ ℕ → (A = 1 ∨ (A − 1) ∈ ℕ)) | ||
Theorem | nn1suc 7714* | If a statement holds for 1 and also holds for a successor, it holds for all positive integers. The first three hypotheses give us the substitution instances we need; the last two show that it holds for 1 and for a successor. (Contributed by NM, 11-Oct-2004.) (Revised by Mario Carneiro, 16-May-2014.) |
⊢ (x = 1 → (φ ↔ ψ)) & ⊢ (x = (y + 1) → (φ ↔ χ)) & ⊢ (x = A → (φ ↔ θ)) & ⊢ ψ & ⊢ (y ∈ ℕ → χ) ⇒ ⊢ (A ∈ ℕ → θ) | ||
Theorem | nnaddcl 7715 | Closure of addition of positive integers, proved by induction on the second addend. (Contributed by NM, 12-Jan-1997.) |
⊢ ((A ∈ ℕ ∧ B ∈ ℕ) → (A + B) ∈ ℕ) | ||
Theorem | nnmulcl 7716 | Closure of multiplication of positive integers. (Contributed by NM, 12-Jan-1997.) |
⊢ ((A ∈ ℕ ∧ B ∈ ℕ) → (A · B) ∈ ℕ) | ||
Theorem | nnmulcli 7717 | Closure of multiplication of positive integers. (Contributed by Mario Carneiro, 18-Feb-2014.) |
⊢ A ∈ ℕ & ⊢ B ∈ ℕ ⇒ ⊢ (A · B) ∈ ℕ | ||
Theorem | nnge1 7718 | A positive integer is one or greater. (Contributed by NM, 25-Aug-1999.) |
⊢ (A ∈ ℕ → 1 ≤ A) | ||
Theorem | nnle1eq1 7719 | A positive integer is less than or equal to one iff it is equal to one. (Contributed by NM, 3-Apr-2005.) |
⊢ (A ∈ ℕ → (A ≤ 1 ↔ A = 1)) | ||
Theorem | nngt0 7720 | A positive integer is positive. (Contributed by NM, 26-Sep-1999.) |
⊢ (A ∈ ℕ → 0 < A) | ||
Theorem | nnnlt1 7721 | A positive integer is not less than one. (Contributed by NM, 18-Jan-2004.) (Revised by Mario Carneiro, 27-May-2016.) |
⊢ (A ∈ ℕ → ¬ A < 1) | ||
Theorem | 0nnn 7722 | Zero is not a positive integer. (Contributed by NM, 25-Aug-1999.) |
⊢ ¬ 0 ∈ ℕ | ||
Theorem | nnne0 7723 | A positive integer is nonzero. (Contributed by NM, 27-Sep-1999.) |
⊢ (A ∈ ℕ → A ≠ 0) | ||
Theorem | nnap0 7724 | A positive integer is apart from zero. (Contributed by Jim Kingdon, 8-Mar-2020.) |
⊢ (A ∈ ℕ → A # 0) | ||
Theorem | nngt0i 7725 | A positive integer is positive (inference version). (Contributed by NM, 17-Sep-1999.) |
⊢ A ∈ ℕ ⇒ ⊢ 0 < A | ||
Theorem | nnne0i 7726 | A positive integer is nonzero (inference version). (Contributed by NM, 25-Aug-1999.) |
⊢ A ∈ ℕ ⇒ ⊢ A ≠ 0 | ||
Theorem | nn2ge 7727* | There exists a positive integer greater than or equal to any two others. (Contributed by NM, 18-Aug-1999.) |
⊢ ((A ∈ ℕ ∧ B ∈ ℕ) → ∃x ∈ ℕ (A ≤ x ∧ B ≤ x)) | ||
Theorem | nn1gt1 7728 | A positive integer is either one or greater than one. This is for ℕ; 0elnn 4283 is a similar theorem for 𝜔 (the natural numbers as ordinals). (Contributed by Jim Kingdon, 7-Mar-2020.) |
⊢ (A ∈ ℕ → (A = 1 ∨ 1 < A)) | ||
Theorem | nngt1ne1 7729 | A positive integer is greater than one iff it is not equal to one. (Contributed by NM, 7-Oct-2004.) |
⊢ (A ∈ ℕ → (1 < A ↔ A ≠ 1)) | ||
Theorem | nndivre 7730 | The quotient of a real and a positive integer is real. (Contributed by NM, 28-Nov-2008.) |
⊢ ((A ∈ ℝ ∧ 𝑁 ∈ ℕ) → (A / 𝑁) ∈ ℝ) | ||
Theorem | nnrecre 7731 | The reciprocal of a positive integer is real. (Contributed by NM, 8-Feb-2008.) |
⊢ (𝑁 ∈ ℕ → (1 / 𝑁) ∈ ℝ) | ||
Theorem | nnrecgt0 7732 | The reciprocal of a positive integer is positive. (Contributed by NM, 25-Aug-1999.) |
⊢ (A ∈ ℕ → 0 < (1 / A)) | ||
Theorem | nnsub 7733 | Subtraction of positive integers. (Contributed by NM, 20-Aug-2001.) (Revised by Mario Carneiro, 16-May-2014.) |
⊢ ((A ∈ ℕ ∧ B ∈ ℕ) → (A < B ↔ (B − A) ∈ ℕ)) | ||
Theorem | nnsubi 7734 | Subtraction of positive integers. (Contributed by NM, 19-Aug-2001.) |
⊢ A ∈ ℕ & ⊢ B ∈ ℕ ⇒ ⊢ (A < B ↔ (B − A) ∈ ℕ) | ||
Theorem | nndiv 7735* | Two ways to express "A divides B " for positive integers. (Contributed by NM, 3-Feb-2004.) (Proof shortened by Mario Carneiro, 16-May-2014.) |
⊢ ((A ∈ ℕ ∧ B ∈ ℕ) → (∃x ∈ ℕ (A · x) = B ↔ (B / A) ∈ ℕ)) | ||
Theorem | nndivtr 7736 | Transitive property of divisibility: if A divides B and B divides 𝐶, then A divides 𝐶. Typically, 𝐶 would be an integer, although the theorem holds for complex 𝐶. (Contributed by NM, 3-May-2005.) |
⊢ (((A ∈ ℕ ∧ B ∈ ℕ ∧ 𝐶 ∈ ℂ) ∧ ((B / A) ∈ ℕ ∧ (𝐶 / B) ∈ ℕ)) → (𝐶 / A) ∈ ℕ) | ||
Theorem | nnge1d 7737 | A positive integer is one or greater. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (φ → A ∈ ℕ) ⇒ ⊢ (φ → 1 ≤ A) | ||
Theorem | nngt0d 7738 | A positive integer is positive. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (φ → A ∈ ℕ) ⇒ ⊢ (φ → 0 < A) | ||
Theorem | nnne0d 7739 | A positive integer is nonzero. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (φ → A ∈ ℕ) ⇒ ⊢ (φ → A ≠ 0) | ||
Theorem | nnrecred 7740 | The reciprocal of a positive integer is real. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (φ → A ∈ ℕ) ⇒ ⊢ (φ → (1 / A) ∈ ℝ) | ||
Theorem | nnaddcld 7741 | Closure of addition of positive integers. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (φ → A ∈ ℕ) & ⊢ (φ → B ∈ ℕ) ⇒ ⊢ (φ → (A + B) ∈ ℕ) | ||
Theorem | nnmulcld 7742 | Closure of multiplication of positive integers. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (φ → A ∈ ℕ) & ⊢ (φ → B ∈ ℕ) ⇒ ⊢ (φ → (A · B) ∈ ℕ) | ||
Theorem | nndivred 7743 | A positive integer is one or greater. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (φ → A ∈ ℝ) & ⊢ (φ → B ∈ ℕ) ⇒ ⊢ (φ → (A / B) ∈ ℝ) | ||
Note that the numbers 0 and 1 are constants defined as primitives of the complex number axiom system (see df-0 6718 and df-1 6719). Only the digits 0 through 9 (df-0 6718 through df-9 7760) and the number 10 (df-10 7761) are explicitly defined. Most abstract math rarely requires numbers larger than 4. Even in Wiles' proof of Fermat's Last Theorem, the largest number used appears to be 12. | ||
Syntax | c2 7744 | Extend class notation to include the number 2. |
class 2 | ||
Syntax | c3 7745 | Extend class notation to include the number 3. |
class 3 | ||
Syntax | c4 7746 | Extend class notation to include the number 4. |
class 4 | ||
Syntax | c5 7747 | Extend class notation to include the number 5. |
class 5 | ||
Syntax | c6 7748 | Extend class notation to include the number 6. |
class 6 | ||
Syntax | c7 7749 | Extend class notation to include the number 7. |
class 7 | ||
Syntax | c8 7750 | Extend class notation to include the number 8. |
class 8 | ||
Syntax | c9 7751 | Extend class notation to include the number 9. |
class 9 | ||
Syntax | c10 7752 | Extend class notation to include the number 10. |
class 10 | ||
Definition | df-2 7753 | Define the number 2. (Contributed by NM, 27-May-1999.) |
⊢ 2 = (1 + 1) | ||
Definition | df-3 7754 | Define the number 3. (Contributed by NM, 27-May-1999.) |
⊢ 3 = (2 + 1) | ||
Definition | df-4 7755 | Define the number 4. (Contributed by NM, 27-May-1999.) |
⊢ 4 = (3 + 1) | ||
Definition | df-5 7756 | Define the number 5. (Contributed by NM, 27-May-1999.) |
⊢ 5 = (4 + 1) | ||
Definition | df-6 7757 | Define the number 6. (Contributed by NM, 27-May-1999.) |
⊢ 6 = (5 + 1) | ||
Definition | df-7 7758 | Define the number 7. (Contributed by NM, 27-May-1999.) |
⊢ 7 = (6 + 1) | ||
Definition | df-8 7759 | Define the number 8. (Contributed by NM, 27-May-1999.) |
⊢ 8 = (7 + 1) | ||
Definition | df-9 7760 | Define the number 9. (Contributed by NM, 27-May-1999.) |
⊢ 9 = (8 + 1) | ||
Definition | df-10 7761 | Define the number 10. See remarks under df-2 7753. (Contributed by NM, 5-Feb-2007.) |
⊢ 10 = (9 + 1) | ||
Theorem | 0ne1 7762 | 0 ≠ 1 (common case). See aso 1ap0 7374. (Contributed by David A. Wheeler, 8-Dec-2018.) |
⊢ 0 ≠ 1 | ||
Theorem | 1ne0 7763 | 1 ≠ 0. See aso 1ap0 7374. (Contributed by Jim Kingdon, 9-Mar-2020.) |
⊢ 1 ≠ 0 | ||
Theorem | 1m1e0 7764 | (1 − 1) = 0 (common case). (Contributed by David A. Wheeler, 7-Jul-2016.) |
⊢ (1 − 1) = 0 | ||
Theorem | 2re 7765 | The number 2 is real. (Contributed by NM, 27-May-1999.) |
⊢ 2 ∈ ℝ | ||
Theorem | 2cn 7766 | The number 2 is a complex number. (Contributed by NM, 30-Jul-2004.) |
⊢ 2 ∈ ℂ | ||
Theorem | 2ex 7767 | 2 is a set (common case). (Contributed by David A. Wheeler, 8-Dec-2018.) |
⊢ 2 ∈ V | ||
Theorem | 2cnd 7768 | 2 is a complex number, deductive form (common case). (Contributed by David A. Wheeler, 8-Dec-2018.) |
⊢ (φ → 2 ∈ ℂ) | ||
Theorem | 3re 7769 | The number 3 is real. (Contributed by NM, 27-May-1999.) |
⊢ 3 ∈ ℝ | ||
Theorem | 3cn 7770 | The number 3 is a complex number. (Contributed by FL, 17-Oct-2010.) |
⊢ 3 ∈ ℂ | ||
Theorem | 3ex 7771 | 3 is a set (common case). (Contributed by David A. Wheeler, 8-Dec-2018.) |
⊢ 3 ∈ V | ||
Theorem | 4re 7772 | The number 4 is real. (Contributed by NM, 27-May-1999.) |
⊢ 4 ∈ ℝ | ||
Theorem | 4cn 7773 | The number 4 is a complex number. (Contributed by David A. Wheeler, 7-Jul-2016.) |
⊢ 4 ∈ ℂ | ||
Theorem | 5re 7774 | The number 5 is real. (Contributed by NM, 27-May-1999.) |
⊢ 5 ∈ ℝ | ||
Theorem | 5cn 7775 | The number 5 is complex. (Contributed by David A. Wheeler, 8-Dec-2018.) |
⊢ 5 ∈ ℂ | ||
Theorem | 6re 7776 | The number 6 is real. (Contributed by NM, 27-May-1999.) |
⊢ 6 ∈ ℝ | ||
Theorem | 6cn 7777 | The number 6 is complex. (Contributed by David A. Wheeler, 8-Dec-2018.) |
⊢ 6 ∈ ℂ | ||
Theorem | 7re 7778 | The number 7 is real. (Contributed by NM, 27-May-1999.) |
⊢ 7 ∈ ℝ | ||
Theorem | 7cn 7779 | The number 7 is complex. (Contributed by David A. Wheeler, 8-Dec-2018.) |
⊢ 7 ∈ ℂ | ||
Theorem | 8re 7780 | The number 8 is real. (Contributed by NM, 27-May-1999.) |
⊢ 8 ∈ ℝ | ||
Theorem | 8cn 7781 | The number 8 is complex. (Contributed by David A. Wheeler, 8-Dec-2018.) |
⊢ 8 ∈ ℂ | ||
Theorem | 9re 7782 | The number 9 is real. (Contributed by NM, 27-May-1999.) |
⊢ 9 ∈ ℝ | ||
Theorem | 9cn 7783 | The number 9 is complex. (Contributed by David A. Wheeler, 8-Dec-2018.) |
⊢ 9 ∈ ℂ | ||
Theorem | 10re 7784 | The number 10 is real. (Contributed by NM, 5-Feb-2007.) |
⊢ 10 ∈ ℝ | ||
Theorem | 0le0 7785 | Zero is nonnegative. (Contributed by David A. Wheeler, 7-Jul-2016.) |
⊢ 0 ≤ 0 | ||
Theorem | 0le2 7786 | 0 is less than or equal to 2. (Contributed by David A. Wheeler, 7-Dec-2018.) |
⊢ 0 ≤ 2 | ||
Theorem | 2pos 7787 | The number 2 is positive. (Contributed by NM, 27-May-1999.) |
⊢ 0 < 2 | ||
Theorem | 2ne0 7788 | The number 2 is nonzero. (Contributed by NM, 9-Nov-2007.) |
⊢ 2 ≠ 0 | ||
Theorem | 2ap0 7789 | The number 2 is apart from zero. (Contributed by Jim Kingdon, 9-Mar-2020.) |
⊢ 2 # 0 | ||
Theorem | 3pos 7790 | The number 3 is positive. (Contributed by NM, 27-May-1999.) |
⊢ 0 < 3 | ||
Theorem | 3ne0 7791 | The number 3 is nonzero. (Contributed by FL, 17-Oct-2010.) (Proof shortened by Andrew Salmon, 7-May-2011.) |
⊢ 3 ≠ 0 | ||
Theorem | 4pos 7792 | The number 4 is positive. (Contributed by NM, 27-May-1999.) |
⊢ 0 < 4 | ||
Theorem | 4ne0 7793 | The number 4 is nonzero. (Contributed by David A. Wheeler, 5-Dec-2018.) |
⊢ 4 ≠ 0 | ||
Theorem | 5pos 7794 | The number 5 is positive. (Contributed by NM, 27-May-1999.) |
⊢ 0 < 5 | ||
Theorem | 6pos 7795 | The number 6 is positive. (Contributed by NM, 27-May-1999.) |
⊢ 0 < 6 | ||
Theorem | 7pos 7796 | The number 7 is positive. (Contributed by NM, 27-May-1999.) |
⊢ 0 < 7 | ||
Theorem | 8pos 7797 | The number 8 is positive. (Contributed by NM, 27-May-1999.) |
⊢ 0 < 8 | ||
Theorem | 9pos 7798 | The number 9 is positive. (Contributed by NM, 27-May-1999.) |
⊢ 0 < 9 | ||
Theorem | 10pos 7799 | The number 10 is positive. (Contributed by NM, 5-Feb-2007.) |
⊢ 0 < 10 | ||
This includes adding two pairs of values 1..10 (where the right is less than the left) and where the left is less than the right for the values 1..10. | ||
Theorem | neg1cn 7800 | -1 is a complex number (common case). (Contributed by David A. Wheeler, 7-Jul-2016.) |
⊢ -1 ∈ ℂ |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |