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

Theorem 4re 12237
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 12218 . 2 4 = (3 + 1)
2 3re 12233 . . 3 3 ∈ ℝ
3 1re 11155 . . 3 1 ∈ ℝ
42, 3readdcli 11170 . 2 (3 + 1) ∈ ℝ
51, 4eqeltri 2834 1 4 ∈ ℝ
Colors of variables: wff setvar class
Syntax hints:  wcel 2106  (class class class)co 7357  cr 11050  1c1 11052   + caddc 11054  3c3 12209  4c4 12210
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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2707  ax-1cn 11109  ax-icn 11110  ax-addcl 11111  ax-addrcl 11112  ax-mulcl 11113  ax-mulrcl 11114  ax-i2m1 11119  ax-1ne0 11120  ax-rrecex 11123  ax-cnre 11124
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2714  df-cleq 2728  df-clel 2814  df-ne 2944  df-ral 3065  df-rex 3074  df-rab 3408  df-v 3447  df-dif 3913  df-un 3915  df-in 3917  df-ss 3927  df-nul 4283  df-if 4487  df-sn 4587  df-pr 4589  df-op 4593  df-uni 4866  df-br 5106  df-iota 6448  df-fv 6504  df-ov 7360  df-2 12216  df-3 12217  df-4 12218
This theorem is referenced by:  5re  12240  4ne0  12261  5pos  12262  2lt4  12328  1lt4  12329  4lt5  12330  3lt5  12331  2lt5  12332  1lt5  12333  4lt6  12335  3lt6  12336  4lt7  12341  3lt7  12342  4lt8  12348  3lt8  12349  4lt9  12356  3lt9  12357  div4p1lem1div2  12408  4lt10  12754  3lt10  12755  eluz4eluz2  12810  fz0to4untppr  13544  fzo0to42pr  13659  fldiv4p1lem1div2  13740  fldiv4lem1div2uz2  13741  fldiv4lem1div2  13742  iexpcyc  14111  discr  14143  faclbnd2  14191  4bc2eq6  14229  sqrt2gt1lt2  15159  amgm2  15254  bpoly4  15942  ef01bndlem  16066  sin01bnd  16067  cos01bnd  16068  cos2bnd  16070  flodddiv4  16295  flodddiv4t2lthalf  16298  4sqlem12  16828  tsetndxnstarvndx  17240  slotsdifplendx  17256  slotsdifdsndx  17275  slotsdifunifndx  17282  cnfldfunALTOLD  20810  pcoass  24387  csbren  24763  minveclem2  24790  uniioombllem5  24951  dveflem  25343  pilem2  25811  pilem3  25812  sinhalfpilem  25820  sincosq1lem  25854  tangtx  25862  sincos4thpi  25870  log2cnv  26294  ppiublem1  26550  chtublem  26559  bposlem2  26633  bposlem6  26637  bposlem7  26638  bposlem8  26639  bposlem9  26640  gausslemma2dlem0d  26707  gausslemma2dlem3  26716  gausslemma2dlem4  26717  gausslemma2dlem5  26719  2lgslem1a2  26738  2lgslem1  26742  2lgslem2  26743  2sqlem11  26777  chebbnd1lem2  26818  chebbnd1lem3  26819  chebbnd1  26820  pntibndlem1  26937  pntlemb  26945  pntlemg  26946  pntlemr  26950  pntlemf  26953  usgrexmplef  28207  upgr4cycl4dv4e  29129  ex-id  29378  ex-1st  29388  ex-2nd  29389  dipcj  29656  minvecolem2  29817  minvecolem3  29818  normlem6  30057  lnophmlem2  30959  sqsscirc1  32489  hgt750lemd  33261  hgt750lem  33264  hgt750lem2  33265  hgt750leme  33271  problem2  34254  problem3  34255  iccioo01  35798  lcmineqlem21  40506  lcmineqlem23  40508  3lexlogpow2ineq2  40516  aks4d1p1p7  40531  aks4d1p1p5  40532  limclner  43882  stoweidlem13  44244  stoweidlem26  44257  stoweidlem34  44265  stoweid  44294  stirlinglem12  44316  stirlinglem13  44317  fmtno4prmfac  45754  lighneallem4a  45790  requad01  45803  requad1  45804  requad2  45805  341fppr2  45916  4fppr1  45917  9fppr8  45919  gbowgt5  45944  sbgoldbwt  45959  sbgoldbst  45960  sbgoldbaltlem1  45961  sbgoldbalt  45963  sgoldbeven3prm  45965  nnsum4primes4  45971  nnsum4primesprm  45973  nnsum4primesgbe  45975  nnsum3primesle9  45976  nnsum4primesle9  45977  nnsum4primeseven  45982  nnsum4primesevenALTV  45983  wtgoldbnnsum4prm  45984  bgoldbnnsum3prm  45986  bgoldbtbndlem2  45988  bgoldbtbndlem3  45989  bgoldbtbnd  45991  tgblthelfgott  45997  ackval42  46772  itsclc0yqsollem2  46839  itscnhlinecirc02plem1  46858  2p2ne5  47235
  Copyright terms: Public domain W3C validator