Theorem 2re 11453

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 11442	. 2 ⊢ 2 = (1 + 1)
2		1re 10378	. . 3 ⊢ 1 ∈ ℝ
3	2, 2	readdcli 10394	. 2 ⊢ (1 + 1) ∈ ℝ
4	1, 3	eqeltri 2855	1 ⊢ 2 ∈ ℝ

Syntax hints:   ∈ wcel 2107  (class class class)co 6924  ℝcr 10273  1c1 10275   + caddc 10277  2c2 11434

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2055  ax-9 2116  ax-10 2135  ax-11 2150  ax-12 2163  ax-13 2334  ax-ext 2754  ax-1cn 10332  ax-icn 10333  ax-addcl 10334  ax-addrcl 10335  ax-mulcl 10336  ax-mulrcl 10337  ax-i2m1 10342  ax-1ne0 10343  ax-rrecex 10346  ax-cnre 10347

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-3an 1073  df-tru 1605  df-ex 1824  df-nf 1828  df-sb 2012  df-clab 2764  df-cleq 2770  df-clel 2774  df-nfc 2921  df-ne 2970  df-ral 3095  df-rex 3096  df-rab 3099  df-v 3400  df-dif 3795  df-un 3797  df-in 3799  df-ss 3806  df-nul 4142  df-if 4308  df-sn 4399  df-pr 4401  df-op 4405  df-uni 4674  df-br 4889  df-iota 6101  df-fv 6145  df-ov 6927  df-2 11442

