P. 105 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 10401-10500   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	lemul1ad 10401	Multiplication of both sides of 'less than or equal to' by a nonnegative number. (Contributed by Mario Carneiro, 28-May-2016.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> C e. RR )   &    |- ( ph -> 0 <_ C )   &    |- ( ph -> A <_ B )   =>    |- ( ph -> ( A x. C ) <_ ( B x. C ) )
Theorem	lemul2ad 10402	Multiplication of both sides of 'less than or equal to' by a nonnegative number. (Contributed by Mario Carneiro, 28-May-2016.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> C e. RR )   &    |- ( ph -> 0 <_ C )   &    |- ( ph -> A <_ B )   =>    |- ( ph -> ( C x. A ) <_ ( C x. B ) )
Theorem	ltmul12ad 10403	Comparison of product of two positive numbers. (Contributed by Mario Carneiro, 28-May-2016.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> C e. RR )   &    |- ( ph -> D e. RR )   &    |- ( ph -> 0 <_ A )   &    |- ( ph -> A < B )   &    |- ( ph -> 0 <_ C )   &    |- ( ph -> C < D )   =>    |- ( ph -> ( A x. C ) < ( B x. D ) )
Theorem	lemul12ad 10404	Comparison of product of two nonnegative numbers. (Contributed by Mario Carneiro, 28-May-2016.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> C e. RR )   &    |- ( ph -> D e. RR )   &    |- ( ph -> 0 <_ A )   &    |- ( ph -> 0 <_ C )   &    |- ( ph -> A <_ B )   &    |- ( ph -> C <_ D )   =>    |- ( ph -> ( A x. C ) <_ ( B x. D ) )
Theorem	lemul12bd 10405	Comparison of product of two nonnegative numbers. (Contributed by Mario Carneiro, 28-May-2016.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> C e. RR )   &    |- ( ph -> D e. RR )   &    |- ( ph -> 0 <_ A )   &    |- ( ph -> 0 <_ D )   &    |- ( ph -> A <_ B )   &    |- ( ph -> C <_ D )   =>    |- ( ph -> ( A x. C ) <_ ( B x. D ) )
5.3.8  Completeness Axiom and Suprema
Theorem	fimaxre 10406*	A finite set of real numbers has a maximum. (Contributed by Jeff Madsen, 2-Sep-2009.)
|- ( ( A C_ RR /\ A e. Fin /\ A =/= (/) ) -> E. x e. A A. y e. A y <_ x )
Theorem	fimaxre2 10407*	A nonempty finite set of real numbers has a maximum. (Contributed by Jeff Madsen, 27-May-2011.) (Revised by Mario Carneiro, 13-Feb-2014.)
|- ( ( A C_ RR /\ A e. Fin ) -> E. x e. RR A. y e. A y <_ x )
Theorem	fimaxre3 10408*	A nonempty finite set of real numbers has a maximum (image set version). (Contributed by Mario Carneiro, 13-Feb-2014.)
|- ( ( A e. Fin /\ A. y e. A B e. RR ) -> E. x e. RR A. y e. A B <_ x )
Theorem	lbreu 10409*	If a set of reals contains a lower bound, it contains a unique lower bound. (Contributed by NM, 9-Oct-2005.)
|- ( ( S C_ RR /\ E. x e. S A. y e. S x <_ y ) -> E! x e. S A. y e. S x <_ y )
Theorem	lbcl 10410*	If a set of reals contains a lower bound, it contains a unique lower bound that belongs to the set. (Contributed by NM, 9-Oct-2005.) (Revised by Mario Carneiro, 24-Dec-2016.)
|- ( ( S C_ RR /\ E. x e. S A. y e. S x <_ y ) -> ( iota_ x e. S A. y e. S x <_ y ) e. S )
Theorem	lble 10411*	If a set of reals contains a lower bound, the lower bound is less than or equal to all members of the set. (Contributed by NM, 9-Oct-2005.) (Proof shortened by Mario Carneiro, 24-Dec-2016.)
|- ( ( S C_ RR /\ E. x e. S A. y e. S x <_ y /\ A e. S ) -> ( iota_ x e. S A. y e. S x <_ y ) <_ A )
Theorem	lbinfm 10412*	If a set of reals contains a lower bound, the lower bound is its infimum. (Contributed by NM, 9-Oct-2005.) (Revised by Mario Carneiro, 16-Jun-2013.)
|- ( ( S C_ RR /\ E. x e. S A. y e. S x <_ y ) -> sup ( S , RR , `' < ) = ( iota_ x e. S A. y e. S x <_ y ) )
Theorem	lbinfmcl 10413*	If a set of reals contains a lower bound, it contains its infimum. (Contributed by NM, 11-Oct-2005.)
|- ( ( S C_ RR /\ E. x e. S A. y e. S x <_ y ) -> sup ( S , RR , `' < ) e. S )
Theorem	lbinfmle 10414*	If a set of reals contains a lower bound, its infimum is less than or equal to all members of the set. (Contributed by NM, 11-Oct-2005.)
|- ( ( S C_ RR /\ E. x e. S A. y e. S x <_ y /\ A e. S ) -> sup ( S , RR , `' < ) <_ A )
Theorem	sup2 10415*	A nonempty, bounded-above set of reals has a supremum. Stronger version of completeness axiom (it has a slightly weaker antecedent). (Contributed by NM, 19-Jan-1997.)
|- ( ( A C_ RR /\ A =/= (/) /\ E. x e. RR A. y e. A ( y < x \/ y = x ) ) -> E. x e. RR ( A. y e. A -. x < y /\ A. y e. RR ( y < x -> E. z e. A y < z ) ) )
Theorem	sup3 10416*	A version of the completeness axiom for reals. (Contributed by NM, 12-Oct-2004.)
|- ( ( A C_ RR /\ A =/= (/) /\ E. x e. RR A. y e. A y <_ x ) -> E. x e. RR ( A. y e. A -. x < y /\ A. y e. RR ( y < x -> E. z e. A y < z ) ) )
Theorem	infm3lem 10417*	Lemma for infm3 10418. (Contributed by NM, 14-Jun-2005.)
|- ( x e. RR -> E. y e. RR x = -u y )
Theorem	infm3 10418*	The completeness axiom for reals in terms of infimum: a nonempty, bounded-below set of reals has an infimum. (This theorem is the dual of sup3 10416.) (Contributed by NM, 14-Jun-2005.)
|- ( ( A C_ RR /\ A =/= (/) /\ E. x e. RR A. y e. A x <_ y ) -> E. x e. RR ( A. y e. A -. y < x /\ A. y e. RR ( x < y -> E. z e. A z < y ) ) )
Theorem	suprcl 10419*	Closure of supremum of a nonempty bounded set of reals. (Contributed by NM, 12-Oct-2004.)
|- ( ( A C_ RR /\ A =/= (/) /\ E. x e. RR A. y e. A y <_ x ) -> sup ( A , RR , < ) e. RR )
Theorem	suprub 10420*	A member of a nonempty bounded set of reals is less than or equal to the set's upper bound. (Contributed by NM, 12-Oct-2004.)
|- ( ( ( A C_ RR /\ A =/= (/) /\ E. x e. RR A. y e. A y <_ x ) /\ B e. A ) -> B <_ sup ( A , RR , < ) )
Theorem	suprlub 10421*	The supremum of a nonempty bounded set of reals is the least upper bound. (Contributed by NM, 15-Nov-2004.) (Revised by Mario Carneiro, 6-Sep-2014.)
|- ( ( ( A C_ RR /\ A =/= (/) /\ E. x e. RR A. y e. A y <_ x ) /\ B e. RR ) -> ( B < sup ( A , RR , < ) <-> E. z e. A B < z ) )
Theorem	suprnub 10422*	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.)
|- ( ( ( A C_ RR /\ A =/= (/) /\ E. x e. RR A. y e. A y <_ x ) /\ B e. RR ) -> ( -. B < sup ( A , RR , < ) <-> A. z e. A -. B < z ) )
Theorem	suprleub 10423*	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.)
|- ( ( ( A C_ RR /\ A =/= (/) /\ E. x e. RR A. y e. A y <_ x ) /\ B e. RR ) -> ( sup ( A , RR , < ) <_ B <-> A. z e. A z <_ B ) )
Theorem	supmul1 10424*	The supremum function distributes over multiplication, in the sense that A x. ( sup B ) = sup ( A x. B ), where A x. B is shorthand for { A x. b | b e. B } and is defined as C below. This is the simple version, with only one set argument; see supmul 10427 for the more general case with two set arguments. (Contributed by Mario Carneiro, 5-Jul-2013.)
|- C = { z | E. v e. B z = ( A x. v ) }   &    |- ( ph <-> ( ( A e. RR /\ 0 <_ A /\ A. x e. B 0 <_ x ) /\ ( B C_ RR /\ B =/= (/) /\ E. x e. RR A. y e. B y <_ x ) ) )   =>    |- ( ph -> ( A x. sup ( B , RR , < ) ) = sup ( C , RR , < ) )
Theorem	supmullem1 10425*	Lemma for supmul 10427. (Contributed by Mario Carneiro, 5-Jul-2013.)
|- C = { z | E. v e. A E. b e. B z = ( v x. b ) }   &    |- ( ph <-> ( ( A. x e. A 0 <_ x /\ A. x e. B 0 <_ x ) /\ ( A C_ RR /\ A =/= (/) /\ E. x e. RR A. y e. A y <_ x ) /\ ( B C_ RR /\ B =/= (/) /\ E. x e. RR A. y e. B y <_ x ) ) )   =>    |- ( ph -> A. w e. C w <_ ( sup ( A , RR , < ) x. sup ( B , RR , < ) ) )
Theorem	supmullem2 10426*	Lemma for supmul 10427. (Contributed by Mario Carneiro, 5-Jul-2013.)
|- C = { z | E. v e. A E. b e. B z = ( v x. b ) }   &    |- ( ph <-> ( ( A. x e. A 0 <_ x /\ A. x e. B 0 <_ x ) /\ ( A C_ RR /\ A =/= (/) /\ E. x e. RR A. y e. A y <_ x ) /\ ( B C_ RR /\ B =/= (/) /\ E. x e. RR A. y e. B y <_ x ) ) )   =>    |- ( ph -> ( C C_ RR /\ C =/= (/) /\ E. x e. RR A. w e. C w <_ x ) )
Theorem	supmul 10427*	The supremum function distributes over multiplication, in the sense that ( sup A ) x. ( sup B ) = sup ( A x. B ), where A x. B is shorthand for { a x. b | a e. A , b e. B } and is defined as C below. We made use of this in our definition of multiplication in the Dedekind cut construction of the reals (see df-mp 9273). (Contributed by Mario Carneiro, 5-Jul-2013.) (Revised by Mario Carneiro, 6-Sep-2014.)
|- C = { z | E. v e. A E. b e. B z = ( v x. b ) }   &    |- ( ph <-> ( ( A. x e. A 0 <_ x /\ A. x e. B 0 <_ x ) /\ ( A C_ RR /\ A =/= (/) /\ E. x e. RR A. y e. A y <_ x ) /\ ( B C_ RR /\ B =/= (/) /\ E. x e. RR A. y e. B y <_ x ) ) )   =>    |- ( ph -> ( sup ( A , RR , < ) x. sup ( B , RR , < ) ) = sup ( C , RR , < ) )
Theorem	sup3ii 10428*	A version of the completeness axiom for reals. (Contributed by NM, 23-Aug-1999.)
|- ( A C_ RR /\ A =/= (/) /\ E. x e. RR A. y e. A y <_ x )   =>    |- E. x e. RR ( A. y e. A -. x < y /\ A. y e. RR ( y < x -> E. z e. A y < z ) )
Theorem	suprclii 10429*	Closure of supremum of a nonempty bounded set of reals. (Contributed by NM, 12-Sep-1999.)
|- ( A C_ RR /\ A =/= (/) /\ E. x e. RR A. y e. A y <_ x )   =>    |- sup ( A , RR , < ) e. RR
Theorem	suprubii 10430*	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.)
|- ( A C_ RR /\ A =/= (/) /\ E. x e. RR A. y e. A y <_ x )   =>    |- ( B e. A -> B <_ sup ( A , RR , < ) )
Theorem	suprlubii 10431*	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.)
|- ( A C_ RR /\ A =/= (/) /\ E. x e. RR A. y e. A y <_ x )   =>    |- ( B e. RR -> ( B < sup ( A , RR , < ) <-> E. z e. A B < z ) )
Theorem	suprnubii 10432*	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.)
|- ( A C_ RR /\ A =/= (/) /\ E. x e. RR A. y e. A y <_ x )   =>    |- ( B e. RR -> ( -. B < sup ( A , RR , < ) <-> A. z e. A -. B < z ) )
Theorem	suprleubii 10433*	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.)
|- ( A C_ RR /\ A =/= (/) /\ E. x e. RR A. y e. A y <_ x )   =>    |- ( B e. RR -> ( sup ( A , RR , < ) <_ B <-> A. z e. A z <_ B ) )
Theorem	riotaneg 10434*	The negative of the unique real such that ph. (Contributed by NM, 13-Jun-2005.)
|- ( x = -u y -> ( ph <-> ps ) )   =>    |- ( E! x e. RR ph -> ( iota_ x e. RR ph ) = -u ( iota_ y e. RR ps ) )
Theorem	negiso 10435	Negation is an order anti-isomorphism of the real numbers, which is its own inverse. (Contributed by Mario Carneiro, 24-Dec-2016.)
|- F = ( x e. RR |-> -u x )   =>    |- ( F Isom < , `' < ( RR , RR ) /\ `' F = F )
Theorem	dfinfmr 10436*	The infimum (expressed as supremum with converse 'less-than') of a set of reals A. (Contributed by NM, 9-Oct-2005.)
|- ( A C_ RR -> sup ( A , RR , `' < ) = U. { x e. RR | ( A. y e. A x <_ y /\ A. y e. RR ( x < y -> E. z e. A z < y ) ) } )
Theorem	infmsup 10437*	The infimum (expressed as supremum with converse 'less-than') of a set of reals A is the negative of the supremum of the negatives of its elements. The antecedent ensures that A is nonempty and has a lower bound. (Contributed by NM, 14-Jun-2005.) (Proof shortened by Mario Carneiro, 24-Dec-2016.)
|- ( ( A C_ RR /\ A =/= (/) /\ E. x e. RR A. y e. A x <_ y ) -> sup ( A , RR , `' < ) = -u sup ( { z e. RR | -u z e. A } , RR , < ) )
Theorem	infmrcl 10438*	Closure of infimum of a nonempty bounded set of reals. (Contributed by NM, 8-Oct-2005.)
|- ( ( A C_ RR /\ A =/= (/) /\ E. x e. RR A. y e. A x <_ y ) -> sup ( A , RR , `' < ) e. RR )
Theorem	infmrgelb 10439*	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 Mario Carneiro, 6-Sep-2014.)
|- ( ( ( A C_ RR /\ A =/= (/) /\ E. x e. RR A. y e. A x <_ y ) /\ B e. RR ) -> ( B <_ sup ( A , RR , `' < ) <-> A. z e. A B <_ z ) )
Theorem	infmrlb 10440*	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.)
|- ( ( B C_ RR /\ E. x e. RR A. y e. B x <_ y /\ A e. B ) -> sup ( B , RR , `' < ) <_ A )
Theorem	supfirege 10441	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.)
|- ( ph -> B C_ RR )   &    |- ( ph -> B e. Fin )   &    |- ( ph -> C e. B )   &    |- ( ph -> S = sup ( B , RR , < ) )   =>    |- ( ph -> C <_ S )
5.3.9  Imaginary and complex number properties
Theorem	inelr 10442	The imaginary unit _i is not a real number. (Contributed by NM, 6-May-1999.)
|- -. _i e. RR
Theorem	rimul 10443	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.)
|- ( ( A e. RR /\ ( _i x. A ) e. RR ) -> A = 0 )
Theorem	cru 10444	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.)
|- ( ( ( A e. RR /\ B e. RR ) /\ ( C e. RR /\ D e. RR ) ) -> ( ( A + ( _i x. B ) ) = ( C + ( _i x. D ) ) <-> ( A = C /\ B = D ) ) )
Theorem	crne0 10445	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.)
|- ( ( A e. RR /\ B e. RR ) -> ( ( A =/= 0 \/ B =/= 0 ) <-> ( A + ( _i x. B ) ) =/= 0 ) )
Theorem	creur 10446*	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.)
|- ( A e. CC -> E! x e. RR E. y e. RR A = ( x + ( _i x. y ) ) )
Theorem	creui 10447*	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.)
|- ( A e. CC -> E! y e. RR E. x e. RR A = ( x + ( _i x. y ) ) )
Theorem	cju 10448*	The complex conjugate of a complex number is unique. (Contributed by Mario Carneiro, 6-Nov-2013.)
|- ( A e. CC -> E! x e. CC ( ( A + x ) e. RR /\ ( _i x. ( A - x ) ) e. RR ) )
5.3.10  Function operation analogue theorems
Theorem	ofsubeq0 10449	Function analog of subeq0 9758. (Contributed by Mario Carneiro, 24-Jul-2014.)
|- ( ( A e. V /\ F : A --> CC /\ G : A --> CC ) -> ( ( F oF - G ) = ( A X. { 0 } ) <-> F = G ) )
Theorem	ofnegsub 10450	Function analog of negsub 9780. (Contributed by Mario Carneiro, 24-Jul-2014.)
|- ( ( A e. V /\ F : A --> CC /\ G : A --> CC ) -> ( F oF + ( ( A X. { -u 1 } ) oF x. G ) ) = ( F oF - G ) )
Theorem	ofsubge0 10451	Function analog of subge0 9983. (Contributed by Mario Carneiro, 24-Jul-2014.)
|- ( ( A e. V /\ F : A --> RR /\ G : A --> RR ) -> ( ( A X. { 0 } ) oR <_ ( F oF - G ) <-> G oR <_ F ) )
5.4  Integer sets
5.4.1  Positive integers (as a subset of complex numbers)
Syntax	cn 10452	Extend class notation to include the class of positive integers.
class NN
Definition	df-nn 10453	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 NN is a subset of complex numbers (nnsscn 10457), in contrast to the more elementary ordinal natural numbers om, df-om 6600). See nnind 10470 for the principle of mathematical induction. See df-n0 10713 for the set of nonnegative integers NN0. See dfn2 10725 for NN defined in terms of NN0. This is a technical definition that helps us avoid the Axiom of Infinity ax-inf2 7972 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 10466 (or its slight variant dfnn2 10465). (Contributed by NM, 10-Jan-1997.) (Revised by Mario Carneiro, 3-May-2014.)
|- NN = ( rec ( ( x e. _V |-> ( x + 1 ) ) , 1 ) " om )
Theorem	nnexALT 10454	Alternate proof of nnex 10458, more direct. (Contributed by NM, 3-Oct-1999.) (Revised by Mario Carneiro, 3-May-2014.) (Proof modification is discouraged.) (New usage is discouraged.)
|- NN e. _V
Theorem	peano5nni 10455*	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 e. A /\ A. x e. A ( x + 1 ) e. A ) -> NN C_ A )
Theorem	nnssre 10456	The positive integers are a subset of the reals. (Contributed by NM, 10-Jan-1997.) (Revised by Mario Carneiro, 16-Jun-2013.)
|- NN C_ RR
Theorem	nnsscn 10457	The positive integers are a subset of the complex numbers. (Contributed by NM, 2-Aug-2004.)
|- NN C_ CC
Theorem	nnex 10458	The set of positive integers exists. (Contributed by NM, 3-Oct-1999.) (Revised by Mario Carneiro, 17-Nov-2014.)
|- NN e. _V
Theorem	nnre 10459	A positive integer is a real number. (Contributed by NM, 18-Aug-1999.)
|- ( A e. NN -> A e. RR )
Theorem	nncn 10460	A positive integer is a complex number. (Contributed by NM, 18-Aug-1999.)
|- ( A e. NN -> A e. CC )
Theorem	nnrei 10461	A positive integer is a real number. (Contributed by NM, 18-Aug-1999.)
|- A e. NN   =>    |- A e. RR
Theorem	nncni 10462	A positive integer is a complex number. (Contributed by NM, 18-Aug-1999.)
|- A e. NN   =>    |- A e. CC
Theorem	1nn 10463	Peano postulate: 1 is a positive integer. (Contributed by NM, 11-Jan-1997.) (Revised by Mario Carneiro, 17-Nov-2014.)
|- 1 e. NN
Theorem	peano2nn 10464	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.)
|- ( A e. NN -> ( A + 1 ) e. NN )
Theorem	dfnn2 10465*	Alternate definition of the set of positive integers. This was our original definition, before the current df-nn 10453 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.)
|- NN = |^| { x | ( 1 e. x /\ A. y e. x ( y + 1 ) e. x ) }
Theorem	dfnn3 10466*	Alternate definition of the set of positive integers. Definition of positive integers in [Apostol] p. 22. (Contributed by NM, 3-Jul-2005.)
|- NN = |^| { x | ( x C_ RR /\ 1 e. x /\ A. y e. x ( y + 1 ) e. x ) }
Theorem	nnred 10467	A positive integer is a real number. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. NN )   =>    |- ( ph -> A e. RR )
Theorem	nncnd 10468	A positive integer is a complex number. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. NN )   =>    |- ( ph -> A e. CC )
Theorem	peano2nnd 10469	Peano postulate: a successor of a positive integer is a positive integer. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. NN )   =>    |- ( ph -> ( A + 1 ) e. NN )
5.4.2  Principle of mathematical induction
Theorem	nnind 10470*	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 10474 for an example of its use. See nn0ind 10874 for induction on nonnegative integers and uzind 10871, uzind4 11059 for induction on an arbitrary upper set of integers. See indstr 11069 for strong induction. See also nnindALT 10471. This is an alternative for Metamath 100 proof #74. (Contributed by NM, 10-Jan-1997.) (Revised by Mario Carneiro, 16-Jun-2013.)
|- ( x = 1 -> ( ph <-> ps ) )   &    |- ( x = y -> ( ph <-> ch ) )   &    |- ( x = ( y + 1 ) -> ( ph <-> th ) )   &    |- ( x = A -> ( ph <-> ta ) )   &    |- ps   &    |- ( y e. NN -> ( ch -> th ) )   =>    |- ( A e. NN -> ta )
Theorem	nnindALT 10471*	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 10470 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 /allow". (Contributed by NM, 7-Dec-2005.) (New usage is discouraged.) (Proof modification is discouraged.)
|- ( y e. NN -> ( ch -> th ) )   &    |- ps   &    |- ( x = 1 -> ( ph <-> ps ) )   &    |- ( x = y -> ( ph <-> ch ) )   &    |- ( x = ( y + 1 ) -> ( ph <-> th ) )   &    |- ( x = A -> ( ph <-> ta ) )   =>    |- ( A e. NN -> ta )
Theorem	nn1m1nn 10472	Every positive integer is one or a successor. (Contributed by Mario Carneiro, 16-May-2014.)
|- ( A e. NN -> ( A = 1 \/ ( A - 1 ) e. NN ) )
Theorem	nn1suc 10473*	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.)
|- ( x = 1 -> ( ph <-> ps ) )   &    |- ( x = ( y + 1 ) -> ( ph <-> ch ) )   &    |- ( x = A -> ( ph <-> th ) )   &    |- ps   &    |- ( y e. NN -> ch )   =>    |- ( A e. NN -> th )
Theorem	nnaddcl 10474	Closure of addition of positive integers, proved by induction on the second addend. (Contributed by NM, 12-Jan-1997.)
|- ( ( A e. NN /\ B e. NN ) -> ( A + B ) e. NN )
Theorem	nnmulcl 10475	Closure of multiplication of positive integers. (Contributed by NM, 12-Jan-1997.)
|- ( ( A e. NN /\ B e. NN ) -> ( A x. B ) e. NN )
Theorem	nnmulcli 10476	Closure of multiplication of positive integers. (Contributed by Mario Carneiro, 18-Feb-2014.)
|- A e. NN   &    |- B e. NN   =>    |- ( A x. B ) e. NN
Theorem	nn2ge 10477*	There exists a positive integer greater than or equal to any two others. (Contributed by NM, 18-Aug-1999.)
|- ( ( A e. NN /\ B e. NN ) -> E. x e. NN ( A <_ x /\ B <_ x ) )
Theorem	nnge1 10478	A positive integer is one or greater. (Contributed by NM, 25-Aug-1999.)
|- ( A e. NN -> 1 <_ A )
Theorem	nngt1ne1 10479	A positive integer is greater than one iff it is not equal to one. (Contributed by NM, 7-Oct-2004.)
|- ( A e. NN -> ( 1 < A <-> A =/= 1 ) )
Theorem	nnle1eq1 10480	A positive integer is less than or equal to one iff it is equal to one. (Contributed by NM, 3-Apr-2005.)
|- ( A e. NN -> ( A <_ 1 <-> A = 1 ) )
Theorem	nngt0 10481	A positive integer is positive. (Contributed by NM, 26-Sep-1999.)
|- ( A e. NN -> 0 < A )
Theorem	nnnlt1 10482	A positive integer is not less than one. (Contributed by NM, 18-Jan-2004.) (Revised by Mario Carneiro, 27-May-2016.)
|- ( A e. NN -> -. A < 1 )
Theorem	nnnle0 10483	A positive integer is not less than or equal to zero . (Contributed by AV, 13-May-2020.)
|- ( A e. NN -> -. A <_ 0 )
Theorem	0nnn 10484	Zero is not a positive integer. (Contributed by NM, 25-Aug-1999.)
|- -. 0 e. NN
Theorem	nnne0 10485	A positive integer is nonzero. (Contributed by NM, 27-Sep-1999.)
|- ( A e. NN -> A =/= 0 )
Theorem	nngt0i 10486	A positive integer is positive (inference version). (Contributed by NM, 17-Sep-1999.)
|- A e. NN   =>    |- 0 < A
Theorem	nnne0i 10487	A positive integer is nonzero (inference version). (Contributed by NM, 25-Aug-1999.)
|- A e. NN   =>    |- A =/= 0
Theorem	nndivre 10488	The quotient of a real and a positive integer is real. (Contributed by NM, 28-Nov-2008.)
|- ( ( A e. RR /\ N e. NN ) -> ( A / N ) e. RR )
Theorem	nnrecre 10489	The reciprocal of a positive integer is real. (Contributed by NM, 8-Feb-2008.)
|- ( N e. NN -> ( 1 / N ) e. RR )
Theorem	nnrecgt0 10490	The reciprocal of a positive integer is positive. (Contributed by NM, 25-Aug-1999.)
|- ( A e. NN -> 0 < ( 1 / A ) )
Theorem	nnsub 10491	Subtraction of positive integers. (Contributed by NM, 20-Aug-2001.) (Revised by Mario Carneiro, 16-May-2014.)
|- ( ( A e. NN /\ B e. NN ) -> ( A < B <-> ( B - A ) e. NN ) )
Theorem	nnsubi 10492	Subtraction of positive integers. (Contributed by NM, 19-Aug-2001.)
|- A e. NN   &    |- B e. NN   =>    |- ( A < B <-> ( B - A ) e. NN )
Theorem	nndiv 10493*	Two ways to express " A divides B " for positive integers. (Contributed by NM, 3-Feb-2004.) (Proof shortened by Mario Carneiro, 16-May-2014.)
|- ( ( A e. NN /\ B e. NN ) -> ( E. x e. NN ( A x. x ) = B <-> ( B / A ) e. NN ) )
Theorem	nndivtr 10494	Transitive property of divisibility: if A divides B and B divides C, then A divides C. Typically, C would be an integer, although the theorem holds for complex C. (Contributed by NM, 3-May-2005.)
|- ( ( ( A e. NN /\ B e. NN /\ C e. CC ) /\ ( ( B / A ) e. NN /\ ( C / B ) e. NN ) ) -> ( C / A ) e. NN )
Theorem	nnge1d 10495	A positive integer is one or greater. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. NN )   =>    |- ( ph -> 1 <_ A )
Theorem	nngt0d 10496	A positive integer is positive. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. NN )   =>    |- ( ph -> 0 < A )
Theorem	nnne0d 10497	A positive integer is nonzero. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. NN )   =>    |- ( ph -> A =/= 0 )
Theorem	nnrecred 10498	The reciprocal of a positive integer is real. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. NN )   =>    |- ( ph -> ( 1 / A ) e. RR )
Theorem	nnaddcld 10499	Closure of addition of positive integers. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. NN )   &    |- ( ph -> B e. NN )   =>    |- ( ph -> ( A + B ) e. NN )
Theorem	nnmulcld 10500	Closure of multiplication of positive integers. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. NN )   &    |- ( ph -> B e. NN )   =>    |- ( ph -> ( A x. B ) e. NN )