Theorem 5cn 12412

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 12389	. 2 ⊢ 5 = (4 + 1)
2		4cn 12409	. . 3 ⊢ 4 ∈ ℂ
3		ax-1cn 11239	. . 3 ⊢ 1 ∈ ℂ
4	2, 3	addcli 11296	. 2 ⊢ (4 + 1) ∈ ℂ
5	1, 4	eqeltri 2857	1 ⊢ 5 ∈ ℂ

This proof depends on syntax axioms:   ∈ wcel 2145  (class class class)co 7412  ℂcc 11179  1c1 11182   + caddc 11184  4c4 12380  5c5 12381

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733  ax-1cn 11239  ax-addcl 11241

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2753  df-clel 2836  df-2 12386  df-3 12387  df-4 12388  df-5 12389

This theorem is used by:  6cn  12415  6m1e5  12454  5p2e7  12479  5p3e8  12480  5p4e9  12481  5p5e10  12871  5t2e10  12900  5recm6rec  12945  bpoly4  16205  ef01bndlem  16332  5ndvds3  16563  5ndvds6  16564  dec5dvds  17222  dec5nprm  17224  2exp11  17247  2exp16  17248  prmlem1  17265  17prm  17275  139prm  17282  163prm  17283  317prm  17284  631prm  17285  1259lem1  17289  1259lem2  17290  1259lem3  17291  1259lem4  17292  2503lem1  17295  2503lem2  17296  2503lem3  17297  4001lem1  17299  4001lem2  17300  4001lem3  17301  4001lem4  17302  4001prm  17303  log2ublem3  27258  log2ub  27259  ppiub  27513  bclbnd  27589  bposlem4  27596  bposlem5  27597  bposlem6  27598  bposlem8  27600  bposlem9  27601  lgsdir2lem1  27634  2lgslem3c  27707  2lgsoddprmlem3d  27722  ex-fac  31034  fib6  35021  hgt750lem2  35264  12lcm5e60  43026  lcmineqlem23  43069  3lexlogpow5ineq1  43072  3lexlogpow5ineq5  43078  aks4d1p1p4  43089  aks4d1p1p6  43091  aks4d1p1p7  43092  25or6to4  43224  1p6e7  43281  2p7e9  43288  sqn5i  43310  4t5e20  43316  sq5  43319  235t711  43330  ex-decpmul  43331  inductionexd  45114  cos5t  47869  goldrasin  47873  goldracos5teq  47876  goldratmolem2  47877  goldratmolem3  47878  ceil5half3  48360  fmtno5lem1  48582  fmtno5lem2  48583  257prm  48590  fmtno4prmfac193  48602  fmtno4nprmfac193  48603  flsqrt5  48623  139prmALT  48625  127prm  48628  5tcu2e40  48644  41prothprmlem2  48647  41prothprm  48648  2exp340mod341  48775  gbpart8  48810  gpg5order  49102  linevalexample  49451  ackval3012  49748  5m4e1  50879