Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > 5cn | Structured version Visualization version GIF version |
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.) |
Ref | Expression |
---|---|
5cn | ⊢ 5 ∈ ℂ |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-5 11692 | . 2 ⊢ 5 = (4 + 1) | |
2 | 4cn 11711 | . . 3 ⊢ 4 ∈ ℂ | |
3 | ax-1cn 10584 | . . 3 ⊢ 1 ∈ ℂ | |
4 | 2, 3 | addcli 10636 | . 2 ⊢ (4 + 1) ∈ ℂ |
5 | 1, 4 | eqeltri 2909 | 1 ⊢ 5 ∈ ℂ |
Colors of variables: wff setvar class |
Syntax hints: ∈ wcel 2105 (class class class)co 7145 ℂcc 10524 1c1 10527 + caddc 10529 4c4 11683 5c5 11684 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1787 ax-4 1801 ax-5 1902 ax-6 1961 ax-7 2006 ax-8 2107 ax-9 2115 ax-ext 2793 ax-1cn 10584 ax-addcl 10586 |
This theorem depends on definitions: df-bi 208 df-an 397 df-ex 1772 df-cleq 2814 df-clel 2893 df-2 11689 df-3 11690 df-4 11691 df-5 11692 |
This theorem is referenced by: 6cn 11717 6m1e5 11757 5p2e7 11782 5p3e8 11783 5p4e9 11784 5p5e10 12158 5t2e10 12187 5recm6rec 12231 bpoly4 15403 ef01bndlem 15527 dec5dvds 16390 dec5nprm 16392 2exp16 16414 prmlem1 16431 17prm 16440 139prm 16447 163prm 16448 317prm 16449 631prm 16450 1259lem1 16454 1259lem2 16455 1259lem3 16456 1259lem4 16457 2503lem1 16460 2503lem2 16461 2503lem3 16462 4001lem1 16464 4001lem2 16465 4001lem3 16466 4001lem4 16467 4001prm 16468 log2ublem3 25454 log2ub 25455 ppiub 25708 bclbnd 25784 bposlem4 25791 bposlem5 25792 bposlem6 25793 bposlem8 25795 bposlem9 25796 lgsdir2lem1 25829 2lgslem3c 25902 2lgsoddprmlem3d 25917 ex-fac 28158 fib6 31564 hgt750lem2 31823 sqn5i 39051 235t711 39057 ex-decpmul 39058 inductionexd 40385 fmtno5lem1 43562 fmtno5lem2 43563 257prm 43570 fmtno4prmfac193 43582 fmtno4nprmfac193 43583 flsqrt5 43604 139prmALT 43606 127prm 43610 2exp11 43612 5tcu2e40 43627 41prothprmlem2 43630 41prothprm 43631 2exp340mod341 43745 gbpart8 43780 linevalexample 44348 5m4e1 44796 |
Copyright terms: Public domain | W3C validator |