Theorem 5re 12323

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

Assertion

Ref	Expression
5re	⊢ 5 ∈ ℝ

Proof of Theorem 5re

Step	Hyp	Ref	Expression
1		df-5 12301	. 2 ⊢ 5 = (4 + 1)
2		4re 12320	. . 3 ⊢ 4 ∈ ℝ
3		1re 11203	. . 3 ⊢ 1 ∈ ℝ
4	2, 3	readdcli 11219	. 2 ⊢ (4 + 1) ∈ ℝ
5	1, 4	eqeltri 2859	1 ⊢ 5 ∈ ℝ

Syntax hints:   ∈ wcel 2143  (class class class)co 7410  ℝcr 11094  1c1 11096   + caddc 11098  4c4 12292  5c5 12293

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735  ax-1cn 11153  ax-icn 11154  ax-addcl 11155  ax-addrcl 11156  ax-mulcl 11157  ax-mulrcl 11158  ax-i2m1 11163  ax-1ne0 11164  ax-rrecex 11167  ax-cnre 11168

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-ne 2959  df-ral 3080  df-rex 3090  df-rab 3417  df-v 3457  df-dif 3908  df-un 3910  df-ss 3922  df-nul 4287  df-if 4488  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4873  df-br 5110  df-iota 6492  df-fv 6544  df-ov 7413  df-2 12298  df-3 12299  df-4 12300  df-5 12301

This theorem is referenced by:  6re  12326  3lt5  12416  2lt5  12417  1lt5  12418  5lt6  12419  4lt6  12420  5lt7  12425  4lt7  12426  5lt8  12432  4lt8  12433  5lt9  12440  4lt9  12441  5lt10  12847  5recm6rec  12856  5eluz3  12902  5rp  13018  fz0to5un2tp  13655  ef01bndlem  16235  prm23ge5  16870  prmlem1  17162  vscandxnscandx  17372  slotsdifipndx  17383  slotstnscsi  17408  plendxnscandx  17421  slotsdnscsi  17440  ppiublem1  27366  ppiub  27368  bposlem3  27450  bposlem4  27451  bposlem5  27452  bposlem6  27453  bposlem8  27455  bposlem9  27456  lgsdir2lem1  27489  gausslemma2dlem4  27533  2lgslem3  27568  ex-id  30785  ex-sqrt  30805  threehalves  33234  cyc3conja  33477  hgt750lem2  35039  hgt750leme  35045  problem2  36158  12gcd5e1  42790  lcmineqlem23  42838  3lexlogpow2ineq1  42845  3lexlogpow2ineq2  42846  aks4d1p1p4  42858  aks4d1p1p6  42860  aks4d1p1p7  42861  aks4d1p1p5  42862  stoweidlem13  46747  goldrarr  47638  goldrasin  47639  goldrapos  47640  goldracos5teq  47642  ceil5half3  48103  modm2nep1  48129  modp2nep1  48130  modm1nep2  48131  modm1nem2  48132  modm1p1ne  48133  31prm  48369  gbegt5  48546  gbowgt5  48547  sbgoldbo  48572  nnsum3primesle9  48579  nnsum4primesodd  48581  evengpop3  48583  usgrexmpl1lem  48806  usgrexmpl2lem  48811  usgrexmpl2nb4  48820  usgrexmpl2nb5  48821  gpg5nbgrvtx13starlem2  48857  gpg5nbgr3star  48866  gpg5edgnedg  48915