Theorem nncni 12244

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

Syntax hints:   ∈ wcel 2143  ℂcc 11099  ℕcn 12234

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-10 2176  ax-11 2192  ax-12 2213  ax-ext 2735  ax-sep 5258  ax-nul 5270  ax-pr 5406  ax-un 7734  ax-1cn 11159  ax-addcl 11161

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-nf 1814  df-sb 2097  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2838  df-nfc 2912  df-ne 2959  df-ral 3080  df-rex 3090  df-reu 3370  df-rab 3417  df-v 3457  df-sbc 3746  df-csb 3855  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-pss 3926  df-nul 4288  df-if 4489  df-pw 4565  df-sn 4591  df-pr 4593  df-op 4597  df-uni 4874  df-iun 4959  df-br 5111  df-opab 5175  df-mpt 5194  df-tr 5220  df-id 5558  df-eprel 5563  df-po 5571  df-so 5572  df-fr 5616  df-we 5618  df-xp 5669  df-rel 5670  df-cnv 5671  df-co 5672  df-dm 5673  df-rn 5674  df-res 5675  df-ima 5676  df-pred 6304  df-ord 6365  df-on 6366  df-lim 6367  df-suc 6368  df-iota 6494  df-fun 6540  df-fn 6541  df-f 6542  df-f1 6543  df-fo 6544  df-f1o 6545  df-fv 6546  df-ov 7415  df-om 7864  df-2nd 7988  df-frecs 8279  df-wrecs 8310  df-recs 8359  df-rdg 8398  df-nn 12235

This theorem is referenced by:  9p1e10  12714  numnncl2  12740  dec10p  12760  3dec  14304  faclbnd4lem1  14331  4bc2eq6  14367  ef01bndlem  16241  3dvds  16390  divalglem8  16459  pockthi  16968  dec5nprm  17127  dec2nprm  17128  modxai  17129  modxp1i  17131  mod2xnegi  17132  modsubi  17133  23prm  17180  37prm  17182  43prm  17183  83prm  17184  139prm  17185  163prm  17186  1259lem1  17192  1259lem4  17195  2503lem2  17199  4001lem1  17202  4001lem3  17204  mcubic  26990  cubic2  26991  cubic  26992  quart1cl  26997  quart1lem  26998  quart1  26999  quartlem1  27000  quartlem2  27001  log2ublem1  27089  log2ublem2  27090  log2ub  27092  bclbnd  27422  bposlem8  27433  pntlemf  27747  ex-lcm  30787  dpmul10  33192  decdiv10  33193  dp3mul10  33195  dpadd2  33207  dpadd  33208  dpadd3  33209  dpmul  33210  dpmul4  33211  ballotlem2  34857  ballotlemfmpn  34863  ballotth  34906  cnndvlem1  37104  addassnni  42729  addcomnni  42730  mulassnni  42731  mulcomnni  42732  gcdaddmzz2nncomi  42740  lcmeprodgcdi  42752  lcmineqlem6  42779  lcmineqlem23  42796  3lexlogpow5ineq5  42805  sin5tlem5  47591  1t10e1p1e11  48024  deccarry  48025  fmtnoprmfac2lem1  48295  139prmALT  48325  3exp4mod41  48345  41prothprmlem1  48346  2exp340mod341  48475  bgoldbtbndlem1  48547  tgblthelfgott  48557  tgoldbachlt  48558