Theorem 6re 11101

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 11083	. 2 ⊢ 6 = (5 + 1)
2		5re 11099	. . 3 ⊢ 5 ∈ ℝ
3		1re 10039	. . 3 ⊢ 1 ∈ ℝ
4	2, 3	readdcli 10053	. 2 ⊢ (5 + 1) ∈ ℝ
5	1, 4	eqeltri 2697	1 ⊢ 6 ∈ ℝ

Syntax hints:   ∈ wcel 1990  (class class class)co 6650  ℝcr 9935  1c1 9937   + caddc 9939  5c5 11073  6c6 11074

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-1cn 9994  ax-icn 9995  ax-addcl 9996  ax-addrcl 9997  ax-mulcl 9998  ax-mulrcl 9999  ax-i2m1 10004  ax-1ne0 10005  ax-rrecex 10008  ax-cnre 10009

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-ral 2917  df-rex 2918  df-rab 2921  df-v 3202  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-sn 4178  df-pr 4180  df-op 4184  df-uni 4437  df-br 4654  df-iota 5851  df-fv 5896  df-ov 6653  df-2 11079  df-3 11080  df-4 11081  df-5 11082  df-6 11083

This theorem is referenced by:  6cn  11102  7re  11103  7pos  11120  4lt6  11205  3lt6  11206  2lt6  11207  1lt6  11208  6lt7  11209  5lt7  11210  6lt8  11216  5lt8  11217  6lt9  11224  5lt9  11225  6lt10OLD  11233  5lt10OLD  11234  8th4div3  11252  halfpm6th  11253  div4p1lem1div2  11287  6lt10  11676  5lt10  11677  5recm6rec  11686  bpoly2  14788  bpoly3  14789  efi4p  14867  resin4p  14868  recos4p  14869  ef01bndlem  14914  sin01bnd  14915  cos01bnd  14916  lt6abl  18296  sralem  19177  sravsca  19182  zlmlem  19865  sincos6thpi  24267  basellem5  24811  basellem8  24814  basellem9  24815  ppiublem1  24927  ppiublem2  24928  ppiub  24929  chtub  24937  bposlem6  25014  bposlem8  25016  ex-res  27298  zlmds  30008  zlmtset  30009  hgt750lemd  30726  hgt750lem2  30730  hgt750leme  30736  problem4  31562  problem5  31563  pigt3  33402  gbegt5  41649  gbowgt5  41650  gbowge7  41651  gboge9  41652  sbgoldbwt  41665  sgoldbeven3prm  41671  mogoldbb  41673  sbgoldbo  41675  nnsum3primesle9  41682  nnsum4primesodd  41684  wtgoldbnnsum4prm  41690  bgoldbnnsum3prm  41692  pgrple2abl  42146