![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > 8cn | GIF version |
Description: The number 8 is complex. (Contributed by David A. Wheeler, 8-Dec-2018.) |
Ref | Expression |
---|---|
8cn | ⊢ 8 ∈ ℂ |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 8re 8993 | . 2 ⊢ 8 ∈ ℝ | |
2 | 1 | recni 7960 | 1 ⊢ 8 ∈ ℂ |
Colors of variables: wff set class |
Syntax hints: ∈ wcel 2148 ℂcc 7800 8c8 8965 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-5 1447 ax-7 1448 ax-gen 1449 ax-ie1 1493 ax-ie2 1494 ax-8 1504 ax-11 1506 ax-4 1510 ax-17 1526 ax-i9 1530 ax-ial 1534 ax-i5r 1535 ax-ext 2159 ax-resscn 7894 ax-1re 7896 ax-addrcl 7899 |
This theorem depends on definitions: df-bi 117 df-nf 1461 df-sb 1763 df-clab 2164 df-cleq 2170 df-clel 2173 df-in 3135 df-ss 3142 df-2 8967 df-3 8968 df-4 8969 df-5 8970 df-6 8971 df-7 8972 df-8 8973 |
This theorem is referenced by: 9m1e8 9034 8p2e10 9452 8t2e16 9487 8t5e40 9490 cos2bnd 11752 lgsdir2lem1 14096 lgsdir2lem5 14100 ex-exp 14135 |
Copyright terms: Public domain | W3C validator |