Theorem 3cn 11984

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 11967	. 2 ⊢ 3 = (2 + 1)
2		2cn 11978	. . 3 ⊢ 2 ∈ ℂ
3		ax-1cn 10860	. . 3 ⊢ 1 ∈ ℂ
4	2, 3	addcli 10912	. 2 ⊢ (2 + 1) ∈ ℂ
5	1, 4	eqeltri 2835	1 ⊢ 3 ∈ ℂ

Syntax hints:   ∈ wcel 2108  (class class class)co 7255  ℂcc 10800  1c1 10803   + caddc 10805  2c2 11958  3c3 11959

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709  ax-1cn 10860  ax-addcl 10862

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1784  df-cleq 2730  df-clel 2817  df-2 11966  df-3 11967

This theorem is referenced by:  3ex  11985  4cn  11988  4m1e3  12032  3p2e5  12054  3p3e6  12055  4p4e8  12058  5p4e9  12061  3t1e3  12068  3t2e6  12069  3t3e9  12070  8th4div3  12123  halfpm6th  12124  6p4e10  12438  9t8e72  12494  halfthird  12509  sq3  13843  expnass  13852  fac3  13922  sqrlem7  14888  caurcvgr  15313  bpoly2  15695  bpoly3  15696  bpoly4  15697  ef01bndlem  15821  sin01bnd  15822  cos01bnd  15823  cos1bnd  15824  cos2bnd  15825  cos01gt0  15828  rpnnen2lem3  15853  rpnnen2lem11  15861  3dvdsdec  15969  3dvds2dec  15970  3lcm2e6woprm  16248  prmo3  16670  2exp6  16716  2exp16  16720  7prm  16740  13prm  16745  17prm  16746  19prm  16747  37prm  16750  43prm  16751  83prm  16752  139prm  16753  163prm  16754  317prm  16755  631prm  16756  1259lem1  16760  1259lem2  16761  1259lem3  16762  1259lem4  16763  1259lem5  16764  1259prm  16765  2503lem1  16766  2503lem2  16767  2503lem3  16768  2503prm  16769  4001lem1  16770  4001lem2  16771  4001lem3  16772  4001lem4  16773  4001prm  16774  tangtx  25567  sincos6thpi  25577  sincos3rdpi  25578  pigt3  25579  pige3ALT  25581  2logb9irrALT  25853  ang180lem2  25865  1cubr  25897  dcubic1lem  25898  dcubic2  25899  dcubic1  25900  dcubic  25901  mcubic  25902  cubic2  25903  cubic  25904  binom4  25905  quart1cl  25909  quart1lem  25910  quart1  25911  quartlem1  25912  quartlem3  25914  log2cnv  25999  log2tlbnd  26000  log2ublem2  26002  log2ublem3  26003  log2ub  26004  basellem5  26139  basellem8  26142  basellem9  26143  cht3  26227  ppiub  26257  chtub  26265  bclbnd  26333  bposlem6  26342  bposlem8  26344  bposlem9  26345  lgsdir2lem1  26378  lgsdir2lem5  26382  2lgslem3b  26450  2lgslem3d  26452  2lgsoddprmlem3c  26465  2lgsoddprmlem3d  26466  addsqnreup  26496  pntibndlem1  26642  pntlemk  26659  ex-opab  28697  ex-exp  28715  ex-dvds  28721  ex-gcd  28722  ex-lcm  28723  ex-prmo  28724  ex-ind-dvds  28726  fib5  32272  fib6  32273  hgt750lem  32531  hgt750lem2  32532  hgt750leme  32538  problem4  33526  problem5  33527  sinccvglem  33530  mblfinlem3  35743  itg2addnclem2  35756  itg2addnclem3  35757  heiborlem6  35901  heiborlem7  35902  3exp7  39989  3lexlogpow2ineq2  39995  3lexlogpow5ineq5  39996  aks4d1p1  40012  2ap1caineq  40029  fac2xp3  40088  235t711  40240  ex-decpmul  40241  cu3addd  40418  3cubeslem3l  40424  3cubeslem3r  40425  jm2.23  40734  inductionexd  41654  lhe4.4ex1a  41836  stoweidlem13  43444  stoweidlem26  43457  stoweidlem34  43465  wallispilem4  43499  wallispi2lem1  43502  fmtno5lem1  44893  fmtno5lem2  44894  257prm  44901  fmtno4prmfac  44912  fmtno4nprmfac193  44914  139prmALT  44936  127prm  44939  mod42tp1mod8  44942  3exp4mod41  44956  41prothprmlem2  44958  6even  45051  11t31e341  45072  2exp340mod341  45073  gbpart8  45108  sbgoldbwt  45117  sbgoldbst  45118  evengpop3  45138  evengpoap3  45139  nnsum4primeseven  45140  nnsum4primesevenALTV  45141  2t6m3t4e0  45572  linevalexample  45624  zlmodzxzequa  45725  zlmodzxzequap  45728  ackval3  45917  ackval2012  45925  ackval3012  45926  ackval41  45929  ackval42  45930