Theorem negsub 11439

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	⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 + -𝐵) = (𝐴 − 𝐵))

Proof of Theorem negsub

Step	Hyp	Ref	Expression
1		df-neg 11377	. . . 4 ⊢ -𝐵 = (0 − 𝐵)
2	1	oveq2i 7375	. . 3 ⊢ (𝐴 + -𝐵) = (𝐴 + (0 − 𝐵))
3	2	a1i 11	. 2 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 + -𝐵) = (𝐴 + (0 − 𝐵)))
4		0cn 11133	. . 3 ⊢ 0 ∈ ℂ
5		addsubass 11400	. . 3 ⊢ ((𝐴 ∈ ℂ ∧ 0 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 + 0) − 𝐵) = (𝐴 + (0 − 𝐵)))
6	4, 5	mp3an2 1452	. 2 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 + 0) − 𝐵) = (𝐴 + (0 − 𝐵)))
7		simpl 482	. . . 4 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → 𝐴 ∈ ℂ)
8	7	addridd 11343	. . 3 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 + 0) = 𝐴)
9	8	oveq1d 7379	. 2 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 + 0) − 𝐵) = (𝐴 − 𝐵))
10	3, 6, 9	3eqtr2d 2778	1 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 + -𝐵) = (𝐴 − 𝐵))

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1542   ∈ wcel 2114  (class class class)co 7364  ℂcc 11033  0cc0 11035   + caddc 11038   − cmin 11374  -cneg 11375

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5232  ax-nul 5242  ax-pow 5306  ax-pr 5374  ax-un 7686  ax-resscn 11092  ax-1cn 11093  ax-icn 11094  ax-addcl 11095  ax-addrcl 11096  ax-mulcl 11097  ax-mulrcl 11098  ax-mulcom 11099  ax-addass 11100  ax-mulass 11101  ax-distr 11102  ax-i2m1 11103  ax-1ne0 11104  ax-1rid 11105  ax-rnegex 11106  ax-rrecex 11107  ax-cnre 11108  ax-pre-lttri 11109  ax-pre-lttrn 11110  ax-pre-ltadd 11111

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-nel 3038  df-ral 3053  df-rex 3063  df-reu 3344  df-rab 3391  df-v 3432  df-sbc 3730  df-csb 3839  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-pw 4544  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-br 5087  df-opab 5149  df-mpt 5168  df-id 5523  df-po 5536  df-so 5537  df-xp 5634  df-rel 5635  df-cnv 5636  df-co 5637  df-dm 5638  df-rn 5639  df-res 5640  df-ima 5641  df-iota 6452  df-fun 6498  df-fn 6499  df-f 6500  df-f1 6501  df-fo 6502  df-f1o 6503  df-fv 6504  df-riota 7321  df-ov 7367  df-oprab 7368  df-mpo 7369  df-er 8640  df-en 8891  df-dom 8892  df-sdom 8893  df-pnf 11178  df-mnf 11179  df-ltxr 11181  df-sub 11376  df-neg 11377

This theorem is referenced by:  negdi2  11449  negsubdi2  11450  resubcli  11453  resubcl  11455  negsubi  11469  negsubd  11508  submul2  11587  addneg1mul  11589  mulsub  11590  divsubdir  11845  difgtsumgt  12487  elz2  12539  zsubcl  12566  qsubcl  12915  rexsub  13182  fzsubel  13511  ceim1l  13803  modcyc2  13863  negmod  13875  modsumfzodifsn  13903  expsub  14069  binom2sub  14179  seqshft  15044  resub  15086  imsub  15094  cjsub  15108  cjreim  15119  absdiflt  15277  absdifle  15278  abs2dif2  15293  subcn2  15554  bpoly2  16019  bpoly3  16020  efsub  16064  efi4p  16101  sinsub  16132  cossub  16133  demoivreALT  16165  difmod0  16253  dvdssub  16270  modgcd  16498  gzsubcl  16908  psgnunilem2  19467  cnfldsub  21393  itg1sub  25692  plyremlem  26287  sineq0  26507  logneg2  26598  ang180lem2  26793  asinsin  26875  atanneg  26890  atancj  26893  atanlogadd  26897  atanlogsublem  26898  atanlogsub  26899  2efiatan  26901  tanatan  26902  cosatan  26904  atans2  26914  dvatan  26918  zetacvg  26998  wilthlem1  27051  wilthlem2  27052  basellem8  27071  lgsvalmod  27299  cnnvm  30774  cncph  30911  hvsubdistr2  31142  lnfnsubi  32138  subfacval2  35391  itg2addnclem3  38016  lcmineqlem1  42490  pellexlem6  43288  pell14qrdich  43323  rmxm1  43388  rmym1  43389  addsubeq0  47764  omoeALTV  48181  omeoALTV  48182  emoo  48200  emee  48202  zlmodzxzequap  48995  flsubz  49018