Theorem 4cn 12151

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 12131	. 2 ⊢ 4 = (3 + 1)
2		3cn 12147	. . 3 ⊢ 3 ∈ ℂ
3		ax-1cn 11022	. . 3 ⊢ 1 ∈ ℂ
4	2, 3	addcli 11074	. 2 ⊢ (3 + 1) ∈ ℂ
5	1, 4	eqeltri 2833	1 ⊢ 4 ∈ ℂ

Syntax hints:   ∈ wcel 2105  (class class class)co 7329  ℂcc 10962  1c1 10965   + caddc 10967  3c3 12122  4c4 12123

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 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-ext 2707  ax-1cn 11022  ax-addcl 11024

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1781  df-cleq 2728  df-clel 2814  df-2 12129  df-3 12130  df-4 12131

This theorem is referenced by:  5cn  12154  5m1e4  12196  4p2e6  12219  4p3e7  12220  4p4e8  12221  4t2e8  12234  4d2e2  12236  8th4div3  12286  div4p1lem1div2  12321  5p5e10  12601  4t4e16  12629  6t5e30  12637  fldiv4p1lem1div2  13648  sq4e2t8  14009  discr  14048  sqoddm1div8  14051  4bc2eq6  14136  bpoly3  15859  bpoly4  15860  cos2bnd  15988  flodddiv4  16213  6gcd4e2  16337  6lcm4e12  16410  pythagtriplem1  16606  2exp11  16880  13prm  16906  43prm  16912  163prm  16915  317prm  16916  631prm  16917  1259lem1  16921  1259lem2  16922  1259lem3  16923  1259lem4  16924  1259lem5  16925  1259prm  16926  2503lem1  16927  2503lem2  16928  2503lem3  16929  2503prm  16930  4001lem1  16931  4001lem2  16932  4001lem3  16933  4001lem4  16934  4001prm  16935  cphipval2  24503  4cphipval2  24504  minveclem2  24688  minveclem3  24691  minveclem7  24697  uniioombl  24851  dveflem  25241  sincosq4sgn  25756  sincos6thpi  25770  ang180lem2  26058  heron  26086  quad2  26087  quad  26088  dcubic2  26092  dcubic  26094  mcubic  26095  cubic2  26096  cubic  26097  dquartlem1  26099  dquartlem2  26100  dquart  26101  quart1cl  26102  quart1lem  26103  quart1  26104  quartlem1  26105  quartlem2  26106  quartlem4  26108  quart  26109  log2cnv  26192  log2tlbnd  26193  log2ublem3  26196  log2ub  26197  bclbnd  26526  bposlem8  26537  bposlem9  26538  2lgslem3a  26642  2lgslem3b  26643  2lgslem3c  26644  2lgslem3d  26645  2lgsoddprmlem2  26655  2lgsoddprmlem3c  26658  2lgsoddprmlem3d  26659  addsqnreup  26689  addsq2nreurex  26690  pntibndlem2  26837  pntlemb  26843  ex-opab  28997  ex-exp  29015  ex-fac  29016  ex-bc  29017  ex-ind-dvds  29026  4ipval2  29271  ipidsq  29273  dipcl  29275  dipcj  29277  dip0r  29280  dipcn  29283  ip1ilem  29389  ipasslem10  29402  minvecolem2  29438  minvecolem7  29446  normpar2i  29719  polid2i  29720  lnopeq0i  30570  fib5  32585  fib6  32586  hgt750lemd  32841  hgt750lem  32844  hgt750lem2  32845  quad3  33840  60gcd7e1  40260  420lcm8e840  40266  lcmineqlem23  40306  3exp7  40308  3lexlogpow5ineq1  40309  3lexlogpow2ineq2  40314  aks4d1p1p4  40326  aks4d1p1p7  40329  aks4d1p1p5  40330  aks4d1p1  40331  235t711  40569  flt4lem5e  40743  inductionexd  42075  lhe4.4ex1a  42257  limclner  43517  stoweidlem13  43879  wallispi2lem1  43937  wallispi2lem2  43938  stirlinglem3  43942  stirlinglem10  43949  stirlinglem12  43951  sqwvfourb  44095  fouriersw  44097  fmtnorec4  45341  fmtno5lem4  45348  257prm  45353  fmtnofac1  45362  fmtno4prmfac  45364  fmtno5faclem1  45371  fmtno5faclem2  45372  139prmALT  45388  mod42tp1mod8  45394  3exp4mod41  45408  41prothprmlem1  45409  41prothprmlem2  45410  41prothprm  45411  quad1  45412  8even  45505  2exp340mod341  45525  8exp8mod9  45528  mogoldbb  45577  nnsum4primeseven  45592  nnsum4primesevenALTV  45593  bgoldbtbndlem2  45598  zlmodzxzequap  46180  itsclc0yqsollem1  46448  itscnhlinecirc02plem1  46468  5m4e1  46841