Theorem 4cn 12257

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 12237	. 2 ⊢ 4 = (3 + 1)
2		3cn 12253	. . 3 ⊢ 3 ∈ ℂ
3		ax-1cn 11087	. . 3 ⊢ 1 ∈ ℂ
4	2, 3	addcli 11142	. 2 ⊢ (3 + 1) ∈ ℂ
5	1, 4	eqeltri 2835	1 ⊢ 4 ∈ ℂ

Syntax hints:   ∈ wcel 2119  (class class class)co 7356  ℂcc 11027  1c1 11030   + caddc 11032  3c3 12228  4c4 12229

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711  ax-1cn 11087  ax-addcl 11089

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-cleq 2731  df-clel 2814  df-2 12235  df-3 12236  df-4 12237

This theorem is referenced by:  5cn  12260  5m1e4  12297  4p2e6  12320  4p3e7  12321  4p4e8  12322  4t2e8  12335  4div2e2  12337  8th4div3  12388  div4p1lem1div2  12423  5p5e10  12706  4t4e16  12734  6t5e30  12742  fldiv4p1lem1div2  13785  sq4e2t8  14152  discr  14193  sqoddm1div8  14196  4bc2eq6  14282  bpoly3  16014  bpoly4  16015  cos2bnd  16146  flodddiv4  16375  6gcd4e2  16498  6lcm4e12  16576  pythagtriplem1  16778  2exp11  17051  13prm  17077  43prm  17083  163prm  17086  317prm  17087  631prm  17088  1259lem1  17092  1259lem2  17093  1259lem3  17094  1259lem4  17095  1259lem5  17096  1259prm  17097  2503lem1  17098  2503lem2  17099  2503lem3  17100  2503prm  17101  4001lem1  17102  4001lem2  17103  4001lem3  17104  4001lem4  17105  4001prm  17106  cphipval2  25226  4cphipval2  25227  minveclem2  25411  minveclem3  25414  minveclem7  25420  uniioombl  25574  dveflem  25964  sincosq4sgn  26483  tan4thpi  26496  sincos6thpi  26498  ang180lem2  26792  heron  26820  quad2  26821  quad  26822  dcubic2  26826  dcubic  26828  mcubic  26829  cubic2  26830  cubic  26831  dquartlem1  26833  dquartlem2  26834  dquart  26835  quart1cl  26836  quart1lem  26837  quart1  26838  quartlem1  26839  quartlem2  26840  quartlem4  26842  quart  26843  log2cnv  26926  log2tlbnd  26927  log2ublem3  26930  log2ub  26931  bclbnd  27261  bposlem8  27272  bposlem9  27273  2lgslem3a  27377  2lgslem3b  27378  2lgslem3c  27379  2lgslem3d  27380  2lgsoddprmlem2  27390  2lgsoddprmlem3c  27393  2lgsoddprmlem3d  27394  addsqnreup  27424  addsq2nreurex  27425  pntibndlem2  27572  pntlemb  27578  ex-opab  30520  ex-exp  30538  ex-fac  30539  ex-bc  30540  ex-ind-dvds  30549  4ipval2  30797  ipidsq  30799  dipcl  30801  dipcj  30803  dip0r  30806  dipcn  30809  ip1ilem  30915  ipasslem10  30928  minvecolem2  30964  minvecolem7  30972  normpar2i  31245  polid2i  31246  lnopeq0i  32096  quad3d  32841  constrresqrtcl  33961  cos9thpiminplylem1  33966  fib5  34589  fib6  34590  hgt750lemd  34832  hgt750lem  34835  hgt750lem2  34836  quad3  35898  60gcd7e1  42490  420lcm8e840  42496  lcmineqlem23  42536  3exp7  42538  3lexlogpow5ineq1  42539  3lexlogpow2ineq2  42544  aks4d1p1p4  42556  aks4d1p1p7  42559  aks4d1p1p5  42560  aks4d1p1  42561  4t5e20  42768  sq4  42770  235t711  42782  flt4lem5e  43106  inductionexd  44599  lhe4.4ex1a  44773  limclner  46094  stoweidlem13  46456  wallispi2lem1  46514  wallispi2lem2  46515  stirlinglem3  46519  stirlinglem10  46526  stirlinglem12  46528  sqwvfourb  46672  fouriersw  46674  sin5tlem1  47336  sin5tlem2  47337  sin5tlem3  47338  sin5tlem4  47339  cos5t  47342  goldratmolem2  47349  sinnpoly  47354  ceil5half3  47809  modm1p1ne  47839  fmtnorec4  48027  fmtno5lem4  48034  257prm  48039  fmtnofac1  48048  fmtno4prmfac  48050  fmtno5faclem1  48057  fmtno5faclem2  48058  139prmALT  48074  mod42tp1mod8  48080  3exp4mod41  48094  41prothprmlem1  48095  41prothprmlem2  48096  41prothprm  48097  ppivalnn4  48105  quad1  48111  8even  48204  2exp340mod341  48224  8exp8mod9  48227  mogoldbb  48276  nnsum4primeseven  48291  nnsum4primesevenALTV  48292  bgoldbtbndlem2  48297  zlmodzxzequap  48990  itsclc0yqsollem1  49253  itscnhlinecirc02plem1  49273  5m4e1  50287