Theorem 5cn 12347

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 12324	. 2 ⊢ 5 = (4 + 1)
2		4cn 12344	. . 3 ⊢ 4 ∈ ℂ
3		ax-1cn 11176	. . 3 ⊢ 1 ∈ ℂ
4	2, 3	addcli 11233	. 2 ⊢ (4 + 1) ∈ ℂ
5	1, 4	eqeltri 2862	1 ⊢ 5 ∈ ℂ

This proof depends on syntax axioms:   ∈ wcel 2146  (class class class)co 7423  ℂcc 11116  1c1 11119   + caddc 11121  4c4 12315  5c5 12316

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 2148  ax-9 2156  ax-ext 2738  ax-1cn 11176  ax-addcl 11178

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2758  df-clel 2841  df-2 12321  df-3 12322  df-4 12323  df-5 12324

This theorem is used by:  6cn  12350  6m1e5  12389  5p2e7  12414  5p3e8  12415  5p4e9  12416  5p5e10  12805  5t2e10  12834  5recm6rec  12879  bpoly4  16138  ef01bndlem  16265  5ndvds3  16496  5ndvds6  16497  dec5dvds  17149  dec5nprm  17151  2exp11  17174  2exp16  17175  prmlem1  17192  17prm  17202  139prm  17209  163prm  17210  317prm  17211  631prm  17212  1259lem1  17216  1259lem2  17217  1259lem3  17218  1259lem4  17219  2503lem1  17222  2503lem2  17223  2503lem3  17224  4001lem1  17226  4001lem2  17227  4001lem3  17228  4001lem4  17229  4001prm  17230  log2ublem3  27150  log2ub  27151  ppiub  27405  bclbnd  27481  bposlem4  27488  bposlem5  27489  bposlem6  27490  bposlem8  27492  bposlem9  27493  lgsdir2lem1  27526  2lgslem3c  27599  2lgsoddprmlem3d  27614  ex-fac  30839  fib6  34828  hgt750lem2  35071  12lcm5e60  42816  lcmineqlem23  42859  3lexlogpow5ineq1  42862  3lexlogpow5ineq5  42868  aks4d1p1p4  42879  aks4d1p1p6  42881  aks4d1p1p7  42882  25or6to4  43014  sqn5i  43087  4t5e20  43093  sq5  43096  235t711  43107  ex-decpmul  43108  inductionexd  44922  cos5t  47657  goldrasin  47660  goldracos5teq  47663  goldratmolem2  47664  ceil5half3  48124  fmtno5lem1  48346  fmtno5lem2  48347  257prm  48354  fmtno4prmfac193  48366  fmtno4nprmfac193  48367  flsqrt5  48387  139prmALT  48389  127prm  48392  5tcu2e40  48408  41prothprmlem2  48411  41prothprm  48412  2exp340mod341  48539  gbpart8  48574  gpg5order  48866  linevalexample  49216  ackval3012  49513  5m4e1  50658