Theorem 5cn 12322

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 12300	. 2 ⊢ 5 = (4 + 1)
2		4cn 12319	. . 3 ⊢ 4 ∈ ℂ
3		ax-1cn 11188	. . 3 ⊢ 1 ∈ ℂ
4	2, 3	addcli 11242	. 2 ⊢ (4 + 1) ∈ ℂ
5	1, 4	eqeltri 2824	1 ⊢ 5 ∈ ℂ

Syntax hints:   ∈ wcel 2099  (class class class)co 7414  ℂcc 11128  1c1 11131   + caddc 11133  4c4 12291  5c5 12292

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2698  ax-1cn 11188  ax-addcl 11190

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1775  df-cleq 2719  df-clel 2805  df-2 12297  df-3 12298  df-4 12299  df-5 12300

This theorem is referenced by:  6cn  12325  6m1e5  12365  5p2e7  12390  5p3e8  12391  5p4e9  12392  5p5e10  12770  5t2e10  12799  5recm6rec  12843  bpoly4  16027  ef01bndlem  16152  dec5dvds  17024  dec5nprm  17026  2exp11  17050  2exp16  17051  prmlem1  17068  17prm  17077  139prm  17084  163prm  17085  317prm  17086  631prm  17087  1259lem1  17091  1259lem2  17092  1259lem3  17093  1259lem4  17094  2503lem1  17097  2503lem2  17098  2503lem3  17099  4001lem1  17101  4001lem2  17102  4001lem3  17103  4001lem4  17104  4001prm  17105  log2ublem3  26867  log2ub  26868  ppiub  27124  bclbnd  27200  bposlem4  27207  bposlem5  27208  bposlem6  27209  bposlem8  27211  bposlem9  27212  lgsdir2lem1  27245  2lgslem3c  27318  2lgsoddprmlem3d  27333  ex-fac  30248  fib6  33962  hgt750lem2  34220  12lcm5e60  41416  lcmineqlem23  41459  3lexlogpow5ineq1  41462  3lexlogpow5ineq5  41468  aks4d1p1p4  41479  aks4d1p1p6  41481  aks4d1p1p7  41482  sqn5i  41781  4t5e20  41787  235t711  41789  ex-decpmul  41790  inductionexd  43508  fmtno5lem1  46816  fmtno5lem2  46817  257prm  46824  fmtno4prmfac193  46836  fmtno4nprmfac193  46837  flsqrt5  46857  139prmALT  46859  127prm  46862  5tcu2e40  46878  41prothprmlem2  46881  41prothprm  46882  2exp340mod341  46996  gbpart8  47031  linevalexample  47386  ackval3012  47688  5m4e1  48153