MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  4re Structured version   Visualization version   GIF version

Theorem 4re 11713
Description: The number 4 is real. (Contributed by NM, 27-May-1999.)
Assertion
Ref Expression
4re 4 ∈ ℝ

Proof of Theorem 4re
StepHypRef Expression
1 df-4 11694 . 2 4 = (3 + 1)
2 3re 11709 . . 3 3 ∈ ℝ
3 1re 10634 . . 3 1 ∈ ℝ
42, 3readdcli 10649 . 2 (3 + 1) ∈ ℝ
51, 4eqeltri 2889 1 4 ∈ ℝ
Colors of variables: wff setvar class
Syntax hints:  wcel 2112  (class class class)co 7139  cr 10529  1c1 10531   + caddc 10533  3c3 11685  4c4 11686
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2114  ax-9 2122  ax-ext 2773  ax-1cn 10588  ax-icn 10589  ax-addcl 10590  ax-addrcl 10591  ax-mulcl 10592  ax-mulrcl 10593  ax-i2m1 10598  ax-1ne0 10599  ax-rrecex 10602  ax-cnre 10603
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-ex 1782  df-sb 2070  df-clab 2780  df-cleq 2794  df-clel 2873  df-ne 2991  df-ral 3114  df-rex 3115  df-v 3446  df-un 3889  df-in 3891  df-ss 3901  df-sn 4529  df-pr 4531  df-op 4535  df-uni 4804  df-br 5034  df-iota 6287  df-fv 6336  df-ov 7142  df-2 11692  df-3 11693  df-4 11694
This theorem is referenced by:  5re  11716  4ne0  11737  5pos  11738  2lt4  11804  1lt4  11805  4lt5  11806  3lt5  11807  2lt5  11808  1lt5  11809  4lt6  11811  3lt6  11812  4lt7  11817  3lt7  11818  4lt8  11824  3lt8  11825  4lt9  11832  3lt9  11833  div4p1lem1div2  11884  4lt10  12226  3lt10  12227  eluz4eluz2  12277  fz0to4untppr  13009  fzo0to42pr  13123  fldiv4p1lem1div2  13204  fldiv4lem1div2uz2  13205  fldiv4lem1div2  13206  iexpcyc  13569  discr  13601  faclbnd2  13651  4bc2eq6  13689  sqrt2gt1lt2  14629  amgm2  14724  bpoly4  15408  ef01bndlem  15532  sin01bnd  15533  cos01bnd  15534  cos2bnd  15536  flodddiv4  15757  flodddiv4t2lthalf  15760  4sqlem12  16285  cnfldfun  20106  pcoass  23632  csbren  24006  minveclem2  24033  uniioombllem5  24194  dveflem  24585  pilem2  25050  pilem3  25051  sinhalfpilem  25059  sincosq1lem  25093  tangtx  25101  sincos4thpi  25109  log2cnv  25533  ppiublem1  25789  chtublem  25798  bposlem2  25872  bposlem6  25876  bposlem7  25877  bposlem8  25878  bposlem9  25879  gausslemma2dlem0d  25946  gausslemma2dlem3  25955  gausslemma2dlem4  25956  gausslemma2dlem5  25958  2lgslem1a2  25977  2lgslem1  25981  2lgslem2  25982  2sqlem11  26016  chebbnd1lem2  26057  chebbnd1lem3  26058  chebbnd1  26059  pntibndlem1  26176  pntlemb  26184  pntlemg  26185  pntlemr  26189  pntlemf  26192  usgrexmplef  27052  upgr4cycl4dv4e  27973  ex-id  28222  ex-1st  28232  ex-2nd  28233  dipcj  28500  minvecolem2  28661  minvecolem3  28662  normlem6  28901  lnophmlem2  29803  sqsscirc1  31259  hgt750lemd  32027  hgt750lem  32030  hgt750lem2  32031  hgt750leme  32037  problem2  33017  problem3  33018  iccioo01  34736  lcmineqlem21  39330  lcmineqlem23  39332  3lexlogpow5ineq1  39334  limclner  42280  stoweidlem13  42642  stoweidlem26  42655  stoweidlem34  42663  stoweid  42692  stirlinglem12  42714  stirlinglem13  42715  fmtno4prmfac  44076  lighneallem4a  44113  requad01  44126  requad1  44127  requad2  44128  341fppr2  44239  4fppr1  44240  9fppr8  44242  gbowgt5  44267  sbgoldbwt  44282  sbgoldbst  44283  sbgoldbaltlem1  44284  sbgoldbalt  44286  sgoldbeven3prm  44288  nnsum4primes4  44294  nnsum4primesprm  44296  nnsum4primesgbe  44298  nnsum3primesle9  44299  nnsum4primesle9  44300  nnsum4primeseven  44305  nnsum4primesevenALTV  44306  wtgoldbnnsum4prm  44307  bgoldbnnsum3prm  44309  bgoldbtbndlem2  44311  bgoldbtbndlem3  44312  bgoldbtbnd  44314  tgblthelfgott  44320  ackval42  45097  itsclc0yqsollem2  45164  itscnhlinecirc02plem1  45183  2p2ne5  45313
  Copyright terms: Public domain W3C validator