Theorem nn0red 9574

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

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

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 9258  df-n0 9517

This theorem is referenced by:  nn0cnd  9575  nn0readdcl  9579  eluzmn  9881  nn01to3  9970  xnn0dcle  10157  flqmulnn0  10686  modifeq2int  10775  modaddmodup  10776  modaddmodlo  10777  modsumfzodifsn  10785  expnegap0  10936  nn0leexp2  11100  nn0le2msqd  11109  nn0opthlem2d  11111  nn0opthd  11112  faclbnd6  11134  bcval5  11153  filtinf  11182  sshashneg  11233  zfz1isolemiso  11239  wrdlenge2n0  11288  ccatsymb  11318  ccatrn  11325  ccatalpha  11329  ccat2s1fvwd  11363  swrdspsleq  11387  pfxsuffeqwrdeq  11418  swrdccat3blem  11459  mertenslemi1  12250  efcllemp  12373  eftlub  12405  oddge22np1  12596  nn0oddm1d2  12624  bitsfzolem  12669  bitsfzo  12670  bitsmod  12671  gcdaddm  12709  bezoutlemsup  12734  gcdzeq  12747  dvdssqlem  12755  nninfctlemfo  12765  nn0seqcvgd  12767  lcmneg  12800  mulgcddvds  12820  qredeu  12823  pw2dvdseulemle  12893  pw2dvdseu  12894  nn0sqrtelqelz  12932  nonsq  12933  pythagtriplem3  12994  pythagtriplem6  12997  pythagtriplem7  12998  pclemub  13014  pcprendvds  13017  pcpremul  13020  pcidlem  13050  pcgcd1  13055  pc2dvds  13057  pcz  13059  pcprmpw2  13060  fldivp1  13075  pcfaclem  13076  pcfac  13077  pcbc  13078  4sqexercise1  13125  4sqexercise2  13126  4sqlemsdc  13127  4sqlem11  13128  4sqlem12  13129  4sqlem14  13131  ennnfoneleminc  13250  ennnfonelemkh  13251  ennnfonelemex  13253  ennnfonelemim  13263  psrbaglesuppg  14951  psrbagcon  14956  mplsubgfilemcl  14984  plyaddlem1  15742  sgmppw  15990  gausslemma2dlem0h  16059  gausslemma2dlem4  16067  gausslemma2dlem6  16070  lgseisenlem1  16073  2lgsoddprmlem2  16109  2sqlem7  16124  2sqlem8  16126  vtxdgfifival  16416  vtxdgfif  16418  vtxd0nedgbfi  16424  eupth2lemsfi  16603