Theorem 4cn 12213

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 12193	. 2 ⊢ 4 = (3 + 1)
2		3cn 12209	. . 3 ⊢ 3 ∈ ℂ
3		ax-1cn 11067	. . 3 ⊢ 1 ∈ ℂ
4	2, 3	addcli 11121	. 2 ⊢ (3 + 1) ∈ ℂ
5	1, 4	eqeltri 2824	1 ⊢ 4 ∈ ℂ

Syntax hints:   ∈ wcel 2109  (class class class)co 7349  ℂcc 11007  1c1 11010   + caddc 11012  3c3 12184  4c4 12185

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-1cn 11067  ax-addcl 11069

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2721  df-clel 2803  df-2 12191  df-3 12192  df-4 12193

This theorem is referenced by:  5cn  12216  5m1e4  12253  4p2e6  12276  4p3e7  12277  4p4e8  12278  4t2e8  12291  4d2e2  12293  8th4div3  12344  div4p1lem1div2  12379  5p5e10  12662  4t4e16  12690  6t5e30  12698  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  25139  4cphipval2  25140  minveclem2  25324  minveclem3  25327  minveclem7  25333  uniioombl  25488  dveflem  25881  sincosq4sgn  26408  tan4thpi  26421  sincos6thpi  26423  ang180lem2  26718  heron  26746  quad2  26747  quad  26748  dcubic2  26752  dcubic  26754  mcubic  26755  cubic2  26756  cubic  26757  dquartlem1  26759  dquartlem2  26760  dquart  26761  quart1cl  26762  quart1lem  26763  quart1  26764  quartlem1  26765  quartlem2  26766  quartlem4  26768  quart  26769  log2cnv  26852  log2tlbnd  26853  log2ublem3  26856  log2ub  26857  bclbnd  27189  bposlem8  27200  bposlem9  27201  2lgslem3a  27305  2lgslem3b  27306  2lgslem3c  27307  2lgslem3d  27308  2lgsoddprmlem2  27318  2lgsoddprmlem3c  27321  2lgsoddprmlem3d  27322  addsqnreup  27352  addsq2nreurex  27353  pntibndlem2  27500  pntlemb  27506  ex-opab  30376  ex-exp  30394  ex-fac  30395  ex-bc  30396  ex-ind-dvds  30405  4ipval2  30652  ipidsq  30654  dipcl  30656  dipcj  30658  dip0r  30661  dipcn  30664  ip1ilem  30770  ipasslem10  30783  minvecolem2  30819  minvecolem7  30827  normpar2i  31100  polid2i  31101  lnopeq0i  31951  quad3d  32693  constrresqrtcl  33744  cos9thpiminplylem1  33749  fib5  34373  fib6  34374  hgt750lemd  34616  hgt750lem  34619  hgt750lem2  34620  quad3  35647  60gcd7e1  41982  420lcm8e840  41988  lcmineqlem23  42028  3exp7  42030  3lexlogpow5ineq1  42031  3lexlogpow2ineq2  42036  aks4d1p1p4  42048  aks4d1p1p7  42051  aks4d1p1p5  42052  aks4d1p1  42053  4t5e20  42268  sq4  42270  235t711  42282  flt4lem5e  42633  inductionexd  44132  lhe4.4ex1a  44306  limclner  45636  stoweidlem13  45998  wallispi2lem1  46056  wallispi2lem2  46057  stirlinglem3  46061  stirlinglem10  46068  stirlinglem12  46070  sqwvfourb  46214  fouriersw  46216  sinnpoly  46879  ceil5half3  47328  modm1p1ne  47358  fmtnorec4  47537  fmtno5lem4  47544  257prm  47549  fmtnofac1  47558  fmtno4prmfac  47560  fmtno5faclem1  47567  fmtno5faclem2  47568  139prmALT  47584  mod42tp1mod8  47590  3exp4mod41  47604  41prothprmlem1  47605  41prothprmlem2  47606  41prothprm  47607  quad1  47608  8even  47701  2exp340mod341  47721  8exp8mod9  47724  mogoldbb  47773  nnsum4primeseven  47788  nnsum4primesevenALTV  47789  bgoldbtbndlem2  47794  zlmodzxzequap  48488  itsclc0yqsollem1  48751  itscnhlinecirc02plem1  48771  5m4e1  49786