Theorem 2re 12206

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 12195	. 2 ⊢ 2 = (1 + 1)
2		1re 11119	. . 3 ⊢ 1 ∈ ℝ
3	2, 2	readdcli 11134	. 2 ⊢ (1 + 1) ∈ ℝ
4	1, 3	eqeltri 2829	1 ⊢ 2 ∈ ℝ

Syntax hints:   ∈ wcel 2113  (class class class)co 7352  ℝcr 11012  1c1 11014   + caddc 11016  2c2 12187

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2705  ax-1cn 11071  ax-icn 11072  ax-addcl 11073  ax-addrcl 11074  ax-mulcl 11075  ax-mulrcl 11076  ax-i2m1 11081  ax-1ne0 11082  ax-rrecex 11085  ax-cnre 11086

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-ne 2930  df-ral 3049  df-rex 3058  df-rab 3397  df-v 3439  df-dif 3901  df-un 3903  df-ss 3915  df-nul 4283  df-if 4475  df-sn 4576  df-pr 4578  df-op 4582  df-uni 4859  df-br 5094  df-iota 6442  df-fv 6494  df-ov 7355  df-2 12195

This theorem is referenced by:  2cnALT  12208  3re  12212  3pos  12237  2lt3  12299  1lt3  12300  2lt4  12302  1lt4  12303  2lt5  12306  2lt6  12311  1lt6  12312  2lt7  12317  1lt7  12318  2lt8  12324  1lt8  12325  2lt9  12332  1lt9  12333  1le2  12336  2rene0  12338  halfre  12341  halfgt0  12343  halflt1  12345  rehalfcl  12355  halfpos2  12357  halfnneg2  12359  addltmul  12364  nominpos  12365  avglt1  12366  avglt2  12367  div4p1lem1div2  12383  nn0lele2xi  12444  nn0n0n1ge2b  12457  nn0ge2m1nn  12458  nn0le2is012  12543  halfnz  12557  3halfnz  12558  2lt10  12732  1lt10  12733  uzuzle23  12784  uzuzle24  12785  uz3m2nn  12794  2rp  12897  ge2halflem1  13009  xnn0n0n1ge2b  13033  fztpval  13488  fz0to4untppr  13532  fz0to5un2tp  13533  fzo0to42pr  13655  flhalf  13736  fldiv4p1lem1div2  13741  2txmodxeq0  13840  expubnd  14087  expmulnbnd  14144  nn0opthlem2  14178  faclbnd2  14200  faclbnd4lem1  14202  faclbnd5  14207  4bc2eq6  14238  hashgt23el  14333  hashfun  14346  hashge2el2dif  14389  hashge2el2difr  14390  hash3tpde  14402  wrdlenge2n0  14461  f1oun2prg  14826  01sqrexlem7  15157  sqrt4  15181  sqrt2gt1lt2  15183  abstri  15240  sqreulem  15269  amgm2  15279  caucvgrlem  15582  climcndslem1  15758  climcndslem2  15759  climcnds  15760  efcllem  15986  ege2le3  15999  ef01bndlem  16095  cos01bnd  16097  cos2bnd  16099  cos01gt0  16102  sin02gt0  16103  sincos2sgn  16105  sin4lt0  16106  eirrlem  16115  egt2lt3  16117  epos  16118  ene1  16121  sqrt2re  16161  mod2eq1n2dvds  16260  oddge22np1  16262  evennn2n  16264  nn0o1gt2  16294  nno  16295  nn0o  16296  nnoddm1d2  16299  bitsp1o  16346  bitsfzolem  16347  bitsfzo  16348  bitsfi  16350  6gcd4e2  16451  2mulprm  16606  ge2nprmge4  16614  isprm7  16621  3lcm2e6  16645  prmreclem2  16831  prmreclem6  16835  4sqlem11  16869  4sqlem12  16870  prmgaplem7  16971  2expltfac  17006  plusgndxnmulrndx  17203  starvndxnplusgndx  17211  scandxnplusgndx  17223  vscandxnplusgndx  17228  ipndxnplusgndx  17239  tsetndxnplusgndx  17263  plendxnplusgndx  17277  dsndxnplusgndx  17296  slotsdifunifndx  17307  efgredleme  19657  zringndrg  21407  chfacfscmul0  22774  chfacfpmmul0  22778  psmetge0  24228  xmetge0  24260  bl2in  24316  metnrmlem3  24778  iihalf1  24853  iihalf2  24856  pcoass  24952  tcphcphlem1  25163  csbren  25327  trirn  25328  minveclem2  25354  minveclem4  25360  pjthlem1  25365  ovolunlem1a  25425  dyadss  25523  opnmbllem  25530  vitalilem2  25538  vitalilem4  25540  mbfi1fseqlem5  25648  lhop1lem  25946  aaliou3lem2  26279  aaliou3lem8  26281  pilem2  26390  pilem3  26391  pipos  26396  sinhalfpilem  26400  sincosq1lem  26434  sincosq4sgn  26438  tangtx  26442  sinq12gt0  26444  sincos4thpi  26450  tan4thpi  26451  tan4thpiOLD  26452  sincos6thpi  26453  sineq0  26461  cos02pilt1  26463  cosq34lt1  26464  cosordlem  26467  cos0pilt1  26469  tanord1  26474  efif1olem1  26479  efif1olem2  26480  efif1olem4  26482  efif1o  26483  efifo  26484  2irrexpq  26668  cxpcn3lem  26685  root1id  26692  root1eq1  26693  root1cj  26694  cxpeq  26695  2logb9irr  26733  2logb3irr  26735  ang180lem1  26747  ang180lem2  26748  chordthmlem2  26771  1cubrlem  26779  atancj  26848  atantan  26861  atanbndlem  26863  atans2  26869  leibpi  26880  log2tlbnd  26883  log2ublem2  26885  log2ub  26887  divsqrtsumlem  26918  harmonicbnd3  26946  zetacvg  26953  lgamgulmlem2  26968  lgamgulmlem3  26969  lgamgulmlem4  26970  lgamgulmlem6  26972  lgamucov  26976  basellem1  27019  basellem2  27020  basellem3  27021  basellem5  27023  chtdif  27096  ppidif  27101  ppinncl  27112  chtrpcl  27113  ppieq0  27114  ppiltx  27115  ppiublem1  27141  ppiub  27143  chpeq0  27147  chteq0  27148  chtublem  27150  chtub  27151  chpval2  27157  chpub  27159  mersenne  27166  perfectlem1  27168  perfectlem2  27169  dchrptlem1  27203  dchrptlem2  27204  bcmono  27216  bclbnd  27219  bpos1lem  27221  bposlem1  27223  bposlem2  27224  bposlem3  27225  bposlem4  27226  bposlem5  27227  bposlem6  27228  bposlem7  27229  bposlem8  27230  bposlem9  27231  lgslem1  27236  lgsdirprm  27270  gausslemma2dlem0c  27297  gausslemma2dlem1a  27304  gausslemma2dlem2  27306  gausslemma2dlem3  27307  lgseisenlem1  27314  lgseisenlem2  27315  lgseisenlem3  27316  lgseisen  27318  lgsquadlem1  27319  lgsquadlem2  27320  m1lgs  27327  2lgslem1a1  27328  2lgslem1a2  27329  2lgslem1c  27332  2lgslem4  27345  2sqlem11  27368  2sq2  27372  2sqreultlem  27386  2sqreunnltlem  27389  chebbnd1lem1  27408  chebbnd1lem2  27409  chebbnd1lem3  27410  chebbnd1  27411  chtppilimlem1  27412  chtppilimlem2  27413  chtppilim  27414  chto1ub  27415  chebbnd2  27416  chto1lb  27417  chpchtlim  27418  chpo1ub  27419  chpo1ubb  27420  rplogsumlem1  27423  rplogsumlem2  27424  dchrisumlem2  27429  dchrisumlem3  27430  dchrvmasumiflem1  27440  dchrisum0fno1  27450  dchrisum0re  27452  dchrisum0lem1b  27454  dchrisum0lem1  27455  dchrisum0lem2  27457  rplogsum  27466  mulog2sumlem1  27473  mulog2sumlem2  27474  log2sumbnd  27483  selberglem2  27485  selbergb  27488  selberg2b  27491  chpdifbndlem1  27492  logdivbnd  27495  selberg3lem1  27496  selberg3  27498  selberg4lem1  27499  selberg4  27500  pntrmax  27503  pntrsumbnd2  27506  selberg3r  27508  selberg4r  27509  selberg34r  27510  pntrlog2bndlem2  27517  pntrlog2bndlem3  27518  pntrlog2bndlem4  27519  pntrlog2bndlem5  27520  pntrlog2bndlem6  27522  pntrlog2bnd  27523  pntpbnd1a  27524  pntpbnd1  27525  pntpbnd2  27526  pntpbnd  27527  pntibndlem2  27530  pntibndlem3  27531  pntibnd  27532  pntlemb  27536  pntlemg  27537  pntlemh  27538  pntlemr  27541  pntlemk  27545  pntlemo  27546  pnt2  27552  pnt  27553  ostth2lem1  27557  ostth3  27577  slotsinbpsd  28420  slotslnbpsd  28421  istrkg3ld  28440  tgldimor  28481  trgcgrg  28494  tgcgr4  28510  axlowdimlem6  28927  axlowdimlem16  28937  axlowdimlem17  28938  axlowdim  28941  upgrfi  29071  umgrupgr  29083  umgrislfupgrlem  29102  umgrislfupgr  29103  lfgrnloop  29105  usgruspgr  29160  usgrislfuspgr  29167  lfuhgr1v0e  29234  usgrexmpldifpr  29238  usgrexmplef  29239  nbusgrvtxm1  29359  vdegp1bi  29518  upgrewlkle2  29587  lfgrwlkprop  29666  upgr2pthnlp  29712  usgr2pthlem  29743  pthdlem1  29746  wwlksm1edg  29861  wwlksnextwrd  29877  wwlksnextfun  29878  wwlksnextinj  29879  wwlksnextproplem3  29891  clwlkclwwlklem2a1  29974  clwlkclwwlklem2a2  29975  clwlkclwwlklem2fv1  29977  clwlkclwwlklem2fv2  29978  clwlkclwwlklem2a4  29979  clwlkclwwlklem2a  29980  clwlkclwwlklem2  29982  clwlkclwwlk2  29985  clwlkclwwlkf  29990  clwwlkext2edg  30038  konigsbergiedgw  30230  konigsbergssiedgw  30232  konigsberglem1  30234  konigsberglem2  30235  konigsberglem3  30236  konigsberg  30239  frgrreggt1  30375  ex-pss  30410  ex-res  30423  ex-fv  30425  ex-fl  30429  ex-mod  30431  ex-abs  30437  nrt2irr  30455  ipidsq  30692  minvecolem2  30857  minvecolem4  30862  normlem7  31098  norm-ii-i  31119  norm3lemt  31134  normpar2i  31138  bcsiALT  31161  pjhthlem1  31373  opsqrlem6  32127  cdj3lem1  32416  addltmulALT  32428  nexple  32832  2exple2exp  32833  threehalves  32902  pfx1s2  32927  wrdt2ind  32941  cyc3conja  33133  drngidlhash  33406  evl1deg3  33548  rtelextdg2lem  33760  fldext2chn  33762  constraddcl  33796  iconstr  33800  2sqr3minply  33814  2sqr3nconstr  33815  cos9thpinconstrlem1  33823  cos9thpinconstrlem2  33824  sqsscirc1  33942  dya2iocucvr  34318  omssubadd  34334  oddpwdc  34388  eulerpartlemgc  34396  fibp1  34435  coinfliplem  34513  coinflipspace  34515  ballotlem2  34523  signstfveq0  34611  prodfzo03  34637  hgt750lemd  34682  logdivsqrle  34684  hgt750lem  34685  hgt750lem2  34686  hgt750leme  34692  lfuhgr2  35184  usgrcyclgt2v  35196  acycgr2v  35215  subfacp1lem1  35244  subfacp1lem5  35249  subfacval3  35254  problem2  35731  problem5  35734  circum  35739  nn0prpwlem  36387  dnibndlem10  36552  knoppcnlem2  36559  knoppcnlem4  36561  knoppcnlem10  36567  unbdqndv2lem1  36574  knoppndvlem1  36577  knoppndvlem10  36586  knoppndvlem11  36587  knoppndvlem12  36588  knoppndvlem14  36590  knoppndvlem15  36591  knoppndvlem17  36593  knoppndvlem18  36594  knoppndvlem19  36595  knoppndvlem20  36596  knoppndvlem21  36597  cnndvlem1  36602  taupi  37388  iccioo01  37392  relowlpssretop  37429  sin2h  37670  cos2h  37671  tan2h  37672  poimirlem7  37687  poimirlem9  37689  opnmbllem0  37716  mblfinlem1  37717  mblfinlem2  37718  itg2addnclem  37731  isbnd2  37843  isbnd3  37844  heiborlem7  37877  12gcd5e1  42116  lcm2un  42127  lcmineqlem19  42160  lcmineqlem20  42161  lcmineqlem22  42163  3lexlogpow5ineq2  42168  3lexlogpow5ineq4  42169  3lexlogpow5ineq3  42170  3lexlogpow2ineq1  42171  3lexlogpow2ineq2  42172  3lexlogpow5ineq5  42173  aks4d1lem1  42175  aks4d1p1p3  42182  aks4d1p1p2  42183  aks4d1p1p4  42184  aks4d1p1p6  42186  aks4d1p1p7  42187  aks4d1p1p5  42188  aks4d1p1  42189  aks4d1p2  42190  aks4d1p3  42191  aks4d1p5  42193  aks4d1p6  42194  aks4d1p7d1  42195  aks4d1p7  42196  aks4d1p8  42200  aks4d1p9  42201  posbezout  42213  aks6d1c3  42236  2np3bcnp1  42257  2ap1caineq  42258  aks6d1c6lem4  42286  aks6d1c7lem1  42293  aks6d1c7lem2  42294  oexpreposd  42440  asin1half  42475  remul02  42523  sn-0ne2  42524  remul01  42525  flt4lem7  42777  rabren3dioph  42932  pellexlem2  42947  pellexlem5  42950  pell14qrgapw  42993  pellfundex  43003  rmspecsqrtnq  43023  jm2.24nn  43076  jm2.17a  43077  jm2.17b  43078  jm2.17c  43079  acongrep  43097  acongeq  43100  jm2.22  43112  jm2.23  43113  jm2.20nn  43114  jm3.1lem2  43135  expdiophlem1  43138  sqrtcval  43758  imo72b2lem0  44282  lhe4.4ex1a  44446  isosctrlem1ALT  45050  sineq0ALT  45053  lt3addmuld  45426  suplesup  45462  infleinflem2  45493  infleinf  45494  sumnnodd  45754  0ellimcdiv  45771  sinaover2ne0  45990  stoweidlem13  46135  stoweidlem14  46136  stoweidlem26  46148  stoweidlem49  46171  stoweidlem52  46174  wallispilem4  46190  wallispilem5  46191  wallispi  46192  wallispi2lem1  46193  wallispi2lem2  46194  wallispi2  46195  stirlinglem1  46196  stirlinglem3  46198  stirlinglem5  46200  stirlinglem6  46201  stirlinglem7  46202  stirlinglem10  46205  stirlinglem11  46206  stirlinglem15  46210  stirlingr  46212  dirker2re  46214  dirkerval2  46216  dirkerre  46217  dirkerper  46218  dirkertrigeqlem1  46220  dirkertrigeqlem3  46222  dirkercncflem1  46225  dirkercncflem2  46226  dirkercncflem4  46228  fourierdlem24  46253  fourierdlem43  46272  fourierdlem44  46273  fourierdlem57  46285  fourierdlem58  46286  fourierdlem62  46290  fourierdlem66  46294  fourierdlem68  46296  fourierdlem72  46300  fourierdlem76  46304  fourierdlem78  46306  fourierdlem79  46307  fourierdlem94  46322  fourierdlem103  46331  fourierdlem104  46332  fourierdlem111  46339  fourierdlem113  46341  sqwvfoura  46350  sqwvfourb  46351  fourierswlem  46352  fouriersw  46353  etransclem23  46379  salexct2  46461  salexct3  46464  salgencntex  46465  salgensscntex  46466  sge0ad2en  46553  ovnsubaddlem1  46692  smfmullem4  46916  smf2id  46923  nthrucw  47008  2leaddle2  47422  p1lep2  47424  2ltceilhalf  47452  ceilhalfgt1  47453  2tceilhalfelfzo1  47456  rehalfge1  47459  ceilhalfnn  47460  ceil5half3  47464  difmodm1lt  47483  fmtnoge3  47654  fmtnof1  47659  fmtnoprmfac2lem1  47690  fmtno4prmfac  47696  fmtno4prm  47699  2pwp1prm  47713  31prm  47721  sfprmdvdsmersenne  47727  lighneallem2  47730  lighneallem4a  47732  lighneallem4b  47733  requad01  47745  requad1  47746  requad2  47747  dfodd4  47783  nn0o1gt2ALTV  47818  nnoALTV  47819  nn0oALTV  47820  nn0e  47821  nneven  47822  perfectALTVlem1  47845  perfectALTVlem2  47846  341fppr2  47858  9fppr8  47861  fpprel2  47865  nfermltl2rev  47867  gbowgt5  47886  sbgoldbalt  47905  sgoldbeven3prm  47907  mogoldbb  47909  nnsum3primes4  47912  nnsum3primesgbe  47916  nnsum3primesle9  47918  nnsum4primesodd  47920  nnsum4primesoddALTV  47921  wtgoldbnnsum4prm  47926  bgoldbnnsum3prm  47928  cycl3grtri  48071  usgrexmpl1lem  48145  usgrexmpl2lem  48150  usgrexmpl2nb2  48157  usgrexmpl2nb3  48158  usgrexmpl2nb4  48159  usgrexmpl2nb5  48160  usgrexmpl2trifr  48161  gpgprismgrusgra  48182  gpg5nbgrvtx13starlem2  48196  gpg3nbgrvtx0  48200  gpg3kgrtriexlem1  48207  cznnring  48386  ply1mulgsumlem2  48512  zlmodzxznm  48622  zlmodzxzldeplem  48623  nn0eo  48653  flnn0div2ge  48658  rege1logbzge0  48684  fldivexpfllog2  48690  logbpw2m1  48692  fllog2  48693  blenpw2m1  48704  nnpw2blen  48705  nnolog2flm1  48715  blennngt2o2  48717  dig2nn1st  48730  dig2nn0  48736  dig2bits  48739  dignn0flhalflem1  48740  dignn0flhalflem2  48741  dignn0flhalf  48743  nn0sumshdiglemA  48744  ackval42  48821  rrx2xpref1o  48843  itscnhlc0yqe  48884  itsclquadb  48901  2itscp  48906  itscnhlinecirc02p  48910  sepfsepc  49052