Theorem subcld 11612

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

Syntax hints:   → wi 4   ∈ wcel 2099  (class class class)co 7416  ℂcc 11147   − cmin 11485

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-10 2130  ax-11 2147  ax-12 2167  ax-ext 2697  ax-sep 5296  ax-nul 5303  ax-pow 5361  ax-pr 5425  ax-un 7738  ax-resscn 11206  ax-1cn 11207  ax-icn 11208  ax-addcl 11209  ax-addrcl 11210  ax-mulcl 11211  ax-mulrcl 11212  ax-mulcom 11213  ax-addass 11214  ax-mulass 11215  ax-distr 11216  ax-i2m1 11217  ax-1ne0 11218  ax-1rid 11219  ax-rnegex 11220  ax-rrecex 11221  ax-cnre 11222  ax-pre-lttri 11223  ax-pre-lttrn 11224  ax-pre-ltadd 11225

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3or 1085  df-3an 1086  df-tru 1537  df-fal 1547  df-ex 1775  df-nf 1779  df-sb 2061  df-mo 2529  df-eu 2558  df-clab 2704  df-cleq 2718  df-clel 2803  df-nfc 2878  df-ne 2931  df-nel 3037  df-ral 3052  df-rex 3061  df-reu 3365  df-rab 3420  df-v 3464  df-sbc 3776  df-csb 3892  df-dif 3949  df-un 3951  df-in 3953  df-ss 3963  df-nul 4323  df-if 4524  df-pw 4599  df-sn 4624  df-pr 4626  df-op 4630  df-uni 4906  df-br 5146  df-opab 5208  df-mpt 5229  df-id 5572  df-po 5586  df-so 5587  df-xp 5680  df-rel 5681  df-cnv 5682  df-co 5683  df-dm 5684  df-rn 5685  df-res 5686  df-ima 5687  df-iota 6498  df-fun 6548  df-fn 6549  df-f 6550  df-f1 6551  df-fo 6552  df-f1o 6553  df-fv 6554  df-riota 7372  df-ov 7419  df-oprab 7420  df-mpo 7421  df-er 8726  df-en 8967  df-dom 8968  df-sdom 8969  df-pnf 11291  df-mnf 11292  df-ltxr 11294  df-sub 11487

This theorem is referenced by:  pnpncand  11676  muleqadd  11899  lineq  12096  modmuladdnn0  13929  hashfz  14439  hashfzo  14441  hashf1lem2  14470  hashf1  14471  ccatswrd  14671  pfxccatin12lem2  14734  crre  15114  remim  15117  remullem  15128  abs3lem  15338  caubnd2  15357  bhmafibid1cn  15463  bhmafibid2cn  15464  bhmafibid2  15466  rlimuni  15547  climuni  15549  rlimcld2  15575  rlimrege0  15576  rlimrecl  15577  mulcn2  15593  reccn2  15594  cn1lem  15595  o1sub  15613  rlimo1  15614  o1dif  15627  rlimsqzlem  15648  caucvgrlem2  15674  iseralt  15684  fsumparts  15805  cvgcmpce  15817  incexclem  15835  arisum2  15860  geoserg  15865  pwdif  15867  geo2sum2  15873  fallfacfwd  16033  binomfallfaclem2  16037  bpolycl  16049  bpoly3  16055  bpoly4  16056  fsumcube  16057  sinf  16121  tanval2  16130  tanval3  16131  sinneg  16143  efival  16149  sinhval  16151  bitsinv1lem  16436  bitsres  16468  pythagtriplem1  16813  pythagtriplem14  16825  pythagtriplem17  16828  dvdsprmpweqle  16883  4sqlem5  16939  mul4sqlem  16950  4sqlem17  16958  vdwlem5  16982  vdwlem6  16983  vdwlem8  16985  blcvx  24802  recld2  24818  addcnlem  24868  cnllycmp  24970  cphipval2  25257  4cphipval2  25258  cphipval  25259  ipcnlem2  25260  rrxmval  25421  rrxmetlem  25423  pjthlem1  25453  ovollb2lem  25505  itgcnlem  25807  dvlem  25913  dvconst  25934  dvid  25935  dvcnp2  25937  dvcnp2OLD  25938  dvaddbr  25956  dvmulbr  25957  dvmulbrOLD  25958  dvcobr  25965  dvcobrOLD  25966  dvcjbr  25969  dvrec  25975  dvmptim  25990  dvcnvlem  25996  dveflem  25999  dvsincos  26001  cmvth  26011  cmvthOLD  26012  dvlip  26014  dvlipcn  26015  c1liplem1  26017  dveq0  26021  dv11cn  26022  dvle  26028  lhop1lem  26034  dvfsumabs  26045  dvfsumlem1  26048  dvfsumlem2  26049  dvfsumlem2OLD  26050  dvfsumrlim  26054  dvfsumrlim2  26055  ftc1lem4  26062  ftc1lem5  26063  ftc2  26067  dgrcolem2  26299  plydiveu  26323  aaliou2b  26366  taylfvallem1  26381  taylply2  26392  taylply2OLD  26393  dvtaylp  26395  dvntaylp  26396  taylthlem1  26398  taylthlem2  26399  taylthlem2OLD  26400  ulmbdd  26424  ulmcn  26425  ulmdvlem1  26426  mtest  26430  iblulm  26433  itgulm  26434  abelthlem9  26467  ptolemy  26521  tangtx  26530  sineq0  26548  efeq1  26552  efif1olem4  26569  tanarg  26643  logcnlem3  26668  logcnlem4  26669  advlogexp  26679  efopn  26682  cxpcn3lem  26772  cxpeq  26782  ang180lem4  26837  ang180lem5  26838  ang180  26839  isosctrlem2  26844  isosctrlem3  26845  isosctr  26846  ssscongptld  26847  affineequiv  26848  affineequiv2  26849  affineequiv3  26850  affineequiv4  26851  affineequivne  26852  angpieqvdlem  26853  angpieqvdlem2  26854  angpined  26855  angpieqvd  26856  chordthmlem  26857  chordthmlem2  26858  chordthmlem3  26859  chordthmlem4  26860  chordthmlem5  26861  heron  26863  quad2  26864  quad  26865  dcubic1lem  26868  dcubic  26871  mcubic  26872  cubic2  26873  cubic  26874  dquartlem1  26876  dquartlem2  26877  dquart  26878  quart1cl  26879  quart1lem  26880  quart1  26881  quartlem2  26883  quartlem4  26885  quart  26886  atanf  26905  sinasin  26914  asinsin  26917  atanneg  26932  atancj  26935  efiatan  26937  atanlogsub  26941  efiatan2  26942  2efiatan  26943  atanbndlem  26950  dvatan  26960  atantayl  26962  lgamgulmlem2  27055  lgamgulmlem3  27056  lgamgulmlem5  27058  lgamgulmlem6  27059  lgamgulm2  27061  lgamucov  27063  lgamcvg2  27080  gamcvg  27081  gamcvg2lem  27084  ftalem2  27099  logfacrlim  27250  logexprlim  27251  lgsdirprm  27357  gausslemma2dlem1a  27391  gausslemma2dlem4  27395  2sqmod  27462  addsq2nreurex  27470  vmadivsum  27508  rpvmasumlem  27513  dchrisumlem2  27516  dchrisumlem3  27517  dchrmusum2  27520  dchrvmasumlem2  27524  dchrvmasumlem3  27525  dchrvmasumiflem1  27527  rpvmasum2  27538  dchrisum0lem1b  27541  dchrisum0lem1  27542  dchrisum0lem2a  27543  rplogsum  27553  mudivsum  27556  mulogsumlem  27557  mulogsum  27558  mulog2sumlem1  27560  mulog2sumlem2  27561  mulog2sumlem3  27562  vmalogdivsum2  27564  vmalogdivsum  27565  2vmadivsumlem  27566  selberglem1  27571  selberglem2  27572  selberg2lem  27576  selberg2  27577  selberg3lem1  27583  selberg4lem1  27586  selberg4  27587  pntrsumo1  27591  selberg3r  27595  selberg34r  27597  pntrlog2bndlem1  27603  pntrlog2bndlem2  27604  pntrlog2bndlem3  27605  pntrlog2bndlem4  27606  pntrlog2bndlem5  27607  pntibndlem2  27617  pntlemf  27631  pntlemo  27633  ttgcontlem1  28815  brbtwn2  28836  colinearalglem1  28837  colinearalglem2  28838  colinearalg  28841  axsegconlem1  28848  ax5seglem1  28859  ax5seglem2  28860  ax5seglem6  28865  ax5seglem9  28868  axlowdimlem17  28889  axcontlem7  28901  axcontlem8  28902  clwlkclwwlk  29932  clwwlknonex2lem1  30037  2clwwlk2clwwlk  30280  numclwwlk3lem1  30312  smcnlem  30627  ipval2  30637  4ipval2  30638  dipcj  30644  pjhthlem1  31321  submuladdd  32653  quad3d  32657  lt2addrd  32658  bcm1n  32700  cycpmco2lem5  33012  cycpmco2lem6  33013  constrrtll  33604  constrrtlc1  33605  constrrtcclem  33607  constrrtcc  33608  constrsslem  33613  constrconj  33617  constrfin  33618  constrelextdg2  33619  sqsscirc2  33737  signslema  34421  circlemeth  34499  logdivsqrle  34509  revpfxsfxrev  34956  revwlk  34965  subfaclim  35029  divcnvlin  35568  iprodgam  35577  dnicld1  36188  dnibndlem2  36195  dnibndlem3  36196  dnibndlem6  36199  dnibndlem9  36202  dnibndlem10  36203  dnibndlem11  36204  unblimceq0  36223  unbdqndv2lem1  36225  unbdqndv2lem2  36226  knoppndvlem11  36238  knoppndvlem15  36242  knoppndvlem17  36244  knoppndvlem21  36248  bj-bary1lem  37030  bj-bary1lem1  37031  bj-bary1  37032  ftc1cnnclem  37405  ftc1anclem7  37413  ftc1anclem8  37414  ftc1anc  37415  ftc2nc  37416  areacirclem1  37422  areacirclem4  37425  areacirc  37427  cntotbnd  37510  lcmineqlem8  41748  lcmineqlem10  41750  lcmineqlem11  41751  lcmineqlem12  41752  lcmineqlem23  41763  aks4d1p1  41788  aks6d1c5lem1  41848  sticksstones10  41867  sticksstones12a  41869  sticksstones12  41870  sticksstones22  41880  bcle2d  41891  metakunt15  41927  metakunt16  41928  metakunt29  41941  metakunt30  41942  mvrrsubd  42013  lsubrotld  42016  lsubswap23d  42018  nicomachus  42039  sumcubes  42040  ef11d  42066  dffltz  42324  fltnltalem  42352  rencldnfilem  42514  pellexlem2  42524  pellexlem6  42528  pell1234qrne0  42547  pell1234qrmulcl  42549  rmyluc  42632  jm2.18  42683  jm2.19  42688  areaquad  42918  lhe4.4ex1a  44040  bcc0  44051  bccp1k  44052  bccm1k  44053  binomcxplemwb  44059  binomcxplemnn0  44060  binomcxplemrat  44061  binomcxplemfrat  44062  binomcxplemdvbinom  44064  binomcxplemnotnn0  44067  isosctrlem1ALT  44647  sineq0ALT  44650  oddfl  44928  dstregt0  44932  subadd4b  44933  sub31  44941  fzisoeu  44951  absnpncan2d  44953  absnpncan3d  44958  supxrgelem  44988  absimlere  45131  cvgcaule  45143  mullimc  45273  ellimcabssub0  45274  mullimcf  45280  limcrecl  45286  lptre2pt  45297  limcleqr  45301  neglimc  45304  addlimc  45305  0ellimcdiv  45306  limclner  45308  reclimc  45310  climleltrp  45333  climisp  45403  climxrrelem  45406  climxrre  45407  cnrefiisplem  45486  climxlim2lem  45502  fprodsubrecnncnvlem  45564  fperdvper  45576  dvdivbd  45580  dvbdfbdioolem2  45586  ioodvbdlimc1lem1  45588  volioc  45629  volico  45640  stoweidlem1  45658  stoweidlem11  45668  stoweidlem13  45670  stoweidlem26  45683  stoweid  45720  wallispi  45727  wallispi2lem1  45728  wallispi2lem2  45729  wallispi2  45730  stirlinglem1  45731  stirlinglem4  45734  stirlinglem5  45735  stirlinglem7  45737  stirlinglem11  45741  dirkertrigeqlem2  45756  fourierdlem4  45768  fourierdlem26  45790  fourierdlem30  45794  fourierdlem42  45806  fourierdlem63  45826  fourierdlem65  45828  fourierdlem72  45835  fourierdlem74  45837  fourierdlem75  45838  fourierdlem76  45839  fourierdlem80  45843  fourierdlem81  45844  fourierdlem89  45852  fourierdlem90  45853  fourierdlem91  45854  fourierdlem107  45870  fourierdlem109  45872  fouriersw  45888  etransclem1  45892  etransclem4  45895  etransclem8  45899  etransclem18  45909  etransclem20  45911  etransclem21  45912  etransclem23  45914  etransclem35  45926  etransclem46  45937  rrxtopnfi  45944  rrndistlt  45947  sge0gtfsumgt  46100  hoidmv1lelem2  46249  hoidmvlelem2  46253  smfmullem1  46448  sigarmf  46511  sigarms  46513  sigarexp  46516  sigardiv  46518  sigarcol  46521  sharhght  46522  sigaradd  46523  cevathlem2  46525  cevath  46526  resubcnnred  46953  fmtnorec2lem  47150  fmtnorec3  47156  fmtnorec4  47157  lighneallem3  47215  quad1  47228  requad01  47229  requad2  47231  fppr2odd  47339  fldivmod  47942  dignn0flhalflem2  48040  affinecomb2  48127  1subrec1sub  48129  eenglngeehlnmlem1  48161  eenglngeehlnmlem2  48162  rrx2vlinest  48165  rrx2linest  48166  line2  48176  itsclc0yqsollem1  48186  itsclc0yqsol  48188  itscnhlc0xyqsol  48189  itschlc0xyqsol1  48190  itschlc0xyqsol  48191  itsclc0xyqsolr  48193  2itscplem1  48202  2itscplem2  48203  2itscplem3  48204  itscnhlinecirc02plem1  48206  inlinecirc02plem  48210  sinhpcosh  48522  i2linesd  48563