Home | Metamath
Proof Explorer Theorem List (p. 110 of 424) | < 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: | Metamath Proof Explorer
(1-27159) |
Hilbert Space Explorer
(27160-28684) |
Users' Mathboxes
(28685-42360) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | nnssre 10901 | The positive integers are a subset of the reals. (Contributed by NM, 10-Jan-1997.) (Revised by Mario Carneiro, 16-Jun-2013.) |
⊢ ℕ ⊆ ℝ | ||
Theorem | nnsscn 10902 | The positive integers are a subset of the complex numbers. (Contributed by NM, 2-Aug-2004.) |
⊢ ℕ ⊆ ℂ | ||
Theorem | nnex 10903 | The set of positive integers exists. (Contributed by NM, 3-Oct-1999.) (Revised by Mario Carneiro, 17-Nov-2014.) |
⊢ ℕ ∈ V | ||
Theorem | nnre 10904 | A positive integer is a real number. (Contributed by NM, 18-Aug-1999.) |
⊢ (𝐴 ∈ ℕ → 𝐴 ∈ ℝ) | ||
Theorem | nncn 10905 | A positive integer is a complex number. (Contributed by NM, 18-Aug-1999.) |
⊢ (𝐴 ∈ ℕ → 𝐴 ∈ ℂ) | ||
Theorem | nnrei 10906 | A positive integer is a real number. (Contributed by NM, 18-Aug-1999.) |
⊢ 𝐴 ∈ ℕ ⇒ ⊢ 𝐴 ∈ ℝ | ||
Theorem | nncni 10907 | A positive integer is a complex number. (Contributed by NM, 18-Aug-1999.) |
⊢ 𝐴 ∈ ℕ ⇒ ⊢ 𝐴 ∈ ℂ | ||
Theorem | 1nn 10908 | Peano postulate: 1 is a positive integer. (Contributed by NM, 11-Jan-1997.) (Revised by Mario Carneiro, 17-Nov-2014.) |
⊢ 1 ∈ ℕ | ||
Theorem | peano2nn 10909 | 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.) |
⊢ (𝐴 ∈ ℕ → (𝐴 + 1) ∈ ℕ) | ||
Theorem | dfnn2 10910* | Alternate definition of the set of positive integers. This was our original definition, before the current df-nn 10898 replaced it. This definition requires the axiom of infinity to ensure it has the properties we expect. (Contributed by Jeff Hankins, 12-Sep-2013.) (Revised by Mario Carneiro, 3-May-2014.) |
⊢ ℕ = ∩ {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑦 + 1) ∈ 𝑥)} | ||
Theorem | dfnn3 10911* | Alternate definition of the set of positive integers. Definition of positive integers in [Apostol] p. 22. (Contributed by NM, 3-Jul-2005.) |
⊢ ℕ = ∩ {𝑥 ∣ (𝑥 ⊆ ℝ ∧ 1 ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑦 + 1) ∈ 𝑥)} | ||
Theorem | nnred 10912 | A positive integer is a real number. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℕ) ⇒ ⊢ (𝜑 → 𝐴 ∈ ℝ) | ||
Theorem | nncnd 10913 | A positive integer is a complex number. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℕ) ⇒ ⊢ (𝜑 → 𝐴 ∈ ℂ) | ||
Theorem | peano2nnd 10914 | Peano postulate: a successor of a positive integer is a positive integer. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℕ) ⇒ ⊢ (𝜑 → (𝐴 + 1) ∈ ℕ) | ||
Theorem | nnind 10915* | 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 10919 for an example of its use. See nn0ind 11348 for induction on nonnegative integers and uzind 11345, uzind4 11622 for induction on an arbitrary upper set of integers. See indstr 11632 for strong induction. See also nnindALT 10916. This is an alternative for Metamath 100 proof #74. (Contributed by NM, 10-Jan-1997.) (Revised by Mario Carneiro, 16-Jun-2013.) |
⊢ (𝑥 = 1 → (𝜑 ↔ 𝜓)) & ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜒)) & ⊢ (𝑥 = (𝑦 + 1) → (𝜑 ↔ 𝜃)) & ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜏)) & ⊢ 𝜓 & ⊢ (𝑦 ∈ ℕ → (𝜒 → 𝜃)) ⇒ ⊢ (𝐴 ∈ ℕ → 𝜏) | ||
Theorem | nnindALT 10916* |
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 10915 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 /maygrow". (Contributed by NM, 7-Dec-2005.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ (𝑦 ∈ ℕ → (𝜒 → 𝜃)) & ⊢ 𝜓 & ⊢ (𝑥 = 1 → (𝜑 ↔ 𝜓)) & ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜒)) & ⊢ (𝑥 = (𝑦 + 1) → (𝜑 ↔ 𝜃)) & ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜏)) ⇒ ⊢ (𝐴 ∈ ℕ → 𝜏) | ||
Theorem | nn1m1nn 10917 | Every positive integer is one or a successor. (Contributed by Mario Carneiro, 16-May-2014.) |
⊢ (𝐴 ∈ ℕ → (𝐴 = 1 ∨ (𝐴 − 1) ∈ ℕ)) | ||
Theorem | nn1suc 10918* | 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.) |
⊢ (𝑥 = 1 → (𝜑 ↔ 𝜓)) & ⊢ (𝑥 = (𝑦 + 1) → (𝜑 ↔ 𝜒)) & ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜃)) & ⊢ 𝜓 & ⊢ (𝑦 ∈ ℕ → 𝜒) ⇒ ⊢ (𝐴 ∈ ℕ → 𝜃) | ||
Theorem | nnaddcl 10919 | Closure of addition of positive integers, proved by induction on the second addend. (Contributed by NM, 12-Jan-1997.) |
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) → (𝐴 + 𝐵) ∈ ℕ) | ||
Theorem | nnmulcl 10920 | Closure of multiplication of positive integers. (Contributed by NM, 12-Jan-1997.) |
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) → (𝐴 · 𝐵) ∈ ℕ) | ||
Theorem | nnmulcli 10921 | Closure of multiplication of positive integers. (Contributed by Mario Carneiro, 18-Feb-2014.) |
⊢ 𝐴 ∈ ℕ & ⊢ 𝐵 ∈ ℕ ⇒ ⊢ (𝐴 · 𝐵) ∈ ℕ | ||
Theorem | nn2ge 10922* | There exists a positive integer greater than or equal to any two others. (Contributed by NM, 18-Aug-1999.) |
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) → ∃𝑥 ∈ ℕ (𝐴 ≤ 𝑥 ∧ 𝐵 ≤ 𝑥)) | ||
Theorem | nnge1 10923 | A positive integer is one or greater. (Contributed by NM, 25-Aug-1999.) |
⊢ (𝐴 ∈ ℕ → 1 ≤ 𝐴) | ||
Theorem | nngt1ne1 10924 | A positive integer is greater than one iff it is not equal to one. (Contributed by NM, 7-Oct-2004.) |
⊢ (𝐴 ∈ ℕ → (1 < 𝐴 ↔ 𝐴 ≠ 1)) | ||
Theorem | nnle1eq1 10925 | 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 10926 | A positive integer is positive. (Contributed by NM, 26-Sep-1999.) |
⊢ (𝐴 ∈ ℕ → 0 < 𝐴) | ||
Theorem | nnnlt1 10927 | A positive integer is not less than one. (Contributed by NM, 18-Jan-2004.) (Revised by Mario Carneiro, 27-May-2016.) |
⊢ (𝐴 ∈ ℕ → ¬ 𝐴 < 1) | ||
Theorem | nnnle0 10928 | A positive integer is not less than or equal to zero . (Contributed by AV, 13-May-2020.) |
⊢ (𝐴 ∈ ℕ → ¬ 𝐴 ≤ 0) | ||
Theorem | 0nnn 10929 | Zero is not a positive integer. (Contributed by NM, 25-Aug-1999.) |
⊢ ¬ 0 ∈ ℕ | ||
Theorem | nnne0 10930 | A positive integer is nonzero. (Contributed by NM, 27-Sep-1999.) |
⊢ (𝐴 ∈ ℕ → 𝐴 ≠ 0) | ||
Theorem | nngt0i 10931 | A positive integer is positive (inference version). (Contributed by NM, 17-Sep-1999.) |
⊢ 𝐴 ∈ ℕ ⇒ ⊢ 0 < 𝐴 | ||
Theorem | nnne0i 10932 | A positive integer is nonzero (inference version). (Contributed by NM, 25-Aug-1999.) |
⊢ 𝐴 ∈ ℕ ⇒ ⊢ 𝐴 ≠ 0 | ||
Theorem | nndivre 10933 | The quotient of a real and a positive integer is real. (Contributed by NM, 28-Nov-2008.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝑁 ∈ ℕ) → (𝐴 / 𝑁) ∈ ℝ) | ||
Theorem | nnrecre 10934 | The reciprocal of a positive integer is real. (Contributed by NM, 8-Feb-2008.) |
⊢ (𝑁 ∈ ℕ → (1 / 𝑁) ∈ ℝ) | ||
Theorem | nnrecgt0 10935 | The reciprocal of a positive integer is positive. (Contributed by NM, 25-Aug-1999.) |
⊢ (𝐴 ∈ ℕ → 0 < (1 / 𝐴)) | ||
Theorem | nnsub 10936 | Subtraction of positive integers. (Contributed by NM, 20-Aug-2001.) (Revised by Mario Carneiro, 16-May-2014.) |
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) → (𝐴 < 𝐵 ↔ (𝐵 − 𝐴) ∈ ℕ)) | ||
Theorem | nnsubi 10937 | Subtraction of positive integers. (Contributed by NM, 19-Aug-2001.) |
⊢ 𝐴 ∈ ℕ & ⊢ 𝐵 ∈ ℕ ⇒ ⊢ (𝐴 < 𝐵 ↔ (𝐵 − 𝐴) ∈ ℕ) | ||
Theorem | nndiv 10938* | Two ways to express "𝐴 divides 𝐵 " for positive integers. (Contributed by NM, 3-Feb-2004.) (Proof shortened by Mario Carneiro, 16-May-2014.) |
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) → (∃𝑥 ∈ ℕ (𝐴 · 𝑥) = 𝐵 ↔ (𝐵 / 𝐴) ∈ ℕ)) | ||
Theorem | nndivtr 10939 | 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 10940 | A positive integer is one or greater. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℕ) ⇒ ⊢ (𝜑 → 1 ≤ 𝐴) | ||
Theorem | nngt0d 10941 | A positive integer is positive. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℕ) ⇒ ⊢ (𝜑 → 0 < 𝐴) | ||
Theorem | nnne0d 10942 | A positive integer is nonzero. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℕ) ⇒ ⊢ (𝜑 → 𝐴 ≠ 0) | ||
Theorem | nnrecred 10943 | The reciprocal of a positive integer is real. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℕ) ⇒ ⊢ (𝜑 → (1 / 𝐴) ∈ ℝ) | ||
Theorem | nnaddcld 10944 | Closure of addition of positive integers. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℕ) & ⊢ (𝜑 → 𝐵 ∈ ℕ) ⇒ ⊢ (𝜑 → (𝐴 + 𝐵) ∈ ℕ) | ||
Theorem | nnmulcld 10945 | Closure of multiplication of positive integers. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℕ) & ⊢ (𝜑 → 𝐵 ∈ ℕ) ⇒ ⊢ (𝜑 → (𝐴 · 𝐵) ∈ ℕ) | ||
Theorem | nndivred 10946 | 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 9822 through df-9 10963), 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 9822 and df-1 9823). With the decimal constructor df-dec 11370, it is possible to easily express larger integers in base 10. See deccl 11388 and the theorems that follow it. See also 4001prm 15690 (4001 is prime) and the proof of bpos 24818. Note that the decimal constructor builds on the definitions in this section. Note: The symbol 10 representing the number 10 is deprecated (and will be removed in the near future). The number 10 should 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 14757. 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 10947 | Extend class notation to include the number 2. |
class 2 | ||
Syntax | c3 10948 | Extend class notation to include the number 3. |
class 3 | ||
Syntax | c4 10949 | Extend class notation to include the number 4. |
class 4 | ||
Syntax | c5 10950 | Extend class notation to include the number 5. |
class 5 | ||
Syntax | c6 10951 | Extend class notation to include the number 6. |
class 6 | ||
Syntax | c7 10952 | Extend class notation to include the number 7. |
class 7 | ||
Syntax | c8 10953 | Extend class notation to include the number 8. |
class 8 | ||
Syntax | c9 10954 | Extend class notation to include the number 9. |
class 9 | ||
Syntax | c10 10955 | Extend class notation to include the number 10. |
class 10 | ||
Definition | df-2 10956 | Define the number 2. (Contributed by NM, 27-May-1999.) |
⊢ 2 = (1 + 1) | ||
Definition | df-3 10957 | Define the number 3. (Contributed by NM, 27-May-1999.) |
⊢ 3 = (2 + 1) | ||
Definition | df-4 10958 | Define the number 4. (Contributed by NM, 27-May-1999.) |
⊢ 4 = (3 + 1) | ||
Definition | df-5 10959 | Define the number 5. (Contributed by NM, 27-May-1999.) |
⊢ 5 = (4 + 1) | ||
Definition | df-6 10960 | Define the number 6. (Contributed by NM, 27-May-1999.) |
⊢ 6 = (5 + 1) | ||
Definition | df-7 10961 | Define the number 7. (Contributed by NM, 27-May-1999.) |
⊢ 7 = (6 + 1) | ||
Definition | df-8 10962 | Define the number 8. (Contributed by NM, 27-May-1999.) |
⊢ 8 = (7 + 1) | ||
Definition | df-9 10963 | Define the number 9. (Contributed by NM, 27-May-1999.) |
⊢ 9 = (8 + 1) | ||
Definition | df-10OLD 10964 | Define the number 10. See remarks under df-2 10956. (Contributed by NM, 5-Feb-2007.) Obsolete as of 9-Sep-2021. (New usage is discouraged.) |
⊢ 10 = (9 + 1) | ||
Theorem | 0ne1 10965 | 0 ≠ 1 (common case); the reverse order is already proved. (Contributed by David A. Wheeler, 8-Dec-2018.) |
⊢ 0 ≠ 1 | ||
Theorem | 1m1e0 10966 | (1 − 1) = 0 (common case). (Contributed by David A. Wheeler, 7-Jul-2016.) |
⊢ (1 − 1) = 0 | ||
Theorem | 2re 10967 | The number 2 is real. (Contributed by NM, 27-May-1999.) |
⊢ 2 ∈ ℝ | ||
Theorem | 2cn 10968 | The number 2 is a complex number. (Contributed by NM, 30-Jul-2004.) |
⊢ 2 ∈ ℂ | ||
Theorem | 2ex 10969 | 2 is a set (common case). (Contributed by David A. Wheeler, 8-Dec-2018.) |
⊢ 2 ∈ V | ||
Theorem | 2cnd 10970 | 2 is a complex number, deductive form (common case). (Contributed by David A. Wheeler, 8-Dec-2018.) |
⊢ (𝜑 → 2 ∈ ℂ) | ||
Theorem | 3re 10971 | The number 3 is real. (Contributed by NM, 27-May-1999.) |
⊢ 3 ∈ ℝ | ||
Theorem | 3cn 10972 | The number 3 is a complex number. (Contributed by FL, 17-Oct-2010.) |
⊢ 3 ∈ ℂ | ||
Theorem | 3ex 10973 | 3 is a set (common case). (Contributed by David A. Wheeler, 8-Dec-2018.) |
⊢ 3 ∈ V | ||
Theorem | 4re 10974 | The number 4 is real. (Contributed by NM, 27-May-1999.) |
⊢ 4 ∈ ℝ | ||
Theorem | 4cn 10975 | The number 4 is a complex number. (Contributed by David A. Wheeler, 7-Jul-2016.) |
⊢ 4 ∈ ℂ | ||
Theorem | 5re 10976 | The number 5 is real. (Contributed by NM, 27-May-1999.) |
⊢ 5 ∈ ℝ | ||
Theorem | 5cn 10977 | The number 5 is complex. (Contributed by David A. Wheeler, 8-Dec-2018.) |
⊢ 5 ∈ ℂ | ||
Theorem | 6re 10978 | The number 6 is real. (Contributed by NM, 27-May-1999.) |
⊢ 6 ∈ ℝ | ||
Theorem | 6cn 10979 | The number 6 is complex. (Contributed by David A. Wheeler, 8-Dec-2018.) |
⊢ 6 ∈ ℂ | ||
Theorem | 7re 10980 | The number 7 is real. (Contributed by NM, 27-May-1999.) |
⊢ 7 ∈ ℝ | ||
Theorem | 7cn 10981 | The number 7 is complex. (Contributed by David A. Wheeler, 8-Dec-2018.) |
⊢ 7 ∈ ℂ | ||
Theorem | 8re 10982 | The number 8 is real. (Contributed by NM, 27-May-1999.) |
⊢ 8 ∈ ℝ | ||
Theorem | 8cn 10983 | The number 8 is complex. (Contributed by David A. Wheeler, 8-Dec-2018.) |
⊢ 8 ∈ ℂ | ||
Theorem | 9re 10984 | The number 9 is real. (Contributed by NM, 27-May-1999.) |
⊢ 9 ∈ ℝ | ||
Theorem | 9cn 10985 | The number 9 is complex. (Contributed by David A. Wheeler, 8-Dec-2018.) |
⊢ 9 ∈ ℂ | ||
Theorem | 10reOLD 10986 | Obsolete version of 10re 11393 as of 8-Sep-2021. (Contributed by NM, 5-Feb-2007.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ 10 ∈ ℝ | ||
Theorem | 0le0 10987 | Zero is nonnegative. (Contributed by David A. Wheeler, 7-Jul-2016.) |
⊢ 0 ≤ 0 | ||
Theorem | 0le2 10988 | 0 is less than or equal to 2. (Contributed by David A. Wheeler, 7-Dec-2018.) |
⊢ 0 ≤ 2 | ||
Theorem | 2pos 10989 | The number 2 is positive. (Contributed by NM, 27-May-1999.) |
⊢ 0 < 2 | ||
Theorem | 2ne0 10990 | The number 2 is nonzero. (Contributed by NM, 9-Nov-2007.) |
⊢ 2 ≠ 0 | ||
Theorem | 3pos 10991 | The number 3 is positive. (Contributed by NM, 27-May-1999.) |
⊢ 0 < 3 | ||
Theorem | 3ne0 10992 | The number 3 is nonzero. (Contributed by FL, 17-Oct-2010.) (Proof shortened by Andrew Salmon, 7-May-2011.) |
⊢ 3 ≠ 0 | ||
Theorem | 4pos 10993 | The number 4 is positive. (Contributed by NM, 27-May-1999.) |
⊢ 0 < 4 | ||
Theorem | 4ne0 10994 | The number 4 is nonzero. (Contributed by David A. Wheeler, 5-Dec-2018.) |
⊢ 4 ≠ 0 | ||
Theorem | 5pos 10995 | The number 5 is positive. (Contributed by NM, 27-May-1999.) |
⊢ 0 < 5 | ||
Theorem | 6pos 10996 | The number 6 is positive. (Contributed by NM, 27-May-1999.) |
⊢ 0 < 6 | ||
Theorem | 7pos 10997 | The number 7 is positive. (Contributed by NM, 27-May-1999.) |
⊢ 0 < 7 | ||
Theorem | 8pos 10998 | The number 8 is positive. (Contributed by NM, 27-May-1999.) |
⊢ 0 < 8 | ||
Theorem | 9pos 10999 | The number 9 is positive. (Contributed by NM, 27-May-1999.) |
⊢ 0 < 9 | ||
Theorem | 10posOLD 11000 | The number 10 is positive. (Contributed by NM, 5-Feb-2007.) Obsolete version of 10pos 11391 as of 8-Sep-2021. (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ 0 < 10 |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |