P. 97 of Theorem List - Metamath Proof Explorer

Mirrors  >  Metamath Home Page  >  MPE Home Page  >  Theorem List Contents  >  Recent Proofs       This page: Page List

Theorem List for Metamath Proof Explorer - 9601-9700   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	le2subd 9601	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 9602	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 9603	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 9604	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 9605	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	1le1 9606	1 <_ 1. Common special case. (Contributed by David A. Wheeler, 16-Jul-2016.)
|- 1 <_ 1
5.3.5  Reciprocals
Theorem	ixi 9607	_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	recextlem1 9608	Lemma for recex 9610. (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	recextlem2 9609	Lemma for recex 9610. (Contributed by Eric Schmidt, 23-May-2007.)
|- ( ( A e. RR /\ B e. RR /\ ( A + ( _i x. B ) ) =/= 0 ) -> ( ( A x. A ) + ( B x. B ) ) =/= 0 )
Theorem	recex 9610*	Existence of reciprocal of nonzero complex number. (Contributed by Eric Schmidt, 22-May-2007.)
|- ( ( A e. CC /\ A =/= 0 ) -> E. x e. CC ( A x. x ) = 1 )
Theorem	mulcand 9611	Cancellation law for multiplication. Theorem I.7 of [Apostol] p. 18. (Contributed by NM, 26-Jan-1995.) (Revised by Mario Carneiro, 27-May-2016.)
|- ( 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	mulcan2d 9612	Cancellation law for multiplication. Theorem I.7 of [Apostol] p. 18. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( 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	mulcanad 9613	Cancellation of a nonzero factor on the left in an equation. One-way deduction form of mulcand 9611. (Contributed by David Moews, 28-Feb-2017.)
|- ( 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	mulcan2ad 9614	Cancellation of a nonzero factor on the right in an equation. One-way deduction form of mulcan2d 9612. (Contributed by David Moews, 28-Feb-2017.)
|- ( 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	mulcan 9615	Cancellation law for multiplication (full theorem form). Theorem I.7 of [Apostol] p. 18. (Contributed by NM, 29-Jan-1995.) (Revised by Mario Carneiro, 27-May-2016.)
|- ( ( A e. CC /\ B e. CC /\ ( C e. CC /\ C =/= 0 ) ) -> ( ( C x. A ) = ( C x. B ) <-> A = B ) )
Theorem	mulcan2 9616	Cancellation law for multiplication. (Contributed by NM, 21-Jan-2005.) (Revised by Mario Carneiro, 27-May-2016.)
|- ( ( A e. CC /\ B e. CC /\ ( C e. CC /\ C =/= 0 ) ) -> ( ( A x. C ) = ( B x. C ) <-> A = B ) )
Theorem	mulcani 9617	Cancellation law for multiplication. Theorem I.7 of [Apostol] p. 18. (Contributed by NM, 26-Jan-1995.)
|- A e. CC   &    |- B e. CC   &    |- C e. CC   &    |- C =/= 0   =>    |- ( ( C x. A ) = ( C x. B ) <-> A = B )
Theorem	mul0or 9618	If a product is zero, one of its factors must be zero. Theorem I.11 of [Apostol] p. 18. (Contributed by NM, 9-Oct-1999.) (Revised by Mario Carneiro, 27-May-2016.)
|- ( ( A e. CC /\ B e. CC ) -> ( ( A x. B ) = 0 <-> ( A = 0 \/ B = 0 ) ) )
Theorem	mulne0b 9619	The product of two nonzero numbers is nonzero. (Contributed by NM, 1-Aug-2004.) (Proof shortened by Andrew Salmon, 19-Nov-2011.)
|- ( ( A e. CC /\ B e. CC ) -> ( ( A =/= 0 /\ B =/= 0 ) <-> ( A x. B ) =/= 0 ) )
Theorem	mulne0 9620	The product of two nonzero numbers is nonzero. (Contributed by NM, 30-Dec-2007.)
|- ( ( ( A e. CC /\ A =/= 0 ) /\ ( B e. CC /\ B =/= 0 ) ) -> ( A x. B ) =/= 0 )
Theorem	mulne0i 9621	The product of two nonzero numbers is nonzero. (Contributed by NM, 15-Feb-1995.)
|- A e. CC   &    |- B e. CC   &    |- A =/= 0   &    |- B =/= 0   =>    |- ( A x. B ) =/= 0
Theorem	muleqadd 9622	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	receu 9623*	Existential uniqueness of reciprocals. Theorem I.8 of [Apostol] p. 18. (Contributed by NM, 29-Jan-1995.) (Revised by Mario Carneiro, 17-Feb-2014.)
|- ( ( A e. CC /\ B e. CC /\ B =/= 0 ) -> E! x e. CC ( B x. x ) = A )
Theorem	mulnzcnopr 9624	Multiplication maps nonzero complex numbers to nonzero complex numbers. (Contributed by Steve Rodriguez, 23-Feb-2007.)
|- ( x. |` ( ( CC \ { 0 } ) X. ( CC \ { 0 } ) ) ) : ( ( CC \ { 0 } ) X. ( CC \ { 0 } ) ) --> ( CC \ { 0 } )
Theorem	msq0i 9625	A number is zero iff its square is zero (where square is represented using multiplication). (Contributed by NM, 28-Jul-1999.)
|- A e. CC   =>    |- ( ( A x. A ) = 0 <-> A = 0 )
Theorem	mul0ori 9626	If a product is zero, one of its factors must be zero. Theorem I.11 of [Apostol] p. 18. (Contributed by NM, 7-Oct-1999.)
|- A e. CC   &    |- B e. CC   =>    |- ( ( A x. B ) = 0 <-> ( A = 0 \/ B = 0 ) )
Theorem	msq0d 9627	A number is zero iff its square is zero (where square is represented using multiplication). (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. CC )   =>    |- ( ph -> ( ( A x. A ) = 0 <-> A = 0 ) )
Theorem	mul0ord 9628	If a product is zero, one of its factors must be zero. Theorem I.11 of [Apostol] p. 18. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   =>    |- ( ph -> ( ( A x. B ) = 0 <-> ( A = 0 \/ B = 0 ) ) )
Theorem	mulne0bd 9629	The product of two nonzero numbers is nonzero. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   =>    |- ( ph -> ( ( A =/= 0 /\ B =/= 0 ) <-> ( A x. B ) =/= 0 ) )
Theorem	mulne0d 9630	The product of two nonzero numbers is nonzero. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> A =/= 0 )   &    |- ( ph -> B =/= 0 )   =>    |- ( ph -> ( A x. B ) =/= 0 )
Theorem	mulne0bad 9631	A factor of a nonzero complex number is nonzero. Partial converse of mulne0d 9630 and consequence of mulne0bd 9629. (Contributed by David Moews, 28-Feb-2017.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> ( A x. B ) =/= 0 )   =>    |- ( ph -> A =/= 0 )
Theorem	mulne0bbd 9632	A factor of a nonzero complex number is nonzero. Partial converse of mulne0d 9630 and consequence of mulne0bd 9629. (Contributed by David Moews, 28-Feb-2017.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> ( A x. B ) =/= 0 )   =>    |- ( ph -> B =/= 0 )
5.3.6  Division
Syntax	cdiv 9633	Extend class notation to include division.
class /
Definition	df-div 9634*	Define division. Theorem divmuli 9724 relates it to multiplication, and divcli 9712 and redivcli 9737 prove its closure laws. (Contributed by NM, 2-Feb-1995.) (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	1div0 9635	You can't divide by zero, because division explicitly excludes zero from the domain of the function. Thus, by the definition of function value, it evaluates to the empty set. (This theorem is for information only and normally is not referenced by other proofs. To be meaningful, it assumes that (/) is not a complex number, which depends on the particular complex number construction that is used.) (Contributed by Mario Carneiro, 1-Apr-2014.) (New usage is discouraged.)
|- ( 1 / 0 ) = (/)
Theorem	divval 9636*	Value of division: the (unique) element x such that ( B x. x ) = A. This is meaningful only when B is nonzero. (Contributed by NM, 8-May-1999.) (Revised by Mario Carneiro, 17-Feb-2014.)
|- ( ( A e. CC /\ B e. CC /\ B =/= 0 ) -> ( A / B ) = ( iota_ x e. CC ( B x. x ) = A ) )
Theorem	divmul 9637	Relationship between division and multiplication. (Contributed by NM, 2-Aug-2004.) (Revised by Mario Carneiro, 17-Feb-2014.)
|- ( ( A e. CC /\ B e. CC /\ ( C e. CC /\ C =/= 0 ) ) -> ( ( A / C ) = B <-> ( C x. B ) = A ) )
Theorem	divmul2 9638	Relationship between division and multiplication. (Contributed by NM, 7-Feb-2006.)
|- ( ( A e. CC /\ B e. CC /\ ( C e. CC /\ C =/= 0 ) ) -> ( ( A / C ) = B <-> A = ( C x. B ) ) )
Theorem	divmul3 9639	Relationship between division and multiplication. (Contributed by NM, 13-Feb-2006.)
|- ( ( A e. CC /\ B e. CC /\ ( C e. CC /\ C =/= 0 ) ) -> ( ( A / C ) = B <-> A = ( B x. C ) ) )
Theorem	divcl 9640	Closure law for division. (Contributed by NM, 21-Jul-2001.) (Proof shortened by Mario Carneiro, 17-Feb-2014.)
|- ( ( A e. CC /\ B e. CC /\ B =/= 0 ) -> ( A / B ) e. CC )
Theorem	reccl 9641	Closure law for reciprocal. (Contributed by NM, 30-Apr-2005.)
|- ( ( A e. CC /\ A =/= 0 ) -> ( 1 / A ) e. CC )
Theorem	divcan2 9642	A cancellation law for division. (Contributed by NM, 3-Feb-2004.) (Revised by Mario Carneiro, 27-May-2016.)
|- ( ( A e. CC /\ B e. CC /\ B =/= 0 ) -> ( B x. ( A / B ) ) = A )
Theorem	divcan1 9643	A cancellation law for division. (Contributed by NM, 5-Jun-2004.) (Revised by Mario Carneiro, 27-May-2016.)
|- ( ( A e. CC /\ B e. CC /\ B =/= 0 ) -> ( ( A / B ) x. B ) = A )
Theorem	diveq0 9644	A ratio is zero iff the numerator is zero. (Contributed by NM, 20-Apr-2006.) (Revised by Mario Carneiro, 27-May-2016.)
|- ( ( A e. CC /\ B e. CC /\ B =/= 0 ) -> ( ( A / B ) = 0 <-> A = 0 ) )
Theorem	divne0b 9645	The ratio of nonzero numbers is nonzero. (Contributed by NM, 2-Aug-2004.) (Proof shortened by Mario Carneiro, 27-May-2016.)
|- ( ( A e. CC /\ B e. CC /\ B =/= 0 ) -> ( A =/= 0 <-> ( A / B ) =/= 0 ) )
Theorem	divne0 9646	The ratio of nonzero numbers is nonzero. (Contributed by NM, 28-Dec-2007.)
|- ( ( ( A e. CC /\ A =/= 0 ) /\ ( B e. CC /\ B =/= 0 ) ) -> ( A / B ) =/= 0 )
Theorem	recne0 9647	The reciprocal of a nonzero number is nonzero. (Contributed by NM, 9-Feb-2006.) (Proof shortened by Mario Carneiro, 27-May-2016.)
|- ( ( A e. CC /\ A =/= 0 ) -> ( 1 / A ) =/= 0 )
Theorem	recid 9648	Multiplication of a number and its reciprocal. (Contributed by NM, 25-Oct-1999.) (Proof shortened by Mario Carneiro, 27-May-2016.)
|- ( ( A e. CC /\ A =/= 0 ) -> ( A x. ( 1 / A ) ) = 1 )
Theorem	recid2 9649	Multiplication of a number and its reciprocal. (Contributed by NM, 22-Jun-2006.) (Proof shortened by Mario Carneiro, 27-May-2016.)
|- ( ( A e. CC /\ A =/= 0 ) -> ( ( 1 / A ) x. A ) = 1 )
Theorem	divrec 9650	Relationship between division and reciprocal. Theorem I.9 of [Apostol] p. 18. (Contributed by NM, 2-Aug-2004.) (Revised by Mario Carneiro, 27-May-2016.)
|- ( ( A e. CC /\ B e. CC /\ B =/= 0 ) -> ( A / B ) = ( A x. ( 1 / B ) ) )
Theorem	divrec2 9651	Relationship between division and reciprocal. (Contributed by NM, 7-Feb-2006.)
|- ( ( A e. CC /\ B e. CC /\ B =/= 0 ) -> ( A / B ) = ( ( 1 / B ) x. A ) )
Theorem	divass 9652	An associative law for division. (Contributed by NM, 2-Aug-2004.)
|- ( ( A e. CC /\ B e. CC /\ ( C e. CC /\ C =/= 0 ) ) -> ( ( A x. B ) / C ) = ( A x. ( B / C ) ) )
Theorem	div23 9653	A commutative/associative law for division. (Contributed by NM, 2-Aug-2004.)
|- ( ( A e. CC /\ B e. CC /\ ( C e. CC /\ C =/= 0 ) ) -> ( ( A x. B ) / C ) = ( ( A / C ) x. B ) )
Theorem	div32 9654	A commutative/associative law for division. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ( A e. CC /\ ( B e. CC /\ B =/= 0 ) /\ C e. CC ) -> ( ( A / B ) x. C ) = ( A x. ( C / B ) ) )
Theorem	div13 9655	A commutative/associative law for division. (Contributed by NM, 22-Apr-2005.)
|- ( ( A e. CC /\ ( B e. CC /\ B =/= 0 ) /\ C e. CC ) -> ( ( A / B ) x. C ) = ( ( C / B ) x. A ) )
Theorem	div12 9656	A commutative/associative law for division. (Contributed by NM, 30-Apr-2005.)
|- ( ( A e. CC /\ B e. CC /\ ( C e. CC /\ C =/= 0 ) ) -> ( A x. ( B / C ) ) = ( B x. ( A / C ) ) )
Theorem	divdir 9657	Distribution of division over addition. (Contributed by NM, 31-Jul-2004.) (Proof shortened by Mario Carneiro, 27-May-2016.)
|- ( ( A e. CC /\ B e. CC /\ ( C e. CC /\ C =/= 0 ) ) -> ( ( A + B ) / C ) = ( ( A / C ) + ( B / C ) ) )
Theorem	divcan3 9658	A cancellation law for division. (Contributed by NM, 3-Feb-2004.) (Proof shortened by Mario Carneiro, 27-May-2016.)
|- ( ( A e. CC /\ B e. CC /\ B =/= 0 ) -> ( ( B x. A ) / B ) = A )
Theorem	divcan4 9659	A cancellation law for division. (Contributed by NM, 8-Feb-2005.)
|- ( ( A e. CC /\ B e. CC /\ B =/= 0 ) -> ( ( A x. B ) / B ) = A )
Theorem	div11 9660	One-to-one relationship for division. (Contributed by NM, 20-Apr-2006.) (Proof shortened by Mario Carneiro, 27-May-2016.)
|- ( ( A e. CC /\ B e. CC /\ ( C e. CC /\ C =/= 0 ) ) -> ( ( A / C ) = ( B / C ) <-> A = B ) )
Theorem	divid 9661	A number divided by itself is one. (Contributed by NM, 1-Aug-2004.)
|- ( ( A e. CC /\ A =/= 0 ) -> ( A / A ) = 1 )
Theorem	div0 9662	Division into zero is zero. (Contributed by NM, 14-Mar-2005.)
|- ( ( A e. CC /\ A =/= 0 ) -> ( 0 / A ) = 0 )
Theorem	div1 9663	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	diveq1 9664	Equality in terms of unit ratio. (Contributed by Stefan O'Rear, 27-Aug-2015.)
|- ( ( A e. CC /\ B e. CC /\ B =/= 0 ) -> ( ( A / B ) = 1 <-> A = B ) )
Theorem	divneg 9665	Move negative sign inside of a division. (Contributed by NM, 17-Sep-2004.)
|- ( ( A e. CC /\ B e. CC /\ B =/= 0 ) -> -u ( A / B ) = ( -u A / B ) )
Theorem	divsubdir 9666	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	recrec 9667	A number is equal to the reciprocal of its reciprocal. Theorem I.10 of [Apostol] p. 18. (Contributed by NM, 26-Sep-1999.) (Proof shortened by Mario Carneiro, 27-May-2016.)
|- ( ( A e. CC /\ A =/= 0 ) -> ( 1 / ( 1 / A ) ) = A )
Theorem	rec11 9668	Reciprocal is one-to-one. (Contributed by NM, 16-Sep-1999.) (Revised by Mario Carneiro, 27-May-2016.)
|- ( ( ( A e. CC /\ A =/= 0 ) /\ ( B e. CC /\ B =/= 0 ) ) -> ( ( 1 / A ) = ( 1 / B ) <-> A = B ) )
Theorem	rec11r 9669	Mutual reciprocals. (Contributed by Paul Chapman, 18-Oct-2007.)
|- ( ( ( A e. CC /\ A =/= 0 ) /\ ( B e. CC /\ B =/= 0 ) ) -> ( ( 1 / A ) = B <-> ( 1 / B ) = A ) )
Theorem	divmuldiv 9670	Multiplication of two ratios. Theorem I.14 of [Apostol] p. 18. (Contributed by NM, 1-Aug-2004.)
|- ( ( ( 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	divdivdiv 9671	Division of two ratios. Theorem I.15 of [Apostol] p. 18. (Contributed by NM, 2-Aug-2004.)
|- ( ( ( 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	divcan5 9672	Cancellation of common factor in a ratio. (Contributed by NM, 9-Jan-2006.)
|- ( ( A e. CC /\ ( B e. CC /\ B =/= 0 ) /\ ( C e. CC /\ C =/= 0 ) ) -> ( ( C x. A ) / ( C x. B ) ) = ( A / B ) )
Theorem	divmul13 9673	Swap the denominators in the product of two ratios. (Contributed by NM, 3-May-2005.)
|- ( ( ( 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	divmul24 9674	Swap the numerators in the product of two ratios. (Contributed by NM, 3-May-2005.)
|- ( ( ( 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	divmuleq 9675	Cross-multiply in an equality of ratios. (Contributed by Mario Carneiro, 23-Feb-2014.)
|- ( ( ( 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	recdiv 9676	The reciprocal of a ratio. (Contributed by NM, 3-Aug-2004.)
|- ( ( ( A e. CC /\ A =/= 0 ) /\ ( B e. CC /\ B =/= 0 ) ) -> ( 1 / ( A / B ) ) = ( B / A ) )
Theorem	divcan6 9677	Cancellation of inverted fractions. (Contributed by NM, 28-Dec-2007.)
|- ( ( ( A e. CC /\ A =/= 0 ) /\ ( B e. CC /\ B =/= 0 ) ) -> ( ( A / B ) x. ( B / A ) ) = 1 )
Theorem	divdiv32 9678	Swap denominators in a division. (Contributed by NM, 2-Aug-2004.)
|- ( ( A e. CC /\ ( B e. CC /\ B =/= 0 ) /\ ( C e. CC /\ C =/= 0 ) ) -> ( ( A / B ) / C ) = ( ( A / C ) / B ) )
Theorem	divcan7 9679	Cancel equal divisors in a division. (Contributed by Jeff Hankins, 29-Sep-2013.)
|- ( ( A e. CC /\ ( B e. CC /\ B =/= 0 ) /\ ( C e. CC /\ C =/= 0 ) ) -> ( ( A / C ) / ( B / C ) ) = ( A / B ) )
Theorem	dmdcan 9680	Cancellation law for division and multiplication. (Contributed by Scott Fenton, 7-Jun-2013.) (Proof shortened by Fan Zheng, 3-Jul-2016.)
|- ( ( ( A e. CC /\ A =/= 0 ) /\ ( B e. CC /\ B =/= 0 ) /\ C e. CC ) -> ( ( A / B ) x. ( C / A ) ) = ( C / B ) )
Theorem	divdiv1 9681	Division into a fraction. (Contributed by NM, 31-Dec-2007.)
|- ( ( A e. CC /\ ( B e. CC /\ B =/= 0 ) /\ ( C e. CC /\ C =/= 0 ) ) -> ( ( A / B ) / C ) = ( A / ( B x. C ) ) )
Theorem	divdiv2 9682	Division by a fraction. (Contributed by NM, 27-Dec-2008.)
|- ( ( A e. CC /\ ( B e. CC /\ B =/= 0 ) /\ ( C e. CC /\ C =/= 0 ) ) -> ( A / ( B / C ) ) = ( ( A x. C ) / B ) )
Theorem	recdiv2 9683	Division into a reciprocal. (Contributed by NM, 19-Oct-2007.)
|- ( ( ( A e. CC /\ A =/= 0 ) /\ ( B e. CC /\ B =/= 0 ) ) -> ( ( 1 / A ) / B ) = ( 1 / ( A x. B ) ) )
Theorem	ddcan 9684	Cancellation in a double division. (Contributed by Mario Carneiro, 26-Apr-2015.)
|- ( ( ( A e. CC /\ A =/= 0 ) /\ ( B e. CC /\ B =/= 0 ) ) -> ( A / ( A / B ) ) = B )
Theorem	divadddiv 9685	Addition of two ratios. Theorem I.13 of [Apostol] p. 18. (Contributed by NM, 1-Aug-2004.) (Revised by Mario Carneiro, 2-May-2016.)
|- ( ( ( 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	divsubdiv 9686	Subtraction of two ratios. (Contributed by Scott Fenton, 22-Apr-2014.) (Revised by Mario Carneiro, 2-May-2016.)
|- ( ( ( 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	conjmul 9687	Two numbers whose reciprocals sum to 1 are called "conjugates" and satisfy this relationship. Equation 5 of [Kreyszig] p. 12. (Contributed by NM, 12-Nov-2006.)
|- ( ( ( P e. CC /\ P =/= 0 ) /\ ( Q e. CC /\ Q =/= 0 ) ) -> ( ( ( 1 / P ) + ( 1 / Q ) ) = 1 <-> ( ( P - 1 ) x. ( Q - 1 ) ) = 1 ) )
Theorem	rereccl 9688	Closure law for reciprocal. (Contributed by NM, 30-Apr-2005.) (Revised by Mario Carneiro, 27-May-2016.)
|- ( ( A e. RR /\ A =/= 0 ) -> ( 1 / A ) e. RR )
Theorem	redivcl 9689	Closure law for division of reals. (Contributed by NM, 27-Sep-1999.) (Revised by Mario Carneiro, 27-May-2016.)
|- ( ( A e. RR /\ B e. RR /\ B =/= 0 ) -> ( A / B ) e. RR )
Theorem	eqneg 9690	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 9691	A complex number equals its negative iff it is zero. Deduction form of eqneg 9690. (Contributed by David Moews, 28-Feb-2017.)
|- ( ph -> A e. CC )   =>    |- ( ph -> ( A = -u A <-> A = 0 ) )
Theorem	eqnegad 9692	If a complex number equals its own negative, it is zero. One-way deduction form of eqneg 9690. (Contributed by David Moews, 28-Feb-2017.)
|- ( ph -> A e. CC )   &    |- ( ph -> A = -u A )   =>    |- ( ph -> A = 0 )
Theorem	div2neg 9693	Quotient of two negatives. (Contributed by Paul Chapman, 10-Nov-2012.)
|- ( ( A e. CC /\ B e. CC /\ B =/= 0 ) -> ( -u A / -u B ) = ( A / B ) )
Theorem	divneg2 9694	Move negative sign inside of a division. (Contributed by Mario Carneiro, 15-Sep-2014.)
|- ( ( A e. CC /\ B e. CC /\ B =/= 0 ) -> -u ( A / B ) = ( A / -u B ) )
Theorem	recclzi 9695	Closure law for reciprocal. (Contributed by NM, 30-Apr-2005.)
|- A e. CC   =>    |- ( A =/= 0 -> ( 1 / A ) e. CC )
Theorem	recne0zi 9696	The reciprocal of a nonzero number is nonzero. (Contributed by NM, 14-May-1999.)
|- A e. CC   =>    |- ( A =/= 0 -> ( 1 / A ) =/= 0 )
Theorem	recidzi 9697	Multiplication of a number and its reciprocal. (Contributed by NM, 14-May-1999.)
|- A e. CC   =>    |- ( A =/= 0 -> ( A x. ( 1 / A ) ) = 1 )
Theorem	div1i 9698	A number divided by 1 is itself. (Contributed by NM, 9-Jan-2002.)
|- A e. CC   =>    |- ( A / 1 ) = A
Theorem	eqnegi 9699	A number equal to its negative is zero. (Contributed by NM, 29-May-1999.)
|- A e. CC   =>    |- ( A = -u A <-> A = 0 )
Theorem	reccli 9700	Closure law for reciprocal. (Contributed by NM, 30-Apr-2005.)
|- A e. CC   &    |- A =/= 0   =>    |- ( 1 / A ) e. CC