P. 93 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 9201-9300   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	lemuldiv 9201	'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 ) ) -> ( ( A x. C ) <_ B <-> A <_ ( B / C ) ) )
Theorem	lemuldiv2 9202	'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 9203	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 9204	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 9205	Lemma for lt2msq 9206. (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 9206	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 9207	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 9208	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 9209	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 9210	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 9211	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 9212	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 9213	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 9214	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 9215	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 9216	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 9217	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 9218	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 9219	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 9220	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 9221	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 9222	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 9223	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 9224*	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 9225	A number is less than itself plus 1. (Contributed by NM, 20-Aug-2001.)
|- A e. RR   =>    |- A < ( A + 1 )
Theorem	recgt0i 9226	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 9227	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 9228	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 9229	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 9230	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 9231	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 9232	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 9233	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 9234	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 9235	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 9236	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 9237	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 9238	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 9239	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 9240	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 9241	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 9242	'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 9243	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 9244	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 9245	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 9246	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 9247	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 9248	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 9249	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 9250	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 9251	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 9252	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 9253	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 9254	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 9255	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 9256	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 9257	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 9258	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 9259	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 9260	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 9261	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 9262	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 9263	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 9264	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 9265*	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 9266*	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 9267*	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 9268*	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 9269*	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 9270*	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 9271*	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 9272*	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 9273*	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 9274*	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 9275	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 9276*	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 9277*	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 9278	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 9279*	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 9280*	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 9281*	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 9282	Function analogue of negsub 8564. (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 9283	Extend class notation to include the class of positive integers.
class NN
Definition	df-inn 9284*	Definition of the set of positive integers. For naming consistency with the Metamath Proof Explorer usages should refer to dfnn2 9285 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 9285*	Definition of the set of positive integers. Another name for df-inn 9284. (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 9286*	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 9287	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 9288	The positive integers are a subset of the complex numbers. (Contributed by NM, 2-Aug-2004.)
|- NN C_ CC
Theorem	nnex 9289	The set of positive integers exists. (Contributed by NM, 3-Oct-1999.) (Revised by Mario Carneiro, 17-Nov-2014.)
|- NN e. _V
Theorem	nnre 9290	A positive integer is a real number. (Contributed by NM, 18-Aug-1999.)
|- ( A e. NN -> A e. RR )
Theorem	nncn 9291	A positive integer is a complex number. (Contributed by NM, 18-Aug-1999.)
|- ( A e. NN -> A e. CC )
Theorem	nnrei 9292	A positive integer is a real number. (Contributed by NM, 18-Aug-1999.)
|- A e. NN   =>    |- A e. RR
Theorem	nncni 9293	A positive integer is a complex number. (Contributed by NM, 18-Aug-1999.)
|- A e. NN   =>    |- A e. CC
Theorem	1nn 9294	Peano postulate: 1 is a positive integer. (Contributed by NM, 11-Jan-1997.)
|- 1 e. NN
Theorem	peano2nn 9295	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 9296	A positive integer is a real number. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. NN )   =>    |- ( ph -> A e. RR )
Theorem	nncnd 9297	A positive integer is a complex number. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. NN )   =>    |- ( ph -> A e. CC )
Theorem	peano2nnd 9298	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 9299*	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 9303 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 9300*	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 9299 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 )