Theorem 4cn 12242

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 12222	. 2 ⊢ 4 = (3 + 1)
2		3cn 12238	. . 3 ⊢ 3 ∈ ℂ
3		ax-1cn 11096	. . 3 ⊢ 1 ∈ ℂ
4	2, 3	addcli 11150	. 2 ⊢ (3 + 1) ∈ ℂ
5	1, 4	eqeltri 2833	1 ⊢ 4 ∈ ℂ

Syntax hints:   ∈ wcel 2114  (class class class)co 7368  ℂcc 11036  1c1 11039   + caddc 11041  3c3 12213  4c4 12214

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 2709  ax-1cn 11096  ax-addcl 11098

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2729  df-clel 2812  df-2 12220  df-3 12221  df-4 12222

This theorem is referenced by:  5cn  12245  5m1e4  12282  4p2e6  12305  4p3e7  12306  4p4e8  12307  4t2e8  12320  4div2e2  12322  8th4div3  12373  div4p1lem1div2  12408  5p5e10  12690  4t4e16  12718  6t5e30  12726  fldiv4p1lem1div2  13767  sq4e2t8  14134  discr  14175  sqoddm1div8  14178  4bc2eq6  14264  bpoly3  15993  bpoly4  15994  cos2bnd  16125  flodddiv4  16354  6gcd4e2  16477  6lcm4e12  16555  pythagtriplem1  16756  2exp11  17029  13prm  17055  43prm  17061  163prm  17064  317prm  17065  631prm  17066  1259lem1  17070  1259lem2  17071  1259lem3  17072  1259lem4  17073  1259lem5  17074  1259prm  17075  2503lem1  17076  2503lem2  17077  2503lem3  17078  2503prm  17079  4001lem1  17080  4001lem2  17081  4001lem3  17082  4001lem4  17083  4001prm  17084  cphipval2  25209  4cphipval2  25210  minveclem2  25394  minveclem3  25397  minveclem7  25403  uniioombl  25558  dveflem  25951  sincosq4sgn  26478  tan4thpi  26491  sincos6thpi  26493  ang180lem2  26788  heron  26816  quad2  26817  quad  26818  dcubic2  26822  dcubic  26824  mcubic  26825  cubic2  26826  cubic  26827  dquartlem1  26829  dquartlem2  26830  dquart  26831  quart1cl  26832  quart1lem  26833  quart1  26834  quartlem1  26835  quartlem2  26836  quartlem4  26838  quart  26839  log2cnv  26922  log2tlbnd  26923  log2ublem3  26926  log2ub  26927  bclbnd  27259  bposlem8  27270  bposlem9  27271  2lgslem3a  27375  2lgslem3b  27376  2lgslem3c  27377  2lgslem3d  27378  2lgsoddprmlem2  27388  2lgsoddprmlem3c  27391  2lgsoddprmlem3d  27392  addsqnreup  27422  addsq2nreurex  27423  pntibndlem2  27570  pntlemb  27576  ex-opab  30519  ex-exp  30537  ex-fac  30538  ex-bc  30539  ex-ind-dvds  30548  4ipval2  30796  ipidsq  30798  dipcl  30800  dipcj  30802  dip0r  30805  dipcn  30808  ip1ilem  30914  ipasslem10  30927  minvecolem2  30963  minvecolem7  30971  normpar2i  31244  polid2i  31245  lnopeq0i  32095  quad3d  32840  constrresqrtcl  33955  cos9thpiminplylem1  33960  fib5  34583  fib6  34584  hgt750lemd  34826  hgt750lem  34829  hgt750lem2  34830  quad3  35886  60gcd7e1  42375  420lcm8e840  42381  lcmineqlem23  42421  3exp7  42423  3lexlogpow5ineq1  42424  3lexlogpow2ineq2  42429  aks4d1p1p4  42441  aks4d1p1p7  42444  aks4d1p1p5  42445  aks4d1p1  42446  4t5e20  42661  sq4  42663  235t711  42675  flt4lem5e  43014  inductionexd  44511  lhe4.4ex1a  44685  limclner  46009  stoweidlem13  46371  wallispi2lem1  46429  wallispi2lem2  46430  stirlinglem3  46434  stirlinglem10  46441  stirlinglem12  46443  sqwvfourb  46587  fouriersw  46589  sinnpoly  47251  ceil5half3  47700  modm1p1ne  47730  fmtnorec4  47909  fmtno5lem4  47916  257prm  47921  fmtnofac1  47930  fmtno4prmfac  47932  fmtno5faclem1  47939  fmtno5faclem2  47940  139prmALT  47956  mod42tp1mod8  47962  3exp4mod41  47976  41prothprmlem1  47977  41prothprmlem2  47978  41prothprm  47979  quad1  47980  8even  48073  2exp340mod341  48093  8exp8mod9  48096  mogoldbb  48145  nnsum4primeseven  48160  nnsum4primesevenALTV  48161  bgoldbtbndlem2  48166  zlmodzxzequap  48859  itsclc0yqsollem1  49122  itscnhlinecirc02plem1  49142  5m4e1  50156