Theorem 2re 6958

Description: The number 2 is real.

Assertion

Ref	Expression
2re	|- 2 e. RR

Proof of Theorem 2re

Step	Hyp	Ref	Expression
1		df-2 6949	. 2 |- 2 = (1 + 1)
2		1re 6394	. . 3 |- 1 e. RR
3	2, 2	readdcli 6283	. 2 |- (1 + 1) e. RR
4	1, 3	eqeltri 1804	1 |- 2 e. RR

Syntax hints:   e. wcel 1138  (class class class)co 4695  RRcr 6181  1c1 6183   + caddc 6185  2c2 6940

This theorem is referenced by:  2cn 6959  3re 6960  2ne0 6969  3pos 6970  2lt3 7008  1lt3 7009  halfgt0 7010  halflt1 7011  halfpm6th 7013  rehalfcl 7015  halfpos2 7018  halfnneg2 7019  addltmul 7024  nominpos 7025  avgle 7026  nn0lele2xi 7139  halfnz 7201  nneoi 7204  flhalf 7282  fzprval 7482  fztpval 7483  expubnd 7648  discrlem1 7701  discrlem2 7702  nnesqi 7707  nn0opthlem2 7710  sqr4 7762  sqr2gt1lt2 7764  sqr2irrlem1 7769  sqr2irrlem4 7772  sqr2irr 7774  sqr2re 7775  abstrii 7938  abs3lemi 7948  faclbnd2 7993  faclbnd4lem1 7995  faclbnd5 8000  climunii 8153  climaddlem3 8171  arisumi 8282  expcnvlem5 8287  erelem1 8376  erelem2 8377  erelem3 8378  erelem4 8379  ele3lem 8383  ege2le3lem2 8386  efaddlem8 8402  efaddlem12 8406  efaddlem15 8409  efaddlem20 8414  efaddlem22 8416  efaddlem23 8417  efaddlem25 8419  eirrlem1 8446  eirrlem3 8448  egt2OLD 8452  egt2lt3 8454  reeff1olem2 8485  sin01bndlem1 8528  cos01bndlem2 8531  cos2bnd 8536  sin01gt0 8537  cos01gt0 8538  sin02gt0 8539  sincos2sgn 8541  sin4lt0 8542  znnen 8566  ruclem1 8574  ruclem2 8575  ruclem3 8576  ruclem13 8586  ruclem25 8598  ruclem26 8599  metge0 8891  bl2in 8915  dscmet 8991  bcthlem1 9072  bcthlem8 9079  bcthlem21 9092  nvge0 9429  vacnlem3 9464  ipid 9497  ubthlem12 9678  ubthlem12OLD 9679  ubthlem13 9680  ubthlem13OLD 9681  ubthlem14 9682  minveclem16 9700  minveclem21 9705  minveclem25 9709  minveclem26 9710  minveclem27 9711  minveclem35 9719  minveclem38 9722  pilem1 9815  pilem2 9816  pilem3 9817  pigt2lt4 9819  sinhalfpilem 9823  sinperlem1 9830  sincosq1lem 9847  sincosq1sgn 9848  sincosq2sgn 9849  sincosq3sgn 9850  sincosq4sgn 9851  sinq12gt0t 9852  sincos4thpi 9855  sincos6thpi 9856  sineq0re 9862  cosh111lem1 9863  efif 9870  efifolem2 9872  efifolem3 9873  efifolem4 9874  efifolem6 9876  efifolem7 9877  efif1lem1 9879  efif1lem2 9880  efif1lem4 9882  efif1lem5 9883  efif1lem6 9884  efif1lem7 9885  circgrp 9889  shftefif1olem 9890  effoi 9894  efper 9896  normlem7 10407  norm-ii.i 10429  norm3lem 10441  norm3lemt 10444  normpar2i 10448  bcsiALT 10471  hlimcauii 10531  hlimuniii 10533  projlem1 10611  projlem2 10612  projlem3 10613  projlem4 10614  projlem5 10615  projlem6 10616  projlem18 10628  projlem28 10638  opsqrlem3 11505  opsqrlem6 11508  hmopidmchi 11515  staddi 11610  cdj3lem1 11798  addltmulALT 11810  isprm3 13568  4nprm 13573  cntrsetlem 14709  dmse1 14711  msr3 14713  mslb1 14717  msra3 14719  iintlem1 14720  epos 15047  rddif 15480  absrdbnd 15481  fsumltisumi 15505  csbrni 15514  trirni 15515  blhalf 15528  mettrifi 15529  iihalf1 15554  iihalf2 15555  sstotbnd 15618  totbndss 15619  isbnd3 15623  heiborlem16 15652  heiborlem27 15663  heiborlem28 15664  heiborlem30 15666  heiborlem31 15667  heiborlem32 15668  heiborlem33 15669  heiborlem35 15671  heiborlem36 15672  bfp 15691  rrntotbndlem1 15702  rrntotbndlem2 15703  rrntotbnd 15704  phtpycolem1 15733  phtpycolem2 15734  phtpycolem3 15735  phtpycolem4 15736  phtpycolem5 15737  phtpyco 15738  pcoval1 15756  pcoval2 15757  pcocn 15758  pco0 15759  pco1 15760  pcohtpylem1 15762  pcohtpylem2 15763  pcohtpylem3 15764  pcohtpy 15765  pcopt 15766  pcoass 15767  pcorevlem 15768  pcorev 15769  stb2val1 16494  stb2val2 16495  stb3val2 16499  stb3val3 16500  stb2xpl 16501  stb3xpl 16502  divrngmclNEW 16893  invrcl 16900

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1142  ax-gen 1143  ax-8 1144  ax-9 1145  ax-10 1146  ax-11 1147  ax-12 1148  ax-13 1149  ax-14 1150  ax-17 1155  ax-4 1157  ax-5o 1159  ax-6o 1162  ax-9o 1319  ax-10o 1338  ax-16 1418  ax-11o 1426  ax-ext 1702  ax-rep 3243  ax-sep 3253  ax-nul 3260  ax-pow 3296  ax-pr 3339  ax-un 3601  ax-inf2 5540

