Theorem renegcld 11712

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

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

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 2213  ax-ext 2732  ax-sep 5248  ax-nul 5259  ax-pow 5326  ax-pr 5390  ax-un 7734  ax-resscn 11228  ax-1cn 11229  ax-icn 11230  ax-addcl 11231  ax-addrcl 11232  ax-mulcl 11233  ax-mulrcl 11234  ax-mulcom 11235  ax-addass 11236  ax-mulass 11237  ax-distr 11238  ax-i2m1 11239  ax-1ne0 11240  ax-1rid 11241  ax-rnegex 11242  ax-rrecex 11243  ax-cnre 11244  ax-pre-lttri 11245  ax-pre-lttrn 11246  ax-pre-ltadd 11247

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 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-dif 3901  df-un 3903  df-in 3905  df-ss 3915  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 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 6483  df-fun 6529  df-fn 6530  df-f 6531  df-f1 6532  df-fo 6533  df-f1o 6534  df-fv 6535  df-riota 7365  df-ov 7411  df-oprab 7412  df-mpo 7413  df-er 8695  df-en 8952  df-dom 8953  df-sdom 8954  df-pnf 11316  df-mnf 11317  df-ltxr 11319  df-sub 11514  df-neg 11515

This theorem is used by:  ltord2  11814  leord2  11815  eqord2  11816  possumd  11910  recgt0  12132  riotaneg  12265  negiso  12266  nn0negleid  12627  difgtsumgt  12628  nnnegz  12665  neglt  13109  prodge0rd  13198  modsub12d  14039  monoord2  14144  discr1  14350  discr  14351  sgnmul  15227  recj  15258  reneg  15259  imcj  15266  imneg  15267  abslt  15449  absle  15450  o1lo1  15671  o1lo12  15672  icco1  15674  rlimrege0  15713  lo1sub  15765  iseraltlem2  15817  infcvgaux1i  15993  absefib  16333  efieq1re  16334  moddvds  16400  bitscmp  16575  bitsinv1lem  16578  mulgnegnn  19255  cnsubrg  21694  xrhmeo  25228  pjthlem1  25719  ivth2  25737  ovolshft  25793  shftmbl  25820  volsup2  25887  volivth  25889  mbfmulc2lem  25929  mbfposr  25934  mbfposb  25935  ismbf3d  25936  mbfmulc2  25945  mbfinf  25947  mbfi1fseqlem4  26000  mbfi1fseqlem5  26001  mbfi1fseqlem6  26002  mbfi1flimlem  26004  itg2monolem1  26032  iblposlem  26073  iblre  26075  itgreval  26078  itgneg  26085  i1fibl  26089  itgitg1  26090  itgle  26091  ibladd  26102  itgaddlem2  26105  iblabslem  26109  itgmulc2lem2  26114  itgmulc2  26115  bddiblnc  26123  dvferm2lem  26267  dvferm2  26268  rolle  26271  dvivth  26291  lhop2  26296  dvfsumge  26303  dvfsumlem2  26308  dvfsum2  26315  coseq0negpitopi  26795  tanabsge  26798  tanord  26829  tanregt0  26830  abslogimle  26864  logcj  26897  argimgt0  26903  logdiv2  26908  logcnlem3  26935  logccv  26954  abscxpbnd  27044  logreclem  27053  asinlem3a  27161  asinneg  27177  atanlogsublem  27206  atantan  27214  atans2  27222  birthdaylem3  27244  cxplim  27262  amgmlem  27280  emcllem7  27292  zetacvg  27305  eldmgm  27312  lgamgulmlem2  27320  lgsneg  27611  lgsdilem  27614  lgseisenlem1  27665  pntpbnd1  27876  pntibndlem2  27881  padicabvcxp  27922  ostth3  27928  axsegconlem9  29436  nvabs  31207  pjhthlem1  31926  xlt2addrd  33284  expgt0b  33341  oexpled  33360  ccfldextdgrr  34237  constrnegcl  34328  iconstr  34331  constrremulcl  34332  constrmulcl  34336  constrresqrtcl  34342  cos9thpiminplylem1  34347  xrge0iifcnv  34498  xrge0iifiso  34500  xrge0iifhom  34502  dya2ub  34836  signsply0  35114  fdvneggt  35163  fdvnegge  35165  climlec3  36420  poimirlem29  38487  itg2gt0cn  38513  ibladdnc  38515  itgaddnclem2  38517  iblabsnclem  38521  itgmulc2nclem2  38525  itgmulc2nc  38526  ftc1anclem5  38535  dvasin  38542  areacirclem1  38546  areacirclem4  38549  areacirclem5  38550  areacirc  38551  posbezout  43070  bcle2d  43149  aks6d1c7lem1  43150  oexpreposd  43301  3cubeslem4  43638  pellexlem6  43779  pell1234qrdich  43806  acongeq  43928  sqrtcval  44585  radcnvrat  45242  binomcxplemdvbinom  45281  binomcxplemnotnn0  45284  infnsuprnmpt  46183  fperiodmul  46241  supsubc  46287  ltmulneg  46325  rexabslelem  46350  supminfrnmpt  46377  leneg2d  46380  leneg3d  46389  supminfxr  46396  climliminflimsupd  46733  liminfreuzlem  46734  liminfltlem  46736  stoweidlem1  46933  stoweidlem7  46939  stoweidlem13  46945  stoweidlem23  46955  stoweidlem34  46966  stoweidlem42  46974  stoweidlem47  46979  stirlinglem6  47011  stirlinglem10  47015  fourierdlem24  47063  fourierdlem39  47078  fourierdlem40  47079  fourierdlem43  47082  fourierdlem44  47083  fourierdlem46  47084  fourierdlem48  47086  fourierdlem49  47087  fourierdlem58  47096  fourierdlem62  47100  fourierdlem72  47110  fourierdlem78  47116  fourierdlem83  47121  fourierdlem85  47123  fourierdlem88  47126  fourierdlem92  47130  fourierdlem97  47135  fourierdlem103  47141  fourierdlem104  47142  fourierdlem109  47147  fourierdlem111  47149  fourierdlem112  47150  sqwvfoura  47160  etransclem23  47189  etransclem46  47212  hoicvr  47480  hoicvrrex  47488  smfinflem  47749  smfliminflem  47762  finfdm  47778  smfinfdmmbllem  47780  sigaradd  47798  squeezedltsq  47834  sqrtnegnre  48299  proththd  48621  requad01  48641  requad1  48642  requad2  48643  dignn0flhalflem1  49649  eenglngeehlnmlem1  49771  eenglngeehlnmlem2  49772  line2ylem  49785  itscnhlc0yqe  49793  itsclquadb  49810  itscnhlinecirc02p  49819  amgmwlem  50909