Theorem 3cn 11721

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 11704	. 2 ⊢ 3 = (2 + 1)
2		2cn 11715	. . 3 ⊢ 2 ∈ ℂ
3		ax-1cn 10597	. . 3 ⊢ 1 ∈ ℂ
4	2, 3	addcli 10649	. 2 ⊢ (2 + 1) ∈ ℂ
5	1, 4	eqeltri 2911	1 ⊢ 3 ∈ ℂ

Syntax hints:   ∈ wcel 2114  (class class class)co 7158  ℂcc 10537  1c1 10540   + caddc 10542  2c2 11695  3c3 11696

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 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-ext 2795  ax-1cn 10597  ax-addcl 10599

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1781  df-cleq 2816  df-clel 2895  df-2 11703  df-3 11704

This theorem is referenced by:  3ex  11722  4cn  11725  4m1e3  11769  3p2e5  11791  3p3e6  11792  4p4e8  11795  5p4e9  11798  3t1e3  11805  3t2e6  11806  3t3e9  11807  8th4div3  11860  halfpm6th  11861  6p4e10  12173  9t8e72  12229  halfthird  12244  sq3  13564  expnass  13573  fac3  13643  sqrlem7  14610  caurcvgr  15032  bpoly2  15413  bpoly3  15414  bpoly4  15415  ef01bndlem  15539  sin01bnd  15540  cos01bnd  15541  cos1bnd  15542  cos2bnd  15543  cos01gt0  15546  rpnnen2lem3  15571  rpnnen2lem11  15579  3dvdsdec  15683  3dvds2dec  15684  3lcm2e6woprm  15961  prmo3  16379  2exp6  16424  2exp16  16426  7prm  16446  13prm  16451  17prm  16452  19prm  16453  37prm  16456  43prm  16457  83prm  16458  139prm  16459  163prm  16460  317prm  16461  631prm  16462  1259lem1  16466  1259lem2  16467  1259lem3  16468  1259lem4  16469  1259lem5  16470  1259prm  16471  2503lem1  16472  2503lem2  16473  2503lem3  16474  2503prm  16475  4001lem1  16476  4001lem2  16477  4001lem3  16478  4001lem4  16479  4001prm  16480  tangtx  25093  sincos6thpi  25103  sincos3rdpi  25104  pigt3  25105  pige3ALT  25107  2logb9irrALT  25378  ang180lem2  25390  1cubr  25422  dcubic1lem  25423  dcubic2  25424  dcubic1  25425  dcubic  25426  mcubic  25427  cubic2  25428  cubic  25429  binom4  25430  quart1cl  25434  quart1lem  25435  quart1  25436  quartlem1  25437  quartlem3  25439  log2cnv  25524  log2tlbnd  25525  log2ublem2  25527  log2ublem3  25528  log2ub  25529  basellem5  25664  basellem8  25667  basellem9  25668  cht3  25752  ppiub  25782  chtub  25790  bclbnd  25858  bposlem6  25867  bposlem8  25869  bposlem9  25870  lgsdir2lem1  25903  lgsdir2lem5  25907  2lgslem3b  25975  2lgslem3d  25977  2lgsoddprmlem3c  25990  2lgsoddprmlem3d  25991  addsqnreup  26021  pntibndlem1  26167  pntlemk  26184  ex-opab  28213  ex-exp  28231  ex-dvds  28237  ex-gcd  28238  ex-lcm  28239  ex-prmo  28240  ex-ind-dvds  28242  fib5  31665  fib6  31666  hgt750lem  31924  hgt750lem2  31925  hgt750leme  31931  problem4  32913  problem5  32914  sinccvglem  32917  mblfinlem3  34933  itg2addnclem2  34946  itg2addnclem3  34947  heiborlem6  35096  heiborlem7  35097  fac2xp3  39101  235t711  39184  ex-decpmul  39185  cu3addd  39284  3cubeslem3l  39290  3cubeslem3r  39291  jm2.23  39600  inductionexd  40512  lhe4.4ex1a  40668  stoweidlem13  42305  stoweidlem26  42318  stoweidlem34  42326  wallispilem4  42360  wallispi2lem1  42363  fmtno5lem1  43722  fmtno5lem2  43723  257prm  43730  fmtno4prmfac  43741  fmtno4nprmfac193  43743  139prmALT  43766  127prm  43770  mod42tp1mod8  43774  3exp4mod41  43788  41prothprmlem2  43790  6even  43883  11t31e341  43904  2exp340mod341  43905  gbpart8  43940  sbgoldbwt  43949  sbgoldbst  43950  evengpop3  43970  evengpoap3  43971  nnsum4primeseven  43972  nnsum4primesevenALTV  43973  2t6m3t4e0  44403  linevalexample  44457  zlmodzxzequa  44558  zlmodzxzequap  44561