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	subap0 8801	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 8802	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 8803	Equality of complex numbers is stable. Stability here means -. -. A = B -> A = B as defined at df-stab 836. 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 8804	Reverse closure for apartness. (Contributed by Jim Kingdon, 19-Dec-2023.)
|- ( A # B -> ( A e. CC /\ B e. CC ) )
Theorem	apsscn 8805*	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 8806	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 8807	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 8808	Complex apartness (as defined at df-ap 8740) is a tight apartness (as defined at df-tap 7447). (Contributed by Jim Kingdon, 16-Feb-2025.)
|- # TAp CC
4.3.7  Reciprocals
Theorem	recextlem1 8809	Lemma for recexap 8811. (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 8810	Lemma for recexap 8811. (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 8811*	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 8812	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 8813	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 8814	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 8815	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 8816	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 8817	A factor of a complex number apart from zero is apart from zero. Partial converse of mulap0d 8816 and consequence of mulap0bd 8815. (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 8818	A factor of a complex number apart from zero is apart from zero. Partial converse of mulap0d 8816 and consequence of mulap0bd 8815. (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 8819	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 8820	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 8821	Cancellation of a nonzero factor on the left in an equation. One-way deduction form of mulcanapd 8819. (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 8822	Cancellation of a nonzero factor on the right in an equation. One-way deduction form of mulcanap2d 8820. (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 8823	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 8824	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 8825	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	muleqadd 8826	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 8827*	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 8828	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 ) )
Theorem	recapb 8829*	A complex number has a multiplicative inverse if and only if it is apart from zero. Theorem 11.2.4 of [HoTT], p. (varies), generalized from real to complex numbers. (Contributed by Jim Kingdon, 18-Jan-2025.)
|- ( A e. CC -> ( A # 0 <-> E. x e. CC ( A x. x ) = 1 ) )
4.3.8  Division
Syntax	cdiv 8830	Extend class notation to include division.
class /
Definition	df-div 8831*	Define division. Theorem divmulap 8833 relates it to multiplication, and divclap 8836 and redivclap 8889 prove its closure laws. (Contributed by NM, 2-Feb-1995.) Use divvalap 8832 instead. (Revised by Mario Carneiro, 1-Apr-2014.) (New usage is discouraged.)
|- / = ( x e. CC , y e. ( CC \ { 0 } ) |-> ( iota_ z e. CC ( y x. z ) = x ) )
Theorem	divvalap 8832*	Value of division: the (unique) element x such that ( B x. x ) = A. This is meaningful only when B is apart from zero. (Contributed by Jim Kingdon, 21-Feb-2020.)
|- ( ( A e. CC /\ B e. CC /\ B # 0 ) -> ( A / B ) = ( iota_ x e. CC ( B x. x ) = A ) )
Theorem	divmulap 8833	Relationship between division and multiplication. (Contributed by Jim Kingdon, 22-Feb-2020.)
|- ( ( A e. CC /\ B e. CC /\ ( C e. CC /\ C # 0 ) ) -> ( ( A / C ) = B <-> ( C x. B ) = A ) )
Theorem	divmulap2 8834	Relationship between division and multiplication. (Contributed by Jim Kingdon, 22-Feb-2020.)
|- ( ( A e. CC /\ B e. CC /\ ( C e. CC /\ C # 0 ) ) -> ( ( A / C ) = B <-> A = ( C x. B ) ) )
Theorem	divmulap3 8835	Relationship between division and multiplication. (Contributed by Jim Kingdon, 22-Feb-2020.)
|- ( ( A e. CC /\ B e. CC /\ ( C e. CC /\ C # 0 ) ) -> ( ( A / C ) = B <-> A = ( B x. C ) ) )
Theorem	divclap 8836	Closure law for division. (Contributed by Jim Kingdon, 22-Feb-2020.)
|- ( ( A e. CC /\ B e. CC /\ B # 0 ) -> ( A / B ) e. CC )
Theorem	recclap 8837	Closure law for reciprocal. (Contributed by Jim Kingdon, 22-Feb-2020.)
|- ( ( A e. CC /\ A # 0 ) -> ( 1 / A ) e. CC )
Theorem	divcanap2 8838	A cancellation law for division. (Contributed by Jim Kingdon, 22-Feb-2020.)
|- ( ( A e. CC /\ B e. CC /\ B # 0 ) -> ( B x. ( A / B ) ) = A )
Theorem	divcanap1 8839	A cancellation law for division. (Contributed by Jim Kingdon, 22-Feb-2020.)
|- ( ( A e. CC /\ B e. CC /\ B # 0 ) -> ( ( A / B ) x. B ) = A )
Theorem	diveqap0 8840	A ratio is zero iff the numerator is zero. (Contributed by Jim Kingdon, 22-Feb-2020.)
|- ( ( A e. CC /\ B e. CC /\ B # 0 ) -> ( ( A / B ) = 0 <-> A = 0 ) )
Theorem	divap0b 8841	The ratio of numbers apart from zero is apart from zero. (Contributed by Jim Kingdon, 22-Feb-2020.)
|- ( ( A e. CC /\ B e. CC /\ B # 0 ) -> ( A # 0 <-> ( A / B ) # 0 ) )
Theorem	divap0 8842	The ratio of numbers apart from zero is apart from zero. (Contributed by Jim Kingdon, 22-Feb-2020.)
|- ( ( ( A e. CC /\ A # 0 ) /\ ( B e. CC /\ B # 0 ) ) -> ( A / B ) # 0 )
Theorem	recap0 8843	The reciprocal of a number apart from zero is apart from zero. (Contributed by Jim Kingdon, 24-Feb-2020.)
|- ( ( A e. CC /\ A # 0 ) -> ( 1 / A ) # 0 )
Theorem	recidap 8844	Multiplication of a number and its reciprocal. (Contributed by Jim Kingdon, 24-Feb-2020.)
|- ( ( A e. CC /\ A # 0 ) -> ( A x. ( 1 / A ) ) = 1 )
Theorem	recidap2 8845	Multiplication of a number and its reciprocal. (Contributed by Jim Kingdon, 24-Feb-2020.)
|- ( ( A e. CC /\ A # 0 ) -> ( ( 1 / A ) x. A ) = 1 )
Theorem	divrecap 8846	Relationship between division and reciprocal. (Contributed by Jim Kingdon, 24-Feb-2020.)
|- ( ( A e. CC /\ B e. CC /\ B # 0 ) -> ( A / B ) = ( A x. ( 1 / B ) ) )
Theorem	divrecap2 8847	Relationship between division and reciprocal. (Contributed by Jim Kingdon, 25-Feb-2020.)
|- ( ( A e. CC /\ B e. CC /\ B # 0 ) -> ( A / B ) = ( ( 1 / B ) x. A ) )
Theorem	divassap 8848	An associative law for division. (Contributed by Jim Kingdon, 25-Feb-2020.)
|- ( ( A e. CC /\ B e. CC /\ ( C e. CC /\ C # 0 ) ) -> ( ( A x. B ) / C ) = ( A x. ( B / C ) ) )
Theorem	div23ap 8849	A commutative/associative law for division. (Contributed by Jim Kingdon, 25-Feb-2020.)
|- ( ( A e. CC /\ B e. CC /\ ( C e. CC /\ C # 0 ) ) -> ( ( A x. B ) / C ) = ( ( A / C ) x. B ) )
Theorem	div32ap 8850	A commutative/associative law for division. (Contributed by Jim Kingdon, 25-Feb-2020.)
|- ( ( A e. CC /\ ( B e. CC /\ B # 0 ) /\ C e. CC ) -> ( ( A / B ) x. C ) = ( A x. ( C / B ) ) )
Theorem	div13ap 8851	A commutative/associative law for division. (Contributed by Jim Kingdon, 25-Feb-2020.)
|- ( ( A e. CC /\ ( B e. CC /\ B # 0 ) /\ C e. CC ) -> ( ( A / B ) x. C ) = ( ( C / B ) x. A ) )
Theorem	div12ap 8852	A commutative/associative law for division. (Contributed by Jim Kingdon, 25-Feb-2020.)
|- ( ( A e. CC /\ B e. CC /\ ( C e. CC /\ C # 0 ) ) -> ( A x. ( B / C ) ) = ( B x. ( A / C ) ) )
Theorem	divmulassap 8853	An associative law for division and multiplication. (Contributed by Jim Kingdon, 24-Jan-2022.)
|- ( ( ( A e. CC /\ B e. CC /\ C e. CC ) /\ ( D e. CC /\ D # 0 ) ) -> ( ( A x. ( B / D ) ) x. C ) = ( ( A x. B ) x. ( C / D ) ) )
Theorem	divmulasscomap 8854	An associative/commutative law for division and multiplication. (Contributed by Jim Kingdon, 24-Jan-2022.)
|- ( ( ( A e. CC /\ B e. CC /\ C e. CC ) /\ ( D e. CC /\ D # 0 ) ) -> ( ( A x. ( B / D ) ) x. C ) = ( B x. ( ( A x. C ) / D ) ) )
Theorem	divdirap 8855	Distribution of division over addition. (Contributed by Jim Kingdon, 25-Feb-2020.)
|- ( ( A e. CC /\ B e. CC /\ ( C e. CC /\ C # 0 ) ) -> ( ( A + B ) / C ) = ( ( A / C ) + ( B / C ) ) )
Theorem	divcanap3 8856	A cancellation law for division. (Contributed by Jim Kingdon, 25-Feb-2020.)
|- ( ( A e. CC /\ B e. CC /\ B # 0 ) -> ( ( B x. A ) / B ) = A )
Theorem	divcanap4 8857	A cancellation law for division. (Contributed by Jim Kingdon, 25-Feb-2020.)
|- ( ( A e. CC /\ B e. CC /\ B # 0 ) -> ( ( A x. B ) / B ) = A )
Theorem	div11ap 8858	One-to-one relationship for division. (Contributed by Jim Kingdon, 25-Feb-2020.)
|- ( ( A e. CC /\ B e. CC /\ ( C e. CC /\ C # 0 ) ) -> ( ( A / C ) = ( B / C ) <-> A = B ) )
Theorem	dividap 8859	A number divided by itself is one. (Contributed by Jim Kingdon, 25-Feb-2020.)
|- ( ( A e. CC /\ A # 0 ) -> ( A / A ) = 1 )
Theorem	div0ap 8860	Division into zero is zero. (Contributed by Jim Kingdon, 25-Feb-2020.)
|- ( ( A e. CC /\ A # 0 ) -> ( 0 / A ) = 0 )
Theorem	div1 8861	A number divided by 1 is itself. (Contributed by NM, 9-Jan-2002.) (Proof shortened by Mario Carneiro, 27-May-2016.)
|- ( A e. CC -> ( A / 1 ) = A )
Theorem	1div1e1 8862	1 divided by 1 is 1 (common case). (Contributed by David A. Wheeler, 7-Dec-2018.)
|- ( 1 / 1 ) = 1
Theorem	diveqap1 8863	Equality in terms of unit ratio. (Contributed by Jim Kingdon, 25-Feb-2020.)
|- ( ( A e. CC /\ B e. CC /\ B # 0 ) -> ( ( A / B ) = 1 <-> A = B ) )
Theorem	divnegap 8864	Move negative sign inside of a division. (Contributed by Jim Kingdon, 25-Feb-2020.)
|- ( ( A e. CC /\ B e. CC /\ B # 0 ) -> -u ( A / B ) = ( -u A / B ) )
Theorem	muldivdirap 8865	Distribution of division over addition with a multiplication. (Contributed by Jim Kingdon, 11-Nov-2021.)
|- ( ( A e. CC /\ B e. CC /\ ( C e. CC /\ C # 0 ) ) -> ( ( ( C x. A ) + B ) / C ) = ( A + ( B / C ) ) )
Theorem	divsubdirap 8866	Distribution of division over subtraction. (Contributed by NM, 4-Mar-2005.)
|- ( ( A e. CC /\ B e. CC /\ ( C e. CC /\ C # 0 ) ) -> ( ( A - B ) / C ) = ( ( A / C ) - ( B / C ) ) )
Theorem	recrecap 8867	A number is equal to the reciprocal of its reciprocal. (Contributed by Jim Kingdon, 25-Feb-2020.)
|- ( ( A e. CC /\ A # 0 ) -> ( 1 / ( 1 / A ) ) = A )
Theorem	rec11ap 8868	Reciprocal is one-to-one. (Contributed by Jim Kingdon, 25-Feb-2020.)
|- ( ( ( A e. CC /\ A # 0 ) /\ ( B e. CC /\ B # 0 ) ) -> ( ( 1 / A ) = ( 1 / B ) <-> A = B ) )
Theorem	rec11rap 8869	Mutual reciprocals. (Contributed by Jim Kingdon, 25-Feb-2020.)
|- ( ( ( A e. CC /\ A # 0 ) /\ ( B e. CC /\ B # 0 ) ) -> ( ( 1 / A ) = B <-> ( 1 / B ) = A ) )
Theorem	divmuldivap 8870	Multiplication of two ratios. (Contributed by Jim Kingdon, 25-Feb-2020.)
|- ( ( ( A e. CC /\ B e. CC ) /\ ( ( C e. CC /\ C # 0 ) /\ ( D e. CC /\ D # 0 ) ) ) -> ( ( A / C ) x. ( B / D ) ) = ( ( A x. B ) / ( C x. D ) ) )
Theorem	divdivdivap 8871	Division of two ratios. Theorem I.15 of [Apostol] p. 18. (Contributed by Jim Kingdon, 25-Feb-2020.)
|- ( ( ( A e. CC /\ ( B e. CC /\ B # 0 ) ) /\ ( ( C e. CC /\ C # 0 ) /\ ( D e. CC /\ D # 0 ) ) ) -> ( ( A / B ) / ( C / D ) ) = ( ( A x. D ) / ( B x. C ) ) )
Theorem	divcanap5 8872	Cancellation of common factor in a ratio. (Contributed by Jim Kingdon, 25-Feb-2020.)
|- ( ( A e. CC /\ ( B e. CC /\ B # 0 ) /\ ( C e. CC /\ C # 0 ) ) -> ( ( C x. A ) / ( C x. B ) ) = ( A / B ) )
Theorem	divmul13ap 8873	Swap the denominators in the product of two ratios. (Contributed by Jim Kingdon, 26-Feb-2020.)
|- ( ( ( A e. CC /\ B e. CC ) /\ ( ( C e. CC /\ C # 0 ) /\ ( D e. CC /\ D # 0 ) ) ) -> ( ( A / C ) x. ( B / D ) ) = ( ( B / C ) x. ( A / D ) ) )
Theorem	divmul24ap 8874	Swap the numerators in the product of two ratios. (Contributed by Jim Kingdon, 26-Feb-2020.)
|- ( ( ( A e. CC /\ B e. CC ) /\ ( ( C e. CC /\ C # 0 ) /\ ( D e. CC /\ D # 0 ) ) ) -> ( ( A / C ) x. ( B / D ) ) = ( ( A / D ) x. ( B / C ) ) )
Theorem	divmuleqap 8875	Cross-multiply in an equality of ratios. (Contributed by Jim Kingdon, 26-Feb-2020.)
|- ( ( ( A e. CC /\ B e. CC ) /\ ( ( C e. CC /\ C # 0 ) /\ ( D e. CC /\ D # 0 ) ) ) -> ( ( A / C ) = ( B / D ) <-> ( A x. D ) = ( B x. C ) ) )
Theorem	recdivap 8876	The reciprocal of a ratio. (Contributed by Jim Kingdon, 26-Feb-2020.)
|- ( ( ( A e. CC /\ A # 0 ) /\ ( B e. CC /\ B # 0 ) ) -> ( 1 / ( A / B ) ) = ( B / A ) )
Theorem	divcanap6 8877	Cancellation of inverted fractions. (Contributed by Jim Kingdon, 26-Feb-2020.)
|- ( ( ( A e. CC /\ A # 0 ) /\ ( B e. CC /\ B # 0 ) ) -> ( ( A / B ) x. ( B / A ) ) = 1 )
Theorem	divdiv32ap 8878	Swap denominators in a division. (Contributed by Jim Kingdon, 26-Feb-2020.)
|- ( ( A e. CC /\ ( B e. CC /\ B # 0 ) /\ ( C e. CC /\ C # 0 ) ) -> ( ( A / B ) / C ) = ( ( A / C ) / B ) )
Theorem	divcanap7 8879	Cancel equal divisors in a division. (Contributed by Jim Kingdon, 26-Feb-2020.)
|- ( ( A e. CC /\ ( B e. CC /\ B # 0 ) /\ ( C e. CC /\ C # 0 ) ) -> ( ( A / C ) / ( B / C ) ) = ( A / B ) )
Theorem	dmdcanap 8880	Cancellation law for division and multiplication. (Contributed by Jim Kingdon, 26-Feb-2020.)
|- ( ( ( A e. CC /\ A # 0 ) /\ ( B e. CC /\ B # 0 ) /\ C e. CC ) -> ( ( A / B ) x. ( C / A ) ) = ( C / B ) )
Theorem	divdivap1 8881	Division into a fraction. (Contributed by Jim Kingdon, 26-Feb-2020.)
|- ( ( A e. CC /\ ( B e. CC /\ B # 0 ) /\ ( C e. CC /\ C # 0 ) ) -> ( ( A / B ) / C ) = ( A / ( B x. C ) ) )
Theorem	divdivap2 8882	Division by a fraction. (Contributed by Jim Kingdon, 26-Feb-2020.)
|- ( ( A e. CC /\ ( B e. CC /\ B # 0 ) /\ ( C e. CC /\ C # 0 ) ) -> ( A / ( B / C ) ) = ( ( A x. C ) / B ) )
Theorem	recdivap2 8883	Division into a reciprocal. (Contributed by Jim Kingdon, 26-Feb-2020.)
|- ( ( ( A e. CC /\ A # 0 ) /\ ( B e. CC /\ B # 0 ) ) -> ( ( 1 / A ) / B ) = ( 1 / ( A x. B ) ) )
Theorem	ddcanap 8884	Cancellation in a double division. (Contributed by Jim Kingdon, 26-Feb-2020.)
|- ( ( ( A e. CC /\ A # 0 ) /\ ( B e. CC /\ B # 0 ) ) -> ( A / ( A / B ) ) = B )
Theorem	divadddivap 8885	Addition of two ratios. (Contributed by Jim Kingdon, 26-Feb-2020.)
|- ( ( ( A e. CC /\ B e. CC ) /\ ( ( C e. CC /\ C # 0 ) /\ ( D e. CC /\ D # 0 ) ) ) -> ( ( A / C ) + ( B / D ) ) = ( ( ( A x. D ) + ( B x. C ) ) / ( C x. D ) ) )
Theorem	divsubdivap 8886	Subtraction of two ratios. (Contributed by Jim Kingdon, 26-Feb-2020.)
|- ( ( ( A e. CC /\ B e. CC ) /\ ( ( C e. CC /\ C # 0 ) /\ ( D e. CC /\ D # 0 ) ) ) -> ( ( A / C ) - ( B / D ) ) = ( ( ( A x. D ) - ( B x. C ) ) / ( C x. D ) ) )
Theorem	conjmulap 8887	Two numbers whose reciprocals sum to 1 are called "conjugates" and satisfy this relationship. (Contributed by Jim Kingdon, 26-Feb-2020.)
|- ( ( ( P e. CC /\ P # 0 ) /\ ( Q e. CC /\ Q # 0 ) ) -> ( ( ( 1 / P ) + ( 1 / Q ) ) = 1 <-> ( ( P - 1 ) x. ( Q - 1 ) ) = 1 ) )
Theorem	rerecclap 8888	Closure law for reciprocal. (Contributed by Jim Kingdon, 26-Feb-2020.)
|- ( ( A e. RR /\ A # 0 ) -> ( 1 / A ) e. RR )
Theorem	redivclap 8889	Closure law for division of reals. (Contributed by Jim Kingdon, 26-Feb-2020.)
|- ( ( A e. RR /\ B e. RR /\ B # 0 ) -> ( A / B ) e. RR )
Theorem	eqneg 8890	A number equal to its negative is zero. (Contributed by NM, 12-Jul-2005.) (Revised by Mario Carneiro, 27-May-2016.)
|- ( A e. CC -> ( A = -u A <-> A = 0 ) )
Theorem	eqnegd 8891	A complex number equals its negative iff it is zero. Deduction form of eqneg 8890. (Contributed by David Moews, 28-Feb-2017.)
|- ( ph -> A e. CC )   =>    |- ( ph -> ( A = -u A <-> A = 0 ) )
Theorem	eqnegad 8892	If a complex number equals its own negative, it is zero. One-way deduction form of eqneg 8890. (Contributed by David Moews, 28-Feb-2017.)
|- ( ph -> A e. CC )   &    |- ( ph -> A = -u A )   =>    |- ( ph -> A = 0 )
Theorem	div2negap 8893	Quotient of two negatives. (Contributed by Jim Kingdon, 27-Feb-2020.)
|- ( ( A e. CC /\ B e. CC /\ B # 0 ) -> ( -u A / -u B ) = ( A / B ) )
Theorem	divneg2ap 8894	Move negative sign inside of a division. (Contributed by Jim Kingdon, 27-Feb-2020.)
|- ( ( A e. CC /\ B e. CC /\ B # 0 ) -> -u ( A / B ) = ( A / -u B ) )
Theorem	recclapzi 8895	Closure law for reciprocal. (Contributed by Jim Kingdon, 27-Feb-2020.)
|- A e. CC   =>    |- ( A # 0 -> ( 1 / A ) e. CC )
Theorem	recap0apzi 8896	The reciprocal of a number apart from zero is apart from zero. (Contributed by Jim Kingdon, 27-Feb-2020.)
|- A e. CC   =>    |- ( A # 0 -> ( 1 / A ) # 0 )
Theorem	recidapzi 8897	Multiplication of a number and its reciprocal. (Contributed by Jim Kingdon, 27-Feb-2020.)
|- A e. CC   =>    |- ( A # 0 -> ( A x. ( 1 / A ) ) = 1 )
Theorem	div1i 8898	A number divided by 1 is itself. (Contributed by NM, 9-Jan-2002.)
|- A e. CC   =>    |- ( A / 1 ) = A
Theorem	eqnegi 8899	A number equal to its negative is zero. (Contributed by NM, 29-May-1999.)
|- A e. CC   =>    |- ( A = -u A <-> A = 0 )
Theorem	recclapi 8900	Closure law for reciprocal. (Contributed by NM, 30-Apr-2005.)
|- A e. CC   &    |- A # 0   =>    |- ( 1 / A ) e. CC