Theorem nn0re 9334

Description: A nonnegative integer is a real number. (Contributed by NM, 9-May-2004.)

Assertion

Ref	Expression
nn0re	⊢ (𝐴 ∈ ℕ0 → 𝐴 ∈ ℝ)

Proof of Theorem nn0re

Step	Hyp	Ref	Expression
1		nn0ssre 9329	. 2 ⊢ ℕ0 ⊆ ℝ
2	1	sseli 3193	1 ⊢ (𝐴 ∈ ℕ0 → 𝐴 ∈ ℝ)

Syntax hints:   → wi 4   ∈ wcel 2177  ℝcr 7954  ℕ₀cn0 9325

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 711  ax-5 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-10 1529  ax-11 1530  ax-i12 1531  ax-bndl 1533  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-i5r 1559  ax-ext 2188  ax-sep 4173  ax-cnex 8046  ax-resscn 8047  ax-1re 8049  ax-addrcl 8052  ax-rnegex 8064

This theorem depends on definitions:  df-bi 117  df-tru 1376  df-nf 1485  df-sb 1787  df-clab 2193  df-cleq 2199  df-clel 2202  df-nfc 2338  df-ral 2490  df-rex 2491  df-v 2775  df-un 3174  df-in 3176  df-ss 3183  df-sn 3644  df-int 3895  df-inn 9067  df-n0 9326

This theorem is referenced by:  nn0nlt0  9351  nn0le0eq0  9353  nn0p1gt0  9354  elnnnn0c  9370  nn0addge1  9371  nn0addge2  9372  nn0ge2m1nn  9385  nn0nndivcl  9387  xnn0xr  9393  nn0nepnf  9396  xnn0nemnf  9399  elnn0z  9415  elznn0nn  9416  ltsubnn0  9470  nn0negleid  9471  difgtsumgt  9472  nn0lt10b  9483  nn0ge0div  9490  xnn0lenn0nn0  10017  xnn0xadd0  10019  nn0fz0  10271  elfz0fzfz0  10278  fz0fzelfz0  10279  fz0fzdiffz0  10282  fzctr  10285  difelfzle  10286  difelfznle  10287  fzoun  10335  elfzo0le  10341  fzonmapblen  10343  fzofzim  10344  elincfzoext  10354  elfzodifsumelfzo  10362  fzonn0p1  10372  fzonn0p1p1  10374  elfzom1p1elfzo  10375  ubmelm1fzo  10387  fvinim0ffz  10402  subfzo0  10403  adddivflid  10467  divfl0  10471  flltdivnn0lt  10479  addmodid  10549  modfzo0difsn  10572  inftonninf  10619  bernneq  10837  bernneq3  10839  facwordi  10917  faclbnd  10918  faclbnd3  10920  faclbnd6  10921  facubnd  10922  facavg  10923  bcval4  10929  bcval5  10940  bcpasc  10943  fihashneq0  10971  ccat0  11085  swrdsbslen  11152  swrdswrdlem  11190  swrdswrd  11191  nn0maxcl  11621  dvdseq  12244  oddge22np1  12277  nn0ehalf  12299  nn0o  12303  nn0oddm1d2  12305  bitsfi  12353  gcdn0gt0  12384  nn0gcdid0  12387  absmulgcd  12423  nn0seqcvgd  12448  algcvgblem  12456  algcvga  12458  lcmgcdnn  12489  prmfac1  12559  nonsq  12614  hashgcdlem  12645  odzdvds  12653  pcdvdsb  12728  pcidlem  12731  difsqpwdvds  12746  pcfaclem  12757  lgsdinn0  15610  2lgslem1c  15652