Theorem nncni 12226

Description: A positive integer is a complex number. (Contributed by NM, 18-Aug-1999.) Reduce dependencies on axioms. (Revised by Steven Nguyen, 4-Oct-2022.)

Hypothesis

Ref	Expression
nnre.1	⊢ 𝐴 ∈ ℕ

Assertion

Ref	Expression
nncni	⊢ 𝐴 ∈ ℂ

Proof of Theorem nncni

Step	Hyp	Ref	Expression
1		nnre.1	. 2 ⊢ 𝐴 ∈ ℕ
2		nncn 12224	. 2 ⊢ (𝐴 ∈ ℕ → 𝐴 ∈ ℂ)
3	1, 2	ax-mp 5	1 ⊢ 𝐴 ∈ ℂ

Syntax hints:   ∈ wcel 2106  ℂcc 11110  ℕcn 12216

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2703  ax-sep 5299  ax-nul 5306  ax-pr 5427  ax-un 7727  ax-1cn 11170  ax-addcl 11172

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ne 2941  df-ral 3062  df-rex 3071  df-reu 3377  df-rab 3433  df-v 3476  df-sbc 3778  df-csb 3894  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-pss 3967  df-nul 4323  df-if 4529  df-pw 4604  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-iun 4999  df-br 5149  df-opab 5211  df-mpt 5232  df-tr 5266  df-id 5574  df-eprel 5580  df-po 5588  df-so 5589  df-fr 5631  df-we 5633  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-rn 5687  df-res 5688  df-ima 5689  df-pred 6300  df-ord 6367  df-on 6368  df-lim 6369  df-suc 6370  df-iota 6495  df-fun 6545  df-fn 6546  df-f 6547  df-f1 6548  df-fo 6549  df-f1o 6550  df-fv 6551  df-ov 7414  df-om 7858  df-2nd 7978  df-frecs 8268  df-wrecs 8299  df-recs 8373  df-rdg 8412  df-nn 12217

This theorem is referenced by:  9p1e10  12683  numnncl2  12704  dec10p  12724  3dec  14230  faclbnd4lem1  14257  4bc2eq6  14293  ef01bndlem  16131  3dvds  16278  divalglem8  16347  pockthi  16844  dec5nprm  17003  dec2nprm  17004  modxai  17005  modxp1i  17007  mod2xnegi  17008  modsubi  17009  23prm  17056  37prm  17058  43prm  17059  83prm  17060  139prm  17061  163prm  17062  1259lem1  17068  1259lem4  17071  2503lem2  17075  4001lem1  17078  4001lem3  17080  mcubic  26576  cubic2  26577  cubic  26578  quart1cl  26583  quart1lem  26584  quart1  26585  quartlem1  26586  quartlem2  26587  log2ublem1  26675  log2ublem2  26676  log2ub  26678  bclbnd  27007  bposlem8  27018  pntlemf  27332  ex-lcm  29966  dpmul10  32316  decdiv10  32317  dp3mul10  32319  dpadd2  32331  dpadd  32332  dpadd3  32333  dpmul  32334  dpmul4  32335  ballotlem2  33773  ballotlemfmpn  33779  ballotth  33822  cnndvlem1  35716  addassnni  41156  addcomnni  41157  mulassnni  41158  mulcomnni  41159  gcdaddmzz2nncomi  41167  lcmeprodgcdi  41178  lcmineqlem6  41205  lcmineqlem23  41222  3lexlogpow5ineq5  41231  1t10e1p1e11  46317  deccarry  46318  fmtnoprmfac2lem1  46533  139prmALT  46563  3exp4mod41  46583  41prothprmlem1  46584  2exp340mod341  46700  bgoldbtbndlem1  46772  tgblthelfgott  46782  tgoldbachlt  46783