Theorem nncnd 8644

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

Syntax hints:   → wi 4   ∈ wcel 1463  ℂcc 7545  ℕcn 8630

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 681  ax-5 1406  ax-7 1407  ax-gen 1408  ax-ie1 1452  ax-ie2 1453  ax-8 1465  ax-10 1466  ax-11 1467  ax-i12 1468  ax-bndl 1469  ax-4 1470  ax-17 1489  ax-i9 1493  ax-ial 1497  ax-i5r 1498  ax-ext 2097  ax-sep 4006  ax-cnex 7636  ax-resscn 7637  ax-1re 7639  ax-addrcl 7642

This theorem depends on definitions:  df-bi 116  df-tru 1317  df-nf 1420  df-sb 1719  df-clab 2102  df-cleq 2108  df-clel 2111  df-nfc 2244  df-ral 2395  df-v 2659  df-in 3043  df-ss 3050  df-int 3738  df-inn 8631

This theorem is referenced by:  peano5uzti  9063  qapne  9333  qtri3or  9913  exbtwnzlemstep  9918  intfracq  9986  flqdiv  9987  modqmulnn  10008  addmodid  10038  modaddmodup  10053  modsumfzodifsn  10062  addmodlteq  10064  facdiv  10377  facndiv  10378  faclbnd  10380  faclbnd6  10383  facubnd  10384  facavg  10385  bccmpl  10393  bcn0  10394  bcn1  10397  bcm1k  10399  bcp1n  10400  bcp1nk  10401  bcval5  10402  bcpasc  10405  permnn  10410  cvg1nlemcxze  10646  cvg1nlemcau  10648  resqrexlemcalc3  10680  binom11  11147  binom1dif  11148  divcnv  11158  arisum2  11160  trireciplem  11161  trirecip  11162  expcnvap0  11163  geo2sum  11175  geo2lim  11177  cvgratnnlembern  11184  cvgratnnlemnexp  11185  cvgratnnlemmn  11186  cvgratnnlemsumlt  11189  cvgratnnlemfm  11190  cvgratnnlemrate  11191  cvgratz  11193  eftcl  11211  eftabs  11213  efcllemp  11215  ege2le3  11228  efcj  11230  efaddlem  11231  eftlub  11247  eirraplem  11331  oexpneg  11422  divalglemnn  11463  bezoutlemnewy  11530  mulgcd  11550  rplpwr  11561  sqgcd  11563  lcmgcdlem  11604  3lcm2e6woprm  11613  cncongr1  11630  cncongr2  11631  prmind2  11647  divgcdodd  11667  prmdvdsexpr  11674  sqrt2irrlem  11685  oddpwdclemxy  11692  oddpwdclemodd  11695  oddpwdclemdc  11696  oddpwdc  11697  sqpweven  11698  2sqpwodd  11699  sqrt2irraplemnn  11702  sqrt2irrap  11703  qmuldeneqnum  11718  divnumden  11719  qnumgt0  11721  numdensq  11725  hashdvds  11742  phiprmpw  11743  oddennn  11750  evenennn  11751  trilpolemeq1  12925  trilpolemlt1  12926