Theorem 4cn 12296

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 12276	. 2 ⊢ 4 = (3 + 1)
2		3cn 12292	. . 3 ⊢ 3 ∈ ℂ
3		ax-1cn 11167	. . 3 ⊢ 1 ∈ ℂ
4	2, 3	addcli 11219	. 2 ⊢ (3 + 1) ∈ ℂ
5	1, 4	eqeltri 2829	1 ⊢ 4 ∈ ℂ

Syntax hints:   ∈ wcel 2106  (class class class)co 7408  ℂcc 11107  1c1 11110   + caddc 11112  3c3 12267  4c4 12268

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703  ax-1cn 11167  ax-addcl 11169

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1782  df-cleq 2724  df-clel 2810  df-2 12274  df-3 12275  df-4 12276

This theorem is referenced by:  5cn  12299  5m1e4  12341  4p2e6  12364  4p3e7  12365  4p4e8  12366  4t2e8  12379  4d2e2  12381  8th4div3  12431  div4p1lem1div2  12466  5p5e10  12747  4t4e16  12775  6t5e30  12783  fldiv4p1lem1div2  13799  sq4e2t8  14162  discr  14202  sqoddm1div8  14205  4bc2eq6  14288  bpoly3  16001  bpoly4  16002  cos2bnd  16130  flodddiv4  16355  6gcd4e2  16479  6lcm4e12  16552  pythagtriplem1  16748  2exp11  17022  13prm  17048  43prm  17054  163prm  17057  317prm  17058  631prm  17059  1259lem1  17063  1259lem2  17064  1259lem3  17065  1259lem4  17066  1259lem5  17067  1259prm  17068  2503lem1  17069  2503lem2  17070  2503lem3  17071  2503prm  17072  4001lem1  17073  4001lem2  17074  4001lem3  17075  4001lem4  17076  4001prm  17077  cphipval2  24757  4cphipval2  24758  minveclem2  24942  minveclem3  24945  minveclem7  24951  uniioombl  25105  dveflem  25495  sincosq4sgn  26010  sincos6thpi  26024  ang180lem2  26312  heron  26340  quad2  26341  quad  26342  dcubic2  26346  dcubic  26348  mcubic  26349  cubic2  26350  cubic  26351  dquartlem1  26353  dquartlem2  26354  dquart  26355  quart1cl  26356  quart1lem  26357  quart1  26358  quartlem1  26359  quartlem2  26360  quartlem4  26362  quart  26363  log2cnv  26446  log2tlbnd  26447  log2ublem3  26450  log2ub  26451  bclbnd  26780  bposlem8  26791  bposlem9  26792  2lgslem3a  26896  2lgslem3b  26897  2lgslem3c  26898  2lgslem3d  26899  2lgsoddprmlem2  26909  2lgsoddprmlem3c  26912  2lgsoddprmlem3d  26913  addsqnreup  26943  addsq2nreurex  26944  pntibndlem2  27091  pntlemb  27097  ex-opab  29682  ex-exp  29700  ex-fac  29701  ex-bc  29702  ex-ind-dvds  29711  4ipval2  29956  ipidsq  29958  dipcl  29960  dipcj  29962  dip0r  29965  dipcn  29968  ip1ilem  30074  ipasslem10  30087  minvecolem2  30123  minvecolem7  30131  normpar2i  30404  polid2i  30405  lnopeq0i  31255  fib5  33399  fib6  33400  hgt750lemd  33655  hgt750lem  33658  hgt750lem2  33659  quad3  34650  60gcd7e1  40865  420lcm8e840  40871  lcmineqlem23  40911  3exp7  40913  3lexlogpow5ineq1  40914  3lexlogpow2ineq2  40919  aks4d1p1p4  40931  aks4d1p1p7  40934  aks4d1p1p5  40935  aks4d1p1  40936  235t711  41205  flt4lem5e  41399  inductionexd  42896  lhe4.4ex1a  43078  limclner  44357  stoweidlem13  44719  wallispi2lem1  44777  wallispi2lem2  44778  stirlinglem3  44782  stirlinglem10  44789  stirlinglem12  44791  sqwvfourb  44935  fouriersw  44937  fmtnorec4  46207  fmtno5lem4  46214  257prm  46219  fmtnofac1  46228  fmtno4prmfac  46230  fmtno5faclem1  46237  fmtno5faclem2  46238  139prmALT  46254  mod42tp1mod8  46260  3exp4mod41  46274  41prothprmlem1  46275  41prothprmlem2  46276  41prothprm  46277  quad1  46278  8even  46371  2exp340mod341  46391  8exp8mod9  46394  mogoldbb  46443  nnsum4primeseven  46458  nnsum4primesevenALTV  46459  bgoldbtbndlem2  46464  zlmodzxzequap  47170  itsclc0yqsollem1  47438  itscnhlinecirc02plem1  47458  5m4e1  47834