Theorem 5cn 12061

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 12039	. 2 ⊢ 5 = (4 + 1)
2		4cn 12058	. . 3 ⊢ 4 ∈ ℂ
3		ax-1cn 10930	. . 3 ⊢ 1 ∈ ℂ
4	2, 3	addcli 10982	. 2 ⊢ (4 + 1) ∈ ℂ
5	1, 4	eqeltri 2837	1 ⊢ 5 ∈ ℂ

Syntax hints:   ∈ wcel 2110  (class class class)co 7271  ℂcc 10870  1c1 10873   + caddc 10875  4c4 12030  5c5 12031

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2015  ax-8 2112  ax-9 2120  ax-ext 2711  ax-1cn 10930  ax-addcl 10932

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1787  df-cleq 2732  df-clel 2818  df-2 12036  df-3 12037  df-4 12038  df-5 12039

This theorem is referenced by:  6cn  12064  6m1e5  12104  5p2e7  12129  5p3e8  12130  5p4e9  12131  5p5e10  12507  5t2e10  12536  5recm6rec  12580  bpoly4  15767  ef01bndlem  15891  dec5dvds  16763  dec5nprm  16765  2exp11  16789  2exp16  16790  prmlem1  16807  17prm  16816  139prm  16823  163prm  16824  317prm  16825  631prm  16826  1259lem1  16830  1259lem2  16831  1259lem3  16832  1259lem4  16833  2503lem1  16836  2503lem2  16837  2503lem3  16838  4001lem1  16840  4001lem2  16841  4001lem3  16842  4001lem4  16843  4001prm  16844  log2ublem3  26096  log2ub  26097  ppiub  26350  bclbnd  26426  bposlem4  26433  bposlem5  26434  bposlem6  26435  bposlem8  26437  bposlem9  26438  lgsdir2lem1  26471  2lgslem3c  26544  2lgsoddprmlem3d  26559  ex-fac  28811  fib6  32369  hgt750lem2  32628  12lcm5e60  40013  lcmineqlem23  40056  3lexlogpow5ineq1  40059  3lexlogpow5ineq5  40065  aks4d1p1p4  40076  aks4d1p1p6  40078  aks4d1p1p7  40079  sqn5i  40310  235t711  40316  ex-decpmul  40317  inductionexd  41735  fmtno5lem1  44974  fmtno5lem2  44975  257prm  44982  fmtno4prmfac193  44994  fmtno4nprmfac193  44995  flsqrt5  45015  139prmALT  45017  127prm  45020  5tcu2e40  45036  41prothprmlem2  45039  41prothprm  45040  2exp340mod341  45154  gbpart8  45189  linevalexample  45705  ackval3012  46007  5m4e1  46470