Theorem 3cn 12290

Description: The number 3 is a complex number. (Contributed by FL, 17-Oct-2010.) Reduce dependencies on axioms. (Revised by Steven Nguyen, 4-Oct-2022.)

Assertion

Ref	Expression
3cn	⊢ 3 ∈ ℂ

Proof of Theorem 3cn

Step	Hyp	Ref	Expression
1		df-3 12273	. 2 ⊢ 3 = (2 + 1)
2		2cn 12284	. . 3 ⊢ 2 ∈ ℂ
3		ax-1cn 11165	. . 3 ⊢ 1 ∈ ℂ
4	2, 3	addcli 11217	. 2 ⊢ (2 + 1) ∈ ℂ
5	1, 4	eqeltri 2830	1 ⊢ 3 ∈ ℂ

Syntax hints:   ∈ wcel 2107  (class class class)co 7406  ℂcc 11105  1c1 11108   + caddc 11110  2c2 12264  3c3 12265

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704  ax-1cn 11165  ax-addcl 11167

This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-cleq 2725  df-clel 2811  df-2 12272  df-3 12273

This theorem is referenced by:  3ex  12291  4cn  12294  4m1e3  12338  3p2e5  12360  3p3e6  12361  4p4e8  12364  5p4e9  12367  3t1e3  12374  3t2e6  12375  3t3e9  12376  8th4div3  12429  halfpm6th  12430  6p4e10  12746  9t8e72  12802  halfthird  12817  sq3  14159  expnass  14169  fac3  14237  01sqrexlem7  15192  caurcvgr  15617  bpoly2  15998  bpoly3  15999  bpoly4  16000  ef01bndlem  16124  sin01bnd  16125  cos01bnd  16126  cos1bnd  16127  cos2bnd  16128  cos01gt0  16131  rpnnen2lem3  16156  rpnnen2lem11  16164  3dvdsdec  16272  3dvds2dec  16273  3lcm2e6woprm  16549  prmo3  16971  2exp6  17017  2exp16  17021  7prm  17041  13prm  17046  17prm  17047  19prm  17048  37prm  17051  43prm  17052  83prm  17053  139prm  17054  163prm  17055  317prm  17056  631prm  17057  1259lem1  17061  1259lem2  17062  1259lem3  17063  1259lem4  17064  1259lem5  17065  1259prm  17066  2503lem1  17067  2503lem2  17068  2503lem3  17069  2503prm  17070  4001lem1  17071  4001lem2  17072  4001lem3  17073  4001lem4  17074  4001prm  17075  tangtx  26007  sincos6thpi  26017  sincos3rdpi  26018  pigt3  26019  pige3ALT  26021  2logb9irrALT  26293  ang180lem2  26305  1cubr  26337  dcubic1lem  26338  dcubic2  26339  dcubic1  26340  dcubic  26341  mcubic  26342  cubic2  26343  cubic  26344  binom4  26345  quart1cl  26349  quart1lem  26350  quart1  26351  quartlem1  26352  quartlem3  26354  log2cnv  26439  log2tlbnd  26440  log2ublem2  26442  log2ublem3  26443  log2ub  26444  basellem5  26579  basellem8  26582  basellem9  26583  cht3  26667  ppiub  26697  chtub  26705  bclbnd  26773  bposlem6  26782  bposlem8  26784  bposlem9  26785  lgsdir2lem1  26818  lgsdir2lem5  26822  2lgslem3b  26890  2lgslem3d  26892  2lgsoddprmlem3c  26905  2lgsoddprmlem3d  26906  addsqnreup  26936  pntibndlem1  27082  pntlemk  27099  ex-opab  29675  ex-exp  29693  ex-dvds  29699  ex-gcd  29700  ex-lcm  29701  ex-prmo  29702  ex-ind-dvds  29704  fib5  33393  fib6  33394  hgt750lem  33652  hgt750lem2  33653  hgt750leme  33659  problem4  34642  problem5  34643  sinccvglem  34646  mblfinlem3  36516  itg2addnclem2  36529  itg2addnclem3  36530  heiborlem6  36673  heiborlem7  36674  3exp7  40907  3lexlogpow2ineq2  40913  3lexlogpow5ineq5  40914  aks4d1p1  40930  2ap1caineq  40950  fac2xp3  41009  235t711  41201  ex-decpmul  41202  cu3addd  41404  3cubeslem3l  41410  3cubeslem3r  41411  jm2.23  41721  inductionexd  42892  lhe4.4ex1a  43074  stoweidlem13  44716  stoweidlem26  44729  stoweidlem34  44737  wallispilem4  44771  wallispi2lem1  44774  fmtno5lem1  46208  fmtno5lem2  46209  257prm  46216  fmtno4prmfac  46227  fmtno4nprmfac193  46229  139prmALT  46251  127prm  46254  mod42tp1mod8  46257  3exp4mod41  46271  41prothprmlem2  46273  6even  46366  11t31e341  46387  2exp340mod341  46388  gbpart8  46423  sbgoldbwt  46432  sbgoldbst  46433  evengpop3  46453  evengpoap3  46454  nnsum4primeseven  46455  nnsum4primesevenALTV  46456  2t6m3t4e0  46978  linevalexample  47030  zlmodzxzequa  47131  zlmodzxzequap  47134  ackval3  47323  ackval2012  47331  ackval3012  47332  ackval41  47335  ackval42  47336