Theorem nn0red 9626

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

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

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 8271  ax-resscn 8272  ax-1re 8274  ax-addrcl 8277  ax-rnegex 8289

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 9308  df-n0 9569

This theorem is used by:  nn0cnd  9627  nn0readdcl  9631  eluzmn  9938  nn01to3  10027  xnn0dcle  10215  flqmulnn0  10748  modifeq2int  10837  modaddmodup  10838  modaddmodlo  10839  modsumfzodifsn  10847  expnegap0  10998  nn0leexp2  11163  nn0le2msqd  11172  nn0opthlem2d  11174  nn0opthd  11175  faclbnd6  11197  bcval5  11216  filtinf  11245  sshashneg  11296  hashf1  11302  zfz1isolemiso  11306  wrdlenge2n0  11355  ccatsymb  11385  ccatrn  11392  ccatalpha  11396  ccat2s1fvwd  11430  swrdspsleq  11454  pfxsuffeqwrdeq  11485  swrdccat3blem  11526  mertenslemi1  12320  efcllemp  12443  eftlub  12475  oddge22np1  12666  nn0oddm1d2  12694  bitsfzolem  12739  bitsfzo  12740  bitsmod  12741  gcdaddm  12779  bezoutlemsup  12804  gcdzeq  12817  dvdssqlem  12825  nninfctlemfo  12835  nn0seqcvgd  12837  lcmneg  12870  mulgcddvds  12890  qredeu  12893  pwbdvdseulemle  12964  pwbdvdseu  12965  nn0sqrtelqelz  13004  nonsq  13005  pythagtriplem3  13068  pythagtriplem6  13071  pythagtriplem7  13072  pclemub  13088  pcprendvds  13091  pcpremul  13094  pcidlem  13124  pcgcd1  13129  pc2dvds  13131  pcz  13133  pcprmpw2  13134  fldivp1  13149  pcfaclem  13150  pcfac  13151  pcbc  13152  4sqexercise1  13199  4sqexercise2  13200  4sqlemsdc  13201  4sqlem11  13202  4sqlem12  13203  4sqlem14  13205  ennnfoneleminc  13353  ennnfonelemkh  13354  ennnfonelemex  13356  ennnfonelemim  13366  psrbaglesuppg  15108  psrbagcon  15113  psrbaglefifi  15114  mplsubgfilemcl  15142  plyaddlem1  15900  log2tlbndlog2  16142  birthdaylem2  16148  birthdaylem3  16149  ppiqp1le  16189  ppiqltx  16203  sgmppw  16208  ppiqub  16215  chtublem  16217  bcmono  16226  bcmax  16227  bcp1ctr  16228  bclbnd  16229  bposlem5  16237  gausslemma2dlem0h  16297  gausslemma2dlem4  16305  gausslemma2dlem6  16308  lgseisenlem1  16311  2lgsoddprmlem2  16347  2sqlem7  16362  2sqlem8  16364  vtxdgfifival  16654  vtxdgfif  16656  vtxd0nedgbfi  16662  eupth2lemsfi  16841