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

Theorem 4re 10944
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 10928 . 2 4 = (3 + 1)
2 3re 10941 . . 3 3 ∈ ℝ
3 1re 9895 . . 3 1 ∈ ℝ
42, 3readdcli 9909 . 2 (3 + 1) ∈ ℝ
51, 4eqeltri 2683 1 4 ∈ ℝ
Colors of variables: wff setvar class
Syntax hints:  wcel 1976  (class class class)co 6527  cr 9791  1c1 9793   + caddc 9795  3c3 10918  4c4 10919
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-10 2005  ax-11 2020  ax-12 2033  ax-13 2233  ax-ext 2589  ax-1cn 9850  ax-icn 9851  ax-addcl 9852  ax-addrcl 9853  ax-mulcl 9854  ax-mulrcl 9855  ax-i2m1 9860  ax-1ne0 9861  ax-rrecex 9864  ax-cnre 9865
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-clab 2596  df-cleq 2602  df-clel 2605  df-nfc 2739  df-ne 2781  df-ral 2900  df-rex 2901  df-rab 2904  df-v 3174  df-dif 3542  df-un 3544  df-in 3546  df-ss 3553  df-nul 3874  df-if 4036  df-sn 4125  df-pr 4127  df-op 4131  df-uni 4367  df-br 4578  df-iota 5754  df-fv 5798  df-ov 6530  df-2 10926  df-3 10927  df-4 10928
This theorem is referenced by:  4cn  10945  5re  10946  4ne0  10964  5pos  10965  2lt4  11045  1lt4  11046  4lt5  11047  3lt5  11048  2lt5  11049  1lt5  11050  4lt6  11052  3lt6  11053  4lt7  11058  3lt7  11059  4lt8  11065  3lt8  11066  4lt9  11073  3lt9  11074  4lt10OLD  11082  3lt10OLD  11083  div4p1lem1div2  11134  4lt10  11510  3lt10  11511  fz0to4untppr  12266  fzo0to42pr  12377  fldiv4p1lem1div2  12453  fldiv4lem1div2uz2  12454  fldiv4lem1div2  12455  iexpcyc  12786  discr  12818  faclbnd2  12895  4bc2eq6  12933  sqrt2gt1lt2  13809  amgm2  13903  bpoly4  14575  ef01bndlem  14699  sin01bnd  14700  cos01bnd  14701  cos2bnd  14703  flodddiv4  14921  flodddiv4t2lthalf  14924  4sqlem12  15444  pcoass  22563  csbren  22907  minveclem2  22922  uniioombllem5  23078  dveflem  23463  pilem2  23927  pilem3  23928  sinhalfpilem  23936  sincosq1lem  23970  tangtx  23978  sincos4thpi  23986  log2cnv  24388  ppiublem1  24644  chtublem  24653  bposlem2  24727  bposlem6  24731  bposlem7  24732  bposlem8  24733  bposlem9  24734  gausslemma2dlem0d  24801  gausslemma2dlem3  24810  gausslemma2dlem4  24811  gausslemma2dlem5  24813  2lgslem1a2  24832  2lgslem1  24836  2lgslem2  24837  2sqlem11  24871  chebbnd1lem2  24876  chebbnd1lem3  24877  chebbnd1  24878  pntibndlem1  24995  pntlemb  25003  pntlemg  25004  pntlemr  25008  pntlemf  25011  usgraex0elv  25690  usgraex1elv  25691  usgraex2elv  25692  usgraex3elv  25693  4cycl4v4e  25960  4cycl4dv4e  25962  ex-id  26449  ex-1st  26459  ex-2nd  26460  dipcj  26757  minvecolem2  26921  minvecolem3  26922  normlem6  27162  lnophmlem2  28066  sqsscirc1  29088  problem2  30619  problem2OLD  30620  problem3  30621  limclner  38515  stoweidlem13  38703  stoweidlem26  38716  stoweidlem34  38724  stoweid  38753  stirlinglem12  38775  stirlinglem13  38776  fmtno4prmfac  39820  lighneallem4a  39861  gbogt5  39982  bgoldbwt  39997  bgoldbst  39998  sgoldbaltlem1  39999  sgoldbalt  40001  nnsum4primes4  40003  nnsum4primesprm  40005  nnsum4primesgbe  40007  nnsum3primesle9  40008  nnsum4primesle9  40009  nnsum4primeseven  40014  nnsum4primesevenALTV  40015  wtgoldbnnsum4prm  40016  bgoldbnnsum3prm  40018  bgoldbtbndlem2  40020  bgoldbtbndlem3  40021  bgoldbtbnd  40023  tgblthelfgott  40027  tgblthelfgottOLD  40034  upgr4cycl4dv4e  41347  2p2ne5  42309
  Copyright terms: Public domain W3C validator