Theorem 5cn 12260

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 12238	. 2 ⊢ 5 = (4 + 1)
2		4cn 12257	. . 3 ⊢ 4 ∈ ℂ
3		ax-1cn 11087	. . 3 ⊢ 1 ∈ ℂ
4	2, 3	addcli 11142	. 2 ⊢ (4 + 1) ∈ ℂ
5	1, 4	eqeltri 2833	1 ⊢ 5 ∈ ℂ

Syntax hints:   ∈ wcel 2114  (class class class)co 7360  ℂcc 11027  1c1 11030   + caddc 11032  4c4 12229  5c5 12230

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-1cn 11087  ax-addcl 11089

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2729  df-clel 2812  df-2 12235  df-3 12236  df-4 12237  df-5 12238

This theorem is referenced by:  6cn  12263  6m1e5  12298  5p2e7  12323  5p3e8  12324  5p4e9  12325  5p5e10  12706  5t2e10  12735  5recm6rec  12778  bpoly4  16015  ef01bndlem  16142  5ndvds3  16373  5ndvds6  16374  dec5dvds  17026  dec5nprm  17028  2exp11  17051  2exp16  17052  prmlem1  17069  17prm  17078  139prm  17085  163prm  17086  317prm  17087  631prm  17088  1259lem1  17092  1259lem2  17093  1259lem3  17094  1259lem4  17095  2503lem1  17098  2503lem2  17099  2503lem3  17100  4001lem1  17102  4001lem2  17103  4001lem3  17104  4001lem4  17105  4001prm  17106  log2ublem3  26925  log2ub  26926  ppiub  27181  bclbnd  27257  bposlem4  27264  bposlem5  27265  bposlem6  27266  bposlem8  27268  bposlem9  27269  lgsdir2lem1  27302  2lgslem3c  27375  2lgsoddprmlem3d  27390  ex-fac  30536  fib6  34566  hgt750lem2  34812  12lcm5e60  42461  lcmineqlem23  42504  3lexlogpow5ineq1  42507  3lexlogpow5ineq5  42513  aks4d1p1p4  42524  aks4d1p1p6  42526  aks4d1p1p7  42527  sqn5i  42731  4t5e20  42737  sq5  42740  235t711  42751  ex-decpmul  42752  inductionexd  44600  goldrasin  47344  ceil5half3  47806  fmtno5lem1  48028  fmtno5lem2  48029  257prm  48036  fmtno4prmfac193  48048  fmtno4nprmfac193  48049  flsqrt5  48069  139prmALT  48071  127prm  48074  5tcu2e40  48090  41prothprmlem2  48093  41prothprm  48094  2exp340mod341  48221  gbpart8  48256  gpg5order  48548  linevalexample  48883  ackval3012  49180  5m4e1  50284