Theorem 4cn 12228

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 12208	. 2 ⊢ 4 = (3 + 1)
2		3cn 12224	. . 3 ⊢ 3 ∈ ℂ
3		ax-1cn 11082	. . 3 ⊢ 1 ∈ ℂ
4	2, 3	addcli 11136	. 2 ⊢ (3 + 1) ∈ ℂ
5	1, 4	eqeltri 2830	1 ⊢ 4 ∈ ℂ

Syntax hints:   ∈ wcel 2113  (class class class)co 7356  ℂcc 11022  1c1 11025   + caddc 11027  3c3 12199  4c4 12200

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 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2706  ax-1cn 11082  ax-addcl 11084

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2726  df-clel 2809  df-2 12206  df-3 12207  df-4 12208

This theorem is referenced by:  5cn  12231  5m1e4  12268  4p2e6  12291  4p3e7  12292  4p4e8  12293  4t2e8  12306  4div2e2  12308  8th4div3  12359  div4p1lem1div2  12394  5p5e10  12676  4t4e16  12704  6t5e30  12712  fldiv4p1lem1div2  13753  sq4e2t8  14120  discr  14161  sqoddm1div8  14164  4bc2eq6  14250  bpoly3  15979  bpoly4  15980  cos2bnd  16111  flodddiv4  16340  6gcd4e2  16463  6lcm4e12  16541  pythagtriplem1  16742  2exp11  17015  13prm  17041  43prm  17047  163prm  17050  317prm  17051  631prm  17052  1259lem1  17056  1259lem2  17057  1259lem3  17058  1259lem4  17059  1259lem5  17060  1259prm  17061  2503lem1  17062  2503lem2  17063  2503lem3  17064  2503prm  17065  4001lem1  17066  4001lem2  17067  4001lem3  17068  4001lem4  17069  4001prm  17070  cphipval2  25195  4cphipval2  25196  minveclem2  25380  minveclem3  25383  minveclem7  25389  uniioombl  25544  dveflem  25937  sincosq4sgn  26464  tan4thpi  26477  sincos6thpi  26479  ang180lem2  26774  heron  26802  quad2  26803  quad  26804  dcubic2  26808  dcubic  26810  mcubic  26811  cubic2  26812  cubic  26813  dquartlem1  26815  dquartlem2  26816  dquart  26817  quart1cl  26818  quart1lem  26819  quart1  26820  quartlem1  26821  quartlem2  26822  quartlem4  26824  quart  26825  log2cnv  26908  log2tlbnd  26909  log2ublem3  26912  log2ub  26913  bclbnd  27245  bposlem8  27256  bposlem9  27257  2lgslem3a  27361  2lgslem3b  27362  2lgslem3c  27363  2lgslem3d  27364  2lgsoddprmlem2  27374  2lgsoddprmlem3c  27377  2lgsoddprmlem3d  27378  addsqnreup  27408  addsq2nreurex  27409  pntibndlem2  27556  pntlemb  27562  ex-opab  30456  ex-exp  30474  ex-fac  30475  ex-bc  30476  ex-ind-dvds  30485  4ipval2  30732  ipidsq  30734  dipcl  30736  dipcj  30738  dip0r  30741  dipcn  30744  ip1ilem  30850  ipasslem10  30863  minvecolem2  30899  minvecolem7  30907  normpar2i  31180  polid2i  31181  lnopeq0i  32031  quad3d  32778  constrresqrtcl  33883  cos9thpiminplylem1  33888  fib5  34511  fib6  34512  hgt750lemd  34754  hgt750lem  34757  hgt750lem2  34758  quad3  35813  60gcd7e1  42198  420lcm8e840  42204  lcmineqlem23  42244  3exp7  42246  3lexlogpow5ineq1  42247  3lexlogpow2ineq2  42252  aks4d1p1p4  42264  aks4d1p1p7  42267  aks4d1p1p5  42268  aks4d1p1  42269  4t5e20  42488  sq4  42490  235t711  42502  flt4lem5e  42841  inductionexd  44338  lhe4.4ex1a  44512  limclner  45837  stoweidlem13  46199  wallispi2lem1  46257  wallispi2lem2  46258  stirlinglem3  46262  stirlinglem10  46269  stirlinglem12  46271  sqwvfourb  46415  fouriersw  46417  sinnpoly  47079  ceil5half3  47528  modm1p1ne  47558  fmtnorec4  47737  fmtno5lem4  47744  257prm  47749  fmtnofac1  47758  fmtno4prmfac  47760  fmtno5faclem1  47767  fmtno5faclem2  47768  139prmALT  47784  mod42tp1mod8  47790  3exp4mod41  47804  41prothprmlem1  47805  41prothprmlem2  47806  41prothprm  47807  quad1  47808  8even  47901  2exp340mod341  47921  8exp8mod9  47924  mogoldbb  47973  nnsum4primeseven  47988  nnsum4primesevenALTV  47989  bgoldbtbndlem2  47994  zlmodzxzequap  48687  itsclc0yqsollem1  48950  itscnhlinecirc02plem1  48970  5m4e1  49984