Theorem subcld 11573

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2143  (class class class)co 7410  ℂcc 11102   − cmin 11445

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-10 2176  ax-11 2192  ax-12 2213  ax-ext 2735  ax-sep 5257  ax-nul 5269  ax-pow 5336  ax-pr 5404  ax-un 7732  ax-resscn 11161  ax-1cn 11162  ax-icn 11163  ax-addcl 11164  ax-addrcl 11165  ax-mulcl 11166  ax-mulrcl 11167  ax-mulcom 11168  ax-addass 11169  ax-mulass 11170  ax-distr 11171  ax-i2m1 11172  ax-1ne0 11173  ax-1rid 11174  ax-rnegex 11175  ax-rrecex 11176  ax-cnre 11177  ax-pre-lttri 11178  ax-pre-lttrn 11179  ax-pre-ltadd 11180

This proof depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-nf 1814  df-sb 2097  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2838  df-nfc 2912  df-ne 2959  df-nel 3065  df-ral 3080  df-rex 3090  df-reu 3370  df-rab 3417  df-v 3457  df-sbc 3745  df-csb 3854  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-nul 4287  df-if 4488  df-pw 4564  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4873  df-br 5110  df-opab 5174  df-mpt 5193  df-id 5556  df-po 5569  df-so 5570  df-xp 5667  df-rel 5668  df-cnv 5669  df-co 5670  df-dm 5671  df-rn 5672  df-res 5673  df-ima 5674  df-iota 6492  df-fun 6538  df-fn 6539  df-f 6540  df-f1 6541  df-fo 6542  df-f1o 6543  df-fv 6544  df-riota 7367  df-ov 7413  df-oprab 7414  df-mpo 7415  df-er 8690  df-en 8940  df-dom 8941  df-sdom 8942  df-pnf 11249  df-mnf 11250  df-ltxr 11252  df-sub 11447

This theorem is used by:  subsubadd23  11625  addsubsub23  11626  pnpncand  11639  muleqadd  11862  lineq  12056  modmuladdnn0  13956  hashfz  14469  hashfzo  14471  hashf1lem2  14498  hashf1  14499  ccatswrd  14711  pfxccatin12lem2  14773  crre  15170  remim  15173  remullem  15184  abs3lem  15395  caubnd2  15414  bhmafibid1cn  15522  bhmafibid2cn  15523  bhmafibid2  15525  rlimuni  15606  climuni  15608  rlimcld2  15634  rlimrege0  15635  rlimrecl  15636  mulcn2  15652  reccn2  15653  cn1lem  15654  o1sub  15672  rlimo1  15673  o1dif  15686  rlimsqzlem  15705  caucvgrlem2  15731  iseralt  15741  fsumparts  15863  cvgcmpce  15875  incexclem  15895  arisum2  15920  geoserg  15925  pwdif  15927  geo2sum2  15933  fallfacfwd  16094  binomfallfaclem2  16098  bpolycl  16110  bpoly3  16116  bpoly4  16117  fsumcube  16118  sinf  16184  tanval2  16193  tanval3  16194  sinneg  16206  efival  16212  sinhval  16214  bitsinv1lem  16503  bitsres  16535  pythagtriplem1  16880  pythagtriplem14  16892  pythagtriplem17  16895  dvdsprmpweqle  16950  4sqlem5  17006  mul4sqlem  17017  4sqlem17  17025  vdwlem5  17049  vdwlem6  17050  vdwlem8  17052  blcvx  24964  recld2  24981  addcnlem  25031  cnllycmp  25124  cphipval2  25409  4cphipval2  25410  cphipval  25411  ipcnlem2  25412  rrxmval  25573  rrxmetlem  25575  pjthlem1  25605  ovollb2lem  25656  itgcnlem  25958  dvlem  26064  dvconst  26085  dvid  26086  dvcnp2  26088  dvaddbr  26106  dvmulbr  26107  dvcobr  26114  dvcjbr  26117  dvrec  26123  dvmptim  26138  dvcnvlem  26144  dveflem  26147  dvsincos  26149  cmvth  26159  dvlip  26161  dvlipcn  26162  c1liplem1  26164  dveq0  26168  dv11cn  26169  dvle  26175  lhop1lem  26181  dvfsumabs  26191  dvfsumlem1  26194  dvfsumlem2  26195  dvfsumrlim  26199  dvfsumrlim2  26200  ftc1lem4  26207  ftc1lem5  26208  ftc2  26212  dgrcolem2  26440  plydiveu  26468  aaliou2b  26513  taylfvallem1  26529  taylply2  26540  dvtaylp  26542  dvntaylp  26543  taylthlem1  26545  taylthlem2  26546  ulmbdd  26570  ulmcn  26571  ulmdvlem1  26572  mtest  26576  iblulm  26579  itgulm  26580  abelthlem9  26612  ptolemy  26670  tangtx  26679  sineq0  26698  efeq1  26702  efif1olem4  26719  tanarg  26793  logcnlem3  26818  logcnlem4  26819  advlogexp  26829  efopn  26832  cxpcn3lem  26921  cxpeq  26931  ang180lem4  26986  ang180lem5  26987  ang180  26988  isosctrlem2  26993  isosctrlem3  26994  isosctr  26995  ssscongptld  26996  affineequiv  26997  affineequiv2  26998  affineequiv3  26999  affineequiv4  27000  affineequivne  27001  angpieqvdlem  27002  angpieqvdlem2  27003  angpined  27004  angpieqvd  27005  chordthmlem  27006  chordthmlem2  27007  chordthmlem3  27008  chordthmlem4  27009  chordthmlem5  27010  heron  27012  quad2  27013  quad  27014  dcubic1lem  27017  dcubic  27020  mcubic  27021  cubic2  27022  cubic  27023  dquartlem1  27025  dquartlem2  27026  dquart  27027  quart1cl  27028  quart1lem  27029  quart1  27030  quartlem2  27032  quartlem4  27034  quart  27035  atanf  27054  sinasin  27063  asinsin  27066  atanneg  27081  atancj  27084  efiatan  27086  atanlogsub  27090  efiatan2  27091  2efiatan  27092  atanbndlem  27099  dvatan  27109  atantayl  27111  lgamgulmlem2  27203  lgamgulmlem3  27204  lgamgulmlem5  27206  lgamgulmlem6  27207  lgamgulm2  27209  lgamucov  27211  lgamcvg2  27228  gamcvg  27229  gamcvg2lem  27232  ftalem2  27247  logfacrlim  27397  logexprlim  27398  lgsdirprm  27504  gausslemma2dlem1a  27538  gausslemma2dlem4  27542  2sqmod  27609  addsq2nreurex  27617  vmadivsum  27655  rpvmasumlem  27660  dchrisumlem2  27663  dchrisumlem3  27664  dchrmusum2  27667  dchrvmasumlem2  27671  dchrvmasumlem3  27672  dchrvmasumiflem1  27674  rpvmasum2  27685  dchrisum0lem1b  27688  dchrisum0lem1  27689  dchrisum0lem2a  27690  rplogsum  27700  mudivsum  27703  mulogsumlem  27704  mulogsum  27705  mulog2sumlem1  27707  mulog2sumlem2  27708  mulog2sumlem3  27709  vmalogdivsum2  27711  vmalogdivsum  27712  2vmadivsumlem  27713  selberglem1  27718  selberglem2  27719  selberg2lem  27723  selberg2  27724  selberg3lem1  27730  selberg4lem1  27733  selberg4  27734  pntrsumo1  27738  selberg3r  27742  selberg34r  27744  pntrlog2bndlem1  27750  pntrlog2bndlem2  27751  pntrlog2bndlem3  27752  pntrlog2bndlem4  27753  pntrlog2bndlem5  27754  pntibndlem2  27764  pntlemf  27778  pntlemo  27780  ttgcontlem1  29243  brbtwn2  29264  colinearalglem1  29265  colinearalglem2  29266  colinearalg  29269  axsegconlem1  29276  ax5seglem1  29287  ax5seglem2  29288  ax5seglem6  29293  ax5seglem9  29296  axlowdimlem17  29317  axcontlem7  29329  axcontlem8  29330  clwlkclwwlk  30362  clwwlknonex2lem1  30467  2clwwlk2clwwlk  30710  numclwwlk3lem1  30742  smcnlem  31058  ipval2  31068  4ipval2  31069  dipcj  31075  pjhthlem1  31752  submuladdd  33094  binom2subadd  33095  pythagreim  33099  quad3d  33103  lt2addrd  33104  bcm1n  33149  cycpmco2lem5  33459  cycpmco2lem6  33460  vietalem  33978  constrrtll  34130  constrrtlc1  34131  constrrtcclem  34133  constrrtcc  34134  constrsslem  34140  constrconj  34144  constrfin  34145  constrelextdg2  34146  constraddcl  34161  iconstr  34165  constrremulcl  34166  constrrecl  34168  constrmulcl  34170  constrreinvcl  34171  constrresqrtcl  34176  cos9thpiminplylem2  34182  cos9thpiminplylem3  34183  sqsscirc2  34308  signslema  34958  circlemeth  35036  logdivsqrle  35046  revpfxsfxrev  35615  revwlk  35625  subfaclim  35688  divcnvlin  36233  iprodgam  36242  dnicld1  37089  dnibndlem2  37096  dnibndlem3  37097  dnibndlem6  37100  dnibndlem9  37103  dnibndlem10  37104  dnibndlem11  37105  unblimceq0  37124  unbdqndv2lem1  37126  unbdqndv2lem2  37127  knoppndvlem11  37139  knoppndvlem15  37143  knoppndvlem17  37145  knoppndvlem21  37149  bj-bary1lem  37982  bj-bary1lem1  37983  bj-bary1  37984  qdiff  37999  ftc1cnnclem  38370  ftc1anclem7  38378  ftc1anclem8  38379  ftc1anc  38380  ftc2nc  38381  areacirclem1  38387  areacirclem4  38390  areacirc  38392  cntotbnd  38475  lcmineqlem8  42831  lcmineqlem10  42833  lcmineqlem11  42834  lcmineqlem12  42835  lcmineqlem23  42846  aks4d1p1  42871  aks6d1c5lem1  42931  sticksstones10  42950  sticksstones12a  42952  sticksstones12  42953  sticksstones22  42963  bcle2d  42974  quadfac  43000  mvrrsubd  43063  lsubrotld  43066  lsubswap23d  43068  nicomachus  43101  sumcubes  43102  ef11d  43128  tanhalfpim  43138  sinpim  43139  cospim  43140  dffltz  43394  fltnltalem  43422  rencldnfilem  43575  pellexlem2  43585  pellexlem6  43589  pell1234qrne0  43608  pell1234qrmulcl  43610  rmyluc  43692  jm2.18  43743  jm2.19  43748  areaquad  43971  lhe4.4ex1a  45067  bcc0  45078  bccp1k  45079  bccm1k  45080  binomcxplemwb  45086  binomcxplemnn0  45087  binomcxplemrat  45088  binomcxplemfrat  45089  binomcxplemdvbinom  45091  binomcxplemnotnn0  45094  isosctrlem1ALT  45670  sineq0ALT  45673  oddfl  46025  dstregt0  46029  subadd4b  46030  sub31  46037  fzisoeu  46047  absnpncan2d  46049  absnpncan3d  46054  supxrgelem  46081  absimlere  46221  cvgcaule  46233  mullimc  46360  ellimcabssub0  46361  mullimcf  46367  limcrecl  46373  lptre2pt  46382  limcleqr  46386  neglimc  46389  addlimc  46390  0ellimcdiv  46391  limclner  46393  reclimc  46395  climleltrp  46418  climisp  46488  climxrrelem  46491  climxrre  46492  cnrefiisplem  46571  climxlim2lem  46587  fprodsubrecnncnvlem  46649  fperdvper  46661  dvdivbd  46665  dvbdfbdioolem2  46671  ioodvbdlimc1lem1  46673  volioc  46714  volico  46725  stoweidlem1  46743  stoweidlem11  46753  stoweidlem13  46755  stoweidlem26  46768  stoweid  46805  wallispi  46812  wallispi2lem1  46813  wallispi2lem2  46814  wallispi2  46815  stirlinglem1  46816  stirlinglem4  46819  stirlinglem5  46820  stirlinglem7  46822  stirlinglem11  46826  dirkertrigeqlem2  46841  fourierdlem4  46853  fourierdlem26  46875  fourierdlem30  46879  fourierdlem42  46891  fourierdlem63  46911  fourierdlem65  46913  fourierdlem72  46920  fourierdlem74  46922  fourierdlem75  46923  fourierdlem76  46924  fourierdlem80  46928  fourierdlem81  46929  fourierdlem89  46937  fourierdlem90  46938  fourierdlem91  46939  fourierdlem107  46955  fourierdlem109  46957  fouriersw  46973  etransclem1  46977  etransclem4  46980  etransclem8  46984  etransclem18  46994  etransclem20  46996  etransclem21  46997  etransclem23  46999  etransclem35  47011  etransclem46  47022  rrxtopnfi  47029  rrndistlt  47032  sge0gtfsumgt  47185  hoidmv1lelem2  47334  hoidmvlelem2  47338  smfmullem1  47533  sigarmf  47596  sigarms  47598  sigarexp  47601  sigardiv  47603  sigarcol  47606  sharhght  47607  sigaradd  47608  cevathlem2  47610  cevath  47611  sin5tlem3  47640  sin5tlem4  47641  sin5tlem5  47642  cos5t  47644  resubcnnred  48069  fldivmod  48109  ceildivmod  48110  fmtnorec2lem  48322  fmtnorec3  48328  fmtnorec4  48329  lighneallem3  48387  quad1  48413  requad01  48414  requad2  48416  fppr2odd  48524  dignn0flhalflem2  49424  affinecomb2  49511  1subrec1sub  49513  eenglngeehlnmlem1  49545  eenglngeehlnmlem2  49546  rrx2vlinest  49549  rrx2linest  49550  line2  49560  itsclc0yqsollem1  49570  itsclc0yqsol  49572  itscnhlc0xyqsol  49573  itschlc0xyqsol1  49574  itschlc0xyqsol  49575  itsclc0xyqsolr  49577  2itscplem1  49586  2itscplem2  49587  2itscplem3  49588  itscnhlinecirc02plem1  49590  inlinecirc02plem  49594  sinhpcosh  50546  i2linesd  50585