P. 96 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 9501-9600   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	infsupneg 9501*	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 9500. (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 9502*	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	eluznn0 9503	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 9504	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 9505	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 9506	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 9507	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 9508	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 9509	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 9510	1 is not in ( ZZ>= ` 2 ). (Contributed by Paul Chapman, 21-Nov-2012.)
|- -. 1 e. ( ZZ>= ` 2 )
Theorem	elnn1uz2 9511	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 9512	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 9513*	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 9514	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	ublbneg 9515*	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 9500. (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 9516*	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 9517*	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 9518*	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 9519	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 9520	Alternate proof of nn0ge2m1nn 9144: 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 9439, 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 9144. (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 9521	Extend class notation to include the class of rationals.
class QQ
Definition	df-q 9522	Define the set of rational numbers. Based on definition of rationals in [Apostol] p. 22. See elq 9524 for the relation "is rational." (Contributed by NM, 8-Jan-2002.)
|- QQ = ( / " ( ZZ X. NN ) )
Theorem	divfnzn 9523	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 9524*	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 9525*	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 9526	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 9527	A rational number is a real number. (Contributed by NM, 14-Nov-2002.)
|- ( A e. QQ -> A e. RR )
Theorem	zq 9528	An integer is a rational number. (Contributed by NM, 9-Jan-2002.)
|- ( A e. ZZ -> A e. QQ )
Theorem	zssq 9529	The integers are a subset of the rationals. (Contributed by NM, 9-Jan-2002.)
|- ZZ C_ QQ
Theorem	nn0ssq 9530	The nonnegative integers are a subset of the rationals. (Contributed by NM, 31-Jul-2004.)
|- NN0 C_ QQ
Theorem	nnssq 9531	The positive integers are a subset of the rationals. (Contributed by NM, 31-Jul-2004.)
|- NN C_ QQ
Theorem	qssre 9532	The rationals are a subset of the reals. (Contributed by NM, 9-Jan-2002.)
|- QQ C_ RR
Theorem	qsscn 9533	The rationals are a subset of the complex numbers. (Contributed by NM, 2-Aug-2004.)
|- QQ C_ CC
Theorem	qex 9534	The set of rational numbers exists. (Contributed by NM, 30-Jul-2004.) (Revised by Mario Carneiro, 17-Nov-2014.)
|- QQ e. _V
Theorem	nnq 9535	A positive integer is rational. (Contributed by NM, 17-Nov-2004.)
|- ( A e. NN -> A e. QQ )
Theorem	qcn 9536	A rational number is a complex number. (Contributed by NM, 2-Aug-2004.)
|- ( A e. QQ -> A e. CC )
Theorem	qaddcl 9537	Closure of addition of rationals. (Contributed by NM, 1-Aug-2004.)
|- ( ( A e. QQ /\ B e. QQ ) -> ( A + B ) e. QQ )
Theorem	qnegcl 9538	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 9539	Closure of multiplication of rationals. (Contributed by NM, 1-Aug-2004.)
|- ( ( A e. QQ /\ B e. QQ ) -> ( A x. B ) e. QQ )
Theorem	qsubcl 9540	Closure of subtraction of rationals. (Contributed by NM, 2-Aug-2004.)
|- ( ( A e. QQ /\ B e. QQ ) -> ( A - B ) e. QQ )
Theorem	qapne 9541	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 9542	Rational 'Less than' expressed in terms of 'less than or equal to'. Also see ltleap 8501 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 9543	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 9544	Closure of reciprocal of rationals. (Contributed by NM, 3-Aug-2004.)
|- ( ( A e. QQ /\ A =/= 0 ) -> ( 1 / A ) e. QQ )
Theorem	qdivcl 9545	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 9546	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 9547	The reciprocal of a positive integer is rational. (Contributed by NM, 17-Nov-2004.)
|- ( A e. NN -> ( 1 / A ) e. QQ )
Theorem	irradd 9548	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 9549	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 ) )
Theorem	elpq 9550*	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 9551*	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 9552*	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 7732), 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
4.5  Order sets
4.5.1  Positive reals (as a subset of complex numbers)
Syntax	crp 9553	Extend class notation to include the class of positive reals.
class RR+
Definition	df-rp 9554	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 9555	Membership in the set of positive reals. (Contributed by NM, 27-Oct-2007.)
|- ( A e. RR+ <-> ( A e. RR /\ 0 < A ) )
Theorem	elrpii 9556	Membership in the set of positive reals. (Contributed by NM, 23-Feb-2008.)
|- A e. RR   &    |- 0 < A   =>    |- A e. RR+
Theorem	1rp 9557	1 is a positive real. (Contributed by Jeff Hankins, 23-Nov-2008.)
|- 1 e. RR+
Theorem	2rp 9558	2 is a positive real. (Contributed by Mario Carneiro, 28-May-2016.)
|- 2 e. RR+
Theorem	3rp 9559	3 is a positive real. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- 3 e. RR+
Theorem	rpre 9560	A positive real is a real. (Contributed by NM, 27-Oct-2007.)
|- ( A e. RR+ -> A e. RR )
Theorem	rpxr 9561	A positive real is an extended real. (Contributed by Mario Carneiro, 21-Aug-2015.)
|- ( A e. RR+ -> A e. RR* )
Theorem	rpcn 9562	A positive real is a complex number. (Contributed by NM, 11-Nov-2008.)
|- ( A e. RR+ -> A e. CC )
Theorem	nnrp 9563	A positive integer is a positive real. (Contributed by NM, 28-Nov-2008.)
|- ( A e. NN -> A e. RR+ )
Theorem	rpssre 9564	The positive reals are a subset of the reals. (Contributed by NM, 24-Feb-2008.)
|- RR+ C_ RR
Theorem	rpgt0 9565	A positive real is greater than zero. (Contributed by FL, 27-Dec-2007.)
|- ( A e. RR+ -> 0 < A )
Theorem	rpge0 9566	A positive real is greater than or equal to zero. (Contributed by NM, 22-Feb-2008.)
|- ( A e. RR+ -> 0 <_ A )
Theorem	rpregt0 9567	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 9568	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 9569	A positive real is nonzero. (Contributed by NM, 18-Jul-2008.)
|- ( A e. RR+ -> A =/= 0 )
Theorem	rpap0 9570	A positive real is apart from zero. (Contributed by Jim Kingdon, 22-Mar-2020.)
|- ( A e. RR+ -> A # 0 )
Theorem	rprene0 9571	A positive real is a nonzero real number. (Contributed by NM, 11-Nov-2008.)
|- ( A e. RR+ -> ( A e. RR /\ A =/= 0 ) )
Theorem	rpreap0 9572	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 9573	A positive real is a nonzero complex number. (Contributed by NM, 11-Nov-2008.)
|- ( A e. RR+ -> ( A e. CC /\ A =/= 0 ) )
Theorem	rpcnap0 9574	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 9575	Quantification over positive reals. (Contributed by NM, 12-Feb-2008.)
|- ( A. x e. RR+ ph <-> A. x e. RR ( 0 < x -> ph ) )
Theorem	rexrp 9576	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 9577	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 9578	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 9579	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 9580	Closure law for reciprocation of positive reals. (Contributed by Jeff Hankins, 23-Nov-2008.)
|- ( A e. RR+ -> ( 1 / A ) e. RR+ )
Theorem	rphalfcl 9581	Closure law for half of a positive real. (Contributed by Mario Carneiro, 31-Jan-2014.)
|- ( A e. RR+ -> ( A / 2 ) e. RR+ )
Theorem	rpgecl 9582	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 9583	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 9584	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 9585	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 9586	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 9587	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 9588	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 9589	Zero is not a positive real. Axiom 9 of [Apostol] p. 20. (Contributed by NM, 27-Oct-2007.)
|- -. 0 e. RR+
Theorem	ltsubrp 9590	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 9591	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 9592	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 9593	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 9594	A positive integer is a positive real. (Contributed by Mario Carneiro, 28-May-2016.)
|- ( ph -> A e. NN )   =>    |- ( ph -> A e. RR+ )
Theorem	zgt1rpn0n1 9595	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 9596	A positive real is a real. (Contributed by Mario Carneiro, 28-May-2016.)
|- ( ph -> A e. RR+ )   =>    |- ( ph -> A e. RR )
Theorem	rpxrd 9597	A positive real is an extended real. (Contributed by Mario Carneiro, 28-May-2016.)
|- ( ph -> A e. RR+ )   =>    |- ( ph -> A e. RR* )
Theorem	rpcnd 9598	A positive real is a complex number. (Contributed by Mario Carneiro, 28-May-2016.)
|- ( ph -> A e. RR+ )   =>    |- ( ph -> A e. CC )
Theorem	rpgt0d 9599	A positive real is greater than zero. (Contributed by Mario Carneiro, 28-May-2016.)
|- ( ph -> A e. RR+ )   =>    |- ( ph -> 0 < A )
Theorem	rpge0d 9600	A positive real is greater than or equal to zero. (Contributed by Mario Carneiro, 28-May-2016.)
|- ( ph -> A e. RR+ )   =>    |- ( ph -> 0 <_ A )