Theorem 3cn 12299

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 12281	. 2 ⊢ 3 = (2 + 1)
2		2cn 12293	. . 3 ⊢ 2 ∈ ℂ
3		ax-1cn 11131	. . 3 ⊢ 1 ∈ ℂ
4	2, 3	addcli 11188	. 2 ⊢ (2 + 1) ∈ ℂ
5	1, 4	eqeltri 2858	1 ⊢ 3 ∈ ℂ

Syntax hints:   ∈ wcel 2142  (class class class)co 7396  ℂcc 11071  1c1 11074   + caddc 11076  2c2 12272  3c3 12273

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-ext 2734  ax-1cn 11131  ax-addcl 11133

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1800  df-cleq 2754  df-clel 2837  df-2 12280  df-3 12281

This theorem is referenced by:  3ex  12300  4cn  12303  4m1e3  12346  3p2e5  12368  3p3e6  12369  4p4e8  12372  5p4e9  12375  3t1e3  12382  3t2e6  12383  2t3e6  12384  3t3e9  12385  8th4div3  12441  halfthird  12442  halfpm6th  12443  6p4e10  12765  9t8e72  12821  sq3  14211  expnass  14221  fac3  14293  01sqrexlem7  15275  caurcvgr  15701  bpoly2  16087  bpoly3  16088  bpoly4  16089  ef01bndlem  16216  sin01bnd  16217  cos01bnd  16218  cos1bnd  16219  cos2bnd  16220  cos01gt0  16223  rpnnen2lem3  16248  rpnnen2lem11  16256  3dvdsdec  16366  3dvds2dec  16367  5ndvds3  16447  3lcm2e6woprm  16649  prmo3  17077  2exp6  17122  2exp16  17126  7prm  17146  13prm  17152  17prm  17153  19prm  17154  37prm  17157  43prm  17158  83prm  17159  139prm  17160  163prm  17161  317prm  17162  631prm  17163  1259lem1  17167  1259lem2  17168  1259lem3  17169  1259lem4  17170  1259lem5  17171  1259prm  17172  2503lem1  17173  2503lem2  17174  2503lem3  17175  2503prm  17176  4001lem1  17177  4001lem2  17178  4001lem3  17179  4001lem4  17180  4001prm  17181  tangtx  26570  sincos6thpi  26581  sincos3rdpi  26582  pigt3  26583  pige3ALT  26585  2logb9irrALT  26863  ang180lem2  26875  1cubr  26907  dcubic1lem  26908  dcubic2  26909  dcubic1  26910  dcubic  26911  mcubic  26912  cubic2  26913  cubic  26914  binom4  26915  quart1cl  26919  quart1lem  26920  quart1  26921  quartlem1  26922  quartlem3  26924  log2cnv  27009  log2tlbnd  27010  log2ublem2  27012  log2ublem3  27013  log2ub  27014  basellem5  27149  basellem8  27152  basellem9  27153  ppiub  27268  chtub  27276  bclbnd  27344  bposlem6  27353  bposlem8  27355  bposlem9  27356  lgsdir2lem1  27389  lgsdir2lem5  27393  2lgslem3b  27461  2lgslem3d  27463  2lgsoddprmlem3c  27476  2lgsoddprmlem3d  27477  addsqnreup  27507  pntibndlem1  27653  pntlemk  27670  ex-opab  30634  ex-exp  30652  ex-dvds  30658  ex-gcd  30659  ex-lcm  30660  ex-prmo  30661  ex-ind-dvds  30663  ply1dg3rt0irred  33780  2sqr3minply  34077  2sqr3nconstr  34078  cos9thpiminplylem2  34080  cos9thpiminplylem3  34081  cos9thpiminplylem4  34082  cos9thpiminplylem5  34083  cos9thpiminply  34085  cos9thpinconstrlem1  34086  cos9thpinconstrlem2  34087  cos9thpinconstr  34088  fib5  34702  fib6  34703  hgt750lem  34945  hgt750lem2  34946  hgt750leme  34952  problem4  36018  problem5  36019  sinccvglem  36022  mblfinlem3  38158  itg2addnclem2  38171  itg2addnclem3  38172  heiborlem6  38315  heiborlem7  38316  3exp7  42670  3lexlogpow2ineq2  42676  3lexlogpow5ineq5  42677  aks4d1p1  42693  2ap1caineq  42762  3rdpwhole  42901  235t711  42914  ex-decpmul  42915  tan3rdpi  42961  sin2t3rdpi  42962  cos2t3rdpi  42963  sin4t3rdpi  42964  cos4t3rdpi  42965  cu3addd  43262  3cubeslem3l  43267  3cubeslem3r  43268  jm2.23  43573  inductionexd  44731  lhe4.4ex1a  44905  stoweidlem13  46587  stoweidlem26  46600  stoweidlem34  46608  wallispilem4  46642  wallispi2lem1  46645  sin5tlem1  47467  sin5tlem2  47468  sin5tlem3  47469  sin5tlem4  47470  sin5tlem5  47471  sin5t  47472  goldrasin  47476  ceil5half3  47940  fmtno5lem1  48162  fmtno5lem2  48163  257prm  48170  fmtno4prmfac  48181  fmtno4nprmfac193  48183  139prmALT  48205  127prm  48208  mod42tp1mod8  48211  3exp4mod41  48225  41prothprmlem2  48227  ppivalnn4  48236  6even  48333  11t31e341  48354  2exp340mod341  48355  gbpart8  48390  sbgoldbwt  48399  sbgoldbst  48400  evengpop3  48420  evengpoap3  48421  nnsum4primeseven  48422  nnsum4primesevenALTV  48423  2t6m3t4e0  48970  linevalexample  49017  zlmodzxzequa  49118  zlmodzxzequap  49121  ackval3  49305  ackval2012  49313  ackval3012  49314  ackval41  49317  ackval42  49318