Theorem 3cn 12253

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 12236	. 2 ⊢ 3 = (2 + 1)
2		2cn 12247	. . 3 ⊢ 2 ∈ ℂ
3		ax-1cn 11087	. . 3 ⊢ 1 ∈ ℂ
4	2, 3	addcli 11142	. 2 ⊢ (2 + 1) ∈ ℂ
5	1, 4	eqeltri 2835	1 ⊢ 3 ∈ ℂ

Syntax hints:   ∈ wcel 2119  (class class class)co 7356  ℂcc 11027  1c1 11030   + caddc 11032  2c2 12227  3c3 12228

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711  ax-1cn 11087  ax-addcl 11089

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-cleq 2731  df-clel 2814  df-2 12235  df-3 12236

This theorem is referenced by:  3ex  12254  4cn  12257  4m1e3  12296  3p2e5  12318  3p3e6  12319  4p4e8  12322  5p4e9  12325  3t1e3  12332  3t2e6  12333  3t3e9  12334  8th4div3  12388  halfthird  12389  halfpm6th  12390  6p4e10  12707  9t8e72  12763  sq3  14151  expnass  14161  fac3  14233  01sqrexlem7  15201  caurcvgr  15627  bpoly2  16013  bpoly3  16014  bpoly4  16015  ef01bndlem  16142  sin01bnd  16143  cos01bnd  16144  cos1bnd  16145  cos2bnd  16146  cos01gt0  16149  rpnnen2lem3  16174  rpnnen2lem11  16182  3dvdsdec  16292  3dvds2dec  16293  5ndvds3  16373  3lcm2e6woprm  16575  prmo3  17003  2exp6  17048  2exp16  17052  7prm  17072  13prm  17077  17prm  17078  19prm  17079  37prm  17082  43prm  17083  83prm  17084  139prm  17085  163prm  17086  317prm  17087  631prm  17088  1259lem1  17092  1259lem2  17093  1259lem3  17094  1259lem4  17095  1259lem5  17096  1259prm  17097  2503lem1  17098  2503lem2  17099  2503lem3  17100  2503prm  17101  4001lem1  17102  4001lem2  17103  4001lem3  17104  4001lem4  17105  4001prm  17106  tangtx  26487  sincos6thpi  26498  sincos3rdpi  26499  pigt3  26500  pige3ALT  26502  2logb9irrALT  26780  ang180lem2  26792  1cubr  26824  dcubic1lem  26825  dcubic2  26826  dcubic1  26827  dcubic  26828  mcubic  26829  cubic2  26830  cubic  26831  binom4  26832  quart1cl  26836  quart1lem  26837  quart1  26838  quartlem1  26839  quartlem3  26841  log2cnv  26926  log2tlbnd  26927  log2ublem2  26929  log2ublem3  26930  log2ub  26931  basellem5  27066  basellem8  27069  basellem9  27070  cht3  27154  ppiub  27185  chtub  27193  bclbnd  27261  bposlem6  27270  bposlem8  27272  bposlem9  27273  lgsdir2lem1  27306  lgsdir2lem5  27310  2lgslem3b  27378  2lgslem3d  27380  2lgsoddprmlem3c  27393  2lgsoddprmlem3d  27394  addsqnreup  27424  pntibndlem1  27570  pntlemk  27587  ex-opab  30520  ex-exp  30538  ex-dvds  30544  ex-gcd  30545  ex-lcm  30546  ex-prmo  30547  ex-ind-dvds  30549  ply1dg3rt0irred  33667  2sqr3minply  33964  2sqr3nconstr  33965  cos9thpiminplylem2  33967  cos9thpiminplylem3  33968  cos9thpiminplylem4  33969  cos9thpiminplylem5  33970  cos9thpiminply  33972  cos9thpinconstrlem1  33973  cos9thpinconstrlem2  33974  cos9thpinconstr  33975  fib5  34589  fib6  34590  hgt750lem  34835  hgt750lem2  34836  hgt750leme  34842  problem4  35896  problem5  35897  sinccvglem  35900  mblfinlem3  38026  itg2addnclem2  38039  itg2addnclem3  38040  heiborlem6  38183  heiborlem7  38184  3exp7  42538  3lexlogpow2ineq2  42544  3lexlogpow5ineq5  42545  aks4d1p1  42561  2ap1caineq  42630  3rdpwhole  42769  235t711  42782  ex-decpmul  42783  tan3rdpi  42829  sin2t3rdpi  42830  cos2t3rdpi  42831  sin4t3rdpi  42832  cos4t3rdpi  42833  cu3addd  43130  3cubeslem3l  43135  3cubeslem3r  43136  jm2.23  43441  inductionexd  44599  lhe4.4ex1a  44773  stoweidlem13  46456  stoweidlem26  46469  stoweidlem34  46477  wallispilem4  46511  wallispi2lem1  46514  sin5tlem1  47336  sin5tlem2  47337  sin5tlem3  47338  sin5tlem4  47339  sin5tlem5  47340  sin5t  47341  goldrasin  47345  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