P. 91 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 9001-9100   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	divfnzn 9001	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 9002*	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 9003*	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 9004	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 9005	A rational number is a real number. (Contributed by NM, 14-Nov-2002.)
|- ( A e. QQ -> A e. RR )
Theorem	zq 9006	An integer is a rational number. (Contributed by NM, 9-Jan-2002.)
|- ( A e. ZZ -> A e. QQ )
Theorem	zssq 9007	The integers are a subset of the rationals. (Contributed by NM, 9-Jan-2002.)
|- ZZ C_ QQ
Theorem	nn0ssq 9008	The nonnegative integers are a subset of the rationals. (Contributed by NM, 31-Jul-2004.)
|- NN0 C_ QQ
Theorem	nnssq 9009	The positive integers are a subset of the rationals. (Contributed by NM, 31-Jul-2004.)
|- NN C_ QQ
Theorem	qssre 9010	The rationals are a subset of the reals. (Contributed by NM, 9-Jan-2002.)
|- QQ C_ RR
Theorem	qsscn 9011	The rationals are a subset of the complex numbers. (Contributed by NM, 2-Aug-2004.)
|- QQ C_ CC
Theorem	qex 9012	The set of rational numbers exists. (Contributed by NM, 30-Jul-2004.) (Revised by Mario Carneiro, 17-Nov-2014.)
|- QQ e. _V
Theorem	nnq 9013	A positive integer is rational. (Contributed by NM, 17-Nov-2004.)
|- ( A e. NN -> A e. QQ )
Theorem	qcn 9014	A rational number is a complex number. (Contributed by NM, 2-Aug-2004.)
|- ( A e. QQ -> A e. CC )
Theorem	qaddcl 9015	Closure of addition of rationals. (Contributed by NM, 1-Aug-2004.)
|- ( ( A e. QQ /\ B e. QQ ) -> ( A + B ) e. QQ )
Theorem	qnegcl 9016	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 9017	Closure of multiplication of rationals. (Contributed by NM, 1-Aug-2004.)
|- ( ( A e. QQ /\ B e. QQ ) -> ( A x. B ) e. QQ )
Theorem	qsubcl 9018	Closure of subtraction of rationals. (Contributed by NM, 2-Aug-2004.)
|- ( ( A e. QQ /\ B e. QQ ) -> ( A - B ) e. QQ )
Theorem	qapne 9019	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 9020	Rational 'Less than' expressed in terms of 'less than or equal to'. Also see ltleap 8007 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 9021	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 9022	Closure of reciprocal of rationals. (Contributed by NM, 3-Aug-2004.)
|- ( ( A e. QQ /\ A =/= 0 ) -> ( 1 / A ) e. QQ )
Theorem	qdivcl 9023	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 9024	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 9025	The reciprocal of a positive integer is rational. (Contributed by NM, 17-Nov-2004.)
|- ( A e. NN -> ( 1 / A ) e. QQ )
Theorem	irradd 9026	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 9027	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). (Contributed by NM, 7-Nov-2008.)
|- ( ( A e. ( RR \ QQ ) /\ B e. QQ /\ B =/= 0 ) -> ( A x. B ) e. ( RR \ QQ ) )
3.4.13  Complex numbers as pairs of reals
Theorem	cnref1o 9028*	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 7259), 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
3.5  Order sets
3.5.1  Positive reals (as a subset of complex numbers)
Syntax	crp 9029	Extend class notation to include the class of positive reals.
class RR+
Definition	df-rp 9030	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 9031	Membership in the set of positive reals. (Contributed by NM, 27-Oct-2007.)
|- ( A e. RR+ <-> ( A e. RR /\ 0 < A ) )
Theorem	elrpii 9032	Membership in the set of positive reals. (Contributed by NM, 23-Feb-2008.)
|- A e. RR   &    |- 0 < A   =>    |- A e. RR+
Theorem	1rp 9033	1 is a positive real. (Contributed by Jeff Hankins, 23-Nov-2008.)
|- 1 e. RR+
Theorem	2rp 9034	2 is a positive real. (Contributed by Mario Carneiro, 28-May-2016.)
|- 2 e. RR+
Theorem	rpre 9035	A positive real is a real. (Contributed by NM, 27-Oct-2007.)
|- ( A e. RR+ -> A e. RR )
Theorem	rpxr 9036	A positive real is an extended real. (Contributed by Mario Carneiro, 21-Aug-2015.)
|- ( A e. RR+ -> A e. RR* )
Theorem	rpcn 9037	A positive real is a complex number. (Contributed by NM, 11-Nov-2008.)
|- ( A e. RR+ -> A e. CC )
Theorem	nnrp 9038	A positive integer is a positive real. (Contributed by NM, 28-Nov-2008.)
|- ( A e. NN -> A e. RR+ )
Theorem	rpssre 9039	The positive reals are a subset of the reals. (Contributed by NM, 24-Feb-2008.)
|- RR+ C_ RR
Theorem	rpgt0 9040	A positive real is greater than zero. (Contributed by FL, 27-Dec-2007.)
|- ( A e. RR+ -> 0 < A )
Theorem	rpge0 9041	A positive real is greater than or equal to zero. (Contributed by NM, 22-Feb-2008.)
|- ( A e. RR+ -> 0 <_ A )
Theorem	rpregt0 9042	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 9043	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 9044	A positive real is nonzero. (Contributed by NM, 18-Jul-2008.)
|- ( A e. RR+ -> A =/= 0 )
Theorem	rpap0 9045	A positive real is apart from zero. (Contributed by Jim Kingdon, 22-Mar-2020.)
|- ( A e. RR+ -> A # 0 )
Theorem	rprene0 9046	A positive real is a nonzero real number. (Contributed by NM, 11-Nov-2008.)
|- ( A e. RR+ -> ( A e. RR /\ A =/= 0 ) )
Theorem	rpreap0 9047	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 9048	A positive real is a nonzero complex number. (Contributed by NM, 11-Nov-2008.)
|- ( A e. RR+ -> ( A e. CC /\ A =/= 0 ) )
Theorem	rpcnap0 9049	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 9050	Quantification over positive reals. (Contributed by NM, 12-Feb-2008.)
|- ( A. x e. RR+ ph <-> A. x e. RR ( 0 < x -> ph ) )
Theorem	rexrp 9051	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 9052	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 9053	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 9054	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 9055	Closure law for reciprocation of positive reals. (Contributed by Jeff Hankins, 23-Nov-2008.)
|- ( A e. RR+ -> ( 1 / A ) e. RR+ )
Theorem	rphalfcl 9056	Closure law for half of a positive real. (Contributed by Mario Carneiro, 31-Jan-2014.)
|- ( A e. RR+ -> ( A / 2 ) e. RR+ )
Theorem	rpgecl 9057	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 9058	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 9059	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 9060	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 9061	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	0nrp 9062	Zero is not a positive real. Axiom 9 of [Apostol] p. 20. (Contributed by NM, 27-Oct-2007.)
|- -. 0 e. RR+
Theorem	ltsubrp 9063	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 9064	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 9065	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 9066	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 9067	A positive integer is a positive real. (Contributed by Mario Carneiro, 28-May-2016.)
|- ( ph -> A e. NN )   =>    |- ( ph -> A e. RR+ )
Theorem	rpred 9068	A positive real is a real. (Contributed by Mario Carneiro, 28-May-2016.)
|- ( ph -> A e. RR+ )   =>    |- ( ph -> A e. RR )
Theorem	rpxrd 9069	A positive real is an extended real. (Contributed by Mario Carneiro, 28-May-2016.)
|- ( ph -> A e. RR+ )   =>    |- ( ph -> A e. RR* )
Theorem	rpcnd 9070	A positive real is a complex number. (Contributed by Mario Carneiro, 28-May-2016.)
|- ( ph -> A e. RR+ )   =>    |- ( ph -> A e. CC )
Theorem	rpgt0d 9071	A positive real is greater than zero. (Contributed by Mario Carneiro, 28-May-2016.)
|- ( ph -> A e. RR+ )   =>    |- ( ph -> 0 < A )
Theorem	rpge0d 9072	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 9073	A positive real is nonzero. (Contributed by Mario Carneiro, 28-May-2016.)
|- ( ph -> A e. RR+ )   =>    |- ( ph -> A =/= 0 )
Theorem	rpap0d 9074	A positive real is apart from zero. (Contributed by Jim Kingdon, 28-Jul-2021.)
|- ( ph -> A e. RR+ )   =>    |- ( ph -> A # 0 )
Theorem	rpregt0d 9075	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 9076	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 9077	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 9078	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 9079	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 9080	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 9081	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 9082	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 9083	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 9084	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 9085	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 9086	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 9087	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 9088	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 ) ) )
Theorem	ltrec1d 9089	Reciprocal swap in a 'less than' relation. (Contributed by Mario Carneiro, 28-May-2016.)
|- ( ph -> A e. RR+ )   &    |- ( ph -> B e. RR+ )   &    |- ( ph -> ( 1 / A ) < B )   =>    |- ( ph -> ( 1 / B ) < A )
Theorem	lerec2d 9090	Reciprocal swap in a 'less than or equal to' relation. (Contributed by Mario Carneiro, 28-May-2016.)
|- ( ph -> A e. RR+ )   &    |- ( ph -> B e. RR+ )   &    |- ( ph -> A <_ ( 1 / B ) )   =>    |- ( ph -> B <_ ( 1 / A ) )
Theorem	lediv2ad 9091	Division of both sides of 'less than or equal to' into 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 / B ) <_ ( C / A ) )
Theorem	ltdiv2d 9092	Division of a positive number by both sides of 'less than'. (Contributed by Mario Carneiro, 28-May-2016.)
|- ( ph -> A e. RR+ )   &    |- ( ph -> B e. RR+ )   &    |- ( ph -> C e. RR+ )   =>    |- ( ph -> ( A < B <-> ( C / B ) < ( C / A ) ) )
Theorem	lediv2d 9093	Division of a positive number by both sides of 'less than or equal to'. (Contributed by Mario Carneiro, 28-May-2016.)
|- ( ph -> A e. RR+ )   &    |- ( ph -> B e. RR+ )   &    |- ( ph -> C e. RR+ )   =>    |- ( ph -> ( A <_ B <-> ( C / B ) <_ ( C / A ) ) )
Theorem	ledivdivd 9094	Invert ratios of positive numbers and swap their ordering. (Contributed by Mario Carneiro, 28-May-2016.)
|- ( ph -> A e. RR+ )   &    |- ( ph -> B e. RR+ )   &    |- ( ph -> C e. RR+ )   &    |- ( ph -> D e. RR+ )   &    |- ( ph -> ( A / B ) <_ ( C / D ) )   =>    |- ( ph -> ( D / C ) <_ ( B / A ) )
Theorem	divge1 9095	The ratio of a number over a smaller positive number is larger than 1. (Contributed by Glauco Siliprandi, 5-Apr-2020.)
|- ( ( A e. RR+ /\ B e. RR /\ A <_ B ) -> 1 <_ ( B / A ) )
Theorem	divlt1lt 9096	A real number divided by a positive real number is less than 1 iff the real number is less than the positive real number. (Contributed by AV, 25-May-2020.)
|- ( ( A e. RR /\ B e. RR+ ) -> ( ( A / B ) < 1 <-> A < B ) )
Theorem	divle1le 9097	A real number divided by a positive real number is less than or equal to 1 iff the real number is less than or equal to the positive real number. (Contributed by AV, 29-Jun-2021.)
|- ( ( A e. RR /\ B e. RR+ ) -> ( ( A / B ) <_ 1 <-> A <_ B ) )
Theorem	ledivge1le 9098	If a number is less than or equal to another number, the number divided by a positive number greater than or equal to one is less than or equal to the other number. (Contributed by AV, 29-Jun-2021.)
|- ( ( A e. RR /\ B e. RR+ /\ ( C e. RR+ /\ 1 <_ C ) ) -> ( A <_ B -> ( A / C ) <_ B ) )
Theorem	ge0p1rpd 9099	A nonnegative number plus one is a positive number. (Contributed by Mario Carneiro, 28-May-2016.)
|- ( ph -> A e. RR )   &    |- ( ph -> 0 <_ A )   =>    |- ( ph -> ( A + 1 ) e. RR+ )
Theorem	rerpdivcld 9100	Closure law for division of a real by a positive real. (Contributed by Mario Carneiro, 28-May-2016.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR+ )   =>    |- ( ph -> ( A / B ) e. RR )