Theorem 3cn 12159

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 12142	. 2 ⊢ 3 = (2 + 1)
2		2cn 12153	. . 3 ⊢ 2 ∈ ℂ
3		ax-1cn 11034	. . 3 ⊢ 1 ∈ ℂ
4	2, 3	addcli 11086	. 2 ⊢ (2 + 1) ∈ ℂ
5	1, 4	eqeltri 2834	1 ⊢ 3 ∈ ℂ

Syntax hints:   ∈ wcel 2106  (class class class)co 7341  ℂcc 10974  1c1 10977   + caddc 10979  2c2 12133  3c3 12134

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2708  ax-1cn 11034  ax-addcl 11036

This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1782  df-cleq 2729  df-clel 2815  df-2 12141  df-3 12142

This theorem is referenced by:  3ex  12160  4cn  12163  4m1e3  12207  3p2e5  12229  3p3e6  12230  4p4e8  12233  5p4e9  12236  3t1e3  12243  3t2e6  12244  3t3e9  12245  8th4div3  12298  halfpm6th  12299  6p4e10  12614  9t8e72  12670  halfthird  12685  sq3  14020  expnass  14029  fac3  14099  sqrlem7  15059  caurcvgr  15484  bpoly2  15866  bpoly3  15867  bpoly4  15868  ef01bndlem  15992  sin01bnd  15993  cos01bnd  15994  cos1bnd  15995  cos2bnd  15996  cos01gt0  15999  rpnnen2lem3  16024  rpnnen2lem11  16032  3dvdsdec  16140  3dvds2dec  16141  3lcm2e6woprm  16417  prmo3  16839  2exp6  16885  2exp16  16889  7prm  16909  13prm  16914  17prm  16915  19prm  16916  37prm  16919  43prm  16920  83prm  16921  139prm  16922  163prm  16923  317prm  16924  631prm  16925  1259lem1  16929  1259lem2  16930  1259lem3  16931  1259lem4  16932  1259lem5  16933  1259prm  16934  2503lem1  16935  2503lem2  16936  2503lem3  16937  2503prm  16938  4001lem1  16939  4001lem2  16940  4001lem3  16941  4001lem4  16942  4001prm  16943  tangtx  25767  sincos6thpi  25777  sincos3rdpi  25778  pigt3  25779  pige3ALT  25781  2logb9irrALT  26053  ang180lem2  26065  1cubr  26097  dcubic1lem  26098  dcubic2  26099  dcubic1  26100  dcubic  26101  mcubic  26102  cubic2  26103  cubic  26104  binom4  26105  quart1cl  26109  quart1lem  26110  quart1  26111  quartlem1  26112  quartlem3  26114  log2cnv  26199  log2tlbnd  26200  log2ublem2  26202  log2ublem3  26203  log2ub  26204  basellem5  26339  basellem8  26342  basellem9  26343  cht3  26427  ppiub  26457  chtub  26465  bclbnd  26533  bposlem6  26542  bposlem8  26544  bposlem9  26545  lgsdir2lem1  26578  lgsdir2lem5  26582  2lgslem3b  26650  2lgslem3d  26652  2lgsoddprmlem3c  26665  2lgsoddprmlem3d  26666  addsqnreup  26696  pntibndlem1  26842  pntlemk  26859  ex-opab  29083  ex-exp  29101  ex-dvds  29107  ex-gcd  29108  ex-lcm  29109  ex-prmo  29110  ex-ind-dvds  29112  fib5  32670  fib6  32671  hgt750lem  32929  hgt750lem2  32930  hgt750leme  32936  problem4  33923  problem5  33924  sinccvglem  33927  mblfinlem3  35972  itg2addnclem2  35985  itg2addnclem3  35986  heiborlem6  36130  heiborlem7  36131  3exp7  40366  3lexlogpow2ineq2  40372  3lexlogpow5ineq5  40373  aks4d1p1  40389  2ap1caineq  40409  fac2xp3  40468  235t711  40630  ex-decpmul  40631  cu3addd  40815  3cubeslem3l  40821  3cubeslem3r  40822  jm2.23  41132  inductionexd  42138  lhe4.4ex1a  42320  stoweidlem13  43942  stoweidlem26  43955  stoweidlem34  43963  wallispilem4  43997  wallispi2lem1  44000  fmtno5lem1  45423  fmtno5lem2  45424  257prm  45431  fmtno4prmfac  45442  fmtno4nprmfac193  45444  139prmALT  45466  127prm  45469  mod42tp1mod8  45472  3exp4mod41  45486  41prothprmlem2  45488  6even  45581  11t31e341  45602  2exp340mod341  45603  gbpart8  45638  sbgoldbwt  45647  sbgoldbst  45648  evengpop3  45668  evengpoap3  45669  nnsum4primeseven  45670  nnsum4primesevenALTV  45671  2t6m3t4e0  46102  linevalexample  46154  zlmodzxzequa  46255  zlmodzxzequap  46258  ackval3  46447  ackval2012  46455  ackval3012  46456  ackval41  46459  ackval42  46460