Theorem nn0red 9232

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

Syntax hints:   → wi 4   ∈ wcel 2148  ℝcr 7812  ℕ₀cn0 9178

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 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159  ax-sep 4123  ax-cnex 7904  ax-resscn 7905  ax-1re 7907  ax-addrcl 7910  ax-rnegex 7922

This theorem depends on definitions:  df-bi 117  df-tru 1356  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-ral 2460  df-rex 2461  df-v 2741  df-un 3135  df-in 3137  df-ss 3144  df-sn 3600  df-int 3847  df-inn 8922  df-n0 9179

This theorem is referenced by:  nn0cnd  9233  nn0readdcl  9237  nn01to3  9619  xnn0dcle  9804  flqmulnn0  10301  modifeq2int  10388  modaddmodup  10389  modaddmodlo  10390  modsumfzodifsn  10398  expnegap0  10530  nn0leexp2  10692  nn0le2msqd  10701  nn0opthlem2d  10703  nn0opthd  10704  faclbnd6  10726  bcval5  10745  filtinf  10773  zfz1isolemiso  10821  mertenslemi1  11545  efcllemp  11668  eftlub  11700  oddge22np1  11888  nn0oddm1d2  11916  gcdaddm  11987  bezoutlemsup  12012  gcdzeq  12025  dvdssqlem  12033  nn0seqcvgd  12043  lcmneg  12076  mulgcddvds  12096  qredeu  12099  pw2dvdseulemle  12169  pw2dvdseu  12170  nn0sqrtelqelz  12208  nonsq  12209  pythagtriplem3  12269  pythagtriplem6  12272  pythagtriplem7  12273  pclemub  12289  pcprendvds  12292  pcpremul  12295  pcidlem  12324  pcgcd1  12329  pc2dvds  12331  pcz  12333  pcprmpw2  12334  fldivp1  12348  pcfaclem  12349  pcfac  12350  pcbc  12351  ennnfoneleminc  12414  ennnfonelemkh  12415  ennnfonelemex  12417  ennnfonelemim  12427  lgseisenlem1  14535  2lgsoddprmlem2  14539  2sqlem7  14553  2sqlem8  14555