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	recclap 8901	Closure law for reciprocal. (Contributed by Jim Kingdon, 22-Feb-2020.)
|- ( ( A e. CC /\ A # 0 ) -> ( 1 / A ) e. CC )
Theorem	divcanap2 8902	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 8903	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 8904	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 8905	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 8906	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 8907	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 8908	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 8909	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 8910	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 8911	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 8912	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 8913	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 8914	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 8915	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 8916	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 8917	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 8918	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 8919	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 8920	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 8921	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 8922	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 8923	A number divided by itself is one. (Contributed by Jim Kingdon, 25-Feb-2020.)
|- ( ( A e. CC /\ A # 0 ) -> ( A / A ) = 1 )
Theorem	div0ap 8924	Division into zero is zero. (Contributed by Jim Kingdon, 25-Feb-2020.)
|- ( ( A e. CC /\ A # 0 ) -> ( 0 / A ) = 0 )
Theorem	div1 8925	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 8926	1 divided by 1 is 1 (common case). (Contributed by David A. Wheeler, 7-Dec-2018.)
|- ( 1 / 1 ) = 1
Theorem	diveqap1 8927	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 8928	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 8929	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 8930	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 8931	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 8932	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 8933	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 8934	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 8935	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 8936	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 8937	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 8938	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 8939	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 8940	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 8941	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 8942	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 8943	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 8944	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 8945	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 8946	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 8947	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 8948	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 8949	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 8950	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 8951	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 8952	Closure law for reciprocal. (Contributed by Jim Kingdon, 26-Feb-2020.)
|- ( ( A e. RR /\ A # 0 ) -> ( 1 / A ) e. RR )
Theorem	redivclap 8953	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 8954	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 8955	A complex number equals its negative iff it is zero. Deduction form of eqneg 8954. (Contributed by David Moews, 28-Feb-2017.)
|- ( ph -> A e. CC )   =>    |- ( ph -> ( A = -u A <-> A = 0 ) )
Theorem	eqnegad 8956	If a complex number equals its own negative, it is zero. One-way deduction form of eqneg 8954. (Contributed by David Moews, 28-Feb-2017.)
|- ( ph -> A e. CC )   &    |- ( ph -> A = -u A )   =>    |- ( ph -> A = 0 )
Theorem	div2negap 8957	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 8958	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 8959	Closure law for reciprocal. (Contributed by Jim Kingdon, 27-Feb-2020.)
|- A e. CC   =>    |- ( A # 0 -> ( 1 / A ) e. CC )
Theorem	recap0apzi 8960	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 8961	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 8962	A number divided by 1 is itself. (Contributed by NM, 9-Jan-2002.)
|- A e. CC   =>    |- ( A / 1 ) = A
Theorem	eqnegi 8963	A number equal to its negative is zero. (Contributed by NM, 29-May-1999.)
|- A e. CC   =>    |- ( A = -u A <-> A = 0 )
Theorem	recclapi 8964	Closure law for reciprocal. (Contributed by NM, 30-Apr-2005.)
|- A e. CC   &    |- A # 0   =>    |- ( 1 / A ) e. CC
Theorem	recidapi 8965	Multiplication of a number and its reciprocal. (Contributed by NM, 9-Feb-1995.)
|- A e. CC   &    |- A # 0   =>    |- ( A x. ( 1 / A ) ) = 1
Theorem	recrecapi 8966	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	dividapi 8967	A number divided by itself is one. (Contributed by NM, 9-Feb-1995.)
|- A e. CC   &    |- A # 0   =>    |- ( A / A ) = 1
Theorem	div0api 8968	Division into zero is zero. (Contributed by NM, 12-Aug-1999.)
|- A e. CC   &    |- A # 0   =>    |- ( 0 / A ) = 0
Theorem	divclapzi 8969	Closure law for division. (Contributed by Jim Kingdon, 27-Feb-2020.)
|- A e. CC   &    |- B e. CC   =>    |- ( B # 0 -> ( A / B ) e. CC )
Theorem	divcanap1zi 8970	A cancellation law for division. (Contributed by Jim Kingdon, 27-Feb-2020.)
|- A e. CC   &    |- B e. CC   =>    |- ( B # 0 -> ( ( A / B ) x. B ) = A )
Theorem	divcanap2zi 8971	A cancellation law for division. (Contributed by Jim Kingdon, 27-Feb-2020.)
|- A e. CC   &    |- B e. CC   =>    |- ( B # 0 -> ( B x. ( A / B ) ) = A )
Theorem	divrecapzi 8972	Relationship between division and reciprocal. (Contributed by Jim Kingdon, 27-Feb-2020.)
|- A e. CC   &    |- B e. CC   =>    |- ( B # 0 -> ( A / B ) = ( A x. ( 1 / B ) ) )
Theorem	divcanap3zi 8973	A cancellation law for division. (Contributed by Jim Kingdon, 27-Feb-2020.)
|- A e. CC   &    |- B e. CC   =>    |- ( B # 0 -> ( ( B x. A ) / B ) = A )
Theorem	divcanap4zi 8974	A cancellation law for division. (Contributed by Jim Kingdon, 27-Feb-2020.)
|- A e. CC   &    |- B e. CC   =>    |- ( B # 0 -> ( ( A x. B ) / B ) = A )
Theorem	rec11api 8975	Reciprocal is one-to-one. (Contributed by Jim Kingdon, 28-Feb-2020.)
|- A e. CC   &    |- B e. CC   =>    |- ( ( A # 0 /\ B # 0 ) -> ( ( 1 / A ) = ( 1 / B ) <-> A = B ) )
Theorem	divclapi 8976	Closure law for division. (Contributed by Jim Kingdon, 28-Feb-2020.)
|- A e. CC   &    |- B e. CC   &    |- B # 0   =>    |- ( A / B ) e. CC
Theorem	divcanap2i 8977	A cancellation law for division. (Contributed by Jim Kingdon, 28-Feb-2020.)
|- A e. CC   &    |- B e. CC   &    |- B # 0   =>    |- ( B x. ( A / B ) ) = A
Theorem	divcanap1i 8978	A cancellation law for division. (Contributed by Jim Kingdon, 28-Feb-2020.)
|- A e. CC   &    |- B e. CC   &    |- B # 0   =>    |- ( ( A / B ) x. B ) = A
Theorem	divrecapi 8979	Relationship between division and reciprocal. (Contributed by Jim Kingdon, 28-Feb-2020.)
|- A e. CC   &    |- B e. CC   &    |- B # 0   =>    |- ( A / B ) = ( A x. ( 1 / B ) )
Theorem	divcanap3i 8980	A cancellation law for division. (Contributed by Jim Kingdon, 28-Feb-2020.)
|- A e. CC   &    |- B e. CC   &    |- B # 0   =>    |- ( ( B x. A ) / B ) = A
Theorem	divcanap4i 8981	A cancellation law for division. (Contributed by Jim Kingdon, 28-Feb-2020.)
|- A e. CC   &    |- B e. CC   &    |- B # 0   =>    |- ( ( A x. B ) / B ) = A
Theorem	divap0i 8982	The ratio of numbers apart from zero is apart from zero. (Contributed by Jim Kingdon, 28-Feb-2020.)
|- A e. CC   &    |- B e. CC   &    |- A # 0   &    |- B # 0   =>    |- ( A / B ) # 0
Theorem	rec11apii 8983	Reciprocal is one-to-one. (Contributed by Jim Kingdon, 28-Feb-2020.)
|- A e. CC   &    |- B e. CC   &    |- A # 0   &    |- B # 0   =>    |- ( ( 1 / A ) = ( 1 / B ) <-> A = B )
Theorem	divassapzi 8984	An associative law for division. (Contributed by Jim Kingdon, 28-Feb-2020.)
|- A e. CC   &    |- B e. CC   &    |- C e. CC   =>    |- ( C # 0 -> ( ( A x. B ) / C ) = ( A x. ( B / C ) ) )
Theorem	divmulapzi 8985	Relationship between division and multiplication. (Contributed by Jim Kingdon, 28-Feb-2020.)
|- A e. CC   &    |- B e. CC   &    |- C e. CC   =>    |- ( B # 0 -> ( ( A / B ) = C <-> ( B x. C ) = A ) )
Theorem	divdirapzi 8986	Distribution of division over addition. (Contributed by Jim Kingdon, 28-Feb-2020.)
|- A e. CC   &    |- B e. CC   &    |- C e. CC   =>    |- ( C # 0 -> ( ( A + B ) / C ) = ( ( A / C ) + ( B / C ) ) )
Theorem	divdiv23apzi 8987	Swap denominators in a division. (Contributed by Jim Kingdon, 28-Feb-2020.)
|- A e. CC   &    |- B e. CC   &    |- C e. CC   =>    |- ( ( B # 0 /\ C # 0 ) -> ( ( A / B ) / C ) = ( ( A / C ) / B ) )
Theorem	divmulapi 8988	Relationship between division and multiplication. (Contributed by Jim Kingdon, 29-Feb-2020.)
|- A e. CC   &    |- B e. CC   &    |- C e. CC   &    |- B # 0   =>    |- ( ( A / B ) = C <-> ( B x. C ) = A )
Theorem	divdiv32api 8989	Swap denominators in a division. (Contributed by Jim Kingdon, 29-Feb-2020.)
|- A e. CC   &    |- B e. CC   &    |- C e. CC   &    |- B # 0   &    |- C # 0   =>    |- ( ( A / B ) / C ) = ( ( A / C ) / B )
Theorem	divassapi 8990	An associative law for division. (Contributed by Jim Kingdon, 9-Mar-2020.)
|- A e. CC   &    |- B e. CC   &    |- C e. CC   &    |- C # 0   =>    |- ( ( A x. B ) / C ) = ( A x. ( B / C ) )
Theorem	divdirapi 8991	Distribution of division over addition. (Contributed by Jim Kingdon, 9-Mar-2020.)
|- A e. CC   &    |- B e. CC   &    |- C e. CC   &    |- C # 0   =>    |- ( ( A + B ) / C ) = ( ( A / C ) + ( B / C ) )
Theorem	div23api 8992	A commutative/associative law for division. (Contributed by Jim Kingdon, 9-Mar-2020.)
|- A e. CC   &    |- B e. CC   &    |- C e. CC   &    |- C # 0   =>    |- ( ( A x. B ) / C ) = ( ( A / C ) x. B )
Theorem	div11api 8993	One-to-one relationship for division. (Contributed by Jim Kingdon, 9-Mar-2020.)
|- A e. CC   &    |- B e. CC   &    |- C e. CC   &    |- C # 0   =>    |- ( ( A / C ) = ( B / C ) <-> A = B )
Theorem	divmuldivapi 8994	Multiplication of two ratios. (Contributed by Jim Kingdon, 9-Mar-2020.)
|- 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	divmul13api 8995	Swap denominators of two ratios. (Contributed by Jim Kingdon, 9-Mar-2020.)
|- 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	divadddivapi 8996	Addition of two ratios. (Contributed by Jim Kingdon, 9-Mar-2020.)
|- 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	divdivdivapi 8997	Division of two ratios. (Contributed by Jim Kingdon, 9-Mar-2020.)
|- 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	rerecclapzi 8998	Closure law for reciprocal. (Contributed by Jim Kingdon, 9-Mar-2020.)
|- A e. RR   =>    |- ( A # 0 -> ( 1 / A ) e. RR )
Theorem	rerecclapi 8999	Closure law for reciprocal. (Contributed by Jim Kingdon, 9-Mar-2020.)
|- A e. RR   &    |- A # 0   =>    |- ( 1 / A ) e. RR
Theorem	redivclapzi 9000	Closure law for division of reals. (Contributed by Jim Kingdon, 9-Mar-2020.)
|- A e. RR   &    |- B e. RR   =>    |- ( B # 0 -> ( A / B ) e. RR )