Theorem 3cn 12054

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 12037	. 2 ⊢ 3 = (2 + 1)
2		2cn 12048	. . 3 ⊢ 2 ∈ ℂ
3		ax-1cn 10929	. . 3 ⊢ 1 ∈ ℂ
4	2, 3	addcli 10981	. 2 ⊢ (2 + 1) ∈ ℂ
5	1, 4	eqeltri 2835	1 ⊢ 3 ∈ ℂ

Syntax hints:   ∈ wcel 2106  (class class class)co 7275  ℂcc 10869  1c1 10872   + caddc 10874  2c2 12028  3c3 12029

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709  ax-1cn 10929  ax-addcl 10931

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1783  df-cleq 2730  df-clel 2816  df-2 12036  df-3 12037

This theorem is referenced by:  3ex  12055  4cn  12058  4m1e3  12102  3p2e5  12124  3p3e6  12125  4p4e8  12128  5p4e9  12131  3t1e3  12138  3t2e6  12139  3t3e9  12140  8th4div3  12193  halfpm6th  12194  6p4e10  12509  9t8e72  12565  halfthird  12580  sq3  13915  expnass  13924  fac3  13994  sqrlem7  14960  caurcvgr  15385  bpoly2  15767  bpoly3  15768  bpoly4  15769  ef01bndlem  15893  sin01bnd  15894  cos01bnd  15895  cos1bnd  15896  cos2bnd  15897  cos01gt0  15900  rpnnen2lem3  15925  rpnnen2lem11  15933  3dvdsdec  16041  3dvds2dec  16042  3lcm2e6woprm  16320  prmo3  16742  2exp6  16788  2exp16  16792  7prm  16812  13prm  16817  17prm  16818  19prm  16819  37prm  16822  43prm  16823  83prm  16824  139prm  16825  163prm  16826  317prm  16827  631prm  16828  1259lem1  16832  1259lem2  16833  1259lem3  16834  1259lem4  16835  1259lem5  16836  1259prm  16837  2503lem1  16838  2503lem2  16839  2503lem3  16840  2503prm  16841  4001lem1  16842  4001lem2  16843  4001lem3  16844  4001lem4  16845  4001prm  16846  tangtx  25662  sincos6thpi  25672  sincos3rdpi  25673  pigt3  25674  pige3ALT  25676  2logb9irrALT  25948  ang180lem2  25960  1cubr  25992  dcubic1lem  25993  dcubic2  25994  dcubic1  25995  dcubic  25996  mcubic  25997  cubic2  25998  cubic  25999  binom4  26000  quart1cl  26004  quart1lem  26005  quart1  26006  quartlem1  26007  quartlem3  26009  log2cnv  26094  log2tlbnd  26095  log2ublem2  26097  log2ublem3  26098  log2ub  26099  basellem5  26234  basellem8  26237  basellem9  26238  cht3  26322  ppiub  26352  chtub  26360  bclbnd  26428  bposlem6  26437  bposlem8  26439  bposlem9  26440  lgsdir2lem1  26473  lgsdir2lem5  26477  2lgslem3b  26545  2lgslem3d  26547  2lgsoddprmlem3c  26560  2lgsoddprmlem3d  26561  addsqnreup  26591  pntibndlem1  26737  pntlemk  26754  ex-opab  28796  ex-exp  28814  ex-dvds  28820  ex-gcd  28821  ex-lcm  28822  ex-prmo  28823  ex-ind-dvds  28825  fib5  32372  fib6  32373  hgt750lem  32631  hgt750lem2  32632  hgt750leme  32638  problem4  33626  problem5  33627  sinccvglem  33630  mblfinlem3  35816  itg2addnclem2  35829  itg2addnclem3  35830  heiborlem6  35974  heiborlem7  35975  3exp7  40061  3lexlogpow2ineq2  40067  3lexlogpow5ineq5  40068  aks4d1p1  40084  2ap1caineq  40101  fac2xp3  40160  235t711  40319  ex-decpmul  40320  cu3addd  40502  3cubeslem3l  40508  3cubeslem3r  40509  jm2.23  40818  inductionexd  41765  lhe4.4ex1a  41947  stoweidlem13  43554  stoweidlem26  43567  stoweidlem34  43575  wallispilem4  43609  wallispi2lem1  43612  fmtno5lem1  45005  fmtno5lem2  45006  257prm  45013  fmtno4prmfac  45024  fmtno4nprmfac193  45026  139prmALT  45048  127prm  45051  mod42tp1mod8  45054  3exp4mod41  45068  41prothprmlem2  45070  6even  45163  11t31e341  45184  2exp340mod341  45185  gbpart8  45220  sbgoldbwt  45229  sbgoldbst  45230  evengpop3  45250  evengpoap3  45251  nnsum4primeseven  45252  nnsum4primesevenALTV  45253  2t6m3t4e0  45684  linevalexample  45736  zlmodzxzequa  45837  zlmodzxzequap  45840  ackval3  46029  ackval2012  46037  ackval3012  46038  ackval41  46041  ackval42  46042