![]() |
Metamath
Proof Explorer Theorem List (p. 124 of 491) | < 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-30946) |
![]() (30947-32469) |
![]() (32470-49035) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | nnne0ALT 12301 | Alternate version of nnne0 12297. A positive integer is nonzero. (Contributed by NM, 27-Sep-1999.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ (𝐴 ∈ ℕ → 𝐴 ≠ 0) | ||
Theorem | nngt0i 12302 | A positive integer is positive (inference version). (Contributed by NM, 17-Sep-1999.) |
⊢ 𝐴 ∈ ℕ ⇒ ⊢ 0 < 𝐴 | ||
Theorem | nnne0i 12303 | A positive integer is nonzero (inference version). (Contributed by NM, 25-Aug-1999.) |
⊢ 𝐴 ∈ ℕ ⇒ ⊢ 𝐴 ≠ 0 | ||
Theorem | nndivre 12304 | The quotient of a real and a positive integer is real. (Contributed by NM, 28-Nov-2008.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝑁 ∈ ℕ) → (𝐴 / 𝑁) ∈ ℝ) | ||
Theorem | nnrecre 12305 | The reciprocal of a positive integer is real. (Contributed by NM, 8-Feb-2008.) |
⊢ (𝑁 ∈ ℕ → (1 / 𝑁) ∈ ℝ) | ||
Theorem | nnrecgt0 12306 | The reciprocal of a positive integer is positive. (Contributed by NM, 25-Aug-1999.) |
⊢ (𝐴 ∈ ℕ → 0 < (1 / 𝐴)) | ||
Theorem | nnsub 12307 | Subtraction of positive integers. (Contributed by NM, 20-Aug-2001.) (Revised by Mario Carneiro, 16-May-2014.) |
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) → (𝐴 < 𝐵 ↔ (𝐵 − 𝐴) ∈ ℕ)) | ||
Theorem | nnsubi 12308 | Subtraction of positive integers. (Contributed by NM, 19-Aug-2001.) |
⊢ 𝐴 ∈ ℕ & ⊢ 𝐵 ∈ ℕ ⇒ ⊢ (𝐴 < 𝐵 ↔ (𝐵 − 𝐴) ∈ ℕ) | ||
Theorem | nndiv 12309* | Two ways to express "𝐴 divides 𝐵 " for positive integers. (Contributed by NM, 3-Feb-2004.) (Proof shortened by Mario Carneiro, 16-May-2014.) |
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) → (∃𝑥 ∈ ℕ (𝐴 · 𝑥) = 𝐵 ↔ (𝐵 / 𝐴) ∈ ℕ)) | ||
Theorem | nndivtr 12310 | 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 12311 | A positive integer is one or greater. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℕ) ⇒ ⊢ (𝜑 → 1 ≤ 𝐴) | ||
Theorem | nngt0d 12312 | A positive integer is positive. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℕ) ⇒ ⊢ (𝜑 → 0 < 𝐴) | ||
Theorem | nnne0d 12313 | A positive integer is nonzero. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℕ) ⇒ ⊢ (𝜑 → 𝐴 ≠ 0) | ||
Theorem | nnrecred 12314 | The reciprocal of a positive integer is real. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℕ) ⇒ ⊢ (𝜑 → (1 / 𝐴) ∈ ℝ) | ||
Theorem | nnaddcld 12315 | Closure of addition of positive integers. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℕ) & ⊢ (𝜑 → 𝐵 ∈ ℕ) ⇒ ⊢ (𝜑 → (𝐴 + 𝐵) ∈ ℕ) | ||
Theorem | nnmulcld 12316 | Closure of multiplication of positive integers. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℕ) & ⊢ (𝜑 → 𝐵 ∈ ℕ) ⇒ ⊢ (𝜑 → (𝐴 · 𝐵) ∈ ℕ) | ||
Theorem | nndivred 12317 | 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 11159 through df-9 12333), 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 11159 and df-1 11160). With the decimal constructor df-dec 12731, it is possible to easily express larger integers in base 10. See deccl 12745 and the theorems that follow it. See also 4001prm 17178 (4001 is prime) and the proof of bpos 27351. 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 16220. 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 12318 | Extend class notation to include the number 2. |
class 2 | ||
Syntax | c3 12319 | Extend class notation to include the number 3. |
class 3 | ||
Syntax | c4 12320 | Extend class notation to include the number 4. |
class 4 | ||
Syntax | c5 12321 | Extend class notation to include the number 5. |
class 5 | ||
Syntax | c6 12322 | Extend class notation to include the number 6. |
class 6 | ||
Syntax | c7 12323 | Extend class notation to include the number 7. |
class 7 | ||
Syntax | c8 12324 | Extend class notation to include the number 8. |
class 8 | ||
Syntax | c9 12325 | Extend class notation to include the number 9. |
class 9 | ||
Definition | df-2 12326 | Define the number 2. (Contributed by NM, 27-May-1999.) |
⊢ 2 = (1 + 1) | ||
Definition | df-3 12327 | Define the number 3. (Contributed by NM, 27-May-1999.) |
⊢ 3 = (2 + 1) | ||
Definition | df-4 12328 | Define the number 4. (Contributed by NM, 27-May-1999.) |
⊢ 4 = (3 + 1) | ||
Definition | df-5 12329 | Define the number 5. (Contributed by NM, 27-May-1999.) |
⊢ 5 = (4 + 1) | ||
Definition | df-6 12330 | Define the number 6. (Contributed by NM, 27-May-1999.) |
⊢ 6 = (5 + 1) | ||
Definition | df-7 12331 | Define the number 7. (Contributed by NM, 27-May-1999.) |
⊢ 7 = (6 + 1) | ||
Definition | df-8 12332 | Define the number 8. (Contributed by NM, 27-May-1999.) |
⊢ 8 = (7 + 1) | ||
Definition | df-9 12333 | Define the number 9. (Contributed by NM, 27-May-1999.) |
⊢ 9 = (8 + 1) | ||
Theorem | 0ne1 12334 | Zero is different from one (the commuted form is Axiom ax-1ne0 11221). (Contributed by David A. Wheeler, 8-Dec-2018.) |
⊢ 0 ≠ 1 | ||
Theorem | 1m1e0 12335 | One minus one equals zero. (Contributed by David A. Wheeler, 7-Jul-2016.) |
⊢ (1 − 1) = 0 | ||
Theorem | 2nn 12336 | 2 is a positive integer. (Contributed by NM, 20-Aug-2001.) |
⊢ 2 ∈ ℕ | ||
Theorem | 2re 12337 | The number 2 is real. (Contributed by NM, 27-May-1999.) |
⊢ 2 ∈ ℝ | ||
Theorem | 2cn 12338 | 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 12339 | Alternate proof of 2cn 12338. Shorter but uses more axioms. Similar proofs are possible for 3cn 12344, ... , 9cn 12363. (Contributed by NM, 30-Jul-2004.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ 2 ∈ ℂ | ||
Theorem | 2ex 12340 | The number 2 is a set. (Contributed by David A. Wheeler, 8-Dec-2018.) |
⊢ 2 ∈ V | ||
Theorem | 2cnd 12341 | The number 2 is a complex number, deduction form. (Contributed by David A. Wheeler, 8-Dec-2018.) |
⊢ (𝜑 → 2 ∈ ℂ) | ||
Theorem | 3nn 12342 | 3 is a positive integer. (Contributed by NM, 8-Jan-2006.) |
⊢ 3 ∈ ℕ | ||
Theorem | 3re 12343 | The number 3 is real. (Contributed by NM, 27-May-1999.) |
⊢ 3 ∈ ℝ | ||
Theorem | 3cn 12344 | 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 12345 | The number 3 is a set. (Contributed by David A. Wheeler, 8-Dec-2018.) |
⊢ 3 ∈ V | ||
Theorem | 4nn 12346 | 4 is a positive integer. (Contributed by NM, 8-Jan-2006.) |
⊢ 4 ∈ ℕ | ||
Theorem | 4re 12347 | The number 4 is real. (Contributed by NM, 27-May-1999.) |
⊢ 4 ∈ ℝ | ||
Theorem | 4cn 12348 | 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 12349 | 5 is a positive integer. (Contributed by Mario Carneiro, 15-Sep-2013.) |
⊢ 5 ∈ ℕ | ||
Theorem | 5re 12350 | The number 5 is real. (Contributed by NM, 27-May-1999.) |
⊢ 5 ∈ ℝ | ||
Theorem | 5cn 12351 | 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 12352 | 6 is a positive integer. (Contributed by Mario Carneiro, 15-Sep-2013.) |
⊢ 6 ∈ ℕ | ||
Theorem | 6re 12353 | The number 6 is real. (Contributed by NM, 27-May-1999.) |
⊢ 6 ∈ ℝ | ||
Theorem | 6cn 12354 | 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 12355 | 7 is a positive integer. (Contributed by Mario Carneiro, 15-Sep-2013.) |
⊢ 7 ∈ ℕ | ||
Theorem | 7re 12356 | The number 7 is real. (Contributed by NM, 27-May-1999.) |
⊢ 7 ∈ ℝ | ||
Theorem | 7cn 12357 | 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 12358 | 8 is a positive integer. (Contributed by Mario Carneiro, 15-Sep-2013.) |
⊢ 8 ∈ ℕ | ||
Theorem | 8re 12359 | The number 8 is real. (Contributed by NM, 27-May-1999.) |
⊢ 8 ∈ ℝ | ||
Theorem | 8cn 12360 | 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 12361 | 9 is a positive integer. (Contributed by NM, 21-Oct-2012.) |
⊢ 9 ∈ ℕ | ||
Theorem | 9re 12362 | The number 9 is real. (Contributed by NM, 27-May-1999.) |
⊢ 9 ∈ ℝ | ||
Theorem | 9cn 12363 | 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 12364 | Zero is nonnegative. (Contributed by David A. Wheeler, 7-Jul-2016.) |
⊢ 0 ≤ 0 | ||
Theorem | 0le2 12365 | The number 0 is less than or equal to 2. (Contributed by David A. Wheeler, 7-Dec-2018.) |
⊢ 0 ≤ 2 | ||
Theorem | 2pos 12366 | The number 2 is positive. (Contributed by NM, 27-May-1999.) |
⊢ 0 < 2 | ||
Theorem | 2ne0 12367 | The number 2 is nonzero. (Contributed by NM, 9-Nov-2007.) |
⊢ 2 ≠ 0 | ||
Theorem | 3pos 12368 | The number 3 is positive. (Contributed by NM, 27-May-1999.) |
⊢ 0 < 3 | ||
Theorem | 3ne0 12369 | The number 3 is nonzero. (Contributed by FL, 17-Oct-2010.) (Proof shortened by Andrew Salmon, 7-May-2011.) |
⊢ 3 ≠ 0 | ||
Theorem | 4pos 12370 | The number 4 is positive. (Contributed by NM, 27-May-1999.) |
⊢ 0 < 4 | ||
Theorem | 4ne0 12371 | The number 4 is nonzero. (Contributed by David A. Wheeler, 5-Dec-2018.) |
⊢ 4 ≠ 0 | ||
Theorem | 5pos 12372 | The number 5 is positive. (Contributed by NM, 27-May-1999.) |
⊢ 0 < 5 | ||
Theorem | 6pos 12373 | The number 6 is positive. (Contributed by NM, 27-May-1999.) |
⊢ 0 < 6 | ||
Theorem | 7pos 12374 | The number 7 is positive. (Contributed by NM, 27-May-1999.) |
⊢ 0 < 7 | ||
Theorem | 8pos 12375 | The number 8 is positive. (Contributed by NM, 27-May-1999.) |
⊢ 0 < 8 | ||
Theorem | 9pos 12376 | 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 12377 | -1 is a complex number. (Contributed by David A. Wheeler, 7-Jul-2016.) |
⊢ -1 ∈ ℂ | ||
Theorem | neg1rr 12378 | -1 is a real number. (Contributed by David A. Wheeler, 5-Dec-2018.) |
⊢ -1 ∈ ℝ | ||
Theorem | neg1ne0 12379 | -1 is nonzero. (Contributed by David A. Wheeler, 8-Dec-2018.) |
⊢ -1 ≠ 0 | ||
Theorem | neg1lt0 12380 | -1 is less than 0. (Contributed by David A. Wheeler, 8-Dec-2018.) |
⊢ -1 < 0 | ||
Theorem | negneg1e1 12381 | --1 is 1. (Contributed by David A. Wheeler, 8-Dec-2018.) |
⊢ --1 = 1 | ||
Theorem | 1pneg1e0 12382 | 1 + -1 is 0. (Contributed by David A. Wheeler, 8-Dec-2018.) |
⊢ (1 + -1) = 0 | ||
Theorem | 0m0e0 12383 | 0 minus 0 equals 0. (Contributed by David A. Wheeler, 8-Dec-2018.) |
⊢ (0 − 0) = 0 | ||
Theorem | 1m0e1 12384 | 1 - 0 = 1. (Contributed by David A. Wheeler, 8-Dec-2018.) |
⊢ (1 − 0) = 1 | ||
Theorem | 0p1e1 12385 | 0 + 1 = 1. (Contributed by David A. Wheeler, 7-Jul-2016.) |
⊢ (0 + 1) = 1 | ||
Theorem | fv0p1e1 12386 | 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 12387 | 1 + 0 = 1. (Contributed by David A. Wheeler, 8-Dec-2018.) |
⊢ (1 + 0) = 1 | ||
Theorem | 1p1e2 12388 | 1 + 1 = 2. (Contributed by NM, 1-Apr-2008.) |
⊢ (1 + 1) = 2 | ||
Theorem | 2m1e1 12389 | 2 - 1 = 1. The result is on the right-hand-side to be consistent with similar proofs like 4p4e8 12418. (Contributed by David A. Wheeler, 4-Jan-2017.) |
⊢ (2 − 1) = 1 | ||
Theorem | 1e2m1 12390 | 1 = 2 - 1. (Contributed by David A. Wheeler, 8-Dec-2018.) |
⊢ 1 = (2 − 1) | ||
Theorem | 3m1e2 12391 | 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 12392 | 4 - 1 = 3. (Contributed by AV, 8-Feb-2021.) (Proof shortened by AV, 6-Sep-2021.) |
⊢ (4 − 1) = 3 | ||
Theorem | 5m1e4 12393 | 5 - 1 = 4. (Contributed by AV, 6-Sep-2021.) |
⊢ (5 − 1) = 4 | ||
Theorem | 6m1e5 12394 | 6 - 1 = 5. (Contributed by AV, 6-Sep-2021.) |
⊢ (6 − 1) = 5 | ||
Theorem | 7m1e6 12395 | 7 - 1 = 6. (Contributed by AV, 6-Sep-2021.) |
⊢ (7 − 1) = 6 | ||
Theorem | 8m1e7 12396 | 8 - 1 = 7. (Contributed by AV, 6-Sep-2021.) |
⊢ (8 − 1) = 7 | ||
Theorem | 9m1e8 12397 | 9 - 1 = 8. (Contributed by AV, 6-Sep-2021.) |
⊢ (9 − 1) = 8 | ||
Theorem | 2p2e4 12398 | Two plus two equals four. For more information, see "2+2=4 Trivia" on the Metamath Proof Explorer Home Page: mmset.html#trivia. This proof is simple, but it depends on many other proof steps because 2 and 4 are complex numbers and thus it depends on our construction of complex numbers. The proof o2p2e4 8577 is similar but proves 2 + 2 = 4 using ordinal natural numbers (finite integers starting at 0), so that proof depends on fewer intermediate steps. (Contributed by NM, 27-May-1999.) |
⊢ (2 + 2) = 4 | ||
Theorem | 2times 12399 | 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 · 𝐴) = (𝐴 + 𝐴)) | ||
Theorem | times2 12400 | A number times 2. (Contributed by NM, 16-Oct-2007.) |
⊢ (𝐴 ∈ ℂ → (𝐴 · 2) = (𝐴 + 𝐴)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |