Theorem nn0red 9632

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  9633  nn0readdcl  9637  eluzmn  9944  nn01to3  10033  xnn0dcle  10221  flqmulnn0  10755  modifeq2int  10844  modaddmodup  10845  modaddmodlo  10846  modsumfzodifsn  10854  expnegap0  11005  nn0leexp2  11170  nn0le2msqd  11179  nn0opthlem2d  11181  nn0opthd  11182  faclbnd6  11204  bcval5  11223  filtinf  11252  sshashneg  11303  hashf1  11309  zfz1isolemiso  11313  wrdlenge2n0  11362  ccatsymb  11392  ccatrn  11399  ccatalpha  11403  ccat2s1fvwd  11437  swrdspsleq  11461  pfxsuffeqwrdeq  11492  swrdccat3blem  11533  mertenslemi1  12327  efcllemp  12450  eftlub  12482  oddge22np1  12673  nn0oddm1d2  12701  bitsfzolem  12746  bitsfzo  12747  bitsmod  12748  gcdaddm  12786  bezoutlemsup  12811  gcdzeq  12824  dvdssqlem  12832  nninfctlemfo  12842  nn0seqcvgd  12844  lcmneg  12877  mulgcddvds  12897  qredeu  12900  pwbdvdseulemle  12971  pwbdvdseu  12972  nn0sqrtelqelz  13011  nonsq  13012  pythagtriplem3  13075  pythagtriplem6  13078  pythagtriplem7  13079  pclemub  13095  pcprendvds  13098  pcpremul  13101  pcidlem  13131  pcgcd1  13136  pc2dvds  13138  pcz  13140  pcprmpw2  13141  fldivp1  13156  pcfaclem  13157  pcfac  13158  pcbc  13159  4sqexercise1  13206  4sqexercise2  13207  4sqlemsdc  13208  4sqlem11  13209  4sqlem12  13210  4sqlem14  13212  ennnfoneleminc  13360  ennnfonelemkh  13361  ennnfonelemex  13363  ennnfonelemim  13373  psrbaglesuppg  15166  psrbagcon  15171  psrbaglefifi  15172  mplsubgfilemcl  15215  plyaddlem1  15973  log2tlbndlog2  16220  birthdaylem2  16226  birthdaylem3  16227  ppiqp1le  16267  ppiqltx  16281  sgmppw  16286  ppiqub  16293  chtublem  16295  bcmono  16304  bcmax  16305  bcp1ctr  16306  bclbnd  16307  bposlem5  16315  gausslemma2dlem0h  16380  gausslemma2dlem4  16388  gausslemma2dlem6  16391  lgseisenlem1  16394  2lgsoddprmlem2  16430  2sqlem7  16445  2sqlem8  16447  vtxdgfifival  16737  vtxdgfif  16739  vtxd0nedgbfi  16745  eupth2lemsfi  16924