P. 89 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 8801-8900   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	lt2addi 8801	Adding both side of two inequalities. Theorem I.25 of [Apostol] p. 20. (Contributed by NM, 14-May-1999.)
|- A e. RR   &    |- B e. RR   &    |- C e. RR   &    |- D e. RR   =>    |- ( ( A < C /\ B < D ) -> ( A + B ) < ( C + D ) )
Theorem	le2addi 8802	Adding both side of two inequalities. (Contributed by NM, 16-Sep-1999.)
|- A e. RR   &    |- B e. RR   &    |- C e. RR   &    |- D e. RR   =>    |- ( ( A <_ C /\ B <_ D ) -> ( A + B ) <_ ( C + D ) )
Theorem	gt0ne0d 8803	Positive implies nonzero. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> 0 < A )   =>    |- ( ph -> A =/= 0 )
Theorem	lt0ne0d 8804	Something less than zero is not zero. Deduction form. See also lt0ap0d 8940 which is similar but for apartness. (Contributed by David Moews, 28-Feb-2017.)
|- ( ph -> A < 0 )   =>    |- ( ph -> A =/= 0 )
Theorem	leidd 8805	'Less than or equal to' is reflexive. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. RR )   =>    |- ( ph -> A <_ A )
Theorem	lt0neg1d 8806	Comparison of a number and its negative to zero. Theorem I.23 of [Apostol] p. 20. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. RR )   =>    |- ( ph -> ( A < 0 <-> 0 < -u A ) )
Theorem	lt0neg2d 8807	Comparison of a number and its negative to zero. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. RR )   =>    |- ( ph -> ( 0 < A <-> -u A < 0 ) )
Theorem	le0neg1d 8808	Comparison of a number and its negative to zero. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. RR )   =>    |- ( ph -> ( A <_ 0 <-> 0 <_ -u A ) )
Theorem	le0neg2d 8809	Comparison of a number and its negative to zero. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. RR )   =>    |- ( ph -> ( 0 <_ A <-> -u A <_ 0 ) )
Theorem	addgegt0d 8810	Addition of nonnegative and positive numbers is positive. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> 0 <_ A )   &    |- ( ph -> 0 < B )   =>    |- ( ph -> 0 < ( A + B ) )
Theorem	addgtge0d 8811	Addition of positive and nonnegative numbers is positive. (Contributed by Asger C. Ipsen, 12-May-2021.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> 0 < A )   &    |- ( ph -> 0 <_ B )   =>    |- ( ph -> 0 < ( A + B ) )
Theorem	addgt0d 8812	Addition of 2 positive numbers is positive. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> 0 < A )   &    |- ( ph -> 0 < B )   =>    |- ( ph -> 0 < ( A + B ) )
Theorem	addge0d 8813	Addition of 2 nonnegative numbers is nonnegative. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> 0 <_ A )   &    |- ( ph -> 0 <_ B )   =>    |- ( ph -> 0 <_ ( A + B ) )
Theorem	ltnegd 8814	Negative of both sides of 'less than'. Theorem I.23 of [Apostol] p. 20. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   =>    |- ( ph -> ( A < B <-> -u B < -u A ) )
Theorem	lenegd 8815	Negative of both sides of 'less than or equal to'. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   =>    |- ( ph -> ( A <_ B <-> -u B <_ -u A ) )
Theorem	ltnegcon1d 8816	Contraposition of negative in 'less than'. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> -u A < B )   =>    |- ( ph -> -u B < A )
Theorem	ltnegcon2d 8817	Contraposition of negative in 'less than'. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> A < -u B )   =>    |- ( ph -> B < -u A )
Theorem	lenegcon1d 8818	Contraposition of negative in 'less than or equal to'. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> -u A <_ B )   =>    |- ( ph -> -u B <_ A )
Theorem	lenegcon2d 8819	Contraposition of negative in 'less than or equal to'. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> A <_ -u B )   =>    |- ( ph -> B <_ -u A )
Theorem	ltaddposd 8820	Adding a positive number to another number increases it. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   =>    |- ( ph -> ( 0 < A <-> B < ( B + A ) ) )
Theorem	ltaddpos2d 8821	Adding a positive number to another number increases it. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   =>    |- ( ph -> ( 0 < A <-> B < ( A + B ) ) )
Theorem	ltsubposd 8822	Subtracting a positive number from another number decreases it. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   =>    |- ( ph -> ( 0 < A <-> ( B - A ) < B ) )
Theorem	posdifd 8823	Comparison of two numbers whose difference is positive. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   =>    |- ( ph -> ( A < B <-> 0 < ( B - A ) ) )
Theorem	addge01d 8824	A number is less than or equal to itself plus a nonnegative number. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   =>    |- ( ph -> ( 0 <_ B <-> A <_ ( A + B ) ) )
Theorem	addge02d 8825	A number is less than or equal to itself plus a nonnegative number. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   =>    |- ( ph -> ( 0 <_ B <-> A <_ ( B + A ) ) )
Theorem	subge0d 8826	Nonnegative subtraction. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   =>    |- ( ph -> ( 0 <_ ( A - B ) <-> B <_ A ) )
Theorem	suble0d 8827	Nonpositive subtraction. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   =>    |- ( ph -> ( ( A - B ) <_ 0 <-> A <_ B ) )
Theorem	subge02d 8828	Nonnegative subtraction. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   =>    |- ( ph -> ( 0 <_ B <-> ( A - B ) <_ A ) )
Theorem	ltadd1d 8829	Addition to both sides of 'less than'. Theorem I.18 of [Apostol] p. 20. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> C e. RR )   =>    |- ( ph -> ( A < B <-> ( A + C ) < ( B + C ) ) )
Theorem	leadd1d 8830	Addition to both sides of 'less than or equal to'. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> C e. RR )   =>    |- ( ph -> ( A <_ B <-> ( A + C ) <_ ( B + C ) ) )
Theorem	leadd2d 8831	Addition to both sides of 'less than or equal to'. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> C e. RR )   =>    |- ( ph -> ( A <_ B <-> ( C + A ) <_ ( C + B ) ) )
Theorem	ltsubaddd 8832	'Less than' relationship between subtraction and addition. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> C e. RR )   =>    |- ( ph -> ( ( A - B ) < C <-> A < ( C + B ) ) )
Theorem	lesubaddd 8833	'Less than or equal to' relationship between subtraction and addition. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> C e. RR )   =>    |- ( ph -> ( ( A - B ) <_ C <-> A <_ ( C + B ) ) )
Theorem	ltsubadd2d 8834	'Less than' relationship between subtraction and addition. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> C e. RR )   =>    |- ( ph -> ( ( A - B ) < C <-> A < ( B + C ) ) )
Theorem	lesubadd2d 8835	'Less than or equal to' relationship between subtraction and addition. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> C e. RR )   =>    |- ( ph -> ( ( A - B ) <_ C <-> A <_ ( B + C ) ) )
Theorem	ltaddsubd 8836	'Less than' relationship between subtraction and addition. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> C e. RR )   =>    |- ( ph -> ( ( A + B ) < C <-> A < ( C - B ) ) )
Theorem	ltaddsub2d 8837	'Less than' relationship between subtraction and addition. (Contributed by Mario Carneiro, 29-Dec-2016.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> C e. RR )   =>    |- ( ph -> ( ( A + B ) < C <-> B < ( C - A ) ) )
Theorem	leaddsub2d 8838	'Less than or equal to' relationship between and addition and subtraction. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> C e. RR )   =>    |- ( ph -> ( ( A + B ) <_ C <-> B <_ ( C - A ) ) )
Theorem	subled 8839	Swap subtrahends in an inequality. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> C e. RR )   &    |- ( ph -> ( A - B ) <_ C )   =>    |- ( ph -> ( A - C ) <_ B )
Theorem	lesubd 8840	Swap subtrahends in an inequality. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> C e. RR )   &    |- ( ph -> A <_ ( B - C ) )   =>    |- ( ph -> C <_ ( B - A ) )
Theorem	ltsub23d 8841	'Less than' relationship between subtraction and addition. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> C e. RR )   &    |- ( ph -> ( A - B ) < C )   =>    |- ( ph -> ( A - C ) < B )
Theorem	ltsub13d 8842	'Less than' relationship between subtraction and addition. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> C e. RR )   &    |- ( ph -> A < ( B - C ) )   =>    |- ( ph -> C < ( B - A ) )
Theorem	lesub1d 8843	Subtraction from both sides of 'less than or equal to'. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> C e. RR )   =>    |- ( ph -> ( A <_ B <-> ( A - C ) <_ ( B - C ) ) )
Theorem	lesub2d 8844	Subtraction of both sides of 'less than or equal to'. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> C e. RR )   =>    |- ( ph -> ( A <_ B <-> ( C - B ) <_ ( C - A ) ) )
Theorem	ltsub1d 8845	Subtraction from both sides of 'less than'. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> C e. RR )   =>    |- ( ph -> ( A < B <-> ( A - C ) < ( B - C ) ) )
Theorem	ltsub2d 8846	Subtraction of both sides of 'less than'. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> C e. RR )   =>    |- ( ph -> ( A < B <-> ( C - B ) < ( C - A ) ) )
Theorem	ltadd1dd 8847	Addition to both sides of 'less than'. Theorem I.18 of [Apostol] p. 20. (Contributed by Mario Carneiro, 30-May-2016.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> C e. RR )   &    |- ( ph -> A < B )   =>    |- ( ph -> ( A + C ) < ( B + C ) )
Theorem	ltsub1dd 8848	Subtraction from both sides of 'less than'. (Contributed by Mario Carneiro, 30-May-2016.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> C e. RR )   &    |- ( ph -> A < B )   =>    |- ( ph -> ( A - C ) < ( B - C ) )
Theorem	ltsub2dd 8849	Subtraction of both sides of 'less than'. (Contributed by Mario Carneiro, 30-May-2016.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> C e. RR )   &    |- ( ph -> A < B )   =>    |- ( ph -> ( C - B ) < ( C - A ) )
Theorem	leadd1dd 8850	Addition to both sides of 'less than or equal to'. (Contributed by Mario Carneiro, 30-May-2016.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> C e. RR )   &    |- ( ph -> A <_ B )   =>    |- ( ph -> ( A + C ) <_ ( B + C ) )
Theorem	leadd2dd 8851	Addition to both sides of 'less than or equal to'. (Contributed by Mario Carneiro, 30-May-2016.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> C e. RR )   &    |- ( ph -> A <_ B )   =>    |- ( ph -> ( C + A ) <_ ( C + B ) )
Theorem	lesub1dd 8852	Subtraction from both sides of 'less than or equal to'. (Contributed by Mario Carneiro, 30-May-2016.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> C e. RR )   &    |- ( ph -> A <_ B )   =>    |- ( ph -> ( A - C ) <_ ( B - C ) )
Theorem	lesub2dd 8853	Subtraction of both sides of 'less than or equal to'. (Contributed by Mario Carneiro, 30-May-2016.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> C e. RR )   &    |- ( ph -> A <_ B )   =>    |- ( ph -> ( C - B ) <_ ( C - A ) )
Theorem	le2addd 8854	Adding both side of two inequalities. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> C e. RR )   &    |- ( ph -> D e. RR )   &    |- ( ph -> A <_ C )   &    |- ( ph -> B <_ D )   =>    |- ( ph -> ( A + B ) <_ ( C + D ) )
Theorem	le2subd 8855	Subtracting both sides of two 'less than or equal to' relations. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> C e. RR )   &    |- ( ph -> D e. RR )   &    |- ( ph -> A <_ C )   &    |- ( ph -> B <_ D )   =>    |- ( ph -> ( A - D ) <_ ( C - B ) )
Theorem	ltleaddd 8856	Adding both sides of two orderings. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> C e. RR )   &    |- ( ph -> D e. RR )   &    |- ( ph -> A < C )   &    |- ( ph -> B <_ D )   =>    |- ( ph -> ( A + B ) < ( C + D ) )
Theorem	leltaddd 8857	Adding both sides of two orderings. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> C e. RR )   &    |- ( ph -> D e. RR )   &    |- ( ph -> A <_ C )   &    |- ( ph -> B < D )   =>    |- ( ph -> ( A + B ) < ( C + D ) )
Theorem	lt2addd 8858	Adding both side of two inequalities. Theorem I.25 of [Apostol] p. 20. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> C e. RR )   &    |- ( ph -> D e. RR )   &    |- ( ph -> A < C )   &    |- ( ph -> B < D )   =>    |- ( ph -> ( A + B ) < ( C + D ) )
Theorem	lt2subd 8859	Subtracting both sides of two 'less than' relations. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> C e. RR )   &    |- ( ph -> D e. RR )   &    |- ( ph -> A < C )   &    |- ( ph -> B < D )   =>    |- ( ph -> ( A - D ) < ( C - B ) )
Theorem	possumd 8860	Condition for a positive sum. (Contributed by Scott Fenton, 16-Dec-2017.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   =>    |- ( ph -> ( 0 < ( A + B ) <-> -u B < A ) )
Theorem	sublt0d 8861	When a subtraction gives a negative result. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   =>    |- ( ph -> ( ( A - B ) < 0 <-> A < B ) )
Theorem	ltaddsublt 8862	Addition and subtraction on one side of 'less than'. (Contributed by AV, 24-Nov-2018.)
|- ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( B < C <-> ( ( A + B ) - C ) < A ) )
Theorem	1le1 8863	1 <_ 1. Common special case. (Contributed by David A. Wheeler, 16-Jul-2016.)
|- 1 <_ 1
Theorem	gt0add 8864	A positive sum must have a positive addend. Part of Definition 11.2.7(vi) of [HoTT], p. (varies). (Contributed by Jim Kingdon, 26-Jan-2020.)
|- ( ( A e. RR /\ B e. RR /\ 0 < ( A + B ) ) -> ( 0 < A \/ 0 < B ) )
4.3.5  Real Apartness
Syntax	creap 8865	Class of real apartness relation.
class #ℝ
Definition	df-reap 8866*	Define real apartness. Definition in Section 11.2.1 of [HoTT], p. (varies). Although #ℝ is an apartness relation on the reals (see df-ap 8873 for more discussion of apartness relations), for our purposes it is just a stepping stone to defining # which is an apartness relation on complex numbers. On the reals, #ℝ and # agree (apreap 8878). (Contributed by Jim Kingdon, 26-Jan-2020.)
|- #ℝ = { <. x , y >. | ( ( x e. RR /\ y e. RR ) /\ ( x < y \/ y < x ) ) }
Theorem	reapval 8867	Real apartness in terms of classes. Beyond the development of # itself, proofs should use reaplt 8879 instead. (New usage is discouraged.) (Contributed by Jim Kingdon, 29-Jan-2020.)
|- ( ( A e. RR /\ B e. RR ) -> ( A #ℝ B <-> ( A < B \/ B < A ) ) )
Theorem	reapirr 8868	Real apartness is irreflexive. Part of Definition 11.2.7(v) of [HoTT], p. (varies). Beyond the development of # itself, proofs should use apirr 8896 instead. (Contributed by Jim Kingdon, 26-Jan-2020.)
|- ( A e. RR -> -. A #ℝ A )
Theorem	recexre 8869*	Existence of reciprocal of real number. (Contributed by Jim Kingdon, 29-Jan-2020.)
|- ( ( A e. RR /\ A #ℝ 0 ) -> E. x e. RR ( A x. x ) = 1 )
Theorem	reapti 8870	Real apartness is tight. Beyond the development of apartness itself, proofs should use apti 8913. (Contributed by Jim Kingdon, 30-Jan-2020.) (New usage is discouraged.)
|- ( ( A e. RR /\ B e. RR ) -> ( A = B <-> -. A #ℝ B ) )
Theorem	recexgt0 8871*	Existence of reciprocal of positive real number. (Contributed by Jim Kingdon, 6-Feb-2020.)
|- ( ( A e. RR /\ 0 < A ) -> E. x e. RR ( 0 < x /\ ( A x. x ) = 1 ) )
4.3.6  Complex Apartness
Syntax	cap 8872	Class of complex apartness relation.
class #
Definition	df-ap 8873*	Define complex apartness. Definition 6.1 of [Geuvers], p. 17. Two numbers are considered apart if it is possible to separate them. One common usage is that we can divide by a number if it is apart from zero (see for example recclap 8970 which says that a number apart from zero has a reciprocal). The defining characteristics of an apartness are irreflexivity (apirr 8896), symmetry (apsym 8897), and cotransitivity (apcotr 8898). Apartness implies negated equality, as seen at apne 8914, and the converse would also follow if we assumed excluded middle. In addition, apartness of complex numbers is tight, which means that two numbers which are not apart are equal (apti 8913). (Contributed by Jim Kingdon, 26-Jan-2020.)
|- # = { <. x , y >. | E. r e. RR E. s e. RR E. t e. RR E. u e. RR ( ( x = ( r + ( _i x. s ) ) /\ y = ( t + ( _i x. u ) ) ) /\ ( r #ℝ t \/ s #ℝ u ) ) }
Theorem	ixi 8874	_i times itself is minus 1. (Contributed by NM, 6-May-1999.) (Proof shortened by Andrew Salmon, 19-Nov-2011.)
|- ( _i x. _i ) = -u 1
Theorem	inelr 8875	The imaginary unit _i is not a real number. (Contributed by NM, 6-May-1999.)
|- -. _i e. RR
Theorem	rimul 8876	A real number times the imaginary unit is real only if the number is 0. (Contributed by NM, 28-May-1999.) (Revised by Mario Carneiro, 27-May-2016.)
|- ( ( A e. RR /\ ( _i x. A ) e. RR ) -> A = 0 )
Theorem	rereim 8877	Decomposition of a real number into real part (itself) and imaginary part (zero). (Contributed by Jim Kingdon, 30-Jan-2020.)
|- ( ( ( A e. RR /\ B e. RR ) /\ ( C e. RR /\ A = ( B + ( _i x. C ) ) ) ) -> ( B = A /\ C = 0 ) )
Theorem	apreap 8878	Complex apartness and real apartness agree on the real numbers. (Contributed by Jim Kingdon, 31-Jan-2020.)
|- ( ( A e. RR /\ B e. RR ) -> ( A # B <-> A #ℝ B ) )
Theorem	reaplt 8879	Real apartness in terms of less than. Part of Definition 11.2.7(vi) of [HoTT], p. (varies). (Contributed by Jim Kingdon, 1-Feb-2020.)
|- ( ( A e. RR /\ B e. RR ) -> ( A # B <-> ( A < B \/ B < A ) ) )
Theorem	reapltxor 8880	Real apartness in terms of less than (exclusive-or version). (Contributed by Jim Kingdon, 23-Mar-2020.)
|- ( ( A e. RR /\ B e. RR ) -> ( A # B <-> ( A < B \/_ B < A ) ) )
Theorem	1ap0 8881	One is apart from zero. (Contributed by Jim Kingdon, 24-Feb-2020.)
|- 1 # 0
Theorem	ltmul1a 8882	Multiplication of both sides of 'less than' by a positive number. Theorem I.19 of [Apostol] p. 20. (Contributed by NM, 15-May-1999.) (Revised by Mario Carneiro, 27-May-2016.)
|- ( ( ( A e. RR /\ B e. RR /\ ( C e. RR /\ 0 < C ) ) /\ A < B ) -> ( A x. C ) < ( B x. C ) )
Theorem	ltmul1 8883	Multiplication of both sides of 'less than' by a positive number. Theorem I.19 of [Apostol] p. 20. Part of Definition 11.2.7(vi) of [HoTT], p. (varies). (Contributed by NM, 13-Feb-2005.) (Revised by Mario Carneiro, 27-May-2016.)
|- ( ( A e. RR /\ B e. RR /\ ( C e. RR /\ 0 < C ) ) -> ( A < B <-> ( A x. C ) < ( B x. C ) ) )
Theorem	lemul1 8884	Multiplication of both sides of 'less than or equal to' by a positive number. (Contributed by NM, 21-Feb-2005.)
|- ( ( A e. RR /\ B e. RR /\ ( C e. RR /\ 0 < C ) ) -> ( A <_ B <-> ( A x. C ) <_ ( B x. C ) ) )
Theorem	reapmul1lem 8885	Lemma for reapmul1 8886. (Contributed by Jim Kingdon, 8-Feb-2020.)
|- ( ( A e. RR /\ B e. RR /\ ( C e. RR /\ 0 < C ) ) -> ( A # B <-> ( A x. C ) # ( B x. C ) ) )
Theorem	reapmul1 8886	Multiplication of both sides of real apartness by a real number apart from zero. Special case of apmul1 9079. (Contributed by Jim Kingdon, 8-Feb-2020.)
|- ( ( A e. RR /\ B e. RR /\ ( C e. RR /\ C # 0 ) ) -> ( A # B <-> ( A x. C ) # ( B x. C ) ) )
Theorem	reapadd1 8887	Real addition respects apartness. (Contributed by Jim Kingdon, 13-Feb-2020.)
|- ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( A # B <-> ( A + C ) # ( B + C ) ) )
Theorem	reapneg 8888	Real negation respects apartness. (Contributed by Jim Kingdon, 13-Feb-2020.)
|- ( ( A e. RR /\ B e. RR ) -> ( A # B <-> -u A # -u B ) )
Theorem	reapcotr 8889	Real apartness is cotransitive. Part of Definition 11.2.7(v) of [HoTT], p. (varies). (Contributed by Jim Kingdon, 16-Feb-2020.)
|- ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( A # B -> ( A # C \/ B # C ) ) )
Theorem	remulext1 8890	Left extensionality for multiplication. (Contributed by Jim Kingdon, 19-Feb-2020.)
|- ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( ( A x. C ) # ( B x. C ) -> A # B ) )
Theorem	remulext2 8891	Right extensionality for real multiplication. (Contributed by Jim Kingdon, 22-Feb-2020.)
|- ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( ( C x. A ) # ( C x. B ) -> A # B ) )
Theorem	apsqgt0 8892	The square of a real number apart from zero is positive. (Contributed by Jim Kingdon, 7-Feb-2020.)
|- ( ( A e. RR /\ A # 0 ) -> 0 < ( A x. A ) )
Theorem	cru 8893	The representation of complex numbers in terms of real and imaginary parts 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. RR /\ B e. RR ) /\ ( C e. RR /\ D e. RR ) ) -> ( ( A + ( _i x. B ) ) = ( C + ( _i x. D ) ) <-> ( A = C /\ B = D ) ) )
Theorem	apreim 8894	Complex apartness in terms of real and imaginary parts. (Contributed by Jim Kingdon, 12-Feb-2020.)
|- ( ( ( A e. RR /\ B e. RR ) /\ ( C e. RR /\ D e. RR ) ) -> ( ( A + ( _i x. B ) ) # ( C + ( _i x. D ) ) <-> ( A # C \/ B # D ) ) )
Theorem	mulreim 8895	Complex multiplication in terms of real and imaginary parts. (Contributed by Jim Kingdon, 23-Feb-2020.)
|- ( ( ( A e. RR /\ B e. RR ) /\ ( C e. RR /\ D e. RR ) ) -> ( ( A + ( _i x. B ) ) x. ( C + ( _i x. D ) ) ) = ( ( ( A x. C ) + -u ( B x. D ) ) + ( _i x. ( ( C x. B ) + ( D x. A ) ) ) ) )
Theorem	apirr 8896	Apartness is irreflexive. (Contributed by Jim Kingdon, 16-Feb-2020.)
|- ( A e. CC -> -. A # A )
Theorem	apsym 8897	Apartness is symmetric. This theorem for real numbers is part of Definition 11.2.7(v) of [HoTT], p. (varies). (Contributed by Jim Kingdon, 16-Feb-2020.)
|- ( ( A e. CC /\ B e. CC ) -> ( A # B <-> B # A ) )
Theorem	apcotr 8898	Apartness is cotransitive. (Contributed by Jim Kingdon, 16-Feb-2020.)
|- ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( A # B -> ( A # C \/ B # C ) ) )
Theorem	apadd1 8899	Addition respects apartness. Analogue of addcan 8469 for apartness. (Contributed by Jim Kingdon, 13-Feb-2020.)
|- ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( A # B <-> ( A + C ) # ( B + C ) ) )
Theorem	apadd2 8900	Addition respects apartness. (Contributed by Jim Kingdon, 16-Feb-2020.)
|- ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( A # B <-> ( C + A ) # ( C + B ) ) )