Theorem 6re 12156

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

Assertion

Ref	Expression
6re	⊢ 6 ∈ ℝ

Proof of Theorem 6re

Step	Hyp	Ref	Expression
1		df-6 12133	. 2 ⊢ 6 = (5 + 1)
2		5re 12153	. . 3 ⊢ 5 ∈ ℝ
3		1re 11068	. . 3 ⊢ 1 ∈ ℝ
4	2, 3	readdcli 11083	. 2 ⊢ (5 + 1) ∈ ℝ
5	1, 4	eqeltri 2833	1 ⊢ 6 ∈ ℝ

Syntax hints:   ∈ wcel 2105  (class class class)co 7329  ℝcr 10963  1c1 10965   + caddc 10967  5c5 12124  6c6 12125

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-ext 2707  ax-1cn 11022  ax-icn 11023  ax-addcl 11024  ax-addrcl 11025  ax-mulcl 11026  ax-mulrcl 11027  ax-i2m1 11032  ax-1ne0 11033  ax-rrecex 11036  ax-cnre 11037

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-sb 2067  df-clab 2714  df-cleq 2728  df-clel 2814  df-ne 2941  df-ral 3062  df-rex 3071  df-rab 3404  df-v 3443  df-dif 3900  df-un 3902  df-in 3904  df-ss 3914  df-nul 4269  df-if 4473  df-sn 4573  df-pr 4575  df-op 4579  df-uni 4852  df-br 5090  df-iota 6425  df-fv 6481  df-ov 7332  df-2 12129  df-3 12130  df-4 12131  df-5 12132  df-6 12133

This theorem is referenced by:  7re  12159  7pos  12177  4lt6  12248  3lt6  12249  2lt6  12250  1lt6  12251  6lt7  12252  5lt7  12253  6lt8  12259  5lt8  12260  6lt9  12267  5lt9  12268  8th4div3  12286  halfpm6th  12287  div4p1lem1div2  12321  6lt10  12664  5lt10  12665  5recm6rec  12674  bpoly2  15858  bpoly3  15859  efi4p  15937  resin4p  15938  recos4p  15939  ef01bndlem  15984  sin01bnd  15985  cos01bnd  15986  slotsdifipndx  17134  slotstnscsi  17159  plendxnvscandx  17173  slotsdnscsi  17191  lt6abl  19583  sralemOLD  20538  sravscaOLD  20548  zlmlemOLD  20817  sincos6thpi  25770  pigt3  25772  basellem5  26332  basellem8  26335  basellem9  26336  ppiublem1  26448  ppiublem2  26449  ppiub  26450  chtub  26458  bposlem6  26535  bposlem8  26537  slotsinbpsd  27032  slotslnbpsd  27033  ex-res  29034  zlmdsOLD  32152  zlmtsetOLD  32154  hgt750lemd  32869  hgt750lem2  32873  hgt750leme  32879  problem4  33866  problem5  33867  gbegt5  45553  gbowgt5  45554  gbowge7  45555  gboge9  45556  sbgoldbwt  45569  sgoldbeven3prm  45575  mogoldbb  45577  sbgoldbo  45579  nnsum3primesle9  45586  nnsum4primesodd  45588  wtgoldbnnsum4prm  45594  bgoldbnnsum3prm  45596  pgrple2abl  46041