Theorem 3cn 12224

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 12207	. 2 ⊢ 3 = (2 + 1)
2		2cn 12218	. . 3 ⊢ 2 ∈ ℂ
3		ax-1cn 11082	. . 3 ⊢ 1 ∈ ℂ
4	2, 3	addcli 11136	. 2 ⊢ (2 + 1) ∈ ℂ
5	1, 4	eqeltri 2830	1 ⊢ 3 ∈ ℂ

Syntax hints:   ∈ wcel 2113  (class class class)co 7356  ℂcc 11022  1c1 11025   + caddc 11027  2c2 12198  3c3 12199

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2706  ax-1cn 11082  ax-addcl 11084

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2726  df-clel 2809  df-2 12206  df-3 12207

This theorem is referenced by:  3ex  12225  4cn  12228  4m1e3  12267  3p2e5  12289  3p3e6  12290  4p4e8  12293  5p4e9  12296  3t1e3  12303  3t2e6  12304  3t3e9  12305  8th4div3  12359  halfthird  12360  halfpm6th  12361  6p4e10  12677  9t8e72  12733  sq3  14119  expnass  14129  fac3  14201  01sqrexlem7  15169  caurcvgr  15595  bpoly2  15978  bpoly3  15979  bpoly4  15980  ef01bndlem  16107  sin01bnd  16108  cos01bnd  16109  cos1bnd  16110  cos2bnd  16111  cos01gt0  16114  rpnnen2lem3  16139  rpnnen2lem11  16147  3dvdsdec  16257  3dvds2dec  16258  5ndvds3  16338  3lcm2e6woprm  16540  prmo3  16967  2exp6  17012  2exp16  17016  7prm  17036  13prm  17041  17prm  17042  19prm  17043  37prm  17046  43prm  17047  83prm  17048  139prm  17049  163prm  17050  317prm  17051  631prm  17052  1259lem1  17056  1259lem2  17057  1259lem3  17058  1259lem4  17059  1259lem5  17060  1259prm  17061  2503lem1  17062  2503lem2  17063  2503lem3  17064  2503prm  17065  4001lem1  17066  4001lem2  17067  4001lem3  17068  4001lem4  17069  4001prm  17070  tangtx  26468  sincos6thpi  26479  sincos3rdpi  26480  pigt3  26481  pige3ALT  26483  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  27049  basellem8  27052  basellem9  27053  cht3  27137  ppiub  27169  chtub  27177  bclbnd  27245  bposlem6  27254  bposlem8  27256  bposlem9  27257  lgsdir2lem1  27290  lgsdir2lem5  27294  2lgslem3b  27362  2lgslem3d  27364  2lgsoddprmlem3c  27377  2lgsoddprmlem3d  27378  addsqnreup  27408  pntibndlem1  27554  pntlemk  27571  ex-opab  30456  ex-exp  30474  ex-dvds  30480  ex-gcd  30481  ex-lcm  30482  ex-prmo  30483  ex-ind-dvds  30485  ply1dg3rt0irred  33614  2sqr3minply  33886  2sqr3nconstr  33887  cos9thpiminplylem2  33889  cos9thpiminplylem3  33890  cos9thpiminplylem4  33891  cos9thpiminplylem5  33892  cos9thpiminply  33894  cos9thpinconstrlem1  33895  cos9thpinconstrlem2  33896  cos9thpinconstr  33897  fib5  34511  fib6  34512  hgt750lem  34757  hgt750lem2  34758  hgt750leme  34764  problem4  35811  problem5  35812  sinccvglem  35815  mblfinlem3  37799  itg2addnclem2  37812  itg2addnclem3  37813  heiborlem6  37956  heiborlem7  37957  3exp7  42246  3lexlogpow2ineq2  42252  3lexlogpow5ineq5  42253  aks4d1p1  42269  2ap1caineq  42338  3rdpwhole  42489  235t711  42502  ex-decpmul  42503  tan3rdpi  42549  sin2t3rdpi  42550  cos2t3rdpi  42551  sin4t3rdpi  42552  cos4t3rdpi  42553  cu3addd  42865  3cubeslem3l  42870  3cubeslem3r  42871  jm2.23  43180  inductionexd  44338  lhe4.4ex1a  44512  stoweidlem13  46199  stoweidlem26  46212  stoweidlem34  46220  wallispilem4  46254  wallispi2lem1  46257  ceil5half3  47528  fmtno5lem1  47741  fmtno5lem2  47742  257prm  47749  fmtno4prmfac  47760  fmtno4nprmfac193  47762  139prmALT  47784  127prm  47787  mod42tp1mod8  47790  3exp4mod41  47804  41prothprmlem2  47806  6even  47899  11t31e341  47920  2exp340mod341  47921  gbpart8  47956  sbgoldbwt  47965  sbgoldbst  47966  evengpop3  47986  evengpoap3  47987  nnsum4primeseven  47988  nnsum4primesevenALTV  47989  2t6m3t4e0  48536  linevalexample  48583  zlmodzxzequa  48684  zlmodzxzequap  48687  ackval3  48871  ackval2012  48879  ackval3012  48880  ackval41  48883  ackval42  48884