![]() |
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 8991 | . 2 ⊢ 2 ∈ ℝ | |
2 | 1 | recni 7971 | 1 ⊢ 2 ∈ ℂ |
Colors of variables: wff set class |
Syntax hints: ∈ wcel 2148 ℂcc 7811 2c2 8972 |
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 7905 ax-1re 7907 ax-addrcl 7910 |
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 3137 df-ss 3144 df-2 8980 |
This theorem is referenced by: 2ex 8993 2cnd 8994 2m1e1 9039 3m1e2 9041 2p2e4 9048 times2 9050 2div2e1 9053 1p2e3 9055 3p3e6 9063 4p3e7 9065 5p3e8 9068 6p3e9 9071 2t1e2 9074 2t2e4 9075 3t3e9 9078 2t0e0 9080 4d2e2 9081 2cnne0 9130 1mhlfehlf 9139 8th4div3 9140 halfpm6th 9141 2mulicn 9143 2muliap0 9145 halfcl 9147 half0 9149 2halves 9150 halfaddsub 9155 div4p1lem1div2 9174 3halfnz 9352 zneo 9356 nneoor 9357 zeo 9360 7p3e10 9460 4t4e16 9484 6t3e18 9490 7t7e49 9499 8t5e40 9503 9t9e81 9514 decbin0 9525 decbin2 9526 halfthird 9528 fztpval 10085 fz0tp 10124 fz0to4untppr 10126 fzo0to3tp 10221 2tnp1ge0ge0 10303 expubnd 10579 sq2 10618 sq4e2t8 10620 cu2 10621 subsq2 10630 binom2sub 10636 binom3 10640 zesq 10641 fac2 10713 fac3 10714 faclbnd2 10724 bcn2 10746 4bc2eq6 10756 crre 10868 addcj 10902 imval2 10905 resqrexlemover 11021 resqrexlemcalc1 11025 resqrexlemnm 11029 resqrexlemcvg 11030 amgm2 11129 arisum 11508 arisum2 11509 geo2sum2 11525 geo2lim 11526 geoihalfsum 11532 efcllemp 11668 ege2le3 11681 tanval2ap 11723 tanval3ap 11724 efi4p 11727 efival 11742 sinadd 11746 cosadd 11747 sinmul 11754 cosmul 11755 cos2tsin 11761 ef01bndlem 11766 sin01bnd 11767 cos01bnd 11768 cos1bnd 11769 cos2bnd 11770 cos01gt0 11772 sin02gt0 11773 sin4lt0 11776 cos12dec 11777 egt2lt3 11789 odd2np1lem 11879 odd2np1 11880 ltoddhalfle 11900 halfleoddlt 11901 opoe 11902 omoe 11903 opeo 11904 omeo 11905 nno 11913 nn0o 11914 flodddiv4 11941 6gcd4e2 11998 3lcm2e6woprm 12088 6lcm4e12 12089 sqrt2irrlem 12163 oddpwdclemodd 12174 pythagtriplem1 12267 pythagtriplem12 12277 pythagtriplem14 12279 coscn 14276 sinhalfpilem 14297 cospi 14306 ef2pi 14311 ef2kpi 14312 efper 14313 sinperlem 14314 sin2kpi 14317 cos2kpi 14318 sin2pim 14319 cos2pim 14320 ptolemy 14330 sincosq3sgn 14334 sincosq4sgn 14335 sinq12gt0 14336 cosq23lt0 14339 coseq00topi 14341 tangtx 14344 sincos4thpi 14346 sincos6thpi 14348 sincos3rdpi 14349 pigt3 14350 abssinper 14352 coskpi 14354 cosq34lt1 14356 logsqrt 14428 2logb9irrALT 14477 lgsdir2lem2 14515 m1lgs 14537 2lgsoddprmlem2 14539 2lgsoddprmlem3c 14542 2lgsoddprmlem3d 14543 ex-fl 14562 ex-ceil 14563 ex-exp 14564 ex-fac 14565 |
Copyright terms: Public domain | W3C validator |