Theorem 4re 12057

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 12038	. 2 ⊢ 4 = (3 + 1)
2		3re 12053	. . 3 ⊢ 3 ∈ ℝ
3		1re 10975	. . 3 ⊢ 1 ∈ ℝ
4	2, 3	readdcli 10990	. 2 ⊢ (3 + 1) ∈ ℝ
5	1, 4	eqeltri 2835	1 ⊢ 4 ∈ ℝ

Syntax hints:   ∈ wcel 2106  (class class class)co 7275  ℝcr 10870  1c1 10872   + caddc 10874  3c3 12029  4c4 12030

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709  ax-1cn 10929  ax-icn 10930  ax-addcl 10931  ax-addrcl 10932  ax-mulcl 10933  ax-mulrcl 10934  ax-i2m1 10939  ax-1ne0 10940  ax-rrecex 10943  ax-cnre 10944

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-ne 2944  df-ral 3069  df-rex 3070  df-rab 3073  df-v 3434  df-dif 3890  df-un 3892  df-in 3894  df-ss 3904  df-nul 4257  df-if 4460  df-sn 4562  df-pr 4564  df-op 4568  df-uni 4840  df-br 5075  df-iota 6391  df-fv 6441  df-ov 7278  df-2 12036  df-3 12037  df-4 12038

This theorem is referenced by:  5re  12060  4ne0  12081  5pos  12082  2lt4  12148  1lt4  12149  4lt5  12150  3lt5  12151  2lt5  12152  1lt5  12153  4lt6  12155  3lt6  12156  4lt7  12161  3lt7  12162  4lt8  12168  3lt8  12169  4lt9  12176  3lt9  12177  div4p1lem1div2  12228  4lt10  12573  3lt10  12574  eluz4eluz2  12625  fz0to4untppr  13359  fzo0to42pr  13474  fldiv4p1lem1div2  13555  fldiv4lem1div2uz2  13556  fldiv4lem1div2  13557  iexpcyc  13923  discr  13955  faclbnd2  14005  4bc2eq6  14043  sqrt2gt1lt2  14986  amgm2  15081  bpoly4  15769  ef01bndlem  15893  sin01bnd  15894  cos01bnd  15895  cos2bnd  15897  flodddiv4  16122  flodddiv4t2lthalf  16125  4sqlem12  16657  tsetndxnstarvndx  17069  slotsdifplendx  17085  slotsdifdsndx  17104  slotsdifunifndx  17111  cnfldfunALTOLD  20611  pcoass  24187  csbren  24563  minveclem2  24590  uniioombllem5  24751  dveflem  25143  pilem2  25611  pilem3  25612  sinhalfpilem  25620  sincosq1lem  25654  tangtx  25662  sincos4thpi  25670  log2cnv  26094  ppiublem1  26350  chtublem  26359  bposlem2  26433  bposlem6  26437  bposlem7  26438  bposlem8  26439  bposlem9  26440  gausslemma2dlem0d  26507  gausslemma2dlem3  26516  gausslemma2dlem4  26517  gausslemma2dlem5  26519  2lgslem1a2  26538  2lgslem1  26542  2lgslem2  26543  2sqlem11  26577  chebbnd1lem2  26618  chebbnd1lem3  26619  chebbnd1  26620  pntibndlem1  26737  pntlemb  26745  pntlemg  26746  pntlemr  26750  pntlemf  26753  usgrexmplef  27626  upgr4cycl4dv4e  28549  ex-id  28798  ex-1st  28808  ex-2nd  28809  dipcj  29076  minvecolem2  29237  minvecolem3  29238  normlem6  29477  lnophmlem2  30379  sqsscirc1  31858  hgt750lemd  32628  hgt750lem  32631  hgt750lem2  32632  hgt750leme  32638  problem2  33624  problem3  33625  iccioo01  35498  lcmineqlem21  40057  lcmineqlem23  40059  3lexlogpow2ineq2  40067  aks4d1p1p7  40082  aks4d1p1p5  40083  limclner  43192  stoweidlem13  43554  stoweidlem26  43567  stoweidlem34  43575  stoweid  43604  stirlinglem12  43626  stirlinglem13  43627  fmtno4prmfac  45024  lighneallem4a  45060  requad01  45073  requad1  45074  requad2  45075  341fppr2  45186  4fppr1  45187  9fppr8  45189  gbowgt5  45214  sbgoldbwt  45229  sbgoldbst  45230  sbgoldbaltlem1  45231  sbgoldbalt  45233  sgoldbeven3prm  45235  nnsum4primes4  45241  nnsum4primesprm  45243  nnsum4primesgbe  45245  nnsum3primesle9  45246  nnsum4primesle9  45247  nnsum4primeseven  45252  nnsum4primesevenALTV  45253  wtgoldbnnsum4prm  45254  bgoldbnnsum3prm  45256  bgoldbtbndlem2  45258  bgoldbtbndlem3  45259  bgoldbtbnd  45261  tgblthelfgott  45267  ackval42  46042  itsclc0yqsollem2  46109  itscnhlinecirc02plem1  46128  2p2ne5  46502