Theorem 4cn 12326

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 12305	. 2 ⊢ 4 = (3 + 1)
2		3cn 12322	. . 3 ⊢ 3 ∈ ℂ
3		ax-1cn 11158	. . 3 ⊢ 1 ∈ ℂ
4	2, 3	addcli 11215	. 2 ⊢ (3 + 1) ∈ ℂ
5	1, 4	eqeltri 2865	1 ⊢ 4 ∈ ℂ

Syntax hints:   ∈ wcel 2149  (class class class)co 7411  ℂcc 11098  1c1 11101   + caddc 11103  3c3 12296  4c4 12297

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741  ax-1cn 11158  ax-addcl 11160

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1807  df-cleq 2761  df-clel 2844  df-2 12303  df-3 12304  df-4 12305

This theorem is referenced by:  5cn  12329  5m1e4  12370  4p2e6  12393  4p3e7  12394  4p4e8  12395  4t2e8  12409  2t4e8  12410  4div2e2  12412  8th4div3  12464  div4p1lem1div2  12499  5p5e10  12787  4t4e16  12815  6t5e30  12823  fldiv4p1lem1div2  13868  sq4e2t8  14235  discr  14276  sqoddm1div8  14279  4bc2eq6  14365  bpoly3  16112  bpoly4  16113  cos2bnd  16244  flodddiv4  16473  6gcd4e2  16596  6lcm4e12  16674  pythagtriplem1  16876  2exp11  17149  13prm  17176  43prm  17182  163prm  17185  317prm  17186  631prm  17187  1259lem1  17191  1259lem2  17192  1259lem3  17193  1259lem4  17194  1259lem5  17195  1259prm  17196  2503lem1  17197  2503lem2  17198  2503lem3  17199  2503prm  17200  4001lem1  17201  4001lem2  17202  4001lem3  17203  4001lem4  17204  4001prm  17205  cphipval2  25369  4cphipval2  25370  minveclem2  25554  minveclem3  25557  minveclem7  25563  uniioombl  25717  dveflem  26107  sincosq4sgn  26632  tan4thpi  26645  sincos6thpi  26647  ang180lem2  26941  heron  26969  quad2  26970  quad  26971  dcubic2  26975  dcubic  26977  mcubic  26978  cubic2  26979  cubic  26980  dquartlem1  26982  dquartlem2  26983  dquart  26984  quart1cl  26985  quart1lem  26986  quart1  26987  quartlem1  26988  quartlem2  26989  quartlem4  26991  quart  26992  log2cnv  27075  log2tlbnd  27076  log2ublem3  27079  log2ub  27080  bclbnd  27410  bposlem8  27421  bposlem9  27422  2lgslem3a  27526  2lgslem3b  27527  2lgslem3c  27528  2lgslem3d  27529  2lgsoddprmlem2  27539  2lgsoddprmlem3c  27542  2lgsoddprmlem3d  27543  addsqnreup  27573  addsq2nreurex  27574  pntibndlem2  27721  pntlemb  27727  ex-opab  30724  ex-exp  30742  ex-fac  30743  ex-bc  30744  ex-ind-dvds  30753  4ipval2  31001  ipidsq  31003  dipcl  31005  dipcj  31007  dip0r  31010  dipcn  31013  ip1ilem  31119  ipasslem10  31132  minvecolem2  31168  minvecolem7  31176  normpar2i  31449  polid2i  31450  lnopeq0i  32300  quad3d  33035  constrresqrtcl  34112  cos9thpiminplylem1  34117  fib5  34740  fib6  34741  hgt750lemd  34980  hgt750lem  34983  hgt750lem2  34984  quad3  36061  60gcd7e1  42662  420lcm8e840  42668  lcmineqlem23  42708  3exp7  42710  3lexlogpow5ineq1  42711  3lexlogpow2ineq2  42716  aks4d1p1p4  42728  aks4d1p1p7  42731  aks4d1p1p5  42732  aks4d1p1  42733  25or6to4  42863  4t5e20  42942  sq4  42944  235t711  42956  flt4lem5e  43280  inductionexd  44773  lhe4.4ex1a  44931  limclner  46257  stoweidlem13  46619  wallispi2lem1  46677  wallispi2lem2  46678  stirlinglem3  46682  stirlinglem10  46689  stirlinglem12  46691  sqwvfourb  46835  fouriersw  46837  sin5tlem1  47499  sin5tlem2  47500  sin5tlem3  47501  sin5tlem4  47502  cos5t  47505  goldratmolem2  47512  sinnpoly  47517  ceil5half3  47972  modm1p1ne  48002  fmtnorec4  48190  fmtno5lem4  48197  257prm  48202  fmtnofac1  48211  fmtno4prmfac  48213  fmtno5faclem1  48220  fmtno5faclem2  48221  139prmALT  48237  mod42tp1mod8  48243  3exp4mod41  48257  41prothprmlem1  48258  41prothprmlem2  48259  41prothprm  48260  ppivalnn4  48268  quad1  48274  8even  48367  2exp340mod341  48387  8exp8mod9  48390  mogoldbb  48439  nnsum4primeseven  48454  nnsum4primesevenALTV  48455  bgoldbtbndlem2  48460  zlmodzxzequap  49164  itsclc0yqsollem1  49427  itscnhlinecirc02plem1  49447  5m4e1  50471