Theorem negsub 7793

Description: Relationship between subtraction and negative. Theorem I.3 of [Apostol] p. 18. (Contributed by NM, 21-Jan-1997.) (Proof shortened by Mario Carneiro, 27-May-2016.)

Assertion

Ref	Expression
negsub	|- ( ( A e. CC /\ B e. CC ) -> ( A + -u B ) = ( A - B ) )

Proof of Theorem negsub

Step	Hyp	Ref	Expression
1		df-neg 7719	. . . 4 |- -u B = ( 0 - B )
2	1	oveq2i 5679	. . 3 |- ( A + -u B ) = ( A + ( 0 - B ) )
3	2	a1i 9	. 2 |- ( ( A e. CC /\ B e. CC ) -> ( A + -u B ) = ( A + ( 0 - B ) ) )
4		0cn 7543	. . 3 |- 0 e. CC
5		addsubass 7755	. . 3 |- ( ( A e. CC /\ 0 e. CC /\ B e. CC ) -> ( ( A + 0 ) - B ) = ( A + ( 0 - B ) ) )
6	4, 5	mp3an2 1262	. 2 |- ( ( A e. CC /\ B e. CC ) -> ( ( A + 0 ) - B ) = ( A + ( 0 - B ) ) )
7		simpl 108	. . . 4 |- ( ( A e. CC /\ B e. CC ) -> A e. CC )
8	7	addid1d 7694	. . 3 |- ( ( A e. CC /\ B e. CC ) -> ( A + 0 ) = A )
9	8	oveq1d 5683	. 2 |- ( ( A e. CC /\ B e. CC ) -> ( ( A + 0 ) - B ) = ( A - B ) )
10	3, 6, 9	3eqtr2d 2127	1 |- ( ( A e. CC /\ B e. CC ) -> ( A + -u B ) = ( A - B ) )

Syntax hints:   -> wi 4   /\ wa 103   = wceq 1290   e. wcel 1439  (class class class)co 5668   CCcc 7411   0cc0 7413   + caddc 7416   - cmin 7716   -ucneg 7717

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 580  ax-in2 581  ax-io 666  ax-5 1382  ax-7 1383  ax-gen 1384  ax-ie1 1428  ax-ie2 1429  ax-8 1441  ax-10 1442  ax-11 1443  ax-i12 1444  ax-bndl 1445  ax-4 1446  ax-14 1451  ax-17 1465  ax-i9 1469  ax-ial 1473  ax-i5r 1474  ax-ext 2071  ax-sep 3965  ax-pow 4017  ax-pr 4047  ax-setind 4368  ax-resscn 7500  ax-1cn 7501  ax-icn 7503  ax-addcl 7504  ax-addrcl 7505  ax-mulcl 7506  ax-addcom 7508  ax-addass 7510  ax-distr 7512  ax-i2m1 7513  ax-0id 7516  ax-rnegex 7517  ax-cnre 7519

This theorem depends on definitions:  df-bi 116  df-3an 927  df-tru 1293  df-fal 1296  df-nf 1396  df-sb 1694  df-eu 1952  df-mo 1953  df-clab 2076  df-cleq 2082  df-clel 2085  df-nfc 2218  df-ne 2257  df-ral 2365  df-rex 2366  df-reu 2367  df-rab 2369  df-v 2624  df-sbc 2844  df-dif 3004  df-un 3006  df-in 3008  df-ss 3015  df-pw 3437  df-sn 3458  df-pr 3459  df-op 3461  df-uni 3662  df-br 3854  df-opab 3908  df-id 4131  df-xp 4460  df-rel 4461  df-cnv 4462  df-co 4463  df-dm 4464  df-iota 4995  df-fun 5032  df-fv 5038  df-riota 5624  df-ov 5671  df-oprab 5672  df-mpt2 5673  df-sub 7718  df-neg 7719

This theorem is referenced by:  negdi2  7803  negsubdi2  7804  resubcli  7808  resubcl  7809  negsubi  7823  negsubd  7862  submul2  7940  mulsub  7942  subap0  8181  divsubdirap  8238  zsubcl  8854  elz2  8881  qsubcl  9186  fzsubel  9537  expsubap  10066  binom2sub  10130  resub  10367  imsub  10375  cjsub  10389  cjreim  10400  absdiflt  10588  absdifle  10589  abs2dif2  10603  subcn2  10763  efsub  11034  efi4p  11071  sinsub  11094  cossub  11095  demoivreALT  11126  dvdssub  11182  modgcd  11323