Theorem 4cn 12266

Description: The number 4 is a complex number. (Contributed by David A. Wheeler, 7-Jul-2016.) Reduce dependencies on axioms. (Revised by Steven Nguyen, 4-Oct-2022.)

Assertion

Ref	Expression
4cn	⊢ 4 ∈ ℂ

Proof of Theorem 4cn

Step	Hyp	Ref	Expression
1		df-4 12246	. 2 ⊢ 4 = (3 + 1)
2		3cn 12262	. . 3 ⊢ 3 ∈ ℂ
3		ax-1cn 11096	. . 3 ⊢ 1 ∈ ℂ
4	2, 3	addcli 11151	. 2 ⊢ (3 + 1) ∈ ℂ
5	1, 4	eqeltri 2832	1 ⊢ 4 ∈ ℂ

Syntax hints:   ∈ wcel 2114  (class class class)co 7367  ℂcc 11036  1c1 11039   + caddc 11041  3c3 12237  4c4 12238

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708  ax-1cn 11096  ax-addcl 11098

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2728  df-clel 2811  df-2 12244  df-3 12245  df-4 12246

This theorem is referenced by:  5cn  12269  5m1e4  12306  4p2e6  12329  4p3e7  12330  4p4e8  12331  4t2e8  12344  4div2e2  12346  8th4div3  12397  div4p1lem1div2  12432  5p5e10  12715  4t4e16  12743  6t5e30  12751  fldiv4p1lem1div2  13794  sq4e2t8  14161  discr  14202  sqoddm1div8  14205  4bc2eq6  14291  bpoly3  16023  bpoly4  16024  cos2bnd  16155  flodddiv4  16384  6gcd4e2  16507  6lcm4e12  16585  pythagtriplem1  16787  2exp11  17060  13prm  17086  43prm  17092  163prm  17095  317prm  17096  631prm  17097  1259lem1  17101  1259lem2  17102  1259lem3  17103  1259lem4  17104  1259lem5  17105  1259prm  17106  2503lem1  17107  2503lem2  17108  2503lem3  17109  2503prm  17110  4001lem1  17111  4001lem2  17112  4001lem3  17113  4001lem4  17114  4001prm  17115  cphipval2  25208  4cphipval2  25209  minveclem2  25393  minveclem3  25396  minveclem7  25402  uniioombl  25556  dveflem  25946  sincosq4sgn  26465  tan4thpi  26478  sincos6thpi  26480  ang180lem2  26774  heron  26802  quad2  26803  quad  26804  dcubic2  26808  dcubic  26810  mcubic  26811  cubic2  26812  cubic  26813  dquartlem1  26815  dquartlem2  26816  dquart  26817  quart1cl  26818  quart1lem  26819  quart1  26820  quartlem1  26821  quartlem2  26822  quartlem4  26824  quart  26825  log2cnv  26908  log2tlbnd  26909  log2ublem3  26912  log2ub  26913  bclbnd  27243  bposlem8  27254  bposlem9  27255  2lgslem3a  27359  2lgslem3b  27360  2lgslem3c  27361  2lgslem3d  27362  2lgsoddprmlem2  27372  2lgsoddprmlem3c  27375  2lgsoddprmlem3d  27376  addsqnreup  27406  addsq2nreurex  27407  pntibndlem2  27554  pntlemb  27560  ex-opab  30502  ex-exp  30520  ex-fac  30521  ex-bc  30522  ex-ind-dvds  30531  4ipval2  30779  ipidsq  30781  dipcl  30783  dipcj  30785  dip0r  30788  dipcn  30791  ip1ilem  30897  ipasslem10  30910  minvecolem2  30946  minvecolem7  30954  normpar2i  31227  polid2i  31228  lnopeq0i  32078  quad3d  32822  constrresqrtcl  33921  cos9thpiminplylem1  33926  fib5  34549  fib6  34550  hgt750lemd  34792  hgt750lem  34795  hgt750lem2  34796  quad3  35852  60gcd7e1  42444  420lcm8e840  42450  lcmineqlem23  42490  3exp7  42492  3lexlogpow5ineq1  42493  3lexlogpow2ineq2  42498  aks4d1p1p4  42510  aks4d1p1p7  42513  aks4d1p1p5  42514  aks4d1p1  42515  4t5e20  42723  sq4  42725  235t711  42737  flt4lem5e  43089  inductionexd  44582  lhe4.4ex1a  44756  limclner  46079  stoweidlem13  46441  wallispi2lem1  46499  wallispi2lem2  46500  stirlinglem3  46504  stirlinglem10  46511  stirlinglem12  46513  sqwvfourb  46657  fouriersw  46659  sin5tlem1  47321  sin5tlem2  47322  sin5tlem3  47323  sin5tlem4  47324  cos5t  47327  goldratmolem2  47334  sinnpoly  47339  ceil5half3  47794  modm1p1ne  47824  fmtnorec4  48012  fmtno5lem4  48019  257prm  48024  fmtnofac1  48033  fmtno4prmfac  48035  fmtno5faclem1  48042  fmtno5faclem2  48043  139prmALT  48059  mod42tp1mod8  48065  3exp4mod41  48079  41prothprmlem1  48080  41prothprmlem2  48081  41prothprm  48082  ppivalnn4  48090  quad1  48096  8even  48189  2exp340mod341  48209  8exp8mod9  48212  mogoldbb  48261  nnsum4primeseven  48276  nnsum4primesevenALTV  48277  bgoldbtbndlem2  48282  zlmodzxzequap  48975  itsclc0yqsollem1  49238  itscnhlinecirc02plem1  49258  5m4e1  50272