Theorem nncnd 9256

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

Hypothesis

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

Assertion

Ref	Expression
nncnd	⊢ (𝜑 → 𝐴 ∈ ℂ)

Proof of Theorem nncnd

Step	Hyp	Ref	Expression
1		nnsscn 9247	. 2 ⊢ ℕ ⊆ ℂ
2		nnred.1	. 2 ⊢ (𝜑 → 𝐴 ∈ ℕ)
3	1, 2	sselid 3238	1 ⊢ (𝜑 → 𝐴 ∈ ℂ)

Syntax hints:   → wi 4   ∈ wcel 2205  ℂcc 8130  ℕcn 9242

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 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2216  ax-sep 4230  ax-cnex 8223  ax-resscn 8224  ax-1re 8226  ax-addrcl 8229

This theorem depends on definitions:  df-bi 117  df-tru 1401  df-nf 1510  df-sb 1812  df-clab 2221  df-cleq 2227  df-clel 2230  df-nfc 2375  df-ral 2527  df-v 2817  df-in 3219  df-ss 3226  df-int 3952  df-inn 9243

This theorem is referenced by:  peano5uzti  9692  qapne  9977  qtri3or  10607  exbtwnzlemstep  10614  intfracq  10689  flqdiv  10690  modqmulnn  10711  addmodid  10741  modaddmodup  10756  modsumfzodifsn  10765  addmodlteq  10767  facdiv  11108  facndiv  11109  faclbnd  11111  faclbnd6  11114  facubnd  11115  facavg  11116  bccmpl  11124  bcn0  11125  bcn1  11128  bcm1k  11130  bcp1n  11131  bcp1nk  11132  bcval5  11133  bcpasc  11136  permnn  11142  cvg1nlemcxze  11675  cvg1nlemcau  11677  resqrexlemcalc3  11709  binom11  12180  binom1dif  12181  divcnv  12191  arisum2  12193  trireciplem  12194  trirecip  12195  expcnvap0  12196  geo2sum  12208  geo2lim  12210  cvgratnnlembern  12217  cvgratnnlemnexp  12218  cvgratnnlemmn  12219  cvgratnnlemsumlt  12222  cvgratnnlemfm  12223  cvgratnnlemrate  12224  cvgratz  12226  eftcl  12348  eftabs  12350  efcllemp  12352  ege2le3  12365  efcj  12367  efaddlem  12368  eftlub  12384  eirraplem  12471  oexpneg  12571  divalglemnn  12612  bitsp1  12645  bitsfzolem  12648  bitsfzo  12649  bitsmod  12650  bitscmp  12652  bitsinv1lem  12655  bitsinv1  12656  dvdsgcdidd  12698  bezoutlemnewy  12700  mulgcd  12720  rplpwr  12731  sqgcd  12733  lcmgcdlem  12782  3lcm2e6woprm  12791  cncongr1  12808  cncongr2  12809  prmind2  12825  isprm5  12847  divgcdodd  12848  prmdvdsexpr  12855  sqrt2irrlem  12866  oddpwdclemxy  12874  oddpwdclemodd  12877  oddpwdclemdc  12878  oddpwdc  12879  sqpweven  12880  2sqpwodd  12881  sqrt2irraplemnn  12884  sqrt2irrap  12885  qmuldeneqnum  12900  divnumden  12901  qnumgt0  12903  numdensq  12907  hashdvds  12926  phiprmpw  12927  prmdiv  12940  prmdivdiv  12942  phisum  12946  modprm0  12960  pythagtriplem4  12974  pythagtriplem6  12976  pythagtriplem7  12977  pythagtriplem14  12983  pythagtriplem15  12984  pythagtriplem16  12985  pythagtriplem19  12988  pythagtrip  12989  pcprendvds2  12997  pcpre1  12998  pcpremul  12999  pceulem  13000  pcdiv  13008  pcqmul  13009  pcelnn  13027  pcid  13030  pc2dvds  13036  dvdsprmpweqnn  13042  dvdsprmpweqle  13043  pcaddlem  13045  pcadd  13046  pcfaclem  13055  qexpz  13058  expnprm  13059  oddprmdvds  13060  prmpwdvds  13061  pockthlem  13062  pockthg  13063  infpnlem1  13065  4sqlem6  13089  4sqlem7  13090  4sqlem10  13093  mul4sqlem  13099  4sqlem11  13107  4sqlem12  13108  4sqlem14  13110  4sqlem17  13113  4sqlem18  13114  ballotfilemfc0  13157  ballotfilemfcc  13158  oddennn  13164  evenennn  13165  mulgnndir  13889  mulgnnass  13895  znrrg  14857  logbgcd1irraplemap  15883  pellexlem2  15895  wilthlem1  15897  0sgm  15902  mpodvdsmulf1o  15907  1sgmprm  15911  1sgm2ppw  15912  mersenne  15914  perfect1  15915  perfectlem1  15916  perfectlem2  15917  perfect  15918  lgsval2lem  15932  gausslemma2dlem6  15989  gausslemma2dlem7  15990  gausslemma2d  15991  lgseisenlem1  15992  lgseisenlem4  15995  lgsquadlem1  15999  lgsquadlem2  16000  lgsquadlem3  16001  lgsquad2  16005  m1lgs  16007  2sqlem3  16039  2sqlem4  16040  trilpolemeq1  16873  trilpolemlt1  16874  redcwlpolemeq1  16888  nconstwlpolemgt0  16899