Theorem nn0red 9630

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

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

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 4251  ax-cnex 8276  ax-resscn 8277  ax-1re 8279  ax-addrcl 8282  ax-rnegex 8294

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 9314  df-n0 9575

This theorem is used by:  nn0cnd  9631  nn0readdcl  9635  eluzmn  9943  nn01to3  10032  xnn0dcle  10220  flqmulnn0  10754  modifeq2int  10843  modaddmodup  10844  modaddmodlo  10845  modsumfzodifsn  10853  expnegap0  11004  nn0leexp2  11169  nn0le2msqd  11178  nn0opthlem2d  11180  nn0opthd  11181  faclbnd6  11203  bcval5  11222  filtinf  11251  sshashneg  11302  hashf1  11308  zfz1isolemiso  11312  wrdlenge2n0  11361  ccatsymb  11391  ccatrn  11398  ccatalpha  11402  ccat2s1fvwd  11436  swrdspsleq  11460  pfxsuffeqwrdeq  11491  swrdccat3blem  11532  mertenslemi1  12326  efcllemp  12449  eftlub  12481  oddge22np1  12672  nn0oddm1d2  12700  bitsfzolem  12745  bitsfzo  12746  bitsmod  12747  gcdaddm  12785  bezoutlemsup  12810  gcdzeq  12823  dvdssqlem  12831  nninfctlemfo  12841  nn0seqcvgd  12843  lcmneg  12876  mulgcddvds  12896  qredeu  12899  pwbdvdseulemle  12970  pwbdvdseu  12971  nn0sqrtelqelz  13010  nonsq  13011  pythagtriplem3  13074  pythagtriplem6  13077  pythagtriplem7  13078  pclemub  13094  pcprendvds  13097  pcpremul  13100  pcidlem  13130  pcgcd1  13135  pc2dvds  13137  pcz  13139  pcprmpw2  13140  fldivp1  13155  pcfaclem  13156  pcfac  13157  pcbc  13158  4sqexercise1  13205  4sqexercise2  13206  4sqlemsdc  13207  4sqlem11  13208  4sqlem12  13209  4sqlem14  13211  ennnfoneleminc  13359  ennnfonelemkh  13360  ennnfonelemex  13362  ennnfonelemim  13372  psrbaglesuppg  15170  psrbagcon  15174  psrbaglefifi  15175  psrbagmaxlem1  15178  psrbagmaxlem1x  15181  psrbagmaxlem1y  15182  plyaddlem1  15990  log2tlbndlog2  16237  birthdaylem2  16243  birthdaylem3  16244  ppiqp1le  16284  ppiqltx  16298  sgmppw  16303  ppiqub  16310  chtublem  16312  bcmono  16321  bcmax  16322  bcp1ctr  16323  bclbnd  16324  bposlem5  16332  gausslemma2dlem0h  16397  gausslemma2dlem4  16405  gausslemma2dlem6  16408  lgseisenlem1  16411  2lgsoddprmlem2  16447  2sqlem7  16462  2sqlem8  16464  vtxdgfifival  16754  vtxdgfif  16756  vtxd0nedgbfi  16762  eupth2lemsfi  16941