Theorem nncnd 8053

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

Syntax hints:   → wi 4   ∈ wcel 1433  ℂcc 6979  ℕcn 8039

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-io 662  ax-5 1376  ax-7 1377  ax-gen 1378  ax-ie1 1422  ax-ie2 1423  ax-8 1435  ax-10 1436  ax-11 1437  ax-i12 1438  ax-bndl 1439  ax-4 1440  ax-17 1459  ax-i9 1463  ax-ial 1467  ax-i5r 1468  ax-ext 2063  ax-sep 3896  ax-cnex 7067  ax-resscn 7068  ax-1re 7070  ax-addrcl 7073

This theorem depends on definitions:  df-bi 115  df-tru 1287  df-nf 1390  df-sb 1686  df-clab 2068  df-cleq 2074  df-clel 2077  df-nfc 2208  df-ral 2353  df-v 2603  df-in 2979  df-ss 2986  df-int 3637  df-inn 8040

This theorem is referenced by:  peano5uzti  8455  qapne  8724  qtri3or  9252  qbtwnzlemstep  9257  intfracq  9322  flqdiv  9323  modqmulnn  9344  addmodid  9374  modaddmodup  9389  modsumfzodifsn  9398  addmodlteq  9400  facdiv  9665  facndiv  9666  faclbnd  9668  faclbnd6  9671  facubnd  9672  facavg  9673  bccmpl  9681  bcn0  9682  bcn1  9685  bcm1k  9687  bcp1n  9688  bcp1nk  9689  ibcval5  9690  bcpasc  9693  permnn  9698  cvg1nlemcxze  9868  cvg1nlemcau  9870  resqrexlemcalc3  9902  oexpneg  10276  divalglemnn  10318  bezoutlemnewy  10385  mulgcd  10405  rplpwr  10416  sqgcd  10418  lcmgcdlem  10459  3lcm2e6woprm  10468  cncongr1  10485  cncongr2  10486  prmind2  10502  divgcdodd  10522  prmdvdsexpr  10529  sqrt2irrlem  10540  oddpwdclemxy  10547  oddpwdclemodd  10550  oddpwdclemdc  10551  oddpwdc  10552  sqpweven  10553  2sqpwodd  10554  sqrt2irraplemnn  10557  sqrt2irrap  10558