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 12302	. 2 ⊢ 5 = (4 + 1)
2		4re 12320	. . 3 ⊢ 4 ∈ ℝ
3		1re 11238	. . 3 ⊢ 1 ∈ ℝ
4	2, 3	readdcli 11253	. 2 ⊢ (4 + 1) ∈ ℝ
5	1, 4	eqeltri 2824	1 ⊢ 5 ∈ ℝ

Syntax hints:   ∈ wcel 2099  (class class class)co 7414  ℝcr 11131  1c1 11133   + caddc 11135  4c4 12293  5c5 12294

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 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2698  ax-1cn 11190  ax-icn 11191  ax-addcl 11192  ax-addrcl 11193  ax-mulcl 11194  ax-mulrcl 11195  ax-i2m1 11200  ax-1ne0 11201  ax-rrecex 11204  ax-cnre 11205

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 847  df-3an 1087  df-tru 1537  df-fal 1547  df-ex 1775  df-sb 2061  df-clab 2705  df-cleq 2719  df-clel 2805  df-ne 2936  df-ral 3057  df-rex 3066  df-rab 3428  df-v 3471  df-dif 3947  df-un 3949  df-in 3951  df-ss 3961  df-nul 4319  df-if 4525  df-sn 4625  df-pr 4627  df-op 4631  df-uni 4904  df-br 5143  df-iota 6494  df-fv 6550  df-ov 7417  df-2 12299  df-3 12300  df-4 12301  df-5 12302

This theorem is referenced by:  6re  12326  6pos  12346  3lt5  12414  2lt5  12415  1lt5  12416  5lt6  12417  4lt6  12418  5lt7  12423  4lt7  12424  5lt8  12430  4lt8  12431  5lt9  12438  4lt9  12439  5lt10  12836  4lt10  12837  5recm6rec  12845  ef01bndlem  16154  prm23ge5  16777  prmlem1  17070  vscandxnscandx  17298  slotsdifipndx  17309  slotstnscsi  17334  plendxnscandx  17347  slotsdnscsi  17366  rmodislmodOLD  20807  sralemOLD  21055  srascaOLD  21063  zlmlemOLD  21436  ppiublem1  27128  ppiub  27130  bposlem3  27212  bposlem4  27213  bposlem5  27214  bposlem6  27215  bposlem8  27217  bposlem9  27218  lgsdir2lem1  27251  gausslemma2dlem4  27295  2lgslem3  27330  cchhllemOLD  28691  ex-id  30237  ex-sqrt  30257  threehalves  32632  cyc3conja  32872  resvvscaOLD  33043  zlmdsOLD  33554  zlmtsetOLD  33556  hgt750lem2  34274  hgt750leme  34280  problem2  35260  12gcd5e1  41463  lcmineqlem23  41511  3lexlogpow2ineq1  41518  3lexlogpow2ineq2  41519  aks4d1p1p4  41531  aks4d1p1p6  41533  aks4d1p1p7  41534  aks4d1p1p5  41535  stoweidlem13  45373  31prm  46909  gbegt5  47073  gbowgt5  47074  sbgoldbo  47099  nnsum3primesle9  47106  nnsum4primesodd  47108  evengpop3  47110