Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > 3cn | GIF version |
Description: The number 3 is a complex number. (Contributed by FL, 17-Oct-2010.) |
Ref | Expression |
---|---|
3cn | ⊢ 3 ∈ ℂ |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 3re 8787 | . 2 ⊢ 3 ∈ ℝ | |
2 | 1 | recni 7771 | 1 ⊢ 3 ∈ ℂ |
Colors of variables: wff set class |
Syntax hints: ∈ wcel 1480 ℂcc 7611 3c3 8765 |
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 |
This theorem is referenced by: 3ex 8789 3m1e2 8833 4m1e3 8834 3p2e5 8854 3p3e6 8855 4p4e8 8858 5p4e9 8861 3t1e3 8868 3t2e6 8869 3t3e9 8870 8th4div3 8932 halfpm6th 8933 6p4e10 9246 9t8e72 9302 halfthird 9317 fzo0to42pr 9990 sq3 10382 expnass 10391 fac3 10471 4bc3eq4 10512 ef01bndlem 11452 sin01bnd 11453 cos01bnd 11454 cos1bnd 11455 cos2bnd 11456 cos01gt0 11458 3dvdsdec 11551 3dvds2dec 11552 3lcm2e6woprm 11756 cosq23lt0 12903 tangtx 12908 sincos6thpi 12912 sincos3rdpi 12913 pigt3 12914 ex-exp 12928 ex-dvds 12931 ex-gcd 12932 |
Copyright terms: Public domain | W3C validator |