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	gt0add 8901	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 8902	Class of real apartness relation.
class #ℝ
Definition	df-reap 8903*	Define real apartness. Definition in Section 11.2.1 of [HoTT], p. (varies). Although #ℝ is an apartness relation on the reals (see df-ap 8910 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 8915). (Contributed by Jim Kingdon, 26-Jan-2020.)
|- #ℝ = { <. x , y >. | ( ( x e. RR /\ y e. RR ) /\ ( x < y \/ y < x ) ) }
Theorem	reapval 8904	Real apartness in terms of classes. Beyond the development of # itself, proofs should use reaplt 8916 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 8905	Real apartness is irreflexive. Part of Definition 11.2.7(v) of [HoTT], p. (varies). Beyond the development of # itself, proofs should use apirr 8933 instead. (Contributed by Jim Kingdon, 26-Jan-2020.)
|- ( A e. RR -> -. A #ℝ A )
Theorem	recexre 8906*	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 8907	Real apartness is tight. Beyond the development of apartness itself, proofs should use apti 8950. (Contributed by Jim Kingdon, 30-Jan-2020.) (New usage is discouraged.)
|- ( ( A e. RR /\ B e. RR ) -> ( A = B <-> -. A #ℝ B ) )
Theorem	recexgt0 8908*	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 8909	Class of complex apartness relation.
class #
Definition	df-ap 8910*	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 9009 which says that a number apart from zero has a reciprocal). The defining characteristics of an apartness are irreflexivity (apirr 8933), symmetry (apsym 8934), and cotransitivity (apcotr 8935). Apartness implies negated equality, as seen at apne 8951, 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 8950). (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 8911	_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 8912	The imaginary unit _i is not a real number. (Contributed by NM, 6-May-1999.)
|- -. _i e. RR
Theorem	rimul 8913	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 8914	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 8915	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 8916	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 8917	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 8918	One is apart from zero. (Contributed by Jim Kingdon, 24-Feb-2020.)
|- 1 # 0
Theorem	ltmul1a 8919	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 8920	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 8921	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 8922	Lemma for reapmul1 8923. (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 8923	Multiplication of both sides of real apartness by a real number apart from zero. Special case of apmul1 9118. (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 8924	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 8925	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 8926	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 8927	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 8928	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 8929	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 8930	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 8931	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 8932	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 8933	Apartness is irreflexive. (Contributed by Jim Kingdon, 16-Feb-2020.)
|- ( A e. CC -> -. A # A )
Theorem	apsym 8934	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 8935	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 8936	Addition respects apartness. Analogue of addcan 8506 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 8937	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 ) ) )
Theorem	addext 8938	Strong extensionality for addition. Given excluded middle, apartness would be equivalent to negated equality and this would follow readily (for all operations) from oveq12 6094. For us, it is proved a different way. (Contributed by Jim Kingdon, 15-Feb-2020.)
|- ( ( ( A e. CC /\ B e. CC ) /\ ( C e. CC /\ D e. CC ) ) -> ( ( A + B ) # ( C + D ) -> ( A # C \/ B # D ) ) )
Theorem	apneg 8939	Negation respects apartness. (Contributed by Jim Kingdon, 14-Feb-2020.)
|- ( ( A e. CC /\ B e. CC ) -> ( A # B <-> -u A # -u B ) )
Theorem	mulext1 8940	Left extensionality for complex multiplication. (Contributed by Jim Kingdon, 22-Feb-2020.)
|- ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( ( A x. C ) # ( B x. C ) -> A # B ) )
Theorem	mulext2 8941	Right extensionality for complex multiplication. (Contributed by Jim Kingdon, 22-Feb-2020.)
|- ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( ( C x. A ) # ( C x. B ) -> A # B ) )
Theorem	mulext 8942	Strong extensionality for multiplication. Given excluded middle, apartness would be equivalent to negated equality and this would follow readily (for all operations) from oveq12 6094. For us, it is proved a different way. (Contributed by Jim Kingdon, 23-Feb-2020.)
|- ( ( ( A e. CC /\ B e. CC ) /\ ( C e. CC /\ D e. CC ) ) -> ( ( A x. B ) # ( C x. D ) -> ( A # C \/ B # D ) ) )
Theorem	mulap0r 8943	A product apart from zero. Lemma 2.13 of [Geuvers], p. 6. (Contributed by Jim Kingdon, 24-Feb-2020.)
|- ( ( A e. CC /\ B e. CC /\ ( A x. B ) # 0 ) -> ( A # 0 /\ B # 0 ) )
Theorem	msqge0 8944	A square is nonnegative. Lemma 2.35 of [Geuvers], p. 9. (Contributed by NM, 23-May-2007.) (Revised by Mario Carneiro, 27-May-2016.)
|- ( A e. RR -> 0 <_ ( A x. A ) )
Theorem	msqge0i 8945	A square is nonnegative. (Contributed by NM, 14-May-1999.) (Proof shortened by Andrew Salmon, 19-Nov-2011.)
|- A e. RR   =>    |- 0 <_ ( A x. A )
Theorem	msqge0d 8946	A square is nonnegative. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. RR )   =>    |- ( ph -> 0 <_ ( A x. A ) )
Theorem	mulge0 8947	The product of two nonnegative numbers is nonnegative. (Contributed by NM, 8-Oct-1999.) (Revised by Mario Carneiro, 27-May-2016.)
|- ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 <_ B ) ) -> 0 <_ ( A x. B ) )
Theorem	mulge0i 8948	The product of two nonnegative numbers is nonnegative. (Contributed by NM, 30-Jul-1999.)
|- A e. RR   &    |- B e. RR   =>    |- ( ( 0 <_ A /\ 0 <_ B ) -> 0 <_ ( A x. B ) )
Theorem	mulge0d 8949	The product of two 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 x. B ) )
Theorem	apti 8950	Complex apartness is tight. (Contributed by Jim Kingdon, 21-Feb-2020.)
|- ( ( A e. CC /\ B e. CC ) -> ( A = B <-> -. A # B ) )
Theorem	apne 8951	Apartness implies negated equality. We cannot in general prove the converse (as shown at neapmkv 17118), which is the whole point of having separate notations for apartness and negated equality. (Contributed by Jim Kingdon, 21-Feb-2020.)
|- ( ( A e. CC /\ B e. CC ) -> ( A # B -> A =/= B ) )
Theorem	apcon4bid 8952	Contrapositive law deduction for apartness. (Contributed by Jim Kingdon, 31-Jul-2023.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> C e. CC )   &    |- ( ph -> D e. CC )   &    |- ( ph -> ( A # B <-> C # D ) )   =>    |- ( ph -> ( A = B <-> C = D ) )
Theorem	leltap 8953	<_ implies 'less than' is 'apart'. (Contributed by Jim Kingdon, 13-Aug-2021.)
|- ( ( A e. RR /\ B e. RR /\ A <_ B ) -> ( A < B <-> B # A ) )
Theorem	gt0ap0 8954	Positive implies apart from zero. (Contributed by Jim Kingdon, 27-Feb-2020.)
|- ( ( A e. RR /\ 0 < A ) -> A # 0 )
Theorem	gt0ap0i 8955	Positive means apart from zero (useful for ordering theorems involving division). (Contributed by Jim Kingdon, 27-Feb-2020.)
|- A e. RR   =>    |- ( 0 < A -> A # 0 )
Theorem	gt0ap0ii 8956	Positive implies apart from zero. (Contributed by Jim Kingdon, 27-Feb-2020.)
|- A e. RR   &    |- 0 < A   =>    |- A # 0
Theorem	gt0ap0d 8957	Positive implies apart from zero. Because of the way we define #, A must be an element of RR, not just RR*. (Contributed by Jim Kingdon, 27-Feb-2020.)
|- ( ph -> A e. RR )   &    |- ( ph -> 0 < A )   =>    |- ( ph -> A # 0 )
Theorem	negap0 8958	A number is apart from zero iff its negative is apart from zero. (Contributed by Jim Kingdon, 27-Feb-2020.)
|- ( A e. CC -> ( A # 0 <-> -u A # 0 ) )
Theorem	negap0d 8959	The negative of a number apart from zero is apart from zero. (Contributed by Jim Kingdon, 25-Feb-2024.)
|- ( ph -> A e. CC )   &    |- ( ph -> A # 0 )   =>    |- ( ph -> -u A # 0 )
Theorem	ltleap 8960	Less than in terms of non-strict order and apartness. (Contributed by Jim Kingdon, 28-Feb-2020.)
|- ( ( A e. RR /\ B e. RR ) -> ( A < B <-> ( A <_ B /\ A # B ) ) )
Theorem	ltap 8961	'Less than' implies apart. (Contributed by Jim Kingdon, 12-Aug-2021.)
|- ( ( A e. RR /\ B e. RR /\ A < B ) -> B # A )
Theorem	gtapii 8962	'Greater than' implies apart. (Contributed by Jim Kingdon, 12-Aug-2021.)
|- A e. RR   &    |- B e. RR   &    |- A < B   =>    |- B # A
Theorem	ltapii 8963	'Less than' implies apart. (Contributed by Jim Kingdon, 12-Aug-2021.)
|- A e. RR   &    |- B e. RR   &    |- A < B   =>    |- A # B
Theorem	ltapi 8964	'Less than' implies apart. (Contributed by Jim Kingdon, 12-Aug-2021.)
|- A e. RR   &    |- B e. RR   =>    |- ( A < B -> B # A )
Theorem	gtapd 8965	'Greater than' implies apart. (Contributed by Jim Kingdon, 12-Aug-2021.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> A < B )   =>    |- ( ph -> B # A )
Theorem	ltapd 8966	'Less than' implies apart. (Contributed by Jim Kingdon, 12-Aug-2021.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> A < B )   =>    |- ( ph -> A # B )
Theorem	leltapd 8967	<_ implies 'less than' is 'apart'. (Contributed by Jim Kingdon, 13-Aug-2021.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> A <_ B )   =>    |- ( ph -> ( A < B <-> B # A ) )
Theorem	ap0gt0 8968	A nonnegative number is apart from zero if and only if it is positive. (Contributed by Jim Kingdon, 11-Aug-2021.)
|- ( ( A e. RR /\ 0 <_ A ) -> ( A # 0 <-> 0 < A ) )
Theorem	ap0gt0d 8969	A nonzero nonnegative number is positive. (Contributed by Jim Kingdon, 11-Aug-2021.)
|- ( ph -> A e. RR )   &    |- ( ph -> 0 <_ A )   &    |- ( ph -> A # 0 )   =>    |- ( ph -> 0 < A )
Theorem	apsub1 8970	Subtraction respects apartness. Analogue of subcan2 8551 for apartness. (Contributed by Jim Kingdon, 6-Jan-2022.)
|- ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( A # B <-> ( A - C ) # ( B - C ) ) )
Theorem	subap0 8971	Two numbers being apart is equivalent to their difference being apart from zero. (Contributed by Jim Kingdon, 25-Dec-2022.)
|- ( ( A e. CC /\ B e. CC ) -> ( ( A - B ) # 0 <-> A # B ) )
Theorem	subap0d 8972	Two numbers apart from each other have difference apart from zero. (Contributed by Jim Kingdon, 12-Aug-2021.) (Proof shortened by BJ, 15-Aug-2024.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> A # B )   =>    |- ( ph -> ( A - B ) # 0 )
Theorem	cnstab 8973	Equality of complex numbers is stable. Stability here means -. -. A = B -> A = B as defined at df-stab 843. This theorem for real numbers is Proposition 5.2 of [BauerHanson], p. 27. (Contributed by Jim Kingdon, 1-Aug-2023.) (Proof shortened by BJ, 15-Aug-2024.)
|- ( ( A e. CC /\ B e. CC ) -> STAB A = B )
Theorem	aprcl 8974	Reverse closure for apartness. (Contributed by Jim Kingdon, 19-Dec-2023.)
|- ( A # B -> ( A e. CC /\ B e. CC ) )
Theorem	apsscn 8975*	The points apart from a given point are complex numbers. (Contributed by Jim Kingdon, 19-Dec-2023.)
|- { x e. A | x # B } C_ CC
Theorem	lt0ap0 8976	A number which is less than zero is apart from zero. (Contributed by Jim Kingdon, 25-Feb-2024.)
|- ( ( A e. RR /\ A < 0 ) -> A # 0 )
Theorem	lt0ap0d 8977	A real number less than zero is apart from zero. Deduction form. (Contributed by Jim Kingdon, 24-Feb-2024.)
|- ( ph -> A e. RR )   &    |- ( ph -> A < 0 )   =>    |- ( ph -> A # 0 )
Theorem	aptap 8978	Complex apartness (as defined at df-ap 8910) is a tight apartness (as defined at df-tap 7615). (Contributed by Jim Kingdon, 16-Feb-2025.)
|- # TAp CC
4.3.7  Reciprocals
Theorem	recextlem1 8979	Lemma for recexap 8981. (Contributed by Eric Schmidt, 23-May-2007.)
|- ( ( A e. CC /\ B e. CC ) -> ( ( A + ( _i x. B ) ) x. ( A - ( _i x. B ) ) ) = ( ( A x. A ) + ( B x. B ) ) )
Theorem	recexaplem2 8980	Lemma for recexap 8981. (Contributed by Jim Kingdon, 20-Feb-2020.)
|- ( ( A e. RR /\ B e. RR /\ ( A + ( _i x. B ) ) # 0 ) -> ( ( A x. A ) + ( B x. B ) ) # 0 )
Theorem	recexap 8981*	Existence of reciprocal of nonzero complex number. (Contributed by Jim Kingdon, 20-Feb-2020.)
|- ( ( A e. CC /\ A # 0 ) -> E. x e. CC ( A x. x ) = 1 )
Theorem	mulap0 8982	The product of two numbers apart from zero is apart from zero. Lemma 2.15 of [Geuvers], p. 6. (Contributed by Jim Kingdon, 22-Feb-2020.)
|- ( ( ( A e. CC /\ A # 0 ) /\ ( B e. CC /\ B # 0 ) ) -> ( A x. B ) # 0 )
Theorem	mulap0b 8983	The product of two numbers apart from zero is apart from zero. (Contributed by Jim Kingdon, 24-Feb-2020.)
|- ( ( A e. CC /\ B e. CC ) -> ( ( A # 0 /\ B # 0 ) <-> ( A x. B ) # 0 ) )
Theorem	mulap0i 8984	The product of two numbers apart from zero is apart from zero. (Contributed by Jim Kingdon, 23-Feb-2020.)
|- A e. CC   &    |- B e. CC   &    |- A # 0   &    |- B # 0   =>    |- ( A x. B ) # 0
Theorem	mulap0bd 8985	The product of two numbers apart from zero is apart from zero. Exercise 11.11 of [HoTT], p. (varies). (Contributed by Jim Kingdon, 24-Feb-2020.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   =>    |- ( ph -> ( ( A # 0 /\ B # 0 ) <-> ( A x. B ) # 0 ) )
Theorem	mulap0d 8986	The product of two numbers apart from zero is apart from zero. (Contributed by Jim Kingdon, 23-Feb-2020.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> A # 0 )   &    |- ( ph -> B # 0 )   =>    |- ( ph -> ( A x. B ) # 0 )
Theorem	mulap0bad 8987	A factor of a complex number apart from zero is apart from zero. Partial converse of mulap0d 8986 and consequence of mulap0bd 8985. (Contributed by Jim Kingdon, 24-Feb-2020.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> ( A x. B ) # 0 )   =>    |- ( ph -> A # 0 )
Theorem	mulap0bbd 8988	A factor of a complex number apart from zero is apart from zero. Partial converse of mulap0d 8986 and consequence of mulap0bd 8985. (Contributed by Jim Kingdon, 24-Feb-2020.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> ( A x. B ) # 0 )   =>    |- ( ph -> B # 0 )
Theorem	mulcanapd 8989	Cancellation law for multiplication. (Contributed by Jim Kingdon, 21-Feb-2020.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> C e. CC )   &    |- ( ph -> C # 0 )   =>    |- ( ph -> ( ( C x. A ) = ( C x. B ) <-> A = B ) )
Theorem	mulcanap2d 8990	Cancellation law for multiplication. (Contributed by Jim Kingdon, 21-Feb-2020.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> C e. CC )   &    |- ( ph -> C # 0 )   =>    |- ( ph -> ( ( A x. C ) = ( B x. C ) <-> A = B ) )
Theorem	mulcanapad 8991	Cancellation of a nonzero factor on the left in an equation. One-way deduction form of mulcanapd 8989. (Contributed by Jim Kingdon, 21-Feb-2020.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> C e. CC )   &    |- ( ph -> C # 0 )   &    |- ( ph -> ( C x. A ) = ( C x. B ) )   =>    |- ( ph -> A = B )
Theorem	mulcanap2ad 8992	Cancellation of a nonzero factor on the right in an equation. One-way deduction form of mulcanap2d 8990. (Contributed by Jim Kingdon, 21-Feb-2020.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> C e. CC )   &    |- ( ph -> C # 0 )   &    |- ( ph -> ( A x. C ) = ( B x. C ) )   =>    |- ( ph -> A = B )
Theorem	mulcanap 8993	Cancellation law for multiplication (full theorem form). (Contributed by Jim Kingdon, 21-Feb-2020.)
|- ( ( A e. CC /\ B e. CC /\ ( C e. CC /\ C # 0 ) ) -> ( ( C x. A ) = ( C x. B ) <-> A = B ) )
Theorem	mulcanap2 8994	Cancellation law for multiplication. (Contributed by Jim Kingdon, 21-Feb-2020.)
|- ( ( A e. CC /\ B e. CC /\ ( C e. CC /\ C # 0 ) ) -> ( ( A x. C ) = ( B x. C ) <-> A = B ) )
Theorem	mulcanapi 8995	Cancellation law for multiplication. (Contributed by Jim Kingdon, 21-Feb-2020.)
|- A e. CC   &    |- B e. CC   &    |- C e. CC   &    |- C # 0   =>    |- ( ( C x. A ) = ( C x. B ) <-> A = B )
Theorem	msqap0 8996	A number is apart from zero iff its square is apart from zero. (Contributed by Matthew House, 28-Jun-2026.)
|- ( A e. CC -> ( ( A x. A ) # 0 <-> A # 0 ) )
Theorem	msq0 8997	A number is zero iff its square is zero. (Contributed by Matthew House, 28-Jun-2026.)
|- ( A e. CC -> ( ( A x. A ) = 0 <-> A = 0 ) )
Theorem	muleqadd 8998	Property of numbers whose product equals their sum. Equation 5 of [Kreyszig] p. 12. (Contributed by NM, 13-Nov-2006.)
|- ( ( A e. CC /\ B e. CC ) -> ( ( A x. B ) = ( A + B ) <-> ( ( A - 1 ) x. ( B - 1 ) ) = 1 ) )
Theorem	receuap 8999*	Existential uniqueness of reciprocals. (Contributed by Jim Kingdon, 21-Feb-2020.)
|- ( ( A e. CC /\ B e. CC /\ B # 0 ) -> E! x e. CC ( B x. x ) = A )
Theorem	mul0eqap 9000	If two numbers are apart from each other and their product is zero, one of them must be zero. (Contributed by Jim Kingdon, 31-Jul-2023.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> A # B )   &    |- ( ph -> ( A x. B ) = 0 )   =>    |- ( ph -> ( A = 0 \/ B = 0 ) )