Theorem 3cn 12267

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 12250	. 2 ⊢ 3 = (2 + 1)
2		2cn 12261	. . 3 ⊢ 2 ∈ ℂ
3		ax-1cn 11126	. . 3 ⊢ 1 ∈ ℂ
4	2, 3	addcli 11180	. 2 ⊢ (2 + 1) ∈ ℂ
5	1, 4	eqeltri 2824	1 ⊢ 3 ∈ ℂ

Syntax hints:   ∈ wcel 2109  (class class class)co 7387  ℂcc 11066  1c1 11069   + caddc 11071  2c2 12241  3c3 12242

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-1cn 11126  ax-addcl 11128

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2721  df-clel 2803  df-2 12249  df-3 12250

This theorem is referenced by:  3ex  12268  4cn  12271  4m1e3  12310  3p2e5  12332  3p3e6  12333  4p4e8  12336  5p4e9  12339  3t1e3  12346  3t2e6  12347  3t3e9  12348  8th4div3  12402  halfthird  12403  halfpm6th  12404  6p4e10  12721  9t8e72  12777  sq3  14163  expnass  14173  fac3  14245  01sqrexlem7  15214  caurcvgr  15640  bpoly2  16023  bpoly3  16024  bpoly4  16025  ef01bndlem  16152  sin01bnd  16153  cos01bnd  16154  cos1bnd  16155  cos2bnd  16156  cos01gt0  16159  rpnnen2lem3  16184  rpnnen2lem11  16192  3dvdsdec  16302  3dvds2dec  16303  5ndvds3  16383  3lcm2e6woprm  16585  prmo3  17012  2exp6  17057  2exp16  17061  7prm  17081  13prm  17086  17prm  17087  19prm  17088  37prm  17091  43prm  17092  83prm  17093  139prm  17094  163prm  17095  317prm  17096  631prm  17097  1259lem1  17101  1259lem2  17102  1259lem3  17103  1259lem4  17104  1259lem5  17105  1259prm  17106  2503lem1  17107  2503lem2  17108  2503lem3  17109  2503prm  17110  4001lem1  17111  4001lem2  17112  4001lem3  17113  4001lem4  17114  4001prm  17115  tangtx  26414  sincos6thpi  26425  sincos3rdpi  26426  pigt3  26427  pige3ALT  26429  2logb9irrALT  26708  ang180lem2  26720  1cubr  26752  dcubic1lem  26753  dcubic2  26754  dcubic1  26755  dcubic  26756  mcubic  26757  cubic2  26758  cubic  26759  binom4  26760  quart1cl  26764  quart1lem  26765  quart1  26766  quartlem1  26767  quartlem3  26769  log2cnv  26854  log2tlbnd  26855  log2ublem2  26857  log2ublem3  26858  log2ub  26859  basellem5  26995  basellem8  26998  basellem9  26999  cht3  27083  ppiub  27115  chtub  27123  bclbnd  27191  bposlem6  27200  bposlem8  27202  bposlem9  27203  lgsdir2lem1  27236  lgsdir2lem5  27240  2lgslem3b  27308  2lgslem3d  27310  2lgsoddprmlem3c  27323  2lgsoddprmlem3d  27324  addsqnreup  27354  pntibndlem1  27500  pntlemk  27517  ex-opab  30361  ex-exp  30379  ex-dvds  30385  ex-gcd  30386  ex-lcm  30387  ex-prmo  30388  ex-ind-dvds  30390  ply1dg3rt0irred  33551  2sqr3minply  33770  2sqr3nconstr  33771  cos9thpiminplylem2  33773  cos9thpiminplylem3  33774  cos9thpiminplylem4  33775  cos9thpiminplylem5  33776  cos9thpiminply  33778  cos9thpinconstrlem1  33779  cos9thpinconstrlem2  33780  cos9thpinconstr  33781  fib5  34396  fib6  34397  hgt750lem  34642  hgt750lem2  34643  hgt750leme  34649  problem4  35655  problem5  35656  sinccvglem  35659  mblfinlem3  37653  itg2addnclem2  37666  itg2addnclem3  37667  heiborlem6  37810  heiborlem7  37811  3exp7  42041  3lexlogpow2ineq2  42047  3lexlogpow5ineq5  42048  aks4d1p1  42064  2ap1caineq  42133  3rdpwhole  42280  235t711  42293  ex-decpmul  42294  tan3rdpi  42340  sin2t3rdpi  42341  cos2t3rdpi  42342  sin4t3rdpi  42343  cos4t3rdpi  42344  cu3addd  42669  3cubeslem3l  42674  3cubeslem3r  42675  jm2.23  42985  inductionexd  44144  lhe4.4ex1a  44318  stoweidlem13  46011  stoweidlem26  46024  stoweidlem34  46032  wallispilem4  46066  wallispi2lem1  46069  ceil5half3  47341  fmtno5lem1  47554  fmtno5lem2  47555  257prm  47562  fmtno4prmfac  47573  fmtno4nprmfac193  47575  139prmALT  47597  127prm  47600  mod42tp1mod8  47603  3exp4mod41  47617  41prothprmlem2  47619  6even  47712  11t31e341  47733  2exp340mod341  47734  gbpart8  47769  sbgoldbwt  47778  sbgoldbst  47779  evengpop3  47799  evengpoap3  47800  nnsum4primeseven  47801  nnsum4primesevenALTV  47802  2t6m3t4e0  48336  linevalexample  48384  zlmodzxzequa  48485  zlmodzxzequap  48488  ackval3  48672  ackval2012  48680  ackval3012  48681  ackval41  48684  ackval42  48685