Theorem 2re 5940

Description: The number 2 is real.

Assertion

Ref	Expression
2re	|- 2 e. RR

Proof of Theorem 2re

Step	Hyp	Ref	Expression
1		df-2 5931	. 2 |- 2 = (1 + 1)
2		1re 5422	. . 3 |- 1 e. RR
3	2, 2	readdcl 5321	. 2 |- (1 + 1) e. RR
4	1, 3	eqeltr 1543	1 |- 2 e. RR

Syntax hints:   e. wcel 957  (class class class)co 3960  RRcr 5220  1c1 5222   + caddc 5224  2c2 5922

This theorem is referenced by:  2cn 5941  3re 5942  2ne0 5951  3pos 5952  halfgt0 5990  halflt1 5991  halfpm6th 5993  rehalfclt 5995  halfpos2t 5998  halfnneg2t 5999  nominpos 6004  avglet 6005  nn0lele2x 6096  halfnz 6155  nneo 6158  flhalft 6206  expubndt 6558  discrlem1 6606  discrlem2 6607  nnesq 6612  nn0opthlem2 6615  nn0opthlem2OLD 6616  sqr4 6668  sqr2gt1lt2 6670  sqr2irrlem1 6675  sqr2irrlem4 6678  sqr2irr 6680  sqr2re 6681  abstri 6856  abs3lem 6866  faclbnd2 6912  faclbnd4lem1 6914  faclbnd5 6919  climunii 7066  climaddlem3 7085  ser1f0 7141  fnsmnt 7197  expcnvlem5 7202  erelem1 7297  erelem2 7298  erelem3 7299  erelem4 7300  ele3lem 7304  ege2le3lem2 7307  efaddlem8 7323  efaddlem12 7327  efaddlem15 7330  efaddlem20 7335  efaddlem22 7337  efaddlem23 7338  efaddlem25 7340  eirrlem1 7366  eirrlem3 7368  reeff1olem2 7401  reeff1olem2OLD 7403  sin01bndlem1 7445  cos01bndlem2 7448  cos2bnd 7453  sin01gt0 7454  cos01gt0 7455  sin02gt0 7456  sincos2sgn 7458  sin4lt0 7459  znnen 7481  ruclem1 7489  ruclem2 7490  ruclem3 7491  ruclem13 7501  ruclem25 7513  ruclem26 7514  metge0 7800  bl2in 7825  dscmet 7901  bcthlem1 7982  bcthlem8 7989  bcthlem21 8002  nvge0 8287  ipid 8349  ubthlem12 8524  ubthlem13 8525  ubthlem14 8526  minveclem16 8544  minveclem21 8549  minveclem25 8553  minveclem26 8554  minveclem27 8555  minveclem35 8563  minveclem38 8566  pilem1 8654  pilem2 8655  pilem3 8656  pigt2lt4 8658  sinhalfpilem 8662  sinperlem1 8669  sincosq1lem 8684  sincosq1sgn 8685  sincosq2sgn 8686  sincosq3sgn 8687  sincosq4sgn 8688  sinq12gt0t 8689  sincos4thpi 8691  sincos6thpi 8692  cosh111lem1 8693  efif 8700  efifolem2 8702  efifolem3 8703  efifolem4 8704  efifolem6 8706  efifolem7 8707  efif1lem1 8709  efif1lem2 8710  efif1lem4 8712  efif1lem5 8713  efif1lem6 8714  efif1lem7 8715  circgrp 8724  shftefif1olem 8725  effoi 8729  efper 8731  normlem7 8966  norm-ii 8988  norm3lem 9000  norm3lemt 9003  normpar2 9007  bcsALT 9034  hlimcaui 9094  hlimunii 9096  projlem1 9174  projlem2 9175  projlem3 9176  projlem4 9177  projlem5 9178  projlem6 9179  projlem18 9191  projlem28 9201  hmopidmch 10070  stadd 10164  cdj3lem1 10352  dmse1 10574  msr3 10576  msr4 10577  mslb1 10580  msra3 10582  iintlem1 10583

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 961  ax-gen 962  ax-8 963  ax-9 964  ax-10 965  ax-11 966  ax-12 967  ax-13 968  ax-14 969  ax-17 970  ax-4 972  ax-5o 974  ax-6o 977  ax-9o 1122  ax-10o 1139  ax-16 1210  ax-11o 1218  ax-ext 1459  ax-rep 2690  ax-sep 2700  ax-nul 2707  ax-pow 2739  ax-pr 2776  ax-un 2863  ax-inf2 4612

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-3or 775  df-3an 776  df-ex 980  df-sb 1172  df-eu 1382  df-mo 1383  df-clab 1464  df-cleq 1469  df-clel 1472  df-ne 1586  df-ral 1648  df-rex 1649  df-reu 1650  df-rab 1651  df-v 1810  df-sbc 1940  df-csb 2000  df-dif 2047  df-un 2048  df-in 2049  df-ss 2051  df-pss 2053  df-nul 2279  df-if 2360  df-pw 2400  df-sn 2410  df-pr 2411  df-tp 2413  df-op 2414  df-uni 2501  df-int 2531  df-iun 2565  df-br 2617  df-opab 2664  df-tr 2678  df-eprel 2829  df-id 2832  df-po 2837  df-so 2847  df-fr 2914  df-we 2931  df-ord 2948  df-on 2949  df-lim 2950  df-suc 2951  df-om 3129  df-xp 3181  df-rel 3182  df-cnv 3183  df-co 3184  df-dm 3185  df-rn 3186  df-res 3187  df-ima 3188  df-fun 3189  df-fn 3190  df-f 3191  df-fv 3195  df-rdg 3929  df-opr 3962  df-oprab 3963  df-1st 4076  df-2nd 4077  df-1o 4130  df-oadd 4132  df-omul 4133  df-er 4258  df-ec 4260  df-qs 4263  df-ni 4987  df-pli 4988  df-mi 4989  df-lti 4990  df-plpq 5022  df-mpq 5023  df-enq 5024  df-nq 5025  df-plq 5026  df-mq 5027  df-rq 5028  df-ltq 5029  df-1q 5030  df-np 5073  df-1p 5074  df-plp 5075  df-mp 5076  df-ltp 5077  df-plpr 5151  df-mpr 5152  df-enr 5153  df-nr 5154  df-plr 5155  df-mr 5156  df-ltr 5157  df-0r 5158  df-1r 5159  df-m1r 5160  df-c 5227  df-0 5228  df-1 5229  df-i 5230  df-r 5231  df-plus 5232  df-mul 5233  df-sub 5343  df-neg 5345  df-2 5931

Copyright terms: Public domain