Theorem 2re 12249

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 12238	. 2 ⊢ 2 = (1 + 1)
2		1re 11138	. . 3 ⊢ 1 ∈ ℝ
3	2, 2	readdcli 11154	. 2 ⊢ (1 + 1) ∈ ℝ
4	1, 3	eqeltri 2833	1 ⊢ 2 ∈ ℝ

Syntax hints:   ∈ wcel 2114  (class class class)co 7361  ℝcr 11031  1c1 11033   + caddc 11035  2c2 12230

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-ext 2709  ax-1cn 11090  ax-icn 11091  ax-addcl 11092  ax-addrcl 11093  ax-mulcl 11094  ax-mulrcl 11095  ax-i2m1 11100  ax-1ne0 11101  ax-rrecex 11104  ax-cnre 11105

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-ne 2934  df-ral 3053  df-rex 3063  df-rab 3391  df-v 3432  df-dif 3893  df-un 3895  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-br 5087  df-iota 6449  df-fv 6501  df-ov 7364  df-2 12238

This theorem is referenced by:  2cnALT  12251  3re  12255  3pos  12280  2lt3  12342  1lt3  12343  2lt4  12345  1lt4  12346  2lt5  12349  2lt6  12354  1lt6  12355  2lt7  12360  1lt7  12361  2lt8  12367  1lt8  12368  2lt9  12375  1lt9  12376  1le2  12379  2rene0  12381  halfre  12384  halfgt0  12386  halflt1  12388  rehalfcl  12398  halfpos2  12400  halfnneg2  12402  addltmul  12407  nominpos  12408  avglt1  12409  avglt2  12410  div4p1lem1div2  12426  nn0lele2xi  12487  nn0n0n1ge2b  12500  nn0ge2m1nn  12501  nn0le2is012  12587  halfnz  12601  3halfnz  12602  2lt10  12776  1lt10  12777  uzuzle23  12828  uzuzle24  12829  uz3m2nn  12838  2rp  12941  ge2halflem1  13053  xnn0n0n1ge2b  13077  fztpval  13534  fz0to4untppr  13578  fz0to5un2tp  13579  fzo0to42pr  13702  flhalf  13783  fldiv4p1lem1div2  13788  2txmodxeq0  13887  expubnd  14134  expmulnbnd  14191  nn0opthlem2  14225  faclbnd2  14247  faclbnd4lem1  14249  faclbnd5  14254  4bc2eq6  14285  hashgt23el  14380  hashfun  14393  hashge2el2dif  14436  hashge2el2difr  14437  hash3tpde  14449  wrdlenge2n0  14508  f1oun2prg  14873  01sqrexlem7  15204  sqrt4  15228  sqrt2gt1lt2  15230  abstri  15287  sqreulem  15316  amgm2  15326  caucvgrlem  15629  climcndslem1  15808  climcndslem2  15809  climcnds  15810  efcllem  16036  ege2le3  16049  ef01bndlem  16145  cos01bnd  16147  cos2bnd  16149  cos01gt0  16152  sin02gt0  16153  sincos2sgn  16155  sin4lt0  16156  eirrlem  16165  egt2lt3  16167  epos  16168  ene1  16171  sqrt2re  16211  mod2eq1n2dvds  16310  oddge22np1  16312  evennn2n  16314  nn0o1gt2  16344  nno  16345  nn0o  16346  nnoddm1d2  16349  bitsp1o  16396  bitsfzolem  16397  bitsfzo  16398  bitsfi  16400  6gcd4e2  16501  2mulprm  16656  ge2nprmge4  16665  isprm7  16672  3lcm2e6  16696  prmreclem2  16882  prmreclem6  16886  4sqlem11  16920  4sqlem12  16921  prmgaplem7  17022  2expltfac  17057  plusgndxnmulrndx  17254  starvndxnplusgndx  17262  scandxnplusgndx  17274  vscandxnplusgndx  17279  ipndxnplusgndx  17290  tsetndxnplusgndx  17314  plendxnplusgndx  17328  dsndxnplusgndx  17347  slotsdifunifndx  17358  efgredleme  19712  zringndrg  21461  chfacfscmul0  22836  chfacfpmmul0  22840  psmetge0  24290  xmetge0  24322  bl2in  24378  metnrmlem3  24840  iihalf1  24911  iihalf2  24913  pcoass  25004  tcphcphlem1  25215  csbren  25379  trirn  25380  minveclem2  25406  minveclem4  25412  pjthlem1  25417  ovolunlem1a  25476  dyadss  25574  opnmbllem  25581  vitalilem2  25589  vitalilem4  25591  mbfi1fseqlem5  25699  lhop1lem  25993  aaliou3lem2  26323  aaliou3lem8  26325  pilem2  26433  pilem3  26434  pipos  26439  sinhalfpilem  26443  sincosq1lem  26477  sincosq4sgn  26481  tangtx  26485  sinq12gt0  26487  sincos4thpi  26493  tan4thpi  26494  tan4thpiOLD  26495  sincos6thpi  26496  sineq0  26504  cos02pilt1  26506  cosq34lt1  26507  cosordlem  26510  cos0pilt1  26512  tanord1  26517  efif1olem1  26522  efif1olem2  26523  efif1olem4  26525  efif1o  26526  efifo  26527  2irrexpq  26711  cxpcn3lem  26727  root1id  26734  root1eq1  26735  root1cj  26736  cxpeq  26737  2logb9irr  26775  2logb3irr  26777  ang180lem1  26789  ang180lem2  26790  chordthmlem2  26813  1cubrlem  26821  atancj  26890  atantan  26903  atanbndlem  26905  atans2  26911  leibpi  26922  log2tlbnd  26925  log2ublem2  26927  log2ub  26929  divsqrtsumlem  26960  harmonicbnd3  26988  zetacvg  26995  lgamgulmlem2  27010  lgamgulmlem3  27011  lgamgulmlem4  27012  lgamgulmlem6  27014  lgamucov  27018  basellem1  27061  basellem2  27062  basellem3  27063  basellem5  27065  chtdif  27138  ppidif  27143  ppinncl  27154  chtrpcl  27155  ppieq0  27156  ppiltx  27157  ppiublem1  27182  ppiub  27184  chpeq0  27188  chteq0  27189  chtublem  27191  chtub  27192  chpval2  27198  chpub  27200  mersenne  27207  perfectlem1  27209  perfectlem2  27210  dchrptlem1  27244  dchrptlem2  27245  bcmono  27257  bclbnd  27260  bpos1lem  27262  bposlem1  27264  bposlem2  27265  bposlem3  27266  bposlem4  27267  bposlem5  27268  bposlem6  27269  bposlem7  27270  bposlem8  27271  bposlem9  27272  lgslem1  27277  lgsdirprm  27311  gausslemma2dlem0c  27338  gausslemma2dlem1a  27345  gausslemma2dlem2  27347  gausslemma2dlem3  27348  lgseisenlem1  27355  lgseisenlem2  27356  lgseisenlem3  27357  lgseisen  27359  lgsquadlem1  27360  lgsquadlem2  27361  m1lgs  27368  2lgslem1a1  27369  2lgslem1a2  27370  2lgslem1c  27373  2lgslem4  27386  2sqlem11  27409  2sq2  27413  2sqreultlem  27427  2sqreunnltlem  27430  chebbnd1lem1  27449  chebbnd1lem2  27450  chebbnd1lem3  27451  chebbnd1  27452  chtppilimlem1  27453  chtppilimlem2  27454  chtppilim  27455  chto1ub  27456  chebbnd2  27457  chto1lb  27458  chpchtlim  27459  chpo1ub  27460  chpo1ubb  27461  rplogsumlem1  27464  rplogsumlem2  27465  dchrisumlem2  27470  dchrisumlem3  27471  dchrvmasumiflem1  27481  dchrisum0fno1  27491  dchrisum0re  27493  dchrisum0lem1b  27495  dchrisum0lem1  27496  dchrisum0lem2  27498  rplogsum  27507  mulog2sumlem1  27514  mulog2sumlem2  27515  log2sumbnd  27524  selberglem2  27526  selbergb  27529  selberg2b  27532  chpdifbndlem1  27533  logdivbnd  27536  selberg3lem1  27537  selberg3  27539  selberg4lem1  27540  selberg4  27541  pntrmax  27544  pntrsumbnd2  27547  selberg3r  27549  selberg4r  27550  selberg34r  27551  pntrlog2bndlem2  27558  pntrlog2bndlem3  27559  pntrlog2bndlem4  27560  pntrlog2bndlem5  27561  pntrlog2bndlem6  27563  pntrlog2bnd  27564  pntpbnd1a  27565  pntpbnd1  27566  pntpbnd2  27567  pntpbnd  27568  pntibndlem2  27571  pntibndlem3  27572  pntibnd  27573  pntlemb  27577  pntlemg  27578  pntlemh  27579  pntlemr  27582  pntlemk  27586  pntlemo  27587  pnt2  27593  pnt  27594  ostth2lem1  27598  ostth3  27618  slotsinbpsd  28526  slotslnbpsd  28527  istrkg3ld  28546  tgldimor  28587  trgcgrg  28600  tgcgr4  28616  axlowdimlem6  29033  axlowdimlem16  29043  axlowdimlem17  29044  axlowdim  29047  upgrfi  29177  umgrupgr  29189  umgrislfupgrlem  29208  umgrislfupgr  29209  lfgrnloop  29211  usgruspgr  29266  usgrislfuspgr  29273  lfuhgr1v0e  29340  usgrexmpldifpr  29344  usgrexmplef  29345  nbusgrvtxm1  29465  vdegp1bi  29624  upgrewlkle2  29693  lfgrwlkprop  29772  upgr2pthnlp  29818  usgr2pthlem  29849  pthdlem1  29852  wwlksm1edg  29967  wwlksnextwrd  29983  wwlksnextfun  29984  wwlksnextinj  29985  wwlksnextproplem3  29997  clwlkclwwlklem2a1  30080  clwlkclwwlklem2a2  30081  clwlkclwwlklem2fv1  30083  clwlkclwwlklem2fv2  30084  clwlkclwwlklem2a4  30085  clwlkclwwlklem2a  30086  clwlkclwwlklem2  30088  clwlkclwwlk2  30091  clwlkclwwlkf  30096  clwwlkext2edg  30144  konigsbergiedgw  30336  konigsbergssiedgw  30338  konigsberglem1  30340  konigsberglem2  30341  konigsberglem3  30342  konigsberg  30345  frgrreggt1  30481  ex-pss  30516  ex-res  30529  ex-fv  30531  ex-fl  30535  ex-mod  30537  ex-abs  30543  nrt2irr  30561  ipidsq  30799  minvecolem2  30964  minvecolem4  30969  normlem7  31205  norm-ii-i  31226  norm3lemt  31241  normpar2i  31245  bcsiALT  31268  pjhthlem1  31480  opsqrlem6  32234  cdj3lem1  32523  addltmulALT  32535  nexple  32935  2exple2exp  32936  threehalves  32992  pfx1s2  33017  wrdt2ind  33031  cyc3conja  33236  drngidlhash  33512  evl1deg3  33656  rtelextdg2lem  33889  fldext2chn  33891  constraddcl  33925  iconstr  33929  2sqr3minply  33943  2sqr3nconstr  33944  cos9thpinconstrlem1  33952  cos9thpinconstrlem2  33953  sqsscirc1  34071  dya2iocucvr  34447  omssubadd  34463  oddpwdc  34517  eulerpartlemgc  34525  fibp1  34564  coinfliplem  34642  coinflipspace  34644  ballotlem2  34652  signstfveq0  34740  prodfzo03  34766  hgt750lemd  34811  logdivsqrle  34813  hgt750lem  34814  hgt750lem2  34815  hgt750leme  34821  lfuhgr2  35320  usgrcyclgt2v  35332  acycgr2v  35351  subfacp1lem1  35380  subfacp1lem5  35385  subfacval3  35390  problem2  35867  problem5  35870  circum  35875  nn0prpwlem  36523  dnibndlem10  36766  knoppcnlem2  36773  knoppcnlem4  36775  knoppcnlem10  36781  unbdqndv2lem1  36788  knoppndvlem1  36791  knoppndvlem10  36800  knoppndvlem11  36801  knoppndvlem12  36802  knoppndvlem14  36804  knoppndvlem15  36805  knoppndvlem17  36807  knoppndvlem18  36808  knoppndvlem19  36809  knoppndvlem20  36810  knoppndvlem21  36811  cnndvlem1  36816  taupi  37656  iccioo01  37660  relowlpssretop  37697  sin2h  37948  cos2h  37949  tan2h  37950  poimirlem7  37965  poimirlem9  37967  opnmbllem0  37994  mblfinlem1  37995  mblfinlem2  37996  itg2addnclem  38009  isbnd2  38121  isbnd3  38122  heiborlem7  38155  12gcd5e1  42459  lcm2un  42470  lcmineqlem19  42503  lcmineqlem20  42504  lcmineqlem22  42506  3lexlogpow5ineq2  42511  3lexlogpow5ineq4  42512  3lexlogpow5ineq3  42513  3lexlogpow2ineq1  42514  3lexlogpow2ineq2  42515  3lexlogpow5ineq5  42516  aks4d1lem1  42518  aks4d1p1p3  42525  aks4d1p1p2  42526  aks4d1p1p4  42527  aks4d1p1p6  42529  aks4d1p1p7  42530  aks4d1p1p5  42531  aks4d1p1  42532  aks4d1p2  42533  aks4d1p3  42534  aks4d1p5  42536  aks4d1p6  42537  aks4d1p7d1  42538  aks4d1p7  42539  aks4d1p8  42543  aks4d1p9  42544  posbezout  42556  aks6d1c3  42579  2np3bcnp1  42600  2ap1caineq  42601  aks6d1c6lem4  42629  aks6d1c7lem1  42636  aks6d1c7lem2  42637  oexpreposd  42771  asin1half  42806  remul02  42854  sn-0ne2  42855  remul01  42856  flt4lem7  43109  rabren3dioph  43264  pellexlem2  43279  pellexlem5  43282  pell14qrgapw  43325  pellfundex  43335  rmspecsqrtnq  43355  jm2.24nn  43408  jm2.17a  43409  jm2.17b  43410  jm2.17c  43411  acongrep  43429  acongeq  43432  jm2.22  43444  jm2.23  43445  jm2.20nn  43446  jm3.1lem2  43467  expdiophlem1  43470  sqrtcval  44089  imo72b2lem0  44613  lhe4.4ex1a  44777  isosctrlem1ALT  45381  sineq0ALT  45384  lt3addmuld  45755  suplesup  45790  infleinflem2  45821  infleinf  45822  sumnnodd  46081  0ellimcdiv  46098  sinaover2ne0  46317  stoweidlem13  46462  stoweidlem14  46463  stoweidlem26  46475  stoweidlem49  46498  stoweidlem52  46501  wallispilem4  46517  wallispilem5  46518  wallispi  46519  wallispi2lem1  46520  wallispi2lem2  46521  wallispi2  46522  stirlinglem1  46523  stirlinglem3  46525  stirlinglem5  46527  stirlinglem6  46528  stirlinglem7  46529  stirlinglem10  46532  stirlinglem11  46533  stirlinglem15  46537  stirlingr  46539  dirker2re  46541  dirkerval2  46543  dirkerre  46544  dirkerper  46545  dirkertrigeqlem1  46547  dirkertrigeqlem3  46549  dirkercncflem1  46552  dirkercncflem2  46553  dirkercncflem4  46555  fourierdlem24  46580  fourierdlem43  46599  fourierdlem44  46600  fourierdlem57  46612  fourierdlem58  46613  fourierdlem62  46617  fourierdlem66  46621  fourierdlem68  46623  fourierdlem72  46627  fourierdlem76  46631  fourierdlem78  46633  fourierdlem79  46634  fourierdlem94  46649  fourierdlem103  46658  fourierdlem104  46659  fourierdlem111  46666  fourierdlem113  46668  sqwvfoura  46677  sqwvfourb  46678  fourierswlem  46679  fouriersw  46680  etransclem23  46706  salexct2  46788  salexct3  46791  salgencntex  46792  salgensscntex  46793  sge0ad2en  46880  ovnsubaddlem1  47019  smfmullem4  47243  smf2id  47250  nthrucw  47335  goldrarr  47346  goldrapos  47348  2leaddle2  47761  p1lep2  47763  2ltceilhalf  47795  ceilhalfgt1  47796  2tceilhalfelfzo1  47799  rehalfge1  47802  ceilhalfnn  47803  ceil5half3  47809  difmodm1lt  47828  2timesltsq  47841  2timesltsqm1  47842  fmtnoge3  48008  fmtnof1  48013  fmtnoprmfac2lem1  48044  fmtno4prmfac  48050  fmtno4prm  48053  2pwp1prm  48067  31prm  48075  sfprmdvdsmersenne  48081  lighneallem2  48084  lighneallem4a  48086  lighneallem4b  48087  nprmdvdsfacm1lem2  48099  nprmdvdsfacm1lem4  48101  ppivalnnnprmge6  48104  requad01  48112  requad1  48113  requad2  48114  dfodd4  48150  nn0o1gt2ALTV  48185  nnoALTV  48186  nn0oALTV  48187  nn0e  48188  nneven  48189  perfectALTVlem1  48212  perfectALTVlem2  48213  341fppr2  48225  9fppr8  48228  fpprel2  48232  nfermltl2rev  48234  gbowgt5  48253  sbgoldbalt  48272  sgoldbeven3prm  48274  mogoldbb  48276  nnsum3primes4  48279  nnsum3primesgbe  48283  nnsum3primesle9  48285  nnsum4primesodd  48287  nnsum4primesoddALTV  48288  wtgoldbnnsum4prm  48293  bgoldbnnsum3prm  48295  cycl3grtri  48438  usgrexmpl1lem  48512  usgrexmpl2lem  48517  usgrexmpl2nb2  48524  usgrexmpl2nb3  48525  usgrexmpl2nb4  48526  usgrexmpl2nb5  48527  usgrexmpl2trifr  48528  gpgprismgrusgra  48549  gpg5nbgrvtx13starlem2  48563  gpg3nbgrvtx0  48567  gpg3kgrtriexlem1  48574  cznnring  48753  ply1mulgsumlem2  48878  zlmodzxznm  48988  zlmodzxzldeplem  48989  nn0eo  49019  flnn0div2ge  49024  rege1logbzge0  49050  fldivexpfllog2  49056  logbpw2m1  49058  fllog2  49059  blenpw2m1  49070  nnpw2blen  49071  nnolog2flm1  49081  blennngt2o2  49083  dig2nn1st  49096  dig2nn0  49102  dig2bits  49105  dignn0flhalflem1  49106  dignn0flhalflem2  49107  dignn0flhalf  49109  nn0sumshdiglemA  49110  ackval42  49187  rrx2xpref1o  49209  itscnhlc0yqe  49250  itsclquadb  49267  2itscp  49272  itscnhlinecirc02p  49276  sepfsepc  49418