Theorem neg1rr 12136

Description: -1 is a real number. (Contributed by David A. Wheeler, 5-Dec-2018.)

Assertion

Ref	Expression
neg1rr	⊢ -1 ∈ ℝ

Proof of Theorem neg1rr

Step	Hyp	Ref	Expression
1		1re 11135	. 2 ⊢ 1 ∈ ℝ
2	1	renegcli 11446	1 ⊢ -1 ∈ ℝ

Syntax hints:   ∈ wcel 2114  ℝcr 11028  1c1 11030  -cneg 11369

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5231  ax-nul 5241  ax-pow 5302  ax-pr 5370  ax-un 7682  ax-resscn 11086  ax-1cn 11087  ax-icn 11088  ax-addcl 11089  ax-addrcl 11090  ax-mulcl 11091  ax-mulrcl 11092  ax-mulcom 11093  ax-addass 11094  ax-mulass 11095  ax-distr 11096  ax-i2m1 11097  ax-1ne0 11098  ax-1rid 11099  ax-rnegex 11100  ax-rrecex 11101  ax-cnre 11102  ax-pre-lttri 11103  ax-pre-lttrn 11104  ax-pre-ltadd 11105

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-nel 3038  df-ral 3053  df-rex 3063  df-reu 3344  df-rab 3391  df-v 3432  df-sbc 3730  df-csb 3839  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-pw 4544  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-br 5087  df-opab 5149  df-mpt 5168  df-id 5519  df-po 5532  df-so 5533  df-xp 5630  df-rel 5631  df-cnv 5632  df-co 5633  df-dm 5634  df-rn 5635  df-res 5636  df-ima 5637  df-iota 6448  df-fun 6494  df-fn 6495  df-f 6496  df-f1 6497  df-fo 6498  df-f1o 6499  df-fv 6500  df-riota 7317  df-ov 7363  df-oprab 7364  df-mpo 7365  df-er 8636  df-en 8887  df-dom 8888  df-sdom 8889  df-pnf 11172  df-mnf 11173  df-ltxr 11175  df-sub 11370  df-neg 11371

This theorem is referenced by:  inelr  12140  dfceil2  13789  bernneq  14182  crre  15067  remim  15070  iseraltlem2  15636  iseraltlem3  15637  iseralt  15638  tanhbnd  16119  sinbnd2  16140  cosbnd2  16141  chnub  18579  psgnodpmr  21580  xrhmeo  24923  xrhmph  24924  vitalilem2  25586  vitalilem4  25588  vitali  25590  mbfneg  25627  i1fsub  25685  itg1sub  25686  i1fibl  25785  itgitg1  25786  cos0pilt1  26509  recosf1o  26512  efif1olem3  26521  relogbdiv  26756  ang180lem3  26788  1cubrlem  26818  atanre  26862  acosrecl  26880  atandmcj  26886  leibpilem2  26918  leibpi  26919  leibpisum  26920  wilthlem1  27045  wilthlem2  27046  basellem3  27060  zabsle1  27273  lgsvalmod  27293  lgsdir2lem4  27305  gausslemma2dlem6  27349  lgseisen  27356  ostth3  27615  axlowdimlem7  29031  ipidsq  30796  ipasslem10  30925  hisubcomi  31190  normlem9  31204  hmopd  32108  sgnclre  32920  sgnnbi  32926  sgnpbi  32927  sgnsgn  32929  cos9thpiminplylem1  33942  signswch  34721  signstf  34726  signsvfn  34742  subfacval2  35385  iexpire  35933  bcneg1  35934  cnndvlem1  36813  irrdiff  37656  ftc1anclem5  38032  asindmre  38038  dvasin  38039  dvacos  38040  dvreasin  38041  dvreacos  38042  areacirclem1  38043  sqrtcval  44086  sqrtcval2  44087  resqrtval  44088  imsqrtval  44089  stoweidlem22  46468  etransclem46  46726  smfneg  47249  3exp4mod41  48091