Theorem 3cn 12206

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 12189	. 2 ⊢ 3 = (2 + 1)
2		2cn 12200	. . 3 ⊢ 2 ∈ ℂ
3		ax-1cn 11064	. . 3 ⊢ 1 ∈ ℂ
4	2, 3	addcli 11118	. 2 ⊢ (2 + 1) ∈ ℂ
5	1, 4	eqeltri 2827	1 ⊢ 3 ∈ ℂ

Syntax hints:   ∈ wcel 2111  (class class class)co 7346  ℂcc 11004  1c1 11007   + caddc 11009  2c2 12180  3c3 12181

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 2113  ax-9 2121  ax-ext 2703  ax-1cn 11064  ax-addcl 11066

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2723  df-clel 2806  df-2 12188  df-3 12189

This theorem is referenced by:  3ex  12207  4cn  12210  4m1e3  12249  3p2e5  12271  3p3e6  12272  4p4e8  12275  5p4e9  12278  3t1e3  12285  3t2e6  12286  3t3e9  12287  8th4div3  12341  halfthird  12342  halfpm6th  12343  6p4e10  12660  9t8e72  12716  sq3  14105  expnass  14115  fac3  14187  01sqrexlem7  15155  caurcvgr  15581  bpoly2  15964  bpoly3  15965  bpoly4  15966  ef01bndlem  16093  sin01bnd  16094  cos01bnd  16095  cos1bnd  16096  cos2bnd  16097  cos01gt0  16100  rpnnen2lem3  16125  rpnnen2lem11  16133  3dvdsdec  16243  3dvds2dec  16244  5ndvds3  16324  3lcm2e6woprm  16526  prmo3  16953  2exp6  16998  2exp16  17002  7prm  17022  13prm  17027  17prm  17028  19prm  17029  37prm  17032  43prm  17033  83prm  17034  139prm  17035  163prm  17036  317prm  17037  631prm  17038  1259lem1  17042  1259lem2  17043  1259lem3  17044  1259lem4  17045  1259lem5  17046  1259prm  17047  2503lem1  17048  2503lem2  17049  2503lem3  17050  2503prm  17051  4001lem1  17052  4001lem2  17053  4001lem3  17054  4001lem4  17055  4001prm  17056  tangtx  26441  sincos6thpi  26452  sincos3rdpi  26453  pigt3  26454  pige3ALT  26456  2logb9irrALT  26735  ang180lem2  26747  1cubr  26779  dcubic1lem  26780  dcubic2  26781  dcubic1  26782  dcubic  26783  mcubic  26784  cubic2  26785  cubic  26786  binom4  26787  quart1cl  26791  quart1lem  26792  quart1  26793  quartlem1  26794  quartlem3  26796  log2cnv  26881  log2tlbnd  26882  log2ublem2  26884  log2ublem3  26885  log2ub  26886  basellem5  27022  basellem8  27025  basellem9  27026  cht3  27110  ppiub  27142  chtub  27150  bclbnd  27218  bposlem6  27227  bposlem8  27229  bposlem9  27230  lgsdir2lem1  27263  lgsdir2lem5  27267  2lgslem3b  27335  2lgslem3d  27337  2lgsoddprmlem3c  27350  2lgsoddprmlem3d  27351  addsqnreup  27381  pntibndlem1  27527  pntlemk  27544  ex-opab  30412  ex-exp  30430  ex-dvds  30436  ex-gcd  30437  ex-lcm  30438  ex-prmo  30439  ex-ind-dvds  30441  ply1dg3rt0irred  33546  2sqr3minply  33793  2sqr3nconstr  33794  cos9thpiminplylem2  33796  cos9thpiminplylem3  33797  cos9thpiminplylem4  33798  cos9thpiminplylem5  33799  cos9thpiminply  33801  cos9thpinconstrlem1  33802  cos9thpinconstrlem2  33803  cos9thpinconstr  33804  fib5  34418  fib6  34419  hgt750lem  34664  hgt750lem2  34665  hgt750leme  34671  problem4  35712  problem5  35713  sinccvglem  35716  mblfinlem3  37709  itg2addnclem2  37722  itg2addnclem3  37723  heiborlem6  37866  heiborlem7  37867  3exp7  42156  3lexlogpow2ineq2  42162  3lexlogpow5ineq5  42163  aks4d1p1  42179  2ap1caineq  42248  3rdpwhole  42395  235t711  42408  ex-decpmul  42409  tan3rdpi  42455  sin2t3rdpi  42456  cos2t3rdpi  42457  sin4t3rdpi  42458  cos4t3rdpi  42459  cu3addd  42784  3cubeslem3l  42789  3cubeslem3r  42790  jm2.23  43099  inductionexd  44258  lhe4.4ex1a  44432  stoweidlem13  46121  stoweidlem26  46134  stoweidlem34  46142  wallispilem4  46176  wallispi2lem1  46179  ceil5half3  47450  fmtno5lem1  47663  fmtno5lem2  47664  257prm  47671  fmtno4prmfac  47682  fmtno4nprmfac193  47684  139prmALT  47706  127prm  47709  mod42tp1mod8  47712  3exp4mod41  47726  41prothprmlem2  47728  6even  47821  11t31e341  47842  2exp340mod341  47843  gbpart8  47878  sbgoldbwt  47887  sbgoldbst  47888  evengpop3  47908  evengpoap3  47909  nnsum4primeseven  47910  nnsum4primesevenALTV  47911  2t6m3t4e0  48458  linevalexample  48506  zlmodzxzequa  48607  zlmodzxzequap  48610  ackval3  48794  ackval2012  48802  ackval3012  48803  ackval41  48806  ackval42  48807