Theorem 3cn 11514

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 11497	. 2 ⊢ 3 = (2 + 1)
2		2cn 11508	. . 3 ⊢ 2 ∈ ℂ
3		ax-1cn 10385	. . 3 ⊢ 1 ∈ ℂ
4	2, 3	addcli 10438	. 2 ⊢ (2 + 1) ∈ ℂ
5	1, 4	eqeltri 2856	1 ⊢ 3 ∈ ℂ

Syntax hints:   ∈ wcel 2048  (class class class)co 6970  ℂcc 10325  1c1 10328   + caddc 10330  2c2 11488  3c3 11489

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1964  ax-8 2050  ax-9 2057  ax-ext 2745  ax-1cn 10385  ax-addcl 10387

This theorem depends on definitions:  df-bi 199  df-an 388  df-ex 1743  df-cleq 2765  df-clel 2840  df-2 11496  df-3 11497

This theorem is referenced by:  3ex  11516  4cn  11519  4m1e3  11569  3p2e5  11591  3p3e6  11592  4p4e8  11595  5p4e9  11598  3t1e3  11605  3t2e6  11606  3t3e9  11607  8th4div3  11660  halfpm6th  11661  6p4e10  11978  9t8e72  12034  halfthird  12049  sq3  13369  expnass  13378  fac3  13448  sqrlem7  14459  caurcvgr  14881  bpoly2  15261  bpoly3  15262  bpoly4  15263  ef01bndlem  15387  sin01bnd  15388  cos01bnd  15389  cos1bnd  15390  cos2bnd  15391  cos01gt0  15394  rpnnen2lem3  15419  rpnnen2lem11  15427  3dvdsdec  15531  3dvds2dec  15532  3lcm2e6woprm  15805  prmo3  16223  2exp6  16268  2exp16  16270  7prm  16290  13prm  16295  17prm  16296  19prm  16297  37prm  16300  43prm  16301  83prm  16302  139prm  16303  163prm  16304  317prm  16305  631prm  16306  1259lem1  16310  1259lem2  16311  1259lem3  16312  1259lem4  16313  1259lem5  16314  1259prm  16315  2503lem1  16316  2503lem2  16317  2503lem3  16318  2503prm  16319  4001lem1  16320  4001lem2  16321  4001lem3  16322  4001lem4  16323  4001prm  16324  tangtx  24784  sincos6thpi  24794  sincos3rdpi  24795  pigt3  24796  pige3ALT  24798  2logb9irrALT  25067  ang180lem2  25079  1cubr  25111  dcubic1lem  25112  dcubic2  25113  dcubic1  25114  dcubic  25115  mcubic  25116  cubic2  25117  cubic  25118  binom4  25119  quart1cl  25123  quart1lem  25124  quart1  25125  quartlem1  25126  quartlem3  25128  log2cnv  25214  log2tlbnd  25215  log2ublem2  25217  log2ublem3  25218  log2ub  25219  basellem5  25354  basellem8  25357  basellem9  25358  cht3  25442  ppiub  25472  chtub  25480  bclbnd  25548  bposlem6  25557  bposlem8  25559  bposlem9  25560  lgsdir2lem1  25593  lgsdir2lem5  25597  2lgslem3b  25665  2lgslem3d  25667  2lgsoddprmlem3c  25680  2lgsoddprmlem3d  25681  addsqnreup  25711  pntibndlem1  25857  pntlemk  25874  ex-opab  27979  ex-exp  27997  ex-dvds  28003  ex-gcd  28004  ex-lcm  28005  ex-prmo  28006  ex-ind-dvds  28008  fib5  31266  fib6  31267  hgt750lem  31531  hgt750lem2  31532  hgt750leme  31538  problem4  32371  problem5  32372  sinccvglem  32375  mblfinlem3  34320  itg2addnclem2  34333  itg2addnclem3  34334  heiborlem6  34484  heiborlem7  34485  235t711  38554  ex-decpmul  38555  jm2.23  38934  inductionexd  39813  lhe4.4ex1a  40021  stoweidlem13  41675  stoweidlem26  41688  stoweidlem34  41696  wallispilem4  41730  wallispi2lem1  41733  fmtno5lem1  43023  fmtno5lem2  43024  257prm  43031  fmtno4prmfac  43042  fmtno4nprmfac193  43044  139prmALT  43067  127prm  43071  mod42tp1mod8  43075  3exp4mod41  43089  41prothprmlem2  43091  6even  43184  11t31e341  43205  2exp340mod341  43206  gbpart8  43241  sbgoldbwt  43250  sbgoldbst  43251  evengpop3  43271  evengpoap3  43272  nnsum4primeseven  43273  nnsum4primesevenALTV  43274  2t6m3t4e0  43700  linevalexample  43757  zlmodzxzequa  43858  zlmodzxzequap  43861