Theorem nn0re 9453

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

Syntax hints:   → wi 4   ∈ wcel 2202  ℝcr 8074  ℕ₀cn0 9444

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 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2213  ax-sep 4212  ax-cnex 8166  ax-resscn 8167  ax-1re 8169  ax-addrcl 8172  ax-rnegex 8184

This theorem depends on definitions:  df-bi 117  df-tru 1401  df-nf 1510  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2364  df-ral 2516  df-rex 2517  df-v 2805  df-un 3205  df-in 3207  df-ss 3214  df-sn 3679  df-int 3934  df-inn 9186  df-n0 9445

This theorem is referenced by:  nn0nlt0  9470  nn0le0eq0  9472  nn0p1gt0  9473  elnnnn0c  9489  nn0addge1  9490  nn0addge2  9491  nn0ge2m1nn  9506  nn0nndivcl  9508  xnn0xr  9514  nn0nepnf  9517  xnn0nemnf  9520  elnn0z  9536  elznn0nn  9537  ltsubnn0  9591  nn0negleid  9592  difgtsumgt  9593  nn0lt10b  9604  nn0ge0div  9611  xnn0lenn0nn0  10144  xnn0xadd0  10146  nn0fz0  10399  elfz0fzfz0  10406  fz0fzelfz0  10407  fz0fzdiffz0  10410  fzctr  10413  difelfzle  10414  difelfznle  10415  fzoun  10463  nn0p1elfzo  10467  elfzo0le  10470  fzonmapblen  10472  fzofzim  10473  elincfzoext  10484  elfzodifsumelfzo  10492  fzonn0p1  10502  fzonn0p1p1  10504  elfzom1p1elfzo  10505  ubmelm1fzo  10517  fvinim0ffz  10533  subfzo0  10534  adddivflid  10598  divfl0  10602  flltdivnn0lt  10610  addmodid  10680  modfzo0difsn  10703  inftonninf  10750  bernneq  10968  bernneq3  10970  facwordi  11048  faclbnd  11049  faclbnd3  11051  faclbnd6  11052  facubnd  11053  facavg  11054  bcval4  11060  bcval5  11071  bcpasc  11074  fihashneq0  11102  ccat0  11222  ccat2s1fvwd  11273  swrdsbslen  11296  swrdswrdlem  11334  swrdswrd  11335  swrdccatin1  11355  pfxccatin12lem2  11361  pfxccatin12lem3  11362  pfxccat3  11364  swrdccat  11365  swrdccat3blem  11369  nn0maxcl  11848  dvdseq  12472  oddge22np1  12505  nn0ehalf  12527  nn0o  12531  nn0oddm1d2  12533  bitsfi  12581  gcdn0gt0  12612  nn0gcdid0  12615  absmulgcd  12651  nn0seqcvgd  12676  algcvgblem  12684  algcvga  12686  lcmgcdnn  12717  prmfac1  12787  nonsq  12842  hashgcdlem  12873  odzdvds  12881  pcdvdsb  12956  pcidlem  12959  difsqpwdvds  12974  pcfaclem  12985  lgsdinn0  15850  2lgslem1c  15892  clwwlknonex2lem2  16362  eupth2lemsfi  16402  eupth2fi  16403