Theorem 4cn 12247

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 12227	. 2 ⊢ 4 = (3 + 1)
2		3cn 12243	. . 3 ⊢ 3 ∈ ℂ
3		ax-1cn 11102	. . 3 ⊢ 1 ∈ ℂ
4	2, 3	addcli 11156	. 2 ⊢ (3 + 1) ∈ ℂ
5	1, 4	eqeltri 2824	1 ⊢ 4 ∈ ℂ

Syntax hints:   ∈ wcel 2109  (class class class)co 7369  ℂcc 11042  1c1 11045   + caddc 11047  3c3 12218  4c4 12219

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 2701  ax-1cn 11102  ax-addcl 11104

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2721  df-clel 2803  df-2 12225  df-3 12226  df-4 12227

This theorem is referenced by:  5cn  12250  5m1e4  12287  4p2e6  12310  4p3e7  12311  4p4e8  12312  4t2e8  12325  4d2e2  12327  8th4div3  12378  div4p1lem1div2  12413  5p5e10  12696  4t4e16  12724  6t5e30  12732  fldiv4p1lem1div2  13773  sq4e2t8  14140  discr  14181  sqoddm1div8  14184  4bc2eq6  14270  bpoly3  16000  bpoly4  16001  cos2bnd  16132  flodddiv4  16361  6gcd4e2  16484  6lcm4e12  16562  pythagtriplem1  16763  2exp11  17036  13prm  17062  43prm  17068  163prm  17071  317prm  17072  631prm  17073  1259lem1  17077  1259lem2  17078  1259lem3  17079  1259lem4  17080  1259lem5  17081  1259prm  17082  2503lem1  17083  2503lem2  17084  2503lem3  17085  2503prm  17086  4001lem1  17087  4001lem2  17088  4001lem3  17089  4001lem4  17090  4001prm  17091  cphipval2  25174  4cphipval2  25175  minveclem2  25359  minveclem3  25362  minveclem7  25368  uniioombl  25523  dveflem  25916  sincosq4sgn  26443  tan4thpi  26456  sincos6thpi  26458  ang180lem2  26753  heron  26781  quad2  26782  quad  26783  dcubic2  26787  dcubic  26789  mcubic  26790  cubic2  26791  cubic  26792  dquartlem1  26794  dquartlem2  26795  dquart  26796  quart1cl  26797  quart1lem  26798  quart1  26799  quartlem1  26800  quartlem2  26801  quartlem4  26803  quart  26804  log2cnv  26887  log2tlbnd  26888  log2ublem3  26891  log2ub  26892  bclbnd  27224  bposlem8  27235  bposlem9  27236  2lgslem3a  27340  2lgslem3b  27341  2lgslem3c  27342  2lgslem3d  27343  2lgsoddprmlem2  27353  2lgsoddprmlem3c  27356  2lgsoddprmlem3d  27357  addsqnreup  27387  addsq2nreurex  27388  pntibndlem2  27535  pntlemb  27541  ex-opab  30411  ex-exp  30429  ex-fac  30430  ex-bc  30431  ex-ind-dvds  30440  4ipval2  30687  ipidsq  30689  dipcl  30691  dipcj  30693  dip0r  30696  dipcn  30699  ip1ilem  30805  ipasslem10  30818  minvecolem2  30854  minvecolem7  30862  normpar2i  31135  polid2i  31136  lnopeq0i  31986  quad3d  32723  constrresqrtcl  33760  cos9thpiminplylem1  33765  fib5  34389  fib6  34390  hgt750lemd  34632  hgt750lem  34635  hgt750lem2  34636  quad3  35650  60gcd7e1  41986  420lcm8e840  41992  lcmineqlem23  42032  3exp7  42034  3lexlogpow5ineq1  42035  3lexlogpow2ineq2  42040  aks4d1p1p4  42052  aks4d1p1p7  42055  aks4d1p1p5  42056  aks4d1p1  42057  4t5e20  42272  sq4  42274  235t711  42286  flt4lem5e  42637  inductionexd  44137  lhe4.4ex1a  44311  limclner  45642  stoweidlem13  46004  wallispi2lem1  46062  wallispi2lem2  46063  stirlinglem3  46067  stirlinglem10  46074  stirlinglem12  46076  sqwvfourb  46220  fouriersw  46222  sinnpoly  46885  ceil5half3  47334  modm1p1ne  47364  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  48481  itsclc0yqsollem1  48744  itscnhlinecirc02plem1  48764  5m4e1  49779