P. 90 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 8901-9000   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	lemuldiv2 8901	'Less than or equal' relationship between division and multiplication. (Contributed by NM, 10-Mar-2006.)
|- ( ( A e. RR /\ B e. RR /\ ( C e. RR /\ 0 < C ) ) -> ( ( C x. A ) <_ B <-> A <_ ( B / C ) ) )
Theorem	ltrec 8902	The reciprocal of both sides of 'less than'. (Contributed by NM, 26-Sep-1999.) (Revised by Mario Carneiro, 27-May-2016.)
|- ( ( ( A e. RR /\ 0 < A ) /\ ( B e. RR /\ 0 < B ) ) -> ( A < B <-> ( 1 / B ) < ( 1 / A ) ) )
Theorem	lerec 8903	The reciprocal of both sides of 'less than or equal to'. (Contributed by NM, 3-Oct-1999.) (Proof shortened by Mario Carneiro, 27-May-2016.)
|- ( ( ( A e. RR /\ 0 < A ) /\ ( B e. RR /\ 0 < B ) ) -> ( A <_ B <-> ( 1 / B ) <_ ( 1 / A ) ) )
Theorem	lt2msq1 8904	Lemma for lt2msq 8905. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ( ( A e. RR /\ 0 <_ A ) /\ B e. RR /\ A < B ) -> ( A x. A ) < ( B x. B ) )
Theorem	lt2msq 8905	Two nonnegative numbers compare the same as their squares. (Contributed by Roy F. Longton, 8-Aug-2005.) (Revised by Mario Carneiro, 27-May-2016.)
|- ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 <_ B ) ) -> ( A < B <-> ( A x. A ) < ( B x. B ) ) )
Theorem	ltdiv2 8906	Division of a positive number by both sides of 'less than'. (Contributed by NM, 27-Apr-2005.)
|- ( ( ( A e. RR /\ 0 < A ) /\ ( B e. RR /\ 0 < B ) /\ ( C e. RR /\ 0 < C ) ) -> ( A < B <-> ( C / B ) < ( C / A ) ) )
Theorem	ltrec1 8907	Reciprocal swap in a 'less than' relation. (Contributed by NM, 24-Feb-2005.)
|- ( ( ( A e. RR /\ 0 < A ) /\ ( B e. RR /\ 0 < B ) ) -> ( ( 1 / A ) < B <-> ( 1 / B ) < A ) )
Theorem	lerec2 8908	Reciprocal swap in a 'less than or equal to' relation. (Contributed by NM, 24-Feb-2005.)
|- ( ( ( A e. RR /\ 0 < A ) /\ ( B e. RR /\ 0 < B ) ) -> ( A <_ ( 1 / B ) <-> B <_ ( 1 / A ) ) )
Theorem	ledivdiv 8909	Invert ratios of positive numbers and swap their ordering. (Contributed by NM, 9-Jan-2006.)
|- ( ( ( ( A e. RR /\ 0 < A ) /\ ( B e. RR /\ 0 < B ) ) /\ ( ( C e. RR /\ 0 < C ) /\ ( D e. RR /\ 0 < D ) ) ) -> ( ( A / B ) <_ ( C / D ) <-> ( D / C ) <_ ( B / A ) ) )
Theorem	lediv2 8910	Division of a positive number by both sides of 'less than or equal to'. (Contributed by NM, 10-Jan-2006.)
|- ( ( ( A e. RR /\ 0 < A ) /\ ( B e. RR /\ 0 < B ) /\ ( C e. RR /\ 0 < C ) ) -> ( A <_ B <-> ( C / B ) <_ ( C / A ) ) )
Theorem	ltdiv23 8911	Swap denominator with other side of 'less than'. (Contributed by NM, 3-Oct-1999.)
|- ( ( A e. RR /\ ( B e. RR /\ 0 < B ) /\ ( C e. RR /\ 0 < C ) ) -> ( ( A / B ) < C <-> ( A / C ) < B ) )
Theorem	lediv23 8912	Swap denominator with other side of 'less than or equal to'. (Contributed by NM, 30-May-2005.)
|- ( ( A e. RR /\ ( B e. RR /\ 0 < B ) /\ ( C e. RR /\ 0 < C ) ) -> ( ( A / B ) <_ C <-> ( A / C ) <_ B ) )
Theorem	lediv12a 8913	Comparison of ratio of two nonnegative numbers. (Contributed by NM, 31-Dec-2005.)
|- ( ( ( ( A e. RR /\ B e. RR ) /\ ( 0 <_ A /\ A <_ B ) ) /\ ( ( C e. RR /\ D e. RR ) /\ ( 0 < C /\ C <_ D ) ) ) -> ( A / D ) <_ ( B / C ) )
Theorem	lediv2a 8914	Division of both sides of 'less than or equal to' into a nonnegative number. (Contributed by Paul Chapman, 7-Sep-2007.)
|- ( ( ( ( A e. RR /\ 0 < A ) /\ ( B e. RR /\ 0 < B ) /\ ( C e. RR /\ 0 <_ C ) ) /\ A <_ B ) -> ( C / B ) <_ ( C / A ) )
Theorem	reclt1 8915	The reciprocal of a positive number less than 1 is greater than 1. (Contributed by NM, 23-Feb-2005.)
|- ( ( A e. RR /\ 0 < A ) -> ( A < 1 <-> 1 < ( 1 / A ) ) )
Theorem	recgt1 8916	The reciprocal of a positive number greater than 1 is less than 1. (Contributed by NM, 28-Dec-2005.)
|- ( ( A e. RR /\ 0 < A ) -> ( 1 < A <-> ( 1 / A ) < 1 ) )
Theorem	recgt1i 8917	The reciprocal of a number greater than 1 is positive and less than 1. (Contributed by NM, 23-Feb-2005.)
|- ( ( A e. RR /\ 1 < A ) -> ( 0 < ( 1 / A ) /\ ( 1 / A ) < 1 ) )
Theorem	recp1lt1 8918	Construct a number less than 1 from any nonnegative number. (Contributed by NM, 30-Dec-2005.)
|- ( ( A e. RR /\ 0 <_ A ) -> ( A / ( 1 + A ) ) < 1 )
Theorem	recreclt 8919	Given a positive number A, construct a new positive number less than both A and 1. (Contributed by NM, 28-Dec-2005.)
|- ( ( A e. RR /\ 0 < A ) -> ( ( 1 / ( 1 + ( 1 / A ) ) ) < 1 /\ ( 1 / ( 1 + ( 1 / A ) ) ) < A ) )
Theorem	le2msq 8920	The square function on nonnegative reals is monotonic. (Contributed by NM, 3-Aug-1999.) (Proof shortened by Mario Carneiro, 27-May-2016.)
|- ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 <_ B ) ) -> ( A <_ B <-> ( A x. A ) <_ ( B x. B ) ) )
Theorem	msq11 8921	The square of a nonnegative number is a one-to-one function. (Contributed by NM, 29-Jul-1999.) (Revised by Mario Carneiro, 27-May-2016.)
|- ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 <_ B ) ) -> ( ( A x. A ) = ( B x. B ) <-> A = B ) )
Theorem	ledivp1 8922	Less-than-or-equal-to and division relation. (Lemma for computing upper bounds of products. The "+ 1" prevents division by zero.) (Contributed by NM, 28-Sep-2005.)
|- ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 <_ B ) ) -> ( ( A / ( B + 1 ) ) x. B ) <_ A )
Theorem	squeeze0 8923*	If a nonnegative number is less than any positive number, it is zero. (Contributed by NM, 11-Feb-2006.)
|- ( ( A e. RR /\ 0 <_ A /\ A. x e. RR ( 0 < x -> A < x ) ) -> A = 0 )
Theorem	ltp1i 8924	A number is less than itself plus 1. (Contributed by NM, 20-Aug-2001.)
|- A e. RR   =>    |- A < ( A + 1 )
Theorem	recgt0i 8925	The reciprocal of a positive number is positive. Exercise 4 of [Apostol] p. 21. (Contributed by NM, 15-May-1999.)
|- A e. RR   =>    |- ( 0 < A -> 0 < ( 1 / A ) )
Theorem	recgt0ii 8926	The reciprocal of a positive number is positive. Exercise 4 of [Apostol] p. 21. (Contributed by NM, 15-May-1999.)
|- A e. RR   &    |- 0 < A   =>    |- 0 < ( 1 / A )
Theorem	prodgt0i 8927	Infer that a multiplicand is positive from a nonnegative multiplier and positive product. (Contributed by NM, 15-May-1999.)
|- A e. RR   &    |- B e. RR   =>    |- ( ( 0 <_ A /\ 0 < ( A x. B ) ) -> 0 < B )
Theorem	prodge0i 8928	Infer that a multiplicand is nonnegative from a positive multiplier and nonnegative product. (Contributed by NM, 2-Jul-2005.)
|- A e. RR   &    |- B e. RR   =>    |- ( ( 0 < A /\ 0 <_ ( A x. B ) ) -> 0 <_ B )
Theorem	divgt0i 8929	The ratio of two positive numbers is positive. (Contributed by NM, 16-May-1999.)
|- A e. RR   &    |- B e. RR   =>    |- ( ( 0 < A /\ 0 < B ) -> 0 < ( A / B ) )
Theorem	divge0i 8930	The ratio of nonnegative and positive numbers is nonnegative. (Contributed by NM, 12-Aug-1999.)
|- A e. RR   &    |- B e. RR   =>    |- ( ( 0 <_ A /\ 0 < B ) -> 0 <_ ( A / B ) )
Theorem	ltreci 8931	The reciprocal of both sides of 'less than'. (Contributed by NM, 15-Sep-1999.)
|- A e. RR   &    |- B e. RR   =>    |- ( ( 0 < A /\ 0 < B ) -> ( A < B <-> ( 1 / B ) < ( 1 / A ) ) )
Theorem	lereci 8932	The reciprocal of both sides of 'less than or equal to'. (Contributed by NM, 16-Sep-1999.)
|- A e. RR   &    |- B e. RR   =>    |- ( ( 0 < A /\ 0 < B ) -> ( A <_ B <-> ( 1 / B ) <_ ( 1 / A ) ) )
Theorem	lt2msqi 8933	The square function on nonnegative reals is strictly monotonic. (Contributed by NM, 3-Aug-1999.)
|- A e. RR   &    |- B e. RR   =>    |- ( ( 0 <_ A /\ 0 <_ B ) -> ( A < B <-> ( A x. A ) < ( B x. B ) ) )
Theorem	le2msqi 8934	The square function on nonnegative reals is monotonic. (Contributed by NM, 2-Aug-1999.)
|- A e. RR   &    |- B e. RR   =>    |- ( ( 0 <_ A /\ 0 <_ B ) -> ( A <_ B <-> ( A x. A ) <_ ( B x. B ) ) )
Theorem	msq11i 8935	The square of a nonnegative number is a one-to-one function. (Contributed by NM, 29-Jul-1999.)
|- A e. RR   &    |- B e. RR   =>    |- ( ( 0 <_ A /\ 0 <_ B ) -> ( ( A x. A ) = ( B x. B ) <-> A = B ) )
Theorem	divgt0i2i 8936	The ratio of two positive numbers is positive. (Contributed by NM, 16-May-1999.)
|- A e. RR   &    |- B e. RR   &    |- 0 < B   =>    |- ( 0 < A -> 0 < ( A / B ) )
Theorem	ltrecii 8937	The reciprocal of both sides of 'less than'. (Contributed by NM, 15-Sep-1999.)
|- A e. RR   &    |- B e. RR   &    |- 0 < A   &    |- 0 < B   =>    |- ( A < B <-> ( 1 / B ) < ( 1 / A ) )
Theorem	divgt0ii 8938	The ratio of two positive numbers is positive. (Contributed by NM, 18-May-1999.)
|- A e. RR   &    |- B e. RR   &    |- 0 < A   &    |- 0 < B   =>    |- 0 < ( A / B )
Theorem	ltmul1i 8939	Multiplication of both sides of 'less than' by a positive number. Theorem I.19 of [Apostol] p. 20. (Contributed by NM, 16-May-1999.)
|- A e. RR   &    |- B e. RR   &    |- C e. RR   =>    |- ( 0 < C -> ( A < B <-> ( A x. C ) < ( B x. C ) ) )
Theorem	ltdiv1i 8940	Division of both sides of 'less than' by a positive number. (Contributed by NM, 16-May-1999.)
|- A e. RR   &    |- B e. RR   &    |- C e. RR   =>    |- ( 0 < C -> ( A < B <-> ( A / C ) < ( B / C ) ) )
Theorem	ltmuldivi 8941	'Less than' relationship between division and multiplication. (Contributed by NM, 12-Oct-1999.)
|- A e. RR   &    |- B e. RR   &    |- C e. RR   =>    |- ( 0 < C -> ( ( A x. C ) < B <-> A < ( B / C ) ) )
Theorem	ltmul2i 8942	Multiplication of both sides of 'less than' by a positive number. Theorem I.19 of [Apostol] p. 20. (Contributed by NM, 16-May-1999.)
|- A e. RR   &    |- B e. RR   &    |- C e. RR   =>    |- ( 0 < C -> ( A < B <-> ( C x. A ) < ( C x. B ) ) )
Theorem	lemul1i 8943	Multiplication of both sides of 'less than or equal to' by a positive number. (Contributed by NM, 2-Aug-1999.)
|- A e. RR   &    |- B e. RR   &    |- C e. RR   =>    |- ( 0 < C -> ( A <_ B <-> ( A x. C ) <_ ( B x. C ) ) )
Theorem	lemul2i 8944	Multiplication of both sides of 'less than or equal to' by a positive number. (Contributed by NM, 1-Aug-1999.)
|- A e. RR   &    |- B e. RR   &    |- C e. RR   =>    |- ( 0 < C -> ( A <_ B <-> ( C x. A ) <_ ( C x. B ) ) )
Theorem	ltdiv23i 8945	Swap denominator with other side of 'less than'. (Contributed by NM, 26-Sep-1999.)
|- A e. RR   &    |- B e. RR   &    |- C e. RR   =>    |- ( ( 0 < B /\ 0 < C ) -> ( ( A / B ) < C <-> ( A / C ) < B ) )
Theorem	ltdiv23ii 8946	Swap denominator with other side of 'less than'. (Contributed by NM, 26-Sep-1999.)
|- A e. RR   &    |- B e. RR   &    |- C e. RR   &    |- 0 < B   &    |- 0 < C   =>    |- ( ( A / B ) < C <-> ( A / C ) < B )
Theorem	ltmul1ii 8947	Multiplication of both sides of 'less than' by a positive number. Theorem I.19 of [Apostol] p. 20. (Contributed by NM, 16-May-1999.) (Proof shortened by Paul Chapman, 25-Jan-2008.)
|- A e. RR   &    |- B e. RR   &    |- C e. RR   &    |- 0 < C   =>    |- ( A < B <-> ( A x. C ) < ( B x. C ) )
Theorem	ltdiv1ii 8948	Division of both sides of 'less than' by a positive number. (Contributed by NM, 16-May-1999.)
|- A e. RR   &    |- B e. RR   &    |- C e. RR   &    |- 0 < C   =>    |- ( A < B <-> ( A / C ) < ( B / C ) )
Theorem	ltp1d 8949	A number is less than itself plus 1. (Contributed by Mario Carneiro, 28-May-2016.)
|- ( ph -> A e. RR )   =>    |- ( ph -> A < ( A + 1 ) )
Theorem	lep1d 8950	A number is less than or equal to itself plus 1. (Contributed by Mario Carneiro, 28-May-2016.)
|- ( ph -> A e. RR )   =>    |- ( ph -> A <_ ( A + 1 ) )
Theorem	ltm1d 8951	A number minus 1 is less than itself. (Contributed by Mario Carneiro, 28-May-2016.)
|- ( ph -> A e. RR )   =>    |- ( ph -> ( A - 1 ) < A )
Theorem	lem1d 8952	A number minus 1 is less than or equal to itself. (Contributed by Mario Carneiro, 28-May-2016.)
|- ( ph -> A e. RR )   =>    |- ( ph -> ( A - 1 ) <_ A )
Theorem	recgt0d 8953	The reciprocal of a positive number is positive. Exercise 4 of [Apostol] p. 21. (Contributed by Mario Carneiro, 28-May-2016.)
|- ( ph -> A e. RR )   &    |- ( ph -> 0 < A )   =>    |- ( ph -> 0 < ( 1 / A ) )
Theorem	divgt0d 8954	The ratio of two positive numbers is positive. (Contributed by Mario Carneiro, 28-May-2016.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> 0 < A )   &    |- ( ph -> 0 < B )   =>    |- ( ph -> 0 < ( A / B ) )
Theorem	mulgt1d 8955	The product of two numbers greater than 1 is greater than 1. (Contributed by Mario Carneiro, 28-May-2016.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> 1 < A )   &    |- ( ph -> 1 < B )   =>    |- ( ph -> 1 < ( A x. B ) )
Theorem	lemulge11d 8956	Multiplication by a number greater than or equal to 1. (Contributed by Mario Carneiro, 28-May-2016.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> 0 <_ A )   &    |- ( ph -> 1 <_ B )   =>    |- ( ph -> A <_ ( A x. B ) )
Theorem	lemulge12d 8957	Multiplication by a number greater than or equal to 1. (Contributed by Mario Carneiro, 28-May-2016.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> 0 <_ A )   &    |- ( ph -> 1 <_ B )   =>    |- ( ph -> A <_ ( B x. A ) )
Theorem	lemul1ad 8958	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 8959	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 8960	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 8961	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 8962	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 ) )
Theorem	mulle0r 8963	Multiplying a nonnegative number by a nonpositive number yields a nonpositive number. (Contributed by Jim Kingdon, 28-Oct-2021.)
|- ( ( ( A e. RR /\ B e. RR ) /\ ( A <_ 0 /\ 0 <_ B ) ) -> ( A x. B ) <_ 0 )
4.3.10  Suprema
Theorem	lbreu 8964*	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 8965*	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 8966*	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	lbinf 8967*	If a set of reals contains a lower bound, the lower bound is its infimum. (Contributed by NM, 9-Oct-2005.) (Revised by AV, 4-Sep-2020.)
|- ( ( S C_ RR /\ E. x e. S A. y e. S x <_ y ) -> inf ( S , RR , < ) = ( iota_ x e. S A. y e. S x <_ y ) )
Theorem	lbinfcl 8968*	If a set of reals contains a lower bound, it contains its infimum. (Contributed by NM, 11-Oct-2005.) (Revised by AV, 4-Sep-2020.)
|- ( ( S C_ RR /\ E. x e. S A. y e. S x <_ y ) -> inf ( S , RR , < ) e. S )
Theorem	lbinfle 8969*	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.) (Revised by AV, 4-Sep-2020.)
|- ( ( S C_ RR /\ E. x e. S A. y e. S x <_ y /\ A e. S ) -> inf ( S , RR , < ) <_ A )
Theorem	suprubex 8970*	A member of a nonempty bounded set of reals is less than or equal to the set's upper bound. (Contributed by Jim Kingdon, 18-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 -> B e. A )   =>    |- ( ph -> B <_ sup ( A , RR , < ) )
Theorem	suprlubex 8971*	The supremum of a nonempty bounded set of reals is the least upper bound. (Contributed by Jim Kingdon, 19-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 -> B e. RR )   =>    |- ( ph -> ( B < sup ( A , RR , < ) <-> E. z e. A B < z ) )
Theorem	suprnubex 8972*	An upper bound is not less than the supremum of a nonempty bounded set of reals. (Contributed by Jim Kingdon, 19-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 -> B e. RR )   =>    |- ( ph -> ( -. B < sup ( A , RR , < ) <-> A. z e. A -. B < z ) )
Theorem	suprleubex 8973*	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.)
|- ( 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 -> B e. RR )   =>    |- ( ph -> ( sup ( A , RR , < ) <_ B <-> A. z e. A z <_ B ) )
Theorem	negiso 8974	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	dfinfre 8975*	The infimum of a set of reals A. (Contributed by NM, 9-Oct-2005.) (Revised by AV, 4-Sep-2020.)
|- ( A C_ RR -> inf ( 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	sup3exmid 8976*	If any inhabited set of real numbers bounded from above has a supremum, excluded middle follows. (Contributed by Jim Kingdon, 2-Apr-2023.)
|- ( ( u C_ RR /\ E. w w e. u /\ E. x e. RR A. y e. u y <_ x ) -> E. x e. RR ( A. y e. u -. x < y /\ A. y e. RR ( y < x -> E. z e. u y < z ) ) )   =>    |- DECID ph
4.3.11  Imaginary and complex number properties
Theorem	crap0 8977	The real representation of complex numbers is apart from zero iff one of its terms is apart from zero. (Contributed by Jim Kingdon, 5-Mar-2020.)
|- ( ( A e. RR /\ B e. RR ) -> ( ( A # 0 \/ B # 0 ) <-> ( A + ( _i x. B ) ) # 0 ) )
Theorem	creur 8978*	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 8979*	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 8980*	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 ) )
4.3.12  Function operation analogue theorems
Theorem	ofnegsub 8981	Function analogue of negsub 8267. (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 ) )
4.4  Integer sets
4.4.1  Positive integers (as a subset of complex numbers)
Syntax	cn 8982	Extend class notation to include the class of positive integers.
class NN
Definition	df-inn 8983*	Definition of the set of positive integers. For naming consistency with the Metamath Proof Explorer usages should refer to dfnn2 8984 instead. (Contributed by Jeff Hankins, 12-Sep-2013.) (Revised by Mario Carneiro, 3-May-2014.) (New usage is discouraged.)
|- NN = |^| { x | ( 1 e. x /\ A. y e. x ( y + 1 ) e. x ) }
Theorem	dfnn2 8984*	Definition of the set of positive integers. Another name for df-inn 8983. (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	peano5nni 8985*	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 8986	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 8987	The positive integers are a subset of the complex numbers. (Contributed by NM, 2-Aug-2004.)
|- NN C_ CC
Theorem	nnex 8988	The set of positive integers exists. (Contributed by NM, 3-Oct-1999.) (Revised by Mario Carneiro, 17-Nov-2014.)
|- NN e. _V
Theorem	nnre 8989	A positive integer is a real number. (Contributed by NM, 18-Aug-1999.)
|- ( A e. NN -> A e. RR )
Theorem	nncn 8990	A positive integer is a complex number. (Contributed by NM, 18-Aug-1999.)
|- ( A e. NN -> A e. CC )
Theorem	nnrei 8991	A positive integer is a real number. (Contributed by NM, 18-Aug-1999.)
|- A e. NN   =>    |- A e. RR
Theorem	nncni 8992	A positive integer is a complex number. (Contributed by NM, 18-Aug-1999.)
|- A e. NN   =>    |- A e. CC
Theorem	1nn 8993	Peano postulate: 1 is a positive integer. (Contributed by NM, 11-Jan-1997.)
|- 1 e. NN
Theorem	peano2nn 8994	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	nnred 8995	A positive integer is a real number. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. NN )   =>    |- ( ph -> A e. RR )
Theorem	nncnd 8996	A positive integer is a complex number. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. NN )   =>    |- ( ph -> A e. CC )
Theorem	peano2nnd 8997	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 )
4.4.2  Principle of mathematical induction
Theorem	nnind 8998*	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 9002 for an example of its use. 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 8999*	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 8998 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 9000	Every positive integer is one or a successor. (Contributed by Mario Carneiro, 16-May-2014.)
|- ( A e. NN -> ( A = 1 \/ ( A - 1 ) e. NN ) )