Theorem 4cn 12230

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 12210	. 2 ⊢ 4 = (3 + 1)
2		3cn 12226	. . 3 ⊢ 3 ∈ ℂ
3		ax-1cn 11084	. . 3 ⊢ 1 ∈ ℂ
4	2, 3	addcli 11138	. 2 ⊢ (3 + 1) ∈ ℂ
5	1, 4	eqeltri 2832	1 ⊢ 4 ∈ ℂ

Syntax hints:   ∈ wcel 2113  (class class class)co 7358  ℂcc 11024  1c1 11027   + caddc 11029  3c3 12201  4c4 12202

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 2708  ax-1cn 11084  ax-addcl 11086

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2728  df-clel 2811  df-2 12208  df-3 12209  df-4 12210

This theorem is referenced by:  5cn  12233  5m1e4  12270  4p2e6  12293  4p3e7  12294  4p4e8  12295  4t2e8  12308  4div2e2  12310  8th4div3  12361  div4p1lem1div2  12396  5p5e10  12678  4t4e16  12706  6t5e30  12714  fldiv4p1lem1div2  13755  sq4e2t8  14122  discr  14163  sqoddm1div8  14166  4bc2eq6  14252  bpoly3  15981  bpoly4  15982  cos2bnd  16113  flodddiv4  16342  6gcd4e2  16465  6lcm4e12  16543  pythagtriplem1  16744  2exp11  17017  13prm  17043  43prm  17049  163prm  17052  317prm  17053  631prm  17054  1259lem1  17058  1259lem2  17059  1259lem3  17060  1259lem4  17061  1259lem5  17062  1259prm  17063  2503lem1  17064  2503lem2  17065  2503lem3  17066  2503prm  17067  4001lem1  17068  4001lem2  17069  4001lem3  17070  4001lem4  17071  4001prm  17072  cphipval2  25197  4cphipval2  25198  minveclem2  25382  minveclem3  25385  minveclem7  25391  uniioombl  25546  dveflem  25939  sincosq4sgn  26466  tan4thpi  26479  sincos6thpi  26481  ang180lem2  26776  heron  26804  quad2  26805  quad  26806  dcubic2  26810  dcubic  26812  mcubic  26813  cubic2  26814  cubic  26815  dquartlem1  26817  dquartlem2  26818  dquart  26819  quart1cl  26820  quart1lem  26821  quart1  26822  quartlem1  26823  quartlem2  26824  quartlem4  26826  quart  26827  log2cnv  26910  log2tlbnd  26911  log2ublem3  26914  log2ub  26915  bclbnd  27247  bposlem8  27258  bposlem9  27259  2lgslem3a  27363  2lgslem3b  27364  2lgslem3c  27365  2lgslem3d  27366  2lgsoddprmlem2  27376  2lgsoddprmlem3c  27379  2lgsoddprmlem3d  27380  addsqnreup  27410  addsq2nreurex  27411  pntibndlem2  27558  pntlemb  27564  ex-opab  30507  ex-exp  30525  ex-fac  30526  ex-bc  30527  ex-ind-dvds  30536  4ipval2  30783  ipidsq  30785  dipcl  30787  dipcj  30789  dip0r  30792  dipcn  30795  ip1ilem  30901  ipasslem10  30914  minvecolem2  30950  minvecolem7  30958  normpar2i  31231  polid2i  31232  lnopeq0i  32082  quad3d  32829  constrresqrtcl  33934  cos9thpiminplylem1  33939  fib5  34562  fib6  34563  hgt750lemd  34805  hgt750lem  34808  hgt750lem2  34809  quad3  35864  60gcd7e1  42269  420lcm8e840  42275  lcmineqlem23  42315  3exp7  42317  3lexlogpow5ineq1  42318  3lexlogpow2ineq2  42323  aks4d1p1p4  42335  aks4d1p1p7  42338  aks4d1p1p5  42339  aks4d1p1  42340  4t5e20  42556  sq4  42558  235t711  42570  flt4lem5e  42909  inductionexd  44406  lhe4.4ex1a  44580  limclner  45905  stoweidlem13  46267  wallispi2lem1  46325  wallispi2lem2  46326  stirlinglem3  46330  stirlinglem10  46337  stirlinglem12  46339  sqwvfourb  46483  fouriersw  46485  sinnpoly  47147  ceil5half3  47596  modm1p1ne  47626  fmtnorec4  47805  fmtno5lem4  47812  257prm  47817  fmtnofac1  47826  fmtno4prmfac  47828  fmtno5faclem1  47835  fmtno5faclem2  47836  139prmALT  47852  mod42tp1mod8  47858  3exp4mod41  47872  41prothprmlem1  47873  41prothprmlem2  47874  41prothprm  47875  quad1  47876  8even  47969  2exp340mod341  47989  8exp8mod9  47992  mogoldbb  48041  nnsum4primeseven  48056  nnsum4primesevenALTV  48057  bgoldbtbndlem2  48062  zlmodzxzequap  48755  itsclc0yqsollem1  49018  itscnhlinecirc02plem1  49038  5m4e1  50052