Theorem 3cn 12293

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 12276	. 2 ⊢ 3 = (2 + 1)
2		2cn 12287	. . 3 ⊢ 2 ∈ ℂ
3		ax-1cn 11168	. . 3 ⊢ 1 ∈ ℂ
4	2, 3	addcli 11220	. 2 ⊢ (2 + 1) ∈ ℂ
5	1, 4	eqeltri 2830	1 ⊢ 3 ∈ ℂ

Syntax hints:   ∈ wcel 2107  (class class class)co 7409  ℂcc 11108  1c1 11111   + caddc 11113  2c2 12267  3c3 12268

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 11168  ax-addcl 11170

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

This theorem is referenced by:  3ex  12294  4cn  12297  4m1e3  12341  3p2e5  12363  3p3e6  12364  4p4e8  12367  5p4e9  12370  3t1e3  12377  3t2e6  12378  3t3e9  12379  8th4div3  12432  halfpm6th  12433  6p4e10  12749  9t8e72  12805  halfthird  12820  sq3  14162  expnass  14172  fac3  14240  01sqrexlem7  15195  caurcvgr  15620  bpoly2  16001  bpoly3  16002  bpoly4  16003  ef01bndlem  16127  sin01bnd  16128  cos01bnd  16129  cos1bnd  16130  cos2bnd  16131  cos01gt0  16134  rpnnen2lem3  16159  rpnnen2lem11  16167  3dvdsdec  16275  3dvds2dec  16276  3lcm2e6woprm  16552  prmo3  16974  2exp6  17020  2exp16  17024  7prm  17044  13prm  17049  17prm  17050  19prm  17051  37prm  17054  43prm  17055  83prm  17056  139prm  17057  163prm  17058  317prm  17059  631prm  17060  1259lem1  17064  1259lem2  17065  1259lem3  17066  1259lem4  17067  1259lem5  17068  1259prm  17069  2503lem1  17070  2503lem2  17071  2503lem3  17072  2503prm  17073  4001lem1  17074  4001lem2  17075  4001lem3  17076  4001lem4  17077  4001prm  17078  tangtx  26015  sincos6thpi  26025  sincos3rdpi  26026  pigt3  26027  pige3ALT  26029  2logb9irrALT  26303  ang180lem2  26315  1cubr  26347  dcubic1lem  26348  dcubic2  26349  dcubic1  26350  dcubic  26351  mcubic  26352  cubic2  26353  cubic  26354  binom4  26355  quart1cl  26359  quart1lem  26360  quart1  26361  quartlem1  26362  quartlem3  26364  log2cnv  26449  log2tlbnd  26450  log2ublem2  26452  log2ublem3  26453  log2ub  26454  basellem5  26589  basellem8  26592  basellem9  26593  cht3  26677  ppiub  26707  chtub  26715  bclbnd  26783  bposlem6  26792  bposlem8  26794  bposlem9  26795  lgsdir2lem1  26828  lgsdir2lem5  26832  2lgslem3b  26900  2lgslem3d  26902  2lgsoddprmlem3c  26915  2lgsoddprmlem3d  26916  addsqnreup  26946  pntibndlem1  27092  pntlemk  27109  ex-opab  29685  ex-exp  29703  ex-dvds  29709  ex-gcd  29710  ex-lcm  29711  ex-prmo  29712  ex-ind-dvds  29714  fib5  33404  fib6  33405  hgt750lem  33663  hgt750lem2  33664  hgt750leme  33670  problem4  34653  problem5  34654  sinccvglem  34657  mblfinlem3  36527  itg2addnclem2  36540  itg2addnclem3  36541  heiborlem6  36684  heiborlem7  36685  3exp7  40918  3lexlogpow2ineq2  40924  3lexlogpow5ineq5  40925  aks4d1p1  40941  2ap1caineq  40961  fac2xp3  41020  235t711  41205  ex-decpmul  41206  cu3addd  41418  3cubeslem3l  41424  3cubeslem3r  41425  jm2.23  41735  inductionexd  42906  lhe4.4ex1a  43088  stoweidlem13  44729  stoweidlem26  44742  stoweidlem34  44750  wallispilem4  44784  wallispi2lem1  44787  fmtno5lem1  46221  fmtno5lem2  46222  257prm  46229  fmtno4prmfac  46240  fmtno4nprmfac193  46242  139prmALT  46264  127prm  46267  mod42tp1mod8  46270  3exp4mod41  46284  41prothprmlem2  46286  6even  46379  11t31e341  46400  2exp340mod341  46401  gbpart8  46436  sbgoldbwt  46445  sbgoldbst  46446  evengpop3  46466  evengpoap3  46467  nnsum4primeseven  46468  nnsum4primesevenALTV  46469  2t6m3t4e0  47024  linevalexample  47076  zlmodzxzequa  47177  zlmodzxzequap  47180  ackval3  47369  ackval2012  47377  ackval3012  47378  ackval41  47381  ackval42  47382