Theorem 2re 11090

Description: The number 2 is real. (Contributed by NM, 27-May-1999.)

Assertion

Ref	Expression
2re	|- 2 e. RR

Proof of Theorem 2re

Step	Hyp	Ref	Expression
1		df-2 11079	. 2 |- 2 = ( 1 + 1 )
2		1re 10039	. . 3 |- 1 e. RR
3	2, 2	readdcli 10053	. 2 |- ( 1 + 1 ) e. RR
4	1, 3	eqeltri 2697	1 |- 2 e. RR

Syntax hints:   e. wcel 1990  (class class class)co 6650   RRcr 9935   1c1 9937   + caddc 9939   2c2 11070

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-1cn 9994  ax-icn 9995  ax-addcl 9996  ax-addrcl 9997  ax-mulcl 9998  ax-mulrcl 9999  ax-i2m1 10004  ax-1ne0 10005  ax-rrecex 10008  ax-cnre 10009

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-ral 2917  df-rex 2918  df-rab 2921  df-v 3202  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-sn 4178  df-pr 4180  df-op 4184  df-uni 4437  df-br 4654  df-iota 5851  df-fv 5896  df-ov 6653  df-2 11079

This theorem is referenced by:  2cn  11091  3re  11094  2ne0  11113  3pos  11114  2lt3  11195  1lt3  11196  2lt4  11198  1lt4  11199  2lt5  11202  2lt6  11207  1lt6  11208  2lt7  11213  1lt7  11214  2lt8  11220  1lt8  11221  2lt9  11228  1lt9  11229  2lt10OLD  11237  1lt10OLD  11238  1le2  11241  2rene0  11243  halfre  11246  halfgt0  11248  halflt1  11250  rehalfcl  11258  halfpos2  11261  halfnneg2  11263  addltmul  11268  nominpos  11269  avglt1  11270  avglt2  11271  div4p1lem1div2  11287  nn0lele2xi  11348  nn0n0n1ge2b  11359  nn0ge2m1nn  11360  nn0le2is012  11441  halfnz  11455  3halfnz  11456  2lt10  11680  1lt10  11681  uzuzle23  11729  uz3m2nn  11731  2rp  11837  zgt1rpn0n1  11871  xnn0n0n1ge2b  11965  fztpval  12402  fz0to4untppr  12442  fzo0to42pr  12555  2tnp1ge0ge0  12630  flhalf  12631  fldiv4p1lem1div2  12636  fldiv4lem1div2uz2  12637  2txmodxeq0  12730  expubnd  12921  expmulnbnd  12996  nn0opthlem2  13056  faclbnd2  13078  faclbnd4lem1  13080  faclbnd5  13085  4bc2eq6  13116  hashfun  13224  hashge2el2dif  13262  hashge2el2difr  13263  wrdlenge2n0  13341  f1oun2prg  13662  2swrd2eqwrdeq  13696  sqrlem7  13989  sqrt4  14013  sqrt2gt1lt2  14015  abstri  14070  sqreulem  14099  amgm2  14109  caucvgrlem  14403  iseralt  14415  climcndslem1  14581  climcndslem2  14582  climcnds  14583  geoihalfsum  14614  efcllem  14808  ege2le3  14820  ef01bndlem  14914  cos01bnd  14916  cos2bnd  14918  cos01gt0  14921  sin02gt0  14922  sincos2sgn  14924  sin4lt0  14925  eirrlem  14932  egt2lt3  14934  epos  14935  ene1  14938  sqrt2re  14980  oexpneg  15069  mod2eq1n2dvds  15071  oddge22np1  15073  evennn02n  15074  evennn2n  15075  nn0ehalf  15095  nn0o1gt2  15097  nno  15098  nn0o  15099  nn0oddm1d2  15101  nnoddm1d2  15102  n2dvds1  15104  flodddiv4t2lthalf  15140  bitsp1o  15155  bitsfzolem  15156  bitsfzo  15157  bitsfi  15159  6gcd4e2  15255  isprm7  15420  3lcm2e6  15440  oddprm  15515  iserodd  15540  prmreclem2  15621  prmreclem6  15625  4sqlem11  15659  4sqlem12  15660  prmgaplem7  15761  2expltfac  15799  plusgndxnmulrndx  15998  oppgtset  17782  efgredleme  18156  mgpsca  18496  mgptset  18497  mgpds  18499  rmodislmod  18931  cnfldfun  19758  zringndrg  19838  matplusg  20220  chfacfscmul0  20663  chfacfpmmul0  20667  psmetge0  22117  xmetge0  22149  bl2in  22205  metnrmlem3  22664  iihalf1  22730  iihalf2  22732  pcoass  22824  tchcphlem1  23034  csbren  23182  trirn  23183  minveclem2  23197  minveclem4  23203  pjthlem1  23208  ovolunlem1a  23264  dyadss  23362  opnmbllem  23369  vitalilem2  23378  vitalilem4  23380  mbfi1fseqlem5  23486  lhop1lem  23776  aaliou3lem2  24098  aaliou3lem8  24100  pilem2  24206  pilem3  24207  pipos  24212  sinhalfpilem  24215  sincosq1lem  24249  sincosq4sgn  24253  tangtx  24257  sinq12gt0  24259  sincos4thpi  24265  tan4thpi  24266  sincos6thpi  24267  sineq0  24273  cosordlem  24277  tanord1  24283  efif1olem1  24288  efif1olem2  24289  efif1olem4  24291  efif1o  24292  efifo  24293  cxpcn3lem  24488  root1id  24495  root1eq1  24496  root1cj  24497  cxpeq  24498  logblog  24530  ang180lem1  24539  ang180lem2  24540  chordthmlem2  24560  1cubrlem  24568  atancj  24637  atantan  24650  atanbndlem  24652  atans2  24658  leibpilem1  24667  leibpi  24669  log2tlbnd  24672  log2ublem2  24674  log2ub  24676  divsqrtsumlem  24706  harmonicbnd3  24734  zetacvg  24741  lgamgulmlem2  24756  lgamgulmlem3  24757  lgamgulmlem4  24758  lgamgulmlem6  24760  lgamucov  24764  basellem1  24807  basellem2  24808  basellem3  24809  basellem5  24811  chtdif  24884  ppidif  24889  ppinncl  24900  chtrpcl  24901  ppieq0  24902  ppiltx  24903  ppiublem1  24927  ppiub  24929  chpeq0  24933  chteq0  24934  chtublem  24936  chtub  24937  chpval2  24943  chpub  24945  mersenne  24952  perfectlem1  24954  perfectlem2  24955  dchrptlem1  24989  dchrptlem2  24990  bcmono  25002  bclbnd  25005  bpos1lem  25007  bposlem1  25009  bposlem2  25010  bposlem3  25011  bposlem4  25012  bposlem5  25013  bposlem6  25014  bposlem7  25015  bposlem8  25016  bposlem9  25017  lgslem1  25022  lgsdirprm  25056  gausslemma2dlem0c  25083  gausslemma2dlem1a  25090  gausslemma2dlem2  25092  gausslemma2dlem3  25093  lgseisenlem1  25100  lgseisenlem2  25101  lgseisenlem3  25102  lgseisen  25104  lgsquadlem1  25105  lgsquadlem2  25106  m1lgs  25113  2lgslem1a1  25114  2lgslem1a2  25115  2lgslem1c  25118  2lgslem4  25131  2sqlem11  25154  chebbnd1lem1  25158  chebbnd1lem2  25159  chebbnd1lem3  25160  chebbnd1  25161  chtppilimlem1  25162  chtppilimlem2  25163  chtppilim  25164  chto1ub  25165  chebbnd2  25166  chto1lb  25167  chpchtlim  25168  chpo1ub  25169  chpo1ubb  25170  rplogsumlem1  25173  rplogsumlem2  25174  dchrisumlem2  25179  dchrisumlem3  25180  dchrvmasumiflem1  25190  dchrisum0fno1  25200  dchrisum0re  25202  dchrisum0lem1b  25204  dchrisum0lem1  25205  dchrisum0lem2  25207  rplogsum  25216  mulog2sumlem1  25223  mulog2sumlem2  25224  log2sumbnd  25233  selberglem2  25235  selbergb  25238  selberg2b  25241  chpdifbndlem1  25242  logdivbnd  25245  selberg3lem1  25246  selberg3  25248  selberg4lem1  25249  selberg4  25250  pntrmax  25253  pntrsumbnd2  25256  selberg3r  25258  selberg4r  25259  selberg34r  25260  pntrlog2bndlem2  25267  pntrlog2bndlem3  25268  pntrlog2bndlem4  25269  pntrlog2bndlem5  25270  pntrlog2bndlem6  25272  pntrlog2bnd  25273  pntpbnd1a  25274  pntpbnd1  25275  pntpbnd2  25276  pntpbnd  25277  pntibndlem2  25280  pntibndlem3  25281  pntibnd  25282  pntlemb  25286  pntlemg  25287  pntlemh  25288  pntlemr  25291  pntlemk  25295  pntlemo  25296  pnt2  25302  pnt  25303  ostth2lem1  25307  ostth3  25327  istrkg3ld  25360  tgldimor  25397  trgcgrg  25410  tgcgr4  25426  axlowdimlem6  25827  axlowdimlem16  25837  axlowdimlem17  25838  axlowdim  25841  upgrfi  25986  umgrupgr  25998  umgrislfupgrlem  26017  umgrislfupgr  26018  lfgrnloop  26020  usgruspgr  26073  usgrislfuspgr  26079  lfuhgr1v0e  26146  usgrexmpldifpr  26150  usgrexmplef  26151  nbusgrvtxm1  26281  vdegp1bi  26433  upgrewlkle2  26502  lfgrwlkprop  26584  upgr2pthnlp  26628  usgr2pthlem  26659  pthdlem1  26662  wwlksm1edg  26767  wwlksnextwrd  26792  wwlksnextfun  26793  wwlksnextinj  26794  wwlksnextproplem3  26806  clwlkclwwlklem2a1  26893  clwlkclwwlklem2a2  26894  clwlkclwwlklem2fv1  26896  clwlkclwwlklem2fv2  26897  clwlkclwwlklem2a4  26898  clwlkclwwlklem2a  26899  clwlkclwwlklem2  26901  clwlkclwwlk2  26904  clwwlksext2edg  26923  clwlksfclwwlk  26962  konigsbergiedgw  27108  konigsbergiedgwOLD  27109  konigsbergssiedgw  27111  konigsberglem1  27114  konigsberglem2  27115  konigsberglem3  27116  konigsberg  27119  frgrreggt1  27251  ex-pss  27285  ex-res  27298  ex-fv  27300  ex-fl  27304  ex-mod  27306  ex-abs  27312  nvge0  27528  ipidsq  27565  minvecolem2  27731  minvecolem4  27736  normlem7  27973  norm-ii-i  27994  norm3lemt  28009  normpar2i  28013  bcsiALT  28036  pjhthlem1  28250  opsqrlem6  29004  cdj3lem1  29293  addltmulALT  29305  threehalves  29623  oppgle  29653  resvplusg  29833  sqsscirc1  29954  nexple  30071  dya2iocucvr  30346  omssubadd  30362  oddpwdc  30416  eulerpartlemgc  30424  fibp1  30463  coinfliplem  30540  coinflipspace  30542  ballotlem2  30550  signstfveq0  30654  prodfzo03  30681  hgt750lemd  30726  logdivsqrle  30728  hgt750lem  30729  hgt750lem2  30730  hgt750leme  30736  subfacp1lem1  31161  subfacp1lem5  31166  subfacval3  31171  problem2  31559  problem2OLD  31560  problem5  31563  circum  31568  nn0prpwlem  32317  dnibndlem10  32477  knoppcnlem2  32484  knoppcnlem4  32486  knoppcnlem10  32492  unbdqndv2lem1  32500  knoppndvlem1  32503  knoppndvlem10  32512  knoppndvlem11  32513  knoppndvlem12  32514  knoppndvlem14  32516  knoppndvlem15  32517  knoppndvlem17  32519  knoppndvlem18  32520  knoppndvlem19  32521  knoppndvlem20  32522  knoppndvlem21  32523  cnndvlem1  32528  taupi  33169  relowlpssretop  33212  sin2h  33399  cos2h  33400  tan2h  33401  poimirlem7  33416  poimirlem9  33418  opnmbllem0  33445  mblfinlem1  33446  mblfinlem2  33447  itg2addnclem  33461  isbnd2  33582  isbnd3  33583  heiborlem7  33616  rabren3dioph  37379  pellexlem2  37394  pellexlem5  37397  pell14qrgapw  37440  pellfundex  37450  rmspecsqrtnq  37470  rmspecsqrtnqOLD  37471  jm2.24nn  37526  jm2.17a  37527  jm2.17b  37528  jm2.17c  37529  acongrep  37547  acongeq  37550  jm2.22  37562  jm2.23  37563  jm2.20nn  37564  jm3.1lem2  37585  expdiophlem1  37588  imo72b2lem0  38465  lhe4.4ex1a  38528  isosctrlem1ALT  39170  sineq0ALT  39173  lt3addmuld  39515  suplesup  39555  infleinflem2  39587  infleinf  39588  sumnnodd  39862  0ellimcdiv  39881  sinaover2ne0  40079  stoweidlem13  40230  stoweidlem14  40231  stoweidlem26  40243  stoweidlem49  40266  stoweidlem52  40269  wallispilem4  40285  wallispilem5  40286  wallispi  40287  wallispi2lem1  40288  wallispi2lem2  40289  wallispi2  40290  stirlinglem1  40291  stirlinglem3  40293  stirlinglem5  40295  stirlinglem6  40296  stirlinglem7  40297  stirlinglem10  40300  stirlinglem11  40301  stirlinglem15  40305  stirlingr  40307  dirker2re  40309  dirkerval2  40311  dirkerre  40312  dirkerper  40313  dirkertrigeqlem1  40315  dirkertrigeqlem3  40317  dirkercncflem1  40320  dirkercncflem2  40321  dirkercncflem4  40323  fourierdlem24  40348  fourierdlem43  40367  fourierdlem44  40368  fourierdlem57  40380  fourierdlem58  40381  fourierdlem62  40385  fourierdlem66  40389  fourierdlem68  40391  fourierdlem72  40395  fourierdlem76  40399  fourierdlem78  40401  fourierdlem79  40402  fourierdlem94  40417  fourierdlem103  40426  fourierdlem104  40427  fourierdlem111  40434  fourierdlem113  40436  sqwvfoura  40445  sqwvfourb  40446  fourierswlem  40447  fouriersw  40448  etransclem23  40474  salexct2  40557  salexct3  40560  salgencntex  40561  salgensscntex  40562  sge0ad2en  40648  ovnsubaddlem1  40784  smfmullem4  41001  smf2id  41008  2leaddle2  41312  p1lep2  41314  pfx2  41412  fmtnoge3  41442  fmtnof1  41447  fmtnoprmfac2lem1  41478  fmtno4prmfac  41484  fmtno4prm  41487  2pwp1prm  41503  31prm  41512  sfprmdvdsmersenne  41520  lighneallem2  41523  lighneallem4a  41525  lighneallem4b  41526  dfodd4  41571  oexpnegALTV  41588  nn0o1gt2ALTV  41605  nnoALTV  41606  nn0oALTV  41607  nn0e  41608  perfectALTVlem1  41630  perfectALTVlem2  41631  gbowgt5  41650  sbgoldbalt  41669  sgoldbeven3prm  41671  mogoldbb  41673  nnsum3primes4  41676  nnsum3primesgbe  41680  nnsum3primesle9  41682  nnsum4primesodd  41684  nnsum4primesoddALTV  41685  wtgoldbnnsum4prm  41690  bgoldbnnsum3prm  41692  cznnring  41956  ply1mulgsumlem2  42175  zlmodzxznm  42286  zlmodzxzldeplem  42287  difmodm1lt  42317  nn0eo  42322  flnn0div2ge  42327  rege1logbzge0  42353  fldivexpfllog2  42359  logbpw2m1  42361  fllog2  42362  blenpw2m1  42373  nnpw2blen  42374  nnolog2flm1  42384  blennngt2o2  42386  dig2nn1st  42399  dig2nn0  42405  dig2bits  42408  dignn0flhalflem1  42409  dignn0flhalflem2  42410  dignn0flhalf  42412  nn0sumshdiglemA  42413