P. 101 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 10001-10100   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	uzaddcl 10001	Addition closure law for an upper set of integers. (Contributed by NM, 4-Jun-2006.)
|- ( ( N e. ( ZZ>= ` M ) /\ K e. NN0 ) -> ( N + K ) e. ( ZZ>= ` M ) )
Theorem	nn0pzuz 10002	The sum of a nonnegative integer and an integer is an integer greater than or equal to that integer. (Contributed by Alexander van der Vekens, 3-Oct-2018.)
|- ( ( N e. NN0 /\ Z e. ZZ ) -> ( N + Z ) e. ( ZZ>= ` Z ) )
Theorem	uzind4 10003*	Induction on the upper set of integers that starts at an integer M. The first four hypotheses give us the substitution instances we need, and the last two are the basis and the induction step. (Contributed by NM, 7-Sep-2005.)
|- ( j = M -> ( ph <-> ps ) )   &    |- ( j = k -> ( ph <-> ch ) )   &    |- ( j = ( k + 1 ) -> ( ph <-> th ) )   &    |- ( j = N -> ( ph <-> ta ) )   &    |- ( M e. ZZ -> ps )   &    |- ( k e. ( ZZ>= ` M ) -> ( ch -> th ) )   =>    |- ( N e. ( ZZ>= ` M ) -> ta )
Theorem	uzind4ALT 10004*	Induction on the upper set of integers that starts at an integer M. The last four hypotheses give us the substitution instances we need; the first two are the basis and the induction step. Either uzind4 10003 or uzind4ALT 10004 may be used; see comment for nnind 9329. (Contributed by NM, 7-Sep-2005.) (New usage is discouraged.) (Proof modification is discouraged.)
|- ( M e. ZZ -> ps )   &    |- ( k e. ( ZZ>= ` M ) -> ( ch -> th ) )   &    |- ( j = M -> ( ph <-> ps ) )   &    |- ( j = k -> ( ph <-> ch ) )   &    |- ( j = ( k + 1 ) -> ( ph <-> th ) )   &    |- ( j = N -> ( ph <-> ta ) )   =>    |- ( N e. ( ZZ>= ` M ) -> ta )
Theorem	uzind4s 10005*	Induction on the upper set of integers that starts at an integer M, using explicit substitution. The hypotheses are the basis and the induction step. (Contributed by NM, 4-Nov-2005.)
|- ( M e. ZZ -> [. M / k ]. ph )   &    |- ( k e. ( ZZ>= ` M ) -> ( ph -> [. ( k + 1 ) / k ]. ph ) )   =>    |- ( N e. ( ZZ>= ` M ) -> [. N / k ]. ph )
Theorem	uzind4s2 10006*	Induction on the upper set of integers that starts at an integer M, using explicit substitution. The hypotheses are the basis and the induction step. Use this instead of uzind4s 10005 when j and k must be distinct in [. ( k + 1 ) / j ]. ph. (Contributed by NM, 16-Nov-2005.)
|- ( M e. ZZ -> [. M / j ]. ph )   &    |- ( k e. ( ZZ>= ` M ) -> ( [. k / j ]. ph -> [. ( k + 1 ) / j ]. ph ) )   =>    |- ( N e. ( ZZ>= ` M ) -> [. N / j ]. ph )
Theorem	uzind4i 10007*	Induction on the upper integers that start at M. The first four give us the substitution instances we need, and the last two are the basis and the induction step. This is a stronger version of uzind4 10003 assuming that ps holds unconditionally. Notice that N e. ( ZZ>= ` M ) implies that the lower bound M is an integer ( M e. ZZ, see eluzel2 9941). (Contributed by NM, 4-Sep-2005.) (Revised by AV, 13-Jul-2022.)
|- ( j = M -> ( ph <-> ps ) )   &    |- ( j = k -> ( ph <-> ch ) )   &    |- ( j = ( k + 1 ) -> ( ph <-> th ) )   &    |- ( j = N -> ( ph <-> ta ) )   &    |- ps   &    |- ( k e. ( ZZ>= ` M ) -> ( ch -> th ) )   =>    |- ( N e. ( ZZ>= ` M ) -> ta )
Theorem	indstr 10008*	Strong Mathematical Induction for positive integers (inference schema). (Contributed by NM, 17-Aug-2001.)
|- ( x = y -> ( ph <-> ps ) )   &    |- ( x e. NN -> ( A. y e. NN ( y < x -> ps ) -> ph ) )   =>    |- ( x e. NN -> ph )
Theorem	infrenegsupex 10009*	The infimum of a set of reals A is the negative of the supremum of the negatives of its elements. (Contributed by Jim Kingdon, 14-Jan-2022.)
|- ( ph -> E. x e. RR ( A. y e. A -. y < x /\ A. y e. RR ( x < y -> E. z e. A z < y ) ) )   &    |- ( ph -> A C_ RR )   =>    |- ( ph -> inf ( A , RR , < ) = -u sup ( { z e. RR | -u z e. A } , RR , < ) )
Theorem	supinfneg 10010*	If a set of real numbers has a least upper bound, the set of the negation of those numbers has a greatest lower bound. For a theorem which is similar but only for the boundedness part, see ublbneg 10028. (Contributed by Jim Kingdon, 15-Jan-2022.)
|- ( ph -> E. x e. RR ( A. y e. A -. x < y /\ A. y e. RR ( y < x -> E. z e. A y < z ) ) )   &    |- ( ph -> A C_ RR )   =>    |- ( ph -> E. x e. RR ( A. y e. { w e. RR | -u w e. A } -. y < x /\ A. y e. RR ( x < y -> E. z e. { w e. RR | -u w e. A } z < y ) ) )
Theorem	infsupneg 10011*	If a set of real numbers has a greatest lower bound, the set of the negation of those numbers has a least upper bound. To go in the other direction see supinfneg 10010. (Contributed by Jim Kingdon, 15-Jan-2022.)
|- ( ph -> E. x e. RR ( A. y e. A -. y < x /\ A. y e. RR ( x < y -> E. z e. A z < y ) ) )   &    |- ( ph -> A C_ RR )   =>    |- ( ph -> E. x e. RR ( A. y e. { w e. RR | -u w e. A } -. x < y /\ A. y e. RR ( y < x -> E. z e. { w e. RR | -u w e. A } y < z ) ) )
Theorem	supminfex 10012*	A supremum is the negation of the infimum of that set's image under negation. (Contributed by Jim Kingdon, 14-Jan-2022.)
|- ( ph -> E. x e. RR ( A. y e. A -. x < y /\ A. y e. RR ( y < x -> E. z e. A y < z ) ) )   &    |- ( ph -> A C_ RR )   =>    |- ( ph -> sup ( A , RR , < ) = -uinf ( { w e. RR | -u w e. A } , RR , < ) )
Theorem	infregelbex 10013*	Any lower bound of a set of real numbers with an infimum is less than or equal to the infimum. (Contributed by Jim Kingdon, 27-Sep-2024.)
|- ( ph -> E. x e. RR ( A. y e. A -. y < x /\ A. y e. RR ( x < y -> E. z e. A z < y ) ) )   &    |- ( ph -> A C_ RR )   &    |- ( ph -> B e. RR )   =>    |- ( ph -> ( B <_ inf ( A , RR , < ) <-> A. z e. A B <_ z ) )
Theorem	eluznn0 10014	Membership in a nonnegative upper set of integers implies membership in NN0. (Contributed by Paul Chapman, 22-Jun-2011.)
|- ( ( N e. NN0 /\ M e. ( ZZ>= ` N ) ) -> M e. NN0 )
Theorem	eluznn 10015	Membership in a positive upper set of integers implies membership in NN. (Contributed by JJ, 1-Oct-2018.)
|- ( ( N e. NN /\ M e. ( ZZ>= ` N ) ) -> M e. NN )
Theorem	eluz2b1 10016	Two ways to say "an integer greater than or equal to 2". (Contributed by Paul Chapman, 23-Nov-2012.)
|- ( N e. ( ZZ>= ` 2 ) <-> ( N e. ZZ /\ 1 < N ) )
Theorem	eluz2gt1 10017	An integer greater than or equal to 2 is greater than 1. (Contributed by AV, 24-May-2020.)
|- ( N e. ( ZZ>= ` 2 ) -> 1 < N )
Theorem	eluz2b2 10018	Two ways to say "an integer greater than or equal to 2". (Contributed by Paul Chapman, 23-Nov-2012.)
|- ( N e. ( ZZ>= ` 2 ) <-> ( N e. NN /\ 1 < N ) )
Theorem	eluz2b3 10019	Two ways to say "an integer greater than or equal to 2". (Contributed by Paul Chapman, 23-Nov-2012.)
|- ( N e. ( ZZ>= ` 2 ) <-> ( N e. NN /\ N =/= 1 ) )
Theorem	uz2m1nn 10020	One less than an integer greater than or equal to 2 is a positive integer. (Contributed by Paul Chapman, 17-Nov-2012.)
|- ( N e. ( ZZ>= ` 2 ) -> ( N - 1 ) e. NN )
Theorem	1nuz2 10021	1 is not in ( ZZ>= ` 2 ). (Contributed by Paul Chapman, 21-Nov-2012.)
|- -. 1 e. ( ZZ>= ` 2 )
Theorem	elnn1uz2 10022	A positive integer is either 1 or greater than or equal to 2. (Contributed by Paul Chapman, 17-Nov-2012.)
|- ( N e. NN <-> ( N = 1 \/ N e. ( ZZ>= ` 2 ) ) )
Theorem	uz2mulcl 10023	Closure of multiplication of integers greater than or equal to 2. (Contributed by Paul Chapman, 26-Oct-2012.)
|- ( ( M e. ( ZZ>= ` 2 ) /\ N e. ( ZZ>= ` 2 ) ) -> ( M x. N ) e. ( ZZ>= ` 2 ) )
Theorem	indstr2 10024*	Strong Mathematical Induction for positive integers (inference schema). The first two hypotheses give us the substitution instances we need; the last two are the basis and the induction step. (Contributed by Paul Chapman, 21-Nov-2012.)
|- ( x = 1 -> ( ph <-> ch ) )   &    |- ( x = y -> ( ph <-> ps ) )   &    |- ch   &    |- ( x e. ( ZZ>= ` 2 ) -> ( A. y e. NN ( y < x -> ps ) -> ph ) )   =>    |- ( x e. NN -> ph )
Theorem	eluzdc 10025	Membership of an integer in an upper set of integers is decidable. (Contributed by Jim Kingdon, 18-Apr-2020.)
|- ( ( M e. ZZ /\ N e. ZZ ) -> DECID N e. ( ZZ>= ` M ) )
Theorem	elnn0dc 10026	Membership of an integer in NN0 is decidable. (Contributed by Jim Kingdon, 8-Oct-2024.)
|- ( N e. ZZ -> DECID N e. NN0 )
Theorem	elnndc 10027	Membership of an integer in NN is decidable. (Contributed by Jim Kingdon, 17-Oct-2024.)
|- ( N e. ZZ -> DECID N e. NN )
Theorem	ublbneg 10028*	The image under negation of a bounded-above set of reals is bounded below. For a theorem which is similar but also adds that the bounds need to be the tightest possible, see supinfneg 10010. (Contributed by Paul Chapman, 21-Mar-2011.)
|- ( E. x e. RR A. y e. A y <_ x -> E. x e. RR A. y e. { z e. RR | -u z e. A } x <_ y )
Theorem	eqreznegel 10029*	Two ways to express the image under negation of a set of integers. (Contributed by Paul Chapman, 21-Mar-2011.)
|- ( A C_ ZZ -> { z e. RR | -u z e. A } = { z e. ZZ | -u z e. A } )
Theorem	negm 10030*	The image under negation of an inhabited set of reals is inhabited. (Contributed by Jim Kingdon, 10-Apr-2020.)
|- ( ( A C_ RR /\ E. x x e. A ) -> E. y y e. { z e. RR | -u z e. A } )
Theorem	lbzbi 10031*	If a set of reals is bounded below, it is bounded below by an integer. (Contributed by Paul Chapman, 21-Mar-2011.)
|- ( A C_ RR -> ( E. x e. RR A. y e. A x <_ y <-> E. x e. ZZ A. y e. A x <_ y ) )
Theorem	nn01to3 10032	A (nonnegative) integer between 1 and 3 must be 1, 2 or 3. (Contributed by Alexander van der Vekens, 13-Sep-2018.)
|- ( ( N e. NN0 /\ 1 <_ N /\ N <_ 3 ) -> ( N = 1 \/ N = 2 \/ N = 3 ) )
Theorem	nn0ge2m1nnALT 10033	Alternate proof of nn0ge2m1nn 9636: If a nonnegative integer is greater than or equal to two, the integer decreased by 1 is a positive integer. This version is proved using eluz2 9942, a theorem for upper sets of integers, which are defined later than the positive and nonnegative integers. This proof is, however, much shorter than the proof of nn0ge2m1nn 9636. (Contributed by Alexander van der Vekens, 1-Aug-2018.) (New usage is discouraged.) (Proof modification is discouraged.)
|- ( ( N e. NN0 /\ 2 <_ N ) -> ( N - 1 ) e. NN )
4.4.12  Rational numbers (as a subset of complex numbers)
Syntax	cq 10034	Extend class notation to include the class of rationals.
class QQ
Definition	df-q 10035	Define the set of rational numbers. Based on definition of rationals in [Apostol] p. 22. See elq 10037 for the relation "is rational". (Contributed by NM, 8-Jan-2002.)
|- QQ = ( / " ( ZZ X. NN ) )
Theorem	divfnzn 10036	Division restricted to ZZ X. NN is a function. Given excluded middle, it would be easy to prove this for CC X. ( CC \ { 0 } ). The key difference is that an element of NN is apart from zero, whereas being an element of CC \ { 0 } implies being not equal to zero. (Contributed by Jim Kingdon, 19-Mar-2020.)
|- ( / |` ( ZZ X. NN ) ) Fn ( ZZ X. NN )
Theorem	elq 10037*	Membership in the set of rationals. (Contributed by NM, 8-Jan-2002.) (Revised by Mario Carneiro, 28-Jan-2014.)
|- ( A e. QQ <-> E. x e. ZZ E. y e. NN A = ( x / y ) )
Theorem	qmulz 10038*	If A is rational, then some integer multiple of it is an integer. (Contributed by NM, 7-Nov-2008.) (Revised by Mario Carneiro, 22-Jul-2014.)
|- ( A e. QQ -> E. x e. NN ( A x. x ) e. ZZ )
Theorem	znq 10039	The ratio of an integer and a positive integer is a rational number. (Contributed by NM, 12-Jan-2002.)
|- ( ( A e. ZZ /\ B e. NN ) -> ( A / B ) e. QQ )
Theorem	qre 10040	A rational number is a real number. (Contributed by NM, 14-Nov-2002.)
|- ( A e. QQ -> A e. RR )
Theorem	zq 10041	An integer is a rational number. (Contributed by NM, 9-Jan-2002.)
|- ( A e. ZZ -> A e. QQ )
Theorem	zssq 10042	The integers are a subset of the rationals. (Contributed by NM, 9-Jan-2002.)
|- ZZ C_ QQ
Theorem	nn0ssq 10043	The nonnegative integers are a subset of the rationals. (Contributed by NM, 31-Jul-2004.)
|- NN0 C_ QQ
Theorem	nnssq 10044	The positive integers are a subset of the rationals. (Contributed by NM, 31-Jul-2004.)
|- NN C_ QQ
Theorem	qssre 10045	The rationals are a subset of the reals. (Contributed by NM, 9-Jan-2002.)
|- QQ C_ RR
Theorem	qsscn 10046	The rationals are a subset of the complex numbers. (Contributed by NM, 2-Aug-2004.)
|- QQ C_ CC
Theorem	qex 10047	The set of rational numbers exists. (Contributed by NM, 30-Jul-2004.) (Revised by Mario Carneiro, 17-Nov-2014.)
|- QQ e. _V
Theorem	nnq 10048	A positive integer is rational. (Contributed by NM, 17-Nov-2004.)
|- ( A e. NN -> A e. QQ )
Theorem	qcn 10049	A rational number is a complex number. (Contributed by NM, 2-Aug-2004.)
|- ( A e. QQ -> A e. CC )
Theorem	qaddcl 10050	Closure of addition of rationals. (Contributed by NM, 1-Aug-2004.)
|- ( ( A e. QQ /\ B e. QQ ) -> ( A + B ) e. QQ )
Theorem	qnegcl 10051	Closure law for the negative of a rational. (Contributed by NM, 2-Aug-2004.) (Revised by Mario Carneiro, 15-Sep-2014.)
|- ( A e. QQ -> -u A e. QQ )
Theorem	qmulcl 10052	Closure of multiplication of rationals. (Contributed by NM, 1-Aug-2004.)
|- ( ( A e. QQ /\ B e. QQ ) -> ( A x. B ) e. QQ )
Theorem	qsubcl 10053	Closure of subtraction of rationals. (Contributed by NM, 2-Aug-2004.)
|- ( ( A e. QQ /\ B e. QQ ) -> ( A - B ) e. QQ )
Theorem	qapne 10054	Apartness is equivalent to not equal for rationals. (Contributed by Jim Kingdon, 20-Mar-2020.)
|- ( ( A e. QQ /\ B e. QQ ) -> ( A # B <-> A =/= B ) )
Theorem	qltlen 10055	Rational 'Less than' expressed in terms of 'less than or equal to'. Also see ltleap 8968 which is a similar result for real numbers. (Contributed by Jim Kingdon, 11-Oct-2021.)
|- ( ( A e. QQ /\ B e. QQ ) -> ( A < B <-> ( A <_ B /\ B =/= A ) ) )
Theorem	qlttri2 10056	Apartness is equivalent to not equal for rationals. (Contributed by Jim Kingdon, 9-Nov-2021.)
|- ( ( A e. QQ /\ B e. QQ ) -> ( A =/= B <-> ( A < B \/ B < A ) ) )
Theorem	qreccl 10057	Closure of reciprocal of rationals. (Contributed by NM, 3-Aug-2004.)
|- ( ( A e. QQ /\ A =/= 0 ) -> ( 1 / A ) e. QQ )
Theorem	qdivcl 10058	Closure of division of rationals. (Contributed by NM, 3-Aug-2004.)
|- ( ( A e. QQ /\ B e. QQ /\ B =/= 0 ) -> ( A / B ) e. QQ )
Theorem	qrevaddcl 10059	Reverse closure law for addition of rationals. (Contributed by NM, 2-Aug-2004.)
|- ( B e. QQ -> ( ( A e. CC /\ ( A + B ) e. QQ ) <-> A e. QQ ) )
Theorem	nnrecq 10060	The reciprocal of a positive integer is rational. (Contributed by NM, 17-Nov-2004.)
|- ( A e. NN -> ( 1 / A ) e. QQ )
Theorem	irradd 10061	The sum of a real which is not rational and a rational number is not rational. (Contributed by NM, 7-Nov-2008.)
|- ( ( A e. ( RR \ QQ ) /\ B e. QQ ) -> ( A + B ) e. ( RR \ QQ ) )
Theorem	irraddap 10062*	The sum of an irrational number and a rational number is irrational. (Contributed by Jim Kingdon, 20-Aug-2026.)
|- ( ( ( A e. RR /\ A. q e. QQ A # q ) /\ B e. QQ ) -> ( ( A + B ) e. RR /\ A. q e. QQ ( A + B ) # q ) )
Theorem	irrmul 10063	The product of a real which is not rational with a nonzero rational is not rational. Note that by "not rational" we mean the negation of "is rational" (whereas "irrational" is often defined to mean apart from any rational number - given excluded middle these two definitions would be equivalent). For a similar theorem with irrational in place of not rational, see irrmulap 10064. (Contributed by NM, 7-Nov-2008.)
|- ( ( A e. ( RR \ QQ ) /\ B e. QQ /\ B =/= 0 ) -> ( A x. B ) e. ( RR \ QQ ) )
Theorem	irrmulap 10064*	The product of an irrational with a nonzero rational is irrational. By irrational we mean apart from any rational number. For a similar theorem with not rational in place of irrational, see irrmul 10063. (Contributed by Jim Kingdon, 25-Aug-2025.)
|- ( ph -> A e. RR )   &    |- ( ph -> A. q e. QQ A # q )   &    |- ( ph -> B e. QQ )   &    |- ( ph -> B =/= 0 )   &    |- ( ph -> Q e. QQ )   =>    |- ( ph -> ( A x. B ) # Q )
Theorem	elpq 10065*	A positive rational is the quotient of two positive integers. (Contributed by AV, 29-Dec-2022.)
|- ( ( A e. QQ /\ 0 < A ) -> E. x e. NN E. y e. NN A = ( x / y ) )
Theorem	elpqb 10066*	A class is a positive rational iff it is the quotient of two positive integers. (Contributed by AV, 30-Dec-2022.)
|- ( ( A e. QQ /\ 0 < A ) <-> E. x e. NN E. y e. NN A = ( x / y ) )
4.4.13  Complex numbers as pairs of reals
Theorem	cnref1o 10067*	There is a natural one-to-one mapping from ( RR X. RR ) to CC, where we map <. x , y >. to ( x + ( _i x. y ) ). In our construction of the complex numbers, this is in fact our definition of CC (see df-c 8191), but in the axiomatic treatment we can only show that there is the expected mapping between these two sets. (Contributed by Mario Carneiro, 16-Jun-2013.) (Revised by Mario Carneiro, 17-Feb-2014.)
|- F = ( x e. RR , y e. RR |-> ( x + ( _i x. y ) ) )   =>    |- F : ( RR X. RR ) -1-1-onto-> CC
Theorem	addex 10068	The addition operation is a set. (Contributed by NM, 19-Oct-2004.) (Revised by Mario Carneiro, 17-Nov-2014.)
|- + e. _V
Theorem	mulex 10069	The multiplication operation is a set. (Contributed by NM, 19-Oct-2004.) (Revised by Mario Carneiro, 17-Nov-2014.)
|- x. e. _V
4.5  Order sets
4.5.1  Positive reals (as a subset of complex numbers)
Syntax	crp 10070	Extend class notation to include the class of positive reals.
class RR+
Definition	df-rp 10071	Define the set of positive reals. Definition of positive numbers in [Apostol] p. 20. (Contributed by NM, 27-Oct-2007.)
|- RR+ = { x e. RR | 0 < x }
Theorem	elrp 10072	Membership in the set of positive reals. (Contributed by NM, 27-Oct-2007.)
|- ( A e. RR+ <-> ( A e. RR /\ 0 < A ) )
Theorem	elrpii 10073	Membership in the set of positive reals. (Contributed by NM, 23-Feb-2008.)
|- A e. RR   &    |- 0 < A   =>    |- A e. RR+
Theorem	1rp 10074	1 is a positive real. (Contributed by Jeff Hankins, 23-Nov-2008.)
|- 1 e. RR+
Theorem	2rp 10075	2 is a positive real. (Contributed by Mario Carneiro, 28-May-2016.)
|- 2 e. RR+
Theorem	3rp 10076	3 is a positive real. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- 3 e. RR+
Theorem	rpre 10077	A positive real is a real. (Contributed by NM, 27-Oct-2007.)
|- ( A e. RR+ -> A e. RR )
Theorem	rpxr 10078	A positive real is an extended real. (Contributed by Mario Carneiro, 21-Aug-2015.)
|- ( A e. RR+ -> A e. RR* )
Theorem	rpcn 10079	A positive real is a complex number. (Contributed by NM, 11-Nov-2008.)
|- ( A e. RR+ -> A e. CC )
Theorem	nnrp 10080	A positive integer is a positive real. (Contributed by NM, 28-Nov-2008.)
|- ( A e. NN -> A e. RR+ )
Theorem	rpssre 10081	The positive reals are a subset of the reals. (Contributed by NM, 24-Feb-2008.)
|- RR+ C_ RR
Theorem	rpgt0 10082	A positive real is greater than zero. (Contributed by FL, 27-Dec-2007.)
|- ( A e. RR+ -> 0 < A )
Theorem	rpge0 10083	A positive real is greater than or equal to zero. (Contributed by NM, 22-Feb-2008.)
|- ( A e. RR+ -> 0 <_ A )
Theorem	rpregt0 10084	A positive real is a positive real number. (Contributed by NM, 11-Nov-2008.) (Revised by Mario Carneiro, 31-Jan-2014.)
|- ( A e. RR+ -> ( A e. RR /\ 0 < A ) )
Theorem	rprege0 10085	A positive real is a nonnegative real number. (Contributed by Mario Carneiro, 31-Jan-2014.)
|- ( A e. RR+ -> ( A e. RR /\ 0 <_ A ) )
Theorem	rpne0 10086	A positive real is nonzero. (Contributed by NM, 18-Jul-2008.)
|- ( A e. RR+ -> A =/= 0 )
Theorem	rpap0 10087	A positive real is apart from zero. (Contributed by Jim Kingdon, 22-Mar-2020.)
|- ( A e. RR+ -> A # 0 )
Theorem	rprene0 10088	A positive real is a nonzero real number. (Contributed by NM, 11-Nov-2008.)
|- ( A e. RR+ -> ( A e. RR /\ A =/= 0 ) )
Theorem	rpreap0 10089	A positive real is a real number apart from zero. (Contributed by Jim Kingdon, 22-Mar-2020.)
|- ( A e. RR+ -> ( A e. RR /\ A # 0 ) )
Theorem	rpcnne0 10090	A positive real is a nonzero complex number. (Contributed by NM, 11-Nov-2008.)
|- ( A e. RR+ -> ( A e. CC /\ A =/= 0 ) )
Theorem	rpcnap0 10091	A positive real is a complex number apart from zero. (Contributed by Jim Kingdon, 22-Mar-2020.)
|- ( A e. RR+ -> ( A e. CC /\ A # 0 ) )
Theorem	ralrp 10092	Quantification over positive reals. (Contributed by NM, 12-Feb-2008.)
|- ( A. x e. RR+ ph <-> A. x e. RR ( 0 < x -> ph ) )
Theorem	rexrp 10093	Quantification over positive reals. (Contributed by Mario Carneiro, 21-May-2014.)
|- ( E. x e. RR+ ph <-> E. x e. RR ( 0 < x /\ ph ) )
Theorem	rpaddcl 10094	Closure law for addition of positive reals. Part of Axiom 7 of [Apostol] p. 20. (Contributed by NM, 27-Oct-2007.)
|- ( ( A e. RR+ /\ B e. RR+ ) -> ( A + B ) e. RR+ )
Theorem	rpmulcl 10095	Closure law for multiplication of positive reals. Part of Axiom 7 of [Apostol] p. 20. (Contributed by NM, 27-Oct-2007.)
|- ( ( A e. RR+ /\ B e. RR+ ) -> ( A x. B ) e. RR+ )
Theorem	rpdivcl 10096	Closure law for division of positive reals. (Contributed by FL, 27-Dec-2007.)
|- ( ( A e. RR+ /\ B e. RR+ ) -> ( A / B ) e. RR+ )
Theorem	rpreccl 10097	Closure law for reciprocation of positive reals. (Contributed by Jeff Hankins, 23-Nov-2008.)
|- ( A e. RR+ -> ( 1 / A ) e. RR+ )
Theorem	rphalfcl 10098	Closure law for half of a positive real. (Contributed by Mario Carneiro, 31-Jan-2014.)
|- ( A e. RR+ -> ( A / 2 ) e. RR+ )
Theorem	rpgecl 10099	A number greater or equal to a positive real is positive real. (Contributed by Mario Carneiro, 28-May-2016.)
|- ( ( A e. RR+ /\ B e. RR /\ A <_ B ) -> B e. RR+ )
Theorem	rphalflt 10100	Half of a positive real is less than the original number. (Contributed by Mario Carneiro, 21-May-2014.)
|- ( A e. RR+ -> ( A / 2 ) < A )