Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > 2cn | Unicode version |
Description: The number 2 is a complex number. (Contributed by NM, 30-Jul-2004.) |
Ref | Expression |
---|---|
2cn |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 2re 8783 | . 2 | |
2 | 1 | recni 7771 | 1 |
Colors of variables: wff set class |
Syntax hints: wcel 1480 cc 7611 c2 8764 |
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 |
This theorem is referenced by: 2ex 8785 2cnd 8786 2m1e1 8831 3m1e2 8833 2p2e4 8840 times2 8842 2div2e1 8845 1p2e3 8847 3p3e6 8855 4p3e7 8857 5p3e8 8860 6p3e9 8863 2t1e2 8866 2t2e4 8867 3t3e9 8870 2t0e0 8872 4d2e2 8873 2cnne0 8922 1mhlfehlf 8931 8th4div3 8932 halfpm6th 8933 2mulicn 8935 2muliap0 8937 halfcl 8939 half0 8941 2halves 8942 halfaddsub 8947 div4p1lem1div2 8966 3halfnz 9141 zneo 9145 nneoor 9146 zeo 9149 7p3e10 9249 4t4e16 9273 6t3e18 9279 7t7e49 9288 8t5e40 9292 9t9e81 9303 decbin0 9314 decbin2 9315 halfthird 9317 fztpval 9856 fz0tp 9894 fzo0to3tp 9989 2tnp1ge0ge0 10067 expubnd 10343 sq2 10381 sq4e2t8 10383 cu2 10384 subsq2 10393 binom2sub 10398 binom3 10402 zesq 10403 fac2 10470 fac3 10471 faclbnd2 10481 bcn2 10503 4bc2eq6 10513 crre 10622 addcj 10656 imval2 10659 resqrexlemover 10775 resqrexlemcalc1 10779 resqrexlemnm 10783 resqrexlemcvg 10784 amgm2 10883 arisum 11260 arisum2 11261 geo2sum2 11277 geo2lim 11278 geoihalfsum 11284 efcllemp 11353 ege2le3 11366 tanval2ap 11409 tanval3ap 11410 efi4p 11413 efival 11428 sinadd 11432 cosadd 11433 sinmul 11440 cosmul 11441 cos2tsin 11447 ef01bndlem 11452 sin01bnd 11453 cos01bnd 11454 cos1bnd 11455 cos2bnd 11456 cos01gt0 11458 sin02gt0 11459 sin4lt0 11462 cos12dec 11463 egt2lt3 11475 odd2np1lem 11558 odd2np1 11559 ltoddhalfle 11579 halfleoddlt 11580 opoe 11581 omoe 11582 opeo 11583 omeo 11584 nno 11592 nn0o 11593 flodddiv4 11620 6gcd4e2 11672 3lcm2e6woprm 11756 6lcm4e12 11757 sqrt2irrlem 11828 oddpwdclemodd 11839 coscn 12848 sinhalfpilem 12861 cospi 12870 ef2pi 12875 ef2kpi 12876 efper 12877 sinperlem 12878 sin2kpi 12881 cos2kpi 12882 sin2pim 12883 cos2pim 12884 ptolemy 12894 sincosq3sgn 12898 sincosq4sgn 12899 sinq12gt0 12900 cosq23lt0 12903 coseq00topi 12905 tangtx 12908 sincos4thpi 12910 sincos6thpi 12912 sincos3rdpi 12913 pigt3 12914 abssinper 12916 coskpi 12918 cosq34lt1 12920 ex-fl 12926 ex-ceil 12927 ex-exp 12928 ex-fac 12929 |
Copyright terms: Public domain | W3C validator |