Theorem nn0red 9571

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

Syntax hints:   → wi 4   ∈ wcel 2205  ℝcr 8142  ℕ₀cn0 9513

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 2216  ax-sep 4233  ax-cnex 8234  ax-resscn 8235  ax-1re 8237  ax-addrcl 8240  ax-rnegex 8252

This theorem depends on definitions:  df-bi 117  df-tru 1401  df-nf 1510  df-sb 1812  df-clab 2221  df-cleq 2227  df-clel 2230  df-nfc 2375  df-ral 2527  df-rex 2528  df-v 2817  df-un 3218  df-in 3220  df-ss 3227  df-sn 3700  df-int 3955  df-inn 9255  df-n0 9514

This theorem is referenced by:  nn0cnd  9572  nn0readdcl  9576  eluzmn  9878  nn01to3  9967  xnn0dcle  10154  flqmulnn0  10683  modifeq2int  10772  modaddmodup  10773  modaddmodlo  10774  modsumfzodifsn  10782  expnegap0  10933  nn0leexp2  11097  nn0le2msqd  11106  nn0opthlem2d  11108  nn0opthd  11109  faclbnd6  11131  bcval5  11150  filtinf  11179  sshashneg  11230  zfz1isolemiso  11236  wrdlenge2n0  11285  ccatsymb  11315  ccatrn  11322  ccatalpha  11326  ccat2s1fvwd  11360  swrdspsleq  11384  pfxsuffeqwrdeq  11415  swrdccat3blem  11456  mertenslemi1  12246  efcllemp  12369  eftlub  12401  oddge22np1  12592  nn0oddm1d2  12620  bitsfzolem  12665  bitsfzo  12666  bitsmod  12667  gcdaddm  12705  bezoutlemsup  12730  gcdzeq  12743  dvdssqlem  12751  nninfctlemfo  12761  nn0seqcvgd  12763  lcmneg  12796  mulgcddvds  12816  qredeu  12819  pw2dvdseulemle  12889  pw2dvdseu  12890  nn0sqrtelqelz  12928  nonsq  12929  pythagtriplem3  12990  pythagtriplem6  12993  pythagtriplem7  12994  pclemub  13010  pcprendvds  13013  pcpremul  13016  pcidlem  13046  pcgcd1  13051  pc2dvds  13053  pcz  13055  pcprmpw2  13056  fldivp1  13071  pcfaclem  13072  pcfac  13073  pcbc  13074  4sqexercise1  13121  4sqexercise2  13122  4sqlemsdc  13123  4sqlem11  13124  4sqlem12  13125  4sqlem14  13127  ennnfoneleminc  13246  ennnfonelemkh  13247  ennnfonelemex  13249  ennnfonelemim  13259  psrbaglesuppg  14933  psrbagcon  14938  mplsubgfilemcl  14966  plyaddlem1  15724  sgmppw  15972  gausslemma2dlem0h  16041  gausslemma2dlem4  16049  gausslemma2dlem6  16052  lgseisenlem1  16055  2lgsoddprmlem2  16091  2sqlem7  16106  2sqlem8  16108  vtxdgfifival  16398  vtxdgfif  16400  vtxd0nedgbfi  16406  eupth2lemsfi  16585