Theorem 5cn 12274

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 12252	. 2 ⊢ 5 = (4 + 1)
2		4cn 12271	. . 3 ⊢ 4 ∈ ℂ
3		ax-1cn 11126	. . 3 ⊢ 1 ∈ ℂ
4	2, 3	addcli 11180	. 2 ⊢ (4 + 1) ∈ ℂ
5	1, 4	eqeltri 2824	1 ⊢ 5 ∈ ℂ

Syntax hints:   ∈ wcel 2109  (class class class)co 7387  ℂcc 11066  1c1 11069   + caddc 11071  4c4 12243  5c5 12244

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-1cn 11126  ax-addcl 11128

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2721  df-clel 2803  df-2 12249  df-3 12250  df-4 12251  df-5 12252

This theorem is referenced by:  6cn  12277  6m1e5  12312  5p2e7  12337  5p3e8  12338  5p4e9  12339  5p5e10  12720  5t2e10  12749  5recm6rec  12792  bpoly4  16025  ef01bndlem  16152  5ndvds3  16383  5ndvds6  16384  dec5dvds  17035  dec5nprm  17037  2exp11  17060  2exp16  17061  prmlem1  17078  17prm  17087  139prm  17094  163prm  17095  317prm  17096  631prm  17097  1259lem1  17101  1259lem2  17102  1259lem3  17103  1259lem4  17104  2503lem1  17107  2503lem2  17108  2503lem3  17109  4001lem1  17111  4001lem2  17112  4001lem3  17113  4001lem4  17114  4001prm  17115  log2ublem3  26858  log2ub  26859  ppiub  27115  bclbnd  27191  bposlem4  27198  bposlem5  27199  bposlem6  27200  bposlem8  27202  bposlem9  27203  lgsdir2lem1  27236  2lgslem3c  27309  2lgsoddprmlem3d  27324  ex-fac  30380  fib6  34397  hgt750lem2  34643  12lcm5e60  41996  lcmineqlem23  42039  3lexlogpow5ineq1  42042  3lexlogpow5ineq5  42048  aks4d1p1p4  42059  aks4d1p1p6  42061  aks4d1p1p7  42062  sqn5i  42273  4t5e20  42279  sq5  42282  235t711  42293  ex-decpmul  42294  inductionexd  44144  ceil5half3  47341  fmtno5lem1  47554  fmtno5lem2  47555  257prm  47562  fmtno4prmfac193  47574  fmtno4nprmfac193  47575  flsqrt5  47595  139prmALT  47597  127prm  47600  5tcu2e40  47616  41prothprmlem2  47619  41prothprm  47620  2exp340mod341  47734  gbpart8  47769  gpg5order  48051  linevalexample  48384  ackval3012  48681  5m4e1  49786