Theorem 3cn 12322

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 12304	. 2 ⊢ 3 = (2 + 1)
2		2cn 12316	. . 3 ⊢ 2 ∈ ℂ
3		ax-1cn 11158	. . 3 ⊢ 1 ∈ ℂ
4	2, 3	addcli 11215	. 2 ⊢ (2 + 1) ∈ ℂ
5	1, 4	eqeltri 2865	1 ⊢ 3 ∈ ℂ

Syntax hints:   ∈ wcel 2149  (class class class)co 7411  ℂcc 11098  1c1 11101   + caddc 11103  2c2 12295  3c3 12296

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741  ax-1cn 11158  ax-addcl 11160

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1807  df-cleq 2761  df-clel 2844  df-2 12303  df-3 12304

This theorem is referenced by:  3ex  12323  4cn  12326  4m1e3  12369  3p2e5  12391  3p3e6  12392  4p4e8  12395  5p4e9  12398  3t1e3  12405  3t2e6  12406  2t3e6  12407  3t3e9  12408  8th4div3  12464  halfthird  12465  halfpm6th  12466  6p4e10  12788  9t8e72  12844  sq3  14234  expnass  14244  fac3  14316  01sqrexlem7  15299  caurcvgr  15725  bpoly2  16111  bpoly3  16112  bpoly4  16113  ef01bndlem  16240  sin01bnd  16241  cos01bnd  16242  cos1bnd  16243  cos2bnd  16244  cos01gt0  16247  rpnnen2lem3  16272  rpnnen2lem11  16280  3dvdsdec  16390  3dvds2dec  16391  5ndvds3  16471  3lcm2e6woprm  16673  prmo3  17101  2exp6  17146  2exp16  17150  7prm  17170  13prm  17176  17prm  17177  19prm  17178  37prm  17181  43prm  17182  83prm  17183  139prm  17184  163prm  17185  317prm  17186  631prm  17187  1259lem1  17191  1259lem2  17192  1259lem3  17193  1259lem4  17194  1259lem5  17195  1259prm  17196  2503lem1  17197  2503lem2  17198  2503lem3  17199  2503prm  17200  4001lem1  17201  4001lem2  17202  4001lem3  17203  4001lem4  17204  4001prm  17205  tangtx  26636  sincos6thpi  26647  sincos3rdpi  26648  pigt3  26649  pige3ALT  26651  2logb9irrALT  26929  ang180lem2  26941  1cubr  26973  dcubic1lem  26974  dcubic2  26975  dcubic1  26976  dcubic  26977  mcubic  26978  cubic2  26979  cubic  26980  binom4  26981  quart1cl  26985  quart1lem  26986  quart1  26987  quartlem1  26988  quartlem3  26990  log2cnv  27075  log2tlbnd  27076  log2ublem2  27078  log2ublem3  27079  log2ub  27080  basellem5  27215  basellem8  27218  basellem9  27219  ppiub  27334  chtub  27342  bclbnd  27410  bposlem6  27419  bposlem8  27421  bposlem9  27422  lgsdir2lem1  27455  lgsdir2lem5  27459  2lgslem3b  27527  2lgslem3d  27529  2lgsoddprmlem3c  27542  2lgsoddprmlem3d  27543  addsqnreup  27573  pntibndlem1  27719  pntlemk  27736  ex-opab  30724  ex-exp  30742  ex-dvds  30748  ex-gcd  30749  ex-lcm  30750  ex-prmo  30751  ex-ind-dvds  30753  ply1dg3rt0irred  33819  2sqr3minply  34115  2sqr3nconstr  34116  cos9thpiminplylem2  34118  cos9thpiminplylem3  34119  cos9thpiminplylem4  34120  cos9thpiminplylem5  34121  cos9thpiminply  34123  cos9thpinconstrlem1  34124  cos9thpinconstrlem2  34125  cos9thpinconstr  34126  fib5  34740  fib6  34741  hgt750lem  34983  hgt750lem2  34984  hgt750leme  34990  problem4  36059  problem5  36060  sinccvglem  36063  mblfinlem3  38198  itg2addnclem2  38211  itg2addnclem3  38212  heiborlem6  38355  heiborlem7  38356  3exp7  42710  3lexlogpow2ineq2  42716  3lexlogpow5ineq5  42717  aks4d1p1  42733  2ap1caineq  42802  25or6to4  42863  3rdpwhole  42943  235t711  42956  ex-decpmul  42957  tan3rdpi  43003  sin2t3rdpi  43004  cos2t3rdpi  43005  sin4t3rdpi  43006  cos4t3rdpi  43007  cu3addd  43304  3cubeslem3l  43309  3cubeslem3r  43310  jm2.23  43615  inductionexd  44773  lhe4.4ex1a  44931  stoweidlem13  46619  stoweidlem26  46632  stoweidlem34  46640  wallispilem4  46674  wallispi2lem1  46677  sin5tlem1  47499  sin5tlem2  47500  sin5tlem3  47501  sin5tlem4  47502  sin5tlem5  47503  sin5t  47504  goldrasin  47508  ceil5half3  47972  fmtno5lem1  48194  fmtno5lem2  48195  257prm  48202  fmtno4prmfac  48213  fmtno4nprmfac193  48215  139prmALT  48237  127prm  48240  mod42tp1mod8  48243  3exp4mod41  48257  41prothprmlem2  48259  ppivalnn4  48268  6even  48365  11t31e341  48386  2exp340mod341  48387  gbpart8  48422  sbgoldbwt  48431  sbgoldbst  48432  evengpop3  48452  evengpoap3  48453  nnsum4primeseven  48454  nnsum4primesevenALTV  48455  2t6m3t4e0  49013  linevalexample  49060  zlmodzxzequa  49161  zlmodzxzequap  49164  ackval3  49348  ackval2012  49356  ackval3012  49357  ackval41  49360  ackval42  49361