This theorem is referenced by:  2cnALT  11455  3re  11459  2ne0  11490  3pos  11491  2lt3  11558  1lt3  11559  2lt4  11561  1lt4  11562  2lt5  11565  2lt6  11570  1lt6  11571  2lt7  11576  1lt7  11577  2lt8  11583  1lt8  11584  2lt9  11591  1lt9  11592  1le2  11595  2rene0  11597  halfre  11600  halfgt0  11602  halflt1  11604  rehalfcl  11612  halfpos2  11615  halfnneg2  11617  addltmul  11622  nominpos  11623  avglt1  11624  avglt2  11625  div4p1lem1div2  11641  nn0lele2xi  11703  nn0n0n1ge2b  11714  nn0ge2m1nn  11715  nn0le2is012  11797  halfnz  11811  3halfnz  11812  2lt10  11989  1lt10  11990  uzuzle23  12039  uz3m2nn  12041  2rp  12146  xnn0n0n1ge2b  12280  fztpval  12724  fz0to4untppr  12765  fzo0to42pr  12878  flhalf  12954  fldiv4p1lem1div2  12959  2txmodxeq0  13053  expubnd  13243  expmulnbnd  13319  nn0opthlem2  13378  faclbnd2  13400  faclbnd4lem1  13402  faclbnd5  13407  4bc2eq6  13438  hashfun  13542  hashge2el2dif  13580  hashge2el2difr  13581  wrdlenge2n0  13646  f1oun2prg  14072  pfx2  14102  sqrlem7  14400  sqrt4  14424  sqrt2gt1lt2  14426  abstri  14481  sqreulem  14510  amgm2  14520  caucvgrlem  14815  climcndslem1  14989  climcndslem2  14990  climcnds  14991  efcllem  15214  ege2le3  15226  ef01bndlem  15320  cos01bnd  15322  cos2bnd  15324  cos01gt0  15327  sin02gt0  15328  sincos2sgn  15330  sin4lt0  15331  eirrlem  15340  egt2lt3  15342  epos  15343  ene1  15346  sqrt2re  15387  mod2eq1n2dvds  15479  oddge22np1  15481  evennn2n  15483  n2dvds1OLD  15501  nn0o1gt2  15515  nno  15516  nn0o  15517  nnoddm1d2  15520  bitsp1o  15565  bitsfzolem  15566  bitsfzo  15567  bitsfi  15569  6gcd4e2  15665  isprm7  15828  3lcm2e6  15848  prmreclem2  16029  prmreclem6  16033  4sqlem11  16067  4sqlem12  16068  prmgaplem7  16169  2expltfac  16202  plusgndxnmulrndx  16394  oppgtset  18169  efgredleme  18545  mgpsca  18887  mgptset  18888  mgpds  18890  rmodislmod  19327  cnfldfun  20158  zringndrg  20238  matplusg  20628  chfacfscmul0  21074  chfacfpmmul0  21078  psmetge0  22529  xmetge0  22561  bl2in  22617  metnrmlem3  23076  iihalf1  23142  iihalf2  23144  pcoass  23235  tcphcphlem1  23445  csbren  23609  trirn  23610  minveclem2  23636  minveclem4  23642  pjthlem1  23647  ovolunlem1a  23704  dyadss  23802  opnmbllem  23809  vitalilem2  23817  vitalilem4  23819  mbfi1fseqlem5  23927  lhop1lem  24217  aaliou3lem2  24539  aaliou3lem8  24541  pilem2  24647  pilem3  24648  pilem3OLD  24649  pipos  24654  sinhalfpilem  24657  sincosq1lem  24691  sincosq4sgn  24695  tangtx  24699  sinq12gt0  24701  sincos4thpi  24707  tan4thpi  24708  sincos6thpi  24709  sineq0  24715  cosordlem  24719  tanord1  24725  efif1olem1  24730  efif1olem2  24731  efif1olem4  24733  efif1o  24734  efifo  24735  2irrexpq  24917  cxpcn3lem  24932  root1id  24939  root1eq1  24940  root1cj  24941  cxpeq  24942  logblog  24974  2logb9irr  24977  2logb3irr  24979  ang180lem1  24991  ang180lem2  24992  chordthmlem2  25015  1cubrlem  25023  atancj  25092  atantan  25105  atanbndlem  25107  atans2  25113  leibpilem1OLD  25123  leibpi  25125  log2tlbnd  25128  log2ublem2  25130  log2ub  25132  divsqrtsumlem  25162  harmonicbnd3  25190  zetacvg  25197  lgamgulmlem2  25212  lgamgulmlem3  25213  lgamgulmlem4  25214  lgamgulmlem6  25216  lgamucov  25220  basellem1  25263  basellem2  25264  basellem3  25265  basellem5  25267  chtdif  25340  ppidif  25345  ppinncl  25356  chtrpcl  25357  ppieq0  25358  ppiltx  25359  ppiublem1  25383  ppiub  25385  chpeq0  25389  chteq0  25390  chtublem  25392  chtub  25393  chpval2  25399  chpub  25401  mersenne  25408  perfectlem1  25410  perfectlem2  25411  dchrptlem1  25445  dchrptlem2  25446  bcmono  25458  bclbnd  25461  bpos1lem  25463  bposlem1  25465  bposlem2  25466  bposlem3  25467  bposlem4  25468  bposlem5  25469  bposlem6  25470  bposlem7  25471  bposlem8  25472  bposlem9  25473  lgslem1  25478  lgsdirprm  25512  gausslemma2dlem0c  25539  gausslemma2dlem1a  25546  gausslemma2dlem2  25548  gausslemma2dlem3  25549  lgseisenlem1  25556  lgseisenlem2  25557  lgseisenlem3  25558  lgseisen  25560  lgsquadlem1  25561  lgsquadlem2  25562  m1lgs  25569  2lgslem1a1  25570  2lgslem1a2  25571  2lgslem1c  25574  2lgslem4  25587  2sqlem11  25610  chebbnd1lem1  25614  chebbnd1lem2  25615  chebbnd1lem3  25616  chebbnd1  25617  chtppilimlem1  25618  chtppilimlem2  25619  chtppilim  25620  chto1ub  25621  chebbnd2  25622  chto1lb  25623  chpchtlim  25624  chpo1ub  25625  chpo1ubb  25626  rplogsumlem1  25629  rplogsumlem2  25630  dchrisumlem2  25635  dchrisumlem3  25636  dchrvmasumiflem1  25646  dchrisum0fno1  25656  dchrisum0re  25658  dchrisum0lem1b  25660  dchrisum0lem1  25661  dchrisum0lem2  25663  rplogsum  25672  mulog2sumlem1  25679  mulog2sumlem2  25680  log2sumbnd  25689  selberglem2  25691  selbergb  25694  selberg2b  25697  chpdifbndlem1  25698  logdivbnd  25701  selberg3lem1  25702  selberg3  25704  selberg4lem1  25705  selberg4  25706  pntrmax  25709  pntrsumbnd2  25712  selberg3r  25714  selberg4r  25715  selberg34r  25716  pntrlog2bndlem2  25723  pntrlog2bndlem3  25724  pntrlog2bndlem4  25725  pntrlog2bndlem5  25726  pntrlog2bndlem6  25728  pntrlog2bnd  25729  pntpbnd1a  25730  pntpbnd1  25731  pntpbnd2  25732  pntpbnd  25733  pntibndlem2  25736  pntibndlem3  25737  pntibnd  25738  pntlemb  25742  pntlemg  25743  pntlemh  25744  pntlemr  25747  pntlemk  25751  pntlemo  25752  pnt2  25758  pnt  25759  ostth2lem1  25763  ostth3  25783  istrkg3ld  25816  tgldimor  25857  trgcgrg  25870  tgcgr4  25886  axlowdimlem6  26300  axlowdimlem16  26310  axlowdimlem17  26311  axlowdim  26314  upgrfi  26443  umgrupgr  26455  umgrislfupgrlem  26474  umgrislfupgr  26475  lfgrnloop  26477  usgruspgr  26531  usgrislfuspgr  26537  lfuhgr1v0e  26605  usgrexmpldifpr  26609  usgrexmplef  26610  nbusgrvtxm1  26731  vdegp1bi  26889  upgrewlkle2  26958  lfgrwlkprop  27042  upgr2pthnlp  27088  usgr2pthlem  27119  pthdlem1  27122  wwlksm1edg  27234  wwlksm1edgOLD  27235  wwlksnextwrd  27265  wwlksnextfun  27266  wwlksnextinj  27267  wwlksnextwrdOLD  27270  wwlksnextfunOLD  27271  wwlksnextinjOLD  27272  wwlksnextproplem3  27291  wwlksnextproplem3OLD  27292  clwlkclwwlklem2a1  27376  clwlkclwwlklem2a2  27377  clwlkclwwlklem2fv1  27379  clwlkclwwlklem2fv2  27380  clwlkclwwlklem2a4  27381  clwlkclwwlklem2a  27382  clwlkclwwlklem2  27384  clwlkclwwlk2  27388  clwlkclwwlk2OLD  27389  clwlkclwwlkfOLD  27396  clwlkclwwlkf  27400  clwwlkext2edg  27457  konigsbergiedgw  27658  konigsbergssiedgw  27660  konigsberglem1  27662  konigsberglem2  27663  konigsberglem3  27664  konigsberg  27667  frgrreggt1  27829  ex-pss  27864  ex-res  27877  ex-fv  27879  ex-fl  27883  ex-mod  27885  ex-abs  27891  ipidsq  28141  minvecolem2  28307  minvecolem4  28312  normlem7  28549  norm-ii-i  28570  norm3lemt  28585  normpar2i  28589  bcsiALT  28612  pjhthlem1  28826  opsqrlem6  29580  cdj3lem1  29869  addltmulALT  29881  threehalves  30189  oppgle  30219  resvplusg  30399  sqsscirc1  30556  nexple  30673  dya2iocucvr  30948  omssubadd  30964  oddpwdc  31018  eulerpartlemgc  31026  fibp1  31066  coinfliplem  31143  coinflipspace  31145  ballotlem2  31153  signstfveq0  31259  signstfveq0OLD  31260  prodfzo03  31287  hgt750lemd  31332  logdivsqrle  31334  hgt750lem  31335  hgt750lem2  31336  hgt750leme  31342  subfacp1lem1  31764  subfacp1lem5  31769  subfacval3  31774  problem2  32161  problem5  32164  circum  32169  nn0prpwlem  32909  dnibndlem10  33064  knoppcnlem2  33071  knoppcnlem4  33073  knoppcnlem10  33079  unbdqndv2lem1  33086  knoppndvlem1  33089  knoppndvlem10  33098  knoppndvlem11  33099  knoppndvlem12  33100  knoppndvlem14  33102  knoppndvlem15  33103  knoppndvlem17  33105  knoppndvlem18  33106  knoppndvlem19  33107  knoppndvlem20  33108  knoppndvlem21  33109  cnndvlem1  33114  taupi  33768  relowlpssretop  33810  sin2h  34029  cos2h  34030  tan2h  34031  poimirlem7  34047  poimirlem9  34049  opnmbllem0  34076  mblfinlem1  34077  mblfinlem2  34078  itg2addnclem  34091  isbnd2  34211  isbnd3  34212  heiborlem7  34245  oexpreposd  38165  rabren3dioph  38349  pellexlem2  38364  pellexlem5  38367  pell14qrgapw  38410  pellfundex  38420  rmspecsqrtnq  38440  jm2.24nn  38495  jm2.17a  38496  jm2.17b  38497  jm2.17c  38498  acongrep  38516  acongeq  38519  jm2.22  38531  jm2.23  38532  jm2.20nn  38533  jm3.1lem2  38554  expdiophlem1  38557  imo72b2lem0  39431  lhe4.4ex1a  39494  isosctrlem1ALT  40113  sineq0ALT  40116  lt3addmuld  40434  suplesup  40473  infleinflem2  40505  infleinf  40506  sumnnodd  40780  0ellimcdiv  40799  sinaover2ne0  41017  stoweidlem13  41167  stoweidlem14  41168  stoweidlem26  41180  stoweidlem49  41203  stoweidlem52  41206  wallispilem4  41222  wallispilem5  41223  wallispi  41224  wallispi2lem1  41225  wallispi2lem2  41226  wallispi2  41227  stirlinglem1  41228  stirlinglem3  41230  stirlinglem5  41232  stirlinglem6  41233  stirlinglem7  41234  stirlinglem10  41237  stirlinglem11  41238  stirlinglem15  41242  stirlingr  41244  dirker2re  41246  dirkerval2  41248  dirkerre  41249  dirkerper  41250  dirkertrigeqlem1  41252  dirkertrigeqlem3  41254  dirkercncflem1  41257  dirkercncflem2  41258  dirkercncflem4  41260  fourierdlem24  41285  fourierdlem43  41304  fourierdlem44  41305  fourierdlem57  41317  fourierdlem58  41318  fourierdlem62  41322  fourierdlem66  41326  fourierdlem68  41328  fourierdlem72  41332  fourierdlem76  41336  fourierdlem78  41338  fourierdlem79  41339  fourierdlem94  41354  fourierdlem103  41363  fourierdlem104  41364  fourierdlem111  41371  fourierdlem113  41373  sqwvfoura  41382  sqwvfourb  41383  fourierswlem  41384  fouriersw  41385  etransclem23  41411  salexct2  41491  salexct3  41494  salgencntex  41495  salgensscntex  41496  sge0ad2en  41582  ovnsubaddlem1  41721  smfmullem4  41938  smf2id  41945  2leaddle2  42350  p1lep2  42352  fmtnoge3  42473  fmtnof1  42478  fmtnoprmfac2lem1  42509  fmtno4prmfac  42515  fmtno4prm  42518  2pwp1prm  42534  31prm  42543  sfprmdvdsmersenne  42551  lighneallem2  42554  lighneallem4a  42556  lighneallem4b  42557  requad01  42569  requad1  42570  requad2  42571  dfodd4  42606  nn0o1gt2ALTV  42640  nnoALTV  42641  nn0oALTV  42642  nn0e  42643  perfectALTVlem1  42665  perfectALTVlem2  42666  gbowgt5  42685  sbgoldbalt  42704  sgoldbeven3prm  42706  mogoldbb  42708  nnsum3primes4  42711  nnsum3primesgbe  42715  nnsum3primesle9  42717  nnsum4primesodd  42719  nnsum4primesoddALTV  42720  wtgoldbnnsum4prm  42725  bgoldbnnsum3prm  42727  cznnring  42981  ply1mulgsumlem2  43200  zlmodzxznm  43311  zlmodzxzldeplem  43312  difmodm1lt  43342  nn0eo  43347  flnn0div2ge  43352  rege1logbzge0  43378  fldivexpfllog2  43384  logbpw2m1  43386  fllog2  43387  blenpw2m1  43398  nnpw2blen  43399  nnolog2flm1  43409  blennngt2o2  43411  dig2nn1st  43424  dig2nn0  43430  dig2bits  43433  dignn0flhalflem1  43434  dignn0flhalflem2  43435  dignn0flhalf  43437  nn0sumshdiglemA  43438  rrx2xpref1o  43464  itscnhlc0yqe  43505  itsclquadb  43522  2itscp  43527  itscnhlinecirc02p  43531