Theorem 4cn 12201

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 12181	. 2 ⊢ 4 = (3 + 1)
2		3cn 12197	. . 3 ⊢ 3 ∈ ℂ
3		ax-1cn 11055	. . 3 ⊢ 1 ∈ ℂ
4	2, 3	addcli 11109	. 2 ⊢ (3 + 1) ∈ ℂ
5	1, 4	eqeltri 2824	1 ⊢ 4 ∈ ℂ

Syntax hints:   ∈ wcel 2109  (class class class)co 7340  ℂcc 10995  1c1 10998   + caddc 11000  3c3 12172  4c4 12173

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 11055  ax-addcl 11057

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2721  df-clel 2803  df-2 12179  df-3 12180  df-4 12181

This theorem is referenced by:  5cn  12204  5m1e4  12241  4p2e6  12264  4p3e7  12265  4p4e8  12266  4t2e8  12279  4d2e2  12281  8th4div3  12332  div4p1lem1div2  12367  5p5e10  12650  4t4e16  12678  6t5e30  12686  fldiv4p1lem1div2  13727  sq4e2t8  14094  discr  14135  sqoddm1div8  14138  4bc2eq6  14224  bpoly3  15952  bpoly4  15953  cos2bnd  16084  flodddiv4  16313  6gcd4e2  16436  6lcm4e12  16514  pythagtriplem1  16715  2exp11  16988  13prm  17014  43prm  17020  163prm  17023  317prm  17024  631prm  17025  1259lem1  17029  1259lem2  17030  1259lem3  17031  1259lem4  17032  1259lem5  17033  1259prm  17034  2503lem1  17035  2503lem2  17036  2503lem3  17037  2503prm  17038  4001lem1  17039  4001lem2  17040  4001lem3  17041  4001lem4  17042  4001prm  17043  cphipval2  25122  4cphipval2  25123  minveclem2  25307  minveclem3  25310  minveclem7  25316  uniioombl  25471  dveflem  25864  sincosq4sgn  26391  tan4thpi  26404  sincos6thpi  26406  ang180lem2  26701  heron  26729  quad2  26730  quad  26731  dcubic2  26735  dcubic  26737  mcubic  26738  cubic2  26739  cubic  26740  dquartlem1  26742  dquartlem2  26743  dquart  26744  quart1cl  26745  quart1lem  26746  quart1  26747  quartlem1  26748  quartlem2  26749  quartlem4  26751  quart  26752  log2cnv  26835  log2tlbnd  26836  log2ublem3  26839  log2ub  26840  bclbnd  27172  bposlem8  27183  bposlem9  27184  2lgslem3a  27288  2lgslem3b  27289  2lgslem3c  27290  2lgslem3d  27291  2lgsoddprmlem2  27301  2lgsoddprmlem3c  27304  2lgsoddprmlem3d  27305  addsqnreup  27335  addsq2nreurex  27336  pntibndlem2  27483  pntlemb  27489  ex-opab  30363  ex-exp  30381  ex-fac  30382  ex-bc  30383  ex-ind-dvds  30392  4ipval2  30639  ipidsq  30641  dipcl  30643  dipcj  30645  dip0r  30648  dipcn  30651  ip1ilem  30757  ipasslem10  30770  minvecolem2  30806  minvecolem7  30814  normpar2i  31087  polid2i  31088  lnopeq0i  31938  quad3d  32685  constrresqrtcl  33758  cos9thpiminplylem1  33763  fib5  34386  fib6  34387  hgt750lemd  34629  hgt750lem  34632  hgt750lem2  34633  quad3  35660  60gcd7e1  41995  420lcm8e840  42001  lcmineqlem23  42041  3exp7  42043  3lexlogpow5ineq1  42044  3lexlogpow2ineq2  42049  aks4d1p1p4  42061  aks4d1p1p7  42064  aks4d1p1p5  42065  aks4d1p1  42066  4t5e20  42281  sq4  42283  235t711  42295  flt4lem5e  42646  inductionexd  44145  lhe4.4ex1a  44319  limclner  45646  stoweidlem13  46008  wallispi2lem1  46066  wallispi2lem2  46067  stirlinglem3  46071  stirlinglem10  46078  stirlinglem12  46080  sqwvfourb  46224  fouriersw  46226  sinnpoly  46889  ceil5half3  47338  modm1p1ne  47368  fmtnorec4  47547  fmtno5lem4  47554  257prm  47559  fmtnofac1  47568  fmtno4prmfac  47570  fmtno5faclem1  47577  fmtno5faclem2  47578  139prmALT  47594  mod42tp1mod8  47600  3exp4mod41  47614  41prothprmlem1  47615  41prothprmlem2  47616  41prothprm  47617  quad1  47618  8even  47711  2exp340mod341  47731  8exp8mod9  47734  mogoldbb  47783  nnsum4primeseven  47798  nnsum4primesevenALTV  47799  bgoldbtbndlem2  47804  zlmodzxzequap  48498  itsclc0yqsollem1  48761  itscnhlinecirc02plem1  48781  5m4e1  49796