Theorem 4cn 11721

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 11701	. 2 ⊢ 4 = (3 + 1)
2		3cn 11717	. . 3 ⊢ 3 ∈ ℂ
3		ax-1cn 10594	. . 3 ⊢ 1 ∈ ℂ
4	2, 3	addcli 10646	. 2 ⊢ (3 + 1) ∈ ℂ
5	1, 4	eqeltri 2909	1 ⊢ 4 ∈ ℂ

Syntax hints:   ∈ wcel 2110  (class class class)co 7155  ℂcc 10534  1c1 10537   + caddc 10539  3c3 11692  4c4 11693

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-ext 2793  ax-1cn 10594  ax-addcl 10596

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1777  df-cleq 2814  df-clel 2893  df-2 11699  df-3 11700  df-4 11701

This theorem is referenced by:  5cn  11724  5m1e4  11766  4p2e6  11789  4p3e7  11790  4p4e8  11791  4t2e8  11804  4d2e2  11806  8th4div3  11856  div4p1lem1div2  11891  5p5e10  12168  4t4e16  12196  6t5e30  12204  fldiv4p1lem1div2  13204  sq4e2t8  13561  discr  13600  sqoddm1div8  13603  4bc2eq6  13688  bpoly3  15411  bpoly4  15412  cos2bnd  15540  flodddiv4  15763  6gcd4e2  15885  6lcm4e12  15959  pythagtriplem1  16152  13prm  16448  43prm  16454  163prm  16457  317prm  16458  631prm  16459  1259lem1  16463  1259lem2  16464  1259lem3  16465  1259lem4  16466  1259lem5  16467  1259prm  16468  2503lem1  16469  2503lem2  16470  2503lem3  16471  2503prm  16472  4001lem1  16473  4001lem2  16474  4001lem3  16475  4001lem4  16476  4001prm  16477  cphipval2  23843  4cphipval2  23844  minveclem2  24028  minveclem3  24031  minveclem7  24037  uniioombl  24189  dveflem  24575  sincosq4sgn  25086  sincos6thpi  25100  ang180lem2  25387  heron  25415  quad2  25416  quad  25417  dcubic2  25421  dcubic  25423  mcubic  25424  cubic2  25425  cubic  25426  dquartlem1  25428  dquartlem2  25429  dquart  25430  quart1cl  25431  quart1lem  25432  quart1  25433  quartlem1  25434  quartlem2  25435  quartlem4  25437  quart  25438  log2cnv  25521  log2tlbnd  25522  log2ublem3  25525  log2ub  25526  bclbnd  25855  bposlem8  25866  bposlem9  25867  2lgslem3a  25971  2lgslem3b  25972  2lgslem3c  25973  2lgslem3d  25974  2lgsoddprmlem2  25984  2lgsoddprmlem3c  25987  2lgsoddprmlem3d  25988  addsqnreup  26018  addsq2nreurex  26019  pntibndlem2  26166  pntlemb  26172  ex-opab  28210  ex-exp  28228  ex-fac  28229  ex-bc  28230  ex-ind-dvds  28239  4ipval2  28484  ipidsq  28486  dipcl  28488  dipcj  28490  dip0r  28493  dipcn  28496  ip1ilem  28602  ipasslem10  28615  minvecolem2  28651  minvecolem7  28659  normpar2i  28932  polid2i  28933  lnopeq0i  29783  fib5  31663  fib6  31664  hgt750lemd  31919  hgt750lem  31922  hgt750lem2  31923  quad3  32913  235t711  39175  inductionexd  40503  lhe4.4ex1a  40659  limclner  41930  stoweidlem13  42297  wallispi2lem1  42355  wallispi2lem2  42356  stirlinglem3  42360  stirlinglem10  42367  stirlinglem12  42369  sqwvfourb  42513  fouriersw  42515  fmtnorec4  43710  fmtno5lem4  43717  257prm  43722  fmtnofac1  43731  fmtno4prmfac  43733  fmtno5faclem1  43740  fmtno5faclem2  43741  139prmALT  43758  2exp11  43764  mod42tp1mod8  43766  3exp4mod41  43780  41prothprmlem1  43781  41prothprmlem2  43782  41prothprm  43783  quad1  43784  8even  43877  2exp340mod341  43897  8exp8mod9  43900  mogoldbb  43949  nnsum4primeseven  43964  nnsum4primesevenALTV  43965  bgoldbtbndlem2  43970  zlmodzxzequap  44553  itsclc0yqsollem1  44748  itscnhlinecirc02plem1  44768  5m4e1  44897