Home | Metamath
Proof Explorer Theorem List (p. 122 of 470) | < 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-29646) |
Hilbert Space Explorer
(29647-31169) |
Users' Mathboxes
(31170-46966) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | dfnn3 12101* | 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 12102 | A positive integer is a real number. (Contributed by Mario Carneiro, 27-May-2016.) |
โข (๐ โ ๐ด โ โ) โ โข (๐ โ ๐ด โ โ) | ||
Theorem | nncnd 12103 | A positive integer is a complex number. (Contributed by Mario Carneiro, 27-May-2016.) |
โข (๐ โ ๐ด โ โ) โ โข (๐ โ ๐ด โ โ) | ||
Theorem | peano2nnd 12104 | Peano postulate: a successor of a positive integer is a positive integer. (Contributed by Mario Carneiro, 27-May-2016.) |
โข (๐ โ ๐ด โ โ) โ โข (๐ โ (๐ด + 1) โ โ) | ||
Theorem | nnind 12105* | 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 12110 for an example of its use. See nn0ind 12529 for induction on nonnegative integers and uzind 12526, uzind4 12760 for induction on an arbitrary upper set of integers. See indstr 12770 for strong induction. See also nnindALT 12106. 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 12106* |
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 12105 has a different hypothesis order. It may be easier to use with the Metamath program 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_WITH nnind / MAYGROW";. (Contributed by NM, 7-Dec-2005.) (New usage is discouraged.) (Proof modification is discouraged.) |
โข (๐ฆ โ โ โ (๐ โ ๐)) & โข ๐ & โข (๐ฅ = 1 โ (๐ โ ๐)) & โข (๐ฅ = ๐ฆ โ (๐ โ ๐)) & โข (๐ฅ = (๐ฆ + 1) โ (๐ โ ๐)) & โข (๐ฅ = ๐ด โ (๐ โ ๐)) โ โข (๐ด โ โ โ ๐) | ||
Theorem | nnindd 12107* | Principle of Mathematical Induction (inference schema) on integers, a deduction version. (Contributed by Thierry Arnoux, 19-Jul-2020.) |
โข (๐ฅ = 1 โ (๐ โ ๐)) & โข (๐ฅ = ๐ฆ โ (๐ โ ๐)) & โข (๐ฅ = (๐ฆ + 1) โ (๐ โ ๐)) & โข (๐ฅ = ๐ด โ (๐ โ ๐)) & โข (๐ โ ๐) & โข (((๐ โง ๐ฆ โ โ) โง ๐) โ ๐) โ โข ((๐ โง ๐ด โ โ) โ ๐) | ||
Theorem | nn1m1nn 12108 | Every positive integer is one or a successor. (Contributed by Mario Carneiro, 16-May-2014.) |
โข (๐ด โ โ โ (๐ด = 1 โจ (๐ด โ 1) โ โ)) | ||
Theorem | nn1suc 12109* | 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 12110 | Closure of addition of positive integers, proved by induction on the second addend. (Contributed by NM, 12-Jan-1997.) |
โข ((๐ด โ โ โง ๐ต โ โ) โ (๐ด + ๐ต) โ โ) | ||
Theorem | nnmulcl 12111 | Closure of multiplication of positive integers. (Contributed by NM, 12-Jan-1997.) Remove dependency on ax-mulcom 11049 and ax-mulass 11051. (Revised by Steven Nguyen, 24-Sep-2022.) |
โข ((๐ด โ โ โง ๐ต โ โ) โ (๐ด ยท ๐ต) โ โ) | ||
Theorem | nnmulcli 12112 | Closure of multiplication of positive integers. (Contributed by Mario Carneiro, 18-Feb-2014.) |
โข ๐ด โ โ & โข ๐ต โ โ โ โข (๐ด ยท ๐ต) โ โ | ||
Theorem | nnmtmip 12113 | "Minus times minus is plus, The reason for this we need not discuss." (W. H. Auden, as quoted in M. Guillen "Bridges to Infinity", p. 64, see also Metamath Book, section 1.1.1, p. 5) This statement, formalized to "The product of two negative integers is a positive integer", is proved by the following theorem, therefore it actually need not be discussed anymore. "The reason for this" is that (-๐ด ยท -๐ต) = (๐ด ยท ๐ต) for all complex numbers ๐ด and ๐ต because of mul2neg 11528, ๐ด and ๐ต are complex numbers because of nncn 12095, and (๐ด ยท ๐ต) โ โ because of nnmulcl 12111. This also holds for positive reals, see rpmtmip 12868. Note that the opposites -๐ด and -๐ต of the positive integers ๐ด and ๐ต are negative integers. (Contributed by AV, 23-Dec-2022.) |
โข ((๐ด โ โ โง ๐ต โ โ) โ (-๐ด ยท -๐ต) โ โ) | ||
Theorem | nn2ge 12114* | There exists a positive integer greater than or equal to any two others. (Contributed by NM, 18-Aug-1999.) |
โข ((๐ด โ โ โง ๐ต โ โ) โ โ๐ฅ โ โ (๐ด โค ๐ฅ โง ๐ต โค ๐ฅ)) | ||
Theorem | nnge1 12115 | A positive integer is one or greater. (Contributed by NM, 25-Aug-1999.) |
โข (๐ด โ โ โ 1 โค ๐ด) | ||
Theorem | nngt1ne1 12116 | A positive integer is greater than one iff it is not equal to one. (Contributed by NM, 7-Oct-2004.) |
โข (๐ด โ โ โ (1 < ๐ด โ ๐ด โ 1)) | ||
Theorem | nnle1eq1 12117 | 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 12118 | A positive integer is positive. (Contributed by NM, 26-Sep-1999.) |
โข (๐ด โ โ โ 0 < ๐ด) | ||
Theorem | nnnlt1 12119 | A positive integer is not less than one. (Contributed by NM, 18-Jan-2004.) (Revised by Mario Carneiro, 27-May-2016.) |
โข (๐ด โ โ โ ยฌ ๐ด < 1) | ||
Theorem | nnnle0 12120 | A positive integer is not less than or equal to zero. (Contributed by AV, 13-May-2020.) |
โข (๐ด โ โ โ ยฌ ๐ด โค 0) | ||
Theorem | nnne0 12121 | A positive integer is nonzero. See nnne0ALT 12125 for a shorter proof using ax-pre-mulgt0 11062. This proof avoids 0lt1 11611, and thus ax-pre-mulgt0 11062, by splitting ax-1ne0 11054 into the two separate cases 0 < 1 and 1 < 0. (Contributed by NM, 27-Sep-1999.) Remove dependency on ax-pre-mulgt0 11062. (Revised by Steven Nguyen, 30-Jan-2023.) |
โข (๐ด โ โ โ ๐ด โ 0) | ||
Theorem | nnneneg 12122 | No positive integer is equal to its negation. (Contributed by AV, 20-Jun-2023.) |
โข (๐ด โ โ โ ๐ด โ -๐ด) | ||
Theorem | 0nnn 12123 | Zero is not a positive integer. (Contributed by NM, 25-Aug-1999.) Remove dependency on ax-pre-mulgt0 11062. (Revised by Steven Nguyen, 30-Jan-2023.) |
โข ยฌ 0 โ โ | ||
Theorem | 0nnnALT 12124 | Alternate proof of 0nnn 12123, which requires ax-pre-mulgt0 11062 but is not based on nnne0 12121 (and which can therefore be used in nnne0ALT 12125). (Contributed by NM, 25-Aug-1999.) (New usage is discouraged.) (Proof modification is discouraged.) |
โข ยฌ 0 โ โ | ||
Theorem | nnne0ALT 12125 | Alternate version of nnne0 12121. A positive integer is nonzero. (Contributed by NM, 27-Sep-1999.) (New usage is discouraged.) (Proof modification is discouraged.) |
โข (๐ด โ โ โ ๐ด โ 0) | ||
Theorem | nngt0i 12126 | A positive integer is positive (inference version). (Contributed by NM, 17-Sep-1999.) |
โข ๐ด โ โ โ โข 0 < ๐ด | ||
Theorem | nnne0i 12127 | A positive integer is nonzero (inference version). (Contributed by NM, 25-Aug-1999.) |
โข ๐ด โ โ โ โข ๐ด โ 0 | ||
Theorem | nndivre 12128 | The quotient of a real and a positive integer is real. (Contributed by NM, 28-Nov-2008.) |
โข ((๐ด โ โ โง ๐ โ โ) โ (๐ด / ๐) โ โ) | ||
Theorem | nnrecre 12129 | The reciprocal of a positive integer is real. (Contributed by NM, 8-Feb-2008.) |
โข (๐ โ โ โ (1 / ๐) โ โ) | ||
Theorem | nnrecgt0 12130 | The reciprocal of a positive integer is positive. (Contributed by NM, 25-Aug-1999.) |
โข (๐ด โ โ โ 0 < (1 / ๐ด)) | ||
Theorem | nnsub 12131 | Subtraction of positive integers. (Contributed by NM, 20-Aug-2001.) (Revised by Mario Carneiro, 16-May-2014.) |
โข ((๐ด โ โ โง ๐ต โ โ) โ (๐ด < ๐ต โ (๐ต โ ๐ด) โ โ)) | ||
Theorem | nnsubi 12132 | Subtraction of positive integers. (Contributed by NM, 19-Aug-2001.) |
โข ๐ด โ โ & โข ๐ต โ โ โ โข (๐ด < ๐ต โ (๐ต โ ๐ด) โ โ) | ||
Theorem | nndiv 12133* | Two ways to express "๐ด divides ๐ต " for positive integers. (Contributed by NM, 3-Feb-2004.) (Proof shortened by Mario Carneiro, 16-May-2014.) |
โข ((๐ด โ โ โง ๐ต โ โ) โ (โ๐ฅ โ โ (๐ด ยท ๐ฅ) = ๐ต โ (๐ต / ๐ด) โ โ)) | ||
Theorem | nndivtr 12134 | 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 12135 | A positive integer is one or greater. (Contributed by Mario Carneiro, 27-May-2016.) |
โข (๐ โ ๐ด โ โ) โ โข (๐ โ 1 โค ๐ด) | ||
Theorem | nngt0d 12136 | A positive integer is positive. (Contributed by Mario Carneiro, 27-May-2016.) |
โข (๐ โ ๐ด โ โ) โ โข (๐ โ 0 < ๐ด) | ||
Theorem | nnne0d 12137 | A positive integer is nonzero. (Contributed by Mario Carneiro, 27-May-2016.) |
โข (๐ โ ๐ด โ โ) โ โข (๐ โ ๐ด โ 0) | ||
Theorem | nnrecred 12138 | The reciprocal of a positive integer is real. (Contributed by Mario Carneiro, 27-May-2016.) |
โข (๐ โ ๐ด โ โ) โ โข (๐ โ (1 / ๐ด) โ โ) | ||
Theorem | nnaddcld 12139 | Closure of addition of positive integers. (Contributed by Mario Carneiro, 27-May-2016.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ โ) โ โข (๐ โ (๐ด + ๐ต) โ โ) | ||
Theorem | nnmulcld 12140 | Closure of multiplication of positive integers. (Contributed by Mario Carneiro, 27-May-2016.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ โ) โ โข (๐ โ (๐ด ยท ๐ต) โ โ) | ||
Theorem | nndivred 12141 | 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 10992 through df-9 12157), 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 10992 and df-1 10993). With the decimal constructor df-dec 12552, it is possible to easily express larger integers in base 10. See deccl 12566 and the theorems that follow it. See also 4001prm 16952 (4001 is prime) and the proof of bpos 26563. 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 16005. 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 12142 | Extend class notation to include the number 2. |
class 2 | ||
Syntax | c3 12143 | Extend class notation to include the number 3. |
class 3 | ||
Syntax | c4 12144 | Extend class notation to include the number 4. |
class 4 | ||
Syntax | c5 12145 | Extend class notation to include the number 5. |
class 5 | ||
Syntax | c6 12146 | Extend class notation to include the number 6. |
class 6 | ||
Syntax | c7 12147 | Extend class notation to include the number 7. |
class 7 | ||
Syntax | c8 12148 | Extend class notation to include the number 8. |
class 8 | ||
Syntax | c9 12149 | Extend class notation to include the number 9. |
class 9 | ||
Definition | df-2 12150 | Define the number 2. (Contributed by NM, 27-May-1999.) |
โข 2 = (1 + 1) | ||
Definition | df-3 12151 | Define the number 3. (Contributed by NM, 27-May-1999.) |
โข 3 = (2 + 1) | ||
Definition | df-4 12152 | Define the number 4. (Contributed by NM, 27-May-1999.) |
โข 4 = (3 + 1) | ||
Definition | df-5 12153 | Define the number 5. (Contributed by NM, 27-May-1999.) |
โข 5 = (4 + 1) | ||
Definition | df-6 12154 | Define the number 6. (Contributed by NM, 27-May-1999.) |
โข 6 = (5 + 1) | ||
Definition | df-7 12155 | Define the number 7. (Contributed by NM, 27-May-1999.) |
โข 7 = (6 + 1) | ||
Definition | df-8 12156 | Define the number 8. (Contributed by NM, 27-May-1999.) |
โข 8 = (7 + 1) | ||
Definition | df-9 12157 | Define the number 9. (Contributed by NM, 27-May-1999.) |
โข 9 = (8 + 1) | ||
Theorem | 0ne1 12158 | Zero is different from one (the commuted form is Axiom ax-1ne0 11054). (Contributed by David A. Wheeler, 8-Dec-2018.) |
โข 0 โ 1 | ||
Theorem | 1m1e0 12159 | One minus one equals zero. (Contributed by David A. Wheeler, 7-Jul-2016.) |
โข (1 โ 1) = 0 | ||
Theorem | 2nn 12160 | 2 is a positive integer. (Contributed by NM, 20-Aug-2001.) |
โข 2 โ โ | ||
Theorem | 2re 12161 | The number 2 is real. (Contributed by NM, 27-May-1999.) |
โข 2 โ โ | ||
Theorem | 2cn 12162 | 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 12163 | Alternate proof of 2cn 12162. Shorter but uses more axioms. Similar proofs are possible for 3cn 12168, ... , 9cn 12187. (Contributed by NM, 30-Jul-2004.) (Proof modification is discouraged.) (New usage is discouraged.) |
โข 2 โ โ | ||
Theorem | 2ex 12164 | The number 2 is a set. (Contributed by David A. Wheeler, 8-Dec-2018.) |
โข 2 โ V | ||
Theorem | 2cnd 12165 | The number 2 is a complex number, deduction form. (Contributed by David A. Wheeler, 8-Dec-2018.) |
โข (๐ โ 2 โ โ) | ||
Theorem | 3nn 12166 | 3 is a positive integer. (Contributed by NM, 8-Jan-2006.) |
โข 3 โ โ | ||
Theorem | 3re 12167 | The number 3 is real. (Contributed by NM, 27-May-1999.) |
โข 3 โ โ | ||
Theorem | 3cn 12168 | 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 12169 | The number 3 is a set. (Contributed by David A. Wheeler, 8-Dec-2018.) |
โข 3 โ V | ||
Theorem | 4nn 12170 | 4 is a positive integer. (Contributed by NM, 8-Jan-2006.) |
โข 4 โ โ | ||
Theorem | 4re 12171 | The number 4 is real. (Contributed by NM, 27-May-1999.) |
โข 4 โ โ | ||
Theorem | 4cn 12172 | 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 12173 | 5 is a positive integer. (Contributed by Mario Carneiro, 15-Sep-2013.) |
โข 5 โ โ | ||
Theorem | 5re 12174 | The number 5 is real. (Contributed by NM, 27-May-1999.) |
โข 5 โ โ | ||
Theorem | 5cn 12175 | 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 12176 | 6 is a positive integer. (Contributed by Mario Carneiro, 15-Sep-2013.) |
โข 6 โ โ | ||
Theorem | 6re 12177 | The number 6 is real. (Contributed by NM, 27-May-1999.) |
โข 6 โ โ | ||
Theorem | 6cn 12178 | 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 12179 | 7 is a positive integer. (Contributed by Mario Carneiro, 15-Sep-2013.) |
โข 7 โ โ | ||
Theorem | 7re 12180 | The number 7 is real. (Contributed by NM, 27-May-1999.) |
โข 7 โ โ | ||
Theorem | 7cn 12181 | 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 12182 | 8 is a positive integer. (Contributed by Mario Carneiro, 15-Sep-2013.) |
โข 8 โ โ | ||
Theorem | 8re 12183 | The number 8 is real. (Contributed by NM, 27-May-1999.) |
โข 8 โ โ | ||
Theorem | 8cn 12184 | 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 12185 | 9 is a positive integer. (Contributed by NM, 21-Oct-2012.) |
โข 9 โ โ | ||
Theorem | 9re 12186 | The number 9 is real. (Contributed by NM, 27-May-1999.) |
โข 9 โ โ | ||
Theorem | 9cn 12187 | 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 12188 | Zero is nonnegative. (Contributed by David A. Wheeler, 7-Jul-2016.) |
โข 0 โค 0 | ||
Theorem | 0le2 12189 | The number 0 is less than or equal to 2. (Contributed by David A. Wheeler, 7-Dec-2018.) |
โข 0 โค 2 | ||
Theorem | 2pos 12190 | The number 2 is positive. (Contributed by NM, 27-May-1999.) |
โข 0 < 2 | ||
Theorem | 2ne0 12191 | The number 2 is nonzero. (Contributed by NM, 9-Nov-2007.) |
โข 2 โ 0 | ||
Theorem | 3pos 12192 | The number 3 is positive. (Contributed by NM, 27-May-1999.) |
โข 0 < 3 | ||
Theorem | 3ne0 12193 | The number 3 is nonzero. (Contributed by FL, 17-Oct-2010.) (Proof shortened by Andrew Salmon, 7-May-2011.) |
โข 3 โ 0 | ||
Theorem | 4pos 12194 | The number 4 is positive. (Contributed by NM, 27-May-1999.) |
โข 0 < 4 | ||
Theorem | 4ne0 12195 | The number 4 is nonzero. (Contributed by David A. Wheeler, 5-Dec-2018.) |
โข 4 โ 0 | ||
Theorem | 5pos 12196 | The number 5 is positive. (Contributed by NM, 27-May-1999.) |
โข 0 < 5 | ||
Theorem | 6pos 12197 | The number 6 is positive. (Contributed by NM, 27-May-1999.) |
โข 0 < 6 | ||
Theorem | 7pos 12198 | The number 7 is positive. (Contributed by NM, 27-May-1999.) |
โข 0 < 7 | ||
Theorem | 8pos 12199 | The number 8 is positive. (Contributed by NM, 27-May-1999.) |
โข 0 < 8 | ||
Theorem | 9pos 12200 | The number 9 is positive. (Contributed by NM, 27-May-1999.) |
โข 0 < 9 |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |