Theorem nncnd 11036

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

Hypothesis

Ref	Expression
nnred.1	|- ( ph -> A e. NN )

Assertion

Ref	Expression
nncnd	|- ( ph -> A e. CC )

Proof of Theorem nncnd

Step	Hyp	Ref	Expression
1		nnsscn 11025	. 2 |- NN C_ CC
2		nnred.1	. 2 |- ( ph -> A e. NN )
3	1, 2	sseldi 3601	1 |- ( ph -> A e. CC )

Syntax hints:   -> wi 4   e. wcel 1990   CCcc 9934   NNcn 11020

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-8 1992  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-sep 4781  ax-nul 4789  ax-pow 4843  ax-pr 4906  ax-un 6949  ax-resscn 9993  ax-1cn 9994  ax-icn 9995  ax-addcl 9996  ax-addrcl 9997  ax-mulcl 9998  ax-mulrcl 9999  ax-i2m1 10004  ax-1ne0 10005  ax-rrecex 10008  ax-cnre 10009

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1038  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-ral 2917  df-rex 2918  df-reu 2919  df-rab 2921  df-v 3202  df-sbc 3436  df-csb 3534  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-pss 3590  df-nul 3916  df-if 4087  df-pw 4160  df-sn 4178  df-pr 4180  df-tp 4182  df-op 4184  df-uni 4437  df-iun 4522  df-br 4654  df-opab 4713  df-mpt 4730  df-tr 4753  df-id 5024  df-eprel 5029  df-po 5035  df-so 5036  df-fr 5073  df-we 5075  df-xp 5120  df-rel 5121  df-cnv 5122  df-co 5123  df-dm 5124  df-rn 5125  df-res 5126  df-ima 5127  df-pred 5680  df-ord 5726  df-on 5727  df-lim 5728  df-suc 5729  df-iota 5851  df-fun 5890  df-fn 5891  df-f 5892  df-f1 5893  df-fo 5894  df-f1o 5895  df-fv 5896  df-ov 6653  df-om 7066  df-wrecs 7407  df-recs 7468  df-rdg 7506  df-nn 11021

This theorem is referenced by:  facdiv  13074  facndiv  13075  faclbnd  13077  faclbnd5  13085  faclbnd6  13086  facubnd  13087  facavg  13088  bccmpl  13096  bcn0  13097  bcn1  13100  bcm1k  13102  bcp1n  13103  bcp1nk  13104  bcval5  13105  bcpasc  13108  permnn  13113  hashf1  13241  hashfac  13242  relexpaddnn  13791  binom11  14564  binom1dif  14565  climcndslem2  14582  arisum2  14593  trireciplem  14594  trirecip  14595  geo2sum  14604  geo2lim  14606  fprodfac  14703  risefacfac  14766  fallfacfwd  14767  fallfacval4  14774  bcfallfac  14775  fallfacfac  14776  bpolycl  14783  bpolysum  14784  bpolydiflem  14785  fsumkthpow  14787  eftcl  14804  eftabs  14806  efcllem  14808  ege2le3  14820  efcj  14822  efaddlem  14823  eftlub  14839  eirrlem  14932  sqrt2irrlem  14977  sqrt2irrlemOLD  14978  oexpneg  15069  pwp1fsum  15114  bitsp1  15153  bitsfzolem  15156  bitsfzo  15157  bitsmod  15158  bitscmp  15160  bitsinv1lem  15163  bitsinv1  15164  2ebits  15169  bitsinvp1  15171  sadcaddlem  15179  sadadd3  15183  bitsres  15195  bitsuz  15196  bitsshft  15197  mulgcd  15265  rplpwr  15276  sqgcd  15278  lcmgcdlem  15319  3lcm2e6woprm  15328  coprmprod  15375  coprmproddvdslem  15376  cncongr1  15381  cncongr2  15382  prmind2  15398  isprm5  15419  divgcdodd  15422  prmdvdsexpr  15429  qmuldeneqnum  15455  divnumden  15456  qnumgt0  15458  numdensq  15462  hashdvds  15480  phiprmpw  15481  prmdiv  15490  prmdivdiv  15492  phisum  15495  modprm0  15510  pythagtriplem4  15524  pythagtriplem6  15526  pythagtriplem7  15527  pythagtriplem14  15533  pythagtriplem15  15534  pythagtriplem19  15538  pythagtrip  15539  pcprendvds2  15546  pcpre1  15547  pcpremul  15548  pceulem  15550  pcdiv  15557  pcqmul  15558  pcelnn  15574  pcid  15577  pc2dvds  15583  dvdsprmpweqnn  15589  dvdsprmpweqle  15590  pcaddlem  15592  pcadd  15593  pcfaclem  15602  qexpz  15605  expnprm  15606  oddprmdvds  15607  prmpwdvds  15608  pockthlem  15609  pockthg  15610  infpnlem1  15614  prmreclem1  15620  prmreclem2  15621  prmreclem3  15622  prmreclem4  15623  prmreclem6  15625  4sqlem6  15647  4sqlem7  15648  4sqlem10  15651  mul4sqlem  15657  4sqlem11  15659  4sqlem12  15660  4sqlem14  15662  4sqlem17  15665  4sqlem18  15666  vdwlem1  15685  vdwlem2  15686  vdwlem3  15687  vdwlem5  15689  vdwlem6  15690  vdwlem8  15692  vdwlem9  15693  vdwlem10  15694  vdwlem12  15696  ramub1lem2  15731  ramcl  15733  prmop1  15742  prmdvdsprmo  15746  prmgaplem7  15761  prmgaplem8  15762  gsumccat  17378  mulgnndir  17569  mulgnndirOLD  17570  mulgnnass  17576  mulgnnassOLD  17577  psgnunilem5  17914  odf1o2  17988  pgp0  18011  sylow1lem1  18013  odcau  18019  sylow2blem3  18037  sylow3lem3  18044  sylow3lem4  18045  gexexlem  18255  ablfacrp2  18466  ablfac1lem  18467  ablfac1eu  18472  pgpfac1lem3a  18475  pgpfac1lem3  18476  zringlpirlem3  19834  znrrg  19914  cpmadugsumlemF  20681  lebnumlem3  22762  ovollb2lem  23256  ovolunlem1a  23264  ovolunlem1  23265  uniioombllem3  23353  uniioombllem4  23354  dyaddisjlem  23363  mbfi1fseqlem3  23484  mbfi1fseqlem4  23485  dgrcolem1  24029  vieta1lem1  24065  vieta1lem2  24066  elqaalem2  24075  elqaalem3  24076  aalioulem1  24087  aaliou3lem2  24098  aaliou3lem8  24100  aaliou3lem6  24103  aaliou3lem9  24105  taylfvallem1  24111  tayl0  24116  taylply2  24122  taylply  24123  dvtaylp  24124  taylthlem1  24127  taylthlem2  24128  pserdvlem2  24182  advlogexp  24401  cxpmul2  24435  cxpeq  24498  atantayl3  24666  leibpi  24669  log2cnv  24671  log2tlbnd  24672  birthdaylem2  24679  birthdaylem3  24680  amgmlem  24716  amgm  24717  emcllem5  24726  fsumharmonic  24738  zetacvg  24741  dmgmdivn0  24754  lgamgulmlem3  24757  lgamgulmlem4  24758  lgamgulmlem5  24759  lgamgulmlem6  24760  lgamgulm2  24762  lgamcvg2  24781  gamcvg  24782  gamcvg2lem  24785  facgam  24792  wilthlem1  24794  wilthlem2  24795  wilthlem3  24796  wilthimp  24798  basellem1  24807  basellem2  24808  basellem3  24809  basellem4  24810  basellem5  24811  basellem8  24814  vmaprm  24843  sgmval2  24869  0sgm  24870  sgmf  24871  vma1  24892  fsumdvdsdiaglem  24909  dvdsflf1o  24913  muinv  24919  dvdsmulf1o  24920  sgmppw  24922  1sgmprm  24924  1sgm2ppw  24925  sgmmul  24926  chtublem  24936  fsumvma2  24939  chpchtsum  24944  logfaclbnd  24947  logexprlim  24950  mersenne  24952  perfect1  24953  perfectlem1  24954  perfectlem2  24955  perfect  24956  dchrsum2  24993  dchrhash  24996  bcmono  25002  bcp1ctr  25004  bclbnd  25005  bposlem1  25009  bposlem2  25010  bposlem3  25011  bposlem5  25013  bposlem6  25014  lgsval2lem  25032  lgsqrlem2  25072  gausslemma2dlem6  25097  gausslemma2dlem7  25098  gausslemma2d  25099  lgseisenlem1  25100  lgseisenlem4  25103  lgsquadlem1  25105  lgsquadlem2  25106  lgsquadlem3  25107  lgsquad2  25111  m1lgs  25113  2sqlem3  25145  2sqlem4  25146  chebbnd1lem1  25158  chebbnd1  25161  rplogsumlem1  25173  rplogsumlem2  25174  rpvmasumlem  25176  dchrisumlem1  25178  dchrmusum2  25183  dchrvmasumlem1  25184  dchrvmasum2lem  25185  dchrvmasum2if  25186  dchrvmasumlem2  25187  dchrvmasumlem3  25188  dchrvmasumiflem1  25190  dchrisum0flblem1  25197  dchrisum0flblem2  25198  dchrisum0fno1  25200  rpvmasum2  25201  rplogsum  25216  mulogsumlem  25220  mulogsum  25221  mulog2sumlem2  25224  vmalogdivsum2  25227  vmalogdivsum  25228  2vmadivsumlem  25229  logsqvma  25231  selberglem2  25235  selberglem3  25236  selberg  25237  selberg2lem  25239  logdivbnd  25245  selberg3lem1  25246  selberg4lem1  25249  pntrsumo1  25254  pntrsumbnd2  25256  selberg3r  25258  selberg4r  25259  selberg34r  25260  pntsval2  25265  pntrlog2bndlem2  25267  pntrlog2bndlem4  25269  pntrlog2bndlem6  25272  pntpbnd1  25275  pntpbnd2  25276  pntlemg  25287  pntlemn  25289  pntlemf  25294  pnt  25303  padicabvf  25320  ostth2lem2  25323  ostth3  25327  fusgrhashclwwlkn  26956  eucrct2eupth  27105  numdenneg  29563  ltesubnnd  29568  1smat1  29870  madjusmdetlem2  29894  madjusmdetlem4  29896  qqhnm  30034  oddpwdc  30416  eulerpartlemsv2  30420  eulerpartlems  30422  eulerpartlemsv3  30423  eulerpartlemgc  30424  eulerpartlemv  30426  eulerpartlemgs2  30442  fibp1  30463  ballotlemfc0  30554  ballotlemfcc  30555  signsvtn0  30647  reprpmtf1o  30704  vtscl  30716  hgt750lemb  30734  tgoldbachgt  30741  subfacp1lem1  31161  subfacp1lem5  31166  subfacval2  31169  subfaclim  31170  cvmliftlem2  31268  cvmliftlem7  31273  cvmliftlem10  31276  cvmliftlem11  31277  cvmliftlem13  31278  bcm1nt  31623  bcprod  31624  iprodgam  31628  faclimlem1  31629  faclimlem2  31630  faclim2  31634  nn0prpwlem  32317  nn0prpw  32318  knoppndvlem16  32518  poimirlem1  33410  poimirlem2  33411  poimirlem6  33415  poimirlem7  33416  poimirlem8  33417  poimirlem9  33418  poimirlem10  33419  poimirlem11  33420  poimirlem12  33421  poimirlem13  33422  poimirlem15  33424  poimirlem16  33425  poimirlem17  33426  poimirlem18  33427  poimirlem19  33428  poimirlem20  33429  poimirlem21  33430  poimirlem22  33431  poimirlem23  33432  poimirlem24  33433  poimirlem25  33434  poimirlem26  33435  poimirlem27  33436  poimirlem31  33440  irrapxlem4  37389  irrapxlem5  37390  pellexlem2  37394  pellexlem6  37398  pell1234qrne0  37417  pell1234qrreccl  37418  pell1234qrmulcl  37419  pell1234qrdich  37425  pell14qrdich  37433  pell1qrge1  37434  pell1qr1  37435  pell14qrgapw  37440  rmxyneg  37485  rmxm1  37499  rmxluc  37501  rmxdbl  37504  jm2.19lem1  37556  jm2.27c  37574  itgpowd  37800  relexpmulnn  38001  relexpmulg  38002  inductionexd  38453  hashnzfzclim  38521  bcccl  38538  bcc0  38539  bccp1k  38540  bccm1k  38541  binomcxplemwb  38547  fsumnncl  39803  mccllem  39829  clim1fr1  39833  sumnnodd  39862  dvsinexp  40125  dvxpaek  40155  dvnxpaek  40157  dvnprodlem2  40162  itgsinexplem1  40169  itgsinexp  40170  stoweidlem1  40218  stoweidlem11  40228  stoweidlem25  40242  stoweidlem26  40243  stoweidlem34  40251  stoweidlem37  40254  stoweidlem38  40255  stoweidlem42  40259  wallispi2lem1  40288  wallispi2  40290  stirlinglem4  40294  stirlinglem5  40295  stirlinglem10  40300  stirlinglem15  40305  dirkertrigeqlem3  40317  dirkertrigeq  40318  dirkercncflem2  40321  dirkercncflem4  40323  fourierdlem11  40335  fourierdlem15  40339  fourierdlem79  40402  fourierdlem83  40406  sqwvfourb  40446  etransclem14  40465  etransclem15  40466  etransclem20  40471  etransclem21  40472  etransclem22  40473  etransclem23  40474  etransclem24  40475  etransclem25  40476  etransclem28  40479  etransclem31  40482  etransclem32  40483  etransclem33  40484  etransclem34  40485  etransclem35  40486  etransclem38  40489  etransclem41  40492  etransclem44  40495  etransclem45  40496  etransclem47  40498  etransclem48  40499  nnfoctbdjlem  40672  deccarry  41321  iccpartgtprec  41356  fmtnoodd  41445  fmtnorec2lem  41454  fmtnorec2  41455  fmtnodvds  41456  goldbachthlem2  41458  fmtnorec3  41460  fmtnorec4  41461  fmtnoprmfac1lem  41476  fmtnoprmfac1  41477  fmtnoprmfac2lem1  41478  fmtnoprmfac2  41479  2pwp1prm  41503  sfprmdvdsmersenne  41520  lighneallem4b  41526  lighneal  41528  proththdlem  41530  proththd  41531  oexpnegALTV  41588  perfectALTVlem1  41630  perfectALTVlem2  41631  perfectALTV  41632  nnpw2pmod  42377  nnolog2flm1  42384  blennn0em1  42385  blengt1fldiv2p1  42387  nn0sumshdiglemB  42414  amgmlemALT  42549