Theorem 5re 12353

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 12332	. 2 ⊢ 5 = (4 + 1)
2		4re 12350	. . 3 ⊢ 4 ∈ ℝ
3		1re 11261	. . 3 ⊢ 1 ∈ ℝ
4	2, 3	readdcli 11276	. 2 ⊢ (4 + 1) ∈ ℝ
5	1, 4	eqeltri 2837	1 ⊢ 5 ∈ ℝ

Syntax hints:   ∈ wcel 2108  (class class class)co 7431  ℝcr 11154  1c1 11156   + caddc 11158  4c4 12323  5c5 12324

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 2007  ax-8 2110  ax-9 2118  ax-ext 2708  ax-1cn 11213  ax-icn 11214  ax-addcl 11215  ax-addrcl 11216  ax-mulcl 11217  ax-mulrcl 11218  ax-i2m1 11223  ax-1ne0 11224  ax-rrecex 11227  ax-cnre 11228

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-ne 2941  df-ral 3062  df-rex 3071  df-rab 3437  df-v 3482  df-dif 3954  df-un 3956  df-ss 3968  df-nul 4334  df-if 4526  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-br 5144  df-iota 6514  df-fv 6569  df-ov 7434  df-2 12329  df-3 12330  df-4 12331  df-5 12332

This theorem is referenced by:  6re  12356  6pos  12376  3lt5  12444  2lt5  12445  1lt5  12446  5lt6  12447  4lt6  12448  5lt7  12453  4lt7  12454  5lt8  12460  4lt8  12461  5lt9  12468  4lt9  12469  5lt10  12868  4lt10  12869  5recm6rec  12877  5eluz3  12927  5rp  13041  fz0to5un2tp  13671  ef01bndlem  16220  prm23ge5  16853  prmlem1  17145  vscandxnscandx  17368  slotsdifipndx  17379  slotstnscsi  17404  plendxnscandx  17417  slotsdnscsi  17436  sralemOLD  21176  srascaOLD  21184  zlmlemOLD  21528  ppiublem1  27246  ppiub  27248  bposlem3  27330  bposlem4  27331  bposlem5  27332  bposlem6  27333  bposlem8  27335  bposlem9  27336  lgsdir2lem1  27369  gausslemma2dlem4  27413  2lgslem3  27448  cchhllemOLD  28902  ex-id  30453  ex-sqrt  30473  threehalves  32897  cyc3conja  33177  resvvscaOLD  33364  zlmdsOLD  33962  zlmtsetOLD  33964  hgt750lem2  34667  hgt750leme  34673  problem2  35671  12gcd5e1  42004  lcmineqlem23  42052  3lexlogpow2ineq1  42059  3lexlogpow2ineq2  42060  aks4d1p1p4  42072  aks4d1p1p6  42074  aks4d1p1p7  42075  aks4d1p1p5  42076  stoweidlem13  46028  ceil5half3  47342  31prm  47584  gbegt5  47748  gbowgt5  47749  sbgoldbo  47774  nnsum3primesle9  47781  nnsum4primesodd  47783  evengpop3  47785  usgrexmpl1lem  47980  usgrexmpl2lem  47985  usgrexmpl2nb4  47994  usgrexmpl2nb5  47995  gpg5nbgrvtx13starlem2  48028  gpg5nbgr3star  48037