This theorem depends on definitions:  df-bi 163  df-or 240  df-an 241  df-3or 856  df-3an 857  df-ex 1165  df-sb 1374  df-eu 1613  df-mo 1614  df-clab 1709  df-cleq 1714  df-clel 1717  df-ne 1856  df-ral 1943  df-rex 1944  df-reu 1945  df-rab 1946  df-v 2127  df-sbc 2287  df-csb 2374  df-dif 2430  df-un 2433  df-in 2436  df-ss 2438  df-pss 2440  df-nul 2702  df-if 2807  df-pw 2859  df-sn 2873  df-pr 2874  df-tp 2876  df-op 2877  df-uni 3000  df-int 3037  df-iun 3079  df-br 3159  df-opab 3214  df-tr 3230  df-eprel 3398  df-id 3401  df-po 3406  df-so 3419  df-fr 3440  df-we 3459  df-ord 3475  df-on 3476  df-lim 3477  df-suc 3478  df-om 3761  df-xp 3811  df-rel 3812  df-cnv 3813  df-co 3814  df-dm 3815  df-rn 3816  df-res 3817  df-ima 3818  df-fun 3819  df-fn 3820  df-f 3821  df-f1 3822  df-fo 3823  df-f1o 3824  df-fv 3825  df-opr 4697  df-oprab 4698  df-mpt 4817  df-1st 4831  df-2nd 4832  df-iota 4900  df-rdg 4951  df-1o 4988  df-oadd 4990  df-omul 4991  df-er 5129  df-ec 5131  df-qs 5134  df-en 5238  df-dom 5239  df-sdom 5240  df-undef 5367  df-riota 5371  df-ni 5948  df-pli 5949  df-mi 5950  df-lti 5951  df-plpq 5983  df-mpq 5984  df-enq 5985  df-nq 5986  df-plq 5987  df-mq 5988  df-rq 5989  df-ltq 5990  df-1q 5991  df-np 6034  df-1p 6035  df-plp 6036  df-mp 6037  df-ltp 6038  df-plpr 6112  df-mpr 6113  df-enr 6114  df-nr 6115  df-plr 6116  df-mr 6117  df-ltr 6118  df-0r 6119  df-1r 6120  df-m1r 6121  df-c 6188  df-0 6189  df-1 6190  df-i 6191  df-r 6192  df-plus 6193  df-mul 6194  df-sub 6307  df-neg 6309  df-2 6949

Copyright terms: Public domain