Theorem 5cn 11713

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 11691	. 2 ⊢ 5 = (4 + 1)
2		4cn 11710	. . 3 ⊢ 4 ∈ ℂ
3		ax-1cn 10584	. . 3 ⊢ 1 ∈ ℂ
4	2, 3	addcli 10636	. 2 ⊢ (4 + 1) ∈ ℂ
5	1, 4	eqeltri 2886	1 ⊢ 5 ∈ ℂ

Syntax hints:   ∈ wcel 2111  (class class class)co 7135  ℂcc 10524  1c1 10527   + caddc 10529  4c4 11682  5c5 11683

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770  ax-1cn 10584  ax-addcl 10586

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-cleq 2791  df-clel 2870  df-2 11688  df-3 11689  df-4 11690  df-5 11691

This theorem is referenced by:  6cn  11716  6m1e5  11756  5p2e7  11781  5p3e8  11782  5p4e9  11783  5p5e10  12157  5t2e10  12186  5recm6rec  12230  bpoly4  15405  ef01bndlem  15529  dec5dvds  16390  dec5nprm  16392  2exp16  16416  prmlem1  16433  17prm  16442  139prm  16449  163prm  16450  317prm  16451  631prm  16452  1259lem1  16456  1259lem2  16457  1259lem3  16458  1259lem4  16459  2503lem1  16462  2503lem2  16463  2503lem3  16464  4001lem1  16466  4001lem2  16467  4001lem3  16468  4001lem4  16469  4001prm  16470  log2ublem3  25534  log2ub  25535  ppiub  25788  bclbnd  25864  bposlem4  25871  bposlem5  25872  bposlem6  25873  bposlem8  25875  bposlem9  25876  lgsdir2lem1  25909  2lgslem3c  25982  2lgsoddprmlem3d  25997  ex-fac  28236  fib6  31774  hgt750lem2  32033  12lcm5e60  39296  lcmineqlem23  39339  sqn5i  39479  235t711  39485  ex-decpmul  39486  inductionexd  40858  fmtno5lem1  44070  fmtno5lem2  44071  257prm  44078  fmtno4prmfac193  44090  fmtno4nprmfac193  44091  flsqrt5  44111  139prmALT  44113  127prm  44116  2exp11  44118  5tcu2e40  44133  41prothprmlem2  44136  41prothprm  44137  2exp340mod341  44251  gbpart8  44286  linevalexample  44804  ackval3012  45106  5m4e1  45325