Theorem subcld 11620

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

Syntax hints:   → wi 4   ∈ wcel 2108  (class class class)co 7431  ℂcc 11153   − cmin 11492

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708  ax-sep 5296  ax-nul 5306  ax-pow 5365  ax-pr 5432  ax-un 7755  ax-resscn 11212  ax-1cn 11213  ax-icn 11214  ax-addcl 11215  ax-addrcl 11216  ax-mulcl 11217  ax-mulrcl 11218  ax-mulcom 11219  ax-addass 11220  ax-mulass 11221  ax-distr 11222  ax-i2m1 11223  ax-1ne0 11224  ax-1rid 11225  ax-rnegex 11226  ax-rrecex 11227  ax-cnre 11228  ax-pre-lttri 11229  ax-pre-lttrn 11230  ax-pre-ltadd 11231

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-reu 3381  df-rab 3437  df-v 3482  df-sbc 3789  df-csb 3900  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-nul 4334  df-if 4526  df-pw 4602  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-br 5144  df-opab 5206  df-mpt 5226  df-id 5578  df-po 5592  df-so 5593  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-rn 5696  df-res 5697  df-ima 5698  df-iota 6514  df-fun 6563  df-fn 6564  df-f 6565  df-f1 6566  df-fo 6567  df-f1o 6568  df-fv 6569  df-riota 7388  df-ov 7434  df-oprab 7435  df-mpo 7436  df-er 8745  df-en 8986  df-dom 8987  df-sdom 8988  df-pnf 11297  df-mnf 11298  df-ltxr 11300  df-sub 11494

