P. 88 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 8701-8800   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	div0api 8701	Division into zero is zero. (Contributed by NM, 12-Aug-1999.)
|- A e. CC   &    |- A # 0   =>    |- ( 0 / A ) = 0
Theorem	divclapzi 8702	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 8703	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 8704	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 8705	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 8706	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 8707	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 8708	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 8709	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 8710	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 8711	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 8712	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 8713	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 8714	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 8715	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 8716	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 8717	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 8718	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 8719	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 8720	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 8721	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 8722	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 8723	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 8724	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 8725	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 8726	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 8727	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 8728	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 8729	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 8730	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 8731	Closure law for reciprocal. (Contributed by Jim Kingdon, 9-Mar-2020.)
|- A e. RR   =>    |- ( A # 0 -> ( 1 / A ) e. RR )
Theorem	rerecclapi 8732	Closure law for reciprocal. (Contributed by Jim Kingdon, 9-Mar-2020.)
|- A e. RR   &    |- A # 0   =>    |- ( 1 / A ) e. RR
Theorem	redivclapzi 8733	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 )
Theorem	redivclapi 8734	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
Theorem	div1d 8735	A number divided by 1 is itself. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. CC )   =>    |- ( ph -> ( A / 1 ) = A )
Theorem	recclapd 8736	Closure law for reciprocal. (Contributed by Jim Kingdon, 3-Mar-2020.)
|- ( ph -> A e. CC )   &    |- ( ph -> A # 0 )   =>    |- ( ph -> ( 1 / A ) e. CC )
Theorem	recap0d 8737	The reciprocal of a number apart from zero is apart from zero. (Contributed by Jim Kingdon, 3-Mar-2020.)
|- ( ph -> A e. CC )   &    |- ( ph -> A # 0 )   =>    |- ( ph -> ( 1 / A ) # 0 )
Theorem	recidapd 8738	Multiplication of a number and its reciprocal. (Contributed by Jim Kingdon, 3-Mar-2020.)
|- ( ph -> A e. CC )   &    |- ( ph -> A # 0 )   =>    |- ( ph -> ( A x. ( 1 / A ) ) = 1 )
Theorem	recidap2d 8739	Multiplication of a number and its reciprocal. (Contributed by Jim Kingdon, 3-Mar-2020.)
|- ( ph -> A e. CC )   &    |- ( ph -> A # 0 )   =>    |- ( ph -> ( ( 1 / A ) x. A ) = 1 )
Theorem	recrecapd 8740	A number is equal to the reciprocal of its reciprocal. (Contributed by Jim Kingdon, 3-Mar-2020.)
|- ( ph -> A e. CC )   &    |- ( ph -> A # 0 )   =>    |- ( ph -> ( 1 / ( 1 / A ) ) = A )
Theorem	dividapd 8741	A number divided by itself is one. (Contributed by Jim Kingdon, 3-Mar-2020.)
|- ( ph -> A e. CC )   &    |- ( ph -> A # 0 )   =>    |- ( ph -> ( A / A ) = 1 )
Theorem	div0apd 8742	Division into zero is zero. (Contributed by Jim Kingdon, 3-Mar-2020.)
|- ( ph -> A e. CC )   &    |- ( ph -> A # 0 )   =>    |- ( ph -> ( 0 / A ) = 0 )
Theorem	apmul1 8743	Multiplication of both sides of complex apartness by a complex number apart from zero. (Contributed by Jim Kingdon, 20-Mar-2020.)
|- ( ( A e. CC /\ B e. CC /\ ( C e. CC /\ C # 0 ) ) -> ( A # B <-> ( A x. C ) # ( B x. C ) ) )
Theorem	apmul2 8744	Multiplication of both sides of complex apartness by a complex number apart from zero. (Contributed by Jim Kingdon, 6-Jan-2023.)
|- ( ( A e. CC /\ B e. CC /\ ( C e. CC /\ C # 0 ) ) -> ( A # B <-> ( C x. A ) # ( C x. B ) ) )
Theorem	divclapd 8745	Closure law for division. (Contributed by Jim Kingdon, 29-Feb-2020.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> B # 0 )   =>    |- ( ph -> ( A / B ) e. CC )
Theorem	divcanap1d 8746	A cancellation law for division. (Contributed by Jim Kingdon, 29-Feb-2020.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> B # 0 )   =>    |- ( ph -> ( ( A / B ) x. B ) = A )
Theorem	divcanap2d 8747	A cancellation law for division. (Contributed by Jim Kingdon, 29-Feb-2020.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> B # 0 )   =>    |- ( ph -> ( B x. ( A / B ) ) = A )
Theorem	divrecapd 8748	Relationship between division and reciprocal. Theorem I.9 of [Apostol] p. 18. (Contributed by Jim Kingdon, 29-Feb-2020.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> B # 0 )   =>    |- ( ph -> ( A / B ) = ( A x. ( 1 / B ) ) )
Theorem	divrecap2d 8749	Relationship between division and reciprocal. (Contributed by Jim Kingdon, 29-Feb-2020.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> B # 0 )   =>    |- ( ph -> ( A / B ) = ( ( 1 / B ) x. A ) )
Theorem	divcanap3d 8750	A cancellation law for division. (Contributed by Jim Kingdon, 29-Feb-2020.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> B # 0 )   =>    |- ( ph -> ( ( B x. A ) / B ) = A )
Theorem	divcanap4d 8751	A cancellation law for division. (Contributed by Jim Kingdon, 29-Feb-2020.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> B # 0 )   =>    |- ( ph -> ( ( A x. B ) / B ) = A )
Theorem	diveqap0d 8752	If a ratio is zero, the numerator is zero. (Contributed by Jim Kingdon, 19-Mar-2020.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> B # 0 )   &    |- ( ph -> ( A / B ) = 0 )   =>    |- ( ph -> A = 0 )
Theorem	diveqap1d 8753	Equality in terms of unit ratio. (Contributed by Jim Kingdon, 19-Mar-2020.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> B # 0 )   &    |- ( ph -> ( A / B ) = 1 )   =>    |- ( ph -> A = B )
Theorem	diveqap1ad 8754	The quotient of two complex numbers is one iff they are equal. Deduction form of diveqap1 8660. Generalization of diveqap1d 8753. (Contributed by Jim Kingdon, 19-Mar-2020.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> B # 0 )   =>    |- ( ph -> ( ( A / B ) = 1 <-> A = B ) )
Theorem	diveqap0ad 8755	A fraction of complex numbers is zero iff its numerator is. Deduction form of diveqap0 8637. (Contributed by Jim Kingdon, 19-Mar-2020.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> B # 0 )   =>    |- ( ph -> ( ( A / B ) = 0 <-> A = 0 ) )
Theorem	divap1d 8756	If two complex numbers are apart, their quotient is apart from one. (Contributed by Jim Kingdon, 20-Mar-2020.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> B # 0 )   &    |- ( ph -> A # B )   =>    |- ( ph -> ( A / B ) # 1 )
Theorem	divap0bd 8757	A ratio is zero iff the numerator is zero. (Contributed by Jim Kingdon, 19-Mar-2020.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> B # 0 )   =>    |- ( ph -> ( A # 0 <-> ( A / B ) # 0 ) )
Theorem	divnegapd 8758	Move negative sign inside of a division. (Contributed by Jim Kingdon, 19-Mar-2020.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> B # 0 )   =>    |- ( ph -> -u ( A / B ) = ( -u A / B ) )
Theorem	divneg2apd 8759	Move negative sign inside of a division. (Contributed by Jim Kingdon, 19-Mar-2020.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> B # 0 )   =>    |- ( ph -> -u ( A / B ) = ( A / -u B ) )
Theorem	div2negapd 8760	Quotient of two negatives. (Contributed by Jim Kingdon, 19-Mar-2020.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> B # 0 )   =>    |- ( ph -> ( -u A / -u B ) = ( A / B ) )
Theorem	divap0d 8761	The ratio of numbers apart from zero is apart from zero. (Contributed by Jim Kingdon, 3-Mar-2020.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> A # 0 )   &    |- ( ph -> B # 0 )   =>    |- ( ph -> ( A / B ) # 0 )
Theorem	recdivapd 8762	The reciprocal of a ratio. (Contributed by Jim Kingdon, 3-Mar-2020.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> A # 0 )   &    |- ( ph -> B # 0 )   =>    |- ( ph -> ( 1 / ( A / B ) ) = ( B / A ) )
Theorem	recdivap2d 8763	Division into a reciprocal. (Contributed by Jim Kingdon, 3-Mar-2020.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> A # 0 )   &    |- ( ph -> B # 0 )   =>    |- ( ph -> ( ( 1 / A ) / B ) = ( 1 / ( A x. B ) ) )
Theorem	divcanap6d 8764	Cancellation of inverted fractions. (Contributed by Jim Kingdon, 3-Mar-2020.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> A # 0 )   &    |- ( ph -> B # 0 )   =>    |- ( ph -> ( ( A / B ) x. ( B / A ) ) = 1 )
Theorem	ddcanapd 8765	Cancellation in a double division. (Contributed by Jim Kingdon, 3-Mar-2020.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> A # 0 )   &    |- ( ph -> B # 0 )   =>    |- ( ph -> ( A / ( A / B ) ) = B )
Theorem	rec11apd 8766	Reciprocal is one-to-one. (Contributed by Jim Kingdon, 3-Mar-2020.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> A # 0 )   &    |- ( ph -> B # 0 )   &    |- ( ph -> ( 1 / A ) = ( 1 / B ) )   =>    |- ( ph -> A = B )
Theorem	divmulapd 8767	Relationship between division and multiplication. (Contributed by Jim Kingdon, 8-Mar-2020.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> C e. CC )   &    |- ( ph -> B # 0 )   =>    |- ( ph -> ( ( A / B ) = C <-> ( B x. C ) = A ) )
Theorem	apdivmuld 8768	Relationship between division and multiplication. (Contributed by Jim Kingdon, 26-Dec-2022.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> C e. CC )   &    |- ( ph -> B # 0 )   =>    |- ( ph -> ( ( A / B ) # C <-> ( B x. C ) # A ) )
Theorem	div32apd 8769	A commutative/associative law for division. (Contributed by Jim Kingdon, 8-Mar-2020.)
|- ( 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	div13apd 8770	A commutative/associative law for division. (Contributed by Jim Kingdon, 8-Mar-2020.)
|- ( 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	divdiv32apd 8771	Swap denominators in a division. (Contributed by Jim Kingdon, 8-Mar-2020.)
|- ( 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	divcanap5d 8772	Cancellation of common factor in a ratio. (Contributed by Jim Kingdon, 8-Mar-2020.)
|- ( 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	divcanap5rd 8773	Cancellation of common factor in a ratio. (Contributed by Jim Kingdon, 8-Mar-2020.)
|- ( 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	divcanap7d 8774	Cancel equal divisors in a division. (Contributed by Jim Kingdon, 8-Mar-2020.)
|- ( 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	dmdcanapd 8775	Cancellation law for division and multiplication. (Contributed by Jim Kingdon, 8-Mar-2020.)
|- ( 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	dmdcanap2d 8776	Cancellation law for division and multiplication. (Contributed by Jim Kingdon, 8-Mar-2020.)
|- ( 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	divdivap1d 8777	Division into a fraction. (Contributed by Jim Kingdon, 8-Mar-2020.)
|- ( 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	divdivap2d 8778	Division by a fraction. (Contributed by Jim Kingdon, 8-Mar-2020.)
|- ( 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	divmulap2d 8779	Relationship between division and multiplication. (Contributed by Jim Kingdon, 2-Mar-2020.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> C e. CC )   &    |- ( ph -> C # 0 )   =>    |- ( ph -> ( ( A / C ) = B <-> A = ( C x. B ) ) )
Theorem	divmulap3d 8780	Relationship between division and multiplication. (Contributed by Jim Kingdon, 2-Mar-2020.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> C e. CC )   &    |- ( ph -> C # 0 )   =>    |- ( ph -> ( ( A / C ) = B <-> A = ( B x. C ) ) )
Theorem	divassapd 8781	An associative law for division. (Contributed by Jim Kingdon, 2-Mar-2020.)
|- ( 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	div12apd 8782	A commutative/associative law for division. (Contributed by Jim Kingdon, 2-Mar-2020.)
|- ( 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	div23apd 8783	A commutative/associative law for division. (Contributed by Jim Kingdon, 2-Mar-2020.)
|- ( 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	divdirapd 8784	Distribution of division over addition. (Contributed by Jim Kingdon, 2-Mar-2020.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> C e. CC )   &    |- ( ph -> C # 0 )   =>    |- ( ph -> ( ( A + B ) / C ) = ( ( A / C ) + ( B / C ) ) )
Theorem	divsubdirapd 8785	Distribution of division over subtraction. (Contributed by Jim Kingdon, 2-Mar-2020.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> C e. CC )   &    |- ( ph -> C # 0 )   =>    |- ( ph -> ( ( A - B ) / C ) = ( ( A / C ) - ( B / C ) ) )
Theorem	div11apd 8786	One-to-one relationship for division. (Contributed by Jim Kingdon, 2-Mar-2020.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> C e. CC )   &    |- ( ph -> C # 0 )   &    |- ( ph -> ( A / C ) = ( B / C ) )   =>    |- ( ph -> A = B )
Theorem	divmuldivapd 8787	Multiplication of two ratios. (Contributed by Jim Kingdon, 30-Jul-2021.)
|- ( 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	divmuleqapd 8788	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	rerecclapd 8789	Closure law for reciprocal. (Contributed by Jim Kingdon, 29-Feb-2020.)
|- ( ph -> A e. RR )   &    |- ( ph -> A # 0 )   =>    |- ( ph -> ( 1 / A ) e. RR )
Theorem	redivclapd 8790	Closure law for division of reals. (Contributed by Jim Kingdon, 29-Feb-2020.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> B # 0 )   =>    |- ( ph -> ( A / B ) e. RR )
Theorem	diveqap1bd 8791	If two complex numbers are equal, their quotient is one. One-way deduction form of diveqap1 8660. Converse of diveqap1d 8753. (Contributed by David Moews, 28-Feb-2017.) (Revised by Jim Kingdon, 2-Aug-2023.)
|- ( ph -> B e. CC )   &    |- ( ph -> B # 0 )   &    |- ( ph -> A = B )   =>    |- ( ph -> ( A / B ) = 1 )
Theorem	div2subap 8792	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	div2subapd 8793	Swap subtrahend and minuend inside the numerator and denominator of a fraction. Deduction form of div2subap 8792. (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	subrecap 8794	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	subrecapi 8795	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 ) )
Theorem	subrecapd 8796	Subtraction of reciprocals. (Contributed by Scott Fenton, 9-Jan-2017.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> A # 0 )   &    |- ( ph -> B # 0 )   =>    |- ( ph -> ( ( 1 / A ) - ( 1 / B ) ) = ( ( B - A ) / ( A x. B ) ) )
Theorem	mvllmulapd 8797	Move LHS left multiplication to RHS. (Contributed by Jim Kingdon, 10-Jun-2020.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> A # 0 )   &    |- ( ph -> ( A x. B ) = C )   =>    |- ( ph -> B = ( C / A ) )
Theorem	rerecapb 8798*	A real number has a multiplicative inverse if and only if it is apart from zero. Theorem 11.2.4 of [HoTT], p. (varies). (Contributed by Jim Kingdon, 18-Jan-2025.)
|- ( A e. RR -> ( A # 0 <-> E. x e. RR ( A x. x ) = 1 ) )
4.3.9  Ordering on reals (cont.)
Theorem	ltp1 8799	A number is less than itself plus 1. (Contributed by NM, 20-Aug-2001.)
|- ( A e. RR -> A < ( A + 1 ) )
Theorem	lep1 8800	A number is less than or equal to itself plus 1. (Contributed by NM, 5-Jan-2006.)
|- ( A e. RR -> A <_ ( A + 1 ) )