Theorem subcld 11647

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 11535	. 2 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 − 𝐵) ∈ ℂ)
4	1, 2, 3	syl2anc 583	1 ⊢ (𝜑 → (𝐴 − 𝐵) ∈ ℂ)

Syntax hints:   → wi 4   ∈ wcel 2108  (class class class)co 7448  ℂcc 11182   − cmin 11520

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2158  ax-12 2178  ax-ext 2711  ax-sep 5317  ax-nul 5324  ax-pow 5383  ax-pr 5447  ax-un 7770  ax-resscn 11241  ax-1cn 11242  ax-icn 11243  ax-addcl 11244  ax-addrcl 11245  ax-mulcl 11246  ax-mulrcl 11247  ax-mulcom 11248  ax-addass 11249  ax-mulass 11250  ax-distr 11251  ax-i2m1 11252  ax-1ne0 11253  ax-1rid 11254  ax-rnegex 11255  ax-rrecex 11256  ax-cnre 11257  ax-pre-lttri 11258  ax-pre-lttrn 11259  ax-pre-ltadd 11260

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3or 1088  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-nf 1782  df-sb 2065  df-mo 2543  df-eu 2572  df-clab 2718  df-cleq 2732  df-clel 2819  df-nfc 2895  df-ne 2947  df-nel 3053  df-ral 3068  df-rex 3077  df-reu 3389  df-rab 3444  df-v 3490  df-sbc 3805  df-csb 3922  df-dif 3979  df-un 3981  df-in 3983  df-ss 3993  df-nul 4353  df-if 4549  df-pw 4624  df-sn 4649  df-pr 4651  df-op 4655  df-uni 4932  df-br 5167  df-opab 5229  df-mpt 5250  df-id 5593  df-po 5607  df-so 5608  df-xp 5706  df-rel 5707  df-cnv 5708  df-co 5709  df-dm 5710  df-rn 5711  df-res 5712  df-ima 5713  df-iota 6525  df-fun 6575  df-fn 6576  df-f 6577  df-f1 6578  df-fo 6579  df-f1o 6580  df-fv 6581  df-riota 7404  df-ov 7451  df-oprab 7452  df-mpo 7453  df-er 8763  df-en 9004  df-dom 9005  df-sdom 9006  df-pnf 11326  df-mnf 11327  df-ltxr 11329  df-sub 11522

