Theorem 3cn 12226

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 12209	. 2 ⊢ 3 = (2 + 1)
2		2cn 12220	. . 3 ⊢ 2 ∈ ℂ
3		ax-1cn 11084	. . 3 ⊢ 1 ∈ ℂ
4	2, 3	addcli 11138	. 2 ⊢ (2 + 1) ∈ ℂ
5	1, 4	eqeltri 2832	1 ⊢ 3 ∈ ℂ

Syntax hints:   ∈ wcel 2113  (class class class)co 7358  ℂcc 11024  1c1 11027   + caddc 11029  2c2 12200  3c3 12201

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708  ax-1cn 11084  ax-addcl 11086

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2728  df-clel 2811  df-2 12208  df-3 12209

This theorem is referenced by:  3ex  12227  4cn  12230  4m1e3  12269  3p2e5  12291  3p3e6  12292  4p4e8  12295  5p4e9  12298  3t1e3  12305  3t2e6  12306  3t3e9  12307  8th4div3  12361  halfthird  12362  halfpm6th  12363  6p4e10  12679  9t8e72  12735  sq3  14121  expnass  14131  fac3  14203  01sqrexlem7  15171  caurcvgr  15597  bpoly2  15980  bpoly3  15981  bpoly4  15982  ef01bndlem  16109  sin01bnd  16110  cos01bnd  16111  cos1bnd  16112  cos2bnd  16113  cos01gt0  16116  rpnnen2lem3  16141  rpnnen2lem11  16149  3dvdsdec  16259  3dvds2dec  16260  5ndvds3  16340  3lcm2e6woprm  16542  prmo3  16969  2exp6  17014  2exp16  17018  7prm  17038  13prm  17043  17prm  17044  19prm  17045  37prm  17048  43prm  17049  83prm  17050  139prm  17051  163prm  17052  317prm  17053  631prm  17054  1259lem1  17058  1259lem2  17059  1259lem3  17060  1259lem4  17061  1259lem5  17062  1259prm  17063  2503lem1  17064  2503lem2  17065  2503lem3  17066  2503prm  17067  4001lem1  17068  4001lem2  17069  4001lem3  17070  4001lem4  17071  4001prm  17072  tangtx  26470  sincos6thpi  26481  sincos3rdpi  26482  pigt3  26483  pige3ALT  26485  2logb9irrALT  26764  ang180lem2  26776  1cubr  26808  dcubic1lem  26809  dcubic2  26810  dcubic1  26811  dcubic  26812  mcubic  26813  cubic2  26814  cubic  26815  binom4  26816  quart1cl  26820  quart1lem  26821  quart1  26822  quartlem1  26823  quartlem3  26825  log2cnv  26910  log2tlbnd  26911  log2ublem2  26913  log2ublem3  26914  log2ub  26915  basellem5  27051  basellem8  27054  basellem9  27055  cht3  27139  ppiub  27171  chtub  27179  bclbnd  27247  bposlem6  27256  bposlem8  27258  bposlem9  27259  lgsdir2lem1  27292  lgsdir2lem5  27296  2lgslem3b  27364  2lgslem3d  27366  2lgsoddprmlem3c  27379  2lgsoddprmlem3d  27380  addsqnreup  27410  pntibndlem1  27556  pntlemk  27573  ex-opab  30507  ex-exp  30525  ex-dvds  30531  ex-gcd  30532  ex-lcm  30533  ex-prmo  30534  ex-ind-dvds  30536  ply1dg3rt0irred  33665  2sqr3minply  33937  2sqr3nconstr  33938  cos9thpiminplylem2  33940  cos9thpiminplylem3  33941  cos9thpiminplylem4  33942  cos9thpiminplylem5  33943  cos9thpiminply  33945  cos9thpinconstrlem1  33946  cos9thpinconstrlem2  33947  cos9thpinconstr  33948  fib5  34562  fib6  34563  hgt750lem  34808  hgt750lem2  34809  hgt750leme  34815  problem4  35862  problem5  35863  sinccvglem  35866  mblfinlem3  37856  itg2addnclem2  37869  itg2addnclem3  37870  heiborlem6  38013  heiborlem7  38014  3exp7  42303  3lexlogpow2ineq2  42309  3lexlogpow5ineq5  42310  aks4d1p1  42326  2ap1caineq  42395  3rdpwhole  42543  235t711  42556  ex-decpmul  42557  tan3rdpi  42603  sin2t3rdpi  42604  cos2t3rdpi  42605  sin4t3rdpi  42606  cos4t3rdpi  42607  cu3addd  42919  3cubeslem3l  42924  3cubeslem3r  42925  jm2.23  43234  inductionexd  44392  lhe4.4ex1a  44566  stoweidlem13  46253  stoweidlem26  46266  stoweidlem34  46274  wallispilem4  46308  wallispi2lem1  46311  ceil5half3  47582  fmtno5lem1  47795  fmtno5lem2  47796  257prm  47803  fmtno4prmfac  47814  fmtno4nprmfac193  47816  139prmALT  47838  127prm  47841  mod42tp1mod8  47844  3exp4mod41  47858  41prothprmlem2  47860  6even  47953  11t31e341  47974  2exp340mod341  47975  gbpart8  48010  sbgoldbwt  48019  sbgoldbst  48020  evengpop3  48040  evengpoap3  48041  nnsum4primeseven  48042  nnsum4primesevenALTV  48043  2t6m3t4e0  48590  linevalexample  48637  zlmodzxzequa  48738  zlmodzxzequap  48741  ackval3  48925  ackval2012  48933  ackval3012  48934  ackval41  48937  ackval42  48938