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 8794 | . 2 ⊢ 6 ∈ ℝ | |
2 | 1 | recni 7771 | 1 ⊢ 6 ∈ ℂ |
Colors of variables: wff set class |
Syntax hints: ∈ wcel 1480 ℂcc 7611 6c6 8768 |
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 1423 ax-7 1424 ax-gen 1425 ax-ie1 1469 ax-ie2 1470 ax-8 1482 ax-11 1484 ax-4 1487 ax-17 1506 ax-i9 1510 ax-ial 1514 ax-i5r 1515 ax-ext 2119 ax-resscn 7705 ax-1re 7707 ax-addrcl 7710 |
This theorem depends on definitions: df-bi 116 df-nf 1437 df-sb 1736 df-clab 2124 df-cleq 2130 df-clel 2133 df-in 3072 df-ss 3079 df-2 8772 df-3 8773 df-4 8774 df-5 8775 df-6 8776 |
This theorem is referenced by: 7m1e6 8837 6p2e8 8862 6p3e9 8863 halfpm6th 8933 6p4e10 9246 6t2e12 9278 6t3e18 9279 6t5e30 9281 5recm6rec 9318 efi4p 11413 ef01bndlem 11452 cos01bnd 11454 3lcm2e6woprm 11756 6lcm4e12 11757 sincos6thpi 12912 sincos3rdpi 12913 ex-exp 12928 ex-bc 12930 ex-gcd 12932 |
Copyright terms: Public domain | W3C validator |