Theorem 4cn 12210

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 12190	. 2 ⊢ 4 = (3 + 1)
2		3cn 12206	. . 3 ⊢ 3 ∈ ℂ
3		ax-1cn 11064	. . 3 ⊢ 1 ∈ ℂ
4	2, 3	addcli 11118	. 2 ⊢ (3 + 1) ∈ ℂ
5	1, 4	eqeltri 2827	1 ⊢ 4 ∈ ℂ

Syntax hints:   ∈ wcel 2111  (class class class)co 7346  ℂcc 11004  1c1 11007   + caddc 11009  3c3 12181  4c4 12182

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703  ax-1cn 11064  ax-addcl 11066

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2723  df-clel 2806  df-2 12188  df-3 12189  df-4 12190

This theorem is referenced by:  5cn  12213  5m1e4  12250  4p2e6  12273  4p3e7  12274  4p4e8  12275  4t2e8  12288  4d2e2  12290  8th4div3  12341  div4p1lem1div2  12376  5p5e10  12659  4t4e16  12687  6t5e30  12695  fldiv4p1lem1div2  13739  sq4e2t8  14106  discr  14147  sqoddm1div8  14150  4bc2eq6  14236  bpoly3  15965  bpoly4  15966  cos2bnd  16097  flodddiv4  16326  6gcd4e2  16449  6lcm4e12  16527  pythagtriplem1  16728  2exp11  17001  13prm  17027  43prm  17033  163prm  17036  317prm  17037  631prm  17038  1259lem1  17042  1259lem2  17043  1259lem3  17044  1259lem4  17045  1259lem5  17046  1259prm  17047  2503lem1  17048  2503lem2  17049  2503lem3  17050  2503prm  17051  4001lem1  17052  4001lem2  17053  4001lem3  17054  4001lem4  17055  4001prm  17056  cphipval2  25168  4cphipval2  25169  minveclem2  25353  minveclem3  25356  minveclem7  25362  uniioombl  25517  dveflem  25910  sincosq4sgn  26437  tan4thpi  26450  sincos6thpi  26452  ang180lem2  26747  heron  26775  quad2  26776  quad  26777  dcubic2  26781  dcubic  26783  mcubic  26784  cubic2  26785  cubic  26786  dquartlem1  26788  dquartlem2  26789  dquart  26790  quart1cl  26791  quart1lem  26792  quart1  26793  quartlem1  26794  quartlem2  26795  quartlem4  26797  quart  26798  log2cnv  26881  log2tlbnd  26882  log2ublem3  26885  log2ub  26886  bclbnd  27218  bposlem8  27229  bposlem9  27230  2lgslem3a  27334  2lgslem3b  27335  2lgslem3c  27336  2lgslem3d  27337  2lgsoddprmlem2  27347  2lgsoddprmlem3c  27350  2lgsoddprmlem3d  27351  addsqnreup  27381  addsq2nreurex  27382  pntibndlem2  27529  pntlemb  27535  ex-opab  30412  ex-exp  30430  ex-fac  30431  ex-bc  30432  ex-ind-dvds  30441  4ipval2  30688  ipidsq  30690  dipcl  30692  dipcj  30694  dip0r  30697  dipcn  30700  ip1ilem  30806  ipasslem10  30819  minvecolem2  30855  minvecolem7  30863  normpar2i  31136  polid2i  31137  lnopeq0i  31987  quad3d  32733  constrresqrtcl  33790  cos9thpiminplylem1  33795  fib5  34418  fib6  34419  hgt750lemd  34661  hgt750lem  34664  hgt750lem2  34665  quad3  35714  60gcd7e1  42108  420lcm8e840  42114  lcmineqlem23  42154  3exp7  42156  3lexlogpow5ineq1  42157  3lexlogpow2ineq2  42162  aks4d1p1p4  42174  aks4d1p1p7  42177  aks4d1p1p5  42178  aks4d1p1  42179  4t5e20  42394  sq4  42396  235t711  42408  flt4lem5e  42759  inductionexd  44258  lhe4.4ex1a  44432  limclner  45759  stoweidlem13  46121  wallispi2lem1  46179  wallispi2lem2  46180  stirlinglem3  46184  stirlinglem10  46191  stirlinglem12  46193  sqwvfourb  46337  fouriersw  46339  sinnpoly  47001  ceil5half3  47450  modm1p1ne  47480  fmtnorec4  47659  fmtno5lem4  47666  257prm  47671  fmtnofac1  47680  fmtno4prmfac  47682  fmtno5faclem1  47689  fmtno5faclem2  47690  139prmALT  47706  mod42tp1mod8  47712  3exp4mod41  47726  41prothprmlem1  47727  41prothprmlem2  47728  41prothprm  47729  quad1  47730  8even  47823  2exp340mod341  47843  8exp8mod9  47846  mogoldbb  47895  nnsum4primeseven  47910  nnsum4primesevenALTV  47911  bgoldbtbndlem2  47916  zlmodzxzequap  48610  itsclc0yqsollem1  48873  itscnhlinecirc02plem1  48893  5m4e1  49908