Theorem renegcld 11743

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 11621	. 2 ⊢ (𝐴 ∈ ℝ → -𝐴 ∈ ℝ)
3	1, 2	syl 18	1 ⊢ (𝜑 → -𝐴 ∈ ℝ)

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2144  ℝcr 11199   -cneg 11542

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-10 2177  ax-11 2193  ax-12 2212  ax-ext 2732  ax-sep 5248  ax-nul 5259  ax-pow 5326  ax-pr 5390  ax-un 7751  ax-resscn 11257  ax-1cn 11258  ax-icn 11259  ax-addcl 11260  ax-addrcl 11261  ax-mulcl 11262  ax-mulrcl 11263  ax-mulcom 11264  ax-addass 11265  ax-mulass 11266  ax-distr 11267  ax-i2m1 11268  ax-1ne0 11269  ax-1rid 11270  ax-rnegex 11271  ax-rrecex 11272  ax-cnre 11273  ax-pre-lttri 11274  ax-pre-lttrn 11275  ax-pre-ltadd 11276

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-nf 1816  df-sb 2099  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-nel 3062  df-ral 3077  df-rex 3087  df-reu 3366  df-rab 3413  df-v 3452  df-sbc 3739  df-csb 3847  df-ss 3896  df-dif 4047  df-in 4091  df-un 4151  df-nul 4279  df-if 4482  df-pw 4558  df-sn 4584  df-pr 4586  df-op 4590  df-uni 4867  df-br 5103  df-opab 5167  df-mpt 5186  df-id 5545  df-po 5558  df-so 5559  df-xp 5656  df-rel 5657  df-cnv 5658  df-co 5659  df-dm 5660  df-rn 5661  df-res 5662  df-ima 5663  df-iota 6494  df-fun 6540  df-fn 6541  df-f 6542  df-f1 6543  df-fo 6544  df-f1o 6545  df-fv 6546  df-riota 7377  df-ov 7423  df-oprab 7424  df-mpo 7425  df-er 8717  df-en 8974  df-dom 8975  df-sdom 8976  df-pnf 11345  df-mnf 11346  df-ltxr 11348  df-sub 11543  df-neg 11544

This theorem is used by:  ltord2  11845  leord2  11846  eqord2  11847  possumd  11941  recgt0  12163  riotaneg  12296  negiso  12297  nn0negleid  12658  difgtsumgt  12659  nnnegz  12696  neglt  13140  prodge0rd  13229  modsub12d  14071  monoord2  14176  discr1  14383  discr  14384  sgnmul  15260  recj  15291  reneg  15292  imcj  15299  imneg  15300  abslt  15482  absle  15483  o1lo1  15704  o1lo12  15705  icco1  15707  rlimrege0  15746  lo1sub  15798  iseraltlem2  15850  infcvgaux1i  16026  absefib  16366  efieq1re  16367  moddvds  16433  bitscmp  16608  bitsinv1lem  16611  mulgnegnn  19294  cnsubrg  21733  xrhmeo  25267  pjthlem1  25758  ivth2  25776  ovolshft  25832  shftmbl  25859  volsup2  25926  volivth  25928  mbfmulc2lem  25968  mbfposr  25973  mbfposb  25974  ismbf3d  25975  mbfmulc2  25984  mbfinf  25986  mbfi1fseqlem4  26039  mbfi1fseqlem5  26040  mbfi1fseqlem6  26041  mbfi1flimlem  26043  itg2monolem1  26071  iblposlem  26112  iblre  26114  itgreval  26117  itgneg  26124  i1fibl  26128  itgitg1  26129  itgle  26130  ibladd  26141  itgaddlem2  26144  iblabslem  26148  itgmulc2lem2  26153  itgmulc2  26154  bddiblnc  26162  dvferm2lem  26306  dvferm2  26307  rolle  26310  dvivth  26330  lhop2  26335  dvfsumge  26342  dvfsumlem2  26347  dvfsum2  26354  coseq0negpitopi  26832  tanabsge  26835  tanord  26866  tanregt0  26867  abslogimle  26901  logcj  26934  argimgt0  26940  logdiv2  26945  logcnlem3  26972  logccv  26991  abscxpbnd  27081  logreclem  27090  asinlem3a  27198  asinneg  27214  atanlogsublem  27243  atantan  27251  atans2  27259  birthdaylem3  27281  cxplim  27299  amgmlem  27317  emcllem7  27329  zetacvg  27342  eldmgm  27349  lgamgulmlem2  27357  lgsneg  27648  lgsdilem  27651  lgseisenlem1  27702  pntpbnd1  27913  pntibndlem2  27918  padicabvcxp  27959  ostth3  27965  axsegconlem9  29503  nvabs  31274  pjhthlem1  31993  xlt2addrd  33351  expgt0b  33408  oexpled  33427  ccfldextdgrr  34304  constrnegcl  34395  iconstr  34398  constrremulcl  34399  constrmulcl  34403  constrresqrtcl  34409  cos9thpiminplylem1  34414  xrge0iifcnv  34565  xrge0iifiso  34567  xrge0iifhom  34569  dya2ub  34902  signsply0  35180  fdvneggt  35229  fdvnegge  35231  climlec3  36499  poimirlem29  38568  itg2gt0cn  38594  ibladdnc  38596  itgaddnclem2  38598  iblabsnclem  38602  itgmulc2nclem2  38606  itgmulc2nc  38607  ftc1anclem5  38616  dvasin  38623  areacirclem1  38627  areacirclem4  38630  areacirclem5  38631  areacirc  38632  posbezout  43151  bcle2d  43230  aks6d1c7lem1  43231  oexpreposd  43380  3cubeslem4  43700  pellexlem6  43841  pell1234qrdich  43868  acongeq  43990  sqrtcval  44641  radcnvrat  45298  binomcxplemdvbinom  45337  binomcxplemnotnn0  45340  infnsuprnmpt  46262  fperiodmul  46320  supsubc  46365  ltmulneg  46403  rexabslelem  46428  supminfrnmpt  46455  leneg2d  46458  leneg3d  46467  supminfxr  46474  climliminflimsupd  46811  liminfreuzlem  46812  liminfltlem  46814  stoweidlem1  47011  stoweidlem7  47017  stoweidlem13  47023  stoweidlem23  47033  stoweidlem34  47044  stoweidlem42  47052  stoweidlem47  47057  stirlinglem6  47089  stirlinglem10  47093  fourierdlem24  47141  fourierdlem39  47156  fourierdlem40  47157  fourierdlem43  47160  fourierdlem44  47161  fourierdlem46  47162  fourierdlem48  47164  fourierdlem49  47165  fourierdlem58  47174  fourierdlem62  47178  fourierdlem72  47188  fourierdlem78  47194  fourierdlem83  47199  fourierdlem85  47201  fourierdlem88  47204  fourierdlem92  47208  fourierdlem97  47213  fourierdlem103  47219  fourierdlem104  47220  fourierdlem109  47225  fourierdlem111  47227  fourierdlem112  47228  sqwvfoura  47238  etransclem23  47267  etransclem46  47290  hoicvr  47558  hoicvrrex  47566  smfinflem  47827  smfliminflem  47840  finfdm  47856  smfinfdmmbllem  47858  sigaradd  47876  squeezedltsq  47912  sqrtnegnre  48377  proththd  48699  requad01  48719  requad1  48720  requad2  48721  dignn0flhalflem1  49727  eenglngeehlnmlem1  49849  eenglngeehlnmlem2  49850  line2ylem  49863  itscnhlc0yqe  49871  itsclquadb  49888  itscnhlinecirc02p  49897  amgmwlem  50987