![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > 2cn | GIF version |
Description: The number 2 is a complex number. (Contributed by NM, 30-Jul-2004.) |
Ref | Expression |
---|---|
2cn | ⊢ 2 ∈ ℂ |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 2re 8590 | . 2 ⊢ 2 ∈ ℝ | |
2 | 1 | recni 7597 | 1 ⊢ 2 ∈ ℂ |
Colors of variables: wff set class |
Syntax hints: ∈ wcel 1445 ℂcc 7445 2c2 8571 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-5 1388 ax-7 1389 ax-gen 1390 ax-ie1 1434 ax-ie2 1435 ax-8 1447 ax-11 1449 ax-4 1452 ax-17 1471 ax-i9 1475 ax-ial 1479 ax-i5r 1480 ax-ext 2077 ax-resscn 7534 ax-1re 7536 ax-addrcl 7539 |
This theorem depends on definitions: df-bi 116 df-nf 1402 df-sb 1700 df-clab 2082 df-cleq 2088 df-clel 2091 df-in 3019 df-ss 3026 df-2 8579 |
This theorem is referenced by: 2ex 8592 2cnd 8593 2m1e1 8638 3m1e2 8640 2p2e4 8641 times2 8643 2div2e1 8646 1p2e3 8648 3p3e6 8656 4p3e7 8658 5p3e8 8661 6p3e9 8664 2t1e2 8667 2t2e4 8668 3t3e9 8671 2t0e0 8673 4d2e2 8674 2cnne0 8723 1mhlfehlf 8732 8th4div3 8733 halfpm6th 8734 2mulicn 8736 2muliap0 8738 halfcl 8740 half0 8742 2halves 8743 halfaddsub 8748 div4p1lem1div2 8767 3halfnz 8942 zneo 8946 nneoor 8947 zeo 8950 7p3e10 9050 4t4e16 9074 6t3e18 9080 7t7e49 9089 8t5e40 9093 9t9e81 9104 decbin0 9115 decbin2 9116 fztpval 9646 fz0tp 9684 fzo0to3tp 9779 2tnp1ge0ge0 9857 expubnd 10127 sq2 10165 sq4e2t8 10167 cu2 10168 subsq2 10177 binom2sub 10182 binom3 10186 zesq 10187 fac2 10254 fac3 10255 faclbnd2 10265 bcn2 10287 4bc2eq6 10297 crre 10406 addcj 10440 imval2 10443 resqrexlemover 10558 resqrexlemcalc1 10562 resqrexlemnm 10566 resqrexlemcvg 10567 amgm2 10666 arisum 11041 arisum2 11042 geo2sum2 11058 geo2lim 11059 geoihalfsum 11065 efcllemp 11097 ege2le3 11110 tanval2ap 11153 tanval3ap 11154 efi4p 11157 efival 11172 sinadd 11176 cosadd 11177 sinmul 11184 cosmul 11185 cos2tsin 11191 ef01bndlem 11196 sin01bnd 11197 cos01bnd 11198 cos1bnd 11199 cos2bnd 11200 cos01gt0 11202 sin02gt0 11203 sin4lt0 11206 egt2lt3 11216 odd2np1lem 11299 odd2np1 11300 ltoddhalfle 11320 halfleoddlt 11321 opoe 11322 omoe 11323 opeo 11324 omeo 11325 nno 11333 nn0o 11334 flodddiv4 11361 6gcd4e2 11411 3lcm2e6woprm 11495 6lcm4e12 11496 sqrt2irrlem 11567 oddpwdclemodd 11577 ex-fl 12360 ex-ceil 12361 ex-exp 12362 ex-fac 12363 |
Copyright terms: Public domain | W3C validator |