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	msqge0i 7401	A square is nonnegative. (Contributed by NM, 14-May-1999.) (Proof shortened by Andrew Salmon, 19-Nov-2011.)
|- A e. RR   =>   |- 0 <_ (A x. A)
Theorem	msqge0d 7402	A square is nonnegative. (Contributed by Mario Carneiro, 27-May-2016.)
|- (ph -> A e. RR)   =>   |- (ph -> 0 <_ (A x. A))
Theorem	mulge0 7403	The product of two nonnegative numbers is nonnegative. (Contributed by NM, 8-Oct-1999.) (Revised by Mario Carneiro, 27-May-2016.)
|- (((A e. RR /\ 0 <_ A) /\ (B e. RR /\ 0 <_ B)) -> 0 <_ (A x. B))
Theorem	mulge0i 7404	The product of two nonnegative numbers is nonnegative. (Contributed by NM, 30-Jul-1999.)
|- A e. RR   &   |- B e. RR   =>   |- (( 0 <_ A /\ 0 <_ B) -> 0 <_ (A x. B))
Theorem	mulge0d 7405	The product of two nonnegative numbers is nonnegative. (Contributed by Mario Carneiro, 27-May-2016.)
|- (ph -> A e. RR)   &   |- (ph -> B e. RR)   &   |- (ph -> 0 <_ A)   &   |- (ph -> 0 <_ B)   =>   |- (ph -> 0 <_ (A x. B))
Theorem	apti 7406	Complex apartness is tight. (Contributed by Jim Kingdon, 21-Feb-2020.)
|- ((A e. CC /\ B e. CC) -> (A = B <-> -. A # B))
Theorem	apne 7407	Apartness implies negated equality. We cannot in general prove the converse, which is the whole point of having separate notations for apartness and negated equality. (Contributed by Jim Kingdon, 21-Feb-2020.)
|- ((A e. CC /\ B e. CC) -> (A # B -> A =/= B))
Theorem	gt0ap0 7408	Positive implies apart from zero. (Contributed by Jim Kingdon, 27-Feb-2020.)
|- ((A e. RR /\ 0 < A) -> A # 0)
Theorem	gt0ap0i 7409	Positive means apart from zero (useful for ordering theorems involving division). (Contributed by Jim Kingdon, 27-Feb-2020.)
|- A e. RR   =>   |- ( 0 < A -> A # 0)
Theorem	gt0ap0ii 7410	Positive implies apart from zero. (Contributed by Jim Kingdon, 27-Feb-2020.)
|- A e. RR   &   |- 0 < A   =>   |- A # 0
Theorem	gt0ap0d 7411	Positive implies apart from zero. Because of the way we define #, A must be an element of RR, not just RR*. (Contributed by Jim Kingdon, 27-Feb-2020.)
|- (ph -> A e. RR)   &   |- (ph -> 0 < A)   =>   |- (ph -> A # 0)
Theorem	negap0 7412	A number is apart from zero iff its negative is apart from zero. (Contributed by Jim Kingdon, 27-Feb-2020.)
|- (A e. CC -> (A # 0 <-> -uA # 0))
Theorem	ltleap 7413	Less than in terms of non-strict order and apartness. (Contributed by Jim Kingdon, 28-Feb-2020.)
|- ((A e. RR /\ B e. RR) -> (A < B <-> (A <_ B /\ A # B)))
3.3.7  Reciprocals
Theorem	recextlem1 7414	Lemma for recexap 7416. (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	recexaplem2 7415	Lemma for recexap 7416. (Contributed by Jim Kingdon, 20-Feb-2020.)
|- ((A e. RR /\ B e. RR /\ (A + ( _i x. B)) # 0) -> ((A x. A) + (B x. B)) # 0)
Theorem	recexap 7416*	Existence of reciprocal of nonzero complex number. (Contributed by Jim Kingdon, 20-Feb-2020.)
|- ((A e. CC /\ A # 0) -> E.x e. CC (A x. x) = 1)
Theorem	mulap0 7417	The product of two numbers apart from zero is apart from zero. Lemma 2.15 of [Geuvers], p. 6. (Contributed by Jim Kingdon, 22-Feb-2020.)
|- (((A e. CC /\ A # 0) /\ (B e. CC /\ B # 0)) -> (A x. B) # 0)
Theorem	mulap0b 7418	The product of two numbers apart from zero is apart from zero. (Contributed by Jim Kingdon, 24-Feb-2020.)
|- ((A e. CC /\ B e. CC) -> ((A # 0 /\ B # 0) <-> (A x. B) # 0))
Theorem	mulap0i 7419	The product of two numbers apart from zero is apart from zero. (Contributed by Jim Kingdon, 23-Feb-2020.)
|- A e. CC   &   |- B e. CC   &   |- A # 0   &   |- B # 0   =>   |- (A x. B) # 0
Theorem	mulap0bd 7420	The product of two numbers apart from zero is apart from zero. (Contributed by Jim Kingdon, 24-Feb-2020.)
|- (ph -> A e. CC)   &   |- (ph -> B e. CC)   =>   |- (ph -> ((A # 0 /\ B # 0) <-> (A x. B) # 0))
Theorem	mulap0d 7421	The product of two numbers apart from zero is apart from zero. (Contributed by Jim Kingdon, 23-Feb-2020.)
|- (ph -> A e. CC)   &   |- (ph -> B e. CC)   &   |- (ph -> A # 0)   &   |- (ph -> B # 0)   =>   |- (ph -> (A x. B) # 0)
Theorem	mulap0bad 7422	A factor of a complex number apart from zero is apart from zero. Partial converse of mulap0d 7421 and consequence of mulap0bd 7420. (Contributed by Jim Kingdon, 24-Feb-2020.)
|- (ph -> A e. CC)   &   |- (ph -> B e. CC)   &   |- (ph -> (A x. B) # 0)   =>   |- (ph -> A # 0)
Theorem	mulap0bbd 7423	A factor of a complex number apart from zero is apart from zero. Partial converse of mulap0d 7421 and consequence of mulap0bd 7420. (Contributed by Jim Kingdon, 24-Feb-2020.)
|- (ph -> A e. CC)   &   |- (ph -> B e. CC)   &   |- (ph -> (A x. B) # 0)   =>   |- (ph -> B # 0)
Theorem	mulcanapd 7424	Cancellation law for multiplication. (Contributed by Jim Kingdon, 21-Feb-2020.)
|- (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	mulcanap2d 7425	Cancellation law for multiplication. (Contributed by Jim Kingdon, 21-Feb-2020.)
|- (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	mulcanapad 7426	Cancellation of a nonzero factor on the left in an equation. One-way deduction form of mulcanapd 7424. (Contributed by Jim Kingdon, 21-Feb-2020.)
|- (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	mulcanap2ad 7427	Cancellation of a nonzero factor on the right in an equation. One-way deduction form of mulcanap2d 7425. (Contributed by Jim Kingdon, 21-Feb-2020.)
|- (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	mulcanap 7428	Cancellation law for multiplication (full theorem form). (Contributed by Jim Kingdon, 21-Feb-2020.)
|- ((A e. CC /\ B e. CC /\ ( C e. CC /\ C # 0)) -> (( C x. A) = ( C x. B) <-> A = B))
Theorem	mulcanap2 7429	Cancellation law for multiplication. (Contributed by Jim Kingdon, 21-Feb-2020.)
|- ((A e. CC /\ B e. CC /\ ( C e. CC /\ C # 0)) -> ((A x. C) = (B x. C) <-> A = B))
Theorem	mulcanapi 7430	Cancellation law for multiplication. (Contributed by Jim Kingdon, 21-Feb-2020.)
|- A e. CC   &   |- B e. CC   &   |- C e. CC   &   |- C # 0   =>   |- (( C x. A) = ( C x. B) <-> A = B)
Theorem	muleqadd 7431	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	receuap 7432*	Existential uniqueness of reciprocals. (Contributed by Jim Kingdon, 21-Feb-2020.)
|- ((A e. CC /\ B e. CC /\ B # 0) -> E!x e. CC (B x. x) = A)
3.3.8  Division
Syntax	cdiv 7433	Extend class notation to include division.
class /
Definition	df-div 7434*	Define division. Theorem divmulap 7436 relates it to multiplication, and divclap 7439 and redivclap 7489 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	divvalap 7435*	Value of division: the (unique) element x such that (B x. x) = A. This is meaningful only when B is apart from zero. (Contributed by Jim Kingdon, 21-Feb-2020.)
|- ((A e. CC /\ B e. CC /\ B # 0) -> (A / B) = ( iota_x e. CC (B x. x) = A))
Theorem	divmulap 7436	Relationship between division and multiplication. (Contributed by Jim Kingdon, 22-Feb-2020.)
|- ((A e. CC /\ B e. CC /\ ( C e. CC /\ C # 0)) -> ((A / C) = B <-> ( C x. B) = A))
Theorem	divmulap2 7437	Relationship between division and multiplication. (Contributed by Jim Kingdon, 22-Feb-2020.)
|- ((A e. CC /\ B e. CC /\ ( C e. CC /\ C # 0)) -> ((A / C) = B <-> A = ( C x. B)))
Theorem	divmulap3 7438	Relationship between division and multiplication. (Contributed by Jim Kingdon, 22-Feb-2020.)
|- ((A e. CC /\ B e. CC /\ ( C e. CC /\ C # 0)) -> ((A / C) = B <-> A = (B x. C)))
Theorem	divclap 7439	Closure law for division. (Contributed by Jim Kingdon, 22-Feb-2020.)
|- ((A e. CC /\ B e. CC /\ B # 0) -> (A / B) e. CC)
Theorem	recclap 7440	Closure law for reciprocal. (Contributed by Jim Kingdon, 22-Feb-2020.)
|- ((A e. CC /\ A # 0) -> ( 1 / A) e. CC)
Theorem	divcanap2 7441	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 7442	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 7443	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 7444	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 7445	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 7446	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 7447	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 7448	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 7449	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 7450	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 7451	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 7452	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 7453	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 7454	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 7455	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 7456	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 7457	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 7458	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 7459	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 7460	A number divided by itself is one. (Contributed by Jim Kingdon, 25-Feb-2020.)
|- ((A e. CC /\ A # 0) -> (A / A) = 1)
Theorem	div0ap 7461	Division into zero is zero. (Contributed by Jim Kingdon, 25-Feb-2020.)
|- ((A e. CC /\ A # 0) -> ( 0 / A) = 0)
Theorem	div1 7462	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 7463	1 divided by 1 is 1 (common case). (Contributed by David A. Wheeler, 7-Dec-2018.)
|- ( 1 / 1) = 1
Theorem	diveqap1 7464	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 7465	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 7466	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 7467	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 7468	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 7469	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 7470	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 7471	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 7472	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 7473	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 7474	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 7475	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 7476	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 7477	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 7478	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 7479	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 7480	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 7481	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 7482	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 7483	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 7484	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 7485	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 7486	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 7487	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 7488	Closure law for reciprocal. (Contributed by Jim Kingdon, 26-Feb-2020.)
|- ((A e. RR /\ A # 0) -> ( 1 / A) e. RR)
Theorem	redivclap 7489	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 7490	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 7491	A complex number equals its negative iff it is zero. Deduction form of eqneg 7490. (Contributed by David Moews, 28-Feb-2017.)
|- (ph -> A e. CC)   =>   |- (ph -> (A = -uA <-> A = 0))
Theorem	eqnegad 7492	If a complex number equals its own negative, it is zero. One-way deduction form of eqneg 7490. (Contributed by David Moews, 28-Feb-2017.)
|- (ph -> A e. CC)   &   |- (ph -> A = -uA)   =>   |- (ph -> A = 0)
Theorem	div2negap 7493	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 7494	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 7495	Closure law for reciprocal. (Contributed by Jim Kingdon, 27-Feb-2020.)
|- A e. CC   =>   |- (A # 0 -> ( 1 / A) e. CC)
Theorem	recap0apzi 7496	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 7497	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 7498	A number divided by 1 is itself. (Contributed by NM, 9-Jan-2002.)
|- A e. CC   =>   |- (A / 1) = A
Theorem	eqnegi 7499	A number equal to its negative is zero. (Contributed by NM, 29-May-1999.)
|- A e. CC   =>   |- (A = -uA <-> A = 0)
Theorem	recclapi 7500	Closure law for reciprocal. (Contributed by NM, 30-Apr-2005.)
|- A e. CC   &   |- A # 0   =>   |- ( 1 / A) e. CC