![]() |
Intuitionistic Logic Explorer Theorem List (p. 87 of 129) | < 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 | nnge1 8601 | A positive integer is one or greater. (Contributed by NM, 25-Aug-1999.) |
⊢ (𝐴 ∈ ℕ → 1 ≤ 𝐴) | ||
Theorem | nnle1eq1 8602 | A positive integer is less than or equal to one iff it is equal to one. (Contributed by NM, 3-Apr-2005.) |
⊢ (𝐴 ∈ ℕ → (𝐴 ≤ 1 ↔ 𝐴 = 1)) | ||
Theorem | nngt0 8603 | A positive integer is positive. (Contributed by NM, 26-Sep-1999.) |
⊢ (𝐴 ∈ ℕ → 0 < 𝐴) | ||
Theorem | nnnlt1 8604 | A positive integer is not less than one. (Contributed by NM, 18-Jan-2004.) (Revised by Mario Carneiro, 27-May-2016.) |
⊢ (𝐴 ∈ ℕ → ¬ 𝐴 < 1) | ||
Theorem | 0nnn 8605 | Zero is not a positive integer. (Contributed by NM, 25-Aug-1999.) |
⊢ ¬ 0 ∈ ℕ | ||
Theorem | nnne0 8606 | A positive integer is nonzero. (Contributed by NM, 27-Sep-1999.) |
⊢ (𝐴 ∈ ℕ → 𝐴 ≠ 0) | ||
Theorem | nnap0 8607 | A positive integer is apart from zero. (Contributed by Jim Kingdon, 8-Mar-2020.) |
⊢ (𝐴 ∈ ℕ → 𝐴 # 0) | ||
Theorem | nngt0i 8608 | A positive integer is positive (inference version). (Contributed by NM, 17-Sep-1999.) |
⊢ 𝐴 ∈ ℕ ⇒ ⊢ 0 < 𝐴 | ||
Theorem | nnap0i 8609 | A positive integer is apart from zero (inference version). (Contributed by Jim Kingdon, 1-Jan-2023.) |
⊢ 𝐴 ∈ ℕ ⇒ ⊢ 𝐴 # 0 | ||
Theorem | nnne0i 8610 | A positive integer is nonzero (inference version). (Contributed by NM, 25-Aug-1999.) |
⊢ 𝐴 ∈ ℕ ⇒ ⊢ 𝐴 ≠ 0 | ||
Theorem | nn2ge 8611* | There exists a positive integer greater than or equal to any two others. (Contributed by NM, 18-Aug-1999.) |
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) → ∃𝑥 ∈ ℕ (𝐴 ≤ 𝑥 ∧ 𝐵 ≤ 𝑥)) | ||
Theorem | nn1gt1 8612 | A positive integer is either one or greater than one. This is for ℕ; 0elnn 4470 is a similar theorem for ω (the natural numbers as ordinals). (Contributed by Jim Kingdon, 7-Mar-2020.) |
⊢ (𝐴 ∈ ℕ → (𝐴 = 1 ∨ 1 < 𝐴)) | ||
Theorem | nngt1ne1 8613 | A positive integer is greater than one iff it is not equal to one. (Contributed by NM, 7-Oct-2004.) |
⊢ (𝐴 ∈ ℕ → (1 < 𝐴 ↔ 𝐴 ≠ 1)) | ||
Theorem | nndivre 8614 | The quotient of a real and a positive integer is real. (Contributed by NM, 28-Nov-2008.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝑁 ∈ ℕ) → (𝐴 / 𝑁) ∈ ℝ) | ||
Theorem | nnrecre 8615 | The reciprocal of a positive integer is real. (Contributed by NM, 8-Feb-2008.) |
⊢ (𝑁 ∈ ℕ → (1 / 𝑁) ∈ ℝ) | ||
Theorem | nnrecgt0 8616 | The reciprocal of a positive integer is positive. (Contributed by NM, 25-Aug-1999.) |
⊢ (𝐴 ∈ ℕ → 0 < (1 / 𝐴)) | ||
Theorem | nnsub 8617 | Subtraction of positive integers. (Contributed by NM, 20-Aug-2001.) (Revised by Mario Carneiro, 16-May-2014.) |
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) → (𝐴 < 𝐵 ↔ (𝐵 − 𝐴) ∈ ℕ)) | ||
Theorem | nnsubi 8618 | Subtraction of positive integers. (Contributed by NM, 19-Aug-2001.) |
⊢ 𝐴 ∈ ℕ & ⊢ 𝐵 ∈ ℕ ⇒ ⊢ (𝐴 < 𝐵 ↔ (𝐵 − 𝐴) ∈ ℕ) | ||
Theorem | nndiv 8619* | Two ways to express "𝐴 divides 𝐵 " for positive integers. (Contributed by NM, 3-Feb-2004.) (Proof shortened by Mario Carneiro, 16-May-2014.) |
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) → (∃𝑥 ∈ ℕ (𝐴 · 𝑥) = 𝐵 ↔ (𝐵 / 𝐴) ∈ ℕ)) | ||
Theorem | nndivtr 8620 | Transitive property of divisibility: if 𝐴 divides 𝐵 and 𝐵 divides 𝐶, then 𝐴 divides 𝐶. Typically, 𝐶 would be an integer, although the theorem holds for complex 𝐶. (Contributed by NM, 3-May-2005.) |
⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℂ) ∧ ((𝐵 / 𝐴) ∈ ℕ ∧ (𝐶 / 𝐵) ∈ ℕ)) → (𝐶 / 𝐴) ∈ ℕ) | ||
Theorem | nnge1d 8621 | A positive integer is one or greater. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℕ) ⇒ ⊢ (𝜑 → 1 ≤ 𝐴) | ||
Theorem | nngt0d 8622 | A positive integer is positive. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℕ) ⇒ ⊢ (𝜑 → 0 < 𝐴) | ||
Theorem | nnne0d 8623 | A positive integer is nonzero. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℕ) ⇒ ⊢ (𝜑 → 𝐴 ≠ 0) | ||
Theorem | nnap0d 8624 | A positive integer is apart from zero. (Contributed by Jim Kingdon, 25-Aug-2021.) |
⊢ (𝜑 → 𝐴 ∈ ℕ) ⇒ ⊢ (𝜑 → 𝐴 # 0) | ||
Theorem | nnrecred 8625 | The reciprocal of a positive integer is real. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℕ) ⇒ ⊢ (𝜑 → (1 / 𝐴) ∈ ℝ) | ||
Theorem | nnaddcld 8626 | Closure of addition of positive integers. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℕ) & ⊢ (𝜑 → 𝐵 ∈ ℕ) ⇒ ⊢ (𝜑 → (𝐴 + 𝐵) ∈ ℕ) | ||
Theorem | nnmulcld 8627 | Closure of multiplication of positive integers. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℕ) & ⊢ (𝜑 → 𝐵 ∈ ℕ) ⇒ ⊢ (𝜑 → (𝐴 · 𝐵) ∈ ℕ) | ||
Theorem | nndivred 8628 | A positive integer is one or greater. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℕ) ⇒ ⊢ (𝜑 → (𝐴 / 𝐵) ∈ ℝ) | ||
The decimal representation of numbers/integers is based on the decimal digits 0 through 9 (df-0 7507 through df-9 8644), which are explicitly defined in the following. Note that the numbers 0 and 1 are constants defined as primitives of the complex number axiom system (see df-0 7507 and df-1 7508). Integers can also be exhibited as sums of powers of 10 (e.g. the number 103 can be expressed as ((;10↑2) + 3)) or as some other expression built from operations on the numbers 0 through 9. For example, the prime number 823541 can be expressed as (7↑7) − 2. 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 8629 | Extend class notation to include the number 2. |
class 2 | ||
Syntax | c3 8630 | Extend class notation to include the number 3. |
class 3 | ||
Syntax | c4 8631 | Extend class notation to include the number 4. |
class 4 | ||
Syntax | c5 8632 | Extend class notation to include the number 5. |
class 5 | ||
Syntax | c6 8633 | Extend class notation to include the number 6. |
class 6 | ||
Syntax | c7 8634 | Extend class notation to include the number 7. |
class 7 | ||
Syntax | c8 8635 | Extend class notation to include the number 8. |
class 8 | ||
Syntax | c9 8636 | Extend class notation to include the number 9. |
class 9 | ||
Definition | df-2 8637 | Define the number 2. (Contributed by NM, 27-May-1999.) |
⊢ 2 = (1 + 1) | ||
Definition | df-3 8638 | Define the number 3. (Contributed by NM, 27-May-1999.) |
⊢ 3 = (2 + 1) | ||
Definition | df-4 8639 | Define the number 4. (Contributed by NM, 27-May-1999.) |
⊢ 4 = (3 + 1) | ||
Definition | df-5 8640 | Define the number 5. (Contributed by NM, 27-May-1999.) |
⊢ 5 = (4 + 1) | ||
Definition | df-6 8641 | Define the number 6. (Contributed by NM, 27-May-1999.) |
⊢ 6 = (5 + 1) | ||
Definition | df-7 8642 | Define the number 7. (Contributed by NM, 27-May-1999.) |
⊢ 7 = (6 + 1) | ||
Definition | df-8 8643 | Define the number 8. (Contributed by NM, 27-May-1999.) |
⊢ 8 = (7 + 1) | ||
Definition | df-9 8644 | Define the number 9. (Contributed by NM, 27-May-1999.) |
⊢ 9 = (8 + 1) | ||
Theorem | 0ne1 8645 | 0 ≠ 1 (common case). See aso 1ap0 8218. (Contributed by David A. Wheeler, 8-Dec-2018.) |
⊢ 0 ≠ 1 | ||
Theorem | 1ne0 8646 | 1 ≠ 0. See aso 1ap0 8218. (Contributed by Jim Kingdon, 9-Mar-2020.) |
⊢ 1 ≠ 0 | ||
Theorem | 1m1e0 8647 | (1 − 1) = 0 (common case). (Contributed by David A. Wheeler, 7-Jul-2016.) |
⊢ (1 − 1) = 0 | ||
Theorem | 2re 8648 | The number 2 is real. (Contributed by NM, 27-May-1999.) |
⊢ 2 ∈ ℝ | ||
Theorem | 2cn 8649 | The number 2 is a complex number. (Contributed by NM, 30-Jul-2004.) |
⊢ 2 ∈ ℂ | ||
Theorem | 2ex 8650 | 2 is a set (common case). (Contributed by David A. Wheeler, 8-Dec-2018.) |
⊢ 2 ∈ V | ||
Theorem | 2cnd 8651 | 2 is a complex number, deductive form (common case). (Contributed by David A. Wheeler, 8-Dec-2018.) |
⊢ (𝜑 → 2 ∈ ℂ) | ||
Theorem | 3re 8652 | The number 3 is real. (Contributed by NM, 27-May-1999.) |
⊢ 3 ∈ ℝ | ||
Theorem | 3cn 8653 | The number 3 is a complex number. (Contributed by FL, 17-Oct-2010.) |
⊢ 3 ∈ ℂ | ||
Theorem | 3ex 8654 | 3 is a set (common case). (Contributed by David A. Wheeler, 8-Dec-2018.) |
⊢ 3 ∈ V | ||
Theorem | 4re 8655 | The number 4 is real. (Contributed by NM, 27-May-1999.) |
⊢ 4 ∈ ℝ | ||
Theorem | 4cn 8656 | The number 4 is a complex number. (Contributed by David A. Wheeler, 7-Jul-2016.) |
⊢ 4 ∈ ℂ | ||
Theorem | 5re 8657 | The number 5 is real. (Contributed by NM, 27-May-1999.) |
⊢ 5 ∈ ℝ | ||
Theorem | 5cn 8658 | The number 5 is complex. (Contributed by David A. Wheeler, 8-Dec-2018.) |
⊢ 5 ∈ ℂ | ||
Theorem | 6re 8659 | The number 6 is real. (Contributed by NM, 27-May-1999.) |
⊢ 6 ∈ ℝ | ||
Theorem | 6cn 8660 | The number 6 is complex. (Contributed by David A. Wheeler, 8-Dec-2018.) |
⊢ 6 ∈ ℂ | ||
Theorem | 7re 8661 | The number 7 is real. (Contributed by NM, 27-May-1999.) |
⊢ 7 ∈ ℝ | ||
Theorem | 7cn 8662 | The number 7 is complex. (Contributed by David A. Wheeler, 8-Dec-2018.) |
⊢ 7 ∈ ℂ | ||
Theorem | 8re 8663 | The number 8 is real. (Contributed by NM, 27-May-1999.) |
⊢ 8 ∈ ℝ | ||
Theorem | 8cn 8664 | The number 8 is complex. (Contributed by David A. Wheeler, 8-Dec-2018.) |
⊢ 8 ∈ ℂ | ||
Theorem | 9re 8665 | The number 9 is real. (Contributed by NM, 27-May-1999.) |
⊢ 9 ∈ ℝ | ||
Theorem | 9cn 8666 | The number 9 is complex. (Contributed by David A. Wheeler, 8-Dec-2018.) |
⊢ 9 ∈ ℂ | ||
Theorem | 0le0 8667 | Zero is nonnegative. (Contributed by David A. Wheeler, 7-Jul-2016.) |
⊢ 0 ≤ 0 | ||
Theorem | 0le2 8668 | 0 is less than or equal to 2. (Contributed by David A. Wheeler, 7-Dec-2018.) |
⊢ 0 ≤ 2 | ||
Theorem | 2pos 8669 | The number 2 is positive. (Contributed by NM, 27-May-1999.) |
⊢ 0 < 2 | ||
Theorem | 2ne0 8670 | The number 2 is nonzero. (Contributed by NM, 9-Nov-2007.) |
⊢ 2 ≠ 0 | ||
Theorem | 2ap0 8671 | The number 2 is apart from zero. (Contributed by Jim Kingdon, 9-Mar-2020.) |
⊢ 2 # 0 | ||
Theorem | 3pos 8672 | The number 3 is positive. (Contributed by NM, 27-May-1999.) |
⊢ 0 < 3 | ||
Theorem | 3ne0 8673 | The number 3 is nonzero. (Contributed by FL, 17-Oct-2010.) (Proof shortened by Andrew Salmon, 7-May-2011.) |
⊢ 3 ≠ 0 | ||
Theorem | 3ap0 8674 | The number 3 is apart from zero. (Contributed by Jim Kingdon, 10-Oct-2021.) |
⊢ 3 # 0 | ||
Theorem | 4pos 8675 | The number 4 is positive. (Contributed by NM, 27-May-1999.) |
⊢ 0 < 4 | ||
Theorem | 4ne0 8676 | The number 4 is nonzero. (Contributed by David A. Wheeler, 5-Dec-2018.) |
⊢ 4 ≠ 0 | ||
Theorem | 4ap0 8677 | The number 4 is apart from zero. (Contributed by Jim Kingdon, 10-Oct-2021.) |
⊢ 4 # 0 | ||
Theorem | 5pos 8678 | The number 5 is positive. (Contributed by NM, 27-May-1999.) |
⊢ 0 < 5 | ||
Theorem | 6pos 8679 | The number 6 is positive. (Contributed by NM, 27-May-1999.) |
⊢ 0 < 6 | ||
Theorem | 7pos 8680 | The number 7 is positive. (Contributed by NM, 27-May-1999.) |
⊢ 0 < 7 | ||
Theorem | 8pos 8681 | The number 8 is positive. (Contributed by NM, 27-May-1999.) |
⊢ 0 < 8 | ||
Theorem | 9pos 8682 | The number 9 is positive. (Contributed by NM, 27-May-1999.) |
⊢ 0 < 9 | ||
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 8683 | -1 is a complex number (common case). (Contributed by David A. Wheeler, 7-Jul-2016.) |
⊢ -1 ∈ ℂ | ||
Theorem | neg1rr 8684 | -1 is a real number (common case). (Contributed by David A. Wheeler, 5-Dec-2018.) |
⊢ -1 ∈ ℝ | ||
Theorem | neg1ne0 8685 | -1 is nonzero (common case). (Contributed by David A. Wheeler, 8-Dec-2018.) |
⊢ -1 ≠ 0 | ||
Theorem | neg1lt0 8686 | -1 is less than 0 (common case). (Contributed by David A. Wheeler, 8-Dec-2018.) |
⊢ -1 < 0 | ||
Theorem | neg1ap0 8687 | -1 is apart from zero. (Contributed by Jim Kingdon, 9-Jun-2020.) |
⊢ -1 # 0 | ||
Theorem | negneg1e1 8688 | --1 is 1 (common case). (Contributed by David A. Wheeler, 8-Dec-2018.) |
⊢ --1 = 1 | ||
Theorem | 1pneg1e0 8689 | 1 + -1 is 0 (common case). (Contributed by David A. Wheeler, 8-Dec-2018.) |
⊢ (1 + -1) = 0 | ||
Theorem | 0m0e0 8690 | 0 minus 0 equals 0 (common case). (Contributed by David A. Wheeler, 8-Dec-2018.) |
⊢ (0 − 0) = 0 | ||
Theorem | 1m0e1 8691 | 1 - 0 = 1 (common case). (Contributed by David A. Wheeler, 8-Dec-2018.) |
⊢ (1 − 0) = 1 | ||
Theorem | 0p1e1 8692 | 0 + 1 = 1. (Contributed by David A. Wheeler, 7-Jul-2016.) |
⊢ (0 + 1) = 1 | ||
Theorem | fv0p1e1 8693 | Function value at 𝑁 + 1 with 𝑁 replaced by 0. Technical theorem to be used to reduce the size of a significant number of proofs. (Contributed by AV, 13-Aug-2022.) |
⊢ (𝑁 = 0 → (𝐹‘(𝑁 + 1)) = (𝐹‘1)) | ||
Theorem | 1p0e1 8694 | 1 + 0 = 1. (Contributed by David A. Wheeler, 8-Dec-2018.) |
⊢ (1 + 0) = 1 | ||
Theorem | 1p1e2 8695 | 1 + 1 = 2. (Contributed by NM, 1-Apr-2008.) |
⊢ (1 + 1) = 2 | ||
Theorem | 2m1e1 8696 | 2 - 1 = 1. The result is on the right-hand-side to be consistent with similar proofs like 4p4e8 8717. (Contributed by David A. Wheeler, 4-Jan-2017.) |
⊢ (2 − 1) = 1 | ||
Theorem | 1e2m1 8697 | 1 = 2 - 1 (common case). (Contributed by David A. Wheeler, 8-Dec-2018.) |
⊢ 1 = (2 − 1) | ||
Theorem | 3m1e2 8698 | 3 - 1 = 2. (Contributed by FL, 17-Oct-2010.) (Revised by NM, 10-Dec-2017.) |
⊢ (3 − 1) = 2 | ||
Theorem | 2p2e4 8699 | Two plus two equals four. For more information, see "2+2=4 Trivia" on the Metamath Proof Explorer Home Page: https://us.metamath.org/mpeuni/mmset.html#trivia. (Contributed by NM, 27-May-1999.) |
⊢ (2 + 2) = 4 | ||
Theorem | 2times 8700 | Two times a number. (Contributed by NM, 10-Oct-2004.) (Revised by Mario Carneiro, 27-May-2016.) (Proof shortened by AV, 26-Feb-2020.) |
⊢ (𝐴 ∈ ℂ → (2 · 𝐴) = (𝐴 + 𝐴)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |