Theorem subcld 11542

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

Syntax hints:   → wi 4   ∈ wcel 2142  (class class class)co 7396  ℂcc 11071   − cmin 11414

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-10 2175  ax-11 2191  ax-12 2212  ax-ext 2734  ax-sep 5246  ax-nul 5256  ax-pow 5322  ax-pr 5390  ax-un 7718  ax-resscn 11130  ax-1cn 11131  ax-icn 11132  ax-addcl 11133  ax-addrcl 11134  ax-mulcl 11135  ax-mulrcl 11136  ax-mulcom 11137  ax-addass 11138  ax-mulass 11139  ax-distr 11140  ax-i2m1 11141  ax-1ne0 11142  ax-1rid 11143  ax-rnegex 11144  ax-rrecex 11145  ax-cnre 11146  ax-pre-lttri 11147  ax-pre-lttrn 11148  ax-pre-ltadd 11149

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3or 1099  df-3an 1100  df-tru 1563  df-fal 1573  df-ex 1800  df-nf 1804  df-sb 2091  df-mo 2566  df-eu 2596  df-clab 2741  df-cleq 2754  df-clel 2837  df-nfc 2911  df-ne 2958  df-nel 3062  df-ral 3077  df-rex 3087  df-reu 3368  df-rab 3415  df-v 3456  df-sbc 3745  df-csb 3853  df-dif 3907  df-un 3909  df-in 3911  df-ss 3921  df-nul 4286  df-if 4481  df-pw 4557  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-opab 5163  df-mpt 5182  df-id 5542  df-po 5555  df-so 5556  df-xp 5653  df-rel 5654  df-cnv 5655  df-co 5656  df-dm 5657  df-rn 5658  df-res 5659  df-ima 5660  df-iota 6477  df-fun 6523  df-fn 6524  df-f 6525  df-f1 6526  df-fo 6527  df-f1o 6528  df-fv 6529  df-riota 7353  df-ov 7399  df-oprab 7400  df-mpo 7401  df-er 8678  df-en 8928  df-dom 8929  df-sdom 8930  df-pnf 11218  df-mnf 11219  df-ltxr 11221  df-sub 11416

This theorem is referenced by:  subsubadd23  11594  addsubsub23  11595  pnpncand  11608  muleqadd  11831  lineq  12028  modmuladdnn0  13928  hashfz  14440  hashfzo  14442  hashf1lem2  14469  hashf1  14470  ccatswrd  14682  pfxccatin12lem2  14744  crre  15141  remim  15144  remullem  15155  abs3lem  15366  caubnd2  15385  bhmafibid1cn  15493  bhmafibid2cn  15494  bhmafibid2  15496  rlimuni  15577  climuni  15579  rlimcld2  15605  rlimrege0  15606  rlimrecl  15607  mulcn2  15623  reccn2  15624  cn1lem  15625  o1sub  15643  rlimo1  15644  o1dif  15657  rlimsqzlem  15676  caucvgrlem2  15702  iseralt  15712  fsumparts  15834  cvgcmpce  15846  incexclem  15866  arisum2  15891  geoserg  15896  pwdif  15898  geo2sum2  15904  fallfacfwd  16066  binomfallfaclem2  16070  bpolycl  16082  bpoly3  16088  bpoly4  16089  fsumcube  16090  sinf  16156  tanval2  16165  tanval3  16166  sinneg  16178  efival  16184  sinhval  16186  bitsinv1lem  16475  bitsres  16507  pythagtriplem1  16852  pythagtriplem14  16864  pythagtriplem17  16867  dvdsprmpweqle  16922  4sqlem5  16978  mul4sqlem  16989  4sqlem17  16997  vdwlem5  17021  vdwlem6  17022  vdwlem8  17024  blcvx  24858  recld2  24875  addcnlem  24925  cnllycmp  25018  cphipval2  25303  4cphipval2  25304  cphipval  25305  ipcnlem2  25306  rrxmval  25467  rrxmetlem  25469  pjthlem1  25499  ovollb2lem  25550  itgcnlem  25852  dvlem  25958  dvconst  25979  dvid  25980  dvcnp2  25982  dvaddbr  26000  dvmulbr  26001  dvcobr  26008  dvcjbr  26011  dvrec  26017  dvmptim  26032  dvcnvlem  26038  dveflem  26041  dvsincos  26043  cmvth  26053  dvlip  26055  dvlipcn  26056  c1liplem1  26058  dveq0  26062  dv11cn  26063  dvle  26069  lhop1lem  26075  dvfsumabs  26085  dvfsumlem1  26088  dvfsumlem2  26089  dvfsumrlim  26093  dvfsumrlim2  26094  ftc1lem4  26101  ftc1lem5  26102  ftc2  26106  dgrcolem2  26334  plydiveu  26362  aaliou2b  26405  taylfvallem1  26420  taylply2  26431  dvtaylp  26433  dvntaylp  26434  taylthlem1  26436  taylthlem2  26437  ulmbdd  26461  ulmcn  26462  ulmdvlem1  26463  mtest  26467  iblulm  26470  itgulm  26471  abelthlem9  26503  ptolemy  26561  tangtx  26570  sineq0  26589  efeq1  26593  efif1olem4  26610  tanarg  26684  logcnlem3  26709  logcnlem4  26710  advlogexp  26720  efopn  26723  cxpcn3lem  26812  cxpeq  26822  ang180lem4  26877  ang180lem5  26878  ang180  26879  isosctrlem2  26884  isosctrlem3  26885  isosctr  26886  ssscongptld  26887  affineequiv  26888  affineequiv2  26889  affineequiv3  26890  affineequiv4  26891  affineequivne  26892  angpieqvdlem  26893  angpieqvdlem2  26894  angpined  26895  angpieqvd  26896  chordthmlem  26897  chordthmlem2  26898  chordthmlem3  26899  chordthmlem4  26900  chordthmlem5  26901  heron  26903  quad2  26904  quad  26905  dcubic1lem  26908  dcubic  26911  mcubic  26912  cubic2  26913  cubic  26914  dquartlem1  26916  dquartlem2  26917  dquart  26918  quart1cl  26919  quart1lem  26920  quart1  26921  quartlem2  26923  quartlem4  26925  quart  26926  atanf  26945  sinasin  26954  asinsin  26957  atanneg  26972  atancj  26975  efiatan  26977  atanlogsub  26981  efiatan2  26982  2efiatan  26983  atanbndlem  26990  dvatan  27000  atantayl  27002  lgamgulmlem2  27094  lgamgulmlem3  27095  lgamgulmlem5  27097  lgamgulmlem6  27098  lgamgulm2  27100  lgamucov  27102  lgamcvg2  27119  gamcvg  27120  gamcvg2lem  27123  ftalem2  27138  logfacrlim  27288  logexprlim  27289  lgsdirprm  27395  gausslemma2dlem1a  27429  gausslemma2dlem4  27433  2sqmod  27500  addsq2nreurex  27508  vmadivsum  27546  rpvmasumlem  27551  dchrisumlem2  27554  dchrisumlem3  27555  dchrmusum2  27558  dchrvmasumlem2  27562  dchrvmasumlem3  27563  dchrvmasumiflem1  27565  rpvmasum2  27576  dchrisum0lem1b  27579  dchrisum0lem1  27580  dchrisum0lem2a  27581  rplogsum  27591  mudivsum  27594  mulogsumlem  27595  mulogsum  27596  mulog2sumlem1  27598  mulog2sumlem2  27599  mulog2sumlem3  27600  vmalogdivsum2  27602  vmalogdivsum  27603  2vmadivsumlem  27604  selberglem1  27609  selberglem2  27610  selberg2lem  27614  selberg2  27615  selberg3lem1  27621  selberg4lem1  27624  selberg4  27625  pntrsumo1  27629  selberg3r  27633  selberg34r  27635  pntrlog2bndlem1  27641  pntrlog2bndlem2  27642  pntrlog2bndlem3  27643  pntrlog2bndlem4  27644  pntrlog2bndlem5  27645  pntibndlem2  27655  pntlemf  27669  pntlemo  27671  ttgcontlem1  29085  brbtwn2  29106  colinearalglem1  29107  colinearalglem2  29108  colinearalg  29111  axsegconlem1  29118  ax5seglem1  29129  ax5seglem2  29130  ax5seglem6  29135  ax5seglem9  29138  axlowdimlem17  29159  axcontlem7  29171  axcontlem8  29172  clwlkclwwlk  30204  clwwlknonex2lem1  30309  2clwwlk2clwwlk  30552  numclwwlk3lem1  30584  smcnlem  30900  ipval2  30910  4ipval2  30911  dipcj  30917  pjhthlem1  31594  submuladdd  32942  binom2subadd  32943  pythagreim  32947  quad3d  32951  lt2addrd  32952  bcm1n  32997  cycpmco2lem5  33310  cycpmco2lem6  33311  vietalem  33876  constrrtll  34028  constrrtlc1  34029  constrrtcclem  34031  constrrtcc  34032  constrsslem  34038  constrconj  34042  constrfin  34043  constrelextdg2  34044  constraddcl  34059  iconstr  34063  constrremulcl  34064  constrrecl  34066  constrmulcl  34068  constrreinvcl  34069  constrresqrtcl  34074  cos9thpiminplylem2  34080  cos9thpiminplylem3  34081  sqsscirc2  34206  signslema  34856  circlemeth  34934  logdivsqrle  34944  revpfxsfxrev  35466  revwlk  35475  subfaclim  35538  divcnvlin  36083  iprodgam  36092  dnicld1  36910  dnibndlem2  36917  dnibndlem3  36918  dnibndlem6  36921  dnibndlem9  36924  dnibndlem10  36925  dnibndlem11  36926  unblimceq0  36945  unbdqndv2lem1  36947  unbdqndv2lem2  36948  knoppndvlem11  36960  knoppndvlem15  36964  knoppndvlem17  36966  knoppndvlem21  36970  bj-bary1lem  37802  bj-bary1lem1  37803  bj-bary1  37804  qdiff  37819  ftc1cnnclem  38190  ftc1anclem7  38198  ftc1anclem8  38199  ftc1anc  38200  ftc2nc  38201  areacirclem1  38207  areacirclem4  38210  areacirc  38212  cntotbnd  38295  lcmineqlem8  42653  lcmineqlem10  42655  lcmineqlem11  42656  lcmineqlem12  42657  lcmineqlem23  42668  aks4d1p1  42693  aks6d1c5lem1  42753  sticksstones10  42772  sticksstones12a  42774  sticksstones12  42775  sticksstones22  42785  bcle2d  42796  mvrrsubd  42883  lsubrotld  42886  lsubswap23d  42888  nicomachus  42921  sumcubes  42922  ef11d  42948  tanhalfpim  42958  sinpim  42959  cospim  42960  dffltz  43216  fltnltalem  43244  rencldnfilem  43397  pellexlem2  43407  pellexlem6  43411  pell1234qrne0  43430  pell1234qrmulcl  43432  rmyluc  43514  jm2.18  43565  jm2.19  43570  areaquad  43793  lhe4.4ex1a  44905  bcc0  44916  bccp1k  44917  bccm1k  44918  binomcxplemwb  44924  binomcxplemnn0  44925  binomcxplemrat  44926  binomcxplemfrat  44927  binomcxplemdvbinom  44929  binomcxplemnotnn0  44932  isosctrlem1ALT  45509  sineq0ALT  45512  oddfl  45857  dstregt0  45861  subadd4b  45862  sub31  45869  fzisoeu  45879  absnpncan2d  45881  absnpncan3d  45886  supxrgelem  45913  absimlere  46053  cvgcaule  46065  mullimc  46192  ellimcabssub0  46193  mullimcf  46199  limcrecl  46205  lptre2pt  46214  limcleqr  46218  neglimc  46221  addlimc  46222  0ellimcdiv  46223  limclner  46225  reclimc  46227  climleltrp  46250  climisp  46320  climxrrelem  46323  climxrre  46324  cnrefiisplem  46403  climxlim2lem  46419  fprodsubrecnncnvlem  46481  fperdvper  46493  dvdivbd  46497  dvbdfbdioolem2  46503  ioodvbdlimc1lem1  46505  volioc  46546  volico  46557  stoweidlem1  46575  stoweidlem11  46585  stoweidlem13  46587  stoweidlem26  46600  stoweid  46637  wallispi  46644  wallispi2lem1  46645  wallispi2lem2  46646  wallispi2  46647  stirlinglem1  46648  stirlinglem4  46651  stirlinglem5  46652  stirlinglem7  46654  stirlinglem11  46658  dirkertrigeqlem2  46673  fourierdlem4  46685  fourierdlem26  46707  fourierdlem30  46711  fourierdlem42  46723  fourierdlem63  46743  fourierdlem65  46745  fourierdlem72  46752  fourierdlem74  46754  fourierdlem75  46755  fourierdlem76  46756  fourierdlem80  46760  fourierdlem81  46761  fourierdlem89  46769  fourierdlem90  46770  fourierdlem91  46771  fourierdlem107  46787  fourierdlem109  46789  fouriersw  46805  etransclem1  46809  etransclem4  46812  etransclem8  46816  etransclem18  46826  etransclem20  46828  etransclem21  46829  etransclem23  46831  etransclem35  46843  etransclem46  46854  rrxtopnfi  46861  rrndistlt  46864  sge0gtfsumgt  47017  hoidmv1lelem2  47166  hoidmvlelem2  47170  smfmullem1  47365  sigarmf  47428  sigarms  47430  sigarexp  47433  sigardiv  47435  sigarcol  47438  sharhght  47439  sigaradd  47440  cevathlem2  47442  cevath  47443  sin5tlem3  47469  sin5tlem4  47470  sin5tlem5  47471  cos5t  47473  resubcnnred  47898  fldivmod  47938  ceildivmod  47939  fmtnorec2lem  48151  fmtnorec3  48157  fmtnorec4  48158  lighneallem3  48216  quad1  48242  requad01  48243  requad2  48245  fppr2odd  48353  dignn0flhalflem2  49238  affinecomb2  49325  1subrec1sub  49327  eenglngeehlnmlem1  49359  eenglngeehlnmlem2  49360  rrx2vlinest  49363  rrx2linest  49364  line2  49374  itsclc0yqsollem1  49384  itsclc0yqsol  49386  itscnhlc0xyqsol  49387  itschlc0xyqsol1  49388  itschlc0xyqsol  49389  itsclc0xyqsolr  49391  2itscplem1  49400  2itscplem2  49401  2itscplem3  49402  itscnhlinecirc02plem1  49404  inlinecirc02plem  49408  sinhpcosh  50361  i2linesd  50400