Theorem 2re 12424

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 12412	. 2 ⊢ 2 = (1 + 1)
2		1re 11315	. . 3 ⊢ 1 ∈ ℝ
3	2, 2	readdcli 11331	. 2 ⊢ (1 + 1) ∈ ℝ
4	1, 3	eqeltri 2856	1 ⊢ 2 ∈ ℝ

This proof depends on syntax axioms:   ∈ wcel 2144  (class class class)co 7424  ℝcr 11206  1c1 11208   + caddc 11210  2c2 12404

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732  ax-1cn 11265  ax-icn 11266  ax-addcl 11267  ax-addrcl 11268  ax-mulcl 11269  ax-mulrcl 11270  ax-i2m1 11275  ax-1ne0 11276  ax-rrecex 11279  ax-cnre 11280

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-ne 2956  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-ss 3897  df-dif 4046  df-un 4150  df-nul 4278  df-if 4482  df-sn 4585  df-pr 4587  df-op 4835  df-uni 4867  df-br 5103  df-iota 6497  df-fv 6551  df-ov 7427  df-2 12412

This theorem is used by:  2cnALT  12426  3re  12430  0le2  12452  2lt3  12523  2le3  12524  1lt3  12525  2lt4  12527  1lt4  12528  2lt5  12531  2lt6  12536  1lt6  12537  2lt7  12542  1lt7  12543  2lt8  12549  1lt8  12550  2lt9  12557  1lt9  12558  1le2  12561  2rene0  12563  halfre  12566  halfgt0  12568  halflt1  12570  rehalfcl  12580  halfpos2  12582  halfnneg2  12584  addltmul  12589  nominpos  12590  avglt1  12591  avglt2  12592  div4p1lem1div2  12608  nn0lele2xi  12669  nn0n0n1ge2b  12682  nn0ge2m1nn  12683  nn0le2is012  12770  halfnz  12784  3halfnz  12785  2lt10  12965  1lt10OLD  12967  uzuzle23  13018  uzuzle24  13019  uz3m2nn  13028  2rp  13132  ge2halflem1  13244  xnn0n0n1ge2b  13268  fztpval  13727  fz0to4untppr  13771  fz0to5un2tp  13772  fzo0to42pr  13895  flhalf  13977  fldiv4p1lem1div2  13982  2txmodxeq0  14081  expubnd  14328  expmulnbnd  14386  nn0opthlem2  14420  faclbnd2  14442  faclbnd4lem1  14444  faclbnd5  14449  4bc2eq6  14480  hashgt23el  14576  hashfun  14589  hashge2el2dif  14632  hashge2el2difr  14633  hash3tpde  14645  wrdlenge2n0  14704  f1oun2prg  15077  01sqrexlem7  15424  sqrt4  15448  sqrt2gt1lt2  15450  abstri  15507  sqreulem  15536  amgm2  15546  caucvgrlem  15849  climcndslem1  16027  climcndslem2  16028  climcnds  16029  efcllem  16252  ege2le3  16265  ef01bndlem  16361  cos01bnd  16363  cos2bnd  16365  cos01gt0  16368  sin02gt0  16369  sincos2sgn  16371  sin4lt0  16372  eirrlem  16381  egt2lt3  16383  epos  16384  ene1  16387  sqrt2re  16427  mod2eq1n2dvds  16526  oddge22np1  16528  evennn2n  16530  nn0o1gt2  16560  nno  16561  nn0o  16562  nnoddm1d2  16565  bitsp1o  16612  bitsfzolem  16613  bitsfzo  16614  bitsfi  16616  6gcd4e2  16720  2mulprm  16877  ge2nprmge4  16886  isprm7  16893  3lcm2e6  16917  prmreclem2  17104  prmreclem6  17108  4sqlem11  17142  4sqlem12  17143  prmgaplem7  17244  2expltfac  17279  plusgndxnmulrndx  17477  starvndxnplusgndx  17485  scandxnplusgndx  17497  vscandxnplusgndx  17502  ipndxnplusgndx  17513  tsetndxnplusgndx  17537  plendxnplusgndx  17551  dsndxnplusgndx  17570  slotsdifunifndx  17581  efgredleme  19966  zringndrg  21783  chfacfscmul0  23185  chfacfpmmul0  23189  psmetge0  24640  xmetge0  24672  bl2in  24728  metnrmlem3  25190  iihalf1  25261  iihalf2  25263  pcoass  25354  tcphcphlem1  25565  csbren  25729  trirn  25730  minveclem2  25756  minveclem4  25762  pjthlem1  25767  ovolunlem1a  25826  dyadss  25924  opnmbllem  25931  vitalilem2  25939  vitalilem4  25941  mbfi1fseqlem5  26049  lhop1lem  26342  aaliou3lem2  26679  aaliou3lem8  26681  pilem2  26788  pilem3  26789  2pire  26793  pipos  26796  sinhalfpilem  26801  sincosq1lem  26835  sincosq4sgn  26839  tangtx  26843  sinq12gt0  26845  sincos4thpi  26851  tan4thpi  26852  sincos6thpi  26853  sineq0  26861  cos02pilt1  26863  cosq34lt1  26864  cosordlem  26867  cos0pilt1  26869  tanord1  26874  efif1olem1  26879  efif1olem2  26880  efif1olem4  26882  efif1o  26883  efifo  26884  2irrexpq  27068  cxpcn3lem  27084  root1id  27091  root1eq1  27092  root1cj  27093  cxpeq  27094  2logb9irr  27132  2logb3irr  27134  ang180lem1  27146  ang180lem2  27147  chordthmlem2  27170  1cubrlem  27178  atancj  27247  atantan  27260  atanbndlem  27262  atans2  27268  leibpi  27279  log2tlbnd  27282  log2ublem2  27284  log2ub  27286  divsqrtsumlem  27316  harmonicbnd3  27344  zetacvg  27351  lgamgulmlem2  27366  lgamgulmlem3  27367  lgamgulmlem4  27368  lgamgulmlem6  27370  lgamucov  27374  basellem1  27417  basellem2  27418  basellem3  27419  basellem5  27421  chtdif  27494  ppidif  27499  ppinncl  27510  chtrpcl  27511  ppieq0  27512  ppiltx  27513  ppiublem1  27538  ppiub  27540  chpeq0  27544  chteq0  27545  chtublem  27547  chtub  27548  chpval2  27554  chpub  27556  mersenne  27563  perfectlem1  27565  perfectlem2  27566  dchrptlem1  27600  dchrptlem2  27601  bcmono  27613  bclbnd  27616  bpos1lem  27618  bposlem1  27620  bposlem2  27621  bposlem3  27622  bposlem4  27623  bposlem5  27624  bposlem6  27625  bposlem7  27626  bposlem8  27627  bposlem9  27628  lgslem1  27633  lgsdirprm  27667  gausslemma2dlem0c  27694  gausslemma2dlem1a  27701  gausslemma2dlem2  27703  gausslemma2dlem3  27704  lgseisenlem1  27711  lgseisenlem2  27712  lgseisenlem3  27713  lgseisen  27715  lgsquadlem1  27716  lgsquadlem2  27717  m1lgs  27724  2lgslem1a1  27725  2lgslem1a2  27726  2lgslem1c  27729  2lgslem4  27742  2sqlem11  27765  2sq2  27769  2sqreultlem  27783  2sqreunnltlem  27786  chebbnd1lem1  27805  chebbnd1lem2  27806  chebbnd1lem3  27807  chebbnd1  27808  chtppilimlem1  27809  chtppilimlem2  27810  chtppilim  27811  chto1ub  27812  chebbnd2  27813  chto1lb  27814  chpchtlim  27815  chpo1ub  27816  chpo1ubb  27817  rplogsumlem1  27820  rplogsumlem2  27821  dchrisumlem2  27826  dchrisumlem3  27827  dchrvmasumiflem1  27837  dchrisum0fno1  27847  dchrisum0re  27849  dchrisum0lem1b  27851  dchrisum0lem1  27852  dchrisum0lem2  27854  rplogsum  27863  mulog2sumlem1  27870  mulog2sumlem2  27871  log2sumbnd  27880  selberglem2  27882  selbergb  27885  selberg2b  27888  chpdifbndlem1  27889  logdivbnd  27892  selberg3lem1  27893  selberg3  27895  selberg4lem1  27896  selberg4  27897  pntrmax  27900  pntrsumbnd2  27903  selberg3r  27905  selberg4r  27906  selberg34r  27907  pntrlog2bndlem2  27914  pntrlog2bndlem3  27915  pntrlog2bndlem4  27916  pntrlog2bndlem5  27917  pntrlog2bndlem6  27919  pntrlog2bnd  27920  pntpbnd1a  27921  pntpbnd1  27922  pntpbnd2  27923  pntpbnd  27924  pntibndlem2  27927  pntibndlem3  27928  pntibnd  27929  pntlemb  27933  pntlemg  27934  pntlemh  27935  pntlemr  27938  pntlemk  27942  pntlemo  27943  pnt2  27949  pnt  27950  ostth2lem1  27954  ostth3  27974  fltoprmlem2  28003  slotsinbpsd  28912  slotslnbpsd  28913  tgldimor  28974  trgcgrg  28987  tgcgr4  29003  axlowdimlem6  29534  axlowdimlem16  29544  axlowdimlem17  29545  axlowdim  29548  upgrfi  29678  umgrupgr  29690  umgrislfupgrlem  29709  umgrislfupgr  29710  lfgrnloop  29712  lfuhgr2  29736  usgruspgr  29770  usgrislfuspgr  29777  lfuhgr1v0e  29844  usgrexmpldifpr  29848  usgrexmplef  29849  nbusgrvtxm1  29969  vdegp1bi  30127  upgrewlkle2  30196  lfgrwlkprop  30279  upgr2pthnlp  30327  usgr2pthlem  30358  pthdlem1  30361  wwlksm1edg  30479  wwlksnextwrd  30495  wwlksnextfun  30496  wwlksnextinj  30497  wwlksnextproplem3  30509  clwlkclwwlklem2a1  30592  clwlkclwwlklem2a2  30593  clwlkclwwlklem2fv1  30595  clwlkclwwlklem2fv2  30596  clwlkclwwlklem2a4  30597  clwlkclwwlklem2a  30598  clwlkclwwlklem2  30600  clwlkclwwlk2  30603  clwlkclwwlkf  30608  clwwlkext2edg  30656  konigsbergiedgw  30858  konigsbergssiedgw  30860  konigsberglem3  30864  konigsberg  30867  frgrreggt1  31003  ex-pss  31038  ex-res  31051  ex-fv  31053  ex-fl  31057  ex-mod  31059  ex-abs  31065  nrt2irr  31083  ipidsq  31321  minvecolem2  31486  minvecolem4  31491  normlem7  31727  norm-ii-i  31748  norm3lemt  31763  normpar2i  31767  bcsiALT  31790  pjhthlem1  32002  opsqrlem6  32756  cdj3lem1  33045  addltmulALT  33099  nexple  33474  2exple2exp  33475  threehalves  33531  pfx1s2  33556  wrdt2ind  33566  cyc3conja  33768  drngidlhash  34033  evl1deg3  34160  rtelextdg2lem  34408  fldext2chn  34410  constraddcl  34444  iconstr  34448  2sqr3minply  34462  2sqr3nconstr  34463  cos9thpinconstrlem1  34471  cos9thpinconstrlem2  34472  sqsscirc1  34590  dya2iocucvr  34966  omssubadd  34982  oddpwdc  35036  eulerpartlemgc  35044  fibp1  35083  coinfliplem  35161  coinflipspace  35163  ballotlem2  35171  signstfveq0  35256  prodfzo03  35282  hgt750lemd  35327  logdivsqrle  35329  hgt750lem  35330  hgt750lem2  35331  hgt750leme  35337  usgrcyclgt2v  35990  acycgr2v  35995  subfacp1lem1  36034  subfacp1lem5  36039  subfacval3  36044  problem2  36521  problem5  36524  circum  36529  nn0prpwlem  37206  dnibndlem10  37449  knoppcnlem2  37456  knoppcnlem4  37458  knoppcnlem10  37464  unbdqndv2lem1  37471  knoppndvlem1  37474  knoppndvlem10  37483  knoppndvlem11  37484  knoppndvlem12  37485  knoppndvlem14  37487  knoppndvlem15  37488  knoppndvlem17  37490  knoppndvlem18  37491  knoppndvlem19  37492  knoppndvlem20  37493  knoppndvlem21  37494  cnndvlem1  37499  taupi  38353  iccioo01  38359  relowlpssretop  38396  sin2h  38642  cos2h  38643  tan2h  38644  poimirlem7  38654  poimirlem9  38656  opnmbllem0  38683  mblfinlem1  38684  mblfinlem2  38685  itg2addnclem  38698  isbnd2  38826  isbnd3  38827  heiborlem7  38860  12gcd5e1  43162  lcm2un  43173  lcmineqlem19  43206  lcmineqlem20  43207  lcmineqlem22  43209  3lexlogpow5ineq2  43214  3lexlogpow5ineq4  43215  3lexlogpow5ineq3  43216  3lexlogpow2ineq1  43217  3lexlogpow2ineq2  43218  3lexlogpow5ineq5  43219  aks4d1lem1  43221  aks4d1p1p3  43228  aks4d1p1p2  43229  aks4d1p1p4  43230  aks4d1p1p6  43232  aks4d1p1p7  43233  aks4d1p1p5  43234  aks4d1p1  43235  aks4d1p2  43236  aks4d1p3  43237  aks4d1p5  43239  aks4d1p6  43240  aks4d1p7d1  43241  aks4d1p7  43242  aks4d1p8  43246  aks4d1p9  43247  posbezout  43259  aks6d1c3  43282  2np3bcnp1  43303  2ap1caineq  43304  aks6d1c6lem4  43332  aks6d1c7lem1  43339  aks6d1c7lem2  43340  oexpreposd  43488  asin1half  43517  remul02  43565  sn-0ne2  43566  remul01  43567  rabren3dioph  43931  pellexlem2  43946  pellexlem5  43949  pell14qrgapw  43992  pellfundex  44002  rmspecsqrtnq  44022  jm2.24nn  44075  jm2.17a  44076  jm2.17b  44077  jm2.17c  44078  acongrep  44096  acongeq  44099  jm2.22  44111  jm2.23  44112  jm3.1lem2  44134  expdiophlem1  44137  sqrtcval  44750  imo72b2lem0  45274  lhe4.4ex1a  45422  isosctrlem1ALT  46024  sineq0ALT  46027  lt3addmuld  46425  suplesup  46459  infleinflem2  46490  infleinf  46491  sumnnodd  46750  0ellimcdiv  46767  sinaover2ne0  46986  stoweidlem13  47131  stoweidlem14  47132  stoweidlem26  47144  stoweidlem49  47167  stoweidlem52  47170  wallispilem4  47186  wallispilem5  47187  wallispi  47188  wallispi2lem1  47189  wallispi2lem2  47190  wallispi2  47191  stirlinglem1  47192  stirlinglem3  47194  stirlinglem5  47196  stirlinglem6  47197  stirlinglem7  47198  stirlinglem10  47201  stirlinglem11  47202  stirlinglem15  47206  stirlingr  47208  dirker2re  47210  dirkerval2  47212  dirkerre  47213  dirkertrigeqlem1  47216  dirkertrigeqlem3  47218  dirkercncflem1  47221  dirkercncflem4  47224  fourierdlem24  47249  fourierdlem43  47268  fourierdlem44  47269  fourierdlem57  47281  fourierdlem58  47282  fourierdlem62  47286  fourierdlem66  47290  fourierdlem68  47292  fourierdlem72  47296  fourierdlem76  47300  fourierdlem78  47302  fourierdlem79  47303  fourierdlem94  47318  fourierdlem103  47327  fourierdlem104  47328  fourierdlem111  47335  sqwvfoura  47346  sqwvfourb  47347  fourierswlem  47348  fouriersw  47349  etransclem23  47375  salexct2  47457  salexct3  47460  salgencntex  47461  salgensscntex  47462  sge0ad2en  47549  ovnsubaddlem1  47688  smfmullem4  47912  smf2id  47919  goldrarr  48036  goldrapos  48038  goldratmolem4  48043  goldratval  48044  2leaddle2  48476  p1lep2  48478  2ltceilhalf  48510  ceilhalfgt1  48511  2tceilhalfelfzo1  48514  rehalfge1  48517  ceilhalfnn  48518  ceil5half3  48524  difmodm1lt  48543  2timesltsq  48556  2timesltsqm1  48557  fmtnoge3  48723  fmtnof1  48728  fmtnoprmfac2lem1  48759  fmtno4prmfac  48765  fmtno4prm  48768  2pwp1prm  48782  31prm  48790  sfprmdvdsmersenne  48796  lighneallem2  48799  lighneallem4a  48801  lighneallem4b  48802  nprmdvdsfacm1lem2  48814  nprmdvdsfacm1lem4  48816  ppivalnnnprmge6  48819  requad01  48827  requad1  48828  requad2  48829  dfodd4  48865  nn0o1gt2ALTV  48900  nnoALTV  48901  nn0oALTV  48902  nn0e  48903  nneven  48904  perfectALTVlem1  48927  perfectALTVlem2  48928  341fppr2  48940  9fppr8  48943  fpprel2  48947  nfermltl2rev  48949  gbowgt5  48968  sbgoldbalt  48987  sgoldbeven3prm  48989  mogoldbb  48991  nnsum3primes4  48994  nnsum3primesgbe  48998  nnsum3primesle9  49000  nnsum4primesodd  49002  nnsum4primesoddALTV  49003  wtgoldbnnsum4prm  49008  bgoldbnnsum3prm  49010  cycl3grtri  49153  usgrexmpl1lem  49227  usgrexmpl2lem  49232  usgrexmpl2nb2  49239  usgrexmpl2nb3  49240  usgrexmpl2nb4  49241  usgrexmpl2nb5  49242  usgrexmpl2trifr  49243  gpgprismgrusgra  49264  gpg5nbgrvtx13starlem2  49278  gpg3nbgrvtx0  49282  gpg3kgrtriexlem1  49289  cznnring  49467  ply1mulgsumlem2  49607  zlmodzxznm  49717  zlmodzxzldeplem  49718  nn0eo  49748  flnn0div2ge  49753  rege1logbzge0  49779  fldivexpfllog2  49785  logbpw2m1  49787  fllog2  49788  blenpw2m1  49799  nnpw2blen  49800  nnolog2flm1  49810  blennngt2o2  49812  dig2nn1st  49825  dig2nn0  49831  dig2bits  49834  dignn0flhalflem1  49835  dignn0flhalflem2  49836  dignn0flhalf  49838  nn0sumshdiglemA  49839  ackval42  49916  itscnhlc0yqe  49979  itsclquadb  49996  2itscp  50001  itscnhlinecirc02p  50005  sepfsepc  50150  2ne3  51125  veronesev2lem  51157  veronesev4lem  51159  veronesev5lem  51160  veronesev6lem  51161  veronesevrowd  51162  veroquadgsumlem  51166