Theorem 4re 12246

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 12227	. 2 ⊢ 4 = (3 + 1)
2		3re 12242	. . 3 ⊢ 3 ∈ ℝ
3		1re 11150	. . 3 ⊢ 1 ∈ ℝ
4	2, 3	readdcli 11165	. 2 ⊢ (3 + 1) ∈ ℝ
5	1, 4	eqeltri 2824	1 ⊢ 4 ∈ ℝ

Syntax hints:   ∈ wcel 2109  (class class class)co 7369  ℝcr 11043  1c1 11045   + caddc 11047  3c3 12218  4c4 12219

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-1cn 11102  ax-icn 11103  ax-addcl 11104  ax-addrcl 11105  ax-mulcl 11106  ax-mulrcl 11107  ax-i2m1 11112  ax-1ne0 11113  ax-rrecex 11116  ax-cnre 11117

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ne 2926  df-ral 3045  df-rex 3054  df-rab 3403  df-v 3446  df-dif 3914  df-un 3916  df-ss 3928  df-nul 4293  df-if 4485  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4868  df-br 5103  df-iota 6452  df-fv 6507  df-ov 7372  df-2 12225  df-3 12226  df-4 12227

This theorem is referenced by:  5re  12249  5pos  12271  2lt4  12332  1lt4  12333  4lt5  12334  3lt5  12335  2lt5  12336  1lt5  12337  4lt6  12339  3lt6  12340  4lt7  12345  3lt7  12346  4lt8  12352  3lt8  12353  4lt9  12360  3lt9  12361  div4p1lem1div2  12413  4lt10  12761  3lt10  12762  uzuzle24  12820  uzuzle34  12821  fz0to4untppr  13567  fzo0to42pr  13690  fldiv4p1lem1div2  13773  fldiv4lem1div2uz2  13774  fldiv4lem1div2  13775  iexpcyc  14148  discr  14181  faclbnd2  14232  4bc2eq6  14270  sqrt2gt1lt2  15216  amgm2  15312  bpoly4  16001  ef01bndlem  16128  sin01bnd  16129  cos01bnd  16130  cos2bnd  16132  flodddiv4  16361  flodddiv4t2lthalf  16364  4sqlem12  16903  tsetndxnstarvndx  17298  slotsdifplendx  17314  slotsdifdsndx  17333  slotsdifunifndx  17340  pcoass  24900  csbren  25275  minveclem2  25302  uniioombllem5  25464  dveflem  25859  pilem2  26338  pilem3  26339  sinhalfpilem  26348  sincosq1lem  26382  tangtx  26390  sincos4thpi  26398  log2cnv  26830  ppiublem1  27089  chtublem  27098  bposlem2  27172  bposlem6  27176  bposlem7  27177  bposlem8  27178  bposlem9  27179  gausslemma2dlem0d  27246  gausslemma2dlem3  27255  gausslemma2dlem4  27256  gausslemma2dlem5  27258  2lgslem1a2  27277  2lgslem1  27281  2lgslem2  27282  2sqlem11  27316  chebbnd1lem2  27357  chebbnd1lem3  27358  chebbnd1  27359  pntibndlem1  27476  pntlemb  27484  pntlemg  27485  pntlemr  27489  pntlemf  27492  usgrexmplef  29162  upgr4cycl4dv4e  30087  ex-id  30336  ex-1st  30346  ex-2nd  30347  dipcj  30616  minvecolem2  30777  minvecolem3  30778  normlem6  31017  lnophmlem2  31919  cos9thpiminplylem1  33745  sqsscirc1  33871  hgt750lemd  34612  hgt750lem  34615  hgt750lem2  34616  hgt750leme  34622  problem2  35626  problem3  35627  iccioo01  37288  lcmineqlem21  42010  lcmineqlem23  42012  3lexlogpow2ineq2  42020  aks4d1p1p7  42035  aks4d1p1p5  42036  4rp  42261  limclner  45622  stoweidlem13  45984  stoweidlem26  45997  stoweidlem34  46005  stoweid  46034  stirlinglem12  46056  stirlinglem13  46057  sinnpoly  46865  modm1p1ne  47344  fmtno4prmfac  47546  lighneallem4a  47582  requad01  47595  requad1  47596  requad2  47597  341fppr2  47708  4fppr1  47709  9fppr8  47711  gbowgt5  47736  sbgoldbwt  47751  sbgoldbst  47752  sbgoldbaltlem1  47753  sbgoldbalt  47755  sgoldbeven3prm  47757  nnsum4primes4  47763  nnsum4primesprm  47765  nnsum4primesgbe  47767  nnsum3primesle9  47768  nnsum4primesle9  47769  nnsum4primeseven  47774  nnsum4primesevenALTV  47775  wtgoldbnnsum4prm  47776  bgoldbnnsum3prm  47778  bgoldbtbndlem2  47780  bgoldbtbndlem3  47781  bgoldbtbnd  47783  tgblthelfgott  47789  usgrexmpl1lem  47985  usgrexmpl2lem  47990  usgrexmpl2nb4  47999  usgrexmpl2nb5  48000  usgrexmpl2trifr  48001  gpg5nbgr3star  48045  pgnbgreunbgrlem2lem3  48079  ackval42  48658  itsclc0yqsollem2  48725  itscnhlinecirc02plem1  48744  2p2ne5  49760