Theorem 2re 12457

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 12445	. 2 ⊢ 2 = (1 + 1)
2		1re 11347	. . 3 ⊢ 1 ∈ ℝ
3	2, 2	readdcli 11363	. 2 ⊢ (1 + 1) ∈ ℝ
4	1, 3	eqeltri 2860	1 ⊢ 2 ∈ ℝ

This proof depends on syntax axioms:   ∈ wcel 2147  (class class class)co 7451  ℝcr 11238  1c1 11240   + caddc 11242  2c2 12437

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735  ax-1cn 11297  ax-icn 11298  ax-addcl 11299  ax-addrcl 11300  ax-mulcl 11301  ax-mulrcl 11302  ax-i2m1 11307  ax-1ne0 11308  ax-rrecex 11311  ax-cnre 11312

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-ne 2960  df-ral 3081  df-rex 3091  df-rab 3417  df-v 3456  df-ss 3901  df-dif 4050  df-un 4154  df-nul 4282  df-if 4486  df-sn 4589  df-pr 4591  df-op 4841  df-uni 4873  df-br 5109  df-iota 6520  df-fv 6574  df-ov 7454  df-2 12445

This theorem is used by:  2cnALT  12459  3re  12463  0le2  12485  2lt3  12556  2le3  12557  1lt3  12558  2lt4  12560  1lt4  12561  2lt5  12564  2lt6  12569  1lt6  12570  2lt7  12575  1lt7  12576  2lt8  12582  1lt8  12583  2lt9  12590  1lt9  12591  1le2  12594  2rene0  12596  halfre  12599  halfgt0  12601  halflt1  12603  rehalfcl  12613  halfpos2  12615  halfnneg2  12617  addltmul  12622  nominpos  12623  avglt1  12624  avglt2  12625  div4p1lem1div2  12641  nn0lele2xi  12702  nn0n0n1ge2b  12715  nn0ge2m1nn  12716  nn0le2is012  12803  halfnz  12817  3halfnz  12818  2lt10  12998  1lt10OLD  13000  uzuzle23  13051  uzuzle24  13052  uz3m2nn  13061  2rp  13165  ge2halflem1  13277  xnn0n0n1ge2b  13301  fztpval  13760  fz0to4untppr  13804  fz0to5un2tp  13805  fzo0to42pr  13928  flhalf  14010  fldiv4p1lem1div2  14015  2txmodxeq0  14114  expubnd  14361  expmulnbnd  14420  nn0opthlem2  14454  faclbnd2  14476  faclbnd4lem1  14478  faclbnd5  14483  4bc2eq6  14514  hashgt23el  14610  hashfun  14623  hashge2el2dif  14666  hashge2el2difr  14667  hash3tpde  14679  wrdlenge2n0  14738  f1oun2prg  15111  01sqrexlem7  15458  sqrt4  15482  sqrt2gt1lt2  15484  abstri  15541  sqreulem  15571  amgm2  15581  caucvgrlem  15884  climcndslem1  16062  climcndslem2  16063  climcnds  16064  efcllem  16287  ege2le3  16300  ef01bndlem  16396  cos01bnd  16398  cos2bnd  16400  cos01gt0  16403  sin02gt0  16404  sincos2sgn  16406  sin4lt0  16407  eirrlem  16416  egt2lt3  16418  epos  16419  ene1  16422  sqrt2re  16462  mod2eq1n2dvds  16561  oddge22np1  16563  evennn2n  16565  nn0o1gt2  16595  nno  16596  nn0o  16597  nnoddm1d2  16600  bitsp1o  16647  bitsfzolem  16648  bitsfzo  16649  bitsfi  16651  6gcd4e2  16755  2mulprm  16912  ge2nprmge4  16921  isprm7  16928  3lcm2e6  16952  prmreclem2  17139  prmreclem6  17143  4sqlem11  17177  4sqlem12  17178  prmgaplem7  17279  2expltfac  17314  plusgndxnmulrndx  17514  starvndxnplusgndx  17522  scandxnplusgndx  17534  vscandxnplusgndx  17539  ipndxnplusgndx  17550  tsetndxnplusgndx  17574  plendxnplusgndx  17588  dsndxnplusgndx  17607  slotsdifunifndx  17618  efgredleme  20008  zringndrg  21829  chfacfscmul0  23231  chfacfpmmul0  23235  psmetge0  24686  xmetge0  24718  bl2in  24774  metnrmlem3  25236  iihalf1  25307  iihalf2  25309  pcoass  25400  tcphcphlem1  25611  csbren  25775  trirn  25776  minveclem2  25802  minveclem4  25808  pjthlem1  25813  ovolunlem1a  25872  dyadss  25970  opnmbllem  25977  vitalilem2  25985  vitalilem4  25987  mbfi1fseqlem5  26095  lhop1lem  26388  aaliou3lem2  26727  aaliou3lem8  26729  pilem2  26836  pilem3  26837  2pire  26841  pipos  26844  sinhalfpilem  26849  sincosq1lem  26883  sincosq4sgn  26887  tangtx  26891  sinq12gt0  26893  sincos4thpi  26899  tan4thpi  26900  sincos6thpi  26901  sineq0  26909  cos02pilt1  26911  cosq34lt1  26912  cosordlem  26915  cos0pilt1  26917  tanord1  26922  efif1olem1  26927  efif1olem2  26928  efif1olem4  26930  efif1o  26931  efifo  26932  2irrexpq  27116  cxpcn3lem  27132  root1id  27139  root1eq1  27140  root1cj  27141  cxpeq  27142  2logb9irr  27180  2logb3irr  27182  ang180lem1  27194  ang180lem2  27195  chordthmlem2  27218  1cubrlem  27226  atancj  27295  atantan  27308  atanbndlem  27310  atans2  27316  leibpi  27327  log2tlbnd  27330  log2ublem2  27332  log2ub  27334  divsqrtsumlem  27364  harmonicbnd3  27392  zetacvg  27399  lgamgulmlem2  27414  lgamgulmlem3  27415  lgamgulmlem4  27416  lgamgulmlem6  27418  lgamucov  27422  basellem1  27465  basellem2  27466  basellem3  27467  basellem5  27469  chtdif  27542  ppidif  27547  ppinncl  27558  chtrpcl  27559  ppieq0  27560  ppiltx  27561  ppiublem1  27586  ppiub  27588  chpeq0  27592  chteq0  27593  chtublem  27595  chtub  27596  chpval2  27602  chpub  27604  mersenne  27611  perfectlem1  27613  perfectlem2  27614  dchrptlem1  27648  dchrptlem2  27649  bcmono  27661  bclbnd  27664  bpos1lem  27666  bposlem1  27668  bposlem2  27669  bposlem3  27670  bposlem4  27671  bposlem5  27672  bposlem6  27673  bposlem7  27674  bposlem8  27675  bposlem9  27676  lgslem1  27681  lgsdirprm  27715  gausslemma2dlem0c  27742  gausslemma2dlem1a  27749  gausslemma2dlem2  27751  gausslemma2dlem3  27752  lgseisenlem1  27759  lgseisenlem2  27760  lgseisenlem3  27761  lgseisen  27763  lgsquadlem1  27764  lgsquadlem2  27765  m1lgs  27772  2lgslem1a1  27773  2lgslem1a2  27774  2lgslem1c  27777  2lgslem4  27790  2sqlem11  27813  2sq2  27817  2sqreultlem  27831  2sqreunnltlem  27834  chebbnd1lem1  27853  chebbnd1lem2  27854  chebbnd1lem3  27855  chebbnd1  27856  chtppilimlem1  27857  chtppilimlem2  27858  chtppilim  27859  chto1ub  27860  chebbnd2  27861  chto1lb  27862  chpchtlim  27863  chpo1ub  27864  chpo1ubb  27865  rplogsumlem1  27868  rplogsumlem2  27869  dchrisumlem2  27874  dchrisumlem3  27875  dchrvmasumiflem1  27885  dchrisum0fno1  27895  dchrisum0re  27897  dchrisum0lem1b  27899  dchrisum0lem1  27900  dchrisum0lem2  27902  rplogsum  27911  mulog2sumlem1  27918  mulog2sumlem2  27919  log2sumbnd  27928  selberglem2  27930  selbergb  27933  selberg2b  27936  chpdifbndlem1  27937  logdivbnd  27940  selberg3lem1  27941  selberg3  27943  selberg4lem1  27944  selberg4  27945  pntrmax  27948  pntrsumbnd2  27951  selberg3r  27953  selberg4r  27954  selberg34r  27955  pntrlog2bndlem2  27962  pntrlog2bndlem3  27963  pntrlog2bndlem4  27964  pntrlog2bndlem5  27965  pntrlog2bndlem6  27967  pntrlog2bnd  27968  pntpbnd1a  27969  pntpbnd1  27970  pntpbnd2  27971  pntpbnd  27972  pntibndlem2  27975  pntibndlem3  27976  pntibnd  27977  pntlemb  27981  pntlemg  27982  pntlemh  27983  pntlemr  27986  pntlemk  27990  pntlemo  27991  pnt2  27997  pnt  27998  ostth2lem1  28002  ostth3  28022  fltoprmlem2  28051  slotsinbpsd  28960  slotslnbpsd  28961  tgldimor  29022  trgcgrg  29035  tgcgr4  29051  axlowdimlem6  29582  axlowdimlem16  29592  axlowdimlem17  29593  axlowdim  29596  upgrfi  29726  umgrupgr  29738  umgrislfupgrlem  29757  umgrislfupgr  29758  lfgrnloop  29760  lfuhgr2  29784  usgruspgr  29818  usgrislfuspgr  29825  lfuhgr1v0e  29892  usgrexmpldifpr  29896  usgrexmplef  29897  nbusgrvtxm1  30017  vdegp1bi  30175  upgrewlkle2  30244  lfgrwlkprop  30327  upgr2pthnlp  30375  usgr2pthlem  30406  pthdlem1  30409  wwlksm1edg  30527  wwlksnextwrd  30543  wwlksnextfun  30544  wwlksnextinj  30545  wwlksnextproplem3  30557  clwlkclwwlklem2a1  30640  clwlkclwwlklem2a2  30641  clwlkclwwlklem2fv1  30643  clwlkclwwlklem2fv2  30644  clwlkclwwlklem2a4  30645  clwlkclwwlklem2a  30646  clwlkclwwlklem2  30648  clwlkclwwlk2  30651  clwlkclwwlkf  30656  clwwlkext2edg  30704  konigsbergiedgw  30906  konigsbergssiedgw  30908  konigsberglem3  30912  konigsberg  30915  frgrreggt1  31051  ex-pss  31086  ex-res  31099  ex-fv  31101  ex-fl  31105  ex-mod  31107  ex-abs  31113  nrt2irr  31131  ipidsq  31369  minvecolem2  31534  minvecolem4  31539  normlem7  31775  norm-ii-i  31796  norm3lemt  31811  normpar2i  31815  bcsiALT  31838  pjhthlem1  32050  opsqrlem6  32804  cdj3lem1  33093  addltmulALT  33147  nexple  33520  2exple2exp  33521  threehalves  33577  pfx1s2  33602  wrdt2ind  33612  cyc3conja  33817  drngidlhash  34087  evl1deg3  34213  rtelextdg2lem  34469  fldext2chn  34471  constraddcl  34505  iconstr  34509  2sqr3minply  34523  2sqr3nconstr  34524  cos9thpinconstrlem1  34532  cos9thpinconstrlem2  34533  sqsscirc1  34651  dya2iocucvr  35027  omssubadd  35043  oddpwdc  35097  eulerpartlemgc  35105  fibp1  35144  coinfliplem  35222  coinflipspace  35224  ballotlem2  35232  signstfveq0  35317  prodfzo03  35343  hgt750lemd  35388  logdivsqrle  35390  hgt750lem  35391  hgt750lem2  35392  hgt750leme  35398  usgrcyclgt2v  36108  acycgr2v  36113  subfacp1lem1  36152  subfacp1lem5  36157  subfacval3  36162  problem2  36639  problem5  36642  circum  36647  nn0prpwlem  37325  dnibndlem10  37568  knoppcnlem2  37575  knoppcnlem4  37577  knoppcnlem10  37583  unbdqndv2lem1  37590  knoppndvlem1  37593  knoppndvlem10  37602  knoppndvlem11  37603  knoppndvlem12  37604  knoppndvlem14  37606  knoppndvlem15  37607  knoppndvlem17  37609  knoppndvlem18  37610  knoppndvlem19  37611  knoppndvlem20  37612  knoppndvlem21  37613  cnndvlem1  37618  taupi  38512  iccioo01  38518  relowlpssretop  38555  sin2h  38801  cos2h  38802  tan2h  38803  poimirlem7  38813  poimirlem9  38815  opnmbllem0  38842  mblfinlem1  38843  mblfinlem2  38844  itg2addnclem  38857  isbnd2  38983  isbnd3  38984  heiborlem7  39017  12gcd5e1  43319  lcm2un  43330  lcmineqlem19  43363  lcmineqlem20  43364  lcmineqlem22  43366  3lexlogpow5ineq2  43371  3lexlogpow5ineq4  43372  3lexlogpow5ineq3  43373  3lexlogpow2ineq1  43374  3lexlogpow2ineq2  43375  3lexlogpow5ineq5  43376  aks4d1lem1  43378  aks4d1p1p3  43385  aks4d1p1p2  43386  aks4d1p1p4  43387  aks4d1p1p6  43389  aks4d1p1p7  43390  aks4d1p1p5  43391  aks4d1p1  43392  aks4d1p2  43393  aks4d1p3  43394  aks4d1p5  43396  aks4d1p6  43397  aks4d1p7d1  43398  aks4d1p7  43399  aks4d1p8  43403  aks4d1p9  43404  posbezout  43416  aks6d1c3  43439  2np3bcnp1  43460  2ap1caineq  43461  aks6d1c6lem4  43489  aks6d1c7lem1  43496  aks6d1c7lem2  43497  oexpreposd  43645  asin1half  43674  remul02  43722  sn-0ne2  43723  remul01  43724  rabren3dioph  44088  pellexlem2  44103  pellexlem5  44106  pell14qrgapw  44149  pellfundex  44159  rmspecsqrtnq  44179  jm2.24nn  44232  jm2.17a  44233  jm2.17b  44234  jm2.17c  44235  acongrep  44253  acongeq  44256  jm2.22  44268  jm2.23  44269  jm3.1lem2  44291  expdiophlem1  44294  sqrtcval  44902  imo72b2lem0  45426  lhe4.4ex1a  45574  isosctrlem1ALT  46176  sineq0ALT  46179  lt3addmuld  46590  suplesup  46624  infleinflem2  46655  infleinf  46656  sumnnodd  46915  0ellimcdiv  46932  sinaover2ne0  47151  stoweidlem13  47296  stoweidlem14  47297  stoweidlem26  47309  stoweidlem49  47332  stoweidlem52  47335  wallispilem4  47351  wallispilem5  47352  wallispi  47353  wallispi2lem1  47354  wallispi2lem2  47355  wallispi2  47356  stirlinglem1  47357  stirlinglem3  47359  stirlinglem5  47361  stirlinglem6  47362  stirlinglem7  47363  stirlinglem10  47366  stirlinglem11  47367  stirlinglem15  47371  stirlingr  47373  dirker2re  47375  dirkerval2  47377  dirkerre  47378  dirkertrigeqlem1  47381  dirkertrigeqlem3  47383  dirkercncflem1  47386  dirkercncflem4  47389  fourierdlem24  47414  fourierdlem43  47433  fourierdlem44  47434  fourierdlem57  47446  fourierdlem58  47447  fourierdlem62  47451  fourierdlem66  47455  fourierdlem68  47457  fourierdlem72  47461  fourierdlem76  47465  fourierdlem78  47467  fourierdlem79  47468  fourierdlem94  47483  fourierdlem103  47492  fourierdlem104  47493  fourierdlem111  47500  sqwvfoura  47511  sqwvfourb  47512  fourierswlem  47513  fouriersw  47514  etransclem23  47540  salexct2  47622  salexct3  47625  salgencntex  47626  salgensscntex  47627  sge0ad2en  47714  ovnsubaddlem1  47853  smfmullem4  48077  smf2id  48084  goldrarr  48201  goldrapos  48203  goldratmolem4  48208  goldratval  48209  2leaddle2  48641  p1lep2  48643  2ltceilhalf  48675  ceilhalfgt1  48676  2tceilhalfelfzo1  48679  rehalfge1  48682  ceilhalfnn  48683  ceil5half3  48689  difmodm1lt  48708  2timesltsq  48721  2timesltsqm1  48722  fmtnoge3  48888  fmtnof1  48893  fmtnoprmfac2lem1  48924  fmtno4prmfac  48930  fmtno4prm  48933  2pwp1prm  48947  31prm  48955  sfprmdvdsmersenne  48961  lighneallem2  48964  lighneallem4a  48966  lighneallem4b  48967  nprmdvdsfacm1lem2  48979  nprmdvdsfacm1lem4  48981  ppivalnnnprmge6  48984  requad01  48992  requad1  48993  requad2  48994  dfodd4  49030  nn0o1gt2ALTV  49065  nnoALTV  49066  nn0oALTV  49067  nn0e  49068  nneven  49069  perfectALTVlem1  49092  perfectALTVlem2  49093  341fppr2  49105  9fppr8  49108  fpprel2  49112  nfermltl2rev  49114  gbowgt5  49133  sbgoldbalt  49152  sgoldbeven3prm  49154  mogoldbb  49156  nnsum3primes4  49159  nnsum3primesgbe  49163  nnsum3primesle9  49165  nnsum4primesodd  49167  nnsum4primesoddALTV  49168  wtgoldbnnsum4prm  49173  bgoldbnnsum3prm  49175  cycl3grtri  49318  usgrexmpl1lem  49392  usgrexmpl2lem  49397  usgrexmpl2nb2  49404  usgrexmpl2nb3  49405  usgrexmpl2nb4  49406  usgrexmpl2nb5  49407  usgrexmpl2trifr  49408  gpgprismgrusgra  49429  gpg5nbgrvtx13starlem2  49443  gpg3nbgrvtx0  49447  gpg3kgrtriexlem1  49454  cznnring  49632  ply1mulgsumlem2  49830  zlmodzxznm  49940  zlmodzxzldeplem  49941  nn0eo  49971  flnn0div2ge  49976  rege1logbzge0  50002  fldivexpfllog2  50008  logbpw2m1  50010  fllog2  50011  blenpw2m1  50022  nnpw2blen  50023  nnolog2flm1  50033  blennngt2o2  50035  dig2nn1st  50048  dig2nn0  50054  dig2bits  50057  dignn0flhalflem1  50058  dignn0flhalflem2  50059  dignn0flhalf  50061  nn0sumshdiglemA  50062  ackval42  50139  itscnhlc0yqe  50202  itsclquadb  50219  2itscp  50224  itscnhlinecirc02p  50228  sepfsepc  50373  2ne3  51370  veronesev2lem  51402  veronesev4lem  51404  veronesev5lem  51405  veronesev6lem  51406  veronesevrowd  51407  veroquadgsumlem  51411