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	nn0ge2m1nnALT 10001	Alternate proof of nn0ge2m1nn 9610: 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 9910, 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 9610. (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 10002	Extend class notation to include the class of rationals.
class QQ
Definition	df-q 10003	Define the set of rational numbers. Based on definition of rationals in [Apostol] p. 22. See elq 10005 for the relation "is rational". (Contributed by NM, 8-Jan-2002.)
|- QQ = ( / " ( ZZ X. NN ) )
Theorem	divfnzn 10004	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 10005*	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 10006*	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 10007	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 10008	A rational number is a real number. (Contributed by NM, 14-Nov-2002.)
|- ( A e. QQ -> A e. RR )
Theorem	zq 10009	An integer is a rational number. (Contributed by NM, 9-Jan-2002.)
|- ( A e. ZZ -> A e. QQ )
Theorem	zssq 10010	The integers are a subset of the rationals. (Contributed by NM, 9-Jan-2002.)
|- ZZ C_ QQ
Theorem	nn0ssq 10011	The nonnegative integers are a subset of the rationals. (Contributed by NM, 31-Jul-2004.)
|- NN0 C_ QQ
Theorem	nnssq 10012	The positive integers are a subset of the rationals. (Contributed by NM, 31-Jul-2004.)
|- NN C_ QQ
Theorem	qssre 10013	The rationals are a subset of the reals. (Contributed by NM, 9-Jan-2002.)
|- QQ C_ RR
Theorem	qsscn 10014	The rationals are a subset of the complex numbers. (Contributed by NM, 2-Aug-2004.)
|- QQ C_ CC
Theorem	qex 10015	The set of rational numbers exists. (Contributed by NM, 30-Jul-2004.) (Revised by Mario Carneiro, 17-Nov-2014.)
|- QQ e. _V
Theorem	nnq 10016	A positive integer is rational. (Contributed by NM, 17-Nov-2004.)
|- ( A e. NN -> A e. QQ )
Theorem	qcn 10017	A rational number is a complex number. (Contributed by NM, 2-Aug-2004.)
|- ( A e. QQ -> A e. CC )
Theorem	qaddcl 10018	Closure of addition of rationals. (Contributed by NM, 1-Aug-2004.)
|- ( ( A e. QQ /\ B e. QQ ) -> ( A + B ) e. QQ )
Theorem	qnegcl 10019	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 10020	Closure of multiplication of rationals. (Contributed by NM, 1-Aug-2004.)
|- ( ( A e. QQ /\ B e. QQ ) -> ( A x. B ) e. QQ )
Theorem	qsubcl 10021	Closure of subtraction of rationals. (Contributed by NM, 2-Aug-2004.)
|- ( ( A e. QQ /\ B e. QQ ) -> ( A - B ) e. QQ )
Theorem	qapne 10022	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 10023	Rational 'Less than' expressed in terms of 'less than or equal to'. Also see ltleap 8954 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 10024	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 10025	Closure of reciprocal of rationals. (Contributed by NM, 3-Aug-2004.)
|- ( ( A e. QQ /\ A =/= 0 ) -> ( 1 / A ) e. QQ )
Theorem	qdivcl 10026	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 10027	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 10028	The reciprocal of a positive integer is rational. (Contributed by NM, 17-Nov-2004.)
|- ( A e. NN -> ( 1 / A ) e. QQ )
Theorem	irradd 10029	The sum of an irrational number and a rational number is irrational. (Contributed by NM, 7-Nov-2008.)
|- ( ( A e. ( RR \ QQ ) /\ B e. QQ ) -> ( A + B ) e. ( RR \ QQ ) )
Theorem	irrmul 10030	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 10031. (Contributed by NM, 7-Nov-2008.)
|- ( ( A e. ( RR \ QQ ) /\ B e. QQ /\ B =/= 0 ) -> ( A x. B ) e. ( RR \ QQ ) )
Theorem	irrmulap 10031*	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 10030. (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 10032*	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 10033*	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 10034*	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 8179), 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 10035	The addition operation is a set. (Contributed by NM, 19-Oct-2004.) (Revised by Mario Carneiro, 17-Nov-2014.)
|- + e. _V
Theorem	mulex 10036	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 10037	Extend class notation to include the class of positive reals.
class RR+
Definition	df-rp 10038	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 10039	Membership in the set of positive reals. (Contributed by NM, 27-Oct-2007.)
|- ( A e. RR+ <-> ( A e. RR /\ 0 < A ) )
Theorem	elrpii 10040	Membership in the set of positive reals. (Contributed by NM, 23-Feb-2008.)
|- A e. RR   &    |- 0 < A   =>    |- A e. RR+
Theorem	1rp 10041	1 is a positive real. (Contributed by Jeff Hankins, 23-Nov-2008.)
|- 1 e. RR+
Theorem	2rp 10042	2 is a positive real. (Contributed by Mario Carneiro, 28-May-2016.)
|- 2 e. RR+
Theorem	3rp 10043	3 is a positive real. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- 3 e. RR+
Theorem	rpre 10044	A positive real is a real. (Contributed by NM, 27-Oct-2007.)
|- ( A e. RR+ -> A e. RR )
Theorem	rpxr 10045	A positive real is an extended real. (Contributed by Mario Carneiro, 21-Aug-2015.)
|- ( A e. RR+ -> A e. RR* )
Theorem	rpcn 10046	A positive real is a complex number. (Contributed by NM, 11-Nov-2008.)
|- ( A e. RR+ -> A e. CC )
Theorem	nnrp 10047	A positive integer is a positive real. (Contributed by NM, 28-Nov-2008.)
|- ( A e. NN -> A e. RR+ )
Theorem	rpssre 10048	The positive reals are a subset of the reals. (Contributed by NM, 24-Feb-2008.)
|- RR+ C_ RR
Theorem	rpgt0 10049	A positive real is greater than zero. (Contributed by FL, 27-Dec-2007.)
|- ( A e. RR+ -> 0 < A )
Theorem	rpge0 10050	A positive real is greater than or equal to zero. (Contributed by NM, 22-Feb-2008.)
|- ( A e. RR+ -> 0 <_ A )
Theorem	rpregt0 10051	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 10052	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 10053	A positive real is nonzero. (Contributed by NM, 18-Jul-2008.)
|- ( A e. RR+ -> A =/= 0 )
Theorem	rpap0 10054	A positive real is apart from zero. (Contributed by Jim Kingdon, 22-Mar-2020.)
|- ( A e. RR+ -> A # 0 )
Theorem	rprene0 10055	A positive real is a nonzero real number. (Contributed by NM, 11-Nov-2008.)
|- ( A e. RR+ -> ( A e. RR /\ A =/= 0 ) )
Theorem	rpreap0 10056	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 10057	A positive real is a nonzero complex number. (Contributed by NM, 11-Nov-2008.)
|- ( A e. RR+ -> ( A e. CC /\ A =/= 0 ) )
Theorem	rpcnap0 10058	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 10059	Quantification over positive reals. (Contributed by NM, 12-Feb-2008.)
|- ( A. x e. RR+ ph <-> A. x e. RR ( 0 < x -> ph ) )
Theorem	rexrp 10060	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 10061	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 10062	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 10063	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 10064	Closure law for reciprocation of positive reals. (Contributed by Jeff Hankins, 23-Nov-2008.)
|- ( A e. RR+ -> ( 1 / A ) e. RR+ )
Theorem	rphalfcl 10065	Closure law for half of a positive real. (Contributed by Mario Carneiro, 31-Jan-2014.)
|- ( A e. RR+ -> ( A / 2 ) e. RR+ )
Theorem	rpgecl 10066	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 10067	Half of a positive real is less than the original number. (Contributed by Mario Carneiro, 21-May-2014.)
|- ( A e. RR+ -> ( A / 2 ) < A )
Theorem	rerpdivcl 10068	Closure law for division of a real by a positive real. (Contributed by NM, 10-Nov-2008.)
|- ( ( A e. RR /\ B e. RR+ ) -> ( A / B ) e. RR )
Theorem	ge0p1rp 10069	A nonnegative number plus one is a positive number. (Contributed by Mario Carneiro, 5-Oct-2015.)
|- ( ( A e. RR /\ 0 <_ A ) -> ( A + 1 ) e. RR+ )
Theorem	rpnegap 10070	Either a real apart from zero or its negation is a positive real, but not both. (Contributed by Jim Kingdon, 23-Mar-2020.)
|- ( ( A e. RR /\ A # 0 ) -> ( A e. RR+ \/_ -u A e. RR+ ) )
Theorem	negelrp 10071	Elementhood of a negation in the positive real numbers. (Contributed by Thierry Arnoux, 19-Sep-2018.)
|- ( A e. RR -> ( -u A e. RR+ <-> A < 0 ) )
Theorem	negelrpd 10072	The negation of a negative number is in the positive real numbers. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
|- ( ph -> A e. RR )   &    |- ( ph -> A < 0 )   =>    |- ( ph -> -u A e. RR+ )
Theorem	0nrp 10073	Zero is not a positive real. Axiom 9 of [Apostol] p. 20. (Contributed by NM, 27-Oct-2007.)
|- -. 0 e. RR+
Theorem	ltsubrp 10074	Subtracting a positive real from another number decreases it. (Contributed by FL, 27-Dec-2007.)
|- ( ( A e. RR /\ B e. RR+ ) -> ( A - B ) < A )
Theorem	ltaddrp 10075	Adding a positive number to another number increases it. (Contributed by FL, 27-Dec-2007.)
|- ( ( A e. RR /\ B e. RR+ ) -> A < ( A + B ) )
Theorem	difrp 10076	Two ways to say one number is less than another. (Contributed by Mario Carneiro, 21-May-2014.)
|- ( ( A e. RR /\ B e. RR ) -> ( A < B <-> ( B - A ) e. RR+ ) )
Theorem	elrpd 10077	Membership in the set of positive reals. (Contributed by Mario Carneiro, 28-May-2016.)
|- ( ph -> A e. RR )   &    |- ( ph -> 0 < A )   =>    |- ( ph -> A e. RR+ )
Theorem	nnrpd 10078	A positive integer is a positive real. (Contributed by Mario Carneiro, 28-May-2016.)
|- ( ph -> A e. NN )   =>    |- ( ph -> A e. RR+ )
Theorem	zgt1rpn0n1 10079	An integer greater than 1 is a positive real number not equal to 0 or 1. Useful for working with integer logarithm bases (which is a common case, e.g., base 2, base 3, or base 10). (Contributed by Thierry Arnoux, 26-Sep-2017.) (Proof shortened by AV, 9-Jul-2022.)
|- ( B e. ( ZZ>= ` 2 ) -> ( B e. RR+ /\ B =/= 0 /\ B =/= 1 ) )
Theorem	rpred 10080	A positive real is a real. (Contributed by Mario Carneiro, 28-May-2016.)
|- ( ph -> A e. RR+ )   =>    |- ( ph -> A e. RR )
Theorem	rpxrd 10081	A positive real is an extended real. (Contributed by Mario Carneiro, 28-May-2016.)
|- ( ph -> A e. RR+ )   =>    |- ( ph -> A e. RR* )
Theorem	rpcnd 10082	A positive real is a complex number. (Contributed by Mario Carneiro, 28-May-2016.)
|- ( ph -> A e. RR+ )   =>    |- ( ph -> A e. CC )
Theorem	rpgt0d 10083	A positive real is greater than zero. (Contributed by Mario Carneiro, 28-May-2016.)
|- ( ph -> A e. RR+ )   =>    |- ( ph -> 0 < A )
Theorem	rpge0d 10084	A positive real is greater than or equal to zero. (Contributed by Mario Carneiro, 28-May-2016.)
|- ( ph -> A e. RR+ )   =>    |- ( ph -> 0 <_ A )
Theorem	rpne0d 10085	A positive real is nonzero. (Contributed by Mario Carneiro, 28-May-2016.)
|- ( ph -> A e. RR+ )   =>    |- ( ph -> A =/= 0 )
Theorem	rpap0d 10086	A positive real is apart from zero. (Contributed by Jim Kingdon, 28-Jul-2021.)
|- ( ph -> A e. RR+ )   =>    |- ( ph -> A # 0 )
Theorem	rpregt0d 10087	A positive real is real and greater than zero. (Contributed by Mario Carneiro, 28-May-2016.)
|- ( ph -> A e. RR+ )   =>    |- ( ph -> ( A e. RR /\ 0 < A ) )
Theorem	rprege0d 10088	A positive real is real and greater or equal to zero. (Contributed by Mario Carneiro, 28-May-2016.)
|- ( ph -> A e. RR+ )   =>    |- ( ph -> ( A e. RR /\ 0 <_ A ) )
Theorem	rprene0d 10089	A positive real is a nonzero real number. (Contributed by Mario Carneiro, 28-May-2016.)
|- ( ph -> A e. RR+ )   =>    |- ( ph -> ( A e. RR /\ A =/= 0 ) )
Theorem	rpcnne0d 10090	A positive real is a nonzero complex number. (Contributed by Mario Carneiro, 28-May-2016.)
|- ( ph -> A e. RR+ )   =>    |- ( ph -> ( A e. CC /\ A =/= 0 ) )
Theorem	rpreccld 10091	Closure law for reciprocation of positive reals. (Contributed by Mario Carneiro, 28-May-2016.)
|- ( ph -> A e. RR+ )   =>    |- ( ph -> ( 1 / A ) e. RR+ )
Theorem	rprecred 10092	Closure law for reciprocation of positive reals. (Contributed by Mario Carneiro, 28-May-2016.)
|- ( ph -> A e. RR+ )   =>    |- ( ph -> ( 1 / A ) e. RR )
Theorem	rphalfcld 10093	Closure law for half of a positive real. (Contributed by Mario Carneiro, 28-May-2016.)
|- ( ph -> A e. RR+ )   =>    |- ( ph -> ( A / 2 ) e. RR+ )
Theorem	reclt1d 10094	The reciprocal of a positive number less than 1 is greater than 1. (Contributed by Mario Carneiro, 28-May-2016.)
|- ( ph -> A e. RR+ )   =>    |- ( ph -> ( A < 1 <-> 1 < ( 1 / A ) ) )
Theorem	recgt1d 10095	The reciprocal of a positive number greater than 1 is less than 1. (Contributed by Mario Carneiro, 28-May-2016.)
|- ( ph -> A e. RR+ )   =>    |- ( ph -> ( 1 < A <-> ( 1 / A ) < 1 ) )
Theorem	rpaddcld 10096	Closure law for addition of positive reals. Part of Axiom 7 of [Apostol] p. 20. (Contributed by Mario Carneiro, 28-May-2016.)
|- ( ph -> A e. RR+ )   &    |- ( ph -> B e. RR+ )   =>    |- ( ph -> ( A + B ) e. RR+ )
Theorem	rpmulcld 10097	Closure law for multiplication of positive reals. Part of Axiom 7 of [Apostol] p. 20. (Contributed by Mario Carneiro, 28-May-2016.)
|- ( ph -> A e. RR+ )   &    |- ( ph -> B e. RR+ )   =>    |- ( ph -> ( A x. B ) e. RR+ )
Theorem	rpdivcld 10098	Closure law for division of positive reals. (Contributed by Mario Carneiro, 28-May-2016.)
|- ( ph -> A e. RR+ )   &    |- ( ph -> B e. RR+ )   =>    |- ( ph -> ( A / B ) e. RR+ )
Theorem	ltrecd 10099	The reciprocal of both sides of 'less than'. (Contributed by Mario Carneiro, 28-May-2016.)
|- ( ph -> A e. RR+ )   &    |- ( ph -> B e. RR+ )   =>    |- ( ph -> ( A < B <-> ( 1 / B ) < ( 1 / A ) ) )
Theorem	lerecd 10100	The reciprocal of both sides of 'less than or equal to'. (Contributed by Mario Carneiro, 28-May-2016.)
|- ( ph -> A e. RR+ )   &    |- ( ph -> B e. RR+ )   =>    |- ( ph -> ( A <_ B <-> ( 1 / B ) <_ ( 1 / A ) ) )