Theorem 5cn 12434

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 12411	. 2 ⊢ 5 = (4 + 1)
2		4cn 12431	. . 3 ⊢ 4 ∈ ℂ
3		ax-1cn 11261	. . 3 ⊢ 1 ∈ ℂ
4	2, 3	addcli 11318	. 2 ⊢ (4 + 1) ∈ ℂ
5	1, 4	eqeltri 2856	1 ⊢ 5 ∈ ℂ

This proof depends on syntax axioms:   ∈ wcel 2144  (class class class)co 7420  ℂcc 11201  1c1 11204   + caddc 11206  4c4 12402  5c5 12403

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732  ax-1cn 11261  ax-addcl 11263

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-cleq 2752  df-clel 2835  df-2 12408  df-3 12409  df-4 12410  df-5 12411

This theorem is used by:  6cn  12437  6m1e5  12476  5p2e7  12501  5p3e8  12502  5p4e9  12503  5p5e10  12893  5t2e10  12922  5recm6rec  12967  bpoly4  16230  ef01bndlem  16357  5ndvds3  16588  5ndvds6  16589  dec5dvds  17247  dec5nprm  17249  2exp11  17272  2exp16  17273  prmlem1  17290  17prm  17300  139prm  17307  163prm  17308  317prm  17309  631prm  17310  1259lem1  17314  1259lem2  17315  1259lem3  17316  1259lem4  17317  2503lem1  17320  2503lem2  17321  2503lem3  17322  4001lem1  17324  4001lem2  17325  4001lem3  17326  4001lem4  17327  4001prm  17328  log2ublem3  27281  log2ub  27282  ppiub  27536  bclbnd  27612  bposlem4  27619  bposlem5  27620  bposlem6  27621  bposlem8  27623  bposlem9  27624  lgsdir2lem1  27657  2lgslem3c  27730  2lgsoddprmlem3d  27745  ex-fac  31057  fib6  35084  hgt750lem2  35327  12lcm5e60  43151  lcmineqlem23  43194  3lexlogpow5ineq1  43197  3lexlogpow5ineq5  43203  aks4d1p1p4  43214  aks4d1p1p6  43216  aks4d1p1p7  43217  25or6to4  43349  1p6e7  43406  2p7e9  43413  sqn5i  43435  4t5e20  43441  sq5  43444  235t711  43455  ex-decpmul  43456  inductionexd  45248  cos5t  48018  goldrasin  48022  goldracos5teq  48025  goldratmolem2  48026  goldratmolem3  48027  ceil5half3  48509  fmtno5lem1  48731  fmtno5lem2  48732  257prm  48739  fmtno4prmfac193  48751  fmtno4nprmfac193  48752  flsqrt5  48772  139prmALT  48774  127prm  48777  5tcu2e40  48793  41prothprmlem2  48796  41prothprm  48797  2exp340mod341  48924  gbpart8  48959  gpg5order  49251  linevalexample  49600  ackval3012  49897  5m4e1  51103