Theorem 4cn 12428

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 12407	. 2 ⊢ 4 = (3 + 1)
2		3cn 12424	. . 3 ⊢ 3 ∈ ℂ
3		ax-1cn 11258	. . 3 ⊢ 1 ∈ ℂ
4	2, 3	addcli 11315	. 2 ⊢ (3 + 1) ∈ ℂ
5	1, 4	eqeltri 2857	1 ⊢ 4 ∈ ℂ

This proof depends on syntax axioms:   ∈ wcel 2145  (class class class)co 7420  ℂcc 11198  1c1 11201   + caddc 11203  3c3 12398  4c4 12399

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733  ax-1cn 11258  ax-addcl 11260

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2753  df-clel 2836  df-2 12405  df-3 12406  df-4 12407

This theorem is used by:  5cn  12431  5m1e4  12472  4p2e6  12495  4p3e7  12496  4p4e8  12497  4t2e8  12511  2t4e8  12512  4div2e2  12514  8th4div3  12566  div4p1lem1div2  12601  5p5e10  12890  4t4e16  12918  6t5e30  12926  fldiv4p1lem1div2  13975  sq4e2t8  14342  discr  14384  sqoddm1div8  14387  4bc2eq6  14473  bpoly3  16224  bpoly4  16225  cos2bnd  16356  flodddiv4  16585  6gcd4e2  16711  6lcm4e12  16791  pythagtriplem1  16994  2exp11  17267  13prm  17294  43prm  17300  83prm  17301  163prm  17303  317prm  17304  631prm  17305  1259lem1  17309  1259lem2  17310  1259lem3  17311  1259lem4  17312  1259lem5  17313  1259prm  17314  2503lem1  17315  2503lem2  17316  2503lem3  17317  2503prm  17318  4001lem1  17319  4001lem2  17320  4001lem3  17321  4001lem4  17322  4001prm  17323  cphipval2  25562  4cphipval2  25563  minveclem2  25747  minveclem3  25750  minveclem7  25756  uniioombl  25910  dveflem  26299  sincosq4sgn  26830  tan4thpi  26843  sincos6thpi  26844  ang180lem2  27138  heron  27166  quad2  27167  quad  27168  dcubic2  27172  dcubic  27174  mcubic  27175  cubic2  27176  cubic  27177  dquartlem1  27179  dquartlem2  27180  dquart  27181  quart1cl  27182  quart1lem  27183  quart1  27184  quartlem1  27185  quartlem2  27186  quartlem4  27188  quart  27189  log2cnv  27272  log2tlbnd  27273  log2ublem3  27276  log2ub  27277  bclbnd  27607  bposlem8  27618  bposlem9  27619  2lgslem3a  27723  2lgslem3b  27724  2lgslem3c  27725  2lgslem3d  27726  2lgsoddprmlem2  27736  2lgsoddprmlem3c  27739  2lgsoddprmlem3d  27740  addsqnreup  27770  addsq2nreurex  27771  pntibndlem2  27918  pntlemb  27924  flt4lem5e  27986  ex-opab  31033  ex-exp  31051  ex-fac  31052  ex-bc  31053  ex-ind-dvds  31062  4ipval2  31310  ipidsq  31312  dipcl  31314  dipcj  31316  dip0r  31319  dipcn  31322  ip1ilem  31428  ipasslem10  31441  minvecolem2  31477  minvecolem7  31485  normpar2i  31758  polid2i  31759  lnopeq0i  32609  quad3d  33341  constrresqrtcl  34409  cos9thpiminplylem1  34414  fib5  35037  fib6  35038  hgt750lemd  35277  hgt750lem  35280  hgt750lem2  35281  quad3  36435  60gcd7e1  43055  420lcm8e840  43061  lcmineqlem23  43101  3exp7  43103  3lexlogpow5ineq1  43104  3lexlogpow2ineq2  43109  aks4d1p1p4  43121  aks4d1p1p7  43124  aks4d1p1p5  43125  aks4d1p1  43126  25or6to4  43256  4p4e8ALT  43309  1p5e6  43312  2p6e8  43319  4p5e9  43324  4t5e20  43348  sq4  43350  235t711  43362  inductionexd  45154  lhe4.4ex1a  45312  limclner  46660  stoweidlem13  47022  wallispi2lem1  47080  wallispi2lem2  47081  stirlinglem3  47085  stirlinglem10  47092  stirlinglem12  47094  sqwvfourb  47238  fouriersw  47240  sin5tlem1  47918  sin5tlem2  47919  sin5tlem3  47920  sin5tlem4  47921  cos5t  47924  goldpolyfactor  47926  goldratmolem2  47932  goldratval  47935  sinnpoly  47940  ceil5half3  48415  modm1p1ne  48445  fmtnorec4  48633  fmtno5lem4  48640  257prm  48645  fmtnofac1  48654  fmtno4prmfac  48656  fmtno5faclem1  48663  fmtno5faclem2  48664  139prmALT  48680  mod42tp1mod8  48686  3exp4mod41  48700  41prothprmlem1  48701  41prothprmlem2  48702  41prothprm  48703  ppivalnn4  48711  quad1  48717  8even  48810  2exp340mod341  48830  mogoldbb  48882  nnsum4primeseven  48897  nnsum4primesevenALTV  48898  bgoldbtbndlem2  48903  zlmodzxzequap  49610  itsclc0yqsollem1  49873  itscnhlinecirc02plem1  49893  5m4e1  50934