Theorem renegcld 11668

Description: Closure law for negative of reals. (Contributed by Mario Carneiro, 27-May-2016.)

Hypothesis

Ref	Expression
renegcld.1	⊢ (𝜑 → 𝐴 ∈ ℝ)

Assertion

Ref	Expression
renegcld	⊢ (𝜑 → -𝐴 ∈ ℝ)

Proof of Theorem renegcld

Step	Hyp	Ref	Expression
1		renegcld.1	. 2 ⊢ (𝜑 → 𝐴 ∈ ℝ)
2		renegcl 11548	. 2 ⊢ (𝐴 ∈ ℝ → -𝐴 ∈ ℝ)
3	1, 2	syl 18	1 ⊢ (𝜑 → -𝐴 ∈ ℝ)

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145  ℝcr 11126  -cneg 11469

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2215  ax-ext 2734  ax-sep 5255  ax-nul 5267  ax-pow 5334  ax-pr 5402  ax-un 7739  ax-resscn 11184  ax-1cn 11185  ax-icn 11186  ax-addcl 11187  ax-addrcl 11188  ax-mulcl 11189  ax-mulrcl 11190  ax-mulcom 11191  ax-addass 11192  ax-mulass 11193  ax-distr 11194  ax-i2m1 11195  ax-1ne0 11196  ax-1rid 11197  ax-rnegex 11198  ax-rrecex 11199  ax-cnre 11200  ax-pre-lttri 11201  ax-pre-lttrn 11202  ax-pre-ltadd 11203

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2566  df-eu 2596  df-clab 2741  df-cleq 2754  df-clel 2837  df-nfc 2911  df-ne 2958  df-nel 3064  df-ral 3079  df-rex 3089  df-reu 3368  df-rab 3415  df-v 3455  df-sbc 3743  df-csb 3851  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4283  df-if 4486  df-pw 4562  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4871  df-br 5108  df-opab 5172  df-mpt 5191  df-id 5554  df-po 5567  df-so 5568  df-xp 5665  df-rel 5666  df-cnv 5667  df-co 5668  df-dm 5669  df-rn 5670  df-res 5671  df-ima 5672  df-iota 6493  df-fun 6539  df-fn 6540  df-f 6541  df-f1 6542  df-fo 6543  df-f1o 6544  df-fv 6545  df-riota 7373  df-ov 7419  df-oprab 7420  df-mpo 7421  df-er 8699  df-en 8956  df-dom 8957  df-sdom 8958  df-pnf 11272  df-mnf 11273  df-ltxr 11275  df-sub 11470  df-neg 11471

This theorem is used by:  ltord2  11770  leord2  11771  eqord2  11772  possumd  11866  recgt0  12088  riotaneg  12221  negiso  12222  nn0negleid  12583  difgtsumgt  12584  nnnegz  12621  neglt  13064  prodge0rd  13153  modsub12d  13994  monoord2  14099  discr1  14305  discr  14306  sgnmul  15182  recj  15213  reneg  15214  imcj  15221  imneg  15222  abslt  15404  absle  15405  o1lo1  15626  o1lo12  15627  icco1  15629  rlimrege0  15668  lo1sub  15720  iseraltlem2  15772  infcvgaux1i  15948  absefib  16290  efieq1re  16291  moddvds  16357  bitscmp  16532  bitsinv1lem  16535  mulgnegnn  19208  cnsubrg  21641  xrhmeo  25175  pjthlem1  25666  ivth2  25684  ovolshft  25740  shftmbl  25767  volsup2  25834  volivth  25836  mbfmulc2lem  25876  mbfposr  25881  mbfposb  25882  ismbf3d  25883  mbfmulc2  25892  mbfinf  25894  mbfi1fseqlem4  25947  mbfi1fseqlem5  25948  mbfi1fseqlem6  25949  mbfi1flimlem  25951  itg2monolem1  25979  iblposlem  26021  iblre  26023  itgreval  26026  itgneg  26033  i1fibl  26037  itgitg1  26038  itgle  26039  ibladd  26050  itgaddlem2  26053  iblabslem  26057  itgmulc2lem2  26062  itgmulc2  26063  bddiblnc  26071  dvferm2lem  26215  dvferm2  26216  rolle  26219  dvivth  26239  lhop2  26244  dvfsumge  26251  dvfsumlem2  26256  dvfsum2  26263  coseq0negpitopi  26738  tanabsge  26741  tanord  26773  tanregt0  26774  abslogimle  26808  logcj  26841  argimgt0  26847  logdiv2  26852  logcnlem3  26879  logccv  26898  abscxpbnd  26988  logreclem  26997  asinlem3a  27105  asinneg  27121  atanlogsublem  27150  atantan  27158  atans2  27166  birthdaylem3  27188  cxplim  27206  amgmlem  27224  emcllem7  27236  zetacvg  27249  eldmgm  27256  lgamgulmlem2  27264  lgsneg  27555  lgsdilem  27558  lgseisenlem1  27609  pntpbnd1  27820  pntibndlem2  27825  padicabvcxp  27866  ostth3  27872  axsegconlem9  29368  nvabs  31139  pjhthlem1  31858  xlt2addrd  33217  expgt0b  33274  oexpled  33293  ccfldextdgrr  34169  constrnegcl  34260  iconstr  34263  constrremulcl  34264  constrmulcl  34268  constrresqrtcl  34274  cos9thpiminplylem1  34279  xrge0iifcnv  34430  xrge0iifiso  34432  xrge0iifhom  34434  dya2ub  34768  signsply0  35046  fdvneggt  35095  fdvnegge  35097  climlec3  36300  poimirlem29  38385  itg2gt0cn  38411  ibladdnc  38413  itgaddnclem2  38415  iblabsnclem  38419  itgmulc2nclem2  38423  itgmulc2nc  38424  ftc1anclem5  38433  dvasin  38440  areacirclem1  38444  areacirclem4  38447  areacirclem5  38448  areacirc  38449  posbezout  42953  bcle2d  43032  aks6d1c7lem1  43033  oexpreposd  43184  3cubeslem4  43521  pellexlem6  43662  pell1234qrdich  43689  acongeq  43811  sqrtcval  44468  radcnvrat  45125  binomcxplemdvbinom  45164  binomcxplemnotnn0  45167  infnsuprnmpt  46066  fperiodmul  46124  supsubc  46170  ltmulneg  46208  rexabslelem  46233  supminfrnmpt  46260  leneg2d  46263  leneg3d  46272  supminfxr  46279  climliminflimsupd  46616  liminfreuzlem  46617  liminfltlem  46619  stoweidlem1  46816  stoweidlem7  46822  stoweidlem13  46828  stoweidlem23  46838  stoweidlem34  46849  stoweidlem42  46857  stoweidlem47  46862  stirlinglem6  46894  stirlinglem10  46898  fourierdlem24  46946  fourierdlem39  46961  fourierdlem40  46962  fourierdlem43  46965  fourierdlem44  46966  fourierdlem46  46967  fourierdlem48  46969  fourierdlem49  46970  fourierdlem58  46979  fourierdlem62  46983  fourierdlem72  46993  fourierdlem78  46999  fourierdlem83  47004  fourierdlem85  47006  fourierdlem88  47009  fourierdlem92  47013  fourierdlem97  47018  fourierdlem103  47024  fourierdlem104  47025  fourierdlem109  47030  fourierdlem111  47032  fourierdlem112  47033  sqwvfoura  47043  etransclem23  47072  etransclem46  47095  hoicvr  47363  hoicvrrex  47371  smfinflem  47632  smfliminflem  47645  finfdm  47661  smfinfdmmbllem  47663  sigaradd  47681  squeezedltsq  47717  sqrtnegnre  48182  proththd  48504  requad01  48524  requad1  48525  requad2  48526  dignn0flhalflem1  49532  eenglngeehlnmlem1  49654  eenglngeehlnmlem2  49655  line2ylem  49668  itscnhlc0yqe  49676  itsclquadb  49693  itscnhlinecirc02p  49702  amgmwlem  50807