Theorem 3cn 12339

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 12321	. 2 ⊢ 3 = (2 + 1)
2		2cn 12333	. . 3 ⊢ 2 ∈ ℂ
3		ax-1cn 11175	. . 3 ⊢ 1 ∈ ℂ
4	2, 3	addcli 11232	. 2 ⊢ (2 + 1) ∈ ℂ
5	1, 4	eqeltri 2861	1 ⊢ 3 ∈ ℂ

This proof depends on syntax axioms:   ∈ wcel 2146  (class class class)co 7419  ℂcc 11115  1c1 11118   + caddc 11120  2c2 12312  3c3 12313

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2737  ax-1cn 11175  ax-addcl 11177

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2757  df-clel 2840  df-2 12320  df-3 12321

This theorem is used by:  3ex  12340  4cn  12343  4m1e3  12386  3p2e5  12408  3p3e6  12409  4p4e8  12412  5p4e9  12415  3t1e3  12422  3t2e6  12423  2t3e6  12424  3t3e9  12425  8th4div3  12481  halfthird  12482  halfpm6th  12483  6p4e10  12806  9t8e72  12862  sq3  14254  expnass  14264  01sqrexlem7  15325  caurcvgr  15751  bpoly2  16135  bpoly3  16136  bpoly4  16137  ef01bndlem  16264  sin01bnd  16265  cos01bnd  16266  cos1bnd  16267  cos2bnd  16268  cos01gt0  16271  rpnnen2lem3  16296  rpnnen2lem11  16304  3dvdsdec  16414  3dvds2dec  16415  5ndvds3  16495  3lcm2e6woprm  16697  2exp16  17174  13prm  17200  17prm  17201  19prm  17202  37prm  17205  43prm  17206  83prm  17207  139prm  17208  163prm  17209  317prm  17210  631prm  17211  1259lem1  17215  1259lem2  17216  1259lem3  17217  1259lem4  17218  1259lem5  17219  1259prm  17220  2503lem1  17221  2503lem2  17222  2503lem3  17223  2503prm  17224  4001lem1  17225  4001lem2  17226  4001lem3  17227  4001lem4  17228  4001prm  17229  tangtx  26723  sincos6thpi  26734  sincos3rdpi  26735  pigt3  26736  pige3ALT  26738  2logb9irrALT  27016  ang180lem2  27028  1cubr  27060  dcubic1lem  27061  dcubic2  27062  dcubic1  27063  dcubic  27064  mcubic  27065  cubic2  27066  cubic  27067  binom4  27068  quart1cl  27072  quart1lem  27073  quart1  27074  quartlem1  27075  quartlem3  27077  log2cnv  27162  log2tlbnd  27163  log2ublem2  27165  log2ublem3  27166  log2ub  27167  basellem5  27302  basellem8  27305  basellem9  27306  ppiub  27421  chtub  27429  bclbnd  27497  bposlem6  27506  bposlem8  27508  bposlem9  27509  lgsdir2lem1  27542  lgsdir2lem5  27546  2lgslem3b  27614  2lgslem3d  27616  2lgsoddprmlem3c  27629  2lgsoddprmlem3d  27630  addsqnreup  27660  pntibndlem1  27806  pntlemk  27823  ex-opab  30856  ex-exp  30874  ex-dvds  30880  ex-gcd  30881  ex-lcm  30882  ex-prmo  30883  ex-ind-dvds  30885  ply1dg3rt0irred  33940  2sqr3minply  34236  2sqr3nconstr  34237  cos9thpiminplylem2  34239  cos9thpiminplylem3  34240  cos9thpiminplylem4  34241  cos9thpiminplylem5  34242  cos9thpiminply  34244  cos9thpinconstrlem1  34245  cos9thpinconstrlem2  34246  cos9thpinconstr  34247  fib5  34862  fib6  34863  hgt750lem  35105  hgt750lem2  35106  hgt750leme  35112  problem4  36199  problem5  36200  sinccvglem  36203  mblfinlem3  38369  itg2addnclem2  38382  itg2addnclem3  38383  heiborlem6  38527  heiborlem7  38528  3lexlogpow2ineq2  42886  3lexlogpow5ineq5  42887  aks4d1p1  42903  2ap1caineq  42972  25or6to4  43033  3rdpwhole  43113  235t711  43126  ex-decpmul  43127  tan3rdpi  43173  sin2t3rdpi  43174  cos2t3rdpi  43175  sin4t3rdpi  43176  cos4t3rdpi  43177  cu3addd  43472  3cubeslem3l  43477  3cubeslem3r  43478  jm2.23  43783  inductionexd  44941  lhe4.4ex1a  45099  stoweidlem13  46787  stoweidlem26  46800  stoweidlem34  46808  wallispilem4  46842  wallispi2lem1  46845  sin5tlem1  47670  sin5tlem2  47671  sin5tlem3  47672  sin5tlem4  47673  sin5tlem5  47674  sin5t  47675  goldrasin  47679  ceil5half3  48143  fmtno5lem1  48365  fmtno5lem2  48366  257prm  48373  fmtno4prmfac  48384  fmtno4nprmfac193  48386  139prmALT  48408  127prm  48411  mod42tp1mod8  48414  3exp4mod41  48428  41prothprmlem2  48430  ppivalnn4  48439  6even  48536  11t31e341  48557  2exp340mod341  48558  gbpart8  48593  sbgoldbwt  48602  sbgoldbst  48603  evengpop3  48623  evengpoap3  48624  nnsum4primeseven  48625  nnsum4primesevenALTV  48626  2t6m3t4e0  49187  linevalexample  49234  zlmodzxzequa  49335  zlmodzxzequap  49338  ackval3  49522  ackval2012  49530  ackval3012  49531  ackval41  49534  ackval42  49535