Theorem 5cn 12300

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 12278	. 2 ⊢ 5 = (4 + 1)
2		4cn 12297	. . 3 ⊢ 4 ∈ ℂ
3		ax-1cn 11168	. . 3 ⊢ 1 ∈ ℂ
4	2, 3	addcli 11220	. 2 ⊢ (4 + 1) ∈ ℂ
5	1, 4	eqeltri 2830	1 ⊢ 5 ∈ ℂ

Syntax hints:   ∈ wcel 2107  (class class class)co 7409  ℂcc 11108  1c1 11111   + caddc 11113  4c4 12269  5c5 12270

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704  ax-1cn 11168  ax-addcl 11170

This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-cleq 2725  df-clel 2811  df-2 12275  df-3 12276  df-4 12277  df-5 12278

This theorem is referenced by:  6cn  12303  6m1e5  12343  5p2e7  12368  5p3e8  12369  5p4e9  12370  5p5e10  12748  5t2e10  12777  5recm6rec  12821  bpoly4  16003  ef01bndlem  16127  dec5dvds  16997  dec5nprm  16999  2exp11  17023  2exp16  17024  prmlem1  17041  17prm  17050  139prm  17057  163prm  17058  317prm  17059  631prm  17060  1259lem1  17064  1259lem2  17065  1259lem3  17066  1259lem4  17067  2503lem1  17070  2503lem2  17071  2503lem3  17072  4001lem1  17074  4001lem2  17075  4001lem3  17076  4001lem4  17077  4001prm  17078  log2ublem3  26453  log2ub  26454  ppiub  26707  bclbnd  26783  bposlem4  26790  bposlem5  26791  bposlem6  26792  bposlem8  26794  bposlem9  26795  lgsdir2lem1  26828  2lgslem3c  26901  2lgsoddprmlem3d  26916  ex-fac  29704  fib6  33405  hgt750lem2  33664  12lcm5e60  40873  lcmineqlem23  40916  3lexlogpow5ineq1  40919  3lexlogpow5ineq5  40925  aks4d1p1p4  40936  aks4d1p1p6  40938  aks4d1p1p7  40939  sqn5i  41197  4t5e20  41203  235t711  41205  ex-decpmul  41206  inductionexd  42906  fmtno5lem1  46221  fmtno5lem2  46222  257prm  46229  fmtno4prmfac193  46241  fmtno4nprmfac193  46242  flsqrt5  46262  139prmALT  46264  127prm  46267  5tcu2e40  46283  41prothprmlem2  46286  41prothprm  46287  2exp340mod341  46401  gbpart8  46436  linevalexample  47076  ackval3012  47378  5m4e1  47844