![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > 9cn | GIF version |
Description: The number 9 is complex. (Contributed by David A. Wheeler, 8-Dec-2018.) |
Ref | Expression |
---|---|
9cn | ⊢ 9 ∈ ℂ |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 9re 9037 | . 2 ⊢ 9 ∈ ℝ | |
2 | 1 | recni 8000 | 1 ⊢ 9 ∈ ℂ |
Colors of variables: wff set class |
Syntax hints: ∈ wcel 2160 ℂcc 7840 9c9 9008 |
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 1458 ax-7 1459 ax-gen 1460 ax-ie1 1504 ax-ie2 1505 ax-8 1515 ax-11 1517 ax-4 1521 ax-17 1537 ax-i9 1541 ax-ial 1545 ax-i5r 1546 ax-ext 2171 ax-resscn 7934 ax-1re 7936 ax-addrcl 7939 |
This theorem depends on definitions: df-bi 117 df-nf 1472 df-sb 1774 df-clab 2176 df-cleq 2182 df-clel 2185 df-in 3150 df-ss 3157 df-2 9009 df-3 9010 df-4 9011 df-5 9012 df-6 9013 df-7 9014 df-8 9015 df-9 9016 |
This theorem is referenced by: 10m1e9 9510 9t2e18 9536 9t8e72 9542 9t9e81 9543 9t11e99 9544 0.999... 11564 cos2bnd 11803 3dvdsdec 11905 3dvds2dec 11906 |
Copyright terms: Public domain | W3C validator |