Theorem 4re 12320

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 12300	. 2 ⊢ 4 = (3 + 1)
2		3re 12316	. . 3 ⊢ 3 ∈ ℝ
3		1re 11203	. . 3 ⊢ 1 ∈ ℝ
4	2, 3	readdcli 11219	. 2 ⊢ (3 + 1) ∈ ℝ
5	1, 4	eqeltri 2859	1 ⊢ 4 ∈ ℝ

Syntax hints:   ∈ wcel 2143  (class class class)co 7410  ℝcr 11094  1c1 11096   + caddc 11098  3c3 12291  4c4 12292

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735  ax-1cn 11153  ax-icn 11154  ax-addcl 11155  ax-addrcl 11156  ax-mulcl 11157  ax-mulrcl 11158  ax-i2m1 11163  ax-1ne0 11164  ax-rrecex 11167  ax-cnre 11168

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-ne 2959  df-ral 3080  df-rex 3090  df-rab 3417  df-v 3457  df-dif 3908  df-un 3910  df-ss 3922  df-nul 4287  df-if 4488  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4873  df-br 5110  df-iota 6492  df-fv 6544  df-ov 7413  df-2 12298  df-3 12299  df-4 12300

This theorem is referenced by:  5re  12323  2lt4  12413  1lt4  12414  4lt5  12415  3lt5  12416  2lt5  12417  1lt5  12418  4lt6  12420  3lt6  12421  4lt7  12426  3lt7  12427  4lt8  12433  3lt8  12434  4lt9  12441  3lt9  12442  div4p1lem1div2  12494  4lt10  12848  uzuzle24  12904  uzuzle34  12905  fz0to4untppr  13654  fzo0to42pr  13778  fldiv4p1lem1div2  13864  fldiv4lem1div2uz2  13865  fldiv4lem1div2  13866  iexpcyc  14239  discr  14272  faclbnd2  14323  4bc2eq6  14361  sqrt2gt1lt2  15321  amgm2  15417  bpoly4  16108  ef01bndlem  16235  sin01bnd  16236  cos01bnd  16237  cos2bnd  16239  flodddiv4  16468  flodddiv4t2lthalf  16471  4sqlem12  17011  tsetndxnstarvndx  17407  slotsdifplendx  17423  slotsdifdsndx  17442  slotsdifunifndx  17449  pcoass  25183  csbren  25558  minveclem2  25585  uniioombllem5  25746  dveflem  26138  pilem2  26615  pilem3  26616  sinhalfpilem  26628  sincosq1lem  26662  tangtx  26670  sincos4thpi  26678  log2cnv  27109  ppiublem1  27366  chtublem  27375  bposlem2  27449  bposlem6  27453  bposlem7  27454  bposlem8  27455  bposlem9  27456  gausslemma2dlem0d  27523  gausslemma2dlem3  27532  gausslemma2dlem4  27533  gausslemma2dlem5  27535  2lgslem1a2  27554  2lgslem1  27558  2lgslem2  27559  2sqlem11  27593  chebbnd1lem2  27634  chebbnd1lem3  27635  chebbnd1  27636  pntibndlem1  27753  pntlemb  27761  pntlemg  27762  pntlemr  27766  pntlemf  27769  usgrexmplef  29609  upgr4cycl4dv4e  30536  ex-id  30785  ex-1st  30795  ex-2nd  30796  dipcj  31066  minvecolem2  31227  minvecolem3  31228  normlem6  31467  lnophmlem2  32369  cos9thpiminplylem1  34172  sqsscirc1  34298  hgt750lemd  35035  hgt750lem  35038  hgt750lem2  35039  hgt750leme  35045  problem2  36158  problem3  36159  iccioo01  37973  lcmineqlem21  42816  lcmineqlem23  42818  3lexlogpow2ineq2  42826  aks4d1p1p7  42841  aks4d1p1p5  42842  4rp  43061  limclner  46365  stoweidlem13  46727  stoweidlem26  46740  stoweidlem34  46748  stoweid  46777  stirlinglem12  46799  stirlinglem13  46800  sinnpoly  47628  modm1p1ne  48113  fmtno4prmfac  48324  lighneallem4a  48360  nprmdvdsfacm1lem2  48373  nprmdvdsfacm1lem4  48375  nprmdvdsfacm1  48376  requad01  48386  requad1  48387  requad2  48388  341fppr2  48499  4fppr1  48500  9fppr8  48502  gbowgt5  48527  sbgoldbwt  48542  sbgoldbst  48543  sbgoldbaltlem1  48544  sbgoldbalt  48546  sgoldbeven3prm  48548  nnsum4primes4  48554  nnsum4primesprm  48556  nnsum4primesgbe  48558  nnsum3primesle9  48559  nnsum4primesle9  48560  nnsum4primeseven  48565  nnsum4primesevenALTV  48566  wtgoldbnnsum4prm  48567  bgoldbnnsum3prm  48569  bgoldbtbndlem2  48571  bgoldbtbndlem3  48572  bgoldbtbnd  48574  tgblthelfgott  48580  usgrexmpl1lem  48786  usgrexmpl2lem  48791  usgrexmpl2nb4  48800  usgrexmpl2nb5  48801  usgrexmpl2trifr  48802  gpg5nbgr3star  48846  pgnbgreunbgrlem2lem3  48881  ackval42  49476  itsclc0yqsollem2  49543  itscnhlinecirc02plem1  49562  2p2ne5  50618