Theorem 2re 11699

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 11688	. 2 ⊢ 2 = (1 + 1)
2		1re 10630	. . 3 ⊢ 1 ∈ ℝ
3	2, 2	readdcli 10645	. 2 ⊢ (1 + 1) ∈ ℝ
4	1, 3	eqeltri 2886	1 ⊢ 2 ∈ ℝ

Syntax hints:   ∈ wcel 2111  (class class class)co 7135  ℝcr 10525  1c1 10527   + caddc 10529  2c2 11680

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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770  ax-1cn 10584  ax-icn 10585  ax-addcl 10586  ax-addrcl 10587  ax-mulcl 10588  ax-mulrcl 10589  ax-i2m1 10594  ax-1ne0 10595  ax-rrecex 10598  ax-cnre 10599

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-ne 2988  df-ral 3111  df-rex 3112  df-v 3443  df-un 3886  df-in 3888  df-ss 3898  df-sn 4526  df-pr 4528  df-op 4532  df-uni 4801  df-br 5031  df-iota 6283  df-fv 6332  df-ov 7138  df-2 11688

This theorem is referenced by:  2cnALT  11701  3re  11705  2ne0  11729  3pos  11730  2lt3  11797  1lt3  11798  2lt4  11800  1lt4  11801  2lt5  11804  2lt6  11809  1lt6  11810  2lt7  11815  1lt7  11816  2lt8  11822  1lt8  11823  2lt9  11830  1lt9  11831  1le2  11834  2rene0  11836  halfre  11839  halfgt0  11841  halflt1  11843  rehalfcl  11851  halfpos2  11854  halfnneg2  11856  addltmul  11861  nominpos  11862  avglt1  11863  avglt2  11864  div4p1lem1div2  11880  nn0lele2xi  11940  nn0n0n1ge2b  11951  nn0ge2m1nn  11952  nn0le2is012  12034  halfnz  12048  3halfnz  12049  2lt10  12224  1lt10  12225  eluz4eluz2  12273  uzuzle23  12277  uz3m2nn  12279  2rp  12382  xnn0n0n1ge2b  12514  fztpval  12964  fz0to4untppr  13005  fzo0to42pr  13119  flhalf  13195  fldiv4p1lem1div2  13200  2txmodxeq0  13294  expubnd  13537  expmulnbnd  13592  nn0opthlem2  13625  faclbnd2  13647  faclbnd4lem1  13649  faclbnd5  13654  4bc2eq6  13685  hashgt23el  13781  hashfun  13794  hashge2el2dif  13834  hashge2el2difr  13835  wrdlenge2n0  13895  f1oun2prg  14270  sqrlem7  14600  sqrt4  14624  sqrt2gt1lt2  14626  abstri  14682  sqreulem  14711  amgm2  14721  caucvgrlem  15021  climcndslem1  15196  climcndslem2  15197  climcnds  15198  efcllem  15423  ege2le3  15435  ef01bndlem  15529  cos01bnd  15531  cos2bnd  15533  cos01gt0  15536  sin02gt0  15537  sincos2sgn  15539  sin4lt0  15540  eirrlem  15549  egt2lt3  15551  epos  15552  ene1  15555  sqrt2re  15595  mod2eq1n2dvds  15688  oddge22np1  15690  evennn2n  15692  nn0o1gt2  15722  nno  15723  nn0o  15724  nnoddm1d2  15727  bitsp1o  15772  bitsfzolem  15773  bitsfzo  15774  bitsfi  15776  6gcd4e2  15876  2mulprm  16027  ge2nprmge4  16035  isprm7  16042  3lcm2e6  16062  prmreclem2  16243  prmreclem6  16247  4sqlem11  16281  4sqlem12  16282  prmgaplem7  16383  2expltfac  16418  plusgndxnmulrndx  16609  oppgtset  18472  efgredleme  18861  mgpsca  19239  mgptset  19240  mgpds  19242  rmodislmod  19695  cnfldfun  20103  zringndrg  20183  chfacfscmul0  21463  chfacfpmmul0  21467  psmetge0  22919  xmetge0  22951  bl2in  23007  metnrmlem3  23466  iihalf1  23536  iihalf2  23538  pcoass  23629  tcphcphlem1  23839  csbren  24003  trirn  24004  minveclem2  24030  minveclem4  24036  pjthlem1  24041  ovolunlem1a  24100  dyadss  24198  opnmbllem  24205  vitalilem2  24213  vitalilem4  24215  mbfi1fseqlem5  24323  lhop1lem  24616  aaliou3lem2  24939  aaliou3lem8  24941  pilem2  25047  pilem3  25048  pipos  25053  sinhalfpilem  25056  sincosq1lem  25090  sincosq4sgn  25094  tangtx  25098  sinq12gt0  25100  sincos4thpi  25106  tan4thpi  25107  sincos6thpi  25108  sineq0  25116  cos02pilt1  25118  cosq34lt1  25119  cosordlem  25122  cos0pilt1  25124  tanord1  25129  efif1olem1  25134  efif1olem2  25135  efif1olem4  25137  efif1o  25138  efifo  25139  2irrexpq  25321  cxpcn3lem  25336  root1id  25343  root1eq1  25344  root1cj  25345  cxpeq  25346  2logb9irr  25381  2logb3irr  25383  ang180lem1  25395  ang180lem2  25396  chordthmlem2  25419  1cubrlem  25427  atancj  25496  atantan  25509  atanbndlem  25511  atans2  25517  leibpi  25528  log2tlbnd  25531  log2ublem2  25533  log2ub  25535  divsqrtsumlem  25565  harmonicbnd3  25593  zetacvg  25600  lgamgulmlem2  25615  lgamgulmlem3  25616  lgamgulmlem4  25617  lgamgulmlem6  25619  lgamucov  25623  basellem1  25666  basellem2  25667  basellem3  25668  basellem5  25670  chtdif  25743  ppidif  25748  ppinncl  25759  chtrpcl  25760  ppieq0  25761  ppiltx  25762  ppiublem1  25786  ppiub  25788  chpeq0  25792  chteq0  25793  chtublem  25795  chtub  25796  chpval2  25802  chpub  25804  mersenne  25811  perfectlem1  25813  perfectlem2  25814  dchrptlem1  25848  dchrptlem2  25849  bcmono  25861  bclbnd  25864  bpos1lem  25866  bposlem1  25868  bposlem2  25869  bposlem3  25870  bposlem4  25871  bposlem5  25872  bposlem6  25873  bposlem7  25874  bposlem8  25875  bposlem9  25876  lgslem1  25881  lgsdirprm  25915  gausslemma2dlem0c  25942  gausslemma2dlem1a  25949  gausslemma2dlem2  25951  gausslemma2dlem3  25952  lgseisenlem1  25959  lgseisenlem2  25960  lgseisenlem3  25961  lgseisen  25963  lgsquadlem1  25964  lgsquadlem2  25965  m1lgs  25972  2lgslem1a1  25973  2lgslem1a2  25974  2lgslem1c  25977  2lgslem4  25990  2sqlem11  26013  2sq2  26017  2sqreultlem  26031  2sqreunnltlem  26034  chebbnd1lem1  26053  chebbnd1lem2  26054  chebbnd1lem3  26055  chebbnd1  26056  chtppilimlem1  26057  chtppilimlem2  26058  chtppilim  26059  chto1ub  26060  chebbnd2  26061  chto1lb  26062  chpchtlim  26063  chpo1ub  26064  chpo1ubb  26065  rplogsumlem1  26068  rplogsumlem2  26069  dchrisumlem2  26074  dchrisumlem3  26075  dchrvmasumiflem1  26085  dchrisum0fno1  26095  dchrisum0re  26097  dchrisum0lem1b  26099  dchrisum0lem1  26100  dchrisum0lem2  26102  rplogsum  26111  mulog2sumlem1  26118  mulog2sumlem2  26119  log2sumbnd  26128  selberglem2  26130  selbergb  26133  selberg2b  26136  chpdifbndlem1  26137  logdivbnd  26140  selberg3lem1  26141  selberg3  26143  selberg4lem1  26144  selberg4  26145  pntrmax  26148  pntrsumbnd2  26151  selberg3r  26153  selberg4r  26154  selberg34r  26155  pntrlog2bndlem2  26162  pntrlog2bndlem3  26163  pntrlog2bndlem4  26164  pntrlog2bndlem5  26165  pntrlog2bndlem6  26167  pntrlog2bnd  26168  pntpbnd1a  26169  pntpbnd1  26170  pntpbnd2  26171  pntpbnd  26172  pntibndlem2  26175  pntibndlem3  26176  pntibnd  26177  pntlemb  26181  pntlemg  26182  pntlemh  26183  pntlemr  26186  pntlemk  26190  pntlemo  26191  pnt2  26197  pnt  26198  ostth2lem1  26202  ostth3  26222  istrkg3ld  26255  tgldimor  26296  trgcgrg  26309  tgcgr4  26325  axlowdimlem6  26741  axlowdimlem16  26751  axlowdimlem17  26752  axlowdim  26755  upgrfi  26884  umgrupgr  26896  umgrislfupgrlem  26915  umgrislfupgr  26916  lfgrnloop  26918  usgruspgr  26971  usgrislfuspgr  26977  lfuhgr1v0e  27044  usgrexmpldifpr  27048  usgrexmplef  27049  nbusgrvtxm1  27169  vdegp1bi  27327  upgrewlkle2  27396  lfgrwlkprop  27477  upgr2pthnlp  27521  usgr2pthlem  27552  pthdlem1  27555  wwlksm1edg  27667  wwlksnextwrd  27683  wwlksnextfun  27684  wwlksnextinj  27685  wwlksnextproplem3  27697  clwlkclwwlklem2a1  27777  clwlkclwwlklem2a2  27778  clwlkclwwlklem2fv1  27780  clwlkclwwlklem2fv2  27781  clwlkclwwlklem2a4  27782  clwlkclwwlklem2a  27783  clwlkclwwlklem2  27785  clwlkclwwlk2  27788  clwlkclwwlkf  27793  clwwlkext2edg  27841  konigsbergiedgw  28033  konigsbergssiedgw  28035  konigsberglem1  28037  konigsberglem2  28038  konigsberglem3  28039  konigsberg  28042  frgrreggt1  28178  ex-pss  28213  ex-res  28226  ex-fv  28228  ex-fl  28232  ex-mod  28234  ex-abs  28240  ipidsq  28493  minvecolem2  28658  minvecolem4  28663  normlem7  28899  norm-ii-i  28920  norm3lemt  28935  normpar2i  28939  bcsiALT  28962  pjhthlem1  29174  opsqrlem6  29928  cdj3lem1  30217  addltmulALT  30229  threehalves  30617  pfx1s2  30641  wrdt2ind  30653  oppgle  30666  cyc3conja  30849  resvplusg  30957  sqsscirc1  31261  nexple  31378  dya2iocucvr  31652  omssubadd  31668  oddpwdc  31722  eulerpartlemgc  31730  fibp1  31769  coinfliplem  31846  coinflipspace  31848  ballotlem2  31856  signstfveq0  31957  prodfzo03  31984  hgt750lemd  32029  logdivsqrle  32031  hgt750lem  32032  hgt750lem2  32033  hgt750leme  32039  lfuhgr2  32478  usgrcyclgt2v  32491  acycgr2v  32510  subfacp1lem1  32539  subfacp1lem5  32544  subfacval3  32549  problem2  33022  problem5  33025  circum  33030  nn0prpwlem  33783  dnibndlem10  33939  knoppcnlem2  33946  knoppcnlem4  33948  knoppcnlem10  33954  unbdqndv2lem1  33961  knoppndvlem1  33964  knoppndvlem10  33973  knoppndvlem11  33974  knoppndvlem12  33975  knoppndvlem14  33977  knoppndvlem15  33978  knoppndvlem17  33980  knoppndvlem18  33981  knoppndvlem19  33982  knoppndvlem20  33983  knoppndvlem21  33984  cnndvlem1  33989  taupi  34737  iccioo01  34741  relowlpssretop  34781  sin2h  35047  cos2h  35048  tan2h  35049  poimirlem7  35064  poimirlem9  35066  opnmbllem0  35093  mblfinlem1  35094  mblfinlem2  35095  itg2addnclem  35108  isbnd2  35221  isbnd3  35222  heiborlem7  35255  12gcd5e1  39291  lcm2un  39302  lcmineqlem19  39335  lcmineqlem20  39336  lcmineqlem22  39338  3lexlogpow5ineq1  39341  3lexlogpow5ineq2  39342  3lexlogpow5ineq3  39343  2np3bcnp1  39348  2ap1caineq  39349  2xp3dxp2ge1d  39387  oexpreposd  39487  remul02  39543  sn-0ne2  39544  remul01  39545  rabren3dioph  39756  pellexlem2  39771  pellexlem5  39774  pell14qrgapw  39817  pellfundex  39827  rmspecsqrtnq  39847  jm2.24nn  39900  jm2.17a  39901  jm2.17b  39902  jm2.17c  39903  acongrep  39921  acongeq  39924  jm2.22  39936  jm2.23  39937  jm2.20nn  39938  jm3.1lem2  39959  expdiophlem1  39962  sqrtcval  40341  imo72b2lem0  40869  mnringaddgd  40928  lhe4.4ex1a  41033  isosctrlem1ALT  41640  sineq0ALT  41643  lt3addmuld  41933  suplesup  41971  infleinflem2  42003  infleinf  42004  sumnnodd  42272  0ellimcdiv  42291  sinaover2ne0  42510  stoweidlem13  42655  stoweidlem14  42656  stoweidlem26  42668  stoweidlem49  42691  stoweidlem52  42694  wallispilem4  42710  wallispilem5  42711  wallispi  42712  wallispi2lem1  42713  wallispi2lem2  42714  wallispi2  42715  stirlinglem1  42716  stirlinglem3  42718  stirlinglem5  42720  stirlinglem6  42721  stirlinglem7  42722  stirlinglem10  42725  stirlinglem11  42726  stirlinglem15  42730  stirlingr  42732  dirker2re  42734  dirkerval2  42736  dirkerre  42737  dirkerper  42738  dirkertrigeqlem1  42740  dirkertrigeqlem3  42742  dirkercncflem1  42745  dirkercncflem2  42746  dirkercncflem4  42748  fourierdlem24  42773  fourierdlem43  42792  fourierdlem44  42793  fourierdlem57  42805  fourierdlem58  42806  fourierdlem62  42810  fourierdlem66  42814  fourierdlem68  42816  fourierdlem72  42820  fourierdlem76  42824  fourierdlem78  42826  fourierdlem79  42827  fourierdlem94  42842  fourierdlem103  42851  fourierdlem104  42852  fourierdlem111  42859  fourierdlem113  42861  sqwvfoura  42870  sqwvfourb  42871  fourierswlem  42872  fouriersw  42873  etransclem23  42899  salexct2  42979  salexct3  42982  salgencntex  42983  salgensscntex  42984  sge0ad2en  43070  ovnsubaddlem1  43209  smfmullem4  43426  smf2id  43433  2leaddle2  43855  p1lep2  43857  fmtnoge3  44047  fmtnof1  44052  fmtnoprmfac2lem1  44083  fmtno4prmfac  44089  fmtno4prm  44092  2pwp1prm  44106  31prm  44114  sfprmdvdsmersenne  44121  lighneallem2  44124  lighneallem4a  44126  lighneallem4b  44127  requad01  44139  requad1  44140  requad2  44141  dfodd4  44177  nn0o1gt2ALTV  44212  nnoALTV  44213  nn0oALTV  44214  nn0e  44215  nneven  44216  perfectALTVlem1  44239  perfectALTVlem2  44240  341fppr2  44252  9fppr8  44255  fpprel2  44259  nfermltl2rev  44261  gbowgt5  44280  sbgoldbalt  44299  sgoldbeven3prm  44301  mogoldbb  44303  nnsum3primes4  44306  nnsum3primesgbe  44310  nnsum3primesle9  44312  nnsum4primesodd  44314  nnsum4primesoddALTV  44315  wtgoldbnnsum4prm  44320  bgoldbnnsum3prm  44322  cznnring  44580  ply1mulgsumlem2  44795  zlmodzxznm  44906  zlmodzxzldeplem  44907  difmodm1lt  44936  nn0eo  44942  flnn0div2ge  44947  rege1logbzge0  44973  fldivexpfllog2  44979  logbpw2m1  44981  fllog2  44982  blenpw2m1  44993  nnpw2blen  44994  nnolog2flm1  45004  blennngt2o2  45006  dig2nn1st  45019  dig2nn0  45025  dig2bits  45028  dignn0flhalflem1  45029  dignn0flhalflem2  45030  dignn0flhalf  45032  nn0sumshdiglemA  45033  ackval42  45110  rrx2xpref1o  45132  itscnhlc0yqe  45173  itsclquadb  45190  2itscp  45195  itscnhlinecirc02p  45199