Theorem 2re 12330

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 12318	. 2 ⊢ 2 = (1 + 1)
2		1re 11223	. . 3 ⊢ 1 ∈ ℝ
3	2, 2	readdcli 11239	. 2 ⊢ (1 + 1) ∈ ℝ
4	1, 3	eqeltri 2861	1 ⊢ 2 ∈ ℝ

This proof depends on syntax axioms:   ∈ wcel 2146  (class class class)co 7419  ℝcr 11114  1c1 11116   + caddc 11118  2c2 12310

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 2148  ax-9 2156  ax-ext 2737  ax-1cn 11173  ax-icn 11174  ax-addcl 11175  ax-addrcl 11176  ax-mulcl 11177  ax-mulrcl 11178  ax-i2m1 11183  ax-1ne0 11184  ax-rrecex 11187  ax-cnre 11188

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 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-ne 2961  df-ral 3082  df-rex 3092  df-rab 3419  df-v 3459  df-dif 3909  df-un 3911  df-ss 3923  df-nul 4287  df-if 4490  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4875  df-br 5112  df-iota 6496  df-fv 6548  df-ov 7422  df-2 12318

This theorem is used by:  2cnALT  12332  3re  12336  0le2  12358  2lt3  12429  2le3  12430  1lt3  12431  2lt4  12433  1lt4  12434  2lt5  12437  2lt6  12442  1lt6  12443  2lt7  12448  1lt7  12449  2lt8  12455  1lt8  12456  2lt9  12463  1lt9  12464  1le2  12467  2rene0  12469  halfre  12472  halfgt0  12474  halflt1  12476  rehalfcl  12486  halfpos2  12488  halfnneg2  12490  addltmul  12495  nominpos  12496  avglt1  12497  avglt2  12498  div4p1lem1div2  12514  nn0lele2xi  12575  nn0n0n1ge2b  12588  nn0ge2m1nn  12589  nn0le2is012  12676  halfnz  12690  3halfnz  12691  2lt10  12871  1lt10OLD  12873  uzuzle23  12924  uzuzle24  12925  uz3m2nn  12934  2rp  13037  ge2halflem1  13149  xnn0n0n1ge2b  13173  fztpval  13631  fz0to4untppr  13675  fz0to5un2tp  13676  fzo0to42pr  13799  flhalf  13881  fldiv4p1lem1div2  13886  2txmodxeq0  13985  expubnd  14232  expmulnbnd  14289  nn0opthlem2  14323  faclbnd2  14345  faclbnd4lem1  14347  faclbnd5  14352  4bc2eq6  14383  hashgt23el  14479  hashfun  14492  hashge2el2dif  14535  hashge2el2difr  14536  hash3tpde  14548  wrdlenge2n0  14607  f1oun2prg  14978  01sqrexlem7  15323  sqrt4  15347  sqrt2gt1lt2  15349  abstri  15406  sqreulem  15435  amgm2  15445  caucvgrlem  15748  climcndslem1  15926  climcndslem2  15927  climcnds  15928  efcllem  16153  ege2le3  16166  ef01bndlem  16262  cos01bnd  16264  cos2bnd  16266  cos01gt0  16269  sin02gt0  16270  sincos2sgn  16272  sin4lt0  16273  eirrlem  16282  egt2lt3  16284  epos  16285  ene1  16288  sqrt2re  16328  mod2eq1n2dvds  16427  oddge22np1  16429  evennn2n  16431  nn0o1gt2  16461  nno  16462  nn0o  16463  nnoddm1d2  16466  bitsp1o  16513  bitsfzolem  16514  bitsfzo  16515  bitsfi  16517  6gcd4e2  16618  2mulprm  16773  ge2nprmge4  16782  isprm7  16789  3lcm2e6  16813  prmreclem2  16999  prmreclem6  17003  4sqlem11  17037  4sqlem12  17038  prmgaplem7  17139  2expltfac  17174  plusgndxnmulrndx  17372  starvndxnplusgndx  17380  scandxnplusgndx  17392  vscandxnplusgndx  17397  ipndxnplusgndx  17408  tsetndxnplusgndx  17432  plendxnplusgndx  17446  dsndxnplusgndx  17465  slotsdifunifndx  17476  efgredleme  19857  zringndrg  21668  chfacfscmul0  23065  chfacfpmmul0  23069  psmetge0  24520  xmetge0  24552  bl2in  24608  metnrmlem3  25070  iihalf1  25141  iihalf2  25143  pcoass  25234  tcphcphlem1  25445  csbren  25609  trirn  25610  minveclem2  25636  minveclem4  25642  pjthlem1  25647  ovolunlem1a  25706  dyadss  25804  opnmbllem  25811  vitalilem2  25819  vitalilem4  25821  mbfi1fseqlem5  25929  lhop1lem  26223  aaliou3lem2  26557  aaliou3lem8  26559  pilem2  26666  pilem3  26667  2pire  26671  pipos  26674  sinhalfpilem  26679  sincosq1lem  26713  sincosq4sgn  26717  tangtx  26721  sinq12gt0  26723  sincos4thpi  26729  tan4thpi  26730  tan4thpiOLD  26731  sincos6thpi  26732  sineq0  26740  cos02pilt1  26742  cosq34lt1  26743  cosordlem  26746  cos0pilt1  26748  tanord1  26753  efif1olem1  26758  efif1olem2  26759  efif1olem4  26761  efif1o  26762  efifo  26763  2irrexpq  26947  cxpcn3lem  26963  root1id  26970  root1eq1  26971  root1cj  26972  cxpeq  26973  2logb9irr  27011  2logb3irr  27013  ang180lem1  27025  ang180lem2  27026  chordthmlem2  27049  1cubrlem  27057  atancj  27126  atantan  27139  atanbndlem  27141  atans2  27147  leibpi  27158  log2tlbnd  27161  log2ublem2  27163  log2ub  27165  divsqrtsumlem  27195  harmonicbnd3  27223  zetacvg  27230  lgamgulmlem2  27245  lgamgulmlem3  27246  lgamgulmlem4  27247  lgamgulmlem6  27249  lgamucov  27253  basellem1  27296  basellem2  27297  basellem3  27298  basellem5  27300  chtdif  27373  ppidif  27378  ppinncl  27389  chtrpcl  27390  ppieq0  27391  ppiltx  27392  ppiublem1  27417  ppiub  27419  chpeq0  27423  chteq0  27424  chtublem  27426  chtub  27427  chpval2  27433  chpub  27435  mersenne  27442  perfectlem1  27444  perfectlem2  27445  dchrptlem1  27479  dchrptlem2  27480  bcmono  27492  bclbnd  27495  bpos1lem  27497  bposlem1  27499  bposlem2  27500  bposlem3  27501  bposlem4  27502  bposlem5  27503  bposlem6  27504  bposlem7  27505  bposlem8  27506  bposlem9  27507  lgslem1  27512  lgsdirprm  27546  gausslemma2dlem0c  27573  gausslemma2dlem1a  27580  gausslemma2dlem2  27582  gausslemma2dlem3  27583  lgseisenlem1  27590  lgseisenlem2  27591  lgseisenlem3  27592  lgseisen  27594  lgsquadlem1  27595  lgsquadlem2  27596  m1lgs  27603  2lgslem1a1  27604  2lgslem1a2  27605  2lgslem1c  27608  2lgslem4  27621  2sqlem11  27644  2sq2  27648  2sqreultlem  27662  2sqreunnltlem  27665  chebbnd1lem1  27684  chebbnd1lem2  27685  chebbnd1lem3  27686  chebbnd1  27687  chtppilimlem1  27688  chtppilimlem2  27689  chtppilim  27690  chto1ub  27691  chebbnd2  27692  chto1lb  27693  chpchtlim  27694  chpo1ub  27695  chpo1ubb  27696  rplogsumlem1  27699  rplogsumlem2  27700  dchrisumlem2  27705  dchrisumlem3  27706  dchrvmasumiflem1  27716  dchrisum0fno1  27726  dchrisum0re  27728  dchrisum0lem1b  27730  dchrisum0lem1  27731  dchrisum0lem2  27733  rplogsum  27742  mulog2sumlem1  27749  mulog2sumlem2  27750  log2sumbnd  27759  selberglem2  27761  selbergb  27764  selberg2b  27767  chpdifbndlem1  27768  logdivbnd  27771  selberg3lem1  27772  selberg3  27774  selberg4lem1  27775  selberg4  27776  pntrmax  27779  pntrsumbnd2  27782  selberg3r  27784  selberg4r  27785  selberg34r  27786  pntrlog2bndlem2  27793  pntrlog2bndlem3  27794  pntrlog2bndlem4  27795  pntrlog2bndlem5  27796  pntrlog2bndlem6  27798  pntrlog2bnd  27799  pntpbnd1a  27800  pntpbnd1  27801  pntpbnd2  27802  pntpbnd  27803  pntibndlem2  27806  pntibndlem3  27807  pntibnd  27808  pntlemb  27812  pntlemg  27813  pntlemh  27814  pntlemr  27817  pntlemk  27821  pntlemo  27822  pnt2  27828  pnt  27829  ostth2lem1  27833  ostth3  27853  slotsinbpsd  28761  slotslnbpsd  28762  istrkg3ld  28781  tgldimor  28822  trgcgrg  28835  tgcgr4  28851  axlowdimlem6  29352  axlowdimlem16  29362  axlowdimlem17  29363  axlowdim  29366  upgrfi  29496  umgrupgr  29508  umgrislfupgrlem  29527  umgrislfupgr  29528  lfgrnloop  29530  lfuhgr2  29554  usgruspgr  29588  usgrislfuspgr  29595  lfuhgr1v0e  29662  usgrexmpldifpr  29666  usgrexmplef  29667  nbusgrvtxm1  29787  vdegp1bi  29945  upgrewlkle2  30014  lfgrwlkprop  30097  upgr2pthnlp  30145  usgr2pthlem  30176  pthdlem1  30179  wwlksm1edg  30297  wwlksnextwrd  30313  wwlksnextfun  30314  wwlksnextinj  30315  wwlksnextproplem3  30327  clwlkclwwlklem2a1  30410  clwlkclwwlklem2a2  30411  clwlkclwwlklem2fv1  30413  clwlkclwwlklem2fv2  30414  clwlkclwwlklem2a4  30415  clwlkclwwlklem2a  30416  clwlkclwwlklem2  30418  clwlkclwwlk2  30421  clwlkclwwlkf  30426  clwwlkext2edg  30474  konigsbergiedgw  30670  konigsbergssiedgw  30672  konigsberglem1  30674  konigsberglem2  30675  konigsberglem3  30676  konigsberg  30679  frgrreggt1  30815  ex-pss  30850  ex-res  30863  ex-fv  30865  ex-fl  30869  ex-mod  30871  ex-abs  30877  nrt2irr  30895  ipidsq  31133  minvecolem2  31298  minvecolem4  31303  normlem7  31539  norm-ii-i  31560  norm3lemt  31575  normpar2i  31579  bcsiALT  31602  pjhthlem1  31814  opsqrlem6  32568  cdj3lem1  32857  addltmulALT  32869  nexple  33247  2exple2exp  33248  threehalves  33304  pfx1s2  33329  wrdt2ind  33339  cyc3conja  33541  drngidlhash  33805  evl1deg3  33932  rtelextdg2lem  34180  fldext2chn  34182  constraddcl  34216  iconstr  34220  2sqr3minply  34234  2sqr3nconstr  34235  cos9thpinconstrlem1  34243  cos9thpinconstrlem2  34244  sqsscirc1  34362  dya2iocucvr  34739  omssubadd  34755  oddpwdc  34809  eulerpartlemgc  34817  fibp1  34856  coinfliplem  34934  coinflipspace  34936  ballotlem2  34944  signstfveq0  35029  prodfzo03  35055  hgt750lemd  35100  logdivsqrle  35102  hgt750lem  35103  hgt750lem2  35104  hgt750leme  35110  usgrcyclgt2v  35668  acycgr2v  35679  subfacp1lem1  35708  subfacp1lem5  35713  subfacval3  35718  problem2  36195  problem5  36198  circum  36203  nn0prpwlem  36890  dnibndlem10  37133  knoppcnlem2  37140  knoppcnlem4  37142  knoppcnlem10  37148  unbdqndv2lem1  37155  knoppndvlem1  37158  knoppndvlem10  37167  knoppndvlem11  37168  knoppndvlem12  37169  knoppndvlem14  37171  knoppndvlem15  37172  knoppndvlem17  37174  knoppndvlem18  37175  knoppndvlem19  37176  knoppndvlem20  37177  knoppndvlem21  37178  cnndvlem1  37183  taupi  38024  iccioo01  38030  relowlpssretop  38067  sin2h  38318  cos2h  38319  tan2h  38320  poimirlem7  38335  poimirlem9  38337  opnmbllem0  38364  mblfinlem1  38365  mblfinlem2  38366  itg2addnclem  38379  isbnd2  38492  isbnd3  38493  heiborlem7  38526  12gcd5e1  42828  lcm2un  42839  lcmineqlem19  42872  lcmineqlem20  42873  lcmineqlem22  42875  3lexlogpow5ineq2  42880  3lexlogpow5ineq4  42881  3lexlogpow5ineq3  42882  3lexlogpow2ineq1  42883  3lexlogpow2ineq2  42884  3lexlogpow5ineq5  42885  aks4d1lem1  42887  aks4d1p1p3  42894  aks4d1p1p2  42895  aks4d1p1p4  42896  aks4d1p1p6  42898  aks4d1p1p7  42899  aks4d1p1p5  42900  aks4d1p1  42901  aks4d1p2  42902  aks4d1p3  42903  aks4d1p5  42905  aks4d1p6  42906  aks4d1p7d1  42907  aks4d1p7  42908  aks4d1p8  42912  aks4d1p9  42913  posbezout  42925  aks6d1c3  42948  2np3bcnp1  42969  2ap1caineq  42970  aks6d1c6lem4  42998  aks6d1c7lem1  43005  aks6d1c7lem2  43006  oexpreposd  43141  asin1half  43176  remul02  43224  sn-0ne2  43225  remul01  43226  flt4lem7  43449  rabren3dioph  43600  pellexlem2  43615  pellexlem5  43618  pell14qrgapw  43661  pellfundex  43671  rmspecsqrtnq  43691  jm2.24nn  43744  jm2.17a  43745  jm2.17b  43746  jm2.17c  43747  acongrep  43765  acongeq  43768  jm2.22  43780  jm2.23  43781  jm3.1lem2  43803  expdiophlem1  43806  sqrtcval  44425  imo72b2lem0  44949  lhe4.4ex1a  45097  isosctrlem1ALT  45700  sineq0ALT  45703  lt3addmuld  46078  suplesup  46113  infleinflem2  46144  infleinf  46145  sumnnodd  46404  0ellimcdiv  46421  sinaover2ne0  46640  stoweidlem13  46785  stoweidlem14  46786  stoweidlem26  46798  stoweidlem49  46821  stoweidlem52  46824  wallispilem4  46840  wallispilem5  46841  wallispi  46842  wallispi2lem1  46843  wallispi2lem2  46844  wallispi2  46845  stirlinglem1  46846  stirlinglem3  46848  stirlinglem5  46850  stirlinglem6  46851  stirlinglem7  46852  stirlinglem10  46855  stirlinglem11  46856  stirlinglem15  46860  stirlingr  46862  dirker2re  46864  dirkerval2  46866  dirkerre  46867  dirkertrigeqlem1  46870  dirkertrigeqlem3  46872  dirkercncflem1  46875  dirkercncflem4  46878  fourierdlem24  46903  fourierdlem43  46922  fourierdlem44  46923  fourierdlem57  46935  fourierdlem58  46936  fourierdlem62  46940  fourierdlem66  46944  fourierdlem68  46946  fourierdlem72  46950  fourierdlem76  46954  fourierdlem78  46956  fourierdlem79  46957  fourierdlem94  46972  fourierdlem103  46981  fourierdlem104  46982  fourierdlem111  46989  sqwvfoura  47000  sqwvfourb  47001  fourierswlem  47002  fouriersw  47003  etransclem23  47029  salexct2  47111  salexct3  47114  salgencntex  47115  salgensscntex  47116  sge0ad2en  47203  ovnsubaddlem1  47342  smfmullem4  47566  smf2id  47573  goldrarr  47676  goldrapos  47678  2leaddle2  48093  p1lep2  48095  2ltceilhalf  48127  ceilhalfgt1  48128  2tceilhalfelfzo1  48131  rehalfge1  48134  ceilhalfnn  48135  ceil5half3  48141  difmodm1lt  48160  2timesltsq  48173  2timesltsqm1  48174  fmtnoge3  48340  fmtnof1  48345  fmtnoprmfac2lem1  48376  fmtno4prmfac  48382  fmtno4prm  48385  2pwp1prm  48399  31prm  48407  sfprmdvdsmersenne  48413  lighneallem2  48416  lighneallem4a  48418  lighneallem4b  48419  nprmdvdsfacm1lem2  48431  nprmdvdsfacm1lem4  48433  ppivalnnnprmge6  48436  requad01  48444  requad1  48445  requad2  48446  dfodd4  48482  nn0o1gt2ALTV  48517  nnoALTV  48518  nn0oALTV  48519  nn0e  48520  nneven  48521  perfectALTVlem1  48544  perfectALTVlem2  48545  341fppr2  48557  9fppr8  48560  fpprel2  48564  nfermltl2rev  48566  gbowgt5  48585  sbgoldbalt  48604  sgoldbeven3prm  48606  mogoldbb  48608  nnsum3primes4  48611  nnsum3primesgbe  48615  nnsum3primesle9  48617  nnsum4primesodd  48619  nnsum4primesoddALTV  48620  wtgoldbnnsum4prm  48625  bgoldbnnsum3prm  48627  cycl3grtri  48770  usgrexmpl1lem  48844  usgrexmpl2lem  48849  usgrexmpl2nb2  48856  usgrexmpl2nb3  48857  usgrexmpl2nb4  48858  usgrexmpl2nb5  48859  usgrexmpl2trifr  48860  gpgprismgrusgra  48881  gpg5nbgrvtx13starlem2  48895  gpg3nbgrvtx0  48899  gpg3kgrtriexlem1  48906  cznnring  49084  ply1mulgsumlem2  49224  zlmodzxznm  49334  zlmodzxzldeplem  49335  nn0eo  49365  flnn0div2ge  49370  rege1logbzge0  49396  fldivexpfllog2  49402  logbpw2m1  49404  fllog2  49405  blenpw2m1  49416  nnpw2blen  49417  nnolog2flm1  49427  blennngt2o2  49429  dig2nn1st  49442  dig2nn0  49448  dig2bits  49451  dignn0flhalflem1  49452  dignn0flhalflem2  49453  dignn0flhalf  49455  nn0sumshdiglemA  49456  ackval42  49533  rrx2xpref1o  49555  itscnhlc0yqe  49596  itsclquadb  49613  2itscp  49618  itscnhlinecirc02p  49622  sepfsepc  49763  2ne3  50681