Theorem 4re 12209

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

Assertion

Ref	Expression
4re	⊢ 4 ∈ ℝ

Proof of Theorem 4re

Step	Hyp	Ref	Expression
1		df-4 12190	. 2 ⊢ 4 = (3 + 1)
2		3re 12205	. . 3 ⊢ 3 ∈ ℝ
3		1re 11112	. . 3 ⊢ 1 ∈ ℝ
4	2, 3	readdcli 11127	. 2 ⊢ (3 + 1) ∈ ℝ
5	1, 4	eqeltri 2827	1 ⊢ 4 ∈ ℝ

Syntax hints:   ∈ wcel 2111  (class class class)co 7346  ℝcr 11005  1c1 11007   + caddc 11009  3c3 12181  4c4 12182

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703  ax-1cn 11064  ax-icn 11065  ax-addcl 11066  ax-addrcl 11067  ax-mulcl 11068  ax-mulrcl 11069  ax-i2m1 11074  ax-1ne0 11075  ax-rrecex 11078  ax-cnre 11079

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-ne 2929  df-ral 3048  df-rex 3057  df-rab 3396  df-v 3438  df-dif 3900  df-un 3902  df-ss 3914  df-nul 4281  df-if 4473  df-sn 4574  df-pr 4576  df-op 4580  df-uni 4857  df-br 5090  df-iota 6437  df-fv 6489  df-ov 7349  df-2 12188  df-3 12189  df-4 12190

This theorem is referenced by:  5re  12212  5pos  12234  2lt4  12295  1lt4  12296  4lt5  12297  3lt5  12298  2lt5  12299  1lt5  12300  4lt6  12302  3lt6  12303  4lt7  12308  3lt7  12309  4lt8  12315  3lt8  12316  4lt9  12323  3lt9  12324  div4p1lem1div2  12376  4lt10  12724  3lt10  12725  uzuzle24  12783  uzuzle34  12784  fz0to4untppr  13530  fzo0to42pr  13653  fldiv4p1lem1div2  13739  fldiv4lem1div2uz2  13740  fldiv4lem1div2  13741  iexpcyc  14114  discr  14147  faclbnd2  14198  4bc2eq6  14236  sqrt2gt1lt2  15181  amgm2  15277  bpoly4  15966  ef01bndlem  16093  sin01bnd  16094  cos01bnd  16095  cos2bnd  16097  flodddiv4  16326  flodddiv4t2lthalf  16329  4sqlem12  16868  tsetndxnstarvndx  17263  slotsdifplendx  17279  slotsdifdsndx  17298  slotsdifunifndx  17305  pcoass  24951  csbren  25326  minveclem2  25353  uniioombllem5  25515  dveflem  25910  pilem2  26389  pilem3  26390  sinhalfpilem  26399  sincosq1lem  26433  tangtx  26441  sincos4thpi  26449  log2cnv  26881  ppiublem1  27140  chtublem  27149  bposlem2  27223  bposlem6  27227  bposlem7  27228  bposlem8  27229  bposlem9  27230  gausslemma2dlem0d  27297  gausslemma2dlem3  27306  gausslemma2dlem4  27307  gausslemma2dlem5  27309  2lgslem1a2  27328  2lgslem1  27332  2lgslem2  27333  2sqlem11  27367  chebbnd1lem2  27408  chebbnd1lem3  27409  chebbnd1  27410  pntibndlem1  27527  pntlemb  27535  pntlemg  27536  pntlemr  27540  pntlemf  27543  usgrexmplef  29237  upgr4cycl4dv4e  30165  ex-id  30414  ex-1st  30424  ex-2nd  30425  dipcj  30694  minvecolem2  30855  minvecolem3  30856  normlem6  31095  lnophmlem2  31997  cos9thpiminplylem1  33795  sqsscirc1  33921  hgt750lemd  34661  hgt750lem  34664  hgt750lem2  34665  hgt750leme  34671  problem2  35710  problem3  35711  iccioo01  37371  lcmineqlem21  42152  lcmineqlem23  42154  3lexlogpow2ineq2  42162  aks4d1p1p7  42177  aks4d1p1p5  42178  4rp  42403  limclner  45759  stoweidlem13  46121  stoweidlem26  46134  stoweidlem34  46142  stoweid  46171  stirlinglem12  46193  stirlinglem13  46194  sinnpoly  47001  modm1p1ne  47480  fmtno4prmfac  47682  lighneallem4a  47718  requad01  47731  requad1  47732  requad2  47733  341fppr2  47844  4fppr1  47845  9fppr8  47847  gbowgt5  47872  sbgoldbwt  47887  sbgoldbst  47888  sbgoldbaltlem1  47889  sbgoldbalt  47891  sgoldbeven3prm  47893  nnsum4primes4  47899  nnsum4primesprm  47901  nnsum4primesgbe  47903  nnsum3primesle9  47904  nnsum4primesle9  47905  nnsum4primeseven  47910  nnsum4primesevenALTV  47911  wtgoldbnnsum4prm  47912  bgoldbnnsum3prm  47914  bgoldbtbndlem2  47916  bgoldbtbndlem3  47917  bgoldbtbnd  47919  tgblthelfgott  47925  usgrexmpl1lem  48131  usgrexmpl2lem  48136  usgrexmpl2nb4  48145  usgrexmpl2nb5  48146  usgrexmpl2trifr  48147  gpg5nbgr3star  48191  pgnbgreunbgrlem2lem3  48226  ackval42  48807  itsclc0yqsollem2  48874  itscnhlinecirc02plem1  48893  2p2ne5  49909