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