Theorem 2re 5877

Description: The number 2 is real.

Assertion

Ref	Expression
2re	|- 2 e. RR

Proof of Theorem 2re

Step	Hyp	Ref	Expression
1		df-2 5868	. 2 |- 2 = (1 + 1)
2		1re 5358	. . 3 |- 1 e. RR
3	2, 2	readdcl 5257	. 2 |- (1 + 1) e. RR
4	1, 3	eqeltr 1520	1 |- 2 e. RR

Syntax hints:   e. wcel 1105  (class class class)co 3902  RRcr 5156  1c1 5158   + caddc 5160  2c2 5859

This theorem is referenced by:  2cn 5878  3re 5879  2ne0 5888  3pos 5889  halfgt0 5927  halflt1 5928  halfpm6th 5930  rehalfclt 5932  halfpos2t 5935  halfnneg2t 5936  nominpos 5941  avglet 5942  nn0lele2x 6033  halfnz 6092  nneo 6095  flhalft 6140  expubndt 6490  discrlem1 6537  discrlem2 6538  nnesq 6543  nn0opthlem2 6546  sqr4 6598  sqr2gt1lt2 6600  sqr2irrlem1 6605  sqr2irrlem4 6608  sqr2irr 6610  sqr2re 6611  abstri 6780  abs3lem 6789  faclbnd2 6834  faclbnd4lem1 6836  faclbnd5 6841  climunii 6986  climaddlem3 7003  ser1f0 7057  fnsmnt 7112  expcnvlem5 7117  erelem1 7212  erelem2 7213  erelem3 7214  erelem4 7215  ele3lem 7219  ege2le3lem2 7222  efaddlem8 7238  efaddlem12 7242  efaddlem15 7245  efaddlem20 7250  efaddlem22 7252  efaddlem23 7253  efaddlem25 7255  eirrlem1 7281  eirrlem3 7283  reeff1olem2 7316  reeff1olem2OLD 7318  sin01bndlem1 7360  cos01bndlem2 7363  cos2bnd 7368  sin01gt0 7369  cos01gt0 7370  sin02gt0 7371  sincos2sgn 7373  sin4lt0 7374  znnen 7396  ruclem1 7404  ruclem2 7405  ruclem3 7406  ruclem13 7416  ruclem25 7428  ruclem26 7429  metge0 7708  bl2in 7731  dscmet 7804  bcthlem1 7881  bcthlem8 7888  bcthlem21 7901  nvge0 8178  ipid 8232  ubthlem12 8406  ubthlem13 8407  ubthlem14 8408  minveclem16 8426  minveclem21 8431  minveclem25 8435  minveclem26 8436  minveclem27 8437  minveclem35 8445  minveclem38 8448  pilem1 8503  pilem2 8504  pilem3 8505  pigt2lt4 8507  sinhalfpilem 8511  sinperlem1 8518  sincosq1lem 8533  sincosq1sgn 8534  sincosq2sgn 8535  sincosq3sgn 8536  sincosq4sgn 8537  sinq12gt0t 8538  sincos4thpi 8540  sincos6thpi 8541  cosh111lem1 8542  efif 8549  efifolem2 8551  efifolem3 8552  efifolem4 8553  efifolem6 8555  efifolem7 8556  efif1lem1 8558  efif1lem2 8559  efif1lem4 8561  efif1lem5 8562  efif1lem6 8563  efif1lem7 8564  circgrp 8573  shftefif1olem 8574  shftefif1olemOLD 8575  effoi 8579  effoiOLD 8580  efper 8582  dmse1 8817  msr3 8819  msr4 8820  mslb1 8823  msra3 8825  iintlem1 8826  normlem7 9131  norm-ii 9153  norm3lem 9165  norm3lemt 9168  normpar2 9172  bcsALT 9195  hlimcaui 9257  hlimunii 9259  projlem1 9316  projlem2 9317  projlem3 9318  projlem4 9319  projlem5 9320  projlem6 9321  projlem18 9333  projlem28 9343  hmopidmch 10204  stadd 10297  cdj3lem1 10480

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-4 951  ax-5 952  ax-6 953  ax-7 954  ax-gen 955  ax-8 1101  ax-9 1102  ax-10 1103  ax-12 1104  ax-13 1107  ax-14 1108  ax-11 1180  ax-17 1190  ax-16 1194  ax-11o 1202  ax-ext 1436  ax-rep 2661  ax-sep 2671  ax-nul 2678  ax-pow 2710  ax-pr 2747  ax-un 2830  ax-inf2 4549

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-3or 773  df-3an 774  df-ex 957  df-sb 1155  df-eu 1359  df-mo 1360  df-clab 1441  df-cleq 1446  df-clel 1449  df-ne 1563  df-ral 1625  df-rex 1626  df-reu 1627  df-rab 1628  df-v 1787  df-sbc 1913  df-csb 1973  df-dif 2020  df-un 2021  df-in 2022  df-ss 2024  df-pss 2026  df-nul 2252  df-if 2333  df-pw 2373  df-sn 2383  df-pr 2384  df-tp 2386  df-op 2387  df-uni 2472  df-int 2502  df-iun 2536  df-br 2588  df-opab 2635  df-tr 2649  df-eprel 2794  df-id 2797  df-po 2804  df-so 2814  df-fr 2880  df-we 2897  df-ord 2914  df-on 2915  df-lim 2916  df-suc 2917  df-om 3095  df-xp 3147  df-rel 3148  df-cnv 3149  df-co 3150  df-dm 3151  df-rn 3152  df-res 3153  df-ima 3154  df-fun 3155  df-fn 3156  df-f 3157  df-fv 3161  df-rdg 3871  df-opr 3904  df-oprab 3905  df-1st 4017  df-2nd 4018  df-1o 4071  df-oadd 4073  df-omul 4074  df-er 4199  df-ec 4201  df-qs 4204  df-ni 4923  df-pli 4924  df-mi 4925  df-lti 4926  df-plpq 4958  df-mpq 4959  df-enq 4960  df-nq 4961  df-plq 4962  df-mq 4963  df-rq 4964  df-ltq 4965  df-1q 4966  df-np 5009  df-1p 5010  df-plp 5011  df-mp 5012  df-ltp 5013  df-plpr 5087  df-mpr 5088  df-enr 5089  df-nr 5090  df-plr 5091  df-mr 5092  df-ltr 5093  df-0r 5094  df-1r 5095  df-m1r 5096  df-c 5163  df-0 5164  df-1 5165  df-i 5166  df-r 5167  df-plus 5168  df-mul 5169  df-sub 5279  df-neg 5281  df-2 5868

Copyright terms: Public domain