Theorem 3cn 12262

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 12245	. 2 ⊢ 3 = (2 + 1)
2		2cn 12256	. . 3 ⊢ 2 ∈ ℂ
3		ax-1cn 11096	. . 3 ⊢ 1 ∈ ℂ
4	2, 3	addcli 11151	. 2 ⊢ (2 + 1) ∈ ℂ
5	1, 4	eqeltri 2832	1 ⊢ 3 ∈ ℂ

Syntax hints:   ∈ wcel 2114  (class class class)co 7367  ℂcc 11036  1c1 11039   + caddc 11041  2c2 12236  3c3 12237

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 2708  ax-1cn 11096  ax-addcl 11098

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2728  df-clel 2811  df-2 12244  df-3 12245

This theorem is referenced by:  3ex  12263  4cn  12266  4m1e3  12305  3p2e5  12327  3p3e6  12328  4p4e8  12331  5p4e9  12334  3t1e3  12341  3t2e6  12342  3t3e9  12343  8th4div3  12397  halfthird  12398  halfpm6th  12399  6p4e10  12716  9t8e72  12772  sq3  14160  expnass  14170  fac3  14242  01sqrexlem7  15210  caurcvgr  15636  bpoly2  16022  bpoly3  16023  bpoly4  16024  ef01bndlem  16151  sin01bnd  16152  cos01bnd  16153  cos1bnd  16154  cos2bnd  16155  cos01gt0  16158  rpnnen2lem3  16183  rpnnen2lem11  16191  3dvdsdec  16301  3dvds2dec  16302  5ndvds3  16382  3lcm2e6woprm  16584  prmo3  17012  2exp6  17057  2exp16  17061  7prm  17081  13prm  17086  17prm  17087  19prm  17088  37prm  17091  43prm  17092  83prm  17093  139prm  17094  163prm  17095  317prm  17096  631prm  17097  1259lem1  17101  1259lem2  17102  1259lem3  17103  1259lem4  17104  1259lem5  17105  1259prm  17106  2503lem1  17107  2503lem2  17108  2503lem3  17109  2503prm  17110  4001lem1  17111  4001lem2  17112  4001lem3  17113  4001lem4  17114  4001prm  17115  tangtx  26469  sincos6thpi  26480  sincos3rdpi  26481  pigt3  26482  pige3ALT  26484  2logb9irrALT  26762  ang180lem2  26774  1cubr  26806  dcubic1lem  26807  dcubic2  26808  dcubic1  26809  dcubic  26810  mcubic  26811  cubic2  26812  cubic  26813  binom4  26814  quart1cl  26818  quart1lem  26819  quart1  26820  quartlem1  26821  quartlem3  26823  log2cnv  26908  log2tlbnd  26909  log2ublem2  26911  log2ublem3  26912  log2ub  26913  basellem5  27048  basellem8  27051  basellem9  27052  cht3  27136  ppiub  27167  chtub  27175  bclbnd  27243  bposlem6  27252  bposlem8  27254  bposlem9  27255  lgsdir2lem1  27288  lgsdir2lem5  27292  2lgslem3b  27360  2lgslem3d  27362  2lgsoddprmlem3c  27375  2lgsoddprmlem3d  27376  addsqnreup  27406  pntibndlem1  27552  pntlemk  27569  ex-opab  30502  ex-exp  30520  ex-dvds  30526  ex-gcd  30527  ex-lcm  30528  ex-prmo  30529  ex-ind-dvds  30531  ply1dg3rt0irred  33644  2sqr3minply  33924  2sqr3nconstr  33925  cos9thpiminplylem2  33927  cos9thpiminplylem3  33928  cos9thpiminplylem4  33929  cos9thpiminplylem5  33930  cos9thpiminply  33932  cos9thpinconstrlem1  33933  cos9thpinconstrlem2  33934  cos9thpinconstr  33935  fib5  34549  fib6  34550  hgt750lem  34795  hgt750lem2  34796  hgt750leme  34802  problem4  35850  problem5  35851  sinccvglem  35854  mblfinlem3  37980  itg2addnclem2  37993  itg2addnclem3  37994  heiborlem6  38137  heiborlem7  38138  3exp7  42492  3lexlogpow2ineq2  42498  3lexlogpow5ineq5  42499  aks4d1p1  42515  2ap1caineq  42584  3rdpwhole  42724  235t711  42737  ex-decpmul  42738  tan3rdpi  42784  sin2t3rdpi  42785  cos2t3rdpi  42786  sin4t3rdpi  42787  cos4t3rdpi  42788  cu3addd  43113  3cubeslem3l  43118  3cubeslem3r  43119  jm2.23  43424  inductionexd  44582  lhe4.4ex1a  44756  stoweidlem13  46441  stoweidlem26  46454  stoweidlem34  46462  wallispilem4  46496  wallispi2lem1  46499  sin5tlem1  47321  sin5tlem2  47322  sin5tlem3  47323  sin5tlem4  47324  sin5tlem5  47325  sin5t  47326  goldrasin  47330  ceil5half3  47794  fmtno5lem1  48016  fmtno5lem2  48017  257prm  48024  fmtno4prmfac  48035  fmtno4nprmfac193  48037  139prmALT  48059  127prm  48062  mod42tp1mod8  48065  3exp4mod41  48079  41prothprmlem2  48081  ppivalnn4  48090  6even  48187  11t31e341  48208  2exp340mod341  48209  gbpart8  48244  sbgoldbwt  48253  sbgoldbst  48254  evengpop3  48274  evengpoap3  48275  nnsum4primeseven  48276  nnsum4primesevenALTV  48277  2t6m3t4e0  48824  linevalexample  48871  zlmodzxzequa  48972  zlmodzxzequap  48975  ackval3  49159  ackval2012  49167  ackval3012  49168  ackval41  49171  ackval42  49172