Theorem 5cn 12325

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 12303	. 2 ⊢ 5 = (4 + 1)
2		4cn 12322	. . 3 ⊢ 4 ∈ ℂ
3		ax-1cn 11191	. . 3 ⊢ 1 ∈ ℂ
4	2, 3	addcli 11245	. 2 ⊢ (4 + 1) ∈ ℂ
5	1, 4	eqeltri 2825	1 ⊢ 5 ∈ ℂ

Syntax hints:   ∈ wcel 2099  (class class class)co 7415  ℂcc 11131  1c1 11134   + caddc 11136  4c4 12294  5c5 12295

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2699  ax-1cn 11191  ax-addcl 11193

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1775  df-cleq 2720  df-clel 2806  df-2 12300  df-3 12301  df-4 12302  df-5 12303

This theorem is referenced by:  6cn  12328  6m1e5  12368  5p2e7  12393  5p3e8  12394  5p4e9  12395  5p5e10  12773  5t2e10  12802  5recm6rec  12846  bpoly4  16030  ef01bndlem  16155  dec5dvds  17027  dec5nprm  17029  2exp11  17053  2exp16  17054  prmlem1  17071  17prm  17080  139prm  17087  163prm  17088  317prm  17089  631prm  17090  1259lem1  17094  1259lem2  17095  1259lem3  17096  1259lem4  17097  2503lem1  17100  2503lem2  17101  2503lem3  17102  4001lem1  17104  4001lem2  17105  4001lem3  17106  4001lem4  17107  4001prm  17108  log2ublem3  26874  log2ub  26875  ppiub  27131  bclbnd  27207  bposlem4  27214  bposlem5  27215  bposlem6  27216  bposlem8  27218  bposlem9  27219  lgsdir2lem1  27252  2lgslem3c  27325  2lgsoddprmlem3d  27340  ex-fac  30255  fib6  34021  hgt750lem2  34279  12lcm5e60  41474  lcmineqlem23  41517  3lexlogpow5ineq1  41520  3lexlogpow5ineq5  41526  aks4d1p1p4  41537  aks4d1p1p6  41539  aks4d1p1p7  41540  sqn5i  41850  4t5e20  41856  235t711  41858  ex-decpmul  41859  inductionexd  43576  fmtno5lem1  46884  fmtno5lem2  46885  257prm  46892  fmtno4prmfac193  46904  fmtno4nprmfac193  46905  flsqrt5  46925  139prmALT  46927  127prm  46930  5tcu2e40  46946  41prothprmlem2  46949  41prothprm  46950  2exp340mod341  47064  gbpart8  47099  linevalexample  47454  ackval3012  47756  5m4e1  48221

Otomatik - 173.255.232.114 CloudFlare DNS Türk Telekom DNS Google DNS Open DNS

OSZAR »