Theorem 3cn 12424

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 12406	. 2 ⊢ 3 = (2 + 1)
2		2cn 12418	. . 3 ⊢ 2 ∈ ℂ
3		ax-1cn 11258	. . 3 ⊢ 1 ∈ ℂ
4	2, 3	addcli 11315	. 2 ⊢ (2 + 1) ∈ ℂ
5	1, 4	eqeltri 2857	1 ⊢ 3 ∈ ℂ

This proof depends on syntax axioms:   ∈ wcel 2145  (class class class)co 7420  ℂcc 11198  1c1 11201   + caddc 11203  2c2 12397  3c3 12398

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733  ax-1cn 11258  ax-addcl 11260

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2753  df-clel 2836  df-2 12405  df-3 12406

This theorem is used by:  3ex  12425  4cn  12428  4m1e3  12471  3p2e5  12493  3p3e6  12494  4p4e8  12497  5p4e9  12500  3t1e3  12507  3t2e6  12508  2t3e6  12509  3t3e9  12510  8th4div3  12566  halfthird  12567  halfpm6th  12568  6p4e10  12891  9t8e72  12947  sq3  14341  expnass  14352  01sqrexlem7  15415  caurcvgr  15841  bpoly2  16223  bpoly3  16224  bpoly4  16225  ef01bndlem  16352  sin01bnd  16353  cos01bnd  16354  cos1bnd  16355  cos2bnd  16356  cos01gt0  16359  rpnnen2lem3  16384  rpnnen2lem11  16392  3dvdsdec  16502  3dvds2dec  16503  5ndvds3  16583  3lcm2e6woprm  16790  2exp16  17268  13prm  17294  17prm  17295  19prm  17296  37prm  17299  43prm  17300  83prm  17301  139prm  17302  163prm  17303  317prm  17304  631prm  17305  1259lem1  17309  1259lem2  17310  1259lem3  17311  1259lem4  17312  1259lem5  17313  1259prm  17314  2503lem1  17315  2503lem2  17316  2503lem3  17317  2503prm  17318  4001lem1  17319  4001lem2  17320  4001lem3  17321  4001lem4  17322  4001prm  17323  tangtx  26834  sincos6thpi  26844  sincos3rdpi  26845  pigt3  26846  pige3ALT  26848  2logb9irrALT  27126  ang180lem2  27138  1cubr  27170  dcubic1lem  27171  dcubic2  27172  dcubic1  27173  dcubic  27174  mcubic  27175  cubic2  27176  cubic  27177  binom4  27178  quart1cl  27182  quart1lem  27183  quart1  27184  quartlem1  27185  quartlem3  27187  log2cnv  27272  log2tlbnd  27273  log2ublem2  27275  log2ublem3  27276  log2ub  27277  basellem5  27412  basellem8  27415  basellem9  27416  ppiub  27531  chtub  27539  bclbnd  27607  bposlem6  27616  bposlem8  27618  bposlem9  27619  lgsdir2lem1  27652  lgsdir2lem5  27656  2lgslem3b  27724  2lgslem3d  27726  2lgsoddprmlem3c  27739  2lgsoddprmlem3d  27740  addsqnreup  27770  pntibndlem1  27916  pntlemk  27933  ex-opab  31033  ex-exp  31051  ex-dvds  31057  ex-gcd  31058  ex-lcm  31059  ex-prmo  31060  ex-ind-dvds  31062  ply1dg3rt0irred  34116  2sqr3minply  34412  2sqr3nconstr  34413  cos9thpiminplylem2  34415  cos9thpiminplylem3  34416  cos9thpiminplylem4  34417  cos9thpiminplylem5  34418  cos9thpiminply  34420  cos9thpinconstrlem1  34421  cos9thpinconstrlem2  34422  cos9thpinconstr  34423  fib5  35037  fib6  35038  hgt750lem  35280  hgt750lem2  35281  hgt750leme  35287  problem4  36433  problem5  36434  sinccvglem  36437  mblfinlem3  38577  itg2addnclem2  38590  itg2addnclem3  38591  heiborlem6  38750  heiborlem7  38751  3lexlogpow2ineq2  43109  3lexlogpow5ineq5  43110  aks4d1p1  43126  2ap1caineq  43195  25or6to4  43256  1p4e5  43311  2p5e7  43318  3p4e7  43321  3p5e8  43322  3p6e9  43323  3rdpwhole  43349  235t711  43362  ex-decpmul  43363  tan3rdpi  43403  sin2t3rdpi  43404  cos2t3rdpi  43405  sin4t3rdpi  43406  cos4t3rdpi  43407  cu3addd  43691  3cubeslem3l  43696  3cubeslem3r  43697  jm2.23  44002  inductionexd  45154  lhe4.4ex1a  45312  stoweidlem13  47022  stoweidlem26  47035  stoweidlem34  47043  wallispilem4  47077  wallispi2lem1  47080  sin5tlem1  47918  sin5tlem2  47919  sin5tlem3  47920  sin5tlem4  47921  sin5tlem5  47922  sin5t  47923  goldrasin  47928  ceil5half3  48415  fmtno5lem1  48637  fmtno5lem2  48638  257prm  48645  fmtno4prmfac  48656  fmtno4nprmfac193  48658  139prmALT  48680  127prm  48683  mod42tp1mod8  48686  3exp4mod41  48700  41prothprmlem2  48702  ppivalnn4  48711  6even  48808  11t31e341  48829  2exp340mod341  48830  gbpart8  48865  sbgoldbwt  48874  sbgoldbst  48875  evengpop3  48895  evengpoap3  48896  nnsum4primeseven  48897  nnsum4primesevenALTV  48898  2t6m3t4e0  49459  linevalexample  49506  zlmodzxzequa  49607  zlmodzxzequap  49610  ackval3  49794  ackval2012  49802  ackval3012  49803  ackval41  49806  ackval42  49807