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

Theorem 4re 11289
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 11273 . 2 4 = (3 + 1)
2 3re 11286 . . 3 3 ∈ ℝ
3 1re 10231 . . 3 1 ∈ ℝ
42, 3readdcli 10245 . 2 (3 + 1) ∈ ℝ
51, 4eqeltri 2835 1 4 ∈ ℝ
Colors of variables: wff setvar class
Syntax hints:  wcel 2139  (class class class)co 6813  cr 10127  1c1 10129   + caddc 10131  3c3 11263  4c4 11264
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740  ax-1cn 10186  ax-icn 10187  ax-addcl 10188  ax-addrcl 10189  ax-mulcl 10190  ax-mulrcl 10191  ax-i2m1 10196  ax-1ne0 10197  ax-rrecex 10200  ax-cnre 10201
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1074  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-ne 2933  df-ral 3055  df-rex 3056  df-rab 3059  df-v 3342  df-dif 3718  df-un 3720  df-in 3722  df-ss 3729  df-nul 4059  df-if 4231  df-sn 4322  df-pr 4324  df-op 4328  df-uni 4589  df-br 4805  df-iota 6012  df-fv 6057  df-ov 6816  df-2 11271  df-3 11272  df-4 11273
This theorem is referenced by:  4cn  11290  5re  11291  4ne0  11309  5pos  11310  2lt4  11390  1lt4  11391  4lt5  11392  3lt5  11393  2lt5  11394  1lt5  11395  4lt6  11397  3lt6  11398  4lt7  11403  3lt7  11404  4lt8  11410  3lt8  11411  4lt9  11418  3lt9  11419  4lt10OLD  11427  3lt10OLD  11428  div4p1lem1div2  11479  4lt10  11870  3lt10  11871  fz0to4untppr  12636  fzo0to42pr  12749  fldiv4p1lem1div2  12830  fldiv4lem1div2uz2  12831  fldiv4lem1div2  12832  iexpcyc  13163  discr  13195  faclbnd2  13272  4bc2eq6  13310  sqrt2gt1lt2  14214  amgm2  14308  bpoly4  14989  ef01bndlem  15113  sin01bnd  15114  cos01bnd  15115  cos2bnd  15117  flodddiv4  15339  flodddiv4t2lthalf  15342  4sqlem12  15862  cnfldfun  19960  pcoass  23024  csbren  23382  minveclem2  23397  uniioombllem5  23555  dveflem  23941  pilem2  24405  pilem3  24406  sinhalfpilem  24414  sincosq1lem  24448  tangtx  24456  sincos4thpi  24464  log2cnv  24870  ppiublem1  25126  chtublem  25135  bposlem2  25209  bposlem6  25213  bposlem7  25214  bposlem8  25215  bposlem9  25216  gausslemma2dlem0d  25283  gausslemma2dlem3  25292  gausslemma2dlem4  25293  gausslemma2dlem5  25295  2lgslem1a2  25314  2lgslem1  25318  2lgslem2  25319  2sqlem11  25353  chebbnd1lem2  25358  chebbnd1lem3  25359  chebbnd1  25360  pntibndlem1  25477  pntlemb  25485  pntlemg  25486  pntlemr  25490  pntlemf  25493  usgrexmplef  26350  upgr4cycl4dv4e  27337  ex-id  27602  ex-1st  27612  ex-2nd  27613  dipcj  27878  minvecolem2  28040  minvecolem3  28041  normlem6  28281  lnophmlem2  29185  sqsscirc1  30263  hgt750lemd  31035  hgt750lem  31038  hgt750lem2  31039  hgt750leme  31045  problem2  31866  problem2OLD  31867  problem3  31868  limclner  40386  stoweidlem13  40733  stoweidlem26  40746  stoweidlem34  40754  stoweid  40783  stirlinglem12  40805  stirlinglem13  40806  fmtno4prmfac  41994  lighneallem4a  42035  gbowgt5  42160  sbgoldbwt  42175  sbgoldbst  42176  sbgoldbaltlem1  42177  sbgoldbalt  42179  sgoldbeven3prm  42181  nnsum4primes4  42187  nnsum4primesprm  42189  nnsum4primesgbe  42191  nnsum3primesle9  42192  nnsum4primesle9  42193  nnsum4primeseven  42198  nnsum4primesevenALTV  42199  wtgoldbnnsum4prm  42200  bgoldbnnsum3prm  42202  bgoldbtbndlem2  42204  bgoldbtbndlem3  42205  bgoldbtbnd  42207  tgblthelfgott  42213  tgblthelfgottOLD  42219  2p2ne5  43057
  Copyright terms: Public domain W3C validator