Theorem subcld 8627

Description: Closure law for subtraction. (Contributed by Mario Carneiro, 27-May-2016.)

Hypotheses

Ref	Expression
negidd.1	⊢ (𝜑 → 𝐴 ∈ ℂ)
pncand.2	⊢ (𝜑 → 𝐵 ∈ ℂ)

Assertion

Ref	Expression
subcld	⊢ (𝜑 → (𝐴 − 𝐵) ∈ ℂ)

Proof of Theorem subcld

Step	Hyp	Ref	Expression
1		negidd.1	. 2 ⊢ (𝜑 → 𝐴 ∈ ℂ)
2		pncand.2	. 2 ⊢ (𝜑 → 𝐵 ∈ ℂ)
3		subcl 8515	. 2 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 − 𝐵) ∈ ℂ)
4	1, 2, 3	syl2anc 415	1 ⊢ (𝜑 → (𝐴 − 𝐵) ∈ ℂ)

Syntax hints:   → wi 4   ∈ wcel 2209  (class class class)co 6075  ℂcc 8167   − cmin 8487

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 623  ax-in2 624  ax-io 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-14 2212  ax-ext 2220  ax-sep 4244  ax-pow 4306  ax-pr 4341  ax-setind 4679  ax-resscn 8261  ax-1cn 8262  ax-icn 8264  ax-addcl 8265  ax-addrcl 8266  ax-mulcl 8267  ax-addcom 8269  ax-addass 8271  ax-distr 8273  ax-i2m1 8274  ax-0id 8277  ax-rnegex 8278  ax-cnre 8280

This theorem depends on definitions:  df-bi 117  df-3an 1011  df-tru 1405  df-fal 1408  df-nf 1514  df-sb 1816  df-eu 2089  df-mo 2090  df-clab 2225  df-cleq 2231  df-clel 2234  df-nfc 2381  df-ne 2421  df-ral 2533  df-rex 2534  df-reu 2535  df-rab 2537  df-v 2823  df-sbc 3052  df-dif 3222  df-un 3224  df-in 3226  df-ss 3233  df-pw 3687  df-sn 3711  df-pr 3712  df-op 3714  df-uni 3931  df-br 4126  df-opab 4188  df-id 4433  df-xp 4775  df-rel 4776  df-cnv 4777  df-co 4778  df-dm 4779  df-iota 5332  df-fun 5374  df-fv 5380  df-riota 6028  df-ov 6078  df-oprab 6079  df-mpo 6080  df-sub 8489

This theorem is referenced by:  pnpncand  8691  kcnktkm1cn  8700  muleqadd  8988  ofnegsub  9282  peano2zm  9661  peano5uzti  9733  modqmuladdnn0  10783  modsumfzodifsn  10811  bcm1n  11185  hashfz  11240  hashfzo  11241  hashf1lem2  11264  hashf1  11265  ccatswrd  11420  pfxccatin12lem2  11481  shftfvalg  11561  ovshftex  11562  shftfibg  11563  shftfval  11564  shftdm  11565  shftfib  11566  shftval  11568  2shfti  11574  crre  11600  remim  11603  remullem  11614  resqrexlemover  11754  resqrexlemcalc1  11758  abssubne0  11835  abs3lem  11855  caubnd2  11861  maxabslemlub  11951  maxabslemval  11952  maxcl  11954  minabs  11980  bdtrilem  11983  bdtri  11984  climuni  12037  mulcn2  12056  reccn2ap  12057  cn1lem  12058  climcvg1nlem  12093  fsumparts  12215  arisum2  12244  geosergap  12251  geo2sum2  12260  geoisum1c  12265  cvgratnnlemrate  12275  sinval  12447  sinf  12449  tanval2ap  12458  tanval3ap  12459  sinneg  12471  efival  12477  cos12dec  12513  bitsinv1lem  12706  pythagtriplem1  13022  pythagtriplem14  13034  pythagtriplem16  13036  pythagtriplem17  13037  dvdsprmpweqle  13094  4sqlem5  13139  mul4sqlem  13150  4sqlem17  13164  gzsumshift  14126  addcncntoplem  15585  mulcncflem  15631  cnopnap  15635  limcimolemlt  15688  limcimo  15689  cnplimclemle  15692  limccnp2lem  15700  dvlemap  15704  dvconst  15718  dvid  15719  dvconstre  15720  dvidre  15721  dvconstss  15722  dvcnp2cntop  15723  dvaddxxbr  15725  dvmulxxbr  15726  dvcoapbr  15731  dvcjbr  15732  dvrecap  15737  dveflem  15750  dvef  15751  sin0pilem1  15805  ptolemy  15848  tangtx  15862  cosq34lt1  15874  pellexlem2  16006  lgsdirprm  16067  gausslemma2dlem1a  16091  clwwlknonex2lem1  16592  dichmul0orlem7  16673  qdencn  16977  trirec0  16998  apdifflemf  17000  apdifflemr  17001  apdiff  17002  qdiff  17003