Theorem 3cn 12344

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 12327	. 2 ⊢ 3 = (2 + 1)
2		2cn 12338	. . 3 ⊢ 2 ∈ ℂ
3		ax-1cn 11210	. . 3 ⊢ 1 ∈ ℂ
4	2, 3	addcli 11264	. 2 ⊢ (2 + 1) ∈ ℂ
5	1, 4	eqeltri 2834	1 ⊢ 3 ∈ ℂ

Syntax hints:   ∈ wcel 2105  (class class class)co 7430  ℂcc 11150  1c1 11153   + caddc 11155  2c2 12318  3c3 12319

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705  ax-1cn 11210  ax-addcl 11212

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1776  df-cleq 2726  df-clel 2813  df-2 12326  df-3 12327

This theorem is referenced by:  3ex  12345  4cn  12348  4m1e3  12392  3p2e5  12414  3p3e6  12415  4p4e8  12418  5p4e9  12421  3t1e3  12428  3t2e6  12429  3t3e9  12430  8th4div3  12483  halfpm6th  12484  6p4e10  12802  9t8e72  12858  halfthird  12873  sq3  14233  expnass  14243  fac3  14315  01sqrexlem7  15283  caurcvgr  15706  bpoly2  16089  bpoly3  16090  bpoly4  16091  ef01bndlem  16216  sin01bnd  16217  cos01bnd  16218  cos1bnd  16219  cos2bnd  16220  cos01gt0  16223  rpnnen2lem3  16248  rpnnen2lem11  16256  3dvdsdec  16365  3dvds2dec  16366  5ndvds3  16446  3lcm2e6woprm  16648  prmo3  17074  2exp6  17120  2exp16  17124  7prm  17144  13prm  17149  17prm  17150  19prm  17151  37prm  17154  43prm  17155  83prm  17156  139prm  17157  163prm  17158  317prm  17159  631prm  17160  1259lem1  17164  1259lem2  17165  1259lem3  17166  1259lem4  17167  1259lem5  17168  1259prm  17169  2503lem1  17170  2503lem2  17171  2503lem3  17172  2503prm  17173  4001lem1  17174  4001lem2  17175  4001lem3  17176  4001lem4  17177  4001prm  17178  tangtx  26561  sincos6thpi  26572  sincos3rdpi  26573  pigt3  26574  pige3ALT  26576  2logb9irrALT  26855  ang180lem2  26867  1cubr  26899  dcubic1lem  26900  dcubic2  26901  dcubic1  26902  dcubic  26903  mcubic  26904  cubic2  26905  cubic  26906  binom4  26907  quart1cl  26911  quart1lem  26912  quart1  26913  quartlem1  26914  quartlem3  26916  log2cnv  27001  log2tlbnd  27002  log2ublem2  27004  log2ublem3  27005  log2ub  27006  basellem5  27142  basellem8  27145  basellem9  27146  cht3  27230  ppiub  27262  chtub  27270  bclbnd  27338  bposlem6  27347  bposlem8  27349  bposlem9  27350  lgsdir2lem1  27383  lgsdir2lem5  27387  2lgslem3b  27455  2lgslem3d  27457  2lgsoddprmlem3c  27470  2lgsoddprmlem3d  27471  addsqnreup  27501  pntibndlem1  27647  pntlemk  27664  ex-opab  30460  ex-exp  30478  ex-dvds  30484  ex-gcd  30485  ex-lcm  30486  ex-prmo  30487  ex-ind-dvds  30489  ply1dg3rt0irred  33586  2sqr3minply  33752  fib5  34386  fib6  34387  hgt750lem  34644  hgt750lem2  34645  hgt750leme  34651  problem4  35652  problem5  35653  sinccvglem  35656  mblfinlem3  37645  itg2addnclem2  37658  itg2addnclem3  37659  heiborlem6  37802  heiborlem7  37803  3exp7  42034  3lexlogpow2ineq2  42040  3lexlogpow5ineq5  42041  aks4d1p1  42057  2ap1caineq  42126  fac2xp3  42220  235t711  42317  ex-decpmul  42318  tan3rdpi  42364  cu3addd  42667  3cubeslem3l  42673  3cubeslem3r  42674  jm2.23  42984  inductionexd  44144  lhe4.4ex1a  44324  stoweidlem13  45968  stoweidlem26  45981  stoweidlem34  45989  wallispilem4  46023  wallispi2lem1  46026  ceil5half3  47279  fmtno5lem1  47477  fmtno5lem2  47478  257prm  47485  fmtno4prmfac  47496  fmtno4nprmfac193  47498  139prmALT  47520  127prm  47523  mod42tp1mod8  47526  3exp4mod41  47540  41prothprmlem2  47542  6even  47635  11t31e341  47656  2exp340mod341  47657  gbpart8  47692  sbgoldbwt  47701  sbgoldbst  47702  evengpop3  47722  evengpoap3  47723  nnsum4primeseven  47724  nnsum4primesevenALTV  47725  2t6m3t4e0  48192  linevalexample  48240  zlmodzxzequa  48341  zlmodzxzequap  48344  ackval3  48532  ackval2012  48540  ackval3012  48541  ackval41  48544  ackval42  48545