P. 74 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 7301-7400   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	subsub23i 7301	Swap subtrahend and result of subtraction. (Contributed by NM, 7-Oct-1999.)
|- A e. CC   &    |- B e. CC   &    |- C e. CC   =>    |- ( ( A - B ) = C <-> ( A - C ) = B )
Theorem	addsubassi 7302	Associative-type law for subtraction and addition. (Contributed by NM, 16-Sep-1999.)
|- A e. CC   &    |- B e. CC   &    |- C e. CC   =>    |- ( ( A + B ) - C ) = ( A + ( B - C ) )
Theorem	addsubi 7303	Law for subtraction and addition. (Contributed by NM, 6-Aug-2003.)
|- A e. CC   &    |- B e. CC   &    |- C e. CC   =>    |- ( ( A + B ) - C ) = ( ( A - C ) + B )
Theorem	subcani 7304	Cancellation law for subtraction. (Contributed by NM, 8-Feb-2005.)
|- A e. CC   &    |- B e. CC   &    |- C e. CC   =>    |- ( ( A - B ) = ( A - C ) <-> B = C )
Theorem	subcan2i 7305	Cancellation law for subtraction. (Contributed by NM, 8-Feb-2005.)
|- A e. CC   &    |- B e. CC   &    |- C e. CC   =>    |- ( ( A - C ) = ( B - C ) <-> A = B )
Theorem	pnncani 7306	Cancellation law for mixed addition and subtraction. (Contributed by NM, 14-Jan-2006.)
|- A e. CC   &    |- B e. CC   &    |- C e. CC   =>    |- ( ( A + B ) - ( A - C ) ) = ( B + C )
Theorem	addsub4i 7307	Rearrangement of 4 terms in a mixed addition and subtraction. (Contributed by NM, 17-Oct-1999.)
|- A e. CC   &    |- B e. CC   &    |- C e. CC   &    |- D e. CC   =>    |- ( ( A + B ) - ( C + D ) ) = ( ( A - C ) + ( B - D ) )
Theorem	0reALT 7308	Alternate proof of 0re 7027. (Contributed by NM, 19-Feb-2005.) (Proof modification is discouraged.) (New usage is discouraged.)
|- 0 e. RR
Theorem	negcld 7309	Closure law for negative. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. CC )   =>    |- ( ph -> -u A e. CC )
Theorem	subidd 7310	Subtraction of a number from itself. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. CC )   =>    |- ( ph -> ( A - A ) = 0 )
Theorem	subid1d 7311	Identity law for subtraction. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. CC )   =>    |- ( ph -> ( A - 0 ) = A )
Theorem	negidd 7312	Addition of a number and its negative. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. CC )   =>    |- ( ph -> ( A + -u A ) = 0 )
Theorem	negnegd 7313	A number is equal to the negative of its negative. Theorem I.4 of [Apostol] p. 18. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. CC )   =>    |- ( ph -> -u -u A = A )
Theorem	negeq0d 7314	A number is zero iff its negative is zero. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. CC )   =>    |- ( ph -> ( A = 0 <-> -u A = 0 ) )
Theorem	negne0bd 7315	A number is nonzero iff its negative is nonzero. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. CC )   =>    |- ( ph -> ( A =/= 0 <-> -u A =/= 0 ) )
Theorem	negcon1d 7316	Contraposition law for unary minus. Deduction form of negcon1 7263. (Contributed by David Moews, 28-Feb-2017.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   =>    |- ( ph -> ( -u A = B <-> -u B = A ) )
Theorem	negcon1ad 7317	Contraposition law for unary minus. One-way deduction form of negcon1 7263. (Contributed by David Moews, 28-Feb-2017.)
|- ( ph -> A e. CC )   &    |- ( ph -> -u A = B )   =>    |- ( ph -> -u B = A )
Theorem	neg11ad 7318	The negatives of two complex numbers are equal iff they are equal. Deduction form of neg11 7262. Generalization of neg11d 7334. (Contributed by David Moews, 28-Feb-2017.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   =>    |- ( ph -> ( -u A = -u B <-> A = B ) )
Theorem	negned 7319	If two complex numbers are unequal, so are their negatives. Contrapositive of neg11d 7334. (Contributed by David Moews, 28-Feb-2017.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> A =/= B )   =>    |- ( ph -> -u A =/= -u B )
Theorem	negne0d 7320	The negative of a nonzero number is nonzero. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. CC )   &    |- ( ph -> A =/= 0 )   =>    |- ( ph -> -u A =/= 0 )
Theorem	negrebd 7321	The negative of a real is real. (Contributed by Mario Carneiro, 28-May-2016.)
|- ( ph -> A e. CC )   &    |- ( ph -> -u A e. RR )   =>    |- ( ph -> A e. RR )
Theorem	subcld 7322	Closure law for subtraction. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   =>    |- ( ph -> ( A - B ) e. CC )
Theorem	pncand 7323	Cancellation law for subtraction. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   =>    |- ( ph -> ( ( A + B ) - B ) = A )
Theorem	pncan2d 7324	Cancellation law for subtraction. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   =>    |- ( ph -> ( ( A + B ) - A ) = B )
Theorem	pncan3d 7325	Subtraction and addition of equals. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   =>    |- ( ph -> ( A + ( B - A ) ) = B )
Theorem	npcand 7326	Cancellation law for subtraction. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   =>    |- ( ph -> ( ( A - B ) + B ) = A )
Theorem	nncand 7327	Cancellation law for subtraction. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   =>    |- ( ph -> ( A - ( A - B ) ) = B )
Theorem	negsubd 7328	Relationship between subtraction and negative. Theorem I.3 of [Apostol] p. 18. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   =>    |- ( ph -> ( A + -u B ) = ( A - B ) )
Theorem	subnegd 7329	Relationship between subtraction and negative. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   =>    |- ( ph -> ( A - -u B ) = ( A + B ) )
Theorem	subeq0d 7330	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 -> ( A - B ) = 0 )   =>    |- ( ph -> A = B )
Theorem	subne0d 7331	Two unequal numbers have nonzero difference. See also subap0d 7631 which is the same thing for apartness rather than negated equality. (Contributed by Mario Carneiro, 1-Jan-2017.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> A =/= B )   =>    |- ( ph -> ( A - B ) =/= 0 )
Theorem	subeq0ad 7332	The difference of two complex numbers is zero iff they are equal. Deduction form of subeq0 7237. Generalization of subeq0d 7330. (Contributed by David Moews, 28-Feb-2017.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   =>    |- ( ph -> ( ( A - B ) = 0 <-> A = B ) )
Theorem	subne0ad 7333	If the difference of two complex numbers is nonzero, they are unequal. Converse of subne0d 7331. Contrapositive of subeq0bd 7377. (Contributed by David Moews, 28-Feb-2017.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> ( A - B ) =/= 0 )   =>    |- ( ph -> A =/= B )
Theorem	neg11d 7334	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 7335	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 7336	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 7337	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 7338	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 7339	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 7340	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 7341	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 7342	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 7343	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 7344	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 7345	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 7346	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 7347	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 7348	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 7349	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 7350	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 7351	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 7352	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 7353	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 7354	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 7355	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 7356	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 7357	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 7358	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 7359	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 7360	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 7361	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 7362	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 7363	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 7364	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 7365	Cancellation law for subtraction. Deduction form of subcan 7266. Generalization of subcand 7363. (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 7366	Introducing subtraction on both sides of a statement of inequality. Contrapositive of subcand 7363. (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 7367	Cancellation law for subtraction. Deduction form of subcan2 7236. Generalization of subcan2d 7364. (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 7368	Introducing subtraction on both sides of a statement of inequality. Contrapositive of subcan2d 7364. (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 7369	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 7370	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 7371	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 7372	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 7373	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	subeqrev 7374	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 7375	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 7376	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 7377	If two complex numbers are equal, their difference is zero. Consequence of subeq0ad 7332. Converse of subeq0d 7330. Contrapositive of subne0ad 7333. (Contributed by David Moews, 28-Feb-2017.)
|- ( ph -> A e. CC )   &    |- ( ph -> A = B )   =>    |- ( ph -> ( A - B ) = 0 )
Theorem	renegcld 7378	Closure law for negative of reals. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. RR )   =>    |- ( ph -> -u A e. RR )
Theorem	resubcld 7379	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 )
3.3.3  Multiplication
Theorem	kcnktkm1cn 7380	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 7381	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 7382	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 7383	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 7384	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 7385	Zero times a real is zero. Although we prove it as a corollary of mul02 7384, the name is for consistency with the Metamath Proof Explorer which proves it before mul02 7384. (Contributed by Scott Fenton, 3-Jan-2013.)
|- ( A e. RR -> ( 0 x. A ) = 0 )
Theorem	mul01 7386	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 7387	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 7388	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 7389	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 7390	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 7391	The imaginary unit _i is not zero. (Contributed by NM, 6-May-1999.)
|- _i =/= 0
Theorem	mulneg1 7392	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 7393	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 7394	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 7395	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 7396	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 7397	Product with minus one is negative. (Contributed by NM, 16-Nov-1999.)
|- ( A e. CC -> ( -u 1 x. A ) = -u A )
Theorem	mulsub 7398	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 7399	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 7400	Product with minus one is negative. (Contributed by NM, 31-Jul-1999.)
|- A e. CC   =>    |- ( -u 1 x. A ) = -u A