Theorem 4re 12377

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 12358	. 2 ⊢ 4 = (3 + 1)
2		3re 12373	. . 3 ⊢ 3 ∈ ℝ
3		1re 11290	. . 3 ⊢ 1 ∈ ℝ
4	2, 3	readdcli 11305	. 2 ⊢ (3 + 1) ∈ ℝ
5	1, 4	eqeltri 2840	1 ⊢ 4 ∈ ℝ

Syntax hints:   ∈ wcel 2108  (class class class)co 7448  ℝcr 11183  1c1 11185   + caddc 11187  3c3 12349  4c4 12350

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711  ax-1cn 11242  ax-icn 11243  ax-addcl 11244  ax-addrcl 11245  ax-mulcl 11246  ax-mulrcl 11247  ax-i2m1 11252  ax-1ne0 11253  ax-rrecex 11256  ax-cnre 11257

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-ne 2947  df-ral 3068  df-rex 3077  df-rab 3444  df-v 3490  df-dif 3979  df-un 3981  df-ss 3993  df-nul 4353  df-if 4549  df-sn 4649  df-pr 4651  df-op 4655  df-uni 4932  df-br 5167  df-iota 6525  df-fv 6581  df-ov 7451  df-2 12356  df-3 12357  df-4 12358

This theorem is referenced by:  5re  12380  4ne0  12401  5pos  12402  2lt4  12468  1lt4  12469  4lt5  12470  3lt5  12471  2lt5  12472  1lt5  12473  4lt6  12475  3lt6  12476  4lt7  12481  3lt7  12482  4lt8  12488  3lt8  12489  4lt9  12496  3lt9  12497  div4p1lem1div2  12548  4lt10  12894  3lt10  12895  eluz4eluz2  12950  fz0to4untppr  13687  fzo0to42pr  13803  fldiv4p1lem1div2  13886  fldiv4lem1div2uz2  13887  fldiv4lem1div2  13888  iexpcyc  14256  discr  14289  faclbnd2  14340  4bc2eq6  14378  sqrt2gt1lt2  15323  amgm2  15418  bpoly4  16107  ef01bndlem  16232  sin01bnd  16233  cos01bnd  16234  cos2bnd  16236  flodddiv4  16461  flodddiv4t2lthalf  16464  4sqlem12  17003  tsetndxnstarvndx  17418  slotsdifplendx  17434  slotsdifdsndx  17453  slotsdifunifndx  17460  cnfldfunALTOLDOLD  21416  pcoass  25076  csbren  25452  minveclem2  25479  uniioombllem5  25641  dveflem  26037  pilem2  26514  pilem3  26515  sinhalfpilem  26523  sincosq1lem  26557  tangtx  26565  sincos4thpi  26573  log2cnv  27005  ppiublem1  27264  chtublem  27273  bposlem2  27347  bposlem6  27351  bposlem7  27352  bposlem8  27353  bposlem9  27354  gausslemma2dlem0d  27421  gausslemma2dlem3  27430  gausslemma2dlem4  27431  gausslemma2dlem5  27433  2lgslem1a2  27452  2lgslem1  27456  2lgslem2  27457  2sqlem11  27491  chebbnd1lem2  27532  chebbnd1lem3  27533  chebbnd1  27534  pntibndlem1  27651  pntlemb  27659  pntlemg  27660  pntlemr  27664  pntlemf  27667  usgrexmplef  29294  upgr4cycl4dv4e  30217  ex-id  30466  ex-1st  30476  ex-2nd  30477  dipcj  30746  minvecolem2  30907  minvecolem3  30908  normlem6  31147  lnophmlem2  32049  sqsscirc1  33854  hgt750lemd  34625  hgt750lem  34628  hgt750lem2  34629  hgt750leme  34635  problem2  35634  problem3  35635  iccioo01  37293  lcmineqlem21  42006  lcmineqlem23  42008  3lexlogpow2ineq2  42016  aks4d1p1p7  42031  aks4d1p1p5  42032  4rp  42287  limclner  45572  stoweidlem13  45934  stoweidlem26  45947  stoweidlem34  45955  stoweid  45984  stirlinglem12  46006  stirlinglem13  46007  fmtno4prmfac  47446  lighneallem4a  47482  requad01  47495  requad1  47496  requad2  47497  341fppr2  47608  4fppr1  47609  9fppr8  47611  gbowgt5  47636  sbgoldbwt  47651  sbgoldbst  47652  sbgoldbaltlem1  47653  sbgoldbalt  47655  sgoldbeven3prm  47657  nnsum4primes4  47663  nnsum4primesprm  47665  nnsum4primesgbe  47667  nnsum3primesle9  47668  nnsum4primesle9  47669  nnsum4primeseven  47674  nnsum4primesevenALTV  47675  wtgoldbnnsum4prm  47676  bgoldbnnsum3prm  47678  bgoldbtbndlem2  47680  bgoldbtbndlem3  47681  bgoldbtbnd  47683  tgblthelfgott  47689  usgrexmpl1lem  47836  usgrexmpl2lem  47841  usgrexmpl2nb4  47850  usgrexmpl2nb5  47851  usgrexmpl2trifr  47852  ackval42  48430  itsclc0yqsollem2  48497  itscnhlinecirc02plem1  48516  2p2ne5  48892