Theorem 5cn 12333

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 12310	. 2 ⊢ 5 = (4 + 1)
2		4cn 12330	. . 3 ⊢ 4 ∈ ℂ
3		ax-1cn 11162	. . 3 ⊢ 1 ∈ ℂ
4	2, 3	addcli 11219	. 2 ⊢ (4 + 1) ∈ ℂ
5	1, 4	eqeltri 2859	1 ⊢ 5 ∈ ℂ

This proof depends on syntax axioms:   ∈ wcel 2143  (class class class)co 7410  ℂcc 11102  1c1 11105   + caddc 11107  4c4 12301  5c5 12302

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735  ax-1cn 11162  ax-addcl 11164

This proof depends on definitions:  df-bi 210  df-an 401  df-ex 1810  df-cleq 2755  df-clel 2838  df-2 12307  df-3 12308  df-4 12309  df-5 12310

This theorem is used by:  6cn  12336  6m1e5  12375  5p2e7  12400  5p3e8  12401  5p4e9  12402  5p5e10  12791  5t2e10  12820  5recm6rec  12865  bpoly4  16117  ef01bndlem  16244  5ndvds3  16475  5ndvds6  16476  dec5dvds  17128  dec5nprm  17130  2exp11  17153  2exp16  17154  prmlem1  17171  17prm  17181  139prm  17188  163prm  17189  317prm  17190  631prm  17191  1259lem1  17195  1259lem2  17196  1259lem3  17197  1259lem4  17198  2503lem1  17201  2503lem2  17202  2503lem3  17203  4001lem1  17205  4001lem2  17206  4001lem3  17207  4001lem4  17208  4001prm  17209  log2ublem3  27122  log2ub  27123  ppiub  27377  bclbnd  27453  bposlem4  27460  bposlem5  27461  bposlem6  27462  bposlem8  27464  bposlem9  27465  lgsdir2lem1  27498  2lgslem3c  27571  2lgsoddprmlem3d  27586  ex-fac  30811  fib6  34805  hgt750lem2  35048  12lcm5e60  42803  lcmineqlem23  42846  3lexlogpow5ineq1  42849  3lexlogpow5ineq5  42855  aks4d1p1p4  42866  aks4d1p1p6  42868  aks4d1p1p7  42869  25or6to4  43001  sqn5i  43074  4t5e20  43080  sq5  43083  235t711  43094  ex-decpmul  43095  inductionexd  44909  cos5t  47644  goldrasin  47647  goldracos5teq  47650  goldratmolem2  47651  ceil5half3  48111  fmtno5lem1  48333  fmtno5lem2  48334  257prm  48341  fmtno4prmfac193  48353  fmtno4nprmfac193  48354  flsqrt5  48374  139prmALT  48376  127prm  48379  5tcu2e40  48395  41prothprmlem2  48398  41prothprm  48399  2exp340mod341  48526  gbpart8  48561  gpg5order  48853  linevalexample  49203  ackval3012  49500  5m4e1  50645