![]() |
Metamath
Proof Explorer Theorem List (p. 123 of 482) | < 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-30715) |
![]() (30716-32238) |
![]() (32239-48161) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | suprnub 12201* | An upper bound is not less than the supremum of a nonempty bounded set of reals. (Contributed by NM, 15-Nov-2004.) (Revised by Mario Carneiro, 6-Sep-2014.) |
β’ (((π΄ β β β§ π΄ β β β§ βπ₯ β β βπ¦ β π΄ π¦ β€ π₯) β§ π΅ β β) β (Β¬ π΅ < sup(π΄, β, < ) β βπ§ β π΄ Β¬ π΅ < π§)) | ||
Theorem | suprleub 12202* | The supremum of a nonempty bounded set of reals is less than or equal to an upper bound. (Contributed by NM, 18-Mar-2005.) (Revised by Mario Carneiro, 6-Sep-2014.) |
β’ (((π΄ β β β§ π΄ β β β§ βπ₯ β β βπ¦ β π΄ π¦ β€ π₯) β§ π΅ β β) β (sup(π΄, β, < ) β€ π΅ β βπ§ β π΄ π§ β€ π΅)) | ||
Theorem | supaddc 12203* | The supremum function distributes over addition in a sense similar to that in supmul1 12205. (Contributed by Brendan Leahy, 25-Sep-2017.) |
β’ (π β π΄ β β) & β’ (π β π΄ β β ) & β’ (π β βπ₯ β β βπ¦ β π΄ π¦ β€ π₯) & β’ (π β π΅ β β) & β’ πΆ = {π§ β£ βπ£ β π΄ π§ = (π£ + π΅)} β β’ (π β (sup(π΄, β, < ) + π΅) = sup(πΆ, β, < )) | ||
Theorem | supadd 12204* | The supremum function distributes over addition in a sense similar to that in supmul 12208. (Contributed by Brendan Leahy, 26-Sep-2017.) |
β’ (π β π΄ β β) & β’ (π β π΄ β β ) & β’ (π β βπ₯ β β βπ¦ β π΄ π¦ β€ π₯) & β’ (π β π΅ β β) & β’ (π β π΅ β β ) & β’ (π β βπ₯ β β βπ¦ β π΅ π¦ β€ π₯) & β’ πΆ = {π§ β£ βπ£ β π΄ βπ β π΅ π§ = (π£ + π)} β β’ (π β (sup(π΄, β, < ) + sup(π΅, β, < )) = sup(πΆ, β, < )) | ||
Theorem | supmul1 12205* | The supremum function distributes over multiplication, in the sense that π΄ Β· (supπ΅) = sup(π΄ Β· π΅), where π΄ Β· π΅ is shorthand for {π΄ Β· π β£ π β π΅} and is defined as πΆ below. This is the simple version, with only one set argument; see supmul 12208 for the more general case with two set arguments. (Contributed by Mario Carneiro, 5-Jul-2013.) |
β’ πΆ = {π§ β£ βπ£ β π΅ π§ = (π΄ Β· π£)} & β’ (π β ((π΄ β β β§ 0 β€ π΄ β§ βπ₯ β π΅ 0 β€ π₯) β§ (π΅ β β β§ π΅ β β β§ βπ₯ β β βπ¦ β π΅ π¦ β€ π₯))) β β’ (π β (π΄ Β· sup(π΅, β, < )) = sup(πΆ, β, < )) | ||
Theorem | supmullem1 12206* | Lemma for supmul 12208. (Contributed by Mario Carneiro, 5-Jul-2013.) |
β’ πΆ = {π§ β£ βπ£ β π΄ βπ β π΅ π§ = (π£ Β· π)} & β’ (π β ((βπ₯ β π΄ 0 β€ π₯ β§ βπ₯ β π΅ 0 β€ π₯) β§ (π΄ β β β§ π΄ β β β§ βπ₯ β β βπ¦ β π΄ π¦ β€ π₯) β§ (π΅ β β β§ π΅ β β β§ βπ₯ β β βπ¦ β π΅ π¦ β€ π₯))) β β’ (π β βπ€ β πΆ π€ β€ (sup(π΄, β, < ) Β· sup(π΅, β, < ))) | ||
Theorem | supmullem2 12207* | Lemma for supmul 12208. (Contributed by Mario Carneiro, 5-Jul-2013.) |
β’ πΆ = {π§ β£ βπ£ β π΄ βπ β π΅ π§ = (π£ Β· π)} & β’ (π β ((βπ₯ β π΄ 0 β€ π₯ β§ βπ₯ β π΅ 0 β€ π₯) β§ (π΄ β β β§ π΄ β β β§ βπ₯ β β βπ¦ β π΄ π¦ β€ π₯) β§ (π΅ β β β§ π΅ β β β§ βπ₯ β β βπ¦ β π΅ π¦ β€ π₯))) β β’ (π β (πΆ β β β§ πΆ β β β§ βπ₯ β β βπ€ β πΆ π€ β€ π₯)) | ||
Theorem | supmul 12208* | The supremum function distributes over multiplication, in the sense that (supπ΄) Β· (supπ΅) = sup(π΄ Β· π΅), where π΄ Β· π΅ is shorthand for {π Β· π β£ π β π΄, π β π΅} and is defined as πΆ below. We made use of this in our definition of multiplication in the Dedekind cut construction of the reals (see df-mp 10999). (Contributed by Mario Carneiro, 5-Jul-2013.) (Revised by Mario Carneiro, 6-Sep-2014.) |
β’ πΆ = {π§ β£ βπ£ β π΄ βπ β π΅ π§ = (π£ Β· π)} & β’ (π β ((βπ₯ β π΄ 0 β€ π₯ β§ βπ₯ β π΅ 0 β€ π₯) β§ (π΄ β β β§ π΄ β β β§ βπ₯ β β βπ¦ β π΄ π¦ β€ π₯) β§ (π΅ β β β§ π΅ β β β§ βπ₯ β β βπ¦ β π΅ π¦ β€ π₯))) β β’ (π β (sup(π΄, β, < ) Β· sup(π΅, β, < )) = sup(πΆ, β, < )) | ||
Theorem | sup3ii 12209* | A version of the completeness axiom for reals. (Contributed by NM, 23-Aug-1999.) |
β’ (π΄ β β β§ π΄ β β β§ βπ₯ β β βπ¦ β π΄ π¦ β€ π₯) β β’ βπ₯ β β (βπ¦ β π΄ Β¬ π₯ < π¦ β§ βπ¦ β β (π¦ < π₯ β βπ§ β π΄ π¦ < π§)) | ||
Theorem | suprclii 12210* | Closure of supremum of a nonempty bounded set of reals. (Contributed by NM, 12-Sep-1999.) |
β’ (π΄ β β β§ π΄ β β β§ βπ₯ β β βπ¦ β π΄ π¦ β€ π₯) β β’ sup(π΄, β, < ) β β | ||
Theorem | suprubii 12211* | A member of a nonempty bounded set of reals is less than or equal to the set's upper bound. (Contributed by NM, 12-Sep-1999.) |
β’ (π΄ β β β§ π΄ β β β§ βπ₯ β β βπ¦ β π΄ π¦ β€ π₯) β β’ (π΅ β π΄ β π΅ β€ sup(π΄, β, < )) | ||
Theorem | suprlubii 12212* | The supremum of a nonempty bounded set of reals is the least upper bound. (Contributed by NM, 15-Oct-2004.) (Revised by Mario Carneiro, 6-Sep-2014.) |
β’ (π΄ β β β§ π΄ β β β§ βπ₯ β β βπ¦ β π΄ π¦ β€ π₯) β β’ (π΅ β β β (π΅ < sup(π΄, β, < ) β βπ§ β π΄ π΅ < π§)) | ||
Theorem | suprnubii 12213* | An upper bound is not less than the supremum of a nonempty bounded set of reals. (Contributed by NM, 15-Oct-2004.) (Revised by Mario Carneiro, 6-Sep-2014.) |
β’ (π΄ β β β§ π΄ β β β§ βπ₯ β β βπ¦ β π΄ π¦ β€ π₯) β β’ (π΅ β β β (Β¬ π΅ < sup(π΄, β, < ) β βπ§ β π΄ Β¬ π΅ < π§)) | ||
Theorem | suprleubii 12214* | The supremum of a nonempty bounded set of reals is less than or equal to an upper bound. (Contributed by NM, 18-Mar-2005.) (Revised by Mario Carneiro, 6-Sep-2014.) |
β’ (π΄ β β β§ π΄ β β β§ βπ₯ β β βπ¦ β π΄ π¦ β€ π₯) β β’ (π΅ β β β (sup(π΄, β, < ) β€ π΅ β βπ§ β π΄ π§ β€ π΅)) | ||
Theorem | riotaneg 12215* | The negative of the unique real such that π. (Contributed by NM, 13-Jun-2005.) |
β’ (π₯ = -π¦ β (π β π)) β β’ (β!π₯ β β π β (β©π₯ β β π) = -(β©π¦ β β π)) | ||
Theorem | negiso 12216 | Negation is an order anti-isomorphism of the real numbers, which is its own inverse. (Contributed by Mario Carneiro, 24-Dec-2016.) |
β’ πΉ = (π₯ β β β¦ -π₯) β β’ (πΉ Isom < , β‘ < (β, β) β§ β‘πΉ = πΉ) | ||
Theorem | dfinfre 12217* | The infimum of a set of reals π΄. (Contributed by NM, 9-Oct-2005.) (Revised by AV, 4-Sep-2020.) |
β’ (π΄ β β β inf(π΄, β, < ) = βͺ {π₯ β β β£ (βπ¦ β π΄ π₯ β€ π¦ β§ βπ¦ β β (π₯ < π¦ β βπ§ β π΄ π§ < π¦))}) | ||
Theorem | infrecl 12218* | Closure of infimum of a nonempty bounded set of reals. (Contributed by NM, 8-Oct-2005.) (Revised by AV, 4-Sep-2020.) |
β’ ((π΄ β β β§ π΄ β β β§ βπ₯ β β βπ¦ β π΄ π₯ β€ π¦) β inf(π΄, β, < ) β β) | ||
Theorem | infrenegsup 12219* | The infimum of a set of reals π΄ is the negative of the supremum of the negatives of its elements. The antecedent ensures that π΄ is nonempty and has a lower bound. (Contributed by NM, 14-Jun-2005.) (Revised by AV, 4-Sep-2020.) |
β’ ((π΄ β β β§ π΄ β β β§ βπ₯ β β βπ¦ β π΄ π₯ β€ π¦) β inf(π΄, β, < ) = -sup({π§ β β β£ -π§ β π΄}, β, < )) | ||
Theorem | infregelb 12220* | Any lower bound of a nonempty set of real numbers is less than or equal to its infimum. (Contributed by Jeff Hankins, 1-Sep-2013.) (Revised by AV, 4-Sep-2020.) (Proof modification is discouraged.) |
β’ (((π΄ β β β§ π΄ β β β§ βπ₯ β β βπ¦ β π΄ π₯ β€ π¦) β§ π΅ β β) β (π΅ β€ inf(π΄, β, < ) β βπ§ β π΄ π΅ β€ π§)) | ||
Theorem | infrelb 12221* | If a nonempty set of real numbers has a lower bound, its infimum is less than or equal to any of its elements. (Contributed by Jeff Hankins, 15-Sep-2013.) (Revised by AV, 4-Sep-2020.) |
β’ ((π΅ β β β§ βπ₯ β β βπ¦ β π΅ π₯ β€ π¦ β§ π΄ β π΅) β inf(π΅, β, < ) β€ π΄) | ||
Theorem | infrefilb 12222 | The infimum of a finite set of reals is less than or equal to any of its elements. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
β’ ((π΅ β β β§ π΅ β Fin β§ π΄ β π΅) β inf(π΅, β, < ) β€ π΄) | ||
Theorem | supfirege 12223 | The supremum of a finite set of real numbers is greater than or equal to all the real numbers of the set. (Contributed by AV, 1-Oct-2019.) |
β’ (π β π΅ β β) & β’ (π β π΅ β Fin) & β’ (π β πΆ β π΅) & β’ (π β π = sup(π΅, β, < )) β β’ (π β πΆ β€ π) | ||
Theorem | inelr 12224 | The imaginary unit i is not a real number. (Contributed by NM, 6-May-1999.) |
β’ Β¬ i β β | ||
Theorem | rimul 12225 | A real number times the imaginary unit is real only if the number is 0. (Contributed by NM, 28-May-1999.) (Revised by Mario Carneiro, 27-May-2016.) |
β’ ((π΄ β β β§ (i Β· π΄) β β) β π΄ = 0) | ||
Theorem | cru 12226 | The representation of complex numbers in terms of real and imaginary parts is unique. Proposition 10-1.3 of [Gleason] p. 130. (Contributed by NM, 9-May-1999.) (Proof shortened by Mario Carneiro, 27-May-2016.) |
β’ (((π΄ β β β§ π΅ β β) β§ (πΆ β β β§ π· β β)) β ((π΄ + (i Β· π΅)) = (πΆ + (i Β· π·)) β (π΄ = πΆ β§ π΅ = π·))) | ||
Theorem | crne0 12227 | The real representation of complex numbers is nonzero iff one of its terms is nonzero. (Contributed by NM, 29-Apr-2005.) (Proof shortened by Mario Carneiro, 27-May-2016.) |
β’ ((π΄ β β β§ π΅ β β) β ((π΄ β 0 β¨ π΅ β 0) β (π΄ + (i Β· π΅)) β 0)) | ||
Theorem | creur 12228* | The real part of a complex number is unique. Proposition 10-1.3 of [Gleason] p. 130. (Contributed by NM, 9-May-1999.) (Proof shortened by Mario Carneiro, 27-May-2016.) |
β’ (π΄ β β β β!π₯ β β βπ¦ β β π΄ = (π₯ + (i Β· π¦))) | ||
Theorem | creui 12229* | The imaginary part of a complex number is unique. Proposition 10-1.3 of [Gleason] p. 130. (Contributed by NM, 9-May-1999.) (Proof shortened by Mario Carneiro, 27-May-2016.) |
β’ (π΄ β β β β!π¦ β β βπ₯ β β π΄ = (π₯ + (i Β· π¦))) | ||
Theorem | cju 12230* | The complex conjugate of a complex number is unique. (Contributed by Mario Carneiro, 6-Nov-2013.) |
β’ (π΄ β β β β!π₯ β β ((π΄ + π₯) β β β§ (i Β· (π΄ β π₯)) β β)) | ||
Theorem | ofsubeq0 12231 | Function analogue of subeq0 11508. (Contributed by Mario Carneiro, 24-Jul-2014.) |
β’ ((π΄ β π β§ πΉ:π΄βΆβ β§ πΊ:π΄βΆβ) β ((πΉ βf β πΊ) = (π΄ Γ {0}) β πΉ = πΊ)) | ||
Theorem | ofnegsub 12232 | Function analogue of negsub 11530. (Contributed by Mario Carneiro, 24-Jul-2014.) |
β’ ((π΄ β π β§ πΉ:π΄βΆβ β§ πΊ:π΄βΆβ) β (πΉ βf + ((π΄ Γ {-1}) βf Β· πΊ)) = (πΉ βf β πΊ)) | ||
Theorem | ofsubge0 12233 | Function analogue of subge0 11749. (Contributed by Mario Carneiro, 24-Jul-2014.) |
β’ ((π΄ β π β§ πΉ:π΄βΆβ β§ πΊ:π΄βΆβ) β ((π΄ Γ {0}) βr β€ (πΉ βf β πΊ) β πΊ βr β€ πΉ)) | ||
Syntax | cn 12234 | Extend class notation to include the class of positive integers. |
class β | ||
Definition | df-nn 12235 |
Define the set of positive integers. Some authors, especially in analysis
books, call these the natural numbers, whereas other authors choose to
include 0 in their definition of natural numbers. Note that β is a
subset of complex numbers (nnsscn 12239), in contrast to the more elementary
ordinal natural numbers Ο, df-om 7865). See nnind 12252 for the
principle of mathematical induction. See df-n0 12495 for the set of
nonnegative integers β0. See dfn2 12507
for β defined in terms of
β0.
This is a technical definition that helps us avoid the Axiom of Infinity ax-inf2 9656 in certain proofs. For a more conventional and intuitive definition ("the smallest set of reals containing 1 as well as the successor of every member") see dfnn3 12248 (or its slight variant dfnn2 12247). (Contributed by NM, 10-Jan-1997.) (Revised by Mario Carneiro, 3-May-2014.) |
β’ β = (rec((π₯ β V β¦ (π₯ + 1)), 1) β Ο) | ||
Theorem | nnexALT 12236 | Alternate proof of nnex 12240, more direct, that makes use of ax-rep 5279. (Contributed by Mario Carneiro, 3-May-2014.) (Proof modification is discouraged.) (New usage is discouraged.) |
β’ β β V | ||
Theorem | peano5nni 12237* | Peano's inductive postulate. Theorem I.36 (principle of mathematical induction) of [Apostol] p. 34. (Contributed by NM, 10-Jan-1997.) (Revised by Mario Carneiro, 17-Nov-2014.) |
β’ ((1 β π΄ β§ βπ₯ β π΄ (π₯ + 1) β π΄) β β β π΄) | ||
Theorem | nnssre 12238 | The positive integers are a subset of the reals. (Contributed by NM, 10-Jan-1997.) (Revised by Mario Carneiro, 16-Jun-2013.) |
β’ β β β | ||
Theorem | nnsscn 12239 | The positive integers are a subset of the complex numbers. Remark: this could also be proven from nnssre 12238 and ax-resscn 11187 at the cost of using more axioms. (Contributed by NM, 2-Aug-2004.) Reduce dependencies on axioms. (Revised by Steven Nguyen, 4-Oct-2022.) |
β’ β β β | ||
Theorem | nnex 12240 | The set of positive integers exists. (Contributed by NM, 3-Oct-1999.) (Revised by Mario Carneiro, 17-Nov-2014.) |
β’ β β V | ||
Theorem | nnre 12241 | A positive integer is a real number. (Contributed by NM, 18-Aug-1999.) |
β’ (π΄ β β β π΄ β β) | ||
Theorem | nncn 12242 | A positive integer is a complex number. (Contributed by NM, 18-Aug-1999.) |
β’ (π΄ β β β π΄ β β) | ||
Theorem | nnrei 12243 | A positive integer is a real number. (Contributed by NM, 18-Aug-1999.) |
β’ π΄ β β β β’ π΄ β β | ||
Theorem | nncni 12244 | A positive integer is a complex number. (Contributed by NM, 18-Aug-1999.) Reduce dependencies on axioms. (Revised by Steven Nguyen, 4-Oct-2022.) |
β’ π΄ β β β β’ π΄ β β | ||
Theorem | 1nn 12245 | Peano postulate: 1 is a positive integer. (Contributed by NM, 11-Jan-1997.) (Revised by Mario Carneiro, 17-Nov-2014.) |
β’ 1 β β | ||
Theorem | peano2nn 12246 | 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 12247* | Alternate definition of the set of positive integers. This was our original definition, before the current df-nn 12235 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 12248* | 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 12249 | A positive integer is a real number. (Contributed by Mario Carneiro, 27-May-2016.) |
β’ (π β π΄ β β) β β’ (π β π΄ β β) | ||
Theorem | nncnd 12250 | A positive integer is a complex number. (Contributed by Mario Carneiro, 27-May-2016.) |
β’ (π β π΄ β β) β β’ (π β π΄ β β) | ||
Theorem | peano2nnd 12251 | Peano postulate: a successor of a positive integer is a positive integer. (Contributed by Mario Carneiro, 27-May-2016.) |
β’ (π β π΄ β β) β β’ (π β (π΄ + 1) β β) | ||
Theorem | nnind 12252* | 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 12257 for an example of its use. See nn0ind 12679 for induction on nonnegative integers and uzind 12676, uzind4 12912 for induction on an arbitrary upper set of integers. See indstr 12922 for strong induction. See also nnindALT 12253. 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 12253* |
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 12252 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 12254* | Principle of Mathematical Induction (inference schema) on integers, a deduction version. (Contributed by Thierry Arnoux, 19-Jul-2020.) |
β’ (π₯ = 1 β (π β π)) & β’ (π₯ = π¦ β (π β π)) & β’ (π₯ = (π¦ + 1) β (π β π)) & β’ (π₯ = π΄ β (π β π)) & β’ (π β π) & β’ (((π β§ π¦ β β) β§ π) β π) β β’ ((π β§ π΄ β β) β π) | ||
Theorem | nn1m1nn 12255 | Every positive integer is one or a successor. (Contributed by Mario Carneiro, 16-May-2014.) |
β’ (π΄ β β β (π΄ = 1 β¨ (π΄ β 1) β β)) | ||
Theorem | nn1suc 12256* | 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 12257 | Closure of addition of positive integers, proved by induction on the second addend. (Contributed by NM, 12-Jan-1997.) |
β’ ((π΄ β β β§ π΅ β β) β (π΄ + π΅) β β) | ||
Theorem | nnmulcl 12258 | Closure of multiplication of positive integers. (Contributed by NM, 12-Jan-1997.) Remove dependency on ax-mulcom 11194 and ax-mulass 11196. (Revised by Steven Nguyen, 24-Sep-2022.) |
β’ ((π΄ β β β§ π΅ β β) β (π΄ Β· π΅) β β) | ||
Theorem | nnmulcli 12259 | Closure of multiplication of positive integers. (Contributed by Mario Carneiro, 18-Feb-2014.) |
β’ π΄ β β & β’ π΅ β β β β’ (π΄ Β· π΅) β β | ||
Theorem | nnmtmip 12260 | "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 11675, π΄ and π΅ are complex numbers because of nncn 12242, and (π΄ Β· π΅) β β because of nnmulcl 12258. This also holds for positive reals, see rpmtmip 13022. Note that the opposites -π΄ and -π΅ of the positive integers π΄ and π΅ are negative integers. (Contributed by AV, 23-Dec-2022.) |
β’ ((π΄ β β β§ π΅ β β) β (-π΄ Β· -π΅) β β) | ||
Theorem | nn2ge 12261* | There exists a positive integer greater than or equal to any two others. (Contributed by NM, 18-Aug-1999.) |
β’ ((π΄ β β β§ π΅ β β) β βπ₯ β β (π΄ β€ π₯ β§ π΅ β€ π₯)) | ||
Theorem | nnge1 12262 | A positive integer is one or greater. (Contributed by NM, 25-Aug-1999.) |
β’ (π΄ β β β 1 β€ π΄) | ||
Theorem | nngt1ne1 12263 | A positive integer is greater than one iff it is not equal to one. (Contributed by NM, 7-Oct-2004.) |
β’ (π΄ β β β (1 < π΄ β π΄ β 1)) | ||
Theorem | nnle1eq1 12264 | 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 12265 | A positive integer is positive. (Contributed by NM, 26-Sep-1999.) |
β’ (π΄ β β β 0 < π΄) | ||
Theorem | nnnlt1 12266 | A positive integer is not less than one. (Contributed by NM, 18-Jan-2004.) (Revised by Mario Carneiro, 27-May-2016.) |
β’ (π΄ β β β Β¬ π΄ < 1) | ||
Theorem | nnnle0 12267 | A positive integer is not less than or equal to zero. (Contributed by AV, 13-May-2020.) |
β’ (π΄ β β β Β¬ π΄ β€ 0) | ||
Theorem | nnne0 12268 | A positive integer is nonzero. See nnne0ALT 12272 for a shorter proof using ax-pre-mulgt0 11207. This proof avoids 0lt1 11758, and thus ax-pre-mulgt0 11207, by splitting ax-1ne0 11199 into the two separate cases 0 < 1 and 1 < 0. (Contributed by NM, 27-Sep-1999.) Remove dependency on ax-pre-mulgt0 11207. (Revised by Steven Nguyen, 30-Jan-2023.) |
β’ (π΄ β β β π΄ β 0) | ||
Theorem | nnneneg 12269 | No positive integer is equal to its negation. (Contributed by AV, 20-Jun-2023.) |
β’ (π΄ β β β π΄ β -π΄) | ||
Theorem | 0nnn 12270 | Zero is not a positive integer. (Contributed by NM, 25-Aug-1999.) Remove dependency on ax-pre-mulgt0 11207. (Revised by Steven Nguyen, 30-Jan-2023.) |
β’ Β¬ 0 β β | ||
Theorem | 0nnnALT 12271 | Alternate proof of 0nnn 12270, which requires ax-pre-mulgt0 11207 but is not based on nnne0 12268 (and which can therefore be used in nnne0ALT 12272). (Contributed by NM, 25-Aug-1999.) (New usage is discouraged.) (Proof modification is discouraged.) |
β’ Β¬ 0 β β | ||
Theorem | nnne0ALT 12272 | Alternate version of nnne0 12268. A positive integer is nonzero. (Contributed by NM, 27-Sep-1999.) (New usage is discouraged.) (Proof modification is discouraged.) |
β’ (π΄ β β β π΄ β 0) | ||
Theorem | nngt0i 12273 | A positive integer is positive (inference version). (Contributed by NM, 17-Sep-1999.) |
β’ π΄ β β β β’ 0 < π΄ | ||
Theorem | nnne0i 12274 | A positive integer is nonzero (inference version). (Contributed by NM, 25-Aug-1999.) |
β’ π΄ β β β β’ π΄ β 0 | ||
Theorem | nndivre 12275 | The quotient of a real and a positive integer is real. (Contributed by NM, 28-Nov-2008.) |
β’ ((π΄ β β β§ π β β) β (π΄ / π) β β) | ||
Theorem | nnrecre 12276 | The reciprocal of a positive integer is real. (Contributed by NM, 8-Feb-2008.) |
β’ (π β β β (1 / π) β β) | ||
Theorem | nnrecgt0 12277 | The reciprocal of a positive integer is positive. (Contributed by NM, 25-Aug-1999.) |
β’ (π΄ β β β 0 < (1 / π΄)) | ||
Theorem | nnsub 12278 | Subtraction of positive integers. (Contributed by NM, 20-Aug-2001.) (Revised by Mario Carneiro, 16-May-2014.) |
β’ ((π΄ β β β§ π΅ β β) β (π΄ < π΅ β (π΅ β π΄) β β)) | ||
Theorem | nnsubi 12279 | Subtraction of positive integers. (Contributed by NM, 19-Aug-2001.) |
β’ π΄ β β & β’ π΅ β β β β’ (π΄ < π΅ β (π΅ β π΄) β β) | ||
Theorem | nndiv 12280* | Two ways to express "π΄ divides π΅ " for positive integers. (Contributed by NM, 3-Feb-2004.) (Proof shortened by Mario Carneiro, 16-May-2014.) |
β’ ((π΄ β β β§ π΅ β β) β (βπ₯ β β (π΄ Β· π₯) = π΅ β (π΅ / π΄) β β)) | ||
Theorem | nndivtr 12281 | 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 12282 | A positive integer is one or greater. (Contributed by Mario Carneiro, 27-May-2016.) |
β’ (π β π΄ β β) β β’ (π β 1 β€ π΄) | ||
Theorem | nngt0d 12283 | A positive integer is positive. (Contributed by Mario Carneiro, 27-May-2016.) |
β’ (π β π΄ β β) β β’ (π β 0 < π΄) | ||
Theorem | nnne0d 12284 | A positive integer is nonzero. (Contributed by Mario Carneiro, 27-May-2016.) |
β’ (π β π΄ β β) β β’ (π β π΄ β 0) | ||
Theorem | nnrecred 12285 | The reciprocal of a positive integer is real. (Contributed by Mario Carneiro, 27-May-2016.) |
β’ (π β π΄ β β) β β’ (π β (1 / π΄) β β) | ||
Theorem | nnaddcld 12286 | Closure of addition of positive integers. (Contributed by Mario Carneiro, 27-May-2016.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) β β’ (π β (π΄ + π΅) β β) | ||
Theorem | nnmulcld 12287 | Closure of multiplication of positive integers. (Contributed by Mario Carneiro, 27-May-2016.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) β β’ (π β (π΄ Β· π΅) β β) | ||
Theorem | nndivred 12288 | 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 11137 through df-9 12304), 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 11137 and df-1 11138). With the decimal constructor df-dec 12700, it is possible to easily express larger integers in base 10. See deccl 12714 and the theorems that follow it. See also 4001prm 17105 (4001 is prime) and the proof of bpos 27213. 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 16156. 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 12289 | Extend class notation to include the number 2. |
class 2 | ||
Syntax | c3 12290 | Extend class notation to include the number 3. |
class 3 | ||
Syntax | c4 12291 | Extend class notation to include the number 4. |
class 4 | ||
Syntax | c5 12292 | Extend class notation to include the number 5. |
class 5 | ||
Syntax | c6 12293 | Extend class notation to include the number 6. |
class 6 | ||
Syntax | c7 12294 | Extend class notation to include the number 7. |
class 7 | ||
Syntax | c8 12295 | Extend class notation to include the number 8. |
class 8 | ||
Syntax | c9 12296 | Extend class notation to include the number 9. |
class 9 | ||
Definition | df-2 12297 | Define the number 2. (Contributed by NM, 27-May-1999.) |
β’ 2 = (1 + 1) | ||
Definition | df-3 12298 | Define the number 3. (Contributed by NM, 27-May-1999.) |
β’ 3 = (2 + 1) | ||
Definition | df-4 12299 | Define the number 4. (Contributed by NM, 27-May-1999.) |
β’ 4 = (3 + 1) | ||
Definition | df-5 12300 | Define the number 5. (Contributed by NM, 27-May-1999.) |
β’ 5 = (4 + 1) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |