Theorem nn0re 9583

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 9578	. 2 ⊢ ℕ0 ⊆ ℝ
2	1	sseli 3244	1 ⊢ (𝐴 ∈ ℕ0 → 𝐴 ∈ ℝ)

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2209  ℝcr 8184  ℕ₀cn0 9574

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220  ax-sep 4251  ax-cnex 8276  ax-resscn 8277  ax-1re 8279  ax-addrcl 8282  ax-rnegex 8294

This proof depends on definitions:  df-bi 117  df-tru 1405  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-nfc 2381  df-ral 2533  df-rex 2534  df-v 2823  df-un 3224  df-in 3226  df-ss 3233  df-sn 3715  df-int 3971  df-inn 9314  df-n0 9575

This theorem is used by:  nn0nlt0  9600  nn0le0eq0  9602  nn0p1gt0  9603  elnnnn0c  9619  nn0addge1  9620  nn0addge2  9621  nn0ge2m1nn  9636  nn0nndivcl  9638  xnn0xr  9644  nn0nepnf  9647  xnn0nemnf  9650  elnn0z  9666  elznn0nn  9667  ltsubnn0  9721  nn0negleid  9722  difgtsumgt  9723  nn0lt10b  9735  nn0ge0div  9742  xnn0lenn0nn0  10283  xnn0xadd0  10285  nn0fz0  10542  elfz0fzfz0  10549  fz0fzelfz0  10550  fz0fzdiffz0  10553  fzctr  10556  difelfzle  10557  difelfznle  10558  fzoun  10606  nn0p1elfzo  10610  elfzo0le  10613  fzonmapblen  10615  fzofzim  10616  elincfzoext  10627  elfzodifsumelfzo  10635  fzonn0p1  10645  fzonn0p1p1  10647  elfzom1p1elfzo  10648  ubmelm1fzo  10660  fvinim0ffz  10676  subfzo0  10677  adddivflid  10747  divfl0  10751  flltdivnn0lt  10759  addmodid  10829  modfzo0difsn  10852  inftonninf  10899  bernneq  11118  bernneq3  11120  facwordi  11199  faclbnd  11200  faclbnd3  11202  faclbnd6  11203  facubnd  11204  facavg  11205  bcval4  11211  bcval5  11222  bcpasc  11225  fihashneq0  11254  ccat0  11385  ccat2s1fvwd  11436  swrdsbslen  11459  swrdswrdlem  11497  swrdswrd  11498  swrdccatin1  11518  pfxccatin12lem2  11524  pfxccatin12lem3  11525  pfxccat3  11527  swrdccat  11528  swrdccat3blem  11532  nn0maxcl  12013  dvdseq  12639  oddge22np1  12672  nn0ehalf  12694  nn0o  12698  nn0oddm1d2  12700  bitsfi  12748  gcdn0gt0  12779  nn0gcdid0  12782  absmulgcd  12818  nn0seqcvgd  12843  algcvgblem  12851  algcvga  12853  lcmgcdnn  12884  prmfac1  12955  nonsq  13011  sqrtrirr  13013  hashgcdlem  13044  odzdvds  13052  pcdvdsb  13127  pcidlem  13130  difsqpwdvds  13145  pcfaclem  13156  gsumbagdiaglem  15184  psrridmfi  15209  log2tlbndlog2  16237  birthdaylem3  16244  bcmono  16321  bcmax  16322  lgsdinn0  16389  2lgslem1c  16431  clwwlknonex2lem2  16901  eupth2lemsfi  16941  eupth2fi  16942