Theorem nn0re 9411

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

Syntax hints:   → wi 4   ∈ wcel 2202  ℝcr 8031  ℕ₀cn0 9402

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 716  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-10 1553  ax-11 1554  ax-i12 1555  ax-bndl 1557  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-ext 2213  ax-sep 4207  ax-cnex 8123  ax-resscn 8124  ax-1re 8126  ax-addrcl 8129  ax-rnegex 8141

This theorem depends on definitions:  df-bi 117  df-tru 1400  df-nf 1509  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2363  df-ral 2515  df-rex 2516  df-v 2804  df-un 3204  df-in 3206  df-ss 3213  df-sn 3675  df-int 3929  df-inn 9144  df-n0 9403

This theorem is referenced by:  nn0nlt0  9428  nn0le0eq0  9430  nn0p1gt0  9431  elnnnn0c  9447  nn0addge1  9448  nn0addge2  9449  nn0ge2m1nn  9462  nn0nndivcl  9464  xnn0xr  9470  nn0nepnf  9473  xnn0nemnf  9476  elnn0z  9492  elznn0nn  9493  ltsubnn0  9547  nn0negleid  9548  difgtsumgt  9549  nn0lt10b  9560  nn0ge0div  9567  xnn0lenn0nn0  10100  xnn0xadd0  10102  nn0fz0  10354  elfz0fzfz0  10361  fz0fzelfz0  10362  fz0fzdiffz0  10365  fzctr  10368  difelfzle  10369  difelfznle  10370  fzoun  10418  nn0p1elfzo  10422  elfzo0le  10425  fzonmapblen  10427  fzofzim  10428  elincfzoext  10439  elfzodifsumelfzo  10447  fzonn0p1  10457  fzonn0p1p1  10459  elfzom1p1elfzo  10460  ubmelm1fzo  10472  fvinim0ffz  10488  subfzo0  10489  adddivflid  10553  divfl0  10557  flltdivnn0lt  10565  addmodid  10635  modfzo0difsn  10658  inftonninf  10705  bernneq  10923  bernneq3  10925  facwordi  11003  faclbnd  11004  faclbnd3  11006  faclbnd6  11007  facubnd  11008  facavg  11009  bcval4  11015  bcval5  11026  bcpasc  11029  fihashneq0  11057  ccat0  11177  ccat2s1fvwd  11228  swrdsbslen  11251  swrdswrdlem  11289  swrdswrd  11290  swrdccatin1  11310  pfxccatin12lem2  11316  pfxccatin12lem3  11317  pfxccat3  11319  swrdccat  11320  swrdccat3blem  11324  nn0maxcl  11790  dvdseq  12414  oddge22np1  12447  nn0ehalf  12469  nn0o  12473  nn0oddm1d2  12475  bitsfi  12523  gcdn0gt0  12554  nn0gcdid0  12557  absmulgcd  12593  nn0seqcvgd  12618  algcvgblem  12626  algcvga  12628  lcmgcdnn  12659  prmfac1  12729  nonsq  12784  hashgcdlem  12815  odzdvds  12823  pcdvdsb  12898  pcidlem  12901  difsqpwdvds  12916  pcfaclem  12927  lgsdinn0  15783  2lgslem1c  15825  clwwlknonex2lem2  16295  eupth2lemsfi  16335  eupth2fi  16336