Theorem neg1rr 12299

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 11301	. 2 ⊢ 1 ∈ ℝ
2	1	renegcli 11612	1 ⊢ -1 ∈ ℝ

This proof depends on syntax axioms:   ∈ wcel 2145  ℝcr 11192  1c1 11194  -cneg 11535

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 2733  ax-sep 5249  ax-nul 5260  ax-pow 5327  ax-pr 5391  ax-un 7749  ax-resscn 11250  ax-1cn 11251  ax-icn 11252  ax-addcl 11253  ax-addrcl 11254  ax-mulcl 11255  ax-mulrcl 11256  ax-mulcom 11257  ax-addass 11258  ax-mulass 11259  ax-distr 11260  ax-i2m1 11261  ax-1ne0 11262  ax-1rid 11263  ax-rnegex 11264  ax-rrecex 11265  ax-cnre 11266  ax-pre-lttri 11267  ax-pre-lttrn 11268  ax-pre-ltadd 11269

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 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-nel 3063  df-ral 3078  df-rex 3088  df-reu 3367  df-rab 3414  df-v 3453  df-sbc 3740  df-csb 3848  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-opab 5168  df-mpt 5187  df-id 5546  df-po 5559  df-so 5560  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-rn 5662  df-res 5663  df-ima 5664  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 7375  df-ov 7421  df-oprab 7422  df-mpo 7423  df-er 8710  df-en 8967  df-dom 8968  df-sdom 8969  df-pnf 11338  df-mnf 11339  df-ltxr 11341  df-sub 11536  df-neg 11537

This theorem is used by:  inelr  12303  dfceil2  13972  bernneq  14366  sgnclre  15248  sgnnbi  15250  sgnpbi  15251  crre  15274  remim  15277  iseraltlem2  15843  iseraltlem3  15844  iseralt  15845  tanhbnd  16322  sinbnd2  16343  cosbnd2  16344  chnub  18789  psgnodpmr  21889  xrhmeo  25260  xrhmph  25261  vitalilem2  25923  vitalilem4  25925  vitali  25927  mbfneg  25964  i1fsub  26022  itg1sub  26023  i1fibl  26121  itgitg1  26122  cos0pilt1  26853  recosf1o  26856  efif1olem3  26865  relogbdiv  27100  ang180lem3  27132  1cubrlem  27162  atanre  27206  acosrecl  27224  atandmcj  27230  leibpilem2  27262  leibpi  27263  leibpisum  27264  wilthlem1  27388  wilthlem2  27389  basellem3  27403  zabsle1  27616  lgsvalmod  27636  lgsdir2lem4  27648  gausslemma2dlem6  27692  lgseisen  27699  ostth3  27958  axlowdimlem7  29519  ipidsq  31305  ipasslem10  31434  hisubcomi  31699  normlem9  31713  hmopd  32617  sgnsgn  33415  cos9thpiminplylem1  34407  signswch  35183  signstf  35188  signsvfn  35204  subfacval2  35931  iexpire  36479  bcneg1  36480  cnndvlem1  37383  irrdiff  38227  ftc1anclem5  38595  asindmre  38601  dvasin  38602  dvacos  38603  dvreasin  38604  dvreacos  38605  areacirclem1  38606  sqrtcval  44626  sqrtcval2  44627  resqrtval  44628  imsqrtval  44629  stoweidlem22  47001  etransclem46  47259  smfneg  47782  goldratval  47905  sqrtrrnpoly  47911  3exp4mod41  48670