Theorem 4cn 12067

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 12047	. 2 ⊢ 4 = (3 + 1)
2		3cn 12063	. . 3 ⊢ 3 ∈ ℂ
3		ax-1cn 10938	. . 3 ⊢ 1 ∈ ℂ
4	2, 3	addcli 10990	. 2 ⊢ (3 + 1) ∈ ℂ
5	1, 4	eqeltri 2836	1 ⊢ 4 ∈ ℂ

Syntax hints:   ∈ wcel 2107  (class class class)co 7284  ℂcc 10878  1c1 10881   + caddc 10883  3c3 12038  4c4 12039

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2710  ax-1cn 10938  ax-addcl 10940

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1783  df-cleq 2731  df-clel 2817  df-2 12045  df-3 12046  df-4 12047

This theorem is referenced by:  5cn  12070  5m1e4  12112  4p2e6  12135  4p3e7  12136  4p4e8  12137  4t2e8  12150  4d2e2  12152  8th4div3  12202  div4p1lem1div2  12237  5p5e10  12517  4t4e16  12545  6t5e30  12553  fldiv4p1lem1div2  13564  sq4e2t8  13925  discr  13964  sqoddm1div8  13967  4bc2eq6  14052  bpoly3  15777  bpoly4  15778  cos2bnd  15906  flodddiv4  16131  6gcd4e2  16255  6lcm4e12  16330  pythagtriplem1  16526  2exp11  16800  13prm  16826  43prm  16832  163prm  16835  317prm  16836  631prm  16837  1259lem1  16841  1259lem2  16842  1259lem3  16843  1259lem4  16844  1259lem5  16845  1259prm  16846  2503lem1  16847  2503lem2  16848  2503lem3  16849  2503prm  16850  4001lem1  16851  4001lem2  16852  4001lem3  16853  4001lem4  16854  4001prm  16855  cphipval2  24414  4cphipval2  24415  minveclem2  24599  minveclem3  24602  minveclem7  24608  uniioombl  24762  dveflem  25152  sincosq4sgn  25667  sincos6thpi  25681  ang180lem2  25969  heron  25997  quad2  25998  quad  25999  dcubic2  26003  dcubic  26005  mcubic  26006  cubic2  26007  cubic  26008  dquartlem1  26010  dquartlem2  26011  dquart  26012  quart1cl  26013  quart1lem  26014  quart1  26015  quartlem1  26016  quartlem2  26017  quartlem4  26019  quart  26020  log2cnv  26103  log2tlbnd  26104  log2ublem3  26107  log2ub  26108  bclbnd  26437  bposlem8  26448  bposlem9  26449  2lgslem3a  26553  2lgslem3b  26554  2lgslem3c  26555  2lgslem3d  26556  2lgsoddprmlem2  26566  2lgsoddprmlem3c  26569  2lgsoddprmlem3d  26570  addsqnreup  26600  addsq2nreurex  26601  pntibndlem2  26748  pntlemb  26754  ex-opab  28805  ex-exp  28823  ex-fac  28824  ex-bc  28825  ex-ind-dvds  28834  4ipval2  29079  ipidsq  29081  dipcl  29083  dipcj  29085  dip0r  29088  dipcn  29091  ip1ilem  29197  ipasslem10  29210  minvecolem2  29246  minvecolem7  29254  normpar2i  29527  polid2i  29528  lnopeq0i  30378  fib5  32381  fib6  32382  hgt750lemd  32637  hgt750lem  32640  hgt750lem2  32641  quad3  33637  60gcd7e1  40020  420lcm8e840  40026  lcmineqlem23  40066  3exp7  40068  3lexlogpow5ineq1  40069  3lexlogpow2ineq2  40074  aks4d1p1p4  40086  aks4d1p1p7  40089  aks4d1p1p5  40090  aks4d1p1  40091  235t711  40326  flt4lem5e  40500  inductionexd  41772  lhe4.4ex1a  41954  limclner  43199  stoweidlem13  43561  wallispi2lem1  43619  wallispi2lem2  43620  stirlinglem3  43624  stirlinglem10  43631  stirlinglem12  43633  sqwvfourb  43777  fouriersw  43779  fmtnorec4  45012  fmtno5lem4  45019  257prm  45024  fmtnofac1  45033  fmtno4prmfac  45035  fmtno5faclem1  45042  fmtno5faclem2  45043  139prmALT  45059  mod42tp1mod8  45065  3exp4mod41  45079  41prothprmlem1  45080  41prothprmlem2  45081  41prothprm  45082  quad1  45083  8even  45176  2exp340mod341  45196  8exp8mod9  45199  mogoldbb  45248  nnsum4primeseven  45263  nnsum4primesevenALTV  45264  bgoldbtbndlem2  45269  zlmodzxzequap  45851  itsclc0yqsollem1  46119  itscnhlinecirc02plem1  46139  5m4e1  46512