Theorem 5cn 11966

Description: The number 5 is a complex number. (Contributed by David A. Wheeler, 8-Dec-2018.) Reduce dependencies on axioms. (Revised by Steven Nguyen, 4-Oct-2022.)

Assertion

Ref	Expression
5cn	⊢ 5 ∈ ℂ

Proof of Theorem 5cn

Step	Hyp	Ref	Expression
1		df-5 11944	. 2 ⊢ 5 = (4 + 1)
2		4cn 11963	. . 3 ⊢ 4 ∈ ℂ
3		ax-1cn 10835	. . 3 ⊢ 1 ∈ ℂ
4	2, 3	addcli 10887	. 2 ⊢ (4 + 1) ∈ ℂ
5	1, 4	eqeltri 2836	1 ⊢ 5 ∈ ℂ

Syntax hints:   ∈ wcel 2112  (class class class)co 7252  ℂcc 10775  1c1 10778   + caddc 10780  4c4 11935  5c5 11936

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2114  ax-9 2122  ax-ext 2710  ax-1cn 10835  ax-addcl 10837

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1788  df-cleq 2731  df-clel 2818  df-2 11941  df-3 11942  df-4 11943  df-5 11944

This theorem is referenced by:  6cn  11969  6m1e5  12009  5p2e7  12034  5p3e8  12035  5p4e9  12036  5p5e10  12412  5t2e10  12441  5recm6rec  12485  bpoly4  15672  ef01bndlem  15796  dec5dvds  16668  dec5nprm  16670  2exp11  16694  2exp16  16695  prmlem1  16712  17prm  16721  139prm  16728  163prm  16729  317prm  16730  631prm  16731  1259lem1  16735  1259lem2  16736  1259lem3  16737  1259lem4  16738  2503lem1  16741  2503lem2  16742  2503lem3  16743  4001lem1  16745  4001lem2  16746  4001lem3  16747  4001lem4  16748  4001prm  16749  log2ublem3  25978  log2ub  25979  ppiub  26232  bclbnd  26308  bposlem4  26315  bposlem5  26316  bposlem6  26317  bposlem8  26319  bposlem9  26320  lgsdir2lem1  26353  2lgslem3c  26426  2lgsoddprmlem3d  26441  ex-fac  28691  fib6  32248  hgt750lem2  32507  12lcm5e60  39923  lcmineqlem23  39966  3lexlogpow5ineq1  39969  3lexlogpow5ineq5  39975  aks4d1p1p4  39985  aks4d1p1p6  39987  aks4d1p1p7  39988  sqn5i  40206  235t711  40212  ex-decpmul  40213  inductionexd  41627  fmtno5lem1  44866  fmtno5lem2  44867  257prm  44874  fmtno4prmfac193  44886  fmtno4nprmfac193  44887  flsqrt5  44907  139prmALT  44909  127prm  44912  5tcu2e40  44928  41prothprmlem2  44931  41prothprm  44932  2exp340mod341  45046  gbpart8  45081  linevalexample  45597  ackval3012  45899  5m4e1  46360