Theorem 4cn 12343

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 12322	. 2 ⊢ 4 = (3 + 1)
2		3cn 12339	. . 3 ⊢ 3 ∈ ℂ
3		ax-1cn 11175	. . 3 ⊢ 1 ∈ ℂ
4	2, 3	addcli 11232	. 2 ⊢ (3 + 1) ∈ ℂ
5	1, 4	eqeltri 2861	1 ⊢ 4 ∈ ℂ

This proof depends on syntax axioms:   ∈ wcel 2146  (class class class)co 7419  ℂcc 11115  1c1 11118   + caddc 11120  3c3 12313  4c4 12314

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2737  ax-1cn 11175  ax-addcl 11177

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2757  df-clel 2840  df-2 12320  df-3 12321  df-4 12322

This theorem is used by:  5cn  12346  5m1e4  12387  4p2e6  12410  4p3e7  12411  4p4e8  12412  4t2e8  12426  2t4e8  12427  4div2e2  12429  8th4div3  12481  div4p1lem1div2  12516  5p5e10  12805  4t4e16  12833  6t5e30  12841  fldiv4p1lem1div2  13888  sq4e2t8  14255  discr  14296  sqoddm1div8  14299  4bc2eq6  14385  bpoly3  16136  bpoly4  16137  cos2bnd  16268  flodddiv4  16497  6gcd4e2  16620  6lcm4e12  16698  pythagtriplem1  16900  2exp11  17173  13prm  17200  43prm  17206  83prm  17207  163prm  17209  317prm  17210  631prm  17211  1259lem1  17215  1259lem2  17216  1259lem3  17217  1259lem4  17218  1259lem5  17219  1259prm  17220  2503lem1  17221  2503lem2  17222  2503lem3  17223  2503prm  17224  4001lem1  17225  4001lem2  17226  4001lem3  17227  4001lem4  17228  4001prm  17229  cphipval2  25453  4cphipval2  25454  minveclem2  25638  minveclem3  25641  minveclem7  25647  uniioombl  25801  dveflem  26191  sincosq4sgn  26719  tan4thpi  26732  sincos6thpi  26734  ang180lem2  27028  heron  27056  quad2  27057  quad  27058  dcubic2  27062  dcubic  27064  mcubic  27065  cubic2  27066  cubic  27067  dquartlem1  27069  dquartlem2  27070  dquart  27071  quart1cl  27072  quart1lem  27073  quart1  27074  quartlem1  27075  quartlem2  27076  quartlem4  27078  quart  27079  log2cnv  27162  log2tlbnd  27163  log2ublem3  27166  log2ub  27167  bclbnd  27497  bposlem8  27508  bposlem9  27509  2lgslem3a  27613  2lgslem3b  27614  2lgslem3c  27615  2lgslem3d  27616  2lgsoddprmlem2  27626  2lgsoddprmlem3c  27629  2lgsoddprmlem3d  27630  addsqnreup  27660  addsq2nreurex  27661  pntibndlem2  27808  pntlemb  27814  ex-opab  30856  ex-exp  30874  ex-fac  30875  ex-bc  30876  ex-ind-dvds  30885  4ipval2  31133  ipidsq  31135  dipcl  31137  dipcj  31139  dip0r  31142  dipcn  31145  ip1ilem  31251  ipasslem10  31264  minvecolem2  31300  minvecolem7  31308  normpar2i  31581  polid2i  31582  lnopeq0i  32432  quad3d  33166  constrresqrtcl  34233  cos9thpiminplylem1  34238  fib5  34862  fib6  34863  hgt750lemd  35102  hgt750lem  35105  hgt750lem2  35106  quad3  36201  60gcd7e1  42832  420lcm8e840  42838  lcmineqlem23  42878  3exp7  42880  3lexlogpow5ineq1  42881  3lexlogpow2ineq2  42886  aks4d1p1p4  42898  aks4d1p1p7  42901  aks4d1p1p5  42902  aks4d1p1  42903  25or6to4  43033  4t5e20  43112  sq4  43114  235t711  43126  flt4lem5e  43448  inductionexd  44941  lhe4.4ex1a  45099  limclner  46425  stoweidlem13  46787  wallispi2lem1  46845  wallispi2lem2  46846  stirlinglem3  46850  stirlinglem10  46857  stirlinglem12  46859  sqwvfourb  47003  fouriersw  47005  sin5tlem1  47670  sin5tlem2  47671  sin5tlem3  47672  sin5tlem4  47673  cos5t  47676  goldratmolem2  47683  sinnpoly  47688  ceil5half3  48143  modm1p1ne  48173  fmtnorec4  48361  fmtno5lem4  48368  257prm  48373  fmtnofac1  48382  fmtno4prmfac  48384  fmtno5faclem1  48391  fmtno5faclem2  48392  139prmALT  48408  mod42tp1mod8  48414  3exp4mod41  48428  41prothprmlem1  48429  41prothprmlem2  48430  41prothprm  48431  ppivalnn4  48439  quad1  48445  8even  48538  2exp340mod341  48558  mogoldbb  48610  nnsum4primeseven  48625  nnsum4primesevenALTV  48626  bgoldbtbndlem2  48631  zlmodzxzequap  49338  itsclc0yqsollem1  49601  itscnhlinecirc02plem1  49621  5m4e1  50676