Theorem 4cn 12352

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 12332	. 2 ⊢ 4 = (3 + 1)
2		3cn 12348	. . 3 ⊢ 3 ∈ ℂ
3		ax-1cn 11214	. . 3 ⊢ 1 ∈ ℂ
4	2, 3	addcli 11268	. 2 ⊢ (3 + 1) ∈ ℂ
5	1, 4	eqeltri 2836	1 ⊢ 4 ∈ ℂ

Syntax hints:   ∈ wcel 2107  (class class class)co 7432  ℂcc 11154  1c1 11157   + caddc 11159  3c3 12323  4c4 12324

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-ext 2707  ax-1cn 11214  ax-addcl 11216

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1779  df-cleq 2728  df-clel 2815  df-2 12330  df-3 12331  df-4 12332

This theorem is referenced by:  5cn  12355  5m1e4  12397  4p2e6  12420  4p3e7  12421  4p4e8  12422  4t2e8  12435  4d2e2  12437  8th4div3  12488  div4p1lem1div2  12523  5p5e10  12806  4t4e16  12834  6t5e30  12842  fldiv4p1lem1div2  13876  sq4e2t8  14239  discr  14280  sqoddm1div8  14283  4bc2eq6  14369  bpoly3  16095  bpoly4  16096  cos2bnd  16225  flodddiv4  16453  6gcd4e2  16576  6lcm4e12  16654  pythagtriplem1  16855  2exp11  17128  13prm  17154  43prm  17160  163prm  17163  317prm  17164  631prm  17165  1259lem1  17169  1259lem2  17170  1259lem3  17171  1259lem4  17172  1259lem5  17173  1259prm  17174  2503lem1  17175  2503lem2  17176  2503lem3  17177  2503prm  17178  4001lem1  17179  4001lem2  17180  4001lem3  17181  4001lem4  17182  4001prm  17183  cphipval2  25276  4cphipval2  25277  minveclem2  25461  minveclem3  25464  minveclem7  25470  uniioombl  25625  dveflem  26018  sincosq4sgn  26544  tan4thpi  26557  sincos6thpi  26559  ang180lem2  26854  heron  26882  quad2  26883  quad  26884  dcubic2  26888  dcubic  26890  mcubic  26891  cubic2  26892  cubic  26893  dquartlem1  26895  dquartlem2  26896  dquart  26897  quart1cl  26898  quart1lem  26899  quart1  26900  quartlem1  26901  quartlem2  26902  quartlem4  26904  quart  26905  log2cnv  26988  log2tlbnd  26989  log2ublem3  26992  log2ub  26993  bclbnd  27325  bposlem8  27336  bposlem9  27337  2lgslem3a  27441  2lgslem3b  27442  2lgslem3c  27443  2lgslem3d  27444  2lgsoddprmlem2  27454  2lgsoddprmlem3c  27457  2lgsoddprmlem3d  27458  addsqnreup  27488  addsq2nreurex  27489  pntibndlem2  27636  pntlemb  27642  ex-opab  30452  ex-exp  30470  ex-fac  30471  ex-bc  30472  ex-ind-dvds  30481  4ipval2  30728  ipidsq  30730  dipcl  30732  dipcj  30734  dip0r  30737  dipcn  30740  ip1ilem  30846  ipasslem10  30859  minvecolem2  30895  minvecolem7  30903  normpar2i  31176  polid2i  31177  lnopeq0i  32027  quad3d  32755  fib5  34408  fib6  34409  hgt750lemd  34664  hgt750lem  34667  hgt750lem2  34668  quad3  35676  60gcd7e1  42007  420lcm8e840  42013  lcmineqlem23  42053  3exp7  42055  3lexlogpow5ineq1  42056  3lexlogpow2ineq2  42061  aks4d1p1p4  42073  aks4d1p1p7  42076  aks4d1p1p5  42077  aks4d1p1  42078  4t5e20  42331  sq4  42332  235t711  42344  flt4lem5e  42671  inductionexd  44173  lhe4.4ex1a  44353  limclner  45671  stoweidlem13  46033  wallispi2lem1  46091  wallispi2lem2  46092  stirlinglem3  46096  stirlinglem10  46103  stirlinglem12  46105  sqwvfourb  46249  fouriersw  46251  ceil5half3  47347  fmtnorec4  47541  fmtno5lem4  47548  257prm  47553  fmtnofac1  47562  fmtno4prmfac  47564  fmtno5faclem1  47571  fmtno5faclem2  47572  139prmALT  47588  mod42tp1mod8  47594  3exp4mod41  47608  41prothprmlem1  47609  41prothprmlem2  47610  41prothprm  47611  quad1  47612  8even  47705  2exp340mod341  47725  8exp8mod9  47728  mogoldbb  47777  nnsum4primeseven  47792  nnsum4primesevenALTV  47793  bgoldbtbndlem2  47798  zlmodzxzequap  48421  itsclc0yqsollem1  48688  itscnhlinecirc02plem1  48708  5m4e1  49371