Theorem 3cn 12464

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 12446	. 2 ⊢ 3 = (2 + 1)
2		2cn 12458	. . 3 ⊢ 2 ∈ ℂ
3		ax-1cn 11297	. . 3 ⊢ 1 ∈ ℂ
4	2, 3	addcli 11354	. 2 ⊢ (2 + 1) ∈ ℂ
5	1, 4	eqeltri 2860	1 ⊢ 3 ∈ ℂ

This proof depends on syntax axioms:   ∈ wcel 2147  (class class class)co 7451  ℂcc 11237  1c1 11240   + caddc 11242  2c2 12437  3c3 12438

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735  ax-1cn 11297  ax-addcl 11299

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2755  df-clel 2839  df-2 12445  df-3 12446

This theorem is used by:  3ex  12465  4cn  12468  4m1e3  12511  3p2e5  12533  3p3e6  12534  4p4e8  12537  5p4e9  12540  3t1e3  12547  3t2e6  12548  2t3e6  12549  3t3e9  12550  8th4div3  12606  halfthird  12607  halfpm6th  12608  6p4e10  12931  9t8e72  12987  sq3  14381  expnass  14392  01sqrexlem7  15458  caurcvgr  15885  bpoly2  16267  bpoly3  16268  bpoly4  16269  ef01bndlem  16396  sin01bnd  16397  cos01bnd  16398  cos1bnd  16399  cos2bnd  16400  cos01gt0  16403  rpnnen2lem3  16428  rpnnen2lem11  16436  3dvdsdec  16546  3dvds2dec  16547  5ndvds3  16627  3lcm2e6woprm  16834  2exp16  17312  13prm  17338  17prm  17339  19prm  17340  37prm  17343  43prm  17344  83prm  17345  139prm  17346  163prm  17347  317prm  17348  631prm  17349  1259lem1  17353  1259lem2  17354  1259lem3  17355  1259lem4  17356  1259lem5  17357  1259prm  17358  2503lem1  17359  2503lem2  17360  2503lem3  17361  2503prm  17362  4001lem1  17363  4001lem2  17364  4001lem3  17365  4001lem4  17366  4001prm  17367  tangtx  26891  sincos6thpi  26901  sincos3rdpi  26902  pigt3  26903  pige3ALT  26905  2logb9irrALT  27183  ang180lem2  27195  1cubr  27227  dcubic1lem  27228  dcubic2  27229  dcubic1  27230  dcubic  27231  mcubic  27232  cubic2  27233  cubic  27234  binom4  27235  quart1cl  27239  quart1lem  27240  quart1  27241  quartlem1  27242  quartlem3  27244  log2cnv  27329  log2tlbnd  27330  log2ublem2  27332  log2ublem3  27333  log2ub  27334  basellem5  27469  basellem8  27472  basellem9  27473  ppiub  27588  chtub  27596  bclbnd  27664  bposlem6  27673  bposlem8  27675  bposlem9  27676  lgsdir2lem1  27709  lgsdir2lem5  27713  2lgslem3b  27781  2lgslem3d  27783  2lgsoddprmlem3c  27796  2lgsoddprmlem3d  27797  addsqnreup  27827  pntibndlem1  27973  pntlemk  27990  ex-opab  31090  ex-exp  31108  ex-dvds  31114  ex-gcd  31115  ex-lcm  31116  ex-prmo  31117  ex-ind-dvds  31119  ply1dg3rt0irred  34219  2sqr3minply  34523  2sqr3nconstr  34524  cos9thpiminplylem2  34526  cos9thpiminplylem3  34527  cos9thpiminplylem4  34528  cos9thpiminplylem5  34529  cos9thpiminply  34531  cos9thpinconstrlem1  34532  cos9thpinconstrlem2  34533  cos9thpinconstr  34534  fib5  35148  fib6  35149  hgt750lem  35391  hgt750lem2  35392  hgt750leme  35398  problem4  36641  problem5  36642  sinccvglem  36645  mblfinlem3  38845  itg2addnclem2  38858  itg2addnclem3  38859  heiborlem6  39016  heiborlem7  39017  3lexlogpow2ineq2  43375  3lexlogpow5ineq5  43376  aks4d1p1  43392  2ap1caineq  43461  25or6to4  43522  1p4e5  43577  2p5e7  43584  3p4e7  43587  3p5e8  43588  3p6e9  43589  3rdpwhole  43615  235t711  43628  ex-decpmul  43629  tan3rdpi  43669  sin2t3rdpi  43670  cos2t3rdpi  43671  sin4t3rdpi  43672  cos4t3rdpi  43673  cu3addd  43957  3cubeslem3l  43962  3cubeslem3r  43963  jm2.23  44269  inductionexd  45416  lhe4.4ex1a  45574  stoweidlem13  47296  stoweidlem26  47309  stoweidlem34  47317  wallispilem4  47351  wallispi2lem1  47354  sin5tlem1  48192  sin5tlem2  48193  sin5tlem3  48194  sin5tlem4  48195  sin5tlem5  48196  sin5t  48197  goldrasin  48202  ceil5half3  48689  fmtno5lem1  48911  fmtno5lem2  48912  257prm  48919  fmtno4prmfac  48930  fmtno4nprmfac193  48932  139prmALT  48954  127prm  48957  mod42tp1mod8  48960  3exp4mod41  48974  41prothprmlem2  48976  ppivalnn4  48985  6even  49082  11t31e341  49103  2exp340mod341  49104  gbpart8  49139  sbgoldbwt  49148  sbgoldbst  49149  evengpop3  49169  evengpoap3  49170  nnsum4primeseven  49171  nnsum4primesevenALTV  49172  bru3val  49753  bru3cj  49754  2t6m3t4e0  49791  linevalexample  49838  zlmodzxzequa  49939  zlmodzxzequap  49942  ackval3  50126  ackval2012  50134  ackval3012  50135  ackval41  50138  ackval42  50139