| Metamath
Proof Explorer Theorem List (p. 124 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 | nnneneg 12301 | No positive integer is equal to its negation. (Contributed by AV, 20-Jun-2023.) |
| ⊢ (𝐴 ∈ ℕ → 𝐴 ≠ -𝐴) | ||
| Theorem | 0nnn 12302 | Zero is not a positive integer. (Contributed by NM, 25-Aug-1999.) Remove dependency on ax-pre-mulgt0 11232. (Revised by Steven Nguyen, 30-Jan-2023.) |
| ⊢ ¬ 0 ∈ ℕ | ||
| Theorem | 0nnnALT 12303 | Alternate proof of 0nnn 12302, which requires ax-pre-mulgt0 11232 but is not based on nnne0 12300 (and which can therefore be used in nnne0ALT 12304). (Contributed by NM, 25-Aug-1999.) (New usage is discouraged.) (Proof modification is discouraged.) |
| ⊢ ¬ 0 ∈ ℕ | ||
| Theorem | nnne0ALT 12304 | Alternate version of nnne0 12300. A positive integer is nonzero. (Contributed by NM, 27-Sep-1999.) (New usage is discouraged.) (Proof modification is discouraged.) |
| ⊢ (𝐴 ∈ ℕ → 𝐴 ≠ 0) | ||
| Theorem | nngt0i 12305 | A positive integer is positive (inference version). (Contributed by NM, 17-Sep-1999.) |
| ⊢ 𝐴 ∈ ℕ ⇒ ⊢ 0 < 𝐴 | ||
| Theorem | nnne0i 12306 | A positive integer is nonzero (inference version). (Contributed by NM, 25-Aug-1999.) |
| ⊢ 𝐴 ∈ ℕ ⇒ ⊢ 𝐴 ≠ 0 | ||
| Theorem | nndivre 12307 | The quotient of a real and a positive integer is real. (Contributed by NM, 28-Nov-2008.) |
| ⊢ ((𝐴 ∈ ℝ ∧ 𝑁 ∈ ℕ) → (𝐴 / 𝑁) ∈ ℝ) | ||
| Theorem | nnrecre 12308 | The reciprocal of a positive integer is real. (Contributed by NM, 8-Feb-2008.) |
| ⊢ (𝑁 ∈ ℕ → (1 / 𝑁) ∈ ℝ) | ||
| Theorem | nnrecgt0 12309 | The reciprocal of a positive integer is positive. (Contributed by NM, 25-Aug-1999.) |
| ⊢ (𝐴 ∈ ℕ → 0 < (1 / 𝐴)) | ||
| Theorem | nnsub 12310 | Subtraction of positive integers. (Contributed by NM, 20-Aug-2001.) (Revised by Mario Carneiro, 16-May-2014.) |
| ⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) → (𝐴 < 𝐵 ↔ (𝐵 − 𝐴) ∈ ℕ)) | ||
| Theorem | nnsubi 12311 | Subtraction of positive integers. (Contributed by NM, 19-Aug-2001.) |
| ⊢ 𝐴 ∈ ℕ & ⊢ 𝐵 ∈ ℕ ⇒ ⊢ (𝐴 < 𝐵 ↔ (𝐵 − 𝐴) ∈ ℕ) | ||
| Theorem | nndiv 12312* | Two ways to express "𝐴 divides 𝐵 " for positive integers. (Contributed by NM, 3-Feb-2004.) (Proof shortened by Mario Carneiro, 16-May-2014.) |
| ⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) → (∃𝑥 ∈ ℕ (𝐴 · 𝑥) = 𝐵 ↔ (𝐵 / 𝐴) ∈ ℕ)) | ||
| Theorem | nndivtr 12313 | 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 12314 | A positive integer is one or greater. (Contributed by Mario Carneiro, 27-May-2016.) |
| ⊢ (𝜑 → 𝐴 ∈ ℕ) ⇒ ⊢ (𝜑 → 1 ≤ 𝐴) | ||
| Theorem | nngt0d 12315 | A positive integer is positive. (Contributed by Mario Carneiro, 27-May-2016.) |
| ⊢ (𝜑 → 𝐴 ∈ ℕ) ⇒ ⊢ (𝜑 → 0 < 𝐴) | ||
| Theorem | nnne0d 12316 | A positive integer is nonzero. (Contributed by Mario Carneiro, 27-May-2016.) |
| ⊢ (𝜑 → 𝐴 ∈ ℕ) ⇒ ⊢ (𝜑 → 𝐴 ≠ 0) | ||
| Theorem | nnrecred 12317 | The reciprocal of a positive integer is real. (Contributed by Mario Carneiro, 27-May-2016.) |
| ⊢ (𝜑 → 𝐴 ∈ ℕ) ⇒ ⊢ (𝜑 → (1 / 𝐴) ∈ ℝ) | ||
| Theorem | nnaddcld 12318 | Closure of addition of positive integers. (Contributed by Mario Carneiro, 27-May-2016.) |
| ⊢ (𝜑 → 𝐴 ∈ ℕ) & ⊢ (𝜑 → 𝐵 ∈ ℕ) ⇒ ⊢ (𝜑 → (𝐴 + 𝐵) ∈ ℕ) | ||
| Theorem | nnmulcld 12319 | Closure of multiplication of positive integers. (Contributed by Mario Carneiro, 27-May-2016.) |
| ⊢ (𝜑 → 𝐴 ∈ ℕ) & ⊢ (𝜑 → 𝐵 ∈ ℕ) ⇒ ⊢ (𝜑 → (𝐴 · 𝐵) ∈ ℕ) | ||
| Theorem | nndivred 12320 | 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 11162 through df-9 12336), 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 11162 and df-1 11163). With the decimal constructor df-dec 12734, it is possible to easily express larger integers in base 10. See deccl 12748 and the theorems that follow it. See also 4001prm 17182 (4001 is prime) and the proof of bpos 27337. Note that the decimal constructor builds on the definitions in this section. Note: The number 10 will be represented by its digits using the decimal constructor only, i.e., by ;10. Therefore, only decimal digits are needed (as symbols) for the decimal representation of a number. 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. Decimals can be expressed as ratios of integers, as in cos2bnd 16224. 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 12321 | Extend class notation to include the number 2. |
| class 2 | ||
| Syntax | c3 12322 | Extend class notation to include the number 3. |
| class 3 | ||
| Syntax | c4 12323 | Extend class notation to include the number 4. |
| class 4 | ||
| Syntax | c5 12324 | Extend class notation to include the number 5. |
| class 5 | ||
| Syntax | c6 12325 | Extend class notation to include the number 6. |
| class 6 | ||
| Syntax | c7 12326 | Extend class notation to include the number 7. |
| class 7 | ||
| Syntax | c8 12327 | Extend class notation to include the number 8. |
| class 8 | ||
| Syntax | c9 12328 | Extend class notation to include the number 9. |
| class 9 | ||
| Definition | df-2 12329 | Define the number 2. (Contributed by NM, 27-May-1999.) |
| ⊢ 2 = (1 + 1) | ||
| Definition | df-3 12330 | Define the number 3. (Contributed by NM, 27-May-1999.) |
| ⊢ 3 = (2 + 1) | ||
| Definition | df-4 12331 | Define the number 4. (Contributed by NM, 27-May-1999.) |
| ⊢ 4 = (3 + 1) | ||
| Definition | df-5 12332 | Define the number 5. (Contributed by NM, 27-May-1999.) |
| ⊢ 5 = (4 + 1) | ||
| Definition | df-6 12333 | Define the number 6. (Contributed by NM, 27-May-1999.) |
| ⊢ 6 = (5 + 1) | ||
| Definition | df-7 12334 | Define the number 7. (Contributed by NM, 27-May-1999.) |
| ⊢ 7 = (6 + 1) | ||
| Definition | df-8 12335 | Define the number 8. (Contributed by NM, 27-May-1999.) |
| ⊢ 8 = (7 + 1) | ||
| Definition | df-9 12336 | Define the number 9. (Contributed by NM, 27-May-1999.) |
| ⊢ 9 = (8 + 1) | ||
| Theorem | 0ne1 12337 | Zero is different from one (the commuted form is Axiom ax-1ne0 11224). (Contributed by David A. Wheeler, 8-Dec-2018.) |
| ⊢ 0 ≠ 1 | ||
| Theorem | 1m1e0 12338 | One minus one equals zero. (Contributed by David A. Wheeler, 7-Jul-2016.) |
| ⊢ (1 − 1) = 0 | ||
| Theorem | 2nn 12339 | 2 is a positive integer. (Contributed by NM, 20-Aug-2001.) |
| ⊢ 2 ∈ ℕ | ||
| Theorem | 2re 12340 | The number 2 is real. (Contributed by NM, 27-May-1999.) |
| ⊢ 2 ∈ ℝ | ||
| Theorem | 2cn 12341 | The number 2 is a complex number. (Contributed by NM, 30-Jul-2004.) Reduce dependencies on axioms. (Revised by Steven Nguyen, 4-Oct-2022.) |
| ⊢ 2 ∈ ℂ | ||
| Theorem | 2cnALT 12342 | Alternate proof of 2cn 12341. Shorter but uses more axioms. Similar proofs are possible for 3cn 12347, ... , 9cn 12366. (Contributed by NM, 30-Jul-2004.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ 2 ∈ ℂ | ||
| Theorem | 2ex 12343 | The number 2 is a set. (Contributed by David A. Wheeler, 8-Dec-2018.) |
| ⊢ 2 ∈ V | ||
| Theorem | 2cnd 12344 | The number 2 is a complex number, deduction form. (Contributed by David A. Wheeler, 8-Dec-2018.) |
| ⊢ (𝜑 → 2 ∈ ℂ) | ||
| Theorem | 3nn 12345 | 3 is a positive integer. (Contributed by NM, 8-Jan-2006.) |
| ⊢ 3 ∈ ℕ | ||
| Theorem | 3re 12346 | The number 3 is real. (Contributed by NM, 27-May-1999.) |
| ⊢ 3 ∈ ℝ | ||
| Theorem | 3cn 12347 | The number 3 is a complex number. (Contributed by FL, 17-Oct-2010.) Reduce dependencies on axioms. (Revised by Steven Nguyen, 4-Oct-2022.) |
| ⊢ 3 ∈ ℂ | ||
| Theorem | 3ex 12348 | The number 3 is a set. (Contributed by David A. Wheeler, 8-Dec-2018.) |
| ⊢ 3 ∈ V | ||
| Theorem | 4nn 12349 | 4 is a positive integer. (Contributed by NM, 8-Jan-2006.) |
| ⊢ 4 ∈ ℕ | ||
| Theorem | 4re 12350 | The number 4 is real. (Contributed by NM, 27-May-1999.) |
| ⊢ 4 ∈ ℝ | ||
| Theorem | 4cn 12351 | The number 4 is a complex number. (Contributed by David A. Wheeler, 7-Jul-2016.) Reduce dependencies on axioms. (Revised by Steven Nguyen, 4-Oct-2022.) |
| ⊢ 4 ∈ ℂ | ||
| Theorem | 5nn 12352 | 5 is a positive integer. (Contributed by Mario Carneiro, 15-Sep-2013.) |
| ⊢ 5 ∈ ℕ | ||
| Theorem | 5re 12353 | The number 5 is real. (Contributed by NM, 27-May-1999.) |
| ⊢ 5 ∈ ℝ | ||
| Theorem | 5cn 12354 | The number 5 is a complex number. (Contributed by David A. Wheeler, 8-Dec-2018.) Reduce dependencies on axioms. (Revised by Steven Nguyen, 4-Oct-2022.) |
| ⊢ 5 ∈ ℂ | ||
| Theorem | 6nn 12355 | 6 is a positive integer. (Contributed by Mario Carneiro, 15-Sep-2013.) |
| ⊢ 6 ∈ ℕ | ||
| Theorem | 6re 12356 | The number 6 is real. (Contributed by NM, 27-May-1999.) |
| ⊢ 6 ∈ ℝ | ||
| Theorem | 6cn 12357 | The number 6 is a complex number. (Contributed by David A. Wheeler, 8-Dec-2018.) Reduce dependencies on axioms. (Revised by Steven Nguyen, 4-Oct-2022.) |
| ⊢ 6 ∈ ℂ | ||
| Theorem | 7nn 12358 | 7 is a positive integer. (Contributed by Mario Carneiro, 15-Sep-2013.) |
| ⊢ 7 ∈ ℕ | ||
| Theorem | 7re 12359 | The number 7 is real. (Contributed by NM, 27-May-1999.) |
| ⊢ 7 ∈ ℝ | ||
| Theorem | 7cn 12360 | The number 7 is a complex number. (Contributed by David A. Wheeler, 8-Dec-2018.) Reduce dependencies on axioms. (Revised by Steven Nguyen, 4-Oct-2022.) |
| ⊢ 7 ∈ ℂ | ||
| Theorem | 8nn 12361 | 8 is a positive integer. (Contributed by Mario Carneiro, 15-Sep-2013.) |
| ⊢ 8 ∈ ℕ | ||
| Theorem | 8re 12362 | The number 8 is real. (Contributed by NM, 27-May-1999.) |
| ⊢ 8 ∈ ℝ | ||
| Theorem | 8cn 12363 | The number 8 is a complex number. (Contributed by David A. Wheeler, 8-Dec-2018.) Reduce dependencies on axioms. (Revised by Steven Nguyen, 4-Oct-2022.) |
| ⊢ 8 ∈ ℂ | ||
| Theorem | 9nn 12364 | 9 is a positive integer. (Contributed by NM, 21-Oct-2012.) |
| ⊢ 9 ∈ ℕ | ||
| Theorem | 9re 12365 | The number 9 is real. (Contributed by NM, 27-May-1999.) |
| ⊢ 9 ∈ ℝ | ||
| Theorem | 9cn 12366 | The number 9 is a complex number. (Contributed by David A. Wheeler, 8-Dec-2018.) Reduce dependencies on axioms. (Revised by Steven Nguyen, 4-Oct-2022.) |
| ⊢ 9 ∈ ℂ | ||
| Theorem | 0le0 12367 | Zero is nonnegative. (Contributed by David A. Wheeler, 7-Jul-2016.) |
| ⊢ 0 ≤ 0 | ||
| Theorem | 0le2 12368 | The number 0 is less than or equal to 2. (Contributed by David A. Wheeler, 7-Dec-2018.) |
| ⊢ 0 ≤ 2 | ||
| Theorem | 2pos 12369 | The number 2 is positive. (Contributed by NM, 27-May-1999.) |
| ⊢ 0 < 2 | ||
| Theorem | 2ne0 12370 | The number 2 is nonzero. (Contributed by NM, 9-Nov-2007.) |
| ⊢ 2 ≠ 0 | ||
| Theorem | 3pos 12371 | The number 3 is positive. (Contributed by NM, 27-May-1999.) |
| ⊢ 0 < 3 | ||
| Theorem | 3ne0 12372 | The number 3 is nonzero. (Contributed by FL, 17-Oct-2010.) (Proof shortened by Andrew Salmon, 7-May-2011.) |
| ⊢ 3 ≠ 0 | ||
| Theorem | 4pos 12373 | The number 4 is positive. (Contributed by NM, 27-May-1999.) |
| ⊢ 0 < 4 | ||
| Theorem | 4ne0 12374 | The number 4 is nonzero. (Contributed by David A. Wheeler, 5-Dec-2018.) |
| ⊢ 4 ≠ 0 | ||
| Theorem | 5pos 12375 | The number 5 is positive. (Contributed by NM, 27-May-1999.) |
| ⊢ 0 < 5 | ||
| Theorem | 6pos 12376 | The number 6 is positive. (Contributed by NM, 27-May-1999.) |
| ⊢ 0 < 6 | ||
| Theorem | 7pos 12377 | The number 7 is positive. (Contributed by NM, 27-May-1999.) |
| ⊢ 0 < 7 | ||
| Theorem | 8pos 12378 | The number 8 is positive. (Contributed by NM, 27-May-1999.) |
| ⊢ 0 < 8 | ||
| Theorem | 9pos 12379 | The number 9 is positive. (Contributed by NM, 27-May-1999.) |
| ⊢ 0 < 9 | ||
This section includes specific theorems about one-digit natural numbers (membership, addition, subtraction, multiplication, division, ordering). | ||
| Theorem | neg1cn 12380 | -1 is a complex number. (Contributed by David A. Wheeler, 7-Jul-2016.) |
| ⊢ -1 ∈ ℂ | ||
| Theorem | neg1rr 12381 | -1 is a real number. (Contributed by David A. Wheeler, 5-Dec-2018.) |
| ⊢ -1 ∈ ℝ | ||
| Theorem | neg1ne0 12382 | -1 is nonzero. (Contributed by David A. Wheeler, 8-Dec-2018.) |
| ⊢ -1 ≠ 0 | ||
| Theorem | neg1lt0 12383 | -1 is less than 0. (Contributed by David A. Wheeler, 8-Dec-2018.) |
| ⊢ -1 < 0 | ||
| Theorem | negneg1e1 12384 | --1 is 1. (Contributed by David A. Wheeler, 8-Dec-2018.) |
| ⊢ --1 = 1 | ||
| Theorem | 1pneg1e0 12385 | 1 + -1 is 0. (Contributed by David A. Wheeler, 8-Dec-2018.) |
| ⊢ (1 + -1) = 0 | ||
| Theorem | 0m0e0 12386 | 0 minus 0 equals 0. (Contributed by David A. Wheeler, 8-Dec-2018.) |
| ⊢ (0 − 0) = 0 | ||
| Theorem | 1m0e1 12387 | 1 - 0 = 1. (Contributed by David A. Wheeler, 8-Dec-2018.) |
| ⊢ (1 − 0) = 1 | ||
| Theorem | 0p1e1 12388 | 0 + 1 = 1. (Contributed by David A. Wheeler, 7-Jul-2016.) |
| ⊢ (0 + 1) = 1 | ||
| Theorem | fv0p1e1 12389 | 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 12390 | 1 + 0 = 1. (Contributed by David A. Wheeler, 8-Dec-2018.) |
| ⊢ (1 + 0) = 1 | ||
| Theorem | 1p1e2 12391 | 1 + 1 = 2. (Contributed by NM, 1-Apr-2008.) |
| ⊢ (1 + 1) = 2 | ||
| Theorem | 2m1e1 12392 | 2 - 1 = 1. The result is on the right-hand-side to be consistent with similar proofs like 4p4e8 12421. (Contributed by David A. Wheeler, 4-Jan-2017.) |
| ⊢ (2 − 1) = 1 | ||
| Theorem | 1e2m1 12393 | 1 = 2 - 1. (Contributed by David A. Wheeler, 8-Dec-2018.) |
| ⊢ 1 = (2 − 1) | ||
| Theorem | 3m1e2 12394 | 3 - 1 = 2. (Contributed by FL, 17-Oct-2010.) (Revised by NM, 10-Dec-2017.) (Proof shortened by AV, 6-Sep-2021.) |
| ⊢ (3 − 1) = 2 | ||
| Theorem | 4m1e3 12395 | 4 - 1 = 3. (Contributed by AV, 8-Feb-2021.) (Proof shortened by AV, 6-Sep-2021.) |
| ⊢ (4 − 1) = 3 | ||
| Theorem | 5m1e4 12396 | 5 - 1 = 4. (Contributed by AV, 6-Sep-2021.) |
| ⊢ (5 − 1) = 4 | ||
| Theorem | 6m1e5 12397 | 6 - 1 = 5. (Contributed by AV, 6-Sep-2021.) |
| ⊢ (6 − 1) = 5 | ||
| Theorem | 7m1e6 12398 | 7 - 1 = 6. (Contributed by AV, 6-Sep-2021.) |
| ⊢ (7 − 1) = 6 | ||
| Theorem | 8m1e7 12399 | 8 - 1 = 7. (Contributed by AV, 6-Sep-2021.) |
| ⊢ (8 − 1) = 7 | ||
| Theorem | 9m1e8 12400 | 9 - 1 = 8. (Contributed by AV, 6-Sep-2021.) |
| ⊢ (9 − 1) = 8 | ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |