P. 75 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 7401-7500   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	divcanap2 7401	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 7402	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 7403	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 7404	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 7405	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 7406	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 7407	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 7408	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 7409	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 7410	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 7411	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 7412	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 7413	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 7414	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 7415	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	divdirap 7416	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 7417	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 7418	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 7419	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 7420	A number divided by itself is one. (Contributed by Jim Kingdon, 25-Feb-2020.)
|- ((A e. CC /\ A # 0) -> (A / A) = 1)
Theorem	div0ap 7421	Division into zero is zero. (Contributed by Jim Kingdon, 25-Feb-2020.)
|- ((A e. CC /\ A # 0) -> ( 0 / A) = 0)
Theorem	div1 7422	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 7423	1 divided by 1 is 1 (common case). (Contributed by David A. Wheeler, 7-Dec-2018.)
|- ( 1 / 1) = 1
Theorem	diveqap1 7424	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 7425	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) = ( -uA / B))
Theorem	divsubdirap 7426	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 7427	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 7428	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 7429	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 7430	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 7431	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 7432	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 7433	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 7434	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 7435	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 7436	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 7437	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 7438	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 7439	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 7440	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 7441	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 7442	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 7443	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 7444	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 7445	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 7446	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 7447	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 7448	Closure law for reciprocal. (Contributed by Jim Kingdon, 26-Feb-2020.)
|- ((A e. RR /\ A # 0) -> ( 1 / A) e. RR)
Theorem	redivclap 7449	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 7450	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 = -uA <-> A = 0))
Theorem	eqnegd 7451	A complex number equals its negative iff it is zero. Deduction form of eqneg 7450. (Contributed by David Moews, 28-Feb-2017.)
|- (ph -> A e. CC)   =>   |- (ph -> (A = -uA <-> A = 0))
Theorem	eqnegad 7452	If a complex number equals its own negative, it is zero. One-way deduction form of eqneg 7450. (Contributed by David Moews, 28-Feb-2017.)
|- (ph -> A e. CC)   &   |- (ph -> A = -uA)   =>   |- (ph -> A = 0)
Theorem	div2negap 7453	Quotient of two negatives. (Contributed by Jim Kingdon, 27-Feb-2020.)
|- ((A e. CC /\ B e. CC /\ B # 0) -> ( -uA / -uB) = (A / B))
Theorem	divneg2ap 7454	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 / -uB))
Theorem	recclapzi 7455	Closure law for reciprocal. (Contributed by Jim Kingdon, 27-Feb-2020.)
|- A e. CC   =>   |- (A # 0 -> ( 1 / A) e. CC)
Theorem	recap0apzi 7456	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 7457	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 7458	A number divided by 1 is itself. (Contributed by NM, 9-Jan-2002.)
|- A e. CC   =>   |- (A / 1) = A
Theorem	eqnegi 7459	A number equal to its negative is zero. (Contributed by NM, 29-May-1999.)
|- A e. CC   =>   |- (A = -uA <-> A = 0)
Theorem	recclapi 7460	Closure law for reciprocal. (Contributed by NM, 30-Apr-2005.)
|- A e. CC   &   |- A # 0   =>   |- ( 1 / A) e. CC
Theorem	recidapi 7461	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 7462	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 7463	A number divided by itself is one. (Contributed by NM, 9-Feb-1995.)
|- A e. CC   &   |- A # 0   =>   |- (A / A) = 1
Theorem	div0api 7464	Division into zero is zero. (Contributed by NM, 12-Aug-1999.)
|- A e. CC   &   |- A # 0   =>   |- ( 0 / A) = 0
Theorem	divclapzi 7465	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 7466	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 7467	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 7468	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 7469	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 7470	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 7471	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 7472	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 7473	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 7474	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 7475	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 7476	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 7477	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 7478	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 7479	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 7480	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 7481	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 7482	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 7483	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 7484	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 7485	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 7486	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 7487	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 7488	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 7489	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 7490	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 7491	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 7492	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 7493	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 7494	Closure law for reciprocal. (Contributed by Jim Kingdon, 9-Mar-2020.)
|- A e. RR   =>   |- (A # 0 -> ( 1 / A) e. RR)
Theorem	rerecclapi 7495	Closure law for reciprocal. (Contributed by Jim Kingdon, 9-Mar-2020.)
|- A e. RR   &   |- A # 0   =>   |- ( 1 / A) e. RR
Theorem	redivclapzi 7496	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 7497	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 7498	A number divided by 1 is itself. (Contributed by Mario Carneiro, 27-May-2016.)
|- (ph -> A e. CC)   =>   |- (ph -> (A / 1) = A)
Theorem	recclapd 7499	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 7500	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)