Theorem 4re 12256

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 12237	. 2 ⊢ 4 = (3 + 1)
2		3re 12252	. . 3 ⊢ 3 ∈ ℝ
3		1re 11135	. . 3 ⊢ 1 ∈ ℝ
4	2, 3	readdcli 11151	. 2 ⊢ (3 + 1) ∈ ℝ
5	1, 4	eqeltri 2835	1 ⊢ 4 ∈ ℝ

Syntax hints:   ∈ wcel 2119  (class class class)co 7356  ℝcr 11028  1c1 11030   + caddc 11032  3c3 12228  4c4 12229

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711  ax-1cn 11087  ax-icn 11088  ax-addcl 11089  ax-addrcl 11090  ax-mulcl 11091  ax-mulrcl 11092  ax-i2m1 11097  ax-1ne0 11098  ax-rrecex 11101  ax-cnre 11102

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-ne 2935  df-ral 3054  df-rex 3064  df-rab 3392  df-v 3433  df-dif 3886  df-un 3888  df-ss 3900  df-nul 4262  df-if 4455  df-sn 4556  df-pr 4558  df-op 4562  df-uni 4839  df-br 5073  df-iota 6441  df-fv 6493  df-ov 7359  df-2 12235  df-3 12236  df-4 12237

This theorem is referenced by:  5re  12259  5pos  12281  2lt4  12342  1lt4  12343  4lt5  12344  3lt5  12345  2lt5  12346  1lt5  12347  4lt6  12349  3lt6  12350  4lt7  12355  3lt7  12356  4lt8  12362  3lt8  12363  4lt9  12370  3lt9  12371  div4p1lem1div2  12423  4lt10  12771  3lt10  12772  uzuzle24  12826  uzuzle34  12827  fz0to4untppr  13575  fzo0to42pr  13699  fldiv4p1lem1div2  13785  fldiv4lem1div2uz2  13786  fldiv4lem1div2  13787  iexpcyc  14160  discr  14193  faclbnd2  14244  4bc2eq6  14282  sqrt2gt1lt2  15227  amgm2  15323  bpoly4  16015  ef01bndlem  16142  sin01bnd  16143  cos01bnd  16144  cos2bnd  16146  flodddiv4  16375  flodddiv4t2lthalf  16378  4sqlem12  16918  tsetndxnstarvndx  17313  slotsdifplendx  17329  slotsdifdsndx  17348  slotsdifunifndx  17355  pcoass  25009  csbren  25384  minveclem2  25411  uniioombllem5  25572  dveflem  25964  pilem2  26435  pilem3  26436  sinhalfpilem  26445  sincosq1lem  26479  tangtx  26487  sincos4thpi  26495  log2cnv  26926  ppiublem1  27183  chtublem  27192  bposlem2  27266  bposlem6  27270  bposlem7  27271  bposlem8  27272  bposlem9  27273  gausslemma2dlem0d  27340  gausslemma2dlem3  27349  gausslemma2dlem4  27350  gausslemma2dlem5  27352  2lgslem1a2  27371  2lgslem1  27375  2lgslem2  27376  2sqlem11  27410  chebbnd1lem2  27451  chebbnd1lem3  27452  chebbnd1  27453  pntibndlem1  27570  pntlemb  27578  pntlemg  27579  pntlemr  27583  pntlemf  27586  usgrexmplef  29346  upgr4cycl4dv4e  30273  ex-id  30522  ex-1st  30532  ex-2nd  30533  dipcj  30803  minvecolem2  30964  minvecolem3  30965  normlem6  31204  lnophmlem2  32106  cos9thpiminplylem1  33966  sqsscirc1  34092  hgt750lemd  34832  hgt750lem  34835  hgt750lem2  34836  hgt750leme  34842  problem2  35894  problem3  35895  iccioo01  37689  lcmineqlem21  42534  lcmineqlem23  42536  3lexlogpow2ineq2  42544  aks4d1p1p7  42559  aks4d1p1p5  42560  4rp  42777  limclner  46094  stoweidlem13  46456  stoweidlem26  46469  stoweidlem34  46477  stoweid  46506  stirlinglem12  46528  stirlinglem13  46529  sinnpoly  47354  modm1p1ne  47839  fmtno4prmfac  48050  lighneallem4a  48086  nprmdvdsfacm1lem2  48099  nprmdvdsfacm1lem4  48101  nprmdvdsfacm1  48102  requad01  48112  requad1  48113  requad2  48114  341fppr2  48225  4fppr1  48226  9fppr8  48228  gbowgt5  48253  sbgoldbwt  48268  sbgoldbst  48269  sbgoldbaltlem1  48270  sbgoldbalt  48272  sgoldbeven3prm  48274  nnsum4primes4  48280  nnsum4primesprm  48282  nnsum4primesgbe  48284  nnsum3primesle9  48285  nnsum4primesle9  48286  nnsum4primeseven  48291  nnsum4primesevenALTV  48292  wtgoldbnnsum4prm  48293  bgoldbnnsum3prm  48295  bgoldbtbndlem2  48297  bgoldbtbndlem3  48298  bgoldbtbnd  48300  tgblthelfgott  48306  usgrexmpl1lem  48512  usgrexmpl2lem  48517  usgrexmpl2nb4  48526  usgrexmpl2nb5  48527  usgrexmpl2trifr  48528  gpg5nbgr3star  48572  pgnbgreunbgrlem2lem3  48607  ackval42  49187  itsclc0yqsollem2  49254  itscnhlinecirc02plem1  49273  2p2ne5  50288