Theorem nnred 11653

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 11642	. 2 ⊢ ℕ ⊆ ℝ
2		nnred.1	. 2 ⊢ (𝜑 → 𝐴 ∈ ℕ)
3	1, 2	sseldi 3965	1 ⊢ (𝜑 → 𝐴 ∈ ℝ)

Syntax hints:   → wi 4   ∈ wcel 2114  ℝcr 10536  ℕcn 11638

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793  ax-sep 5203  ax-nul 5210  ax-pow 5266  ax-pr 5330  ax-un 7461  ax-1cn 10595  ax-icn 10596  ax-addcl 10597  ax-addrcl 10598  ax-mulcl 10599  ax-mulrcl 10600  ax-i2m1 10605  ax-1ne0 10606  ax-rrecex 10609  ax-cnre 10610

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1084  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-mo 2622  df-eu 2654  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ne 3017  df-ral 3143  df-rex 3144  df-reu 3145  df-rab 3147  df-v 3496  df-sbc 3773  df-csb 3884  df-dif 3939  df-un 3941  df-in 3943  df-ss 3952  df-pss 3954  df-nul 4292  df-if 4468  df-pw 4541  df-sn 4568  df-pr 4570  df-tp 4572  df-op 4574  df-uni 4839  df-iun 4921  df-br 5067  df-opab 5129  df-mpt 5147  df-tr 5173  df-id 5460  df-eprel 5465  df-po 5474  df-so 5475  df-fr 5514  df-we 5516  df-xp 5561  df-rel 5562  df-cnv 5563  df-co 5564  df-dm 5565  df-rn 5566  df-res 5567  df-ima 5568  df-pred 6148  df-ord 6194  df-on 6195  df-lim 6196  df-suc 6197  df-iota 6314  df-fun 6357  df-fn 6358  df-f 6359  df-f1 6360  df-fo 6361  df-f1o 6362  df-fv 6363  df-ov 7159  df-om 7581  df-wrecs 7947  df-recs 8008  df-rdg 8046  df-nn 11639

This theorem is referenced by:  nnne0  11672  uzwo3  12344  modmulnn  13258  bernneq3  13593  expmulnbnd  13597  expnngt1b  13604  facwordi  13650  faclbnd  13651  faclbnd2  13652  faclbnd3  13653  faclbnd5  13659  faclbnd6  13660  facubnd  13661  facavg  13662  bcp1nk  13678  hashf1  13816  swrds2  14302  isercolllem1  15021  isercoll  15024  o1fsum  15168  climcndslem1  15204  climcndslem2  15205  climcnds  15206  eftabs  15429  efcllem  15431  ege2le3  15443  efcj  15445  eftlub  15462  eflegeo  15474  eirrlem  15557  fzm1ndvds  15672  nno  15733  nnoddm1d2  15737  bitsfzolem  15783  bitsfzo  15784  bitsinv1lem  15790  sadcaddlem  15806  smueqlem  15839  bezoutlem3  15889  bezoutlem4  15890  sqgcd  15909  lcmgcdlem  15950  lcmf  15977  prmind2  16029  coprm  16055  prmfac1  16063  prmndvdsfaclt  16067  divdenle  16089  qnumgt0  16090  zsqrtelqelz  16098  hashdvds  16112  eulerthlem2  16119  odzdvds  16132  vfermltl  16138  modprm0  16142  pythagtriplem11  16162  pythagtriplem13  16164  pythagtriplem19  16170  pclem  16175  pcpre1  16179  pcidlem  16208  dvdsprmpweqle  16222  pcadd  16225  pcmpt  16228  pcmpt2  16229  pcfaclem  16234  pcfac  16235  qexpz  16237  pockthlem  16241  pockthg  16242  prmreclem1  16252  prmreclem3  16254  prmreclem4  16255  prmreclem5  16256  1arithlem4  16262  1arith  16263  4sqlem5  16278  4sqlem6  16279  4sqlem10  16283  mul4sqlem  16289  4sqlem11  16291  4sqlem12  16292  4sqlem13  16293  4sqlem14  16294  4sqlem15  16295  4sqlem16  16296  4sqlem17  16297  vdwlem1  16317  vdwlem3  16319  vdwlem6  16322  vdwlem9  16325  vdwlem10  16326  vdwlem12  16328  vdwnnlem3  16333  ramub1lem1  16362  prmolefac  16382  prmgaplem4  16390  prmgaplem5  16391  prmgaplem6  16392  prmgaplem8  16394  2expltfac  16426  cshwshashnsame  16437  setsstruct2  16521  psgnunilem4  18625  mndodconglem  18669  oddvds  18675  sylow1lem1  18723  sylow1lem5  18727  fislw  18750  efgredlem  18873  gexexlem  18972  zringlpirlem3  20633  prmirredlem  20640  fvmptnn04if  21457  fvmptnn04ifb  21459  fvmptnn04ifc  21460  fvmptnn04ifd  21461  chfacfisf  21462  chfacfisfcpmat  21463  chfacfscmulgsum  21468  chfacfpmmulgsum  21472  lebnumii  23570  lmnn  23866  ovolunlem1a  24097  ovoliunlem1  24103  ovolicc2lem3  24120  ovolicc2lem4  24121  iundisj  24149  voliunlem1  24151  uniioombllem3  24186  dyadf  24192  dyadovol  24194  dyaddisjlem  24196  dyadmaxlem  24198  opnmbllem  24202  vitalilem4  24212  mbfi1fseqlem1  24316  mbfi1fseqlem3  24318  mbfi1fseqlem4  24319  mbfi1fseqlem5  24320  mbfi1fseqlem6  24321  itg2gt0  24361  itg2cnlem2  24363  dgreq0  24855  dgrco  24865  elqaalem2  24909  aaliou3lem2  24932  aaliou3lem8  24934  aaliou3lem9  24939  leibpi  25520  log2tlbnd  25523  birthdaylem3  25531  amgm  25568  emcllem2  25574  harmonicbnd4  25588  lgamgulmlem1  25606  lgamgulmlem2  25607  lgamgulmlem3  25608  lgamgulmlem4  25609  lgamgulmlem5  25610  lgamgulmlem6  25611  lgamucov  25615  lgamcvg2  25632  wilthlem1  25645  ftalem5  25654  basellem1  25658  basellem2  25659  basellem3  25660  basellem4  25661  basellem5  25662  basellem6  25663  basellem8  25665  chtge0  25689  chtwordi  25733  vma1  25743  dvdsflf1o  25764  dvdsflsumcom  25765  fsumfldivdiaglem  25766  sgmmul  25777  chtublem  25787  fsumvma2  25790  logfac2  25793  chpchtsum  25795  chpub  25796  logfaclbnd  25798  logexprlim  25801  mersenne  25803  perfectlem2  25806  dchrelbas4  25819  bposlem1  25860  bposlem2  25861  bposlem3  25862  bposlem4  25863  bposlem5  25864  bposlem6  25865  bposlem7  25866  bposlem9  25868  lgslem1  25873  lgsval2lem  25883  lgsdirprm  25907  lgsdir  25908  lgsne0  25911  lgsqrlem2  25923  gausslemma2dlem0h  25939  gausslemma2dlem0i  25940  gausslemma2dlem1a  25941  gausslemma2dlem2  25943  gausslemma2dlem7  25949  gausslemma2d  25950  lgseisenlem1  25951  lgseisenlem2  25952  lgseisenlem3  25953  lgseisenlem4  25954  lgseisen  25955  lgsquadlem1  25956  lgsquadlem2  25957  lgsquadlem3  25958  2sqlem3  25996  2sqlem8  26002  2sqblem  26007  2sqmod  26012  chebbnd1lem1  26045  chebbnd1lem3  26047  chtppilimlem1  26049  rplogsumlem1  26060  rplogsumlem2  26061  dchrisum0lem1a  26062  rpvmasumlem  26063  dchrisumlema  26064  dchrisumlem1  26065  dchrisumlem2  26066  dchrisumlem3  26067  dchrvmasumiflem1  26077  dchrisum0flblem2  26085  dchrisum0re  26089  dchrisum0lem1b  26091  dchrisum0lem1  26092  dirith2  26104  selbergb  26125  selberg2lem  26126  logdivbnd  26132  selberg3lem2  26134  selberg4lem1  26136  pntrsumo1  26141  pntrsumbnd2  26143  pntrlog2bndlem1  26153  pntrlog2bndlem2  26154  pntrlog2bndlem3  26155  pntrlog2bndlem4  26156  pntrlog2bndlem5  26157  pntpbnd1a  26161  pntpbnd1  26162  pntibndlem2a  26166  pntibndlem2  26167  pntlemg  26174  pntlemh  26175  pntlemj  26179  pntlemf  26181  ostth2lem1  26194  padicabvf  26207  padicabvcxp  26208  ostth2lem2  26210  ostth2lem3  26211  ostth2lem4  26212  ostth2  26213  ostth3  26214  numclwwlk5  28167  numclwwlk7  28170  ubthlem2  28648  minvecolem4  28657  iundisjf  30339  ssnnssfz  30510  iundisjfi  30519  pfxlsw2ccat  30626  pmtrto1cl  30741  psgnfzto1stlem  30742  fzto1st1  30744  fzto1st  30745  psgnfzto1st  30747  cycpmco2lem6  30773  cycpmco2lem7  30774  smatrcl  31061  smattr  31064  smatbl  31065  smatbr  31066  1smat1  31069  submateqlem1  31072  submateqlem2  31073  submateq  31074  esumcst  31322  fiunelros  31433  oddpwdc  31612  eulerpartlems  31618  eulerpartlemgc  31620  fiblem  31656  dstfrvunirn  31732  dstfrvclim1  31735  ballotlemimin  31763  fsum2dsub  31878  reprinfz1  31893  hgt750lemd  31919  hgt750lemb  31927  hgt750leme  31929  tgoldbachgtde  31931  tgoldbachgt  31934  subfaclim  32435  subfacval3  32436  erdszelem7  32444  erdszelem8  32445  erdsze2lem2  32451  cvmliftlem2  32533  cvmliftlem6  32537  cvmliftlem7  32538  cvmliftlem8  32539  cvmliftlem9  32540  cvmliftlem10  32541  cvmliftlem13  32543  bcprod  32970  bccolsum  32971  faclimlem2  32976  faclim2  32980  nn0prpwlem  33670  knoppndvlem15  33865  knoppndvlem17  33867  knoppndvlem18  33868  knoppndvlem19  33869  knoppndvlem20  33870  knoppndvlem21  33871  poimirlem3  34910  poimirlem6  34913  poimirlem7  34914  poimirlem8  34915  poimirlem9  34916  poimirlem10  34917  poimirlem11  34918  poimirlem12  34919  poimirlem13  34920  poimirlem15  34922  poimirlem16  34923  poimirlem17  34924  poimirlem19  34926  poimirlem20  34927  poimirlem21  34928  poimirlem22  34929  poimirlem23  34930  poimirlem26  34933  poimirlem28  34935  opnmbllem0  34943  mblfinlem2  34945  incsequz  35038  nninfnub  35041  nnadddir  39212  oexpreposd  39228  nn0expgcd  39233  rtprmirr  39243  fltltc  39322  fltnltalem  39323  fltnlta  39324  3cubeslem3r  39333  irrapxlem3  39470  irrapxlem4  39471  irrapxlem5  39472  pellexlem2  39476  pellexlem6  39480  pell14qrgt0  39505  pell14qrgapw  39522  pellfundgt1  39529  rmspecsqrtnq  39552  ltrmxnn0  39595  jm3.1lem1  39663  jm3.1lem3  39665  dgraa0p  39798  hashnzfz2  40702  rfcnnnub  41342  nnxrd  41348  fzisoeu  41616  fsumnncl  41901  sumnnodd  41960  limsup10exlem  42102  stoweidlem1  42335  stoweidlem3  42337  stoweidlem11  42345  stoweidlem17  42351  stoweidlem20  42354  stoweidlem25  42359  stoweidlem26  42360  stoweidlem34  42368  stoweidlem38  42372  stoweidlem42  42376  stoweidlem44  42378  stoweidlem51  42385  stoweidlem59  42393  stoweidlem60  42394  wallispi  42404  wallispi2  42407  stirlinglem3  42410  stirlinglem4  42411  stirlinglem8  42415  stirlinglem10  42417  stirlinglem12  42419  stirlinglem15  42422  dirkertrigeqlem2  42433  dirkertrigeqlem3  42434  dirkercncflem2  42438  fourierdlem11  42452  fourierdlem14  42455  fourierdlem15  42456  fourierdlem20  42461  fourierdlem31  42472  fourierdlem64  42504  fourierdlem93  42533  fourierdlem95  42535  fourierdlem103  42543  fourierdlem104  42544  fourierdlem112  42552  sqwvfourb  42563  etransclem3  42571  etransclem19  42587  etransclem23  42591  etransclem24  42592  etransclem25  42593  etransclem32  42600  etransclem35  42603  etransclem41  42609  etransclem48  42616  qndenserrnbllem  42628  hoiqssbllem1  42953  hoiqssbllem2  42954  ovolval5lem1  42983  ovolval5lem2  42984  iccpartlt  43633  iccpartgt  43636  odz2prm2pw  43774  fmtnoprmfac1lem  43775  2pwp1prm  43800  sfprmdvdsmersenne  43817  lighneallem2  43820  proththdlem  43827  perfectALTVlem2  43936  gbowge7  43977  ztprmneprm  44444  pgrple2abl  44462  logbpw2m1  44676  nnpw2pmod  44692  nnolog2flm1  44699  blennngt2o2  44701