Theorem 3cn 12434

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 12416	. 2 ⊢ 3 = (2 + 1)
2		2cn 12428	. . 3 ⊢ 2 ∈ ℂ
3		ax-1cn 11268	. . 3 ⊢ 1 ∈ ℂ
4	2, 3	addcli 11325	. 2 ⊢ (2 + 1) ∈ ℂ
5	1, 4	eqeltri 2859	1 ⊢ 3 ∈ ℂ

This proof depends on syntax axioms:   ∈ wcel 2146  (class class class)co 7427  ℂcc 11208  1c1 11211   + caddc 11213  2c2 12407  3c3 12408

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1944  ax-6 2001  ax-7 2042  ax-8 2148  ax-9 2156  ax-ext 2735  ax-1cn 11268  ax-addcl 11270

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-cleq 2755  df-clel 2838  df-2 12415  df-3 12416

This theorem is used by:  3ex  12435  4cn  12438  4m1e3  12481  3p2e5  12503  3p3e6  12504  4p4e8  12507  5p4e9  12510  3t1e3  12517  3t2e6  12518  2t3e6  12519  3t3e9  12520  8th4div3  12576  halfthird  12577  halfpm6th  12578  6p4e10  12901  9t8e72  12957  sq3  14351  expnass  14362  01sqrexlem7  15427  caurcvgr  15853  bpoly2  16235  bpoly3  16236  bpoly4  16237  ef01bndlem  16364  sin01bnd  16365  cos01bnd  16366  cos1bnd  16367  cos2bnd  16368  cos01gt0  16371  rpnnen2lem3  16396  rpnnen2lem11  16404  3dvdsdec  16514  3dvds2dec  16515  5ndvds3  16595  3lcm2e6woprm  16802  2exp16  17280  13prm  17306  17prm  17307  19prm  17308  37prm  17311  43prm  17312  83prm  17313  139prm  17314  163prm  17315  317prm  17316  631prm  17317  1259lem1  17321  1259lem2  17322  1259lem3  17323  1259lem4  17324  1259lem5  17325  1259prm  17326  2503lem1  17327  2503lem2  17328  2503lem3  17329  2503prm  17330  4001lem1  17331  4001lem2  17332  4001lem3  17333  4001lem4  17334  4001prm  17335  tangtx  26846  sincos6thpi  26856  sincos3rdpi  26857  pigt3  26858  pige3ALT  26860  2logb9irrALT  27138  ang180lem2  27150  1cubr  27182  dcubic1lem  27183  dcubic2  27184  dcubic1  27185  dcubic  27186  mcubic  27187  cubic2  27188  cubic  27189  binom4  27190  quart1cl  27194  quart1lem  27195  quart1  27196  quartlem1  27197  quartlem3  27199  log2cnv  27284  log2tlbnd  27285  log2ublem2  27287  log2ublem3  27288  log2ub  27289  basellem5  27424  basellem8  27427  basellem9  27428  ppiub  27543  chtub  27551  bclbnd  27619  bposlem6  27628  bposlem8  27630  bposlem9  27631  lgsdir2lem1  27664  lgsdir2lem5  27668  2lgslem3b  27736  2lgslem3d  27738  2lgsoddprmlem3c  27751  2lgsoddprmlem3d  27752  addsqnreup  27782  pntibndlem1  27928  pntlemk  27945  ex-opab  31045  ex-exp  31063  ex-dvds  31069  ex-gcd  31070  ex-lcm  31071  ex-prmo  31072  ex-ind-dvds  31074  ply1dg3rt0irred  34169  2sqr3minply  34465  2sqr3nconstr  34466  cos9thpiminplylem2  34468  cos9thpiminplylem3  34469  cos9thpiminplylem4  34470  cos9thpiminplylem5  34471  cos9thpiminply  34473  cos9thpinconstrlem1  34474  cos9thpinconstrlem2  34475  cos9thpinconstr  34476  fib5  35090  fib6  35091  hgt750lem  35333  hgt750lem2  35334  hgt750leme  35340  problem4  36554  problem5  36555  sinccvglem  36558  mblfinlem3  38717  itg2addnclem2  38730  itg2addnclem3  38731  heiborlem6  38890  heiborlem7  38891  3lexlogpow2ineq2  43249  3lexlogpow5ineq5  43250  aks4d1p1  43266  2ap1caineq  43335  25or6to4  43396  1p4e5  43451  2p5e7  43458  3p4e7  43461  3p5e8  43462  3p6e9  43463  3rdpwhole  43489  235t711  43502  ex-decpmul  43503  tan3rdpi  43543  sin2t3rdpi  43544  cos2t3rdpi  43545  sin4t3rdpi  43546  cos4t3rdpi  43547  cu3addd  43831  3cubeslem3l  43836  3cubeslem3r  43837  jm2.23  44143  inductionexd  45295  lhe4.4ex1a  45453  stoweidlem13  47162  stoweidlem26  47175  stoweidlem34  47183  wallispilem4  47217  wallispi2lem1  47220  sin5tlem1  48058  sin5tlem2  48059  sin5tlem3  48060  sin5tlem4  48061  sin5tlem5  48062  sin5t  48063  goldrasin  48068  ceil5half3  48555  fmtno5lem1  48777  fmtno5lem2  48778  257prm  48785  fmtno4prmfac  48796  fmtno4nprmfac193  48798  139prmALT  48820  127prm  48823  mod42tp1mod8  48826  3exp4mod41  48840  41prothprmlem2  48842  ppivalnn4  48851  6even  48948  11t31e341  48969  2exp340mod341  48970  gbpart8  49005  sbgoldbwt  49014  sbgoldbst  49015  evengpop3  49035  evengpoap3  49036  nnsum4primeseven  49037  nnsum4primesevenALTV  49038  2t6m3t4e0  49599  linevalexample  49646  zlmodzxzequa  49747  zlmodzxzequap  49750  ackval3  49934  ackval2012  49942  ackval3012  49943  ackval41  49946  ackval42  49947