Theorem 3cn 12355

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 12338	. 2 ⊢ 3 = (2 + 1)
2		2cn 12349	. . 3 ⊢ 2 ∈ ℂ
3		ax-1cn 11223	. . 3 ⊢ 1 ∈ ℂ
4	2, 3	addcli 11277	. 2 ⊢ (2 + 1) ∈ ℂ
5	1, 4	eqeltri 2825	1 ⊢ 3 ∈ ℂ

Syntax hints:   ∈ wcel 2100  (class class class)co 7430  ℂcc 11163  1c1 11166   + caddc 11168  2c2 12329  3c3 12330

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2102  ax-9 2110  ax-ext 2700  ax-1cn 11223  ax-addcl 11225

This theorem depends on definitions:  df-bi 206  df-an 395  df-ex 1775  df-cleq 2721  df-clel 2806  df-2 12337  df-3 12338

This theorem is referenced by:  3ex  12356  4cn  12359  4m1e3  12403  3p2e5  12425  3p3e6  12426  4p4e8  12429  5p4e9  12432  3t1e3  12439  3t2e6  12440  3t3e9  12441  8th4div3  12494  halfpm6th  12495  6p4e10  12811  9t8e72  12867  halfthird  12882  sq3  14227  expnass  14237  fac3  14309  01sqrexlem7  15274  caurcvgr  15699  bpoly2  16080  bpoly3  16081  bpoly4  16082  ef01bndlem  16207  sin01bnd  16208  cos01bnd  16209  cos1bnd  16210  cos2bnd  16211  cos01gt0  16214  rpnnen2lem3  16239  rpnnen2lem11  16247  3dvdsdec  16355  3dvds2dec  16356  3lcm2e6woprm  16637  prmo3  17064  2exp6  17110  2exp16  17114  7prm  17134  13prm  17139  17prm  17140  19prm  17141  37prm  17144  43prm  17145  83prm  17146  139prm  17147  163prm  17148  317prm  17149  631prm  17150  1259lem1  17154  1259lem2  17155  1259lem3  17156  1259lem4  17157  1259lem5  17158  1259prm  17159  2503lem1  17160  2503lem2  17161  2503lem3  17162  2503prm  17163  4001lem1  17164  4001lem2  17165  4001lem3  17166  4001lem4  17167  4001prm  17168  tangtx  26556  sincos6thpi  26566  sincos3rdpi  26567  pigt3  26568  pige3ALT  26570  2logb9irrALT  26849  ang180lem2  26861  1cubr  26893  dcubic1lem  26894  dcubic2  26895  dcubic1  26896  dcubic  26897  mcubic  26898  cubic2  26899  cubic  26900  binom4  26901  quart1cl  26905  quart1lem  26906  quart1  26907  quartlem1  26908  quartlem3  26910  log2cnv  26995  log2tlbnd  26996  log2ublem2  26998  log2ublem3  26999  log2ub  27000  basellem5  27136  basellem8  27139  basellem9  27140  cht3  27224  ppiub  27256  chtub  27264  bclbnd  27332  bposlem6  27341  bposlem8  27343  bposlem9  27344  lgsdir2lem1  27377  lgsdir2lem5  27381  2lgslem3b  27449  2lgslem3d  27451  2lgsoddprmlem3c  27464  2lgsoddprmlem3d  27465  addsqnreup  27495  pntibndlem1  27641  pntlemk  27658  ex-opab  30388  ex-exp  30406  ex-dvds  30412  ex-gcd  30413  ex-lcm  30414  ex-prmo  30415  ex-ind-dvds  30417  ply1dg3rt0irred  33499  2sqr3minply  33665  fib5  34297  fib6  34298  hgt750lem  34555  hgt750lem2  34556  hgt750leme  34562  problem4  35563  problem5  35564  sinccvglem  35567  mblfinlem3  37427  itg2addnclem2  37440  itg2addnclem3  37441  heiborlem6  37584  heiborlem7  37585  3exp7  41819  3lexlogpow2ineq2  41825  3lexlogpow5ineq5  41826  aks4d1p1  41842  2ap1caineq  41911  fac2xp3  42001  235t711  42086  ex-decpmul  42087  cu3addd  42428  3cubeslem3l  42434  3cubeslem3r  42435  jm2.23  42745  inductionexd  43913  lhe4.4ex1a  44094  stoweidlem13  45724  stoweidlem26  45737  stoweidlem34  45745  wallispilem4  45779  wallispi2lem1  45782  fmtno5lem1  47215  fmtno5lem2  47216  257prm  47223  fmtno4prmfac  47234  fmtno4nprmfac193  47236  139prmALT  47258  127prm  47261  mod42tp1mod8  47264  3exp4mod41  47278  41prothprmlem2  47280  6even  47373  11t31e341  47394  2exp340mod341  47395  gbpart8  47430  sbgoldbwt  47439  sbgoldbst  47440  evengpop3  47460  evengpoap3  47461  nnsum4primeseven  47462  nnsum4primesevenALTV  47463  2t6m3t4e0  47828  linevalexample  47879  zlmodzxzequa  47980  zlmodzxzequap  47983  ackval3  48172  ackval2012  48180  ackval3012  48181  ackval41  48184  ackval42  48185