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

Theorem 4re 11135
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 11119 . 2 4 = (3 + 1)
2 3re 11132 . . 3 3 ∈ ℝ
3 1re 10077 . . 3 1 ∈ ℝ
42, 3readdcli 10091 . 2 (3 + 1) ∈ ℝ
51, 4eqeltri 2726 1 4 ∈ ℝ
Colors of variables: wff setvar class
Syntax hints:  wcel 2030  (class class class)co 6690  cr 9973  1c1 9975   + caddc 9977  3c3 11109  4c4 11110
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-1cn 10032  ax-icn 10033  ax-addcl 10034  ax-addrcl 10035  ax-mulcl 10036  ax-mulrcl 10037  ax-i2m1 10042  ax-1ne0 10043  ax-rrecex 10046  ax-cnre 10047
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ne 2824  df-ral 2946  df-rex 2947  df-rab 2950  df-v 3233  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-nul 3949  df-if 4120  df-sn 4211  df-pr 4213  df-op 4217  df-uni 4469  df-br 4686  df-iota 5889  df-fv 5934  df-ov 6693  df-2 11117  df-3 11118  df-4 11119
This theorem is referenced by:  4cn  11136  5re  11137  4ne0  11155  5pos  11156  2lt4  11236  1lt4  11237  4lt5  11238  3lt5  11239  2lt5  11240  1lt5  11241  4lt6  11243  3lt6  11244  4lt7  11249  3lt7  11250  4lt8  11256  3lt8  11257  4lt9  11264  3lt9  11265  4lt10OLD  11273  3lt10OLD  11274  div4p1lem1div2  11325  4lt10  11716  3lt10  11717  fz0to4untppr  12481  fzo0to42pr  12595  fldiv4p1lem1div2  12676  fldiv4lem1div2uz2  12677  fldiv4lem1div2  12678  iexpcyc  13009  discr  13041  faclbnd2  13118  4bc2eq6  13156  sqrt2gt1lt2  14059  amgm2  14153  bpoly4  14834  ef01bndlem  14958  sin01bnd  14959  cos01bnd  14960  cos2bnd  14962  flodddiv4  15184  flodddiv4t2lthalf  15187  4sqlem12  15707  cnfldfun  19806  pcoass  22870  csbren  23228  minveclem2  23243  uniioombllem5  23401  dveflem  23787  pilem2  24251  pilem3  24252  sinhalfpilem  24260  sincosq1lem  24294  tangtx  24302  sincos4thpi  24310  log2cnv  24716  ppiublem1  24972  chtublem  24981  bposlem2  25055  bposlem6  25059  bposlem7  25060  bposlem8  25061  bposlem9  25062  gausslemma2dlem0d  25129  gausslemma2dlem3  25138  gausslemma2dlem4  25139  gausslemma2dlem5  25141  2lgslem1a2  25160  2lgslem1  25164  2lgslem2  25165  2sqlem11  25199  chebbnd1lem2  25204  chebbnd1lem3  25205  chebbnd1  25206  pntibndlem1  25323  pntlemb  25331  pntlemg  25332  pntlemr  25336  pntlemf  25339  usgrexmplef  26196  upgr4cycl4dv4e  27163  ex-id  27421  ex-1st  27431  ex-2nd  27432  dipcj  27697  minvecolem2  27859  minvecolem3  27860  normlem6  28100  lnophmlem2  29004  sqsscirc1  30082  hgt750lemd  30854  hgt750lem  30857  hgt750lem2  30858  hgt750leme  30864  problem2  31685  problem2OLD  31686  problem3  31687  limclner  40201  stoweidlem13  40548  stoweidlem26  40561  stoweidlem34  40569  stoweid  40598  stirlinglem12  40620  stirlinglem13  40621  fmtno4prmfac  41809  lighneallem4a  41850  gbowgt5  41975  sbgoldbwt  41990  sbgoldbst  41991  sbgoldbaltlem1  41992  sbgoldbalt  41994  sgoldbeven3prm  41996  nnsum4primes4  42002  nnsum4primesprm  42004  nnsum4primesgbe  42006  nnsum3primesle9  42007  nnsum4primesle9  42008  nnsum4primeseven  42013  nnsum4primesevenALTV  42014  wtgoldbnnsum4prm  42015  bgoldbnnsum3prm  42017  bgoldbtbndlem2  42019  bgoldbtbndlem3  42020  bgoldbtbnd  42022  tgblthelfgott  42028  tgblthelfgottOLD  42034  2p2ne5  42872
  Copyright terms: Public domain W3C validator