Theorem 2re 12202

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 12191	. 2 ⊢ 2 = (1 + 1)
2		1re 11115	. . 3 ⊢ 1 ∈ ℝ
3	2, 2	readdcli 11130	. 2 ⊢ (1 + 1) ∈ ℝ
4	1, 3	eqeltri 2824	1 ⊢ 2 ∈ ℝ

Syntax hints:   ∈ wcel 2109  (class class class)co 7349  ℝcr 11008  1c1 11010   + caddc 11012  2c2 12183

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 2701  ax-1cn 11067  ax-icn 11068  ax-addcl 11069  ax-addrcl 11070  ax-mulcl 11071  ax-mulrcl 11072  ax-i2m1 11077  ax-1ne0 11078  ax-rrecex 11081  ax-cnre 11082

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 2708  df-cleq 2721  df-clel 2803  df-ne 2926  df-ral 3045  df-rex 3054  df-rab 3395  df-v 3438  df-dif 3906  df-un 3908  df-ss 3920  df-nul 4285  df-if 4477  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4859  df-br 5093  df-iota 6438  df-fv 6490  df-ov 7352  df-2 12191

This theorem is referenced by:  2cnALT  12204  3re  12208  3pos  12233  2lt3  12295  1lt3  12296  2lt4  12298  1lt4  12299  2lt5  12302  2lt6  12307  1lt6  12308  2lt7  12313  1lt7  12314  2lt8  12320  1lt8  12321  2lt9  12328  1lt9  12329  1le2  12332  2rene0  12334  halfre  12337  halfgt0  12339  halflt1  12341  rehalfcl  12351  halfpos2  12353  halfnneg2  12355  addltmul  12360  nominpos  12361  avglt1  12362  avglt2  12363  div4p1lem1div2  12379  nn0lele2xi  12440  nn0n0n1ge2b  12453  nn0ge2m1nn  12454  nn0le2is012  12540  halfnz  12554  3halfnz  12555  2lt10  12729  1lt10  12730  uzuzle23  12785  uzuzle24  12786  uz3m2nn  12795  2rp  12898  ge2halflem1  13010  xnn0n0n1ge2b  13034  fztpval  13489  fz0to4untppr  13533  fz0to5un2tp  13534  fzo0to42pr  13656  flhalf  13734  fldiv4p1lem1div2  13739  2txmodxeq0  13838  expubnd  14085  expmulnbnd  14142  nn0opthlem2  14176  faclbnd2  14198  faclbnd4lem1  14200  faclbnd5  14205  4bc2eq6  14236  hashgt23el  14331  hashfun  14344  hashge2el2dif  14387  hashge2el2difr  14388  hash3tpde  14400  wrdlenge2n0  14459  f1oun2prg  14824  01sqrexlem7  15155  sqrt4  15179  sqrt2gt1lt2  15181  abstri  15238  sqreulem  15267  amgm2  15277  caucvgrlem  15580  climcndslem1  15756  climcndslem2  15757  climcnds  15758  efcllem  15984  ege2le3  15997  ef01bndlem  16093  cos01bnd  16095  cos2bnd  16097  cos01gt0  16100  sin02gt0  16101  sincos2sgn  16103  sin4lt0  16104  eirrlem  16113  egt2lt3  16115  epos  16116  ene1  16119  sqrt2re  16159  mod2eq1n2dvds  16258  oddge22np1  16260  evennn2n  16262  nn0o1gt2  16292  nno  16293  nn0o  16294  nnoddm1d2  16297  bitsp1o  16344  bitsfzolem  16345  bitsfzo  16346  bitsfi  16348  6gcd4e2  16449  2mulprm  16604  ge2nprmge4  16612  isprm7  16619  3lcm2e6  16643  prmreclem2  16829  prmreclem6  16833  4sqlem11  16867  4sqlem12  16868  prmgaplem7  16969  2expltfac  17004  plusgndxnmulrndx  17201  starvndxnplusgndx  17209  scandxnplusgndx  17221  vscandxnplusgndx  17226  ipndxnplusgndx  17237  tsetndxnplusgndx  17261  plendxnplusgndx  17275  dsndxnplusgndx  17294  slotsdifunifndx  17305  efgredleme  19622  zringndrg  21375  chfacfscmul0  22743  chfacfpmmul0  22747  psmetge0  24198  xmetge0  24230  bl2in  24286  metnrmlem3  24748  iihalf1  24823  iihalf2  24826  pcoass  24922  tcphcphlem1  25133  csbren  25297  trirn  25298  minveclem2  25324  minveclem4  25330  pjthlem1  25335  ovolunlem1a  25395  dyadss  25493  opnmbllem  25500  vitalilem2  25508  vitalilem4  25510  mbfi1fseqlem5  25618  lhop1lem  25916  aaliou3lem2  26249  aaliou3lem8  26251  pilem2  26360  pilem3  26361  pipos  26366  sinhalfpilem  26370  sincosq1lem  26404  sincosq4sgn  26408  tangtx  26412  sinq12gt0  26414  sincos4thpi  26420  tan4thpi  26421  tan4thpiOLD  26422  sincos6thpi  26423  sineq0  26431  cos02pilt1  26433  cosq34lt1  26434  cosordlem  26437  cos0pilt1  26439  tanord1  26444  efif1olem1  26449  efif1olem2  26450  efif1olem4  26452  efif1o  26453  efifo  26454  2irrexpq  26638  cxpcn3lem  26655  root1id  26662  root1eq1  26663  root1cj  26664  cxpeq  26665  2logb9irr  26703  2logb3irr  26705  ang180lem1  26717  ang180lem2  26718  chordthmlem2  26741  1cubrlem  26749  atancj  26818  atantan  26831  atanbndlem  26833  atans2  26839  leibpi  26850  log2tlbnd  26853  log2ublem2  26855  log2ub  26857  divsqrtsumlem  26888  harmonicbnd3  26916  zetacvg  26923  lgamgulmlem2  26938  lgamgulmlem3  26939  lgamgulmlem4  26940  lgamgulmlem6  26942  lgamucov  26946  basellem1  26989  basellem2  26990  basellem3  26991  basellem5  26993  chtdif  27066  ppidif  27071  ppinncl  27082  chtrpcl  27083  ppieq0  27084  ppiltx  27085  ppiublem1  27111  ppiub  27113  chpeq0  27117  chteq0  27118  chtublem  27120  chtub  27121  chpval2  27127  chpub  27129  mersenne  27136  perfectlem1  27138  perfectlem2  27139  dchrptlem1  27173  dchrptlem2  27174  bcmono  27186  bclbnd  27189  bpos1lem  27191  bposlem1  27193  bposlem2  27194  bposlem3  27195  bposlem4  27196  bposlem5  27197  bposlem6  27198  bposlem7  27199  bposlem8  27200  bposlem9  27201  lgslem1  27206  lgsdirprm  27240  gausslemma2dlem0c  27267  gausslemma2dlem1a  27274  gausslemma2dlem2  27276  gausslemma2dlem3  27277  lgseisenlem1  27284  lgseisenlem2  27285  lgseisenlem3  27286  lgseisen  27288  lgsquadlem1  27289  lgsquadlem2  27290  m1lgs  27297  2lgslem1a1  27298  2lgslem1a2  27299  2lgslem1c  27302  2lgslem4  27315  2sqlem11  27338  2sq2  27342  2sqreultlem  27356  2sqreunnltlem  27359  chebbnd1lem1  27378  chebbnd1lem2  27379  chebbnd1lem3  27380  chebbnd1  27381  chtppilimlem1  27382  chtppilimlem2  27383  chtppilim  27384  chto1ub  27385  chebbnd2  27386  chto1lb  27387  chpchtlim  27388  chpo1ub  27389  chpo1ubb  27390  rplogsumlem1  27393  rplogsumlem2  27394  dchrisumlem2  27399  dchrisumlem3  27400  dchrvmasumiflem1  27410  dchrisum0fno1  27420  dchrisum0re  27422  dchrisum0lem1b  27424  dchrisum0lem1  27425  dchrisum0lem2  27427  rplogsum  27436  mulog2sumlem1  27443  mulog2sumlem2  27444  log2sumbnd  27453  selberglem2  27455  selbergb  27458  selberg2b  27461  chpdifbndlem1  27462  logdivbnd  27465  selberg3lem1  27466  selberg3  27468  selberg4lem1  27469  selberg4  27470  pntrmax  27473  pntrsumbnd2  27476  selberg3r  27478  selberg4r  27479  selberg34r  27480  pntrlog2bndlem2  27487  pntrlog2bndlem3  27488  pntrlog2bndlem4  27489  pntrlog2bndlem5  27490  pntrlog2bndlem6  27492  pntrlog2bnd  27493  pntpbnd1a  27494  pntpbnd1  27495  pntpbnd2  27496  pntpbnd  27497  pntibndlem2  27500  pntibndlem3  27501  pntibnd  27502  pntlemb  27506  pntlemg  27507  pntlemh  27508  pntlemr  27511  pntlemk  27515  pntlemo  27516  pnt2  27522  pnt  27523  ostth2lem1  27527  ostth3  27547  slotsinbpsd  28386  slotslnbpsd  28387  istrkg3ld  28406  tgldimor  28447  trgcgrg  28460  tgcgr4  28476  axlowdimlem6  28892  axlowdimlem16  28902  axlowdimlem17  28903  axlowdim  28906  upgrfi  29036  umgrupgr  29048  umgrislfupgrlem  29067  umgrislfupgr  29068  lfgrnloop  29070  usgruspgr  29125  usgrislfuspgr  29132  lfuhgr1v0e  29199  usgrexmpldifpr  29203  usgrexmplef  29204  nbusgrvtxm1  29324  vdegp1bi  29483  upgrewlkle2  29552  lfgrwlkprop  29631  upgr2pthnlp  29677  usgr2pthlem  29708  pthdlem1  29711  wwlksm1edg  29826  wwlksnextwrd  29842  wwlksnextfun  29843  wwlksnextinj  29844  wwlksnextproplem3  29856  clwlkclwwlklem2a1  29936  clwlkclwwlklem2a2  29937  clwlkclwwlklem2fv1  29939  clwlkclwwlklem2fv2  29940  clwlkclwwlklem2a4  29941  clwlkclwwlklem2a  29942  clwlkclwwlklem2  29944  clwlkclwwlk2  29947  clwlkclwwlkf  29952  clwwlkext2edg  30000  konigsbergiedgw  30192  konigsbergssiedgw  30194  konigsberglem1  30196  konigsberglem2  30197  konigsberglem3  30198  konigsberg  30201  frgrreggt1  30337  ex-pss  30372  ex-res  30385  ex-fv  30387  ex-fl  30391  ex-mod  30393  ex-abs  30399  nrt2irr  30417  ipidsq  30654  minvecolem2  30819  minvecolem4  30824  normlem7  31060  norm-ii-i  31081  norm3lemt  31096  normpar2i  31100  bcsiALT  31123  pjhthlem1  31335  opsqrlem6  32089  cdj3lem1  32378  addltmulALT  32390  nexple  32789  2exple2exp  32790  threehalves  32855  pfx1s2  32880  wrdt2ind  32895  cyc3conja  33099  drngidlhash  33371  evl1deg3  33513  rtelextdg2lem  33693  fldext2chn  33695  constraddcl  33729  iconstr  33733  2sqr3minply  33747  2sqr3nconstr  33748  cos9thpinconstrlem1  33756  cos9thpinconstrlem2  33757  sqsscirc1  33875  dya2iocucvr  34252  omssubadd  34268  oddpwdc  34322  eulerpartlemgc  34330  fibp1  34369  coinfliplem  34447  coinflipspace  34449  ballotlem2  34457  signstfveq0  34545  prodfzo03  34571  hgt750lemd  34616  logdivsqrle  34618  hgt750lem  34619  hgt750lem2  34620  hgt750leme  34626  lfuhgr2  35092  usgrcyclgt2v  35104  acycgr2v  35123  subfacp1lem1  35152  subfacp1lem5  35157  subfacval3  35162  problem2  35639  problem5  35642  circum  35647  nn0prpwlem  36296  dnibndlem10  36461  knoppcnlem2  36468  knoppcnlem4  36470  knoppcnlem10  36476  unbdqndv2lem1  36483  knoppndvlem1  36486  knoppndvlem10  36495  knoppndvlem11  36496  knoppndvlem12  36497  knoppndvlem14  36499  knoppndvlem15  36500  knoppndvlem17  36502  knoppndvlem18  36503  knoppndvlem19  36504  knoppndvlem20  36505  knoppndvlem21  36506  cnndvlem1  36511  taupi  37297  iccioo01  37301  relowlpssretop  37338  sin2h  37590  cos2h  37591  tan2h  37592  poimirlem7  37607  poimirlem9  37609  opnmbllem0  37636  mblfinlem1  37637  mblfinlem2  37638  itg2addnclem  37651  isbnd2  37763  isbnd3  37764  heiborlem7  37797  12gcd5e1  41976  lcm2un  41987  lcmineqlem19  42020  lcmineqlem20  42021  lcmineqlem22  42023  3lexlogpow5ineq2  42028  3lexlogpow5ineq4  42029  3lexlogpow5ineq3  42030  3lexlogpow2ineq1  42031  3lexlogpow2ineq2  42032  3lexlogpow5ineq5  42033  aks4d1lem1  42035  aks4d1p1p3  42042  aks4d1p1p2  42043  aks4d1p1p4  42044  aks4d1p1p6  42046  aks4d1p1p7  42047  aks4d1p1p5  42048  aks4d1p1  42049  aks4d1p2  42050  aks4d1p3  42051  aks4d1p5  42053  aks4d1p6  42054  aks4d1p7d1  42055  aks4d1p7  42056  aks4d1p8  42060  aks4d1p9  42061  posbezout  42073  aks6d1c3  42096  2np3bcnp1  42117  2ap1caineq  42118  aks6d1c6lem4  42146  aks6d1c7lem1  42153  aks6d1c7lem2  42154  oexpreposd  42295  asin1half  42330  remul02  42378  sn-0ne2  42379  remul01  42380  flt4lem7  42632  rabren3dioph  42788  pellexlem2  42803  pellexlem5  42806  pell14qrgapw  42849  pellfundex  42859  rmspecsqrtnq  42879  jm2.24nn  42932  jm2.17a  42933  jm2.17b  42934  jm2.17c  42935  acongrep  42953  acongeq  42956  jm2.22  42968  jm2.23  42969  jm2.20nn  42970  jm3.1lem2  42991  expdiophlem1  42994  sqrtcval  43614  imo72b2lem0  44138  lhe4.4ex1a  44302  isosctrlem1ALT  44907  sineq0ALT  44910  lt3addmuld  45283  suplesup  45319  infleinflem2  45350  infleinf  45351  sumnnodd  45611  0ellimcdiv  45630  sinaover2ne0  45849  stoweidlem13  45994  stoweidlem14  45995  stoweidlem26  46007  stoweidlem49  46030  stoweidlem52  46033  wallispilem4  46049  wallispilem5  46050  wallispi  46051  wallispi2lem1  46052  wallispi2lem2  46053  wallispi2  46054  stirlinglem1  46055  stirlinglem3  46057  stirlinglem5  46059  stirlinglem6  46060  stirlinglem7  46061  stirlinglem10  46064  stirlinglem11  46065  stirlinglem15  46069  stirlingr  46071  dirker2re  46073  dirkerval2  46075  dirkerre  46076  dirkerper  46077  dirkertrigeqlem1  46079  dirkertrigeqlem3  46081  dirkercncflem1  46084  dirkercncflem2  46085  dirkercncflem4  46087  fourierdlem24  46112  fourierdlem43  46131  fourierdlem44  46132  fourierdlem57  46144  fourierdlem58  46145  fourierdlem62  46149  fourierdlem66  46153  fourierdlem68  46155  fourierdlem72  46159  fourierdlem76  46163  fourierdlem78  46165  fourierdlem79  46166  fourierdlem94  46181  fourierdlem103  46190  fourierdlem104  46191  fourierdlem111  46198  fourierdlem113  46200  sqwvfoura  46209  sqwvfourb  46210  fourierswlem  46211  fouriersw  46212  etransclem23  46238  salexct2  46320  salexct3  46323  salgencntex  46324  salgensscntex  46325  sge0ad2en  46412  ovnsubaddlem1  46551  smfmullem4  46775  smf2id  46782  2leaddle2  47282  p1lep2  47284  2ltceilhalf  47312  ceilhalfgt1  47313  2tceilhalfelfzo1  47316  rehalfge1  47319  ceilhalfnn  47320  ceil5half3  47324  difmodm1lt  47343  fmtnoge3  47514  fmtnof1  47519  fmtnoprmfac2lem1  47550  fmtno4prmfac  47556  fmtno4prm  47559  2pwp1prm  47573  31prm  47581  sfprmdvdsmersenne  47587  lighneallem2  47590  lighneallem4a  47592  lighneallem4b  47593  requad01  47605  requad1  47606  requad2  47607  dfodd4  47643  nn0o1gt2ALTV  47678  nnoALTV  47679  nn0oALTV  47680  nn0e  47681  nneven  47682  perfectALTVlem1  47705  perfectALTVlem2  47706  341fppr2  47718  9fppr8  47721  fpprel2  47725  nfermltl2rev  47727  gbowgt5  47746  sbgoldbalt  47765  sgoldbeven3prm  47767  mogoldbb  47769  nnsum3primes4  47772  nnsum3primesgbe  47776  nnsum3primesle9  47778  nnsum4primesodd  47780  nnsum4primesoddALTV  47781  wtgoldbnnsum4prm  47786  bgoldbnnsum3prm  47788  cycl3grtri  47931  usgrexmpl1lem  48005  usgrexmpl2lem  48010  usgrexmpl2nb2  48017  usgrexmpl2nb3  48018  usgrexmpl2nb4  48019  usgrexmpl2nb5  48020  usgrexmpl2trifr  48021  gpgprismgrusgra  48042  gpg5nbgrvtx13starlem2  48056  gpg3nbgrvtx0  48060  gpg3kgrtriexlem1  48067  cznnring  48246  ply1mulgsumlem2  48372  zlmodzxznm  48482  zlmodzxzldeplem  48483  nn0eo  48513  flnn0div2ge  48518  rege1logbzge0  48544  fldivexpfllog2  48550  logbpw2m1  48552  fllog2  48553  blenpw2m1  48564  nnpw2blen  48565  nnolog2flm1  48575  blennngt2o2  48577  dig2nn1st  48590  dig2nn0  48596  dig2bits  48599  dignn0flhalflem1  48600  dignn0flhalflem2  48601  dignn0flhalf  48603  nn0sumshdiglemA  48604  ackval42  48681  rrx2xpref1o  48703  itscnhlc0yqe  48744  itsclquadb  48761  2itscp  48766  itscnhlinecirc02p  48770  sepfsepc  48912