This theorem is referenced by:  pnpncand  11684  muleqadd  11907  lineq  12104  modmuladdnn0  13956  hashfz  14466  hashfzo  14468  hashf1lem2  14495  hashf1  14496  ccatswrd  14706  pfxccatin12lem2  14769  crre  15153  remim  15156  remullem  15167  abs3lem  15377  caubnd2  15396  bhmafibid1cn  15502  bhmafibid2cn  15503  bhmafibid2  15505  rlimuni  15586  climuni  15588  rlimcld2  15614  rlimrege0  15615  rlimrecl  15616  mulcn2  15632  reccn2  15633  cn1lem  15634  o1sub  15652  rlimo1  15653  o1dif  15666  rlimsqzlem  15685  caucvgrlem2  15711  iseralt  15721  fsumparts  15842  cvgcmpce  15854  incexclem  15872  arisum2  15897  geoserg  15902  pwdif  15904  geo2sum2  15910  fallfacfwd  16072  binomfallfaclem2  16076  bpolycl  16088  bpoly3  16094  bpoly4  16095  fsumcube  16096  sinf  16160  tanval2  16169  tanval3  16170  sinneg  16182  efival  16188  sinhval  16190  bitsinv1lem  16478  bitsres  16510  pythagtriplem1  16854  pythagtriplem14  16866  pythagtriplem17  16869  dvdsprmpweqle  16924  4sqlem5  16980  mul4sqlem  16991  4sqlem17  16999  vdwlem5  17023  vdwlem6  17024  vdwlem8  17026  blcvx  24819  recld2  24836  addcnlem  24886  cnllycmp  24988  cphipval2  25275  4cphipval2  25276  cphipval  25277  ipcnlem2  25278  rrxmval  25439  rrxmetlem  25441  pjthlem1  25471  ovollb2lem  25523  itgcnlem  25825  dvlem  25931  dvconst  25952  dvid  25953  dvcnp2  25955  dvcnp2OLD  25956  dvaddbr  25974  dvmulbr  25975  dvmulbrOLD  25976  dvcobr  25983  dvcobrOLD  25984  dvcjbr  25987  dvrec  25993  dvmptim  26008  dvcnvlem  26014  dveflem  26017  dvsincos  26019  cmvth  26029  cmvthOLD  26030  dvlip  26032  dvlipcn  26033  c1liplem1  26035  dveq0  26039  dv11cn  26040  dvle  26046  lhop1lem  26052  dvfsumabs  26063  dvfsumlem1  26066  dvfsumlem2  26067  dvfsumlem2OLD  26068  dvfsumrlim  26072  dvfsumrlim2  26073  ftc1lem4  26080  ftc1lem5  26081  ftc2  26085  dgrcolem2  26314  plydiveu  26340  aaliou2b  26383  taylfvallem1  26398  taylply2  26409  taylply2OLD  26410  dvtaylp  26412  dvntaylp  26413  taylthlem1  26415  taylthlem2  26416  taylthlem2OLD  26417  ulmbdd  26441  ulmcn  26442  ulmdvlem1  26443  mtest  26447  iblulm  26450  itgulm  26451  abelthlem9  26484  ptolemy  26538  tangtx  26547  sineq0  26566  efeq1  26570  efif1olem4  26587  tanarg  26661  logcnlem3  26686  logcnlem4  26687  advlogexp  26697  efopn  26700  cxpcn3lem  26790  cxpeq  26800  ang180lem4  26855  ang180lem5  26856  ang180  26857  isosctrlem2  26862  isosctrlem3  26863  isosctr  26864  ssscongptld  26865  affineequiv  26866  affineequiv2  26867  affineequiv3  26868  affineequiv4  26869  affineequivne  26870  angpieqvdlem  26871  angpieqvdlem2  26872  angpined  26873  angpieqvd  26874  chordthmlem  26875  chordthmlem2  26876  chordthmlem3  26877  chordthmlem4  26878  chordthmlem5  26879  heron  26881  quad2  26882  quad  26883  dcubic1lem  26886  dcubic  26889  mcubic  26890  cubic2  26891  cubic  26892  dquartlem1  26894  dquartlem2  26895  dquart  26896  quart1cl  26897  quart1lem  26898  quart1  26899  quartlem2  26901  quartlem4  26903  quart  26904  atanf  26923  sinasin  26932  asinsin  26935  atanneg  26950  atancj  26953  efiatan  26955  atanlogsub  26959  efiatan2  26960  2efiatan  26961  atanbndlem  26968  dvatan  26978  atantayl  26980  lgamgulmlem2  27073  lgamgulmlem3  27074  lgamgulmlem5  27076  lgamgulmlem6  27077  lgamgulm2  27079  lgamucov  27081  lgamcvg2  27098  gamcvg  27099  gamcvg2lem  27102  ftalem2  27117  logfacrlim  27268  logexprlim  27269  lgsdirprm  27375  gausslemma2dlem1a  27409  gausslemma2dlem4  27413  2sqmod  27480  addsq2nreurex  27488  vmadivsum  27526  rpvmasumlem  27531  dchrisumlem2  27534  dchrisumlem3  27535  dchrmusum2  27538  dchrvmasumlem2  27542  dchrvmasumlem3  27543  dchrvmasumiflem1  27545  rpvmasum2  27556  dchrisum0lem1b  27559  dchrisum0lem1  27560  dchrisum0lem2a  27561  rplogsum  27571  mudivsum  27574  mulogsumlem  27575  mulogsum  27576  mulog2sumlem1  27578  mulog2sumlem2  27579  mulog2sumlem3  27580  vmalogdivsum2  27582  vmalogdivsum  27583  2vmadivsumlem  27584  selberglem1  27589  selberglem2  27590  selberg2lem  27594  selberg2  27595  selberg3lem1  27601  selberg4lem1  27604  selberg4  27605  pntrsumo1  27609  selberg3r  27613  selberg34r  27615  pntrlog2bndlem1  27621  pntrlog2bndlem2  27622  pntrlog2bndlem3  27623  pntrlog2bndlem4  27624  pntrlog2bndlem5  27625  pntibndlem2  27635  pntlemf  27649  pntlemo  27651  ttgcontlem1  28899  brbtwn2  28920  colinearalglem1  28921  colinearalglem2  28922  colinearalg  28925  axsegconlem1  28932  ax5seglem1  28943  ax5seglem2  28944  ax5seglem6  28949  ax5seglem9  28952  axlowdimlem17  28973  axcontlem7  28985  axcontlem8  28986  clwlkclwwlk  30021  clwwlknonex2lem1  30126  2clwwlk2clwwlk  30369  numclwwlk3lem1  30401  smcnlem  30716  ipval2  30726  4ipval2  30727  dipcj  30733  pjhthlem1  31410  submuladdd  32750  quad3d  32754  lt2addrd  32755  bcm1n  32797  cycpmco2lem5  33150  cycpmco2lem6  33151  constrrtll  33772  constrrtlc1  33773  constrrtcclem  33775  constrrtcc  33776  constrsslem  33782  constrconj  33786  constrfin  33787  constrelextdg2  33788  sqsscirc2  33908  signslema  34577  circlemeth  34655  logdivsqrle  34665  revpfxsfxrev  35121  revwlk  35130  subfaclim  35193  divcnvlin  35733  iprodgam  35742  dnicld1  36473  dnibndlem2  36480  dnibndlem3  36481  dnibndlem6  36484  dnibndlem9  36487  dnibndlem10  36488  dnibndlem11  36489  unblimceq0  36508  unbdqndv2lem1  36510  unbdqndv2lem2  36511  knoppndvlem11  36523  knoppndvlem15  36527  knoppndvlem17  36529  knoppndvlem21  36533  bj-bary1lem  37311  bj-bary1lem1  37312  bj-bary1  37313  ftc1cnnclem  37698  ftc1anclem7  37706  ftc1anclem8  37707  ftc1anc  37708  ftc2nc  37709  areacirclem1  37715  areacirclem4  37718  areacirc  37720  cntotbnd  37803  lcmineqlem8  42037  lcmineqlem10  42039  lcmineqlem11  42040  lcmineqlem12  42041  lcmineqlem23  42052  aks4d1p1  42077  aks6d1c5lem1  42137  sticksstones10  42156  sticksstones12a  42158  sticksstones12  42159  sticksstones22  42169  bcle2d  42180  metakunt15  42220  metakunt16  42221  metakunt29  42234  metakunt30  42235  mvrrsubd  42309  lsubrotld  42312  lsubswap23d  42314  nicomachus  42346  sumcubes  42347  ef11d  42375  tanhalfpim  42385  dffltz  42644  fltnltalem  42672  rencldnfilem  42831  pellexlem2  42841  pellexlem6  42845  pell1234qrne0  42864  pell1234qrmulcl  42866  rmyluc  42949  jm2.18  43000  jm2.19  43005  areaquad  43228  lhe4.4ex1a  44348  bcc0  44359  bccp1k  44360  bccm1k  44361  binomcxplemwb  44367  binomcxplemnn0  44368  binomcxplemrat  44369  binomcxplemfrat  44370  binomcxplemdvbinom  44372  binomcxplemnotnn0  44375  isosctrlem1ALT  44954  sineq0ALT  44957  oddfl  45289  dstregt0  45293  subadd4b  45294  sub31  45302  fzisoeu  45312  absnpncan2d  45314  absnpncan3d  45319  supxrgelem  45348  absimlere  45490  cvgcaule  45502  mullimc  45631  ellimcabssub0  45632  mullimcf  45638  limcrecl  45644  lptre2pt  45655  limcleqr  45659  neglimc  45662  addlimc  45663  0ellimcdiv  45664  limclner  45666  reclimc  45668  climleltrp  45691  climisp  45761  climxrrelem  45764  climxrre  45765  cnrefiisplem  45844  climxlim2lem  45860  fprodsubrecnncnvlem  45922  fperdvper  45934  dvdivbd  45938  dvbdfbdioolem2  45944  ioodvbdlimc1lem1  45946  volioc  45987  volico  45998  stoweidlem1  46016  stoweidlem11  46026  stoweidlem13  46028  stoweidlem26  46041  stoweid  46078  wallispi  46085  wallispi2lem1  46086  wallispi2lem2  46087  wallispi2  46088  stirlinglem1  46089  stirlinglem4  46092  stirlinglem5  46093  stirlinglem7  46095  stirlinglem11  46099  dirkertrigeqlem2  46114  fourierdlem4  46126  fourierdlem26  46148  fourierdlem30  46152  fourierdlem42  46164  fourierdlem63  46184  fourierdlem65  46186  fourierdlem72  46193  fourierdlem74  46195  fourierdlem75  46196  fourierdlem76  46197  fourierdlem80  46201  fourierdlem81  46202  fourierdlem89  46210  fourierdlem90  46211  fourierdlem91  46212  fourierdlem107  46228  fourierdlem109  46230  fouriersw  46246  etransclem1  46250  etransclem4  46253  etransclem8  46257  etransclem18  46267  etransclem20  46269  etransclem21  46270  etransclem23  46272  etransclem35  46284  etransclem46  46295  rrxtopnfi  46302  rrndistlt  46305  sge0gtfsumgt  46458  hoidmv1lelem2  46607  hoidmvlelem2  46611  smfmullem1  46806  sigarmf  46869  sigarms  46871  sigarexp  46874  sigardiv  46876  sigarcol  46879  sharhght  46880  sigaradd  46881  cevathlem2  46883  cevath  46884  resubcnnred  47316  fldivmod  47340  ceildivmod  47341  fmtnorec2lem  47529  fmtnorec3  47535  fmtnorec4  47536  lighneallem3  47594  quad1  47607  requad01  47608  requad2  47610  fppr2odd  47718  dignn0flhalflem2  48537  affinecomb2  48624  1subrec1sub  48626  eenglngeehlnmlem1  48658  eenglngeehlnmlem2  48659  rrx2vlinest  48662  rrx2linest  48663  line2  48673  itsclc0yqsollem1  48683  itsclc0yqsol  48685  itscnhlc0xyqsol  48686  itschlc0xyqsol1  48687  itschlc0xyqsol  48688  itsclc0xyqsolr  48690  2itscplem1  48699  2itscplem2  48700  2itscplem3  48701  itscnhlinecirc02plem1  48703  inlinecirc02plem  48707  sinhpcosh  49259  i2linesd  49298