Theorem nnred 8997

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

Hypothesis

Ref	Expression
nnred.1	⊢ (𝜑 → 𝐴 ∈ ℕ)

Assertion

Ref	Expression
nnred	⊢ (𝜑 → 𝐴 ∈ ℝ)

Proof of Theorem nnred

Step	Hyp	Ref	Expression
1		nnssre 8988	. 2 ⊢ ℕ ⊆ ℝ
2		nnred.1	. 2 ⊢ (𝜑 → 𝐴 ∈ ℕ)
3	1, 2	sselid 3178	1 ⊢ (𝜑 → 𝐴 ∈ ℝ)

Syntax hints:   → wi 4   ∈ wcel 2164  ℝcr 7873  ℕcn 8984

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 710  ax-5 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-ext 2175  ax-sep 4148  ax-cnex 7965  ax-resscn 7966  ax-1re 7968  ax-addrcl 7971

This theorem depends on definitions:  df-bi 117  df-tru 1367  df-nf 1472  df-sb 1774  df-clab 2180  df-cleq 2186  df-clel 2189  df-nfc 2325  df-ral 2477  df-v 2762  df-in 3160  df-ss 3167  df-int 3872  df-inn 8985

This theorem is referenced by:  exbtwnzlemstep  10319  qbtwnrelemcalc  10327  qbtwnre  10328  flqdiv  10395  modqmulnn  10416  modifeq2int  10460  modaddmodup  10461  modaddmodlo  10462  modsumfzodifsn  10470  addmodlteq  10472  bernneq3  10736  expnbnd  10737  facwordi  10814  faclbnd  10815  faclbnd2  10816  faclbnd3  10817  faclbnd6  10818  facubnd  10819  facavg  10820  bcp1nk  10836  bcval5  10837  caucvgrelemcau  11127  caucvgre  11128  cvg1nlemcxze  11129  cvg1nlemcau  11131  cvg1nlemres  11132  resqrexlemdecn  11159  resqrexlemga  11170  fsum3cvg3  11542  divcnv  11643  cvgratnnlembern  11669  cvgratnnlemseq  11672  cvgratnnlemabsle  11673  cvgratnnlemsumlt  11674  cvgratnnlemrate  11676  cvgratz  11678  eftabs  11802  efcllemp  11804  ege2le3  11817  efcj  11819  eftlub  11836  eflegeo  11847  eirraplem  11923  dvdslelemd  11988  nno  12050  nnoddm1d2  12054  divalglemnqt  12064  divalglemeunn  12065  dvdsbnd  12096  sqgcd  12169  uzwodc  12177  lcmgcdlem  12218  ncoprmgcdne1b  12230  prmind2  12261  isprm5lem  12282  coprm  12285  prmfac1  12293  sqrt2irraplemnn  12320  divdenle  12338  qnumgt0  12339  nn0sqrtelqelz  12347  hashdvds  12362  eulerthlemrprm  12370  eulerthlema  12371  odzdvds  12386  pythagtriplem11  12415  pythagtriplem12  12416  pythagtriplem13  12417  pythagtriplem14  12418  pythagtriplem19  12423  pclemub  12428  pcpre1  12433  pcidlem  12464  dvdsprmpweqle  12478  pcadd  12481  pcmpt  12484  pcmpt2  12485  pcfaclem  12490  pcfac  12491  qexpz  12493  pockthlem  12497  pockthg  12498  1arith  12508  4sqlem5  12523  4sqlem6  12524  4sqlem10  12528  mul4sqlem  12534  4sqlem11  12542  4sqlem12  12543  4sqlem13m  12544  4sqlem14  12545  4sqlem15  12546  4sqlem16  12547  4sqlem17  12548  znnen  12558  exmidunben  12586  nninfdclemp1  12610  nninfdclemlt  12611  nninfdclemf1  12612  strleund  12724  strext  12726  psrbaglesuppg  14169  logbgcd1irraplemexp  15141  logbgcd1irraplemap  15142  wilthlem1  15153  lgslem1  15157  lgsval2lem  15167  lgsdirprm  15191  lgsdir  15192  gausslemma2dlem0h  15213  gausslemma2dlem1a  15215  gausslemma2dlem2  15219  lgseisenlem1  15227  lgseisenlem2  15228  lgseisenlem3  15229  lgseisen  15231  lgsquadlem1  15234  lgsquadlem2  15235  lgsquadlem3  15236  2sqlem3  15274  2sqlem8  15280  cvgcmp2nlemabs  15592