P. 98 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 - 9701-9800   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	recidi 9701	Multiplication of a number and its reciprocal. (Contributed by NM, 9-Feb-1995.)
|- A e. CC   &    |- A =/= 0   =>    |- ( A x. ( 1 / A ) ) = 1
Theorem	recreci 9702	A number is equal to the reciprocal of its reciprocal. Theorem I.10 of [Apostol] p. 18. (Contributed by NM, 9-Feb-1995.)
|- A e. CC   &    |- A =/= 0   =>    |- ( 1 / ( 1 / A ) ) = A
Theorem	dividi 9703	A number divided by itself is one. (Contributed by NM, 9-Feb-1995.)
|- A e. CC   &    |- A =/= 0   =>    |- ( A / A ) = 1
Theorem	div0i 9704	Division into zero is zero. (Contributed by NM, 12-Aug-1999.)
|- A e. CC   &    |- A =/= 0   =>    |- ( 0 / A ) = 0
Theorem	divclzi 9705	Closure law for division. (Contributed by NM, 7-May-1999.) (Revised by Mario Carneiro, 17-Feb-2014.)
|- A e. CC   &    |- B e. CC   =>    |- ( B =/= 0 -> ( A / B ) e. CC )
Theorem	divcan1zi 9706	A cancellation law for division. (Contributed by NM, 2-Oct-1999.)
|- A e. CC   &    |- B e. CC   =>    |- ( B =/= 0 -> ( ( A / B ) x. B ) = A )
Theorem	divcan2zi 9707	A cancellation law for division. (Contributed by NM, 10-Aug-1999.)
|- A e. CC   &    |- B e. CC   =>    |- ( B =/= 0 -> ( B x. ( A / B ) ) = A )
Theorem	divreczi 9708	Relationship between division and reciprocal. Theorem I.9 of [Apostol] p. 18. (Contributed by NM, 11-Oct-1999.)
|- A e. CC   &    |- B e. CC   =>    |- ( B =/= 0 -> ( A / B ) = ( A x. ( 1 / B ) ) )
Theorem	divcan3zi 9709	A cancellation law for division. (Eliminates a hypothesis of divcan3i 9716 with the weak deduction theorem.) (Contributed by NM, 3-Feb-2004.)
|- A e. CC   &    |- B e. CC   =>    |- ( B =/= 0 -> ( ( B x. A ) / B ) = A )
Theorem	divcan4zi 9710	A cancellation law for division. (Contributed by NM, 12-Oct-1999.)
|- A e. CC   &    |- B e. CC   =>    |- ( B =/= 0 -> ( ( A x. B ) / B ) = A )
Theorem	rec11i 9711	Reciprocal is one-to-one. (Contributed by NM, 16-Sep-1999.)
|- A e. CC   &    |- B e. CC   =>    |- ( ( A =/= 0 /\ B =/= 0 ) -> ( ( 1 / A ) = ( 1 / B ) <-> A = B ) )
Theorem	divcli 9712	Closure law for division. (Contributed by NM, 2-Feb-1995.) (Revised by Mario Carneiro, 17-Feb-2014.)
|- A e. CC   &    |- B e. CC   &    |- B =/= 0   =>    |- ( A / B ) e. CC
Theorem	divcan2i 9713	A cancellation law for division. (Contributed by NM, 9-Feb-1995.)
|- A e. CC   &    |- B e. CC   &    |- B =/= 0   =>    |- ( B x. ( A / B ) ) = A
Theorem	divcan1i 9714	A cancellation law for division. (Contributed by NM, 18-May-1999.)
|- A e. CC   &    |- B e. CC   &    |- B =/= 0   =>    |- ( ( A / B ) x. B ) = A
Theorem	divreci 9715	Relationship between division and reciprocal. Theorem I.9 of [Apostol] p. 18. (Contributed by NM, 9-Feb-1995.)
|- A e. CC   &    |- B e. CC   &    |- B =/= 0   =>    |- ( A / B ) = ( A x. ( 1 / B ) )
Theorem	divcan3i 9716	A cancellation law for division. (Contributed by NM, 16-Feb-1995.)
|- A e. CC   &    |- B e. CC   &    |- B =/= 0   =>    |- ( ( B x. A ) / B ) = A
Theorem	divcan4i 9717	A cancellation law for division. (Contributed by NM, 18-May-1999.)
|- A e. CC   &    |- B e. CC   &    |- B =/= 0   =>    |- ( ( A x. B ) / B ) = A
Theorem	divne0i 9718	The ratio of nonzero numbers is nonzero. (Contributed by NM, 9-Feb-1995.)
|- A e. CC   &    |- B e. CC   &    |- A =/= 0   &    |- B =/= 0   =>    |- ( A / B ) =/= 0
Theorem	rec11ii 9719	Reciprocal is one-to-one. (Contributed by NM, 16-Sep-1999.)
|- A e. CC   &    |- B e. CC   &    |- A =/= 0   &    |- B =/= 0   =>    |- ( ( 1 / A ) = ( 1 / B ) <-> A = B )
Theorem	divasszi 9720	An associative law for division. (Contributed by NM, 12-Aug-1999.)
|- A e. CC   &    |- B e. CC   &    |- C e. CC   =>    |- ( C =/= 0 -> ( ( A x. B ) / C ) = ( A x. ( B / C ) ) )
Theorem	divmulzi 9721	Relationship between division and multiplication. (Contributed by NM, 8-May-1999.) (Revised by Mario Carneiro, 17-Feb-2014.)
|- A e. CC   &    |- B e. CC   &    |- C e. CC   =>    |- ( B =/= 0 -> ( ( A / B ) = C <-> ( B x. C ) = A ) )
Theorem	divdirzi 9722	Distribution of division over addition. (Contributed by NM, 31-Jul-2004.)
|- A e. CC   &    |- B e. CC   &    |- C e. CC   =>    |- ( C =/= 0 -> ( ( A + B ) / C ) = ( ( A / C ) + ( B / C ) ) )
Theorem	divdiv23zi 9723	Swap denominators in a division. (Contributed by NM, 15-Sep-1999.)
|- A e. CC   &    |- B e. CC   &    |- C e. CC   =>    |- ( ( B =/= 0 /\ C =/= 0 ) -> ( ( A / B ) / C ) = ( ( A / C ) / B ) )
Theorem	divmuli 9724	Relationship between division and multiplication. (Contributed by NM, 2-Feb-1995.) (Revised by Mario Carneiro, 17-Feb-2014.)
|- A e. CC   &    |- B e. CC   &    |- C e. CC   &    |- B =/= 0   =>    |- ( ( A / B ) = C <-> ( B x. C ) = A )
Theorem	divdiv32i 9725	Swap denominators in a division. (Contributed by NM, 15-Sep-1999.)
|- A e. CC   &    |- B e. CC   &    |- C e. CC   &    |- B =/= 0   &    |- C =/= 0   =>    |- ( ( A / B ) / C ) = ( ( A / C ) / B )
Theorem	divassi 9726	An associative law for division. (Contributed by NM, 15-Feb-1995.)
|- A e. CC   &    |- B e. CC   &    |- C e. CC   &    |- C =/= 0   =>    |- ( ( A x. B ) / C ) = ( A x. ( B / C ) )
Theorem	divdiri 9727	Distribution of division over addition. (Contributed by NM, 16-Feb-1995.)
|- A e. CC   &    |- B e. CC   &    |- C e. CC   &    |- C =/= 0   =>    |- ( ( A + B ) / C ) = ( ( A / C ) + ( B / C ) )
Theorem	div23i 9728	A commutative/associative law for division. (Contributed by NM, 3-Sep-1999.)
|- A e. CC   &    |- B e. CC   &    |- C e. CC   &    |- C =/= 0   =>    |- ( ( A x. B ) / C ) = ( ( A / C ) x. B )
Theorem	div11i 9729	One-to-one relationship for division. (Contributed by NM, 20-Aug-2001.)
|- A e. CC   &    |- B e. CC   &    |- C e. CC   &    |- C =/= 0   =>    |- ( ( A / C ) = ( B / C ) <-> A = B )
Theorem	divmuldivi 9730	Multiplication of two ratios. Theorem I.14 of [Apostol] p. 18. (Contributed by NM, 16-Feb-1995.)
|- A e. CC   &    |- B e. CC   &    |- C e. CC   &    |- D e. CC   &    |- B =/= 0   &    |- D =/= 0   =>    |- ( ( A / B ) x. ( C / D ) ) = ( ( A x. C ) / ( B x. D ) )
Theorem	divmul13i 9731	Swap denominators of two ratios. (Contributed by NM, 6-Aug-1999.)
|- A e. CC   &    |- B e. CC   &    |- C e. CC   &    |- D e. CC   &    |- B =/= 0   &    |- D =/= 0   =>    |- ( ( A / B ) x. ( C / D ) ) = ( ( C / B ) x. ( A / D ) )
Theorem	divadddivi 9732	Addition of two ratios. Theorem I.13 of [Apostol] p. 18. (Contributed by NM, 21-Feb-1995.)
|- A e. CC   &    |- B e. CC   &    |- C e. CC   &    |- D e. CC   &    |- B =/= 0   &    |- D =/= 0   =>    |- ( ( A / B ) + ( C / D ) ) = ( ( ( A x. D ) + ( C x. B ) ) / ( B x. D ) )
Theorem	divdivdivi 9733	Division of two ratios. Theorem I.15 of [Apostol] p. 18. (Contributed by NM, 22-Feb-1995.)
|- A e. CC   &    |- B e. CC   &    |- C e. CC   &    |- D e. CC   &    |- B =/= 0   &    |- D =/= 0   &    |- C =/= 0   =>    |- ( ( A / B ) / ( C / D ) ) = ( ( A x. D ) / ( B x. C ) )
Theorem	rerecclzi 9734	Closure law for reciprocal. (Contributed by NM, 30-Apr-2005.)
|- A e. RR   =>    |- ( A =/= 0 -> ( 1 / A ) e. RR )
Theorem	rereccli 9735	Closure law for reciprocal. (Contributed by NM, 30-Apr-2005.)
|- A e. RR   &    |- A =/= 0   =>    |- ( 1 / A ) e. RR
Theorem	redivclzi 9736	Closure law for division of reals. (Contributed by NM, 9-May-1999.)
|- A e. RR   &    |- B e. RR   =>    |- ( B =/= 0 -> ( A / B ) e. RR )
Theorem	redivcli 9737	Closure law for division of reals. (Contributed by NM, 9-May-1999.)
|- A e. RR   &    |- B e. RR   &    |- B =/= 0   =>    |- ( A / B ) e. RR
Theorem	div1d 9738	A number divided by 1 is itself. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. CC )   =>    |- ( ph -> ( A / 1 ) = A )
Theorem	reccld 9739	Closure law for reciprocal. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. CC )   &    |- ( ph -> A =/= 0 )   =>    |- ( ph -> ( 1 / A ) e. CC )
Theorem	recne0d 9740	The reciprocal of a nonzero number is nonzero. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. CC )   &    |- ( ph -> A =/= 0 )   =>    |- ( ph -> ( 1 / A ) =/= 0 )
Theorem	recidd 9741	Multiplication of a number and its reciprocal. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. CC )   &    |- ( ph -> A =/= 0 )   =>    |- ( ph -> ( A x. ( 1 / A ) ) = 1 )
Theorem	recid2d 9742	Multiplication of a number and its reciprocal. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. CC )   &    |- ( ph -> A =/= 0 )   =>    |- ( ph -> ( ( 1 / A ) x. A ) = 1 )
Theorem	recrecd 9743	A number is equal to the reciprocal of its reciprocal. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. CC )   &    |- ( ph -> A =/= 0 )   =>    |- ( ph -> ( 1 / ( 1 / A ) ) = A )
Theorem	dividd 9744	A number divided by itself is one. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. CC )   &    |- ( ph -> A =/= 0 )   =>    |- ( ph -> ( A / A ) = 1 )
Theorem	div0d 9745	Division into zero is zero. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. CC )   &    |- ( ph -> A =/= 0 )   =>    |- ( ph -> ( 0 / A ) = 0 )
Theorem	divcld 9746	Closure law for division. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> B =/= 0 )   =>    |- ( ph -> ( A / B ) e. CC )
Theorem	divcan1d 9747	A cancellation law for division. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> B =/= 0 )   =>    |- ( ph -> ( ( A / B ) x. B ) = A )
Theorem	divcan2d 9748	A cancellation law for division. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> B =/= 0 )   =>    |- ( ph -> ( B x. ( A / B ) ) = A )
Theorem	divrecd 9749	Relationship between division and reciprocal. Theorem I.9 of [Apostol] p. 18. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> B =/= 0 )   =>    |- ( ph -> ( A / B ) = ( A x. ( 1 / B ) ) )
Theorem	divrec2d 9750	Relationship between division and reciprocal. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> B =/= 0 )   =>    |- ( ph -> ( A / B ) = ( ( 1 / B ) x. A ) )
Theorem	divcan3d 9751	A cancellation law for division. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> B =/= 0 )   =>    |- ( ph -> ( ( B x. A ) / B ) = A )
Theorem	divcan4d 9752	A cancellation law for division. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> B =/= 0 )   =>    |- ( ph -> ( ( A x. B ) / B ) = A )
Theorem	diveq0d 9753	A ratio is zero iff the numerator is zero. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> B =/= 0 )   &    |- ( ph -> ( A / B ) = 0 )   =>    |- ( ph -> A = 0 )
Theorem	diveq1d 9754	Equality in terms of unit ratio. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> B =/= 0 )   &    |- ( ph -> ( A / B ) = 1 )   =>    |- ( ph -> A = B )
Theorem	diveq1ad 9755	The quotient of two complex numbers is one iff they are equal. Deduction form of diveq1 9664. Generalization of diveq1d 9754. (Contributed by David Moews, 28-Feb-2017.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> B =/= 0 )   =>    |- ( ph -> ( ( A / B ) = 1 <-> A = B ) )
Theorem	diveq0ad 9756	A fraction of complex numbers is zero iff its numerator is. Deduction form of diveq0 9644. (Contributed by David Moews, 28-Feb-2017.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> B =/= 0 )   =>    |- ( ph -> ( ( A / B ) = 0 <-> A = 0 ) )
Theorem	divne1d 9757	If two complex numbers are unequal, their quotient is not one. Contrapositive of diveq1d 9754. (Contributed by David Moews, 28-Feb-2017.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> B =/= 0 )   &    |- ( ph -> A =/= B )   =>    |- ( ph -> ( A / B ) =/= 1 )
Theorem	divne0bd 9758	A ratio is zero iff the numerator is zero. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> B =/= 0 )   =>    |- ( ph -> ( A =/= 0 <-> ( A / B ) =/= 0 ) )
Theorem	divnegd 9759	Move negative sign inside of a division. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> B =/= 0 )   =>    |- ( ph -> -u ( A / B ) = ( -u A / B ) )
Theorem	divneg2d 9760	Move negative sign inside of a division. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> B =/= 0 )   =>    |- ( ph -> -u ( A / B ) = ( A / -u B ) )
Theorem	div2negd 9761	Quotient of two negatives. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> B =/= 0 )   =>    |- ( ph -> ( -u A / -u B ) = ( A / B ) )
Theorem	divne0d 9762	The ratio of 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 / B ) =/= 0 )
Theorem	recdivd 9763	The reciprocal of a ratio. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> A =/= 0 )   &    |- ( ph -> B =/= 0 )   =>    |- ( ph -> ( 1 / ( A / B ) ) = ( B / A ) )
Theorem	recdiv2d 9764	Division into a reciprocal. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> A =/= 0 )   &    |- ( ph -> B =/= 0 )   =>    |- ( ph -> ( ( 1 / A ) / B ) = ( 1 / ( A x. B ) ) )
Theorem	divcan6d 9765	Cancellation of inverted fractions. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> A =/= 0 )   &    |- ( ph -> B =/= 0 )   =>    |- ( ph -> ( ( A / B ) x. ( B / A ) ) = 1 )
Theorem	ddcand 9766	Cancellation in a double division. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> A =/= 0 )   &    |- ( ph -> B =/= 0 )   =>    |- ( ph -> ( A / ( A / B ) ) = B )
Theorem	rec11d 9767	Reciprocal is one-to-one. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> A =/= 0 )   &    |- ( ph -> B =/= 0 )   &    |- ( ph -> ( 1 / A ) = ( 1 / B ) )   =>    |- ( ph -> A = B )
Theorem	divmuld 9768	Relationship between division and multiplication. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> C e. CC )   &    |- ( ph -> B =/= 0 )   =>    |- ( ph -> ( ( A / B ) = C <-> ( B x. C ) = A ) )
Theorem	div32d 9769	A commutative/associative law for division. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> C e. CC )   &    |- ( ph -> B =/= 0 )   =>    |- ( ph -> ( ( A / B ) x. C ) = ( A x. ( C / B ) ) )
Theorem	div13d 9770	A commutative/associative law for division. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> C e. CC )   &    |- ( ph -> B =/= 0 )   =>    |- ( ph -> ( ( A / B ) x. C ) = ( ( C / B ) x. A ) )
Theorem	divdiv32d 9771	Swap denominators in a division. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> C e. CC )   &    |- ( ph -> B =/= 0 )   &    |- ( ph -> C =/= 0 )   =>    |- ( ph -> ( ( A / B ) / C ) = ( ( A / C ) / B ) )
Theorem	divcan5d 9772	Cancellation of common factor in a ratio. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> C e. CC )   &    |- ( ph -> B =/= 0 )   &    |- ( ph -> C =/= 0 )   =>    |- ( ph -> ( ( C x. A ) / ( C x. B ) ) = ( A / B ) )
Theorem	divcan5rd 9773	Cancellation of common factor in a ratio. (Contributed by Mario Carneiro, 1-Jan-2017.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> C e. CC )   &    |- ( ph -> B =/= 0 )   &    |- ( ph -> C =/= 0 )   =>    |- ( ph -> ( ( A x. C ) / ( B x. C ) ) = ( A / B ) )
Theorem	divcan7d 9774	Cancel equal divisors in a division. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> C e. CC )   &    |- ( ph -> B =/= 0 )   &    |- ( ph -> C =/= 0 )   =>    |- ( ph -> ( ( A / C ) / ( B / C ) ) = ( A / B ) )
Theorem	dmdcand 9775	Cancellation law for division and multiplication. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> C e. CC )   &    |- ( ph -> B =/= 0 )   &    |- ( ph -> C =/= 0 )   =>    |- ( ph -> ( ( B / C ) x. ( A / B ) ) = ( A / C ) )
Theorem	dmdcan2d 9776	Cancellation law for division and multiplication. (Contributed by David Moews, 28-Feb-2017.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> C e. CC )   &    |- ( ph -> B =/= 0 )   &    |- ( ph -> C =/= 0 )   =>    |- ( ph -> ( ( A / B ) x. ( B / C ) ) = ( A / C ) )
Theorem	divdiv1d 9777	Division into a fraction. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> C e. CC )   &    |- ( ph -> B =/= 0 )   &    |- ( ph -> C =/= 0 )   =>    |- ( ph -> ( ( A / B ) / C ) = ( A / ( B x. C ) ) )
Theorem	divdiv2d 9778	Division by a fraction. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> C e. CC )   &    |- ( ph -> B =/= 0 )   &    |- ( ph -> C =/= 0 )   =>    |- ( ph -> ( A / ( B / C ) ) = ( ( A x. C ) / B ) )
Theorem	divmul2d 9779	Relationship between division and multiplication. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> C e. CC )   &    |- ( ph -> C =/= 0 )   =>    |- ( ph -> ( ( A / C ) = B <-> A = ( C x. B ) ) )
Theorem	divmul3d 9780	Relationship between division and multiplication. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> C e. CC )   &    |- ( ph -> C =/= 0 )   =>    |- ( ph -> ( ( A / C ) = B <-> A = ( B x. C ) ) )
Theorem	divassd 9781	An associative law for division. (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. B ) / C ) = ( A x. ( B / C ) ) )
Theorem	div12d 9782	A commutative/associative law for division. (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. ( B / C ) ) = ( B x. ( A / C ) ) )
Theorem	div23d 9783	A commutative/associative law for division. (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. B ) / C ) = ( ( A / C ) x. B ) )
Theorem	divdird 9784	Distribution of division over addition. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> C e. CC )   &    |- ( ph -> C =/= 0 )   =>    |- ( ph -> ( ( A + B ) / C ) = ( ( A / C ) + ( B / C ) ) )
Theorem	divsubdird 9785	Distribution of division over subtraction. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> C e. CC )   &    |- ( ph -> C =/= 0 )   =>    |- ( ph -> ( ( A - B ) / C ) = ( ( A / C ) - ( B / C ) ) )
Theorem	div11d 9786	One-to-one relationship for division. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> C e. CC )   &    |- ( ph -> C =/= 0 )   &    |- ( ph -> ( A / C ) = ( B / C ) )   =>    |- ( ph -> A = B )
Theorem	divmuldivd 9787	Multiplication of two ratios. Theorem I.14 of [Apostol] p. 18. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> C e. CC )   &    |- ( ph -> D e. CC )   &    |- ( ph -> B =/= 0 )   &    |- ( ph -> D =/= 0 )   =>    |- ( ph -> ( ( A / B ) x. ( C / D ) ) = ( ( A x. C ) / ( B x. D ) ) )
Theorem	divmul13d 9788	Swap denominators of two ratios. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> C e. CC )   &    |- ( ph -> D e. CC )   &    |- ( ph -> B =/= 0 )   &    |- ( ph -> D =/= 0 )   =>    |- ( ph -> ( ( A / B ) x. ( C / D ) ) = ( ( C / B ) x. ( A / D ) ) )
Theorem	divmul24d 9789	Swap the numerators in the product of two ratios. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> C e. CC )   &    |- ( ph -> D e. CC )   &    |- ( ph -> B =/= 0 )   &    |- ( ph -> D =/= 0 )   =>    |- ( ph -> ( ( A / B ) x. ( C / D ) ) = ( ( A / D ) x. ( C / B ) ) )
Theorem	divadddivd 9790	Addition of two ratios. Theorem I.13 of [Apostol] p. 18. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> C e. CC )   &    |- ( ph -> D e. CC )   &    |- ( ph -> B =/= 0 )   &    |- ( ph -> D =/= 0 )   =>    |- ( ph -> ( ( A / B ) + ( C / D ) ) = ( ( ( A x. D ) + ( C x. B ) ) / ( B x. D ) ) )
Theorem	divsubdivd 9791	Subtraction of two ratios. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> C e. CC )   &    |- ( ph -> D e. CC )   &    |- ( ph -> B =/= 0 )   &    |- ( ph -> D =/= 0 )   =>    |- ( ph -> ( ( A / B ) - ( C / D ) ) = ( ( ( A x. D ) - ( C x. B ) ) / ( B x. D ) ) )
Theorem	divmuleqd 9792	Cross-multiply in an equality of ratios. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> C e. CC )   &    |- ( ph -> D e. CC )   &    |- ( ph -> B =/= 0 )   &    |- ( ph -> D =/= 0 )   =>    |- ( ph -> ( ( A / B ) = ( C / D ) <-> ( A x. D ) = ( C x. B ) ) )
Theorem	divdivdivd 9793	Division of two ratios. Theorem I.15 of [Apostol] p. 18. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> C e. CC )   &    |- ( ph -> D e. CC )   &    |- ( ph -> B =/= 0 )   &    |- ( ph -> D =/= 0 )   &    |- ( ph -> C =/= 0 )   =>    |- ( ph -> ( ( A / B ) / ( C / D ) ) = ( ( A x. D ) / ( B x. C ) ) )
Theorem	diveq1bd 9794	If two complex numbers are equal, their quotient is one. One-way deduction form of diveq1 9664. Converse of diveq1d 9754. (Contributed by David Moews, 28-Feb-2017.)
|- ( ph -> B e. CC )   &    |- ( ph -> B =/= 0 )   &    |- ( ph -> A = B )   =>    |- ( ph -> ( A / B ) = 1 )
Theorem	div2sub 9795	Swap the order of subtraction in a division. (Contributed by Scott Fenton, 24-Jun-2013.)
|- ( ( ( A e. CC /\ B e. CC ) /\ ( C e. CC /\ D e. CC /\ C =/= D ) ) -> ( ( A - B ) / ( C - D ) ) = ( ( B - A ) / ( D - C ) ) )
Theorem	div2subd 9796	Swap subtrahend and minuend inside the numerator and denominator of a fraction. Deduction form of div2sub 9795. (Contributed by David Moews, 28-Feb-2017.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> C e. CC )   &    |- ( ph -> D e. CC )   &    |- ( ph -> C =/= D )   =>    |- ( ph -> ( ( A - B ) / ( C - D ) ) = ( ( B - A ) / ( D - C ) ) )
Theorem	rereccld 9797	Closure law for reciprocal. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. RR )   &    |- ( ph -> A =/= 0 )   =>    |- ( ph -> ( 1 / A ) e. RR )
Theorem	redivcld 9798	Closure law for division of reals. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> B =/= 0 )   =>    |- ( ph -> ( A / B ) e. RR )
Theorem	subrec 9799	Subtraction of reciprocals. (Contributed by Scott Fenton, 9-Jul-2015.)
|- ( ( ( A e. CC /\ A =/= 0 ) /\ ( B e. CC /\ B =/= 0 ) ) -> ( ( 1 / A ) - ( 1 / B ) ) = ( ( B - A ) / ( A x. B ) ) )
Theorem	subreci 9800	Subtraction of reciprocals. (Contributed by Scott Fenton, 9-Jan-2017.)
|- A e. CC   &    |- B e. CC   &    |- A =/= 0   &    |- B =/= 0   =>    |- ( ( 1 / A ) - ( 1 / B ) ) = ( ( B - A ) / ( A x. B ) )