Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > 6cn | GIF version |
Description: The number 6 is complex. (Contributed by David A. Wheeler, 8-Dec-2018.) |
Ref | Expression |
---|---|
6cn | ⊢ 6 ∈ ℂ |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 6re 8959 | . 2 ⊢ 6 ∈ ℝ | |
2 | 1 | recni 7932 | 1 ⊢ 6 ∈ ℂ |
Colors of variables: wff set class |
Syntax hints: ∈ wcel 2141 ℂcc 7772 6c6 8933 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-5 1440 ax-7 1441 ax-gen 1442 ax-ie1 1486 ax-ie2 1487 ax-8 1497 ax-11 1499 ax-4 1503 ax-17 1519 ax-i9 1523 ax-ial 1527 ax-i5r 1528 ax-ext 2152 ax-resscn 7866 ax-1re 7868 ax-addrcl 7871 |
This theorem depends on definitions: df-bi 116 df-nf 1454 df-sb 1756 df-clab 2157 df-cleq 2163 df-clel 2166 df-in 3127 df-ss 3134 df-2 8937 df-3 8938 df-4 8939 df-5 8940 df-6 8941 |
This theorem is referenced by: 7m1e6 9002 6p2e8 9027 6p3e9 9028 halfpm6th 9098 6p4e10 9414 6t2e12 9446 6t3e18 9447 6t5e30 9449 5recm6rec 9486 efi4p 11680 ef01bndlem 11719 cos01bnd 11721 3lcm2e6woprm 12040 6lcm4e12 12041 sincos6thpi 13557 sincos3rdpi 13558 ex-exp 13762 ex-bc 13764 ex-gcd 13766 |
Copyright terms: Public domain | W3C validator |