Theorem nn0red 9623

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 9569	. 2 ⊢ ℕ0 ⊆ ℝ
2		nn0red.1	. 2 ⊢ (𝜑 → 𝐴 ∈ ℕ0)
3	1, 2	sselid 3246	1 ⊢ (𝜑 → 𝐴 ∈ ℝ)

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

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 4249  ax-cnex 8270  ax-resscn 8271  ax-1re 8273  ax-addrcl 8276  ax-rnegex 8288

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 9306  df-n0 9566

This theorem is used by:  nn0cnd  9624  nn0readdcl  9628  eluzmn  9930  nn01to3  10019  xnn0dcle  10206  flqmulnn0  10736  modifeq2int  10825  modaddmodup  10826  modaddmodlo  10827  modsumfzodifsn  10835  expnegap0  10986  nn0leexp2  11150  nn0le2msqd  11159  nn0opthlem2d  11161  nn0opthd  11162  faclbnd6  11184  bcval5  11203  filtinf  11232  sshashneg  11283  hashf1  11289  zfz1isolemiso  11293  wrdlenge2n0  11342  ccatsymb  11372  ccatrn  11379  ccatalpha  11383  ccat2s1fvwd  11417  swrdspsleq  11441  pfxsuffeqwrdeq  11472  swrdccat3blem  11513  mertenslemi1  12304  efcllemp  12427  eftlub  12459  oddge22np1  12650  nn0oddm1d2  12678  bitsfzolem  12723  bitsfzo  12724  bitsmod  12725  gcdaddm  12763  bezoutlemsup  12788  gcdzeq  12801  dvdssqlem  12809  nninfctlemfo  12819  nn0seqcvgd  12821  lcmneg  12854  mulgcddvds  12874  qredeu  12877  pw2dvdseulemle  12947  pw2dvdseu  12948  nn0sqrtelqelz  12986  nonsq  12987  pythagtriplem3  13048  pythagtriplem6  13051  pythagtriplem7  13052  pclemub  13068  pcprendvds  13071  pcpremul  13074  pcidlem  13104  pcgcd1  13109  pc2dvds  13111  pcz  13113  pcprmpw2  13114  fldivp1  13129  pcfaclem  13130  pcfac  13131  pcbc  13132  4sqexercise1  13179  4sqexercise2  13180  4sqlemsdc  13181  4sqlem11  13182  4sqlem12  13183  4sqlem14  13185  ennnfoneleminc  13304  ennnfonelemkh  13305  ennnfonelemex  13307  ennnfonelemim  13317  psrbaglesuppg  15059  psrbagcon  15064  mplsubgfilemcl  15092  plyaddlem1  15850  log2tlbndlog2  16088  birthdaylem2  16094  birthdaylem3  16095  sgmppw  16112  bcmono  16124  bcmax  16125  bcp1ctr  16126  bclbnd  16127  gausslemma2dlem0h  16187  gausslemma2dlem4  16195  gausslemma2dlem6  16198  lgseisenlem1  16201  2lgsoddprmlem2  16237  2sqlem7  16252  2sqlem8  16254  vtxdgfifival  16544  vtxdgfif  16546  vtxd0nedgbfi  16552  eupth2lemsfi  16731