Theorem nn0red 9439

Description: A nonnegative integer is a real number. (Contributed by Mario Carneiro, 27-May-2016.)

Hypothesis

Ref	Expression
nn0red.1	⊢ (𝜑 → 𝐴 ∈ ℕ0)

Assertion

Ref	Expression
nn0red	⊢ (𝜑 → 𝐴 ∈ ℝ)

Proof of Theorem nn0red

Step	Hyp	Ref	Expression
1		nn0ssre 9389	. 2 ⊢ ℕ0 ⊆ ℝ
2		nn0red.1	. 2 ⊢ (𝜑 → 𝐴 ∈ ℕ0)
3	1, 2	sselid 3222	1 ⊢ (𝜑 → 𝐴 ∈ ℝ)

Syntax hints:   → wi 4   ∈ wcel 2200  ℝcr 8014  ℕ₀cn0 9385

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 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211  ax-sep 4202  ax-cnex 8106  ax-resscn 8107  ax-1re 8109  ax-addrcl 8112  ax-rnegex 8124

This theorem depends on definitions:  df-bi 117  df-tru 1398  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-ral 2513  df-rex 2514  df-v 2801  df-un 3201  df-in 3203  df-ss 3210  df-sn 3672  df-int 3924  df-inn 9127  df-n0 9386

This theorem is referenced by:  nn0cnd  9440  nn0readdcl  9444  eluzmn  9745  nn01to3  9829  xnn0dcle  10015  flqmulnn0  10536  modifeq2int  10625  modaddmodup  10626  modaddmodlo  10627  modsumfzodifsn  10635  expnegap0  10786  nn0leexp2  10949  nn0le2msqd  10958  nn0opthlem2d  10960  nn0opthd  10961  faclbnd6  10983  bcval5  11002  filtinf  11030  zfz1isolemiso  11079  wrdlenge2n0  11125  ccatsymb  11155  ccatrn  11162  ccatalpha  11166  swrdspsleq  11220  pfxsuffeqwrdeq  11251  swrdccat3blem  11292  mertenslemi1  12067  efcllemp  12190  eftlub  12222  oddge22np1  12413  nn0oddm1d2  12441  bitsfzolem  12486  bitsfzo  12487  bitsmod  12488  gcdaddm  12526  bezoutlemsup  12551  gcdzeq  12564  dvdssqlem  12572  nninfctlemfo  12582  nn0seqcvgd  12584  lcmneg  12617  mulgcddvds  12637  qredeu  12640  pw2dvdseulemle  12710  pw2dvdseu  12711  nn0sqrtelqelz  12749  nonsq  12750  pythagtriplem3  12811  pythagtriplem6  12814  pythagtriplem7  12815  pclemub  12831  pcprendvds  12834  pcpremul  12837  pcidlem  12867  pcgcd1  12872  pc2dvds  12874  pcz  12876  pcprmpw2  12877  fldivp1  12892  pcfaclem  12893  pcfac  12894  pcbc  12895  4sqexercise1  12942  4sqexercise2  12943  4sqlemsdc  12944  4sqlem11  12945  4sqlem12  12946  4sqlem14  12948  ennnfoneleminc  13003  ennnfonelemkh  13004  ennnfonelemex  13006  ennnfonelemim  13016  psrbaglesuppg  14657  mplsubgfilemcl  14684  plyaddlem1  15442  sgmppw  15687  gausslemma2dlem0h  15756  gausslemma2dlem4  15764  gausslemma2dlem6  15767  lgseisenlem1  15770  2lgsoddprmlem2  15806  2sqlem7  15821  2sqlem8  15823  vtxdgfifival  16077  vtxdgfif  16079  vtxd0nedgbfi  16085