Theorem 4cn 12335

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 12315	. 2 ⊢ 4 = (3 + 1)
2		3cn 12331	. . 3 ⊢ 3 ∈ ℂ
3		ax-1cn 11203	. . 3 ⊢ 1 ∈ ℂ
4	2, 3	addcli 11257	. 2 ⊢ (3 + 1) ∈ ℂ
5	1, 4	eqeltri 2821	1 ⊢ 4 ∈ ℂ

Syntax hints:   ∈ wcel 2098  (class class class)co 7419  ℂcc 11143  1c1 11146   + caddc 11148  3c3 12306  4c4 12307

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2696  ax-1cn 11203  ax-addcl 11205

This theorem depends on definitions:  df-bi 206  df-an 395  df-ex 1774  df-cleq 2717  df-clel 2802  df-2 12313  df-3 12314  df-4 12315

This theorem is referenced by:  5cn  12338  5m1e4  12380  4p2e6  12403  4p3e7  12404  4p4e8  12405  4t2e8  12418  4d2e2  12420  8th4div3  12470  div4p1lem1div2  12505  5p5e10  12786  4t4e16  12814  6t5e30  12822  fldiv4p1lem1div2  13841  sq4e2t8  14203  discr  14243  sqoddm1div8  14246  4bc2eq6  14332  bpoly3  16046  bpoly4  16047  cos2bnd  16176  flodddiv4  16401  6gcd4e2  16525  6lcm4e12  16603  pythagtriplem1  16804  2exp11  17078  13prm  17104  43prm  17110  163prm  17113  317prm  17114  631prm  17115  1259lem1  17119  1259lem2  17120  1259lem3  17121  1259lem4  17122  1259lem5  17123  1259prm  17124  2503lem1  17125  2503lem2  17126  2503lem3  17127  2503prm  17128  4001lem1  17129  4001lem2  17130  4001lem3  17131  4001lem4  17132  4001prm  17133  cphipval2  25230  4cphipval2  25231  minveclem2  25415  minveclem3  25418  minveclem7  25424  uniioombl  25579  dveflem  25972  sincosq4sgn  26498  sincos6thpi  26512  ang180lem2  26807  heron  26835  quad2  26836  quad  26837  dcubic2  26841  dcubic  26843  mcubic  26844  cubic2  26845  cubic  26846  dquartlem1  26848  dquartlem2  26849  dquart  26850  quart1cl  26851  quart1lem  26852  quart1  26853  quartlem1  26854  quartlem2  26855  quartlem4  26857  quart  26858  log2cnv  26941  log2tlbnd  26942  log2ublem3  26945  log2ub  26946  bclbnd  27278  bposlem8  27289  bposlem9  27290  2lgslem3a  27394  2lgslem3b  27395  2lgslem3c  27396  2lgslem3d  27397  2lgsoddprmlem2  27407  2lgsoddprmlem3c  27410  2lgsoddprmlem3d  27411  addsqnreup  27441  addsq2nreurex  27442  pntibndlem2  27589  pntlemb  27595  ex-opab  30334  ex-exp  30352  ex-fac  30353  ex-bc  30354  ex-ind-dvds  30363  4ipval2  30610  ipidsq  30612  dipcl  30614  dipcj  30616  dip0r  30619  dipcn  30622  ip1ilem  30728  ipasslem10  30741  minvecolem2  30777  minvecolem7  30785  normpar2i  31058  polid2i  31059  lnopeq0i  31909  fib5  34176  fib6  34177  hgt750lemd  34431  hgt750lem  34434  hgt750lem2  34435  quad3  35425  60gcd7e1  41628  420lcm8e840  41634  lcmineqlem23  41674  3exp7  41676  3lexlogpow5ineq1  41677  3lexlogpow2ineq2  41682  aks4d1p1p4  41694  aks4d1p1p7  41697  aks4d1p1p5  41698  aks4d1p1  41699  4t5e20  42019  235t711  42021  flt4lem5e  42220  inductionexd  43732  lhe4.4ex1a  43913  limclner  45182  stoweidlem13  45544  wallispi2lem1  45602  wallispi2lem2  45603  stirlinglem3  45607  stirlinglem10  45614  stirlinglem12  45616  sqwvfourb  45760  fouriersw  45762  fmtnorec4  47031  fmtno5lem4  47038  257prm  47043  fmtnofac1  47052  fmtno4prmfac  47054  fmtno5faclem1  47061  fmtno5faclem2  47062  139prmALT  47078  mod42tp1mod8  47084  3exp4mod41  47098  41prothprmlem1  47099  41prothprmlem2  47100  41prothprm  47101  quad1  47102  8even  47195  2exp340mod341  47215  8exp8mod9  47218  mogoldbb  47267  nnsum4primeseven  47282  nnsum4primesevenALTV  47283  bgoldbtbndlem2  47288  zlmodzxzequap  47758  itsclc0yqsollem1  48026  itscnhlinecirc02plem1  48046  5m4e1  48421