Theorem 5cn 12357

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 12334	. 2 ⊢ 5 = (4 + 1)
2		4cn 12354	. . 3 ⊢ 4 ∈ ℂ
3		ax-1cn 11186	. . 3 ⊢ 1 ∈ ℂ
4	2, 3	addcli 11243	. 2 ⊢ (4 + 1) ∈ ℂ
5	1, 4	eqeltri 2858	1 ⊢ 5 ∈ ℂ

This proof depends on syntax axioms:   ∈ wcel 2145  (class class class)co 7417  ℂcc 11126  1c1 11129   + caddc 11131  4c4 12325  5c5 12326

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 2734  ax-1cn 11186  ax-addcl 11188

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2754  df-clel 2837  df-2 12331  df-3 12332  df-4 12333  df-5 12334

This theorem is used by:  6cn  12360  6m1e5  12399  5p2e7  12424  5p3e8  12425  5p4e9  12426  5p5e10  12816  5t2e10  12845  5recm6rec  12890  bpoly4  16151  ef01bndlem  16278  5ndvds3  16509  5ndvds6  16510  dec5dvds  17162  dec5nprm  17164  2exp11  17187  2exp16  17188  prmlem1  17205  17prm  17215  139prm  17222  163prm  17223  317prm  17224  631prm  17225  1259lem1  17229  1259lem2  17230  1259lem3  17231  1259lem4  17232  2503lem1  17235  2503lem2  17236  2503lem3  17237  4001lem1  17239  4001lem2  17240  4001lem3  17241  4001lem4  17242  4001prm  17243  log2ublem3  27193  log2ub  27194  ppiub  27448  bclbnd  27524  bposlem4  27531  bposlem5  27532  bposlem6  27533  bposlem8  27535  bposlem9  27536  lgsdir2lem1  27569  2lgslem3c  27642  2lgsoddprmlem3d  27657  ex-fac  30939  fib6  34925  hgt750lem2  35168  12lcm5e60  42882  lcmineqlem23  42925  3lexlogpow5ineq1  42928  3lexlogpow5ineq5  42934  aks4d1p1p4  42945  aks4d1p1p6  42947  aks4d1p1p7  42948  25or6to4  43080  1p6e7  43137  2p7e9  43144  sqn5i  43168  4t5e20  43174  sq5  43177  235t711  43188  ex-decpmul  43189  inductionexd  45003  cos5t  47751  goldrasin  47755  goldracos5teq  47758  goldratmolem2  47759  goldratmolem3  47760  ceil5half3  48242  fmtno5lem1  48464  fmtno5lem2  48465  257prm  48472  fmtno4prmfac193  48484  fmtno4nprmfac193  48485  flsqrt5  48505  139prmALT  48507  127prm  48510  5tcu2e40  48526  41prothprmlem2  48529  41prothprm  48530  2exp340mod341  48657  gbpart8  48692  gpg5order  48984  linevalexample  49333  ackval3012  49630  5m4e1  50776