Theorem 3cn 11712

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 11695	. 2 ⊢ 3 = (2 + 1)
2		2cn 11706	. . 3 ⊢ 2 ∈ ℂ
3		ax-1cn 10589	. . 3 ⊢ 1 ∈ ℂ
4	2, 3	addcli 10641	. 2 ⊢ (2 + 1) ∈ ℂ
5	1, 4	eqeltri 2909	1 ⊢ 3 ∈ ℂ

Syntax hints:   ∈ wcel 2110  (class class class)co 7150  ℂcc 10529  1c1 10532   + caddc 10534  2c2 11686  3c3 11687

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-ext 2793  ax-1cn 10589  ax-addcl 10591

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1777  df-cleq 2814  df-clel 2893  df-2 11694  df-3 11695

This theorem is referenced by:  3ex  11713  4cn  11716  4m1e3  11760  3p2e5  11782  3p3e6  11783  4p4e8  11786  5p4e9  11789  3t1e3  11796  3t2e6  11797  3t3e9  11798  8th4div3  11851  halfpm6th  11852  6p4e10  12164  9t8e72  12220  halfthird  12235  sq3  13555  expnass  13564  fac3  13634  sqrlem7  14602  caurcvgr  15024  bpoly2  15405  bpoly3  15406  bpoly4  15407  ef01bndlem  15531  sin01bnd  15532  cos01bnd  15533  cos1bnd  15534  cos2bnd  15535  cos01gt0  15538  rpnnen2lem3  15563  rpnnen2lem11  15571  3dvdsdec  15675  3dvds2dec  15676  3lcm2e6woprm  15953  prmo3  16371  2exp6  16416  2exp16  16418  7prm  16438  13prm  16443  17prm  16444  19prm  16445  37prm  16448  43prm  16449  83prm  16450  139prm  16451  163prm  16452  317prm  16453  631prm  16454  1259lem1  16458  1259lem2  16459  1259lem3  16460  1259lem4  16461  1259lem5  16462  1259prm  16463  2503lem1  16464  2503lem2  16465  2503lem3  16466  2503prm  16467  4001lem1  16468  4001lem2  16469  4001lem3  16470  4001lem4  16471  4001prm  16472  tangtx  25085  sincos6thpi  25095  sincos3rdpi  25096  pigt3  25097  pige3ALT  25099  2logb9irrALT  25370  ang180lem2  25382  1cubr  25414  dcubic1lem  25415  dcubic2  25416  dcubic1  25417  dcubic  25418  mcubic  25419  cubic2  25420  cubic  25421  binom4  25422  quart1cl  25426  quart1lem  25427  quart1  25428  quartlem1  25429  quartlem3  25431  log2cnv  25516  log2tlbnd  25517  log2ublem2  25519  log2ublem3  25520  log2ub  25521  basellem5  25656  basellem8  25659  basellem9  25660  cht3  25744  ppiub  25774  chtub  25782  bclbnd  25850  bposlem6  25859  bposlem8  25861  bposlem9  25862  lgsdir2lem1  25895  lgsdir2lem5  25899  2lgslem3b  25967  2lgslem3d  25969  2lgsoddprmlem3c  25982  2lgsoddprmlem3d  25983  addsqnreup  26013  pntibndlem1  26159  pntlemk  26176  ex-opab  28205  ex-exp  28223  ex-dvds  28229  ex-gcd  28230  ex-lcm  28231  ex-prmo  28232  ex-ind-dvds  28234  fib5  31658  fib6  31659  hgt750lem  31917  hgt750lem2  31918  hgt750leme  31924  problem4  32906  problem5  32907  sinccvglem  32910  mblfinlem3  34925  itg2addnclem2  34938  itg2addnclem3  34939  heiborlem6  35088  heiborlem7  35089  235t711  39170  ex-decpmul  39171  cu3addd  39270  3cubeslem3l  39276  3cubeslem3r  39277  jm2.23  39586  inductionexd  40498  lhe4.4ex1a  40654  stoweidlem13  42292  stoweidlem26  42305  stoweidlem34  42313  wallispilem4  42347  wallispi2lem1  42350  fmtno5lem1  43709  fmtno5lem2  43710  257prm  43717  fmtno4prmfac  43728  fmtno4nprmfac193  43730  139prmALT  43753  127prm  43757  mod42tp1mod8  43761  3exp4mod41  43775  41prothprmlem2  43777  6even  43870  11t31e341  43891  2exp340mod341  43892  gbpart8  43927  sbgoldbwt  43936  sbgoldbst  43937  evengpop3  43957  evengpoap3  43958  nnsum4primeseven  43959  nnsum4primesevenALTV  43960  2t6m3t4e0  44390  linevalexample  44444  zlmodzxzequa  44545  zlmodzxzequap  44548