Theorem 4cn 12438

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 12417	. 2 ⊢ 4 = (3 + 1)
2		3cn 12434	. . 3 ⊢ 3 ∈ ℂ
3		ax-1cn 11268	. . 3 ⊢ 1 ∈ ℂ
4	2, 3	addcli 11325	. 2 ⊢ (3 + 1) ∈ ℂ
5	1, 4	eqeltri 2859	1 ⊢ 4 ∈ ℂ

This proof depends on syntax axioms:   ∈ wcel 2146  (class class class)co 7427  ℂcc 11208  1c1 11211   + caddc 11213  3c3 12408  4c4 12409

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1944  ax-6 2001  ax-7 2042  ax-8 2148  ax-9 2156  ax-ext 2735  ax-1cn 11268  ax-addcl 11270

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-cleq 2755  df-clel 2838  df-2 12415  df-3 12416  df-4 12417

This theorem is used by:  5cn  12441  5m1e4  12482  4p2e6  12505  4p3e7  12506  4p4e8  12507  4t2e8  12521  2t4e8  12522  4div2e2  12524  8th4div3  12576  div4p1lem1div2  12611  5p5e10  12900  4t4e16  12928  6t5e30  12936  fldiv4p1lem1div2  13985  sq4e2t8  14352  discr  14394  sqoddm1div8  14397  4bc2eq6  14483  bpoly3  16236  bpoly4  16237  cos2bnd  16368  flodddiv4  16597  6gcd4e2  16723  6lcm4e12  16803  pythagtriplem1  17006  2exp11  17279  13prm  17306  43prm  17312  83prm  17313  163prm  17315  317prm  17316  631prm  17317  1259lem1  17321  1259lem2  17322  1259lem3  17323  1259lem4  17324  1259lem5  17325  1259prm  17326  2503lem1  17327  2503lem2  17328  2503lem3  17329  2503prm  17330  4001lem1  17331  4001lem2  17332  4001lem3  17333  4001lem4  17334  4001prm  17335  cphipval2  25574  4cphipval2  25575  minveclem2  25759  minveclem3  25762  minveclem7  25768  uniioombl  25922  dveflem  26311  sincosq4sgn  26842  tan4thpi  26855  sincos6thpi  26856  ang180lem2  27150  heron  27178  quad2  27179  quad  27180  dcubic2  27184  dcubic  27186  mcubic  27187  cubic2  27188  cubic  27189  dquartlem1  27191  dquartlem2  27192  dquart  27193  quart1cl  27194  quart1lem  27195  quart1  27196  quartlem1  27197  quartlem2  27198  quartlem4  27200  quart  27201  log2cnv  27284  log2tlbnd  27285  log2ublem3  27288  log2ub  27289  bclbnd  27619  bposlem8  27630  bposlem9  27631  2lgslem3a  27735  2lgslem3b  27736  2lgslem3c  27737  2lgslem3d  27738  2lgsoddprmlem2  27748  2lgsoddprmlem3c  27751  2lgsoddprmlem3d  27752  addsqnreup  27782  addsq2nreurex  27783  pntibndlem2  27930  pntlemb  27936  ex-opab  31045  ex-exp  31063  ex-fac  31064  ex-bc  31065  ex-ind-dvds  31074  4ipval2  31322  ipidsq  31324  dipcl  31326  dipcj  31328  dip0r  31331  dipcn  31334  ip1ilem  31440  ipasslem10  31453  minvecolem2  31489  minvecolem7  31497  normpar2i  31770  polid2i  31771  lnopeq0i  32621  quad3d  33394  constrresqrtcl  34462  cos9thpiminplylem1  34467  fib5  35090  fib6  35091  hgt750lemd  35330  hgt750lem  35333  hgt750lem2  35334  quad3  36556  60gcd7e1  43195  420lcm8e840  43201  lcmineqlem23  43241  3exp7  43243  3lexlogpow5ineq1  43244  3lexlogpow2ineq2  43249  aks4d1p1p4  43261  aks4d1p1p7  43264  aks4d1p1p5  43265  aks4d1p1  43266  25or6to4  43396  4p4e8ALT  43449  1p5e6  43452  2p6e8  43459  4p5e9  43464  4t5e20  43488  sq4  43490  235t711  43502  inductionexd  45295  lhe4.4ex1a  45453  limclner  46800  stoweidlem13  47162  wallispi2lem1  47220  wallispi2lem2  47221  stirlinglem3  47225  stirlinglem10  47232  stirlinglem12  47234  sqwvfourb  47378  fouriersw  47380  sin5tlem1  48058  sin5tlem2  48059  sin5tlem3  48060  sin5tlem4  48061  cos5t  48064  goldpolyfactor  48066  goldratmolem2  48072  goldratval  48075  sinnpoly  48080  ceil5half3  48555  modm1p1ne  48585  fmtnorec4  48773  fmtno5lem4  48780  257prm  48785  fmtnofac1  48794  fmtno4prmfac  48796  fmtno5faclem1  48803  fmtno5faclem2  48804  139prmALT  48820  mod42tp1mod8  48826  3exp4mod41  48840  41prothprmlem1  48841  41prothprmlem2  48842  41prothprm  48843  ppivalnn4  48851  quad1  48857  8even  48950  2exp340mod341  48970  mogoldbb  49022  nnsum4primeseven  49037  nnsum4primesevenALTV  49038  bgoldbtbndlem2  49043  zlmodzxzequap  49750  itsclc0yqsollem1  50013  itscnhlinecirc02plem1  50033  5m4e1  51149