Theorem 3cn 12256

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 12239	. 2 ⊢ 3 = (2 + 1)
2		2cn 12250	. . 3 ⊢ 2 ∈ ℂ
3		ax-1cn 11090	. . 3 ⊢ 1 ∈ ℂ
4	2, 3	addcli 11145	. 2 ⊢ (2 + 1) ∈ ℂ
5	1, 4	eqeltri 2833	1 ⊢ 3 ∈ ℂ

Syntax hints:   ∈ wcel 2114  (class class class)co 7361  ℂcc 11030  1c1 11033   + caddc 11035  2c2 12230  3c3 12231

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-1cn 11090  ax-addcl 11092

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2729  df-clel 2812  df-2 12238  df-3 12239

This theorem is referenced by:  3ex  12257  4cn  12260  4m1e3  12299  3p2e5  12321  3p3e6  12322  4p4e8  12325  5p4e9  12328  3t1e3  12335  3t2e6  12336  3t3e9  12337  8th4div3  12391  halfthird  12392  halfpm6th  12393  6p4e10  12710  9t8e72  12766  sq3  14154  expnass  14164  fac3  14236  01sqrexlem7  15204  caurcvgr  15630  bpoly2  16016  bpoly3  16017  bpoly4  16018  ef01bndlem  16145  sin01bnd  16146  cos01bnd  16147  cos1bnd  16148  cos2bnd  16149  cos01gt0  16152  rpnnen2lem3  16177  rpnnen2lem11  16185  3dvdsdec  16295  3dvds2dec  16296  5ndvds3  16376  3lcm2e6woprm  16578  prmo3  17006  2exp6  17051  2exp16  17055  7prm  17075  13prm  17080  17prm  17081  19prm  17082  37prm  17085  43prm  17086  83prm  17087  139prm  17088  163prm  17089  317prm  17090  631prm  17091  1259lem1  17095  1259lem2  17096  1259lem3  17097  1259lem4  17098  1259lem5  17099  1259prm  17100  2503lem1  17101  2503lem2  17102  2503lem3  17103  2503prm  17104  4001lem1  17105  4001lem2  17106  4001lem3  17107  4001lem4  17108  4001prm  17109  tangtx  26485  sincos6thpi  26496  sincos3rdpi  26497  pigt3  26498  pige3ALT  26500  2logb9irrALT  26778  ang180lem2  26790  1cubr  26822  dcubic1lem  26823  dcubic2  26824  dcubic1  26825  dcubic  26826  mcubic  26827  cubic2  26828  cubic  26829  binom4  26830  quart1cl  26834  quart1lem  26835  quart1  26836  quartlem1  26837  quartlem3  26839  log2cnv  26924  log2tlbnd  26925  log2ublem2  26927  log2ublem3  26928  log2ub  26929  basellem5  27065  basellem8  27068  basellem9  27069  cht3  27153  ppiub  27184  chtub  27192  bclbnd  27260  bposlem6  27269  bposlem8  27271  bposlem9  27272  lgsdir2lem1  27305  lgsdir2lem5  27309  2lgslem3b  27377  2lgslem3d  27379  2lgsoddprmlem3c  27392  2lgsoddprmlem3d  27393  addsqnreup  27423  pntibndlem1  27569  pntlemk  27586  ex-opab  30520  ex-exp  30538  ex-dvds  30544  ex-gcd  30545  ex-lcm  30546  ex-prmo  30547  ex-ind-dvds  30549  ply1dg3rt0irred  33662  2sqr3minply  33943  2sqr3nconstr  33944  cos9thpiminplylem2  33946  cos9thpiminplylem3  33947  cos9thpiminplylem4  33948  cos9thpiminplylem5  33949  cos9thpiminply  33951  cos9thpinconstrlem1  33952  cos9thpinconstrlem2  33953  cos9thpinconstr  33954  fib5  34568  fib6  34569  hgt750lem  34814  hgt750lem2  34815  hgt750leme  34821  problem4  35869  problem5  35870  sinccvglem  35873  mblfinlem3  37997  itg2addnclem2  38010  itg2addnclem3  38011  heiborlem6  38154  heiborlem7  38155  3exp7  42509  3lexlogpow2ineq2  42515  3lexlogpow5ineq5  42516  aks4d1p1  42532  2ap1caineq  42601  3rdpwhole  42741  235t711  42754  ex-decpmul  42755  tan3rdpi  42801  sin2t3rdpi  42802  cos2t3rdpi  42803  sin4t3rdpi  42804  cos4t3rdpi  42805  cu3addd  43130  3cubeslem3l  43135  3cubeslem3r  43136  jm2.23  43445  inductionexd  44603  lhe4.4ex1a  44777  stoweidlem13  46462  stoweidlem26  46475  stoweidlem34  46483  wallispilem4  46517  wallispi2lem1  46520  sin5tlem1  47340  sin5tlem2  47341  sin5tlem3  47342  sin5tlem4  47343  sin5tlem5  47344  sin5t  47345  goldrasin  47347  ceil5half3  47809  fmtno5lem1  48031  fmtno5lem2  48032  257prm  48039  fmtno4prmfac  48050  fmtno4nprmfac193  48052  139prmALT  48074  127prm  48077  mod42tp1mod8  48080  3exp4mod41  48094  41prothprmlem2  48096  ppivalnn4  48105  6even  48202  11t31e341  48223  2exp340mod341  48224  gbpart8  48259  sbgoldbwt  48268  sbgoldbst  48269  evengpop3  48289  evengpoap3  48290  nnsum4primeseven  48291  nnsum4primesevenALTV  48292  2t6m3t4e0  48839  linevalexample  48886  zlmodzxzequa  48987  zlmodzxzequap  48990  ackval3  49174  ackval2012  49182  ackval3012  49183  ackval41  49186  ackval42  49187