![]() |
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 11441 | . 2 ⊢ 5 = (4 + 1) | |
2 | 4cn 11461 | . . 3 ⊢ 4 ∈ ℂ | |
3 | ax-1cn 10330 | . . 3 ⊢ 1 ∈ ℂ | |
4 | 2, 3 | addcli 10383 | . 2 ⊢ (4 + 1) ∈ ℂ |
5 | 1, 4 | eqeltri 2855 | 1 ⊢ 5 ∈ ℂ |
Colors of variables: wff setvar class |
Syntax hints: ∈ wcel 2107 (class class class)co 6922 ℂcc 10270 1c1 10273 + caddc 10275 4c4 11432 5c5 11433 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1839 ax-4 1853 ax-5 1953 ax-6 2021 ax-7 2055 ax-9 2116 ax-ext 2754 ax-1cn 10330 ax-addcl 10332 |
This theorem depends on definitions: df-bi 199 df-an 387 df-ex 1824 df-cleq 2770 df-clel 2774 df-2 11438 df-3 11439 df-4 11440 df-5 11441 |
This theorem is referenced by: 6cn 11469 6m1e5 11513 5p2e7 11538 5p3e8 11539 5p4e9 11540 5p5e10 11918 5t2e10 11947 5recm6rec 11991 bpoly4 15192 ef01bndlem 15316 dec5dvds 16172 dec5nprm 16174 2exp16 16196 prmlem1 16213 17prm 16222 139prm 16229 163prm 16230 317prm 16231 631prm 16232 1259lem1 16236 1259lem2 16237 1259lem3 16238 1259lem4 16239 2503lem1 16242 2503lem2 16243 2503lem3 16244 4001lem1 16246 4001lem2 16247 4001lem3 16248 4001lem4 16249 4001prm 16250 log2ublem3 25127 log2ub 25128 ppiublem2 25380 ppiub 25381 bclbnd 25457 bposlem4 25464 bposlem5 25465 bposlem6 25466 bposlem8 25468 bposlem9 25469 lgsdir2lem1 25502 2lgslem3c 25575 2lgsoddprmlem3d 25590 ex-fac 27883 fib6 31067 hgt750lem2 31332 sqn5i 38153 235t711 38159 ex-decpmul 38160 inductionexd 39413 fmtno5lem1 42490 fmtno5lem2 42491 257prm 42498 fmtno4prmfac193 42510 fmtno4nprmfac193 42511 flsqrt5 42534 139prmALT 42536 127prm 42540 2exp11 42542 5tcu2e40 42557 41prothprmlem2 42560 41prothprm 42561 gbpart8 42685 linevalexample 43203 5m4e1 43653 |
Copyright terms: Public domain | W3C validator |