This theorem is referenced by:  pnpncand  11711  muleqadd  11934  lineq  12131  modmuladdnn0  13966  hashfz  14476  hashfzo  14478  hashf1lem2  14505  hashf1  14506  ccatswrd  14716  pfxccatin12lem2  14779  crre  15163  remim  15166  remullem  15177  abs3lem  15387  caubnd2  15406  bhmafibid1cn  15512  bhmafibid2cn  15513  bhmafibid2  15515  rlimuni  15596  climuni  15598  rlimcld2  15624  rlimrege0  15625  rlimrecl  15626  mulcn2  15642  reccn2  15643  cn1lem  15644  o1sub  15662  rlimo1  15663  o1dif  15676  rlimsqzlem  15697  caucvgrlem2  15723  iseralt  15733  fsumparts  15854  cvgcmpce  15866  incexclem  15884  arisum2  15909  geoserg  15914  pwdif  15916  geo2sum2  15922  fallfacfwd  16084  binomfallfaclem2  16088  bpolycl  16100  bpoly3  16106  bpoly4  16107  fsumcube  16108  sinf  16172  tanval2  16181  tanval3  16182  sinneg  16194  efival  16200  sinhval  16202  bitsinv1lem  16487  bitsres  16519  pythagtriplem1  16863  pythagtriplem14  16875  pythagtriplem17  16878  dvdsprmpweqle  16933  4sqlem5  16989  mul4sqlem  17000  4sqlem17  17008  vdwlem5  17032  vdwlem6  17033  vdwlem8  17035  blcvx  24839  recld2  24855  addcnlem  24905  cnllycmp  25007  cphipval2  25294  4cphipval2  25295  cphipval  25296  ipcnlem2  25297  rrxmval  25458  rrxmetlem  25460  pjthlem1  25490  ovollb2lem  25542  itgcnlem  25845  dvlem  25951  dvconst  25972  dvid  25973  dvcnp2  25975  dvcnp2OLD  25976  dvaddbr  25994  dvmulbr  25995  dvmulbrOLD  25996  dvcobr  26003  dvcobrOLD  26004  dvcjbr  26007  dvrec  26013  dvmptim  26028  dvcnvlem  26034  dveflem  26037  dvsincos  26039  cmvth  26049  cmvthOLD  26050  dvlip  26052  dvlipcn  26053  c1liplem1  26055  dveq0  26059  dv11cn  26060  dvle  26066  lhop1lem  26072  dvfsumabs  26083  dvfsumlem1  26086  dvfsumlem2  26087  dvfsumlem2OLD  26088  dvfsumrlim  26092  dvfsumrlim2  26093  ftc1lem4  26100  ftc1lem5  26101  ftc2  26105  dgrcolem2  26334  plydiveu  26358  aaliou2b  26401  taylfvallem1  26416  taylply2  26427  taylply2OLD  26428  dvtaylp  26430  dvntaylp  26431  taylthlem1  26433  taylthlem2  26434  taylthlem2OLD  26435  ulmbdd  26459  ulmcn  26460  ulmdvlem1  26461  mtest  26465  iblulm  26468  itgulm  26469  abelthlem9  26502  ptolemy  26556  tangtx  26565  sineq0  26584  efeq1  26588  efif1olem4  26605  tanarg  26679  logcnlem3  26704  logcnlem4  26705  advlogexp  26715  efopn  26718  cxpcn3lem  26808  cxpeq  26818  ang180lem4  26873  ang180lem5  26874  ang180  26875  isosctrlem2  26880  isosctrlem3  26881  isosctr  26882  ssscongptld  26883  affineequiv  26884  affineequiv2  26885  affineequiv3  26886  affineequiv4  26887  affineequivne  26888  angpieqvdlem  26889  angpieqvdlem2  26890  angpined  26891  angpieqvd  26892  chordthmlem  26893  chordthmlem2  26894  chordthmlem3  26895  chordthmlem4  26896  chordthmlem5  26897  heron  26899  quad2  26900  quad  26901  dcubic1lem  26904  dcubic  26907  mcubic  26908  cubic2  26909  cubic  26910  dquartlem1  26912  dquartlem2  26913  dquart  26914  quart1cl  26915  quart1lem  26916  quart1  26917  quartlem2  26919  quartlem4  26921  quart  26922  atanf  26941  sinasin  26950  asinsin  26953  atanneg  26968  atancj  26971  efiatan  26973  atanlogsub  26977  efiatan2  26978  2efiatan  26979  atanbndlem  26986  dvatan  26996  atantayl  26998  lgamgulmlem2  27091  lgamgulmlem3  27092  lgamgulmlem5  27094  lgamgulmlem6  27095  lgamgulm2  27097  lgamucov  27099  lgamcvg2  27116  gamcvg  27117  gamcvg2lem  27120  ftalem2  27135  logfacrlim  27286  logexprlim  27287  lgsdirprm  27393  gausslemma2dlem1a  27427  gausslemma2dlem4  27431  2sqmod  27498  addsq2nreurex  27506  vmadivsum  27544  rpvmasumlem  27549  dchrisumlem2  27552  dchrisumlem3  27553  dchrmusum2  27556  dchrvmasumlem2  27560  dchrvmasumlem3  27561  dchrvmasumiflem1  27563  rpvmasum2  27574  dchrisum0lem1b  27577  dchrisum0lem1  27578  dchrisum0lem2a  27579  rplogsum  27589  mudivsum  27592  mulogsumlem  27593  mulogsum  27594  mulog2sumlem1  27596  mulog2sumlem2  27597  mulog2sumlem3  27598  vmalogdivsum2  27600  vmalogdivsum  27601  2vmadivsumlem  27602  selberglem1  27607  selberglem2  27608  selberg2lem  27612  selberg2  27613  selberg3lem1  27619  selberg4lem1  27622  selberg4  27623  pntrsumo1  27627  selberg3r  27631  selberg34r  27633  pntrlog2bndlem1  27639  pntrlog2bndlem2  27640  pntrlog2bndlem3  27641  pntrlog2bndlem4  27642  pntrlog2bndlem5  27643  pntibndlem2  27653  pntlemf  27667  pntlemo  27669  ttgcontlem1  28917  brbtwn2  28938  colinearalglem1  28939  colinearalglem2  28940  colinearalg  28943  axsegconlem1  28950  ax5seglem1  28961  ax5seglem2  28962  ax5seglem6  28967  ax5seglem9  28970  axlowdimlem17  28991  axcontlem7  29003  axcontlem8  29004  clwlkclwwlk  30034  clwwlknonex2lem1  30139  2clwwlk2clwwlk  30382  numclwwlk3lem1  30414  smcnlem  30729  ipval2  30739  4ipval2  30740  dipcj  30746  pjhthlem1  31423  submuladdd  32753  quad3d  32757  lt2addrd  32758  bcm1n  32800  cycpmco2lem5  33123  cycpmco2lem6  33124  constrrtll  33722  constrrtlc1  33723  constrrtcclem  33725  constrrtcc  33726  constrsslem  33731  constrconj  33735  constrfin  33736  constrelextdg2  33737  sqsscirc2  33855  signslema  34539  circlemeth  34617  logdivsqrle  34627  revpfxsfxrev  35083  revwlk  35092  subfaclim  35156  divcnvlin  35695  iprodgam  35704  dnicld1  36438  dnibndlem2  36445  dnibndlem3  36446  dnibndlem6  36449  dnibndlem9  36452  dnibndlem10  36453  dnibndlem11  36454  unblimceq0  36473  unbdqndv2lem1  36475  unbdqndv2lem2  36476  knoppndvlem11  36488  knoppndvlem15  36492  knoppndvlem17  36494  knoppndvlem21  36498  bj-bary1lem  37276  bj-bary1lem1  37277  bj-bary1  37278  ftc1cnnclem  37651  ftc1anclem7  37659  ftc1anclem8  37660  ftc1anc  37661  ftc2nc  37662  areacirclem1  37668  areacirclem4  37671  areacirc  37673  cntotbnd  37756  lcmineqlem8  41993  lcmineqlem10  41995  lcmineqlem11  41996  lcmineqlem12  41997  lcmineqlem23  42008  aks4d1p1  42033  aks6d1c5lem1  42093  sticksstones10  42112  sticksstones12a  42114  sticksstones12  42115  sticksstones22  42125  bcle2d  42136  metakunt15  42176  metakunt16  42177  metakunt29  42190  metakunt30  42191  mvrrsubd  42263  lsubrotld  42266  lsubswap23d  42268  nicomachus  42300  sumcubes  42301  ef11d  42327  tanhalfpim  42337  dffltz  42589  fltnltalem  42617  rencldnfilem  42776  pellexlem2  42786  pellexlem6  42790  pell1234qrne0  42809  pell1234qrmulcl  42811  rmyluc  42894  jm2.18  42945  jm2.19  42950  areaquad  43177  lhe4.4ex1a  44298  bcc0  44309  bccp1k  44310  bccm1k  44311  binomcxplemwb  44317  binomcxplemnn0  44318  binomcxplemrat  44319  binomcxplemfrat  44320  binomcxplemdvbinom  44322  binomcxplemnotnn0  44325  isosctrlem1ALT  44905  sineq0ALT  44908  oddfl  45192  dstregt0  45196  subadd4b  45197  sub31  45205  fzisoeu  45215  absnpncan2d  45217  absnpncan3d  45222  supxrgelem  45252  absimlere  45395  cvgcaule  45407  mullimc  45537  ellimcabssub0  45538  mullimcf  45544  limcrecl  45550  lptre2pt  45561  limcleqr  45565  neglimc  45568  addlimc  45569  0ellimcdiv  45570  limclner  45572  reclimc  45574  climleltrp  45597  climisp  45667  climxrrelem  45670  climxrre  45671  cnrefiisplem  45750  climxlim2lem  45766  fprodsubrecnncnvlem  45828  fperdvper  45840  dvdivbd  45844  dvbdfbdioolem2  45850  ioodvbdlimc1lem1  45852  volioc  45893  volico  45904  stoweidlem1  45922  stoweidlem11  45932  stoweidlem13  45934  stoweidlem26  45947  stoweid  45984  wallispi  45991  wallispi2lem1  45992  wallispi2lem2  45993  wallispi2  45994  stirlinglem1  45995  stirlinglem4  45998  stirlinglem5  45999  stirlinglem7  46001  stirlinglem11  46005  dirkertrigeqlem2  46020  fourierdlem4  46032  fourierdlem26  46054  fourierdlem30  46058  fourierdlem42  46070  fourierdlem63  46090  fourierdlem65  46092  fourierdlem72  46099  fourierdlem74  46101  fourierdlem75  46102  fourierdlem76  46103  fourierdlem80  46107  fourierdlem81  46108  fourierdlem89  46116  fourierdlem90  46117  fourierdlem91  46118  fourierdlem107  46134  fourierdlem109  46136  fouriersw  46152  etransclem1  46156  etransclem4  46159  etransclem8  46163  etransclem18  46173  etransclem20  46175  etransclem21  46176  etransclem23  46178  etransclem35  46190  etransclem46  46201  rrxtopnfi  46208  rrndistlt  46211  sge0gtfsumgt  46364  hoidmv1lelem2  46513  hoidmvlelem2  46517  smfmullem1  46712  sigarmf  46775  sigarms  46777  sigarexp  46780  sigardiv  46782  sigarcol  46785  sharhght  46786  sigaradd  46787  cevathlem2  46789  cevath  46790  resubcnnred  47219  fmtnorec2lem  47416  fmtnorec3  47422  fmtnorec4  47423  lighneallem3  47481  quad1  47494  requad01  47495  requad2  47497  fppr2odd  47605  fldivmod  48252  dignn0flhalflem2  48350  affinecomb2  48437  1subrec1sub  48439  eenglngeehlnmlem1  48471  eenglngeehlnmlem2  48472  rrx2vlinest  48475  rrx2linest  48476  line2  48486  itsclc0yqsollem1  48496  itsclc0yqsol  48498  itscnhlc0xyqsol  48499  itschlc0xyqsol1  48500  itschlc0xyqsol  48501  itsclc0xyqsolr  48503  2itscplem1  48512  2itscplem2  48513  2itscplem3  48514  itscnhlinecirc02plem1  48516  inlinecirc02plem  48520  sinhpcosh  48832  i2linesd  48873