Theorem nncni 12179

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 12177	. 2 ⊢ (𝐴 ∈ ℕ → 𝐴 ∈ ℂ)
3	1, 2	ax-mp 5	1 ⊢ 𝐴 ∈ ℂ

Syntax hints:   ∈ wcel 2121  ℂcc 11031  ℕcn 12169

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1975  ax-7 2016  ax-8 2123  ax-9 2131  ax-10 2154  ax-11 2170  ax-12 2191  ax-ext 2713  ax-sep 5221  ax-nul 5231  ax-pr 5365  ax-un 7682  ax-1cn 11091  ax-addcl 11093

This theorem depends on definitions:  df-bi 209  df-an 398  df-or 855  df-3or 1094  df-3an 1095  df-tru 1551  df-fal 1561  df-ex 1788  df-nf 1792  df-sb 2075  df-mo 2545  df-eu 2575  df-clab 2720  df-cleq 2733  df-clel 2816  df-nfc 2890  df-ne 2937  df-ral 3056  df-rex 3066  df-reu 3347  df-rab 3394  df-v 3435  df-sbc 3726  df-csb 3834  df-dif 3888  df-un 3890  df-in 3892  df-ss 3902  df-pss 3905  df-nul 4265  df-if 4458  df-pw 4534  df-sn 4559  df-pr 4561  df-op 4565  df-uni 4842  df-iun 4926  df-br 5076  df-opab 5138  df-mpt 5157  df-tr 5183  df-id 5516  df-eprel 5521  df-po 5529  df-so 5530  df-fr 5574  df-we 5576  df-xp 5627  df-rel 5628  df-cnv 5629  df-co 5630  df-dm 5631  df-rn 5632  df-res 5633  df-ima 5634  df-pred 6256  df-ord 6317  df-on 6318  df-lim 6319  df-suc 6320  df-iota 6445  df-fun 6491  df-fn 6492  df-f 6493  df-f1 6494  df-fo 6495  df-f1o 6496  df-fv 6497  df-ov 7363  df-om 7811  df-2nd 7936  df-frecs 8225  df-wrecs 8256  df-recs 8305  df-rdg 8343  df-nn 12170

This theorem is referenced by:  9p1e10  12641  numnncl2  12662  dec10p  12682  3dec  14223  faclbnd4lem1  14250  4bc2eq6  14286  ef01bndlem  16146  3dvds  16295  divalglem8  16364  pockthi  16873  dec5nprm  17032  dec2nprm  17033  modxai  17034  modxp1i  17036  mod2xnegi  17037  modsubi  17038  23prm  17084  37prm  17086  43prm  17087  83prm  17088  139prm  17089  163prm  17090  1259lem1  17096  1259lem4  17099  2503lem2  17103  4001lem1  17106  4001lem3  17108  mcubic  26833  cubic2  26834  cubic  26835  quart1cl  26840  quart1lem  26841  quart1  26842  quartlem1  26843  quartlem2  26844  log2ublem1  26932  log2ublem2  26933  log2ub  26935  bclbnd  27265  bposlem8  27276  pntlemf  27590  ex-lcm  30550  dpmul10  32977  decdiv10  32978  dp3mul10  32980  dpadd2  32992  dpadd  32993  dpadd3  32994  dpmul  32995  dpmul4  32996  ballotlem2  34685  ballotlemfmpn  34691  ballotth  34734  cnndvlem1  36858  addassnni  42484  addcomnni  42485  mulassnni  42486  mulcomnni  42487  gcdaddmzz2nncomi  42495  lcmeprodgcdi  42507  lcmineqlem6  42534  lcmineqlem23  42551  3lexlogpow5ineq5  42560  sin5tlem5  47354  1t10e1p1e11  47787  deccarry  47788  fmtnoprmfac2lem1  48058  139prmALT  48088  3exp4mod41  48108  41prothprmlem1  48109  2exp340mod341  48238  bgoldbtbndlem1  48310  tgblthelfgott  48320  tgoldbachlt  48321