P. 98 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 9701-9800   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	readdcld 9701	Closure law for addition of reals. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   =>    |- ( ph -> ( A + B ) e. RR )
Theorem	remulcld 9702	Closure law for multiplication of reals. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   =>    |- ( ph -> ( A x. B ) e. RR )
5.2.2  Infinity and the extended real number system
Syntax	cpnf 9703	Plus infinity.
class +oo
Syntax	cmnf 9704	Minus infinity.
class -oo
Syntax	cxr 9705	The set of extended reals (includes plus and minus infinity).
class RR*
Syntax	clt 9706	'Less than' predicate (extended to include the extended reals).
class <
Syntax	cle 9707	Extend wff notation to include the 'less than or equal to' relation.
class <_
Definition	df-pnf 9708	Define plus infinity. Note that the definition is arbitrary, requiring only that +oo be a set not in RR and different from -oo (df-mnf 9709). We use ~P U. CC to make it independent of the construction of CC, and Cantor's Theorem will show that it is different from any member of CC and therefore RR. See pnfnre 9713, mnfnre 9714, and pnfnemnf 11451. A simpler possibility is to define +oo as CC and -oo as { CC }, but that approach requires the Axiom of Regularity to show that +oo and -oo are different from each other and from all members of RR. (Contributed by NM, 13-Oct-2005.) (New usage is discouraged.)
|- +oo = ~P U. CC
Definition	df-mnf 9709	Define minus infinity as the power set of plus infinity. Note that the definition is arbitrary, requiring only that -oo be a set not in RR and different from +oo (see mnfnre 9714 and pnfnemnf 11451). (Contributed by NM, 13-Oct-2005.) (New usage is discouraged.)
|- -oo = ~P +oo
Definition	df-xr 9710	Define the set of extended reals that includes plus and minus infinity. Definition 12-3.1 of [Gleason] p. 173. (Contributed by NM, 13-Oct-2005.)
|- RR* = ( RR u. { +oo , -oo } )
Definition	df-ltxr 9711*	Define 'less than' on the set of extended reals. Definition 12-3.1 of [Gleason] p. 173. Note that in our postulates for complex numbers, <RR is primitive and not necessarily a relation on RR. (Contributed by NM, 13-Oct-2005.)
|- < = ( { <. x , y >. | ( x e. RR /\ y e. RR /\ x <RR y ) } u. ( ( ( RR u. { -oo } ) X. { +oo } ) u. ( { -oo } X. RR ) ) )
Definition	df-le 9712	Define 'less than or equal to' on the extended real subset of complex numbers. Theorem leloe 9751 relates it to 'less than' for reals. (Contributed by NM, 13-Oct-2005.)
|- <_ = ( ( RR* X. RR* ) \ `' < )
Theorem	pnfnre 9713	Plus infinity is not a real number. (Contributed by NM, 13-Oct-2005.)
|- +oo e/ RR
Theorem	mnfnre 9714	Minus infinity is not a real number. (Contributed by NM, 13-Oct-2005.)
|- -oo e/ RR
Theorem	ressxr 9715	The standard reals are a subset of the extended reals. (Contributed by NM, 14-Oct-2005.)
|- RR C_ RR*
Theorem	rexpssxrxp 9716	The Cartesian product of standard reals are a subset of the Cartesian product of extended reals (common case). (Contributed by David A. Wheeler, 8-Dec-2018.)
|- ( RR X. RR ) C_ ( RR* X. RR* )
Theorem	rexr 9717	A standard real is an extended real. (Contributed by NM, 14-Oct-2005.)
|- ( A e. RR -> A e. RR* )
Theorem	0xr 9718	Zero is an extended real. (Contributed by Mario Carneiro, 15-Jun-2014.)
|- 0 e. RR*
Theorem	renepnf 9719	No (finite) real equals plus infinity. (Contributed by NM, 14-Oct-2005.) (Proof shortened by Andrew Salmon, 19-Nov-2011.)
|- ( A e. RR -> A =/= +oo )
Theorem	renemnf 9720	No real equals minus infinity. (Contributed by NM, 14-Oct-2005.) (Proof shortened by Andrew Salmon, 19-Nov-2011.)
|- ( A e. RR -> A =/= -oo )
Theorem	rexrd 9721	A standard real is an extended real. (Contributed by Mario Carneiro, 28-May-2016.)
|- ( ph -> A e. RR )   =>    |- ( ph -> A e. RR* )
Theorem	renepnfd 9722	No (finite) real equals plus infinity. (Contributed by Mario Carneiro, 28-May-2016.)
|- ( ph -> A e. RR )   =>    |- ( ph -> A =/= +oo )
Theorem	renemnfd 9723	No real equals minus infinity. (Contributed by Mario Carneiro, 28-May-2016.)
|- ( ph -> A e. RR )   =>    |- ( ph -> A =/= -oo )
Theorem	rexri 9724	A standard real is an extended real (inference form.) (Contributed by David Moews, 28-Feb-2017.)
|- A e. RR   =>    |- A e. RR*
Theorem	renfdisj 9725	The reals and the infinities are disjoint. (Contributed by NM, 25-Oct-2005.) (Proof shortened by Andrew Salmon, 19-Nov-2011.)
|- ( RR i^i { +oo , -oo } ) = (/)
Theorem	ltrelxr 9726	'Less than' is a relation on extended reals. (Contributed by Mario Carneiro, 28-Apr-2015.)
|- < C_ ( RR* X. RR* )
Theorem	ltrel 9727	'Less than' is a relation. (Contributed by NM, 14-Oct-2005.)
|- Rel <
Theorem	lerelxr 9728	'Less than or equal' is a relation on extended reals. (Contributed by Mario Carneiro, 28-Apr-2015.)
|- <_ C_ ( RR* X. RR* )
Theorem	lerel 9729	'Less or equal to' is a relation. (Contributed by FL, 2-Aug-2009.) (Revised by Mario Carneiro, 28-Apr-2015.)
|- Rel <_
Theorem	xrlenlt 9730	'Less than or equal to' expressed in terms of 'less than', for extended reals. (Contributed by NM, 14-Oct-2005.)
|- ( ( A e. RR* /\ B e. RR* ) -> ( A <_ B <-> -. B < A ) )
Theorem	xrlenltd 9731	'Less than or equal to' expressed in terms of 'less than', for extended reals. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
|- ( ph -> A e. RR* )   &    |- ( ph -> B e. RR* )   =>    |- ( ph -> ( A <_ B <-> -. B < A ) )
Theorem	xrltnle 9732	'Less than' expressed in terms of 'less than or equal to', for extended reals. (Contributed by NM, 6-Feb-2007.)
|- ( ( A e. RR* /\ B e. RR* ) -> ( A < B <-> -. B <_ A ) )
Theorem	xrnltled 9733	'Not less than ' implies 'less than or equal to'. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- ( ph -> A e. RR* )   &    |- ( ph -> B e. RR* )   &    |- ( ph -> -. B < A )   =>    |- ( ph -> A <_ B )
Theorem	ssxr 9734	The three (non-exclusive) possibilities implied by a subset of extended reals. (Contributed by NM, 25-Oct-2005.) (Proof shortened by Andrew Salmon, 19-Nov-2011.)
|- ( A C_ RR* -> ( A C_ RR \/ +oo e. A \/ -oo e. A ) )
Theorem	ltxrlt 9735	The standard less-than <RR and the extended real less-than < are identical when restricted to the non-extended reals RR. (Contributed by NM, 13-Oct-2005.) (Revised by Mario Carneiro, 28-Apr-2015.)
|- ( ( A e. RR /\ B e. RR ) -> ( A < B <-> A <RR B ) )
5.2.3  Restate the ordering postulates with extended real "less than"
Theorem	axlttri 9736	Ordering on reals satisfies strict trichotomy. Axiom 18 of 22 for real and complex numbers, derived from ZF set theory. (This restates ax-pre-lttri 9644 with ordering on the extended reals.) (Contributed by NM, 13-Oct-2005.)
|- ( ( A e. RR /\ B e. RR ) -> ( A < B <-> -. ( A = B \/ B < A ) ) )
Theorem	axlttrn 9737	Ordering on reals is transitive. Axiom 19 of 22 for real and complex numbers, derived from ZF set theory. This restates ax-pre-lttrn 9645 with ordering on the extended reals. New proofs should use lttr 9741 instead for naming consistency. (New usage is discouraged.) (Contributed by NM, 13-Oct-2005.)
|- ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( ( A < B /\ B < C ) -> A < C ) )
Theorem	axltadd 9738	Ordering property of addition on reals. Axiom 20 of 22 for real and complex numbers, derived from ZF set theory. (This restates ax-pre-ltadd 9646 with ordering on the extended reals.) (Contributed by NM, 13-Oct-2005.)
|- ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( A < B -> ( C + A ) < ( C + B ) ) )
Theorem	axmulgt0 9739	The product of two positive reals is positive. Axiom 21 of 22 for real and complex numbers, derived from ZF set theory. (This restates ax-pre-mulgt0 9647 with ordering on the extended reals.) (Contributed by NM, 13-Oct-2005.)
|- ( ( A e. RR /\ B e. RR ) -> ( ( 0 < A /\ 0 < B ) -> 0 < ( A x. B ) ) )
Theorem	axsup 9740*	A nonempty, bounded-above set of reals has a supremum. Axiom 22 of 22 for real and complex numbers, derived from ZF set theory. (This restates ax-pre-sup 9648 with ordering on the extended reals.) (Contributed by NM, 13-Oct-2005.)
|- ( ( A C_ RR /\ A =/= (/) /\ E. x e. RR A. y e. A y < x ) -> E. x e. RR ( A. y e. A -. x < y /\ A. y e. RR ( y < x -> E. z e. A y < z ) ) )
5.2.4  Ordering on reals
Theorem	lttr 9741	Alias for axlttrn 9737, for naming consistency with lttri 9791. New proofs should generally use this instead of ax-pre-lttrn 9645. (Contributed by NM, 10-Mar-2008.)
|- ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( ( A < B /\ B < C ) -> A < C ) )
Theorem	mulgt0 9742	The product of two positive numbers is positive. (Contributed by NM, 10-Mar-2008.)
|- ( ( ( A e. RR /\ 0 < A ) /\ ( B e. RR /\ 0 < B ) ) -> 0 < ( A x. B ) )
Theorem	lenlt 9743	'Less than or equal to' expressed in terms of 'less than'. (Contributed by NM, 13-May-1999.)
|- ( ( A e. RR /\ B e. RR ) -> ( A <_ B <-> -. B < A ) )
Theorem	ltnle 9744	'Less than' expressed in terms of 'less than or equal to'. (Contributed by NM, 11-Jul-2005.)
|- ( ( A e. RR /\ B e. RR ) -> ( A < B <-> -. B <_ A ) )
Theorem	ltso 9745	'Less than' is a strict ordering. (Contributed by NM, 19-Jan-1997.)
|- < Or RR
Theorem	gtso 9746	'Greater than' is a strict ordering. (Contributed by JJ, 11-Oct-2018.)
|- `' < Or RR
Theorem	lttri2 9747	Consequence of trichotomy. (Contributed by NM, 9-Oct-1999.)
|- ( ( A e. RR /\ B e. RR ) -> ( A =/= B <-> ( A < B \/ B < A ) ) )
Theorem	lttri3 9748	Trichotomy law for 'less than'. (Contributed by NM, 5-May-1999.)
|- ( ( A e. RR /\ B e. RR ) -> ( A = B <-> ( -. A < B /\ -. B < A ) ) )
Theorem	lttri4 9749	Trichotomy law for 'less than'. (Contributed by NM, 20-Sep-2007.) (Proof shortened by Andrew Salmon, 19-Nov-2011.)
|- ( ( A e. RR /\ B e. RR ) -> ( A < B \/ A = B \/ B < A ) )
Theorem	letri3 9750	Trichotomy law. (Contributed by NM, 14-May-1999.)
|- ( ( A e. RR /\ B e. RR ) -> ( A = B <-> ( A <_ B /\ B <_ A ) ) )
Theorem	leloe 9751	'Less than or equal to' expressed in terms of 'less than' or 'equals'. (Contributed by NM, 13-May-1999.)
|- ( ( A e. RR /\ B e. RR ) -> ( A <_ B <-> ( A < B \/ A = B ) ) )
Theorem	eqlelt 9752	Equality in terms of 'less than or equal to', 'less than'. (Contributed by NM, 7-Apr-2001.)
|- ( ( A e. RR /\ B e. RR ) -> ( A = B <-> ( A <_ B /\ -. A < B ) ) )
Theorem	ltle 9753	'Less than' implies 'less than or equal to'. (Contributed by NM, 25-Aug-1999.)
|- ( ( A e. RR /\ B e. RR ) -> ( A < B -> A <_ B ) )
Theorem	leltne 9754	'Less than or equal to' implies 'less than' is not 'equals'. (Contributed by NM, 27-Jul-1999.)
|- ( ( A e. RR /\ B e. RR /\ A <_ B ) -> ( A < B <-> B =/= A ) )
Theorem	lelttr 9755	Transitive law. (Contributed by NM, 23-May-1999.)
|- ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( ( A <_ B /\ B < C ) -> A < C ) )
Theorem	ltletr 9756	Transitive law. (Contributed by NM, 25-Aug-1999.)
|- ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( ( A < B /\ B <_ C ) -> A < C ) )
Theorem	ltleletr 9757	Transitive law, weaker form of ltletr 9756. (Contributed by AV, 14-Oct-2018.)
|- ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( ( A < B /\ B <_ C ) -> A <_ C ) )
Theorem	letr 9758	Transitive law. (Contributed by NM, 12-Nov-1999.)
|- ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( ( A <_ B /\ B <_ C ) -> A <_ C ) )
Theorem	ltnr 9759	'Less than' is irreflexive. (Contributed by NM, 18-Aug-1999.)
|- ( A e. RR -> -. A < A )
Theorem	leid 9760	'Less than or equal to' is reflexive. (Contributed by NM, 18-Aug-1999.)
|- ( A e. RR -> A <_ A )
Theorem	ltne 9761	'Less than' implies not equal. (Contributed by NM, 9-Oct-1999.) (Revised by Mario Carneiro, 16-Sep-2015.)
|- ( ( A e. RR /\ A < B ) -> B =/= A )
Theorem	ltneOLD 9762	'Less than' implies not equal. (Contributed by NM, 9-Oct-1999.) (Proof modification is discouraged.) (New usage is discouraged.)
|- ( ( A e. RR /\ B e. RR /\ A < B ) -> B =/= A )
Theorem	ltnsym 9763	'Less than' is not symmetric. (Contributed by NM, 8-Jan-2002.)
|- ( ( A e. RR /\ B e. RR ) -> ( A < B -> -. B < A ) )
Theorem	ltnsym2 9764	'Less than' is antisymmetric and irreflexive. (Contributed by NM, 13-Aug-2005.) (Proof shortened by Andrew Salmon, 19-Nov-2011.)
|- ( ( A e. RR /\ B e. RR ) -> -. ( A < B /\ B < A ) )
Theorem	letric 9765	Trichotomy law. (Contributed by NM, 18-Aug-1999.) (Proof shortened by Andrew Salmon, 19-Nov-2011.)
|- ( ( A e. RR /\ B e. RR ) -> ( A <_ B \/ B <_ A ) )
Theorem	ltlen 9766	'Less than' expressed in terms of 'less than or equal to'. (Contributed by NM, 27-Oct-1999.)
|- ( ( A e. RR /\ B e. RR ) -> ( A < B <-> ( A <_ B /\ B =/= A ) ) )
Theorem	eqle 9767	Equality implies 'less than or equal to'. (Contributed by NM, 4-Apr-2005.)
|- ( ( A e. RR /\ A = B ) -> A <_ B )
Theorem	eqled 9768	Equality implies 'less than or equal to'. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- ( ph -> A e. RR )   &    |- ( ph -> A = B )   =>    |- ( ph -> A <_ B )
Theorem	ltadd2 9769	Addition to both sides of 'less than'. (Contributed by NM, 12-Nov-1999.) (Revised by Mario Carneiro, 27-May-2016.)
|- ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( A < B <-> ( C + A ) < ( C + B ) ) )
Theorem	ne0gt0 9770	A nonzero nonnegative number is positive. (Contributed by NM, 20-Nov-2007.)
|- ( ( A e. RR /\ 0 <_ A ) -> ( A =/= 0 <-> 0 < A ) )
Theorem	lecasei 9771	Ordering elimination by cases. (Contributed by NM, 6-Jul-2007.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ( ph /\ A <_ B ) -> ps )   &    |- ( ( ph /\ B <_ A ) -> ps )   =>    |- ( ph -> ps )
Theorem	lelttric 9772	Trichotomy law. (Contributed by NM, 4-Apr-2005.)
|- ( ( A e. RR /\ B e. RR ) -> ( A <_ B \/ B < A ) )
Theorem	ltlecasei 9773	Ordering elimination by cases. (Contributed by NM, 1-Jul-2007.) (Proof shortened by Mario Carneiro, 27-May-2016.)
|- ( ( ph /\ A < B ) -> ps )   &    |- ( ( ph /\ B <_ A ) -> ps )   &    |- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   =>    |- ( ph -> ps )
Theorem	ltnri 9774	'Less than' is irreflexive. (Contributed by NM, 18-Aug-1999.)
|- A e. RR   =>    |- -. A < A
Theorem	eqlei 9775	Equality implies 'less than or equal to'. (Contributed by NM, 23-May-1999.) (Revised by Alexander van der Vekens, 20-Mar-2018.)
|- A e. RR   =>    |- ( A = B -> A <_ B )
Theorem	eqlei2 9776	Equality implies 'less than or equal to'. (Contributed by Alexander van der Vekens, 20-Mar-2018.)
|- A e. RR   =>    |- ( B = A -> B <_ A )
Theorem	gtneii 9777	'Less than' implies not equal. (Contributed by Mario Carneiro, 30-Sep-2013.)
|- A e. RR   &    |- A < B   =>    |- B =/= A
Theorem	ltneii 9778	'Greater than' implies not equal. (Contributed by Mario Carneiro, 16-Sep-2015.)
|- A e. RR   &    |- A < B   =>    |- A =/= B
Theorem	lttri2i 9779	Consequence of trichotomy. (Contributed by NM, 19-Jan-1997.)
|- A e. RR   &    |- B e. RR   =>    |- ( A =/= B <-> ( A < B \/ B < A ) )
Theorem	lttri3i 9780	Consequence of trichotomy. (Contributed by NM, 14-May-1999.)
|- A e. RR   &    |- B e. RR   =>    |- ( A = B <-> ( -. A < B /\ -. B < A ) )
Theorem	letri3i 9781	Consequence of trichotomy. (Contributed by NM, 14-May-1999.)
|- A e. RR   &    |- B e. RR   =>    |- ( A = B <-> ( A <_ B /\ B <_ A ) )
Theorem	leloei 9782	'Less than or equal to' in terms of 'less than'. (Contributed by NM, 14-May-1999.)
|- A e. RR   &    |- B e. RR   =>    |- ( A <_ B <-> ( A < B \/ A = B ) )
Theorem	ltleni 9783	'Less than' expressed in terms of 'less than or equal to'. (Contributed by NM, 27-Oct-1999.)
|- A e. RR   &    |- B e. RR   =>    |- ( A < B <-> ( A <_ B /\ B =/= A ) )
Theorem	ltnsymi 9784	'Less than' is not symmetric. (Contributed by NM, 6-May-1999.)
|- A e. RR   &    |- B e. RR   =>    |- ( A < B -> -. B < A )
Theorem	lenlti 9785	'Less than or equal to' in terms of 'less than'. (Contributed by NM, 24-May-1999.)
|- A e. RR   &    |- B e. RR   =>    |- ( A <_ B <-> -. B < A )
Theorem	ltnlei 9786	'Less than' in terms of 'less than or equal to'. (Contributed by NM, 11-Jul-2005.)
|- A e. RR   &    |- B e. RR   =>    |- ( A < B <-> -. B <_ A )
Theorem	ltlei 9787	'Less than' implies 'less than or equal to'. (Contributed by NM, 14-May-1999.)
|- A e. RR   &    |- B e. RR   =>    |- ( A < B -> A <_ B )
Theorem	ltleii 9788	'Less than' implies 'less than or equal to' (inference). (Contributed by NM, 22-Aug-1999.)
|- A e. RR   &    |- B e. RR   &    |- A < B   =>    |- A <_ B
Theorem	ltnei 9789	'Less than' implies not equal. (Contributed by NM, 28-Jul-1999.)
|- A e. RR   &    |- B e. RR   =>    |- ( A < B -> B =/= A )
Theorem	letrii 9790	Trichotomy law for 'less than or equal to'. (Contributed by NM, 2-Aug-1999.)
|- A e. RR   &    |- B e. RR   =>    |- ( A <_ B \/ B <_ A )
Theorem	lttri 9791	'Less than' is transitive. Theorem I.17 of [Apostol] p. 20. (Contributed by NM, 14-May-1999.)
|- A e. RR   &    |- B e. RR   &    |- C e. RR   =>    |- ( ( A < B /\ B < C ) -> A < C )
Theorem	lelttri 9792	'Less than or equal to', 'less than' transitive law. (Contributed by NM, 14-May-1999.)
|- A e. RR   &    |- B e. RR   &    |- C e. RR   =>    |- ( ( A <_ B /\ B < C ) -> A < C )
Theorem	ltletri 9793	'Less than', 'less than or equal to' transitive law. (Contributed by NM, 14-May-1999.)
|- A e. RR   &    |- B e. RR   &    |- C e. RR   =>    |- ( ( A < B /\ B <_ C ) -> A < C )
Theorem	letri 9794	'Less than or equal to' is transitive. (Contributed by NM, 14-May-1999.)
|- A e. RR   &    |- B e. RR   &    |- C e. RR   =>    |- ( ( A <_ B /\ B <_ C ) -> A <_ C )
Theorem	le2tri3i 9795	Extended trichotomy law for 'less than or equal to'. (Contributed by NM, 14-Aug-2000.)
|- A e. RR   &    |- B e. RR   &    |- C e. RR   =>    |- ( ( A <_ B /\ B <_ C /\ C <_ A ) <-> ( A = B /\ B = C /\ C = A ) )
Theorem	ltadd2i 9796	Addition to both sides of 'less than'. (Contributed by NM, 21-Jan-1997.) (Proof shortened by OpenAI, 25-Mar-2020.)
|- A e. RR   &    |- B e. RR   &    |- C e. RR   =>    |- ( A < B <-> ( C + A ) < ( C + B ) )
Theorem	ltadd2iOLD 9797	Addition to both sides of 'less than'. (Contributed by NM, 21-Jan-1997.) (Proof shortened by Paul Chapman, 27-Jan-2008.) Obsolete version of ltadd2i 9796 as of 25-Mar-2020. (New usage is discouraged.) (Proof modification is discouraged.)
|- A e. RR   &    |- B e. RR   &    |- C e. RR   =>    |- ( A < B <-> ( C + A ) < ( C + B ) )
Theorem	mulgt0i 9798	The product of two positive numbers is positive. (Contributed by NM, 16-May-1999.)
|- A e. RR   &    |- B e. RR   =>    |- ( ( 0 < A /\ 0 < B ) -> 0 < ( A x. B ) )
Theorem	mulgt0ii 9799	The product of two positive numbers is positive. (Contributed by NM, 18-May-1999.)
|- A e. RR   &    |- B e. RR   &    |- 0 < A   &    |- 0 < B   =>    |- 0 < ( A x. B )
Theorem	ltnrd 9800	'Less than' is irreflexive. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. RR )   =>    |- ( ph -> -. A < A )