Theorem nn0red 9229

Description: A nonnegative integer is a real number. (Contributed by Mario Carneiro, 27-May-2016.)

Hypothesis

Ref	Expression
nn0red.1	|- ( ph -> A e. NN0 )

Assertion

Ref	Expression
nn0red	|- ( ph -> A e. RR )

Proof of Theorem nn0red

Step	Hyp	Ref	Expression
1		nn0ssre 9179	. 2 |- NN0 C_ RR
2		nn0red.1	. 2 |- ( ph -> A e. NN0 )
3	1, 2	sselid 3153	1 |- ( ph -> A e. RR )

Syntax hints:   -> wi 4   e. wcel 2148   RRcr 7809   NN0cn0 9175

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 4121  ax-cnex 7901  ax-resscn 7902  ax-1re 7904  ax-addrcl 7907  ax-rnegex 7919

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 2739  df-un 3133  df-in 3135  df-ss 3142  df-sn 3598  df-int 3845  df-inn 8919  df-n0 9176

This theorem is referenced by:  nn0cnd  9230  nn0readdcl  9234  nn01to3  9616  xnn0dcle  9801  flqmulnn0  10298  modifeq2int  10385  modaddmodup  10386  modaddmodlo  10387  modsumfzodifsn  10395  expnegap0  10527  nn0leexp2  10689  nn0le2msqd  10698  nn0opthlem2d  10700  nn0opthd  10701  faclbnd6  10723  bcval5  10742  filtinf  10770  zfz1isolemiso  10818  mertenslemi1  11542  efcllemp  11665  eftlub  11697  oddge22np1  11885  nn0oddm1d2  11913  gcdaddm  11984  bezoutlemsup  12009  gcdzeq  12022  dvdssqlem  12030  nn0seqcvgd  12040  lcmneg  12073  mulgcddvds  12093  qredeu  12096  pw2dvdseulemle  12166  pw2dvdseu  12167  nn0sqrtelqelz  12205  nonsq  12206  pythagtriplem3  12266  pythagtriplem6  12269  pythagtriplem7  12270  pclemub  12286  pcprendvds  12289  pcpremul  12292  pcidlem  12321  pcgcd1  12326  pc2dvds  12328  pcz  12330  pcprmpw2  12331  fldivp1  12345  pcfaclem  12346  pcfac  12347  pcbc  12348  ennnfoneleminc  12411  ennnfonelemkh  12412  ennnfonelemex  12414  ennnfonelemim  12424  lgseisenlem1  14420  2lgsoddprmlem2  14424  2sqlem7  14438  2sqlem8  14440