Theorem 4re 12350

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 12330	. 2 ⊢ 4 = (3 + 1)
2		3re 12346	. . 3 ⊢ 3 ∈ ℝ
3		1re 11233	. . 3 ⊢ 1 ∈ ℝ
4	2, 3	readdcli 11249	. 2 ⊢ (3 + 1) ∈ ℝ
5	1, 4	eqeltri 2856	1 ⊢ 4 ∈ ℝ

This proof depends on syntax axioms:   ∈ wcel 2145  (class class class)co 7414  ℝcr 11124  1c1 11126   + caddc 11128  3c3 12321  4c4 12322

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732  ax-1cn 11183  ax-icn 11184  ax-addcl 11185  ax-addrcl 11186  ax-mulcl 11187  ax-mulrcl 11188  ax-i2m1 11193  ax-1ne0 11194  ax-rrecex 11197  ax-cnre 11198

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-ne 2956  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-iota 6489  df-fv 6541  df-ov 7417  df-2 12328  df-3 12329  df-4 12330

This theorem is used by:  5re  12353  2lt4  12443  1lt4  12444  4lt5  12445  3lt5  12446  2lt5  12447  1lt5  12448  4lt6  12450  3lt6  12451  4lt7  12456  3lt7  12457  4lt8  12463  3lt8  12464  4lt9  12471  3lt9  12472  div4p1lem1div2  12524  4lt10  12879  uzuzle24  12935  uzuzle34  12936  fz0to4untppr  13686  fzo0to42pr  13810  fldiv4p1lem1div2  13897  fldiv4lem1div2uz2  13898  fldiv4lem1div2  13899  iexpcyc  14272  discr  14305  faclbnd2  14356  4bc2eq6  14394  sqrt2gt1lt2  15362  amgm2  15458  bpoly4  16146  ef01bndlem  16273  sin01bnd  16274  cos01bnd  16275  cos2bnd  16277  flodddiv4  16506  flodddiv4t2lthalf  16509  4sqlem12  17049  tsetndxnstarvndx  17445  slotsdifplendx  17461  slotsdifdsndx  17480  slotsdifunifndx  17487  pcoass  25253  csbren  25628  minveclem2  25655  uniioombllem5  25816  dveflem  26207  pilem2  26689  pilem3  26690  sinhalfpilem  26702  sincosq1lem  26736  tangtx  26744  sincos4thpi  26752  log2cnv  27182  ppiublem1  27439  chtublem  27448  bposlem2  27522  bposlem6  27526  bposlem7  27527  bposlem8  27528  bposlem9  27529  gausslemma2dlem0d  27596  gausslemma2dlem3  27605  gausslemma2dlem4  27606  gausslemma2dlem5  27608  2lgslem1a2  27627  2lgslem1  27631  2lgslem2  27632  2sqlem11  27666  chebbnd1lem2  27707  chebbnd1lem3  27708  chebbnd1  27709  pntibndlem1  27826  pntlemb  27834  pntlemg  27835  pntlemr  27839  pntlemf  27842  usgrexmplef  29720  upgr4cycl4dv4e  30666  ex-id  30915  ex-1st  30925  ex-2nd  30926  dipcj  31196  minvecolem2  31357  minvecolem3  31358  normlem6  31597  lnophmlem2  32499  cos9thpiminplylem1  34293  sqsscirc1  34419  hgt750lemd  35157  hgt750lem  35160  hgt750lem2  35161  hgt750leme  35167  problem2  36246  problem3  36247  iccioo01  38082  lcmineqlem21  42916  lcmineqlem23  42918  3lexlogpow2ineq2  42926  aks4d1p1p7  42941  aks4d1p1p5  42942  4rp  43176  limclner  46480  stoweidlem13  46842  stoweidlem26  46855  stoweidlem34  46863  stoweid  46892  stirlinglem12  46914  stirlinglem13  46915  sinnpoly  47760  modm1p1ne  48265  fmtno4prmfac  48476  lighneallem4a  48512  nprmdvdsfacm1lem2  48525  nprmdvdsfacm1lem4  48527  nprmdvdsfacm1  48528  requad01  48538  requad1  48539  requad2  48540  341fppr2  48651  4fppr1  48652  9fppr8  48654  gbowgt5  48679  sbgoldbwt  48694  sbgoldbst  48695  sbgoldbaltlem1  48696  sbgoldbalt  48698  sgoldbeven3prm  48700  nnsum4primes4  48706  nnsum4primesprm  48708  nnsum4primesgbe  48710  nnsum3primesle9  48711  nnsum4primesle9  48712  nnsum4primeseven  48717  nnsum4primesevenALTV  48718  wtgoldbnnsum4prm  48719  bgoldbnnsum3prm  48721  bgoldbtbndlem2  48723  bgoldbtbndlem3  48724  bgoldbtbnd  48726  tgblthelfgott  48732  usgrexmpl1lem  48938  usgrexmpl2lem  48943  usgrexmpl2nb4  48952  usgrexmpl2nb5  48953  usgrexmpl2trifr  48954  gpg5nbgr3star  48998  pgnbgreunbgrlem2lem3  49033  ackval42  49627  itsclc0yqsollem2  49694  itscnhlinecirc02plem1  49713  2p2ne5  50770  veronesev4lem  50810  veronesev5lem  50811  veronesev6lem  50812  veronesevrowd  50813  veroquadgsumlem  50817