Theorem 4re 11713

Description: The number 4 is real. (Contributed by NM, 27-May-1999.)

Assertion

Ref	Expression
4re	⊢ 4 ∈ ℝ

Proof of Theorem 4re

Step	Hyp	Ref	Expression
1		df-4 11694	. 2 ⊢ 4 = (3 + 1)
2		3re 11709	. . 3 ⊢ 3 ∈ ℝ
3		1re 10633	. . 3 ⊢ 1 ∈ ℝ
4	2, 3	readdcli 10648	. 2 ⊢ (3 + 1) ∈ ℝ
5	1, 4	eqeltri 2907	1 ⊢ 4 ∈ ℝ

Syntax hints:   ∈ wcel 2108  (class class class)co 7148  ℝcr 10528  1c1 10530   + caddc 10532  3c3 11685  4c4 11686

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1905  ax-6 1964  ax-7 2009  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2154  ax-12 2170  ax-ext 2791  ax-1cn 10587  ax-icn 10588  ax-addcl 10589  ax-addrcl 10590  ax-mulcl 10591  ax-mulrcl 10592  ax-i2m1 10597  ax-1ne0 10598  ax-rrecex 10601  ax-cnre 10602

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1084  df-tru 1534  df-ex 1775  df-nf 1779  df-sb 2064  df-clab 2798  df-cleq 2812  df-clel 2891  df-nfc 2961  df-ne 3015  df-ral 3141  df-rex 3142  df-rab 3145  df-v 3495  df-dif 3937  df-un 3939  df-in 3941  df-ss 3950  df-nul 4290  df-if 4466  df-sn 4560  df-pr 4562  df-op 4566  df-uni 4831  df-br 5058  df-iota 6307  df-fv 6356  df-ov 7151  df-2 11692  df-3 11693  df-4 11694

This theorem is referenced by:  5re  11716  4ne0  11737  5pos  11738  2lt4  11804  1lt4  11805  4lt5  11806  3lt5  11807  2lt5  11808  1lt5  11809  4lt6  11811  3lt6  11812  4lt7  11817  3lt7  11818  4lt8  11824  3lt8  11825  4lt9  11832  3lt9  11833  div4p1lem1div2  11884  4lt10  12226  3lt10  12227  eluz4eluz2  12277  fz0to4untppr  13002  fzo0to42pr  13116  fldiv4p1lem1div2  13197  fldiv4lem1div2uz2  13198  fldiv4lem1div2  13199  iexpcyc  13561  discr  13593  faclbnd2  13643  4bc2eq6  13681  sqrt2gt1lt2  14626  amgm2  14721  bpoly4  15405  ef01bndlem  15529  sin01bnd  15530  cos01bnd  15531  cos2bnd  15533  flodddiv4  15756  flodddiv4t2lthalf  15759  4sqlem12  16284  cnfldfun  20549  pcoass  23620  csbren  23994  minveclem2  24021  uniioombllem5  24180  dveflem  24568  pilem2  25032  pilem3  25033  sinhalfpilem  25041  sincosq1lem  25075  tangtx  25083  sincos4thpi  25091  log2cnv  25514  ppiublem1  25770  chtublem  25779  bposlem2  25853  bposlem6  25857  bposlem7  25858  bposlem8  25859  bposlem9  25860  gausslemma2dlem0d  25927  gausslemma2dlem3  25936  gausslemma2dlem4  25937  gausslemma2dlem5  25939  2lgslem1a2  25958  2lgslem1  25962  2lgslem2  25963  2sqlem11  25997  chebbnd1lem2  26038  chebbnd1lem3  26039  chebbnd1  26040  pntibndlem1  26157  pntlemb  26165  pntlemg  26166  pntlemr  26170  pntlemf  26173  usgrexmplef  27033  upgr4cycl4dv4e  27956  ex-id  28205  ex-1st  28215  ex-2nd  28216  dipcj  28483  minvecolem2  28644  minvecolem3  28645  normlem6  28884  lnophmlem2  29786  sqsscirc1  31144  hgt750lemd  31912  hgt750lem  31915  hgt750lem2  31916  hgt750leme  31922  problem2  32902  problem3  32903  limclner  41921  stoweidlem13  42288  stoweidlem26  42301  stoweidlem34  42309  stoweid  42338  stirlinglem12  42360  stirlinglem13  42361  fmtno4prmfac  43724  lighneallem4a  43763  requad01  43776  requad1  43777  requad2  43778  341fppr2  43889  4fppr1  43890  9fppr8  43892  gbowgt5  43917  sbgoldbwt  43932  sbgoldbst  43933  sbgoldbaltlem1  43934  sbgoldbalt  43936  sgoldbeven3prm  43938  nnsum4primes4  43944  nnsum4primesprm  43946  nnsum4primesgbe  43948  nnsum3primesle9  43949  nnsum4primesle9  43950  nnsum4primeseven  43955  nnsum4primesevenALTV  43956  wtgoldbnnsum4prm  43957  bgoldbnnsum3prm  43959  bgoldbtbndlem2  43961  bgoldbtbndlem3  43962  bgoldbtbnd  43964  tgblthelfgott  43970  itsclc0yqsollem2  44740  itscnhlinecirc02plem1  44759  2p2ne5  44889