Theorem nncnd 8862

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 8853	. 2 |- NN C_ CC
2		nnred.1	. 2 |- ( ph -> A e. NN )
3	1, 2	sseldi 3135	1 |- ( ph -> A e. CC )

Syntax hints:   -> wi 4   e. wcel 2135   CCcc 7742   NNcn 8848

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 699  ax-5 1434  ax-7 1435  ax-gen 1436  ax-ie1 1480  ax-ie2 1481  ax-8 1491  ax-10 1492  ax-11 1493  ax-i12 1494  ax-bndl 1496  ax-4 1497  ax-17 1513  ax-i9 1517  ax-ial 1521  ax-i5r 1522  ax-ext 2146  ax-sep 4094  ax-cnex 7835  ax-resscn 7836  ax-1re 7838  ax-addrcl 7841

This theorem depends on definitions:  df-bi 116  df-tru 1345  df-nf 1448  df-sb 1750  df-clab 2151  df-cleq 2157  df-clel 2160  df-nfc 2295  df-ral 2447  df-v 2723  df-in 3117  df-ss 3124  df-int 3819  df-inn 8849

This theorem is referenced by:  peano5uzti  9290  qapne  9568  qtri3or  10168  exbtwnzlemstep  10173  intfracq  10245  flqdiv  10246  modqmulnn  10267  addmodid  10297  modaddmodup  10312  modsumfzodifsn  10321  addmodlteq  10323  facdiv  10640  facndiv  10641  faclbnd  10643  faclbnd6  10646  facubnd  10647  facavg  10648  bccmpl  10656  bcn0  10657  bcn1  10660  bcm1k  10662  bcp1n  10663  bcp1nk  10664  bcval5  10665  bcpasc  10668  permnn  10673  cvg1nlemcxze  10910  cvg1nlemcau  10912  resqrexlemcalc3  10944  binom11  11413  binom1dif  11414  divcnv  11424  arisum2  11426  trireciplem  11427  trirecip  11428  expcnvap0  11429  geo2sum  11441  geo2lim  11443  cvgratnnlembern  11450  cvgratnnlemnexp  11451  cvgratnnlemmn  11452  cvgratnnlemsumlt  11455  cvgratnnlemfm  11456  cvgratnnlemrate  11457  cvgratz  11459  eftcl  11581  eftabs  11583  efcllemp  11585  ege2le3  11598  efcj  11600  efaddlem  11601  eftlub  11617  eirraplem  11703  oexpneg  11799  divalglemnn  11840  dvdsgcdidd  11912  bezoutlemnewy  11914  mulgcd  11934  rplpwr  11945  sqgcd  11947  lcmgcdlem  11988  3lcm2e6woprm  11997  cncongr1  12014  cncongr2  12015  prmind2  12031  divgcdodd  12052  prmdvdsexpr  12059  sqrt2irrlem  12070  oddpwdclemxy  12078  oddpwdclemodd  12081  oddpwdclemdc  12082  oddpwdc  12083  sqpweven  12084  2sqpwodd  12085  sqrt2irraplemnn  12088  sqrt2irrap  12089  qmuldeneqnum  12104  divnumden  12105  qnumgt0  12107  numdensq  12111  hashdvds  12130  phiprmpw  12131  prmdiv  12144  prmdivdiv  12146  phisum  12149  modprm0  12163  pythagtriplem4  12177  pythagtriplem6  12179  pythagtriplem7  12180  pythagtriplem14  12186  pythagtriplem15  12187  pythagtriplem16  12188  pythagtriplem19  12191  pythagtrip  12192  pcprendvds2  12200  pcpre1  12201  pcpremul  12202  pceulem  12203  pcdiv  12211  pcqmul  12212  pcelnn  12229  pcid  12232  pc2dvds  12238  dvdsprmpweqnn  12244  dvdsprmpweqle  12245  pcaddlem  12247  pcadd  12248  pcfaclem  12256  qexpz  12259  expnprm  12260  oddprmdvds  12261  oddennn  12262  evenennn  12263  logbgcd1irraplemap  13428  trilpolemeq1  13753  trilpolemlt1  13754  redcwlpolemeq1  13767  nconstwlpolemgt0  13776