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

Theorem 4re 10974
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 10958 . 2 4 = (3 + 1)
2 3re 10971 . . 3 3 ∈ ℝ
3 1re 9918 . . 3 1 ∈ ℝ
42, 3readdcli 9932 . 2 (3 + 1) ∈ ℝ
51, 4eqeltri 2684 1 4 ∈ ℝ
Colors of variables: wff setvar class
Syntax hints:  wcel 1977  (class class class)co 6549  cr 9814  1c1 9816   + caddc 9818  3c3 10948  4c4 10949
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-1cn 9873  ax-icn 9874  ax-addcl 9875  ax-addrcl 9876  ax-mulcl 9877  ax-mulrcl 9878  ax-i2m1 9883  ax-1ne0 9884  ax-rrecex 9887  ax-cnre 9888
This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-ral 2901  df-rex 2902  df-rab 2905  df-v 3175  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-sn 4126  df-pr 4128  df-op 4132  df-uni 4373  df-br 4584  df-iota 5768  df-fv 5812  df-ov 6552  df-2 10956  df-3 10957  df-4 10958
This theorem is referenced by:  4cn  10975  5re  10976  4ne0  10994  5pos  10995  2lt4  11075  1lt4  11076  4lt5  11077  3lt5  11078  2lt5  11079  1lt5  11080  4lt6  11082  3lt6  11083  4lt7  11088  3lt7  11089  4lt8  11095  3lt8  11096  4lt9  11103  3lt9  11104  4lt10OLD  11112  3lt10OLD  11113  div4p1lem1div2  11164  4lt10  11554  3lt10  11555  fz0to4untppr  12311  fzo0to42pr  12422  fldiv4p1lem1div2  12498  fldiv4lem1div2uz2  12499  fldiv4lem1div2  12500  iexpcyc  12831  discr  12863  faclbnd2  12940  4bc2eq6  12978  sqrt2gt1lt2  13863  amgm2  13957  bpoly4  14629  ef01bndlem  14753  sin01bnd  14754  cos01bnd  14755  cos2bnd  14757  flodddiv4  14975  flodddiv4t2lthalf  14978  4sqlem12  15498  pcoass  22632  csbren  22990  minveclem2  23005  uniioombllem5  23161  dveflem  23546  pilem2  24010  pilem3  24011  sinhalfpilem  24019  sincosq1lem  24053  tangtx  24061  sincos4thpi  24069  log2cnv  24471  ppiublem1  24727  chtublem  24736  bposlem2  24810  bposlem6  24814  bposlem7  24815  bposlem8  24816  bposlem9  24817  gausslemma2dlem0d  24884  gausslemma2dlem3  24893  gausslemma2dlem4  24894  gausslemma2dlem5  24896  2lgslem1a2  24915  2lgslem1  24919  2lgslem2  24920  2sqlem11  24954  chebbnd1lem2  24959  chebbnd1lem3  24960  chebbnd1  24961  pntibndlem1  25078  pntlemb  25086  pntlemg  25087  pntlemr  25091  pntlemf  25094  usgraex0elv  25924  usgraex1elv  25925  usgraex2elv  25926  usgraex3elv  25927  4cycl4v4e  26194  4cycl4dv4e  26196  ex-id  26683  ex-1st  26693  ex-2nd  26694  dipcj  26953  minvecolem2  27115  minvecolem3  27116  normlem6  27356  lnophmlem2  28260  sqsscirc1  29282  problem2  30813  problem2OLD  30814  problem3  30815  limclner  38718  stoweidlem13  38906  stoweidlem26  38919  stoweidlem34  38927  stoweid  38956  stirlinglem12  38978  stirlinglem13  38979  fmtno4prmfac  40022  lighneallem4a  40063  gbogt5  40184  bgoldbwt  40199  bgoldbst  40200  sgoldbaltlem1  40201  sgoldbalt  40203  nnsum4primes4  40205  nnsum4primesprm  40207  nnsum4primesgbe  40209  nnsum3primesle9  40210  nnsum4primesle9  40211  nnsum4primeseven  40216  nnsum4primesevenALTV  40217  wtgoldbnnsum4prm  40218  bgoldbnnsum3prm  40220  bgoldbtbndlem2  40222  bgoldbtbndlem3  40223  bgoldbtbnd  40225  tgblthelfgott  40229  tgblthelfgottOLD  40236  upgr4cycl4dv4e  41352  2p2ne5  42353
  Copyright terms: Public domain W3C validator