Theorem nn0re 9410

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

Syntax hints:   → wi 4   ∈ wcel 2202  ℝcr 8030  ℕ₀cn0 9401

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 8122  ax-resscn 8123  ax-1re 8125  ax-addrcl 8128  ax-rnegex 8140

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 9143  df-n0 9402

This theorem is referenced by:  nn0nlt0  9427  nn0le0eq0  9429  nn0p1gt0  9430  elnnnn0c  9446  nn0addge1  9447  nn0addge2  9448  nn0ge2m1nn  9461  nn0nndivcl  9463  xnn0xr  9469  nn0nepnf  9472  xnn0nemnf  9475  elnn0z  9491  elznn0nn  9492  ltsubnn0  9546  nn0negleid  9547  difgtsumgt  9548  nn0lt10b  9559  nn0ge0div  9566  xnn0lenn0nn0  10099  xnn0xadd0  10101  nn0fz0  10353  elfz0fzfz0  10360  fz0fzelfz0  10361  fz0fzdiffz0  10364  fzctr  10367  difelfzle  10368  difelfznle  10369  fzoun  10417  elfzo0le  10423  fzonmapblen  10425  fzofzim  10426  elincfzoext  10437  elfzodifsumelfzo  10445  fzonn0p1  10455  fzonn0p1p1  10457  elfzom1p1elfzo  10458  ubmelm1fzo  10470  fvinim0ffz  10486  subfzo0  10487  adddivflid  10551  divfl0  10555  flltdivnn0lt  10563  addmodid  10633  modfzo0difsn  10656  inftonninf  10703  bernneq  10921  bernneq3  10923  facwordi  11001  faclbnd  11002  faclbnd3  11004  faclbnd6  11005  facubnd  11006  facavg  11007  bcval4  11013  bcval5  11024  bcpasc  11027  fihashneq0  11055  ccat0  11172  ccat2s1fvwd  11223  swrdsbslen  11246  swrdswrdlem  11284  swrdswrd  11285  swrdccatin1  11305  pfxccatin12lem2  11311  pfxccatin12lem3  11312  pfxccat3  11314  swrdccat  11315  swrdccat3blem  11319  nn0maxcl  11785  dvdseq  12408  oddge22np1  12441  nn0ehalf  12463  nn0o  12467  nn0oddm1d2  12469  bitsfi  12517  gcdn0gt0  12548  nn0gcdid0  12551  absmulgcd  12587  nn0seqcvgd  12612  algcvgblem  12620  algcvga  12622  lcmgcdnn  12653  prmfac1  12723  nonsq  12778  hashgcdlem  12809  odzdvds  12817  pcdvdsb  12892  pcidlem  12895  difsqpwdvds  12910  pcfaclem  12921  lgsdinn0  15776  2lgslem1c  15818  clwwlknonex2lem2  16288