Theorem 4cn 12330

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 12310	. 2 ⊢ 4 = (3 + 1)
2		3cn 12326	. . 3 ⊢ 3 ∈ ℂ
3		ax-1cn 11192	. . 3 ⊢ 1 ∈ ℂ
4	2, 3	addcli 11246	. 2 ⊢ (3 + 1) ∈ ℂ
5	1, 4	eqeltri 2831	1 ⊢ 4 ∈ ℂ

Syntax hints:   ∈ wcel 2109  (class class class)co 7410  ℂcc 11132  1c1 11135   + caddc 11137  3c3 12301  4c4 12302

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 2708  ax-1cn 11192  ax-addcl 11194

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2728  df-clel 2810  df-2 12308  df-3 12309  df-4 12310

This theorem is referenced by:  5cn  12333  5m1e4  12375  4p2e6  12398  4p3e7  12399  4p4e8  12400  4t2e8  12413  4d2e2  12415  8th4div3  12466  div4p1lem1div2  12501  5p5e10  12784  4t4e16  12812  6t5e30  12820  fldiv4p1lem1div2  13857  sq4e2t8  14222  discr  14263  sqoddm1div8  14266  4bc2eq6  14352  bpoly3  16079  bpoly4  16080  cos2bnd  16211  flodddiv4  16439  6gcd4e2  16562  6lcm4e12  16640  pythagtriplem1  16841  2exp11  17114  13prm  17140  43prm  17146  163prm  17149  317prm  17150  631prm  17151  1259lem1  17155  1259lem2  17156  1259lem3  17157  1259lem4  17158  1259lem5  17159  1259prm  17160  2503lem1  17161  2503lem2  17162  2503lem3  17163  2503prm  17164  4001lem1  17165  4001lem2  17166  4001lem3  17167  4001lem4  17168  4001prm  17169  cphipval2  25198  4cphipval2  25199  minveclem2  25383  minveclem3  25386  minveclem7  25392  uniioombl  25547  dveflem  25940  sincosq4sgn  26467  tan4thpi  26480  sincos6thpi  26482  ang180lem2  26777  heron  26805  quad2  26806  quad  26807  dcubic2  26811  dcubic  26813  mcubic  26814  cubic2  26815  cubic  26816  dquartlem1  26818  dquartlem2  26819  dquart  26820  quart1cl  26821  quart1lem  26822  quart1  26823  quartlem1  26824  quartlem2  26825  quartlem4  26827  quart  26828  log2cnv  26911  log2tlbnd  26912  log2ublem3  26915  log2ub  26916  bclbnd  27248  bposlem8  27259  bposlem9  27260  2lgslem3a  27364  2lgslem3b  27365  2lgslem3c  27366  2lgslem3d  27367  2lgsoddprmlem2  27377  2lgsoddprmlem3c  27380  2lgsoddprmlem3d  27381  addsqnreup  27411  addsq2nreurex  27412  pntibndlem2  27559  pntlemb  27565  ex-opab  30418  ex-exp  30436  ex-fac  30437  ex-bc  30438  ex-ind-dvds  30447  4ipval2  30694  ipidsq  30696  dipcl  30698  dipcj  30700  dip0r  30703  dipcn  30706  ip1ilem  30812  ipasslem10  30825  minvecolem2  30861  minvecolem7  30869  normpar2i  31142  polid2i  31143  lnopeq0i  31993  quad3d  32732  constrresqrtcl  33816  cos9thpiminplylem1  33821  fib5  34442  fib6  34443  hgt750lemd  34685  hgt750lem  34688  hgt750lem2  34689  quad3  35697  60gcd7e1  42023  420lcm8e840  42029  lcmineqlem23  42069  3exp7  42071  3lexlogpow5ineq1  42072  3lexlogpow2ineq2  42077  aks4d1p1p4  42089  aks4d1p1p7  42092  aks4d1p1p5  42093  aks4d1p1  42094  4t5e20  42309  sq4  42311  235t711  42323  flt4lem5e  42654  inductionexd  44154  lhe4.4ex1a  44328  limclner  45660  stoweidlem13  46022  wallispi2lem1  46080  wallispi2lem2  46081  stirlinglem3  46085  stirlinglem10  46092  stirlinglem12  46094  sqwvfourb  46238  fouriersw  46240  ceil5half3  47349  fmtnorec4  47543  fmtno5lem4  47550  257prm  47555  fmtnofac1  47564  fmtno4prmfac  47566  fmtno5faclem1  47573  fmtno5faclem2  47574  139prmALT  47590  mod42tp1mod8  47596  3exp4mod41  47610  41prothprmlem1  47611  41prothprmlem2  47612  41prothprm  47613  quad1  47614  8even  47707  2exp340mod341  47727  8exp8mod9  47730  mogoldbb  47779  nnsum4primeseven  47794  nnsum4primesevenALTV  47795  bgoldbtbndlem2  47800  zlmodzxzequap  48455  itsclc0yqsollem1  48722  itscnhlinecirc02plem1  48742  5m4e1  49641