Theorem 4cn 12271

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 12251	. 2 ⊢ 4 = (3 + 1)
2		3cn 12267	. . 3 ⊢ 3 ∈ ℂ
3		ax-1cn 11126	. . 3 ⊢ 1 ∈ ℂ
4	2, 3	addcli 11180	. 2 ⊢ (3 + 1) ∈ ℂ
5	1, 4	eqeltri 2824	1 ⊢ 4 ∈ ℂ

Syntax hints:   ∈ wcel 2109  (class class class)co 7387  ℂcc 11066  1c1 11069   + caddc 11071  3c3 12242  4c4 12243

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 11126  ax-addcl 11128

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2721  df-clel 2803  df-2 12249  df-3 12250  df-4 12251

This theorem is referenced by:  5cn  12274  5m1e4  12311  4p2e6  12334  4p3e7  12335  4p4e8  12336  4t2e8  12349  4d2e2  12351  8th4div3  12402  div4p1lem1div2  12437  5p5e10  12720  4t4e16  12748  6t5e30  12756  fldiv4p1lem1div2  13797  sq4e2t8  14164  discr  14205  sqoddm1div8  14208  4bc2eq6  14294  bpoly3  16024  bpoly4  16025  cos2bnd  16156  flodddiv4  16385  6gcd4e2  16508  6lcm4e12  16586  pythagtriplem1  16787  2exp11  17060  13prm  17086  43prm  17092  163prm  17095  317prm  17096  631prm  17097  1259lem1  17101  1259lem2  17102  1259lem3  17103  1259lem4  17104  1259lem5  17105  1259prm  17106  2503lem1  17107  2503lem2  17108  2503lem3  17109  2503prm  17110  4001lem1  17111  4001lem2  17112  4001lem3  17113  4001lem4  17114  4001prm  17115  cphipval2  25141  4cphipval2  25142  minveclem2  25326  minveclem3  25329  minveclem7  25335  uniioombl  25490  dveflem  25883  sincosq4sgn  26410  tan4thpi  26423  sincos6thpi  26425  ang180lem2  26720  heron  26748  quad2  26749  quad  26750  dcubic2  26754  dcubic  26756  mcubic  26757  cubic2  26758  cubic  26759  dquartlem1  26761  dquartlem2  26762  dquart  26763  quart1cl  26764  quart1lem  26765  quart1  26766  quartlem1  26767  quartlem2  26768  quartlem4  26770  quart  26771  log2cnv  26854  log2tlbnd  26855  log2ublem3  26858  log2ub  26859  bclbnd  27191  bposlem8  27202  bposlem9  27203  2lgslem3a  27307  2lgslem3b  27308  2lgslem3c  27309  2lgslem3d  27310  2lgsoddprmlem2  27320  2lgsoddprmlem3c  27323  2lgsoddprmlem3d  27324  addsqnreup  27354  addsq2nreurex  27355  pntibndlem2  27502  pntlemb  27508  ex-opab  30361  ex-exp  30379  ex-fac  30380  ex-bc  30381  ex-ind-dvds  30390  4ipval2  30637  ipidsq  30639  dipcl  30641  dipcj  30643  dip0r  30646  dipcn  30649  ip1ilem  30755  ipasslem10  30768  minvecolem2  30804  minvecolem7  30812  normpar2i  31085  polid2i  31086  lnopeq0i  31936  quad3d  32673  constrresqrtcl  33767  cos9thpiminplylem1  33772  fib5  34396  fib6  34397  hgt750lemd  34639  hgt750lem  34642  hgt750lem2  34643  quad3  35657  60gcd7e1  41993  420lcm8e840  41999  lcmineqlem23  42039  3exp7  42041  3lexlogpow5ineq1  42042  3lexlogpow2ineq2  42047  aks4d1p1p4  42059  aks4d1p1p7  42062  aks4d1p1p5  42063  aks4d1p1  42064  4t5e20  42279  sq4  42281  235t711  42293  flt4lem5e  42644  inductionexd  44144  lhe4.4ex1a  44318  limclner  45649  stoweidlem13  46011  wallispi2lem1  46069  wallispi2lem2  46070  stirlinglem3  46074  stirlinglem10  46081  stirlinglem12  46083  sqwvfourb  46227  fouriersw  46229  sinnpoly  46892  ceil5half3  47341  modm1p1ne  47371  fmtnorec4  47550  fmtno5lem4  47557  257prm  47562  fmtnofac1  47571  fmtno4prmfac  47573  fmtno5faclem1  47580  fmtno5faclem2  47581  139prmALT  47597  mod42tp1mod8  47603  3exp4mod41  47617  41prothprmlem1  47618  41prothprmlem2  47619  41prothprm  47620  quad1  47621  8even  47714  2exp340mod341  47734  8exp8mod9  47737  mogoldbb  47786  nnsum4primeseven  47801  nnsum4primesevenALTV  47802  bgoldbtbndlem2  47807  zlmodzxzequap  48488  itsclc0yqsollem1  48751  itscnhlinecirc02plem1  48771  5m4e1  49786