MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  5cn Structured version   Visualization version   GIF version

Theorem 5cn 11713
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
StepHypRef Expression
1 df-5 11691 . 2 5 = (4 + 1)
2 4cn 11710 . . 3 4 ∈ ℂ
3 ax-1cn 10584 . . 3 1 ∈ ℂ
42, 3addcli 10636 . 2 (4 + 1) ∈ ℂ
51, 4eqeltri 2910 1 5 ∈ ℂ
Colors of variables: wff setvar class
Syntax hints:  wcel 2114  (class class class)co 7140  cc 10524  1c1 10527   + caddc 10529  4c4 11682  5c5 11683
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-ext 2794  ax-1cn 10584  ax-addcl 10586
This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-cleq 2815  df-clel 2894  df-2 11688  df-3 11689  df-4 11690  df-5 11691
This theorem is referenced by:  6cn  11716  6m1e5  11756  5p2e7  11781  5p3e8  11782  5p4e9  11783  5p5e10  12157  5t2e10  12186  5recm6rec  12230  bpoly4  15404  ef01bndlem  15528  dec5dvds  16389  dec5nprm  16391  2exp16  16415  prmlem1  16432  17prm  16441  139prm  16448  163prm  16449  317prm  16450  631prm  16451  1259lem1  16455  1259lem2  16456  1259lem3  16457  1259lem4  16458  2503lem1  16461  2503lem2  16462  2503lem3  16463  4001lem1  16465  4001lem2  16466  4001lem3  16467  4001lem4  16468  4001prm  16469  log2ublem3  25532  log2ub  25533  ppiub  25786  bclbnd  25862  bposlem4  25869  bposlem5  25870  bposlem6  25871  bposlem8  25873  bposlem9  25874  lgsdir2lem1  25907  2lgslem3c  25980  2lgsoddprmlem3d  25995  ex-fac  28234  fib6  31738  hgt750lem2  31997  12lcm5e60  39261  lcmineqlem23  39304  sqn5i  39427  235t711  39433  ex-decpmul  39434  inductionexd  40795  fmtno5lem1  44013  fmtno5lem2  44014  257prm  44021  fmtno4prmfac193  44033  fmtno4nprmfac193  44034  flsqrt5  44054  139prmALT  44056  127prm  44059  2exp11  44061  5tcu2e40  44076  41prothprmlem2  44079  41prothprm  44080  2exp340mod341  44194  gbpart8  44229  linevalexample  44747  ackval3012  45049  5m4e1  45268
  Copyright terms: Public domain W3C validator