P. 86 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 8501-8600   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	neg11d 8501	If the difference between two numbers is zero, they are equal. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> -u A = -u B )   =>    |- ( ph -> A = B )
Theorem	negdid 8502	Distribution of negative over addition. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   =>    |- ( ph -> -u ( A + B ) = ( -u A + -u B ) )
Theorem	negdi2d 8503	Distribution of negative over addition. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   =>    |- ( ph -> -u ( A + B ) = ( -u A - B ) )
Theorem	negsubdid 8504	Distribution of negative over subtraction. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   =>    |- ( ph -> -u ( A - B ) = ( -u A + B ) )
Theorem	negsubdi2d 8505	Distribution of negative over subtraction. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   =>    |- ( ph -> -u ( A - B ) = ( B - A ) )
Theorem	neg2subd 8506	Relationship between subtraction and negative. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   =>    |- ( ph -> ( -u A - -u B ) = ( B - A ) )
Theorem	subaddd 8507	Relationship between subtraction and addition. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> C e. CC )   =>    |- ( ph -> ( ( A - B ) = C <-> ( B + C ) = A ) )
Theorem	subadd2d 8508	Relationship between subtraction and addition. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> C e. CC )   =>    |- ( ph -> ( ( A - B ) = C <-> ( C + B ) = A ) )
Theorem	addsubassd 8509	Associative-type law for subtraction and addition. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> C e. CC )   =>    |- ( ph -> ( ( A + B ) - C ) = ( A + ( B - C ) ) )
Theorem	addsubd 8510	Law for subtraction and addition. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> C e. CC )   =>    |- ( ph -> ( ( A + B ) - C ) = ( ( A - C ) + B ) )
Theorem	subadd23d 8511	Commutative/associative law for addition and subtraction. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> C e. CC )   =>    |- ( ph -> ( ( A - B ) + C ) = ( A + ( C - B ) ) )
Theorem	addsub12d 8512	Commutative/associative law for addition and subtraction. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> C e. CC )   =>    |- ( ph -> ( A + ( B - C ) ) = ( B + ( A - C ) ) )
Theorem	npncand 8513	Cancellation law for subtraction. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> C e. CC )   =>    |- ( ph -> ( ( A - B ) + ( B - C ) ) = ( A - C ) )
Theorem	nppcand 8514	Cancellation law for subtraction. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> C e. CC )   =>    |- ( ph -> ( ( ( A - B ) + C ) + B ) = ( A + C ) )
Theorem	nppcan2d 8515	Cancellation law for subtraction. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> C e. CC )   =>    |- ( ph -> ( ( A - ( B + C ) ) + C ) = ( A - B ) )
Theorem	nppcan3d 8516	Cancellation law for subtraction. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> C e. CC )   =>    |- ( ph -> ( ( A - B ) + ( C + B ) ) = ( A + C ) )
Theorem	subsubd 8517	Law for double subtraction. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> C e. CC )   =>    |- ( ph -> ( A - ( B - C ) ) = ( ( A - B ) + C ) )
Theorem	subsub2d 8518	Law for double subtraction. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> C e. CC )   =>    |- ( ph -> ( A - ( B - C ) ) = ( A + ( C - B ) ) )
Theorem	subsub3d 8519	Law for double subtraction. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> C e. CC )   =>    |- ( ph -> ( A - ( B - C ) ) = ( ( A + C ) - B ) )
Theorem	subsub4d 8520	Law for double subtraction. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> C e. CC )   =>    |- ( ph -> ( ( A - B ) - C ) = ( A - ( B + C ) ) )
Theorem	sub32d 8521	Swap the second and third terms in a double subtraction. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> C e. CC )   =>    |- ( ph -> ( ( A - B ) - C ) = ( ( A - C ) - B ) )
Theorem	nnncand 8522	Cancellation law for subtraction. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> C e. CC )   =>    |- ( ph -> ( ( A - ( B - C ) ) - C ) = ( A - B ) )
Theorem	nnncan1d 8523	Cancellation law for subtraction. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> C e. CC )   =>    |- ( ph -> ( ( A - B ) - ( A - C ) ) = ( C - B ) )
Theorem	nnncan2d 8524	Cancellation law for subtraction. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> C e. CC )   =>    |- ( ph -> ( ( A - C ) - ( B - C ) ) = ( A - B ) )
Theorem	npncan3d 8525	Cancellation law for subtraction. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> C e. CC )   =>    |- ( ph -> ( ( A - B ) + ( C - A ) ) = ( C - B ) )
Theorem	pnpcand 8526	Cancellation law for mixed addition and subtraction. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> C e. CC )   =>    |- ( ph -> ( ( A + B ) - ( A + C ) ) = ( B - C ) )
Theorem	pnpcan2d 8527	Cancellation law for mixed addition and subtraction. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> C e. CC )   =>    |- ( ph -> ( ( A + C ) - ( B + C ) ) = ( A - B ) )
Theorem	pnncand 8528	Cancellation law for mixed addition and subtraction. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> C e. CC )   =>    |- ( ph -> ( ( A + B ) - ( A - C ) ) = ( B + C ) )
Theorem	ppncand 8529	Cancellation law for mixed addition and subtraction. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> C e. CC )   =>    |- ( ph -> ( ( A + B ) + ( C - B ) ) = ( A + C ) )
Theorem	subcand 8530	Cancellation law for subtraction. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> C e. CC )   &    |- ( ph -> ( A - B ) = ( A - C ) )   =>    |- ( ph -> B = C )
Theorem	subcan2d 8531	Cancellation law for subtraction. (Contributed by Mario Carneiro, 22-Sep-2016.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> C e. CC )   &    |- ( ph -> ( A - C ) = ( B - C ) )   =>    |- ( ph -> A = B )
Theorem	subcanad 8532	Cancellation law for subtraction. Deduction form of subcan 8433. Generalization of subcand 8530. (Contributed by David Moews, 28-Feb-2017.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> C e. CC )   =>    |- ( ph -> ( ( A - B ) = ( A - C ) <-> B = C ) )
Theorem	subneintrd 8533	Introducing subtraction on both sides of a statement of inequality. Contrapositive of subcand 8530. (Contributed by David Moews, 28-Feb-2017.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> C e. CC )   &    |- ( ph -> B =/= C )   =>    |- ( ph -> ( A - B ) =/= ( A - C ) )
Theorem	subcan2ad 8534	Cancellation law for subtraction. Deduction form of subcan2 8403. Generalization of subcan2d 8531. (Contributed by David Moews, 28-Feb-2017.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> C e. CC )   =>    |- ( ph -> ( ( A - C ) = ( B - C ) <-> A = B ) )
Theorem	subneintr2d 8535	Introducing subtraction on both sides of a statement of inequality. Contrapositive of subcan2d 8531. (Contributed by David Moews, 28-Feb-2017.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> C e. CC )   &    |- ( ph -> A =/= B )   =>    |- ( ph -> ( A - C ) =/= ( B - C ) )
Theorem	addsub4d 8536	Rearrangement of 4 terms in a mixed addition and subtraction. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> C e. CC )   &    |- ( ph -> D e. CC )   =>    |- ( ph -> ( ( A + B ) - ( C + D ) ) = ( ( A - C ) + ( B - D ) ) )
Theorem	subadd4d 8537	Rearrangement of 4 terms in a mixed addition and subtraction. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> C e. CC )   &    |- ( ph -> D e. CC )   =>    |- ( ph -> ( ( A - B ) - ( C - D ) ) = ( ( A + D ) - ( B + C ) ) )
Theorem	sub4d 8538	Rearrangement of 4 terms in a subtraction. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> C e. CC )   &    |- ( ph -> D e. CC )   =>    |- ( ph -> ( ( A - B ) - ( C - D ) ) = ( ( A - C ) - ( B - D ) ) )
Theorem	2addsubd 8539	Law for subtraction and addition. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> C e. CC )   &    |- ( ph -> D e. CC )   =>    |- ( ph -> ( ( ( A + B ) + C ) - D ) = ( ( ( A + C ) - D ) + B ) )
Theorem	addsubeq4d 8540	Relation between sums and differences. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> C e. CC )   &    |- ( ph -> D e. CC )   =>    |- ( ph -> ( ( A + B ) = ( C + D ) <-> ( C - A ) = ( B - D ) ) )
Theorem	subeqxfrd 8541	Transfer two terms of a subtraction in an equality. (Contributed by Thierry Arnoux, 2-Feb-2020.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> C e. CC )   &    |- ( ph -> D e. CC )   &    |- ( ph -> ( A - B ) = ( C - D ) )   =>    |- ( ph -> ( A - C ) = ( B - D ) )
Theorem	mvlraddd 8542	Move LHS right addition to RHS. (Contributed by David A. Wheeler, 15-Oct-2018.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> ( A + B ) = C )   =>    |- ( ph -> A = ( C - B ) )
Theorem	mvlladdd 8543	Move LHS left addition to RHS. (Contributed by David A. Wheeler, 15-Oct-2018.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> ( A + B ) = C )   =>    |- ( ph -> B = ( C - A ) )
Theorem	mvrraddd 8544	Move RHS right addition to LHS. (Contributed by David A. Wheeler, 15-Oct-2018.)
|- ( ph -> B e. CC )   &    |- ( ph -> C e. CC )   &    |- ( ph -> A = ( B + C ) )   =>    |- ( ph -> ( A - C ) = B )
Theorem	mvrladdd 8545	Move RHS left addition to LHS. (Contributed by David A. Wheeler, 11-Oct-2018.)
|- ( ph -> B e. CC )   &    |- ( ph -> C e. CC )   &    |- ( ph -> A = ( B + C ) )   =>    |- ( ph -> ( A - B ) = C )
Theorem	assraddsubd 8546	Associate RHS addition-subtraction. (Contributed by David A. Wheeler, 15-Oct-2018.)
|- ( ph -> B e. CC )   &    |- ( ph -> C e. CC )   &    |- ( ph -> D e. CC )   &    |- ( ph -> A = ( ( B + C ) - D ) )   =>    |- ( ph -> A = ( B + ( C - D ) ) )
Theorem	subaddeqd 8547	Transfer two terms of a subtraction to an addition in an equality. (Contributed by Thierry Arnoux, 2-Feb-2020.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> C e. CC )   &    |- ( ph -> D e. CC )   &    |- ( ph -> ( A + B ) = ( C + D ) )   =>    |- ( ph -> ( A - D ) = ( C - B ) )
Theorem	addlsub 8548	Left-subtraction: Subtraction of the left summand from the result of an addition. (Contributed by BJ, 6-Jun-2019.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> C e. CC )   =>    |- ( ph -> ( ( A + B ) = C <-> A = ( C - B ) ) )
Theorem	addrsub 8549	Right-subtraction: Subtraction of the right summand from the result of an addition. (Contributed by BJ, 6-Jun-2019.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> C e. CC )   =>    |- ( ph -> ( ( A + B ) = C <-> B = ( C - A ) ) )
Theorem	subexsub 8550	A subtraction law: Exchanging the subtrahend and the result of the subtraction. (Contributed by BJ, 6-Jun-2019.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> C e. CC )   =>    |- ( ph -> ( A = ( C - B ) <-> B = ( C - A ) ) )
Theorem	addid0 8551	If adding a number to a another number yields the other number, the added number must be 0. This shows that 0 is the unique (right) identity of the complex numbers. (Contributed by AV, 17-Jan-2021.)
|- ( ( X e. CC /\ Y e. CC ) -> ( ( X + Y ) = X <-> Y = 0 ) )
Theorem	addn0nid 8552	Adding a nonzero number to a complex number does not yield the complex number. (Contributed by AV, 17-Jan-2021.)
|- ( ( X e. CC /\ Y e. CC /\ Y =/= 0 ) -> ( X + Y ) =/= X )
Theorem	pnpncand 8553	Addition/subtraction cancellation law. (Contributed by Scott Fenton, 14-Dec-2017.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> C e. CC )   =>    |- ( ph -> ( ( A + ( B - C ) ) + ( C - B ) ) = A )
Theorem	subeqrev 8554	Reverse the order of subtraction in an equality. (Contributed by Scott Fenton, 8-Jul-2013.)
|- ( ( ( A e. CC /\ B e. CC ) /\ ( C e. CC /\ D e. CC ) ) -> ( ( A - B ) = ( C - D ) <-> ( B - A ) = ( D - C ) ) )
Theorem	pncan1 8555	Cancellation law for addition and subtraction with 1. (Contributed by Alexander van der Vekens, 3-Oct-2018.)
|- ( A e. CC -> ( ( A + 1 ) - 1 ) = A )
Theorem	npcan1 8556	Cancellation law for subtraction and addition with 1. (Contributed by Alexander van der Vekens, 5-Oct-2018.)
|- ( A e. CC -> ( ( A - 1 ) + 1 ) = A )
Theorem	subeq0bd 8557	If two complex numbers are equal, their difference is zero. Consequence of subeq0ad 8499. Converse of subeq0d 8497. Contrapositive of subne0ad 8500. (Contributed by David Moews, 28-Feb-2017.)
|- ( ph -> A e. CC )   &    |- ( ph -> A = B )   =>    |- ( ph -> ( A - B ) = 0 )
Theorem	renegcld 8558	Closure law for negative of reals. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. RR )   =>    |- ( ph -> -u A e. RR )
Theorem	resubcld 8559	Closure law for subtraction of reals. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   =>    |- ( ph -> ( A - B ) e. RR )
Theorem	negf1o 8560*	Negation is an isomorphism of a subset of the real numbers to the negated elements of the subset. (Contributed by AV, 9-Aug-2020.)
|- F = ( x e. A |-> -u x )   =>    |- ( A C_ RR -> F : A -1-1-onto-> { n e. RR | -u n e. A } )
4.3.3  Multiplication
Theorem	kcnktkm1cn 8561	k times k minus 1 is a complex number if k is a complex number. (Contributed by Alexander van der Vekens, 11-Mar-2018.)
|- ( K e. CC -> ( K x. ( K - 1 ) ) e. CC )
Theorem	muladd 8562	Product of two sums. (Contributed by NM, 14-Jan-2006.) (Proof shortened by Andrew Salmon, 19-Nov-2011.)
|- ( ( ( A e. CC /\ B e. CC ) /\ ( C e. CC /\ D e. CC ) ) -> ( ( A + B ) x. ( C + D ) ) = ( ( ( A x. C ) + ( D x. B ) ) + ( ( A x. D ) + ( C x. B ) ) ) )
Theorem	subdi 8563	Distribution of multiplication over subtraction. Theorem I.5 of [Apostol] p. 18. (Contributed by NM, 18-Nov-2004.)
|- ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( A x. ( B - C ) ) = ( ( A x. B ) - ( A x. C ) ) )
Theorem	subdir 8564	Distribution of multiplication over subtraction. Theorem I.5 of [Apostol] p. 18. (Contributed by NM, 30-Dec-2005.)
|- ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( ( A - B ) x. C ) = ( ( A x. C ) - ( B x. C ) ) )
Theorem	mul02 8565	Multiplication by 0. Theorem I.6 of [Apostol] p. 18. (Contributed by NM, 10-Aug-1999.)
|- ( A e. CC -> ( 0 x. A ) = 0 )
Theorem	mul02lem2 8566	Zero times a real is zero. Although we prove it as a corollary of mul02 8565, the name is for consistency with the Metamath Proof Explorer which proves it before mul02 8565. (Contributed by Scott Fenton, 3-Jan-2013.)
|- ( A e. RR -> ( 0 x. A ) = 0 )
Theorem	mul01 8567	Multiplication by 0. Theorem I.6 of [Apostol] p. 18. (Contributed by NM, 15-May-1999.) (Revised by Scott Fenton, 3-Jan-2013.)
|- ( A e. CC -> ( A x. 0 ) = 0 )
Theorem	mul02i 8568	Multiplication by 0. Theorem I.6 of [Apostol] p. 18. (Contributed by NM, 23-Nov-1994.)
|- A e. CC   =>    |- ( 0 x. A ) = 0
Theorem	mul01i 8569	Multiplication by 0. Theorem I.6 of [Apostol] p. 18. (Contributed by NM, 23-Nov-1994.) (Revised by Scott Fenton, 3-Jan-2013.)
|- A e. CC   =>    |- ( A x. 0 ) = 0
Theorem	mul02d 8570	Multiplication by 0. Theorem I.6 of [Apostol] p. 18. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. CC )   =>    |- ( ph -> ( 0 x. A ) = 0 )
Theorem	mul01d 8571	Multiplication by 0. Theorem I.6 of [Apostol] p. 18. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. CC )   =>    |- ( ph -> ( A x. 0 ) = 0 )
Theorem	ine0 8572	The imaginary unit _i is not zero. (Contributed by NM, 6-May-1999.)
|- _i =/= 0
Theorem	mulneg1 8573	Product with negative is negative of product. Theorem I.12 of [Apostol] p. 18. (Contributed by NM, 14-May-1999.) (Proof shortened by Mario Carneiro, 27-May-2016.)
|- ( ( A e. CC /\ B e. CC ) -> ( -u A x. B ) = -u ( A x. B ) )
Theorem	mulneg2 8574	The product with a negative is the negative of the product. (Contributed by NM, 30-Jul-2004.)
|- ( ( A e. CC /\ B e. CC ) -> ( A x. -u B ) = -u ( A x. B ) )
Theorem	mulneg12 8575	Swap the negative sign in a product. (Contributed by NM, 30-Jul-2004.)
|- ( ( A e. CC /\ B e. CC ) -> ( -u A x. B ) = ( A x. -u B ) )
Theorem	mul2neg 8576	Product of two negatives. Theorem I.12 of [Apostol] p. 18. (Contributed by NM, 30-Jul-2004.) (Proof shortened by Andrew Salmon, 19-Nov-2011.)
|- ( ( A e. CC /\ B e. CC ) -> ( -u A x. -u B ) = ( A x. B ) )
Theorem	submul2 8577	Convert a subtraction to addition using multiplication by a negative. (Contributed by NM, 2-Feb-2007.)
|- ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( A - ( B x. C ) ) = ( A + ( B x. -u C ) ) )
Theorem	mulm1 8578	Product with minus one is negative. (Contributed by NM, 16-Nov-1999.)
|- ( A e. CC -> ( -u 1 x. A ) = -u A )
Theorem	mulsub 8579	Product of two differences. (Contributed by NM, 14-Jan-2006.)
|- ( ( ( A e. CC /\ B e. CC ) /\ ( C e. CC /\ D e. CC ) ) -> ( ( A - B ) x. ( C - D ) ) = ( ( ( A x. C ) + ( D x. B ) ) - ( ( A x. D ) + ( C x. B ) ) ) )
Theorem	mulsub2 8580	Swap the order of subtraction in a multiplication. (Contributed by Scott Fenton, 24-Jun-2013.)
|- ( ( ( A e. CC /\ B e. CC ) /\ ( C e. CC /\ D e. CC ) ) -> ( ( A - B ) x. ( C - D ) ) = ( ( B - A ) x. ( D - C ) ) )
Theorem	mulm1i 8581	Product with minus one is negative. (Contributed by NM, 31-Jul-1999.)
|- A e. CC   =>    |- ( -u 1 x. A ) = -u A
Theorem	mulneg1i 8582	Product with negative is negative of product. Theorem I.12 of [Apostol] p. 18. (Contributed by NM, 10-Feb-1995.) (Revised by Mario Carneiro, 27-May-2016.)
|- A e. CC   &    |- B e. CC   =>    |- ( -u A x. B ) = -u ( A x. B )
Theorem	mulneg2i 8583	Product with negative is negative of product. (Contributed by NM, 31-Jul-1999.) (Revised by Mario Carneiro, 27-May-2016.)
|- A e. CC   &    |- B e. CC   =>    |- ( A x. -u B ) = -u ( A x. B )
Theorem	mul2negi 8584	Product of two negatives. Theorem I.12 of [Apostol] p. 18. (Contributed by NM, 14-Feb-1995.) (Revised by Mario Carneiro, 27-May-2016.)
|- A e. CC   &    |- B e. CC   =>    |- ( -u A x. -u B ) = ( A x. B )
Theorem	subdii 8585	Distribution of multiplication over subtraction. Theorem I.5 of [Apostol] p. 18. (Contributed by NM, 26-Nov-1994.)
|- A e. CC   &    |- B e. CC   &    |- C e. CC   =>    |- ( A x. ( B - C ) ) = ( ( A x. B ) - ( A x. C ) )
Theorem	subdiri 8586	Distribution of multiplication over subtraction. Theorem I.5 of [Apostol] p. 18. (Contributed by NM, 8-May-1999.)
|- A e. CC   &    |- B e. CC   &    |- C e. CC   =>    |- ( ( A - B ) x. C ) = ( ( A x. C ) - ( B x. C ) )
Theorem	muladdi 8587	Product of two sums. (Contributed by NM, 17-May-1999.)
|- A e. CC   &    |- B e. CC   &    |- C e. CC   &    |- D e. CC   =>    |- ( ( A + B ) x. ( C + D ) ) = ( ( ( A x. C ) + ( D x. B ) ) + ( ( A x. D ) + ( C x. B ) ) )
Theorem	mulm1d 8588	Product with minus one is negative. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. CC )   =>    |- ( ph -> ( -u 1 x. A ) = -u A )
Theorem	mulneg1d 8589	Product with negative is negative of product. Theorem I.12 of [Apostol] p. 18. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   =>    |- ( ph -> ( -u A x. B ) = -u ( A x. B ) )
Theorem	mulneg2d 8590	Product with negative is negative of product. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   =>    |- ( ph -> ( A x. -u B ) = -u ( A x. B ) )
Theorem	mul2negd 8591	Product of two negatives. Theorem I.12 of [Apostol] p. 18. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   =>    |- ( ph -> ( -u A x. -u B ) = ( A x. B ) )
Theorem	subdid 8592	Distribution of multiplication over subtraction. Theorem I.5 of [Apostol] p. 18. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> C e. CC )   =>    |- ( ph -> ( A x. ( B - C ) ) = ( ( A x. B ) - ( A x. C ) ) )
Theorem	subdird 8593	Distribution of multiplication over subtraction. Theorem I.5 of [Apostol] p. 18. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> C e. CC )   =>    |- ( ph -> ( ( A - B ) x. C ) = ( ( A x. C ) - ( B x. C ) ) )
Theorem	muladdd 8594	Product of two sums. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> C e. CC )   &    |- ( ph -> D e. CC )   =>    |- ( ph -> ( ( A + B ) x. ( C + D ) ) = ( ( ( A x. C ) + ( D x. B ) ) + ( ( A x. D ) + ( C x. B ) ) ) )
Theorem	mulsubd 8595	Product of two differences. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> C e. CC )   &    |- ( ph -> D e. CC )   =>    |- ( ph -> ( ( A - B ) x. ( C - D ) ) = ( ( ( A x. C ) + ( D x. B ) ) - ( ( A x. D ) + ( C x. B ) ) ) )
Theorem	muls1d 8596	Multiplication by one minus a number. (Contributed by Scott Fenton, 23-Dec-2017.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   =>    |- ( ph -> ( A x. ( B - 1 ) ) = ( ( A x. B ) - A ) )
Theorem	mulsubfacd 8597	Multiplication followed by the subtraction of a factor. (Contributed by Alexander van der Vekens, 28-Aug-2018.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   =>    |- ( ph -> ( ( A x. B ) - B ) = ( ( A - 1 ) x. B ) )
4.3.4  Ordering on reals (cont.)
Theorem	ltadd2 8598	Addition to both sides of 'less than'. (Contributed by NM, 12-Nov-1999.) (Revised by Mario Carneiro, 27-May-2016.)
|- ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( A < B <-> ( C + A ) < ( C + B ) ) )
Theorem	ltadd2i 8599	Addition to both sides of 'less than'. (Contributed by NM, 21-Jan-1997.)
|- A e. RR   &    |- B e. RR   &    |- C e. RR   =>    |- ( A < B <-> ( C + A ) < ( C + B ) )
Theorem	ltadd2d 8600	Addition to both sides of 'less than'. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> C e. RR )   =>    |- ( ph -> ( A < B <-> ( C + A ) < ( C + B ) ) )