Theorem nncni 11726

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

Syntax hints:   ∈ wcel 2114  ℂcc 10613  ℕcn 11716

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2020  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2162  ax-12 2179  ax-ext 2710  ax-sep 5167  ax-nul 5174  ax-pr 5296  ax-un 7479  ax-1cn 10673  ax-addcl 10675

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1787  df-nf 1791  df-sb 2075  df-mo 2540  df-eu 2570  df-clab 2717  df-cleq 2730  df-clel 2811  df-nfc 2881  df-ne 2935  df-ral 3058  df-rex 3059  df-reu 3060  df-rab 3062  df-v 3400  df-sbc 3681  df-csb 3791  df-dif 3846  df-un 3848  df-in 3850  df-ss 3860  df-pss 3862  df-nul 4212  df-if 4415  df-pw 4490  df-sn 4517  df-pr 4519  df-tp 4521  df-op 4523  df-uni 4797  df-iun 4883  df-br 5031  df-opab 5093  df-mpt 5111  df-tr 5137  df-id 5429  df-eprel 5434  df-po 5442  df-so 5443  df-fr 5483  df-we 5485  df-xp 5531  df-rel 5532  df-cnv 5533  df-co 5534  df-dm 5535  df-rn 5536  df-res 5537  df-ima 5538  df-pred 6129  df-ord 6175  df-on 6176  df-lim 6177  df-suc 6178  df-iota 6297  df-fun 6341  df-fn 6342  df-f 6343  df-f1 6344  df-fo 6345  df-f1o 6346  df-fv 6347  df-ov 7173  df-om 7600  df-wrecs 7976  df-recs 8037  df-rdg 8075  df-nn 11717

This theorem is referenced by:  9p1e10  12181  numnncl2  12202  dec10p  12222  3dec  13718  faclbnd4lem1  13745  4bc2eq6  13781  ef01bndlem  15629  3dvds  15776  divalglem8  15845  pockthi  16343  dec5nprm  16502  dec2nprm  16503  modxai  16504  modxp1i  16506  mod2xnegi  16507  modsubi  16508  23prm  16555  37prm  16557  43prm  16558  83prm  16559  139prm  16560  163prm  16561  1259lem1  16567  1259lem4  16570  2503lem2  16574  4001lem1  16577  4001lem3  16579  mcubic  25585  cubic2  25586  cubic  25587  quart1cl  25592  quart1lem  25593  quart1  25594  quartlem1  25595  quartlem2  25596  log2ublem1  25684  log2ublem2  25685  log2ub  25687  bclbnd  26016  bposlem8  26027  pntlemf  26341  ex-lcm  28395  dpmul10  30744  decdiv10  30745  dp3mul10  30747  dpadd2  30759  dpadd  30760  dpadd3  30761  dpmul  30762  dpmul4  30763  ballotlem2  32025  ballotlemfmpn  32031  ballotth  32074  cnndvlem1  34355  addassnni  39613  addcomnni  39614  mulassnni  39615  mulcomnni  39616  gcdaddmzz2nncomi  39624  lcmeprodgcdi  39635  lcmineqlem6  39662  lcmineqlem23  39679  3lexlogpow5ineq5  39688  1t10e1p1e11  44336  deccarry  44337  fmtnoprmfac2lem1  44552  139prmALT  44582  3exp4mod41  44602  41prothprmlem1  44603  2exp340mod341  44719  bgoldbtbndlem1  44791  tgblthelfgott  44801  tgoldbachlt  44802