Theorem 4cn 11988

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 11968	. 2 ⊢ 4 = (3 + 1)
2		3cn 11984	. . 3 ⊢ 3 ∈ ℂ
3		ax-1cn 10860	. . 3 ⊢ 1 ∈ ℂ
4	2, 3	addcli 10912	. 2 ⊢ (3 + 1) ∈ ℂ
5	1, 4	eqeltri 2835	1 ⊢ 4 ∈ ℂ

Syntax hints:   ∈ wcel 2108  (class class class)co 7255  ℂcc 10800  1c1 10803   + caddc 10805  3c3 11959  4c4 11960

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709  ax-1cn 10860  ax-addcl 10862

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1784  df-cleq 2730  df-clel 2817  df-2 11966  df-3 11967  df-4 11968

This theorem is referenced by:  5cn  11991  5m1e4  12033  4p2e6  12056  4p3e7  12057  4p4e8  12058  4t2e8  12071  4d2e2  12073  8th4div3  12123  div4p1lem1div2  12158  5p5e10  12437  4t4e16  12465  6t5e30  12473  fldiv4p1lem1div2  13483  sq4e2t8  13844  discr  13883  sqoddm1div8  13886  4bc2eq6  13971  bpoly3  15696  bpoly4  15697  cos2bnd  15825  flodddiv4  16050  6gcd4e2  16174  6lcm4e12  16249  pythagtriplem1  16445  2exp11  16719  13prm  16745  43prm  16751  163prm  16754  317prm  16755  631prm  16756  1259lem1  16760  1259lem2  16761  1259lem3  16762  1259lem4  16763  1259lem5  16764  1259prm  16765  2503lem1  16766  2503lem2  16767  2503lem3  16768  2503prm  16769  4001lem1  16770  4001lem2  16771  4001lem3  16772  4001lem4  16773  4001prm  16774  cphipval2  24310  4cphipval2  24311  minveclem2  24495  minveclem3  24498  minveclem7  24504  uniioombl  24658  dveflem  25048  sincosq4sgn  25563  sincos6thpi  25577  ang180lem2  25865  heron  25893  quad2  25894  quad  25895  dcubic2  25899  dcubic  25901  mcubic  25902  cubic2  25903  cubic  25904  dquartlem1  25906  dquartlem2  25907  dquart  25908  quart1cl  25909  quart1lem  25910  quart1  25911  quartlem1  25912  quartlem2  25913  quartlem4  25915  quart  25916  log2cnv  25999  log2tlbnd  26000  log2ublem3  26003  log2ub  26004  bclbnd  26333  bposlem8  26344  bposlem9  26345  2lgslem3a  26449  2lgslem3b  26450  2lgslem3c  26451  2lgslem3d  26452  2lgsoddprmlem2  26462  2lgsoddprmlem3c  26465  2lgsoddprmlem3d  26466  addsqnreup  26496  addsq2nreurex  26497  pntibndlem2  26644  pntlemb  26650  ex-opab  28697  ex-exp  28715  ex-fac  28716  ex-bc  28717  ex-ind-dvds  28726  4ipval2  28971  ipidsq  28973  dipcl  28975  dipcj  28977  dip0r  28980  dipcn  28983  ip1ilem  29089  ipasslem10  29102  minvecolem2  29138  minvecolem7  29146  normpar2i  29419  polid2i  29420  lnopeq0i  30270  fib5  32272  fib6  32273  hgt750lemd  32528  hgt750lem  32531  hgt750lem2  32532  quad3  33528  60gcd7e1  39941  420lcm8e840  39947  lcmineqlem23  39987  3exp7  39989  3lexlogpow5ineq1  39990  3lexlogpow2ineq2  39995  aks4d1p1p4  40007  aks4d1p1p7  40010  aks4d1p1p5  40011  aks4d1p1  40012  235t711  40240  flt4lem5e  40409  inductionexd  41654  lhe4.4ex1a  41836  limclner  43082  stoweidlem13  43444  wallispi2lem1  43502  wallispi2lem2  43503  stirlinglem3  43507  stirlinglem10  43514  stirlinglem12  43516  sqwvfourb  43660  fouriersw  43662  fmtnorec4  44889  fmtno5lem4  44896  257prm  44901  fmtnofac1  44910  fmtno4prmfac  44912  fmtno5faclem1  44919  fmtno5faclem2  44920  139prmALT  44936  mod42tp1mod8  44942  3exp4mod41  44956  41prothprmlem1  44957  41prothprmlem2  44958  41prothprm  44959  quad1  44960  8even  45053  2exp340mod341  45073  8exp8mod9  45076  mogoldbb  45125  nnsum4primeseven  45140  nnsum4primesevenALTV  45141  bgoldbtbndlem2  45146  zlmodzxzequap  45728  itsclc0yqsollem1  45996  itscnhlinecirc02plem1  46016  5m4e1  46387