Theorem 2re 12267

Description: The number 2 is real. (Contributed by NM, 27-May-1999.)

Assertion

Ref	Expression
2re	⊢ 2 ∈ ℝ

Proof of Theorem 2re

Step	Hyp	Ref	Expression
1		df-2 12256	. 2 ⊢ 2 = (1 + 1)
2		1re 11181	. . 3 ⊢ 1 ∈ ℝ
3	2, 2	readdcli 11196	. 2 ⊢ (1 + 1) ∈ ℝ
4	1, 3	eqeltri 2825	1 ⊢ 2 ∈ ℝ

Syntax hints:   ∈ wcel 2109  (class class class)co 7390  ℝcr 11074  1c1 11076   + caddc 11078  2c2 12248

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2702  ax-1cn 11133  ax-icn 11134  ax-addcl 11135  ax-addrcl 11136  ax-mulcl 11137  ax-mulrcl 11138  ax-i2m1 11143  ax-1ne0 11144  ax-rrecex 11147  ax-cnre 11148

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-ne 2927  df-ral 3046  df-rex 3055  df-rab 3409  df-v 3452  df-dif 3920  df-un 3922  df-ss 3934  df-nul 4300  df-if 4492  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4875  df-br 5111  df-iota 6467  df-fv 6522  df-ov 7393  df-2 12256

This theorem is referenced by:  2cnALT  12269  3re  12273  3pos  12298  2lt3  12360  1lt3  12361  2lt4  12363  1lt4  12364  2lt5  12367  2lt6  12372  1lt6  12373  2lt7  12378  1lt7  12379  2lt8  12385  1lt8  12386  2lt9  12393  1lt9  12394  1le2  12397  2rene0  12399  halfre  12402  halfgt0  12404  halflt1  12406  rehalfcl  12416  halfpos2  12418  halfnneg2  12420  addltmul  12425  nominpos  12426  avglt1  12427  avglt2  12428  div4p1lem1div2  12444  nn0lele2xi  12505  nn0n0n1ge2b  12518  nn0ge2m1nn  12519  nn0le2is012  12605  halfnz  12619  3halfnz  12620  2lt10  12794  1lt10  12795  uzuzle23  12850  uzuzle24  12851  uz3m2nn  12860  2rp  12963  ge2halflem1  13075  xnn0n0n1ge2b  13099  fztpval  13554  fz0to4untppr  13598  fz0to5un2tp  13599  fzo0to42pr  13721  flhalf  13799  fldiv4p1lem1div2  13804  2txmodxeq0  13903  expubnd  14150  expmulnbnd  14207  nn0opthlem2  14241  faclbnd2  14263  faclbnd4lem1  14265  faclbnd5  14270  4bc2eq6  14301  hashgt23el  14396  hashfun  14409  hashge2el2dif  14452  hashge2el2difr  14453  hash3tpde  14465  wrdlenge2n0  14524  f1oun2prg  14890  01sqrexlem7  15221  sqrt4  15245  sqrt2gt1lt2  15247  abstri  15304  sqreulem  15333  amgm2  15343  caucvgrlem  15646  climcndslem1  15822  climcndslem2  15823  climcnds  15824  efcllem  16050  ege2le3  16063  ef01bndlem  16159  cos01bnd  16161  cos2bnd  16163  cos01gt0  16166  sin02gt0  16167  sincos2sgn  16169  sin4lt0  16170  eirrlem  16179  egt2lt3  16181  epos  16182  ene1  16185  sqrt2re  16225  mod2eq1n2dvds  16324  oddge22np1  16326  evennn2n  16328  nn0o1gt2  16358  nno  16359  nn0o  16360  nnoddm1d2  16363  bitsp1o  16410  bitsfzolem  16411  bitsfzo  16412  bitsfi  16414  6gcd4e2  16515  2mulprm  16670  ge2nprmge4  16678  isprm7  16685  3lcm2e6  16709  prmreclem2  16895  prmreclem6  16899  4sqlem11  16933  4sqlem12  16934  prmgaplem7  17035  2expltfac  17070  plusgndxnmulrndx  17267  starvndxnplusgndx  17275  scandxnplusgndx  17287  vscandxnplusgndx  17292  ipndxnplusgndx  17303  tsetndxnplusgndx  17327  plendxnplusgndx  17341  dsndxnplusgndx  17360  slotsdifunifndx  17371  efgredleme  19680  zringndrg  21385  chfacfscmul0  22752  chfacfpmmul0  22756  psmetge0  24207  xmetge0  24239  bl2in  24295  metnrmlem3  24757  iihalf1  24832  iihalf2  24835  pcoass  24931  tcphcphlem1  25142  csbren  25306  trirn  25307  minveclem2  25333  minveclem4  25339  pjthlem1  25344  ovolunlem1a  25404  dyadss  25502  opnmbllem  25509  vitalilem2  25517  vitalilem4  25519  mbfi1fseqlem5  25627  lhop1lem  25925  aaliou3lem2  26258  aaliou3lem8  26260  pilem2  26369  pilem3  26370  pipos  26375  sinhalfpilem  26379  sincosq1lem  26413  sincosq4sgn  26417  tangtx  26421  sinq12gt0  26423  sincos4thpi  26429  tan4thpi  26430  tan4thpiOLD  26431  sincos6thpi  26432  sineq0  26440  cos02pilt1  26442  cosq34lt1  26443  cosordlem  26446  cos0pilt1  26448  tanord1  26453  efif1olem1  26458  efif1olem2  26459  efif1olem4  26461  efif1o  26462  efifo  26463  2irrexpq  26647  cxpcn3lem  26664  root1id  26671  root1eq1  26672  root1cj  26673  cxpeq  26674  2logb9irr  26712  2logb3irr  26714  ang180lem1  26726  ang180lem2  26727  chordthmlem2  26750  1cubrlem  26758  atancj  26827  atantan  26840  atanbndlem  26842  atans2  26848  leibpi  26859  log2tlbnd  26862  log2ublem2  26864  log2ub  26866  divsqrtsumlem  26897  harmonicbnd3  26925  zetacvg  26932  lgamgulmlem2  26947  lgamgulmlem3  26948  lgamgulmlem4  26949  lgamgulmlem6  26951  lgamucov  26955  basellem1  26998  basellem2  26999  basellem3  27000  basellem5  27002  chtdif  27075  ppidif  27080  ppinncl  27091  chtrpcl  27092  ppieq0  27093  ppiltx  27094  ppiublem1  27120  ppiub  27122  chpeq0  27126  chteq0  27127  chtublem  27129  chtub  27130  chpval2  27136  chpub  27138  mersenne  27145  perfectlem1  27147  perfectlem2  27148  dchrptlem1  27182  dchrptlem2  27183  bcmono  27195  bclbnd  27198  bpos1lem  27200  bposlem1  27202  bposlem2  27203  bposlem3  27204  bposlem4  27205  bposlem5  27206  bposlem6  27207  bposlem7  27208  bposlem8  27209  bposlem9  27210  lgslem1  27215  lgsdirprm  27249  gausslemma2dlem0c  27276  gausslemma2dlem1a  27283  gausslemma2dlem2  27285  gausslemma2dlem3  27286  lgseisenlem1  27293  lgseisenlem2  27294  lgseisenlem3  27295  lgseisen  27297  lgsquadlem1  27298  lgsquadlem2  27299  m1lgs  27306  2lgslem1a1  27307  2lgslem1a2  27308  2lgslem1c  27311  2lgslem4  27324  2sqlem11  27347  2sq2  27351  2sqreultlem  27365  2sqreunnltlem  27368  chebbnd1lem1  27387  chebbnd1lem2  27388  chebbnd1lem3  27389  chebbnd1  27390  chtppilimlem1  27391  chtppilimlem2  27392  chtppilim  27393  chto1ub  27394  chebbnd2  27395  chto1lb  27396  chpchtlim  27397  chpo1ub  27398  chpo1ubb  27399  rplogsumlem1  27402  rplogsumlem2  27403  dchrisumlem2  27408  dchrisumlem3  27409  dchrvmasumiflem1  27419  dchrisum0fno1  27429  dchrisum0re  27431  dchrisum0lem1b  27433  dchrisum0lem1  27434  dchrisum0lem2  27436  rplogsum  27445  mulog2sumlem1  27452  mulog2sumlem2  27453  log2sumbnd  27462  selberglem2  27464  selbergb  27467  selberg2b  27470  chpdifbndlem1  27471  logdivbnd  27474  selberg3lem1  27475  selberg3  27477  selberg4lem1  27478  selberg4  27479  pntrmax  27482  pntrsumbnd2  27485  selberg3r  27487  selberg4r  27488  selberg34r  27489  pntrlog2bndlem2  27496  pntrlog2bndlem3  27497  pntrlog2bndlem4  27498  pntrlog2bndlem5  27499  pntrlog2bndlem6  27501  pntrlog2bnd  27502  pntpbnd1a  27503  pntpbnd1  27504  pntpbnd2  27505  pntpbnd  27506  pntibndlem2  27509  pntibndlem3  27510  pntibnd  27511  pntlemb  27515  pntlemg  27516  pntlemh  27517  pntlemr  27520  pntlemk  27524  pntlemo  27525  pnt2  27531  pnt  27532  ostth2lem1  27536  ostth3  27556  slotsinbpsd  28375  slotslnbpsd  28376  istrkg3ld  28395  tgldimor  28436  trgcgrg  28449  tgcgr4  28465  axlowdimlem6  28881  axlowdimlem16  28891  axlowdimlem17  28892  axlowdim  28895  upgrfi  29025  umgrupgr  29037  umgrislfupgrlem  29056  umgrislfupgr  29057  lfgrnloop  29059  usgruspgr  29114  usgrislfuspgr  29121  lfuhgr1v0e  29188  usgrexmpldifpr  29192  usgrexmplef  29193  nbusgrvtxm1  29313  vdegp1bi  29472  upgrewlkle2  29541  lfgrwlkprop  29622  upgr2pthnlp  29669  usgr2pthlem  29700  pthdlem1  29703  wwlksm1edg  29818  wwlksnextwrd  29834  wwlksnextfun  29835  wwlksnextinj  29836  wwlksnextproplem3  29848  clwlkclwwlklem2a1  29928  clwlkclwwlklem2a2  29929  clwlkclwwlklem2fv1  29931  clwlkclwwlklem2fv2  29932  clwlkclwwlklem2a4  29933  clwlkclwwlklem2a  29934  clwlkclwwlklem2  29936  clwlkclwwlk2  29939  clwlkclwwlkf  29944  clwwlkext2edg  29992  konigsbergiedgw  30184  konigsbergssiedgw  30186  konigsberglem1  30188  konigsberglem2  30189  konigsberglem3  30190  konigsberg  30193  frgrreggt1  30329  ex-pss  30364  ex-res  30377  ex-fv  30379  ex-fl  30383  ex-mod  30385  ex-abs  30391  nrt2irr  30409  ipidsq  30646  minvecolem2  30811  minvecolem4  30816  normlem7  31052  norm-ii-i  31073  norm3lemt  31088  normpar2i  31092  bcsiALT  31115  pjhthlem1  31327  opsqrlem6  32081  cdj3lem1  32370  addltmulALT  32382  nexple  32776  2exple2exp  32777  threehalves  32842  pfx1s2  32867  wrdt2ind  32882  cyc3conja  33121  drngidlhash  33412  evl1deg3  33554  rtelextdg2lem  33723  fldext2chn  33725  constraddcl  33759  iconstr  33763  2sqr3minply  33777  2sqr3nconstr  33778  cos9thpinconstrlem1  33786  cos9thpinconstrlem2  33787  sqsscirc1  33905  dya2iocucvr  34282  omssubadd  34298  oddpwdc  34352  eulerpartlemgc  34360  fibp1  34399  coinfliplem  34477  coinflipspace  34479  ballotlem2  34487  signstfveq0  34575  prodfzo03  34601  hgt750lemd  34646  logdivsqrle  34648  hgt750lem  34649  hgt750lem2  34650  hgt750leme  34656  lfuhgr2  35113  usgrcyclgt2v  35125  acycgr2v  35144  subfacp1lem1  35173  subfacp1lem5  35178  subfacval3  35183  problem2  35660  problem5  35663  circum  35668  nn0prpwlem  36317  dnibndlem10  36482  knoppcnlem2  36489  knoppcnlem4  36491  knoppcnlem10  36497  unbdqndv2lem1  36504  knoppndvlem1  36507  knoppndvlem10  36516  knoppndvlem11  36517  knoppndvlem12  36518  knoppndvlem14  36520  knoppndvlem15  36521  knoppndvlem17  36523  knoppndvlem18  36524  knoppndvlem19  36525  knoppndvlem20  36526  knoppndvlem21  36527  cnndvlem1  36532  taupi  37318  iccioo01  37322  relowlpssretop  37359  sin2h  37611  cos2h  37612  tan2h  37613  poimirlem7  37628  poimirlem9  37630  opnmbllem0  37657  mblfinlem1  37658  mblfinlem2  37659  itg2addnclem  37672  isbnd2  37784  isbnd3  37785  heiborlem7  37818  12gcd5e1  41998  lcm2un  42009  lcmineqlem19  42042  lcmineqlem20  42043  lcmineqlem22  42045  3lexlogpow5ineq2  42050  3lexlogpow5ineq4  42051  3lexlogpow5ineq3  42052  3lexlogpow2ineq1  42053  3lexlogpow2ineq2  42054  3lexlogpow5ineq5  42055  aks4d1lem1  42057  aks4d1p1p3  42064  aks4d1p1p2  42065  aks4d1p1p4  42066  aks4d1p1p6  42068  aks4d1p1p7  42069  aks4d1p1p5  42070  aks4d1p1  42071  aks4d1p2  42072  aks4d1p3  42073  aks4d1p5  42075  aks4d1p6  42076  aks4d1p7d1  42077  aks4d1p7  42078  aks4d1p8  42082  aks4d1p9  42083  posbezout  42095  aks6d1c3  42118  2np3bcnp1  42139  2ap1caineq  42140  aks6d1c6lem4  42168  aks6d1c7lem1  42175  aks6d1c7lem2  42176  oexpreposd  42317  asin1half  42352  remul02  42400  sn-0ne2  42401  remul01  42402  flt4lem7  42654  rabren3dioph  42810  pellexlem2  42825  pellexlem5  42828  pell14qrgapw  42871  pellfundex  42881  rmspecsqrtnq  42901  jm2.24nn  42955  jm2.17a  42956  jm2.17b  42957  jm2.17c  42958  acongrep  42976  acongeq  42979  jm2.22  42991  jm2.23  42992  jm2.20nn  42993  jm3.1lem2  43014  expdiophlem1  43017  sqrtcval  43637  imo72b2lem0  44161  lhe4.4ex1a  44325  isosctrlem1ALT  44930  sineq0ALT  44933  lt3addmuld  45306  suplesup  45342  infleinflem2  45374  infleinf  45375  sumnnodd  45635  0ellimcdiv  45654  sinaover2ne0  45873  stoweidlem13  46018  stoweidlem14  46019  stoweidlem26  46031  stoweidlem49  46054  stoweidlem52  46057  wallispilem4  46073  wallispilem5  46074  wallispi  46075  wallispi2lem1  46076  wallispi2lem2  46077  wallispi2  46078  stirlinglem1  46079  stirlinglem3  46081  stirlinglem5  46083  stirlinglem6  46084  stirlinglem7  46085  stirlinglem10  46088  stirlinglem11  46089  stirlinglem15  46093  stirlingr  46095  dirker2re  46097  dirkerval2  46099  dirkerre  46100  dirkerper  46101  dirkertrigeqlem1  46103  dirkertrigeqlem3  46105  dirkercncflem1  46108  dirkercncflem2  46109  dirkercncflem4  46111  fourierdlem24  46136  fourierdlem43  46155  fourierdlem44  46156  fourierdlem57  46168  fourierdlem58  46169  fourierdlem62  46173  fourierdlem66  46177  fourierdlem68  46179  fourierdlem72  46183  fourierdlem76  46187  fourierdlem78  46189  fourierdlem79  46190  fourierdlem94  46205  fourierdlem103  46214  fourierdlem104  46215  fourierdlem111  46222  fourierdlem113  46224  sqwvfoura  46233  sqwvfourb  46234  fourierswlem  46235  fouriersw  46236  etransclem23  46262  salexct2  46344  salexct3  46347  salgencntex  46348  salgensscntex  46349  sge0ad2en  46436  ovnsubaddlem1  46575  smfmullem4  46799  smf2id  46806  2leaddle2  47303  p1lep2  47305  2ltceilhalf  47333  ceilhalfgt1  47334  2tceilhalfelfzo1  47337  rehalfge1  47340  ceilhalfnn  47341  ceil5half3  47345  difmodm1lt  47364  fmtnoge3  47535  fmtnof1  47540  fmtnoprmfac2lem1  47571  fmtno4prmfac  47577  fmtno4prm  47580  2pwp1prm  47594  31prm  47602  sfprmdvdsmersenne  47608  lighneallem2  47611  lighneallem4a  47613  lighneallem4b  47614  requad01  47626  requad1  47627  requad2  47628  dfodd4  47664  nn0o1gt2ALTV  47699  nnoALTV  47700  nn0oALTV  47701  nn0e  47702  nneven  47703  perfectALTVlem1  47726  perfectALTVlem2  47727  341fppr2  47739  9fppr8  47742  fpprel2  47746  nfermltl2rev  47748  gbowgt5  47767  sbgoldbalt  47786  sgoldbeven3prm  47788  mogoldbb  47790  nnsum3primes4  47793  nnsum3primesgbe  47797  nnsum3primesle9  47799  nnsum4primesodd  47801  nnsum4primesoddALTV  47802  wtgoldbnnsum4prm  47807  bgoldbnnsum3prm  47809  cycl3grtri  47950  usgrexmpl1lem  48016  usgrexmpl2lem  48021  usgrexmpl2nb2  48028  usgrexmpl2nb3  48029  usgrexmpl2nb4  48030  usgrexmpl2nb5  48031  usgrexmpl2trifr  48032  gpgprismgrusgra  48053  gpg5nbgrvtx13starlem2  48067  gpg3nbgrvtx0  48071  gpg3kgrtriexlem1  48078  cznnring  48254  ply1mulgsumlem2  48380  zlmodzxznm  48490  zlmodzxzldeplem  48491  nn0eo  48521  flnn0div2ge  48526  rege1logbzge0  48552  fldivexpfllog2  48558  logbpw2m1  48560  fllog2  48561  blenpw2m1  48572  nnpw2blen  48573  nnolog2flm1  48583  blennngt2o2  48585  dig2nn1st  48598  dig2nn0  48604  dig2bits  48607  dignn0flhalflem1  48608  dignn0flhalflem2  48609  dignn0flhalf  48611  nn0sumshdiglemA  48612  ackval42  48689  rrx2xpref1o  48711  itscnhlc0yqe  48752  itsclquadb  48769  2itscp  48774  itscnhlinecirc02p  48778  sepfsepc  48920