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 8790 | . 2 | |
2 | 1 | recni 7778 | 1 |
Colors of variables: wff set class |
Syntax hints: wcel 1480 cc 7618 c2 8771 |
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 2121 ax-resscn 7712 ax-1re 7714 ax-addrcl 7717 |
This theorem depends on definitions: df-bi 116 df-nf 1437 df-sb 1736 df-clab 2126 df-cleq 2132 df-clel 2135 df-in 3077 df-ss 3084 df-2 8779 |
This theorem is referenced by: 2ex 8792 2cnd 8793 2m1e1 8838 3m1e2 8840 2p2e4 8847 times2 8849 2div2e1 8852 1p2e3 8854 3p3e6 8862 4p3e7 8864 5p3e8 8867 6p3e9 8870 2t1e2 8873 2t2e4 8874 3t3e9 8877 2t0e0 8879 4d2e2 8880 2cnne0 8929 1mhlfehlf 8938 8th4div3 8939 halfpm6th 8940 2mulicn 8942 2muliap0 8944 halfcl 8946 half0 8948 2halves 8949 halfaddsub 8954 div4p1lem1div2 8973 3halfnz 9148 zneo 9152 nneoor 9153 zeo 9156 7p3e10 9256 4t4e16 9280 6t3e18 9286 7t7e49 9295 8t5e40 9299 9t9e81 9310 decbin0 9321 decbin2 9322 halfthird 9324 fztpval 9863 fz0tp 9901 fzo0to3tp 9996 2tnp1ge0ge0 10074 expubnd 10350 sq2 10388 sq4e2t8 10390 cu2 10391 subsq2 10400 binom2sub 10405 binom3 10409 zesq 10410 fac2 10477 fac3 10478 faclbnd2 10488 bcn2 10510 4bc2eq6 10520 crre 10629 addcj 10663 imval2 10666 resqrexlemover 10782 resqrexlemcalc1 10786 resqrexlemnm 10790 resqrexlemcvg 10791 amgm2 10890 arisum 11267 arisum2 11268 geo2sum2 11284 geo2lim 11285 geoihalfsum 11291 efcllemp 11364 ege2le3 11377 tanval2ap 11420 tanval3ap 11421 efi4p 11424 efival 11439 sinadd 11443 cosadd 11444 sinmul 11451 cosmul 11452 cos2tsin 11458 ef01bndlem 11463 sin01bnd 11464 cos01bnd 11465 cos1bnd 11466 cos2bnd 11467 cos01gt0 11469 sin02gt0 11470 sin4lt0 11473 cos12dec 11474 egt2lt3 11486 odd2np1lem 11569 odd2np1 11570 ltoddhalfle 11590 halfleoddlt 11591 opoe 11592 omoe 11593 opeo 11594 omeo 11595 nno 11603 nn0o 11604 flodddiv4 11631 6gcd4e2 11683 3lcm2e6woprm 11767 6lcm4e12 11768 sqrt2irrlem 11839 oddpwdclemodd 11850 coscn 12859 sinhalfpilem 12872 cospi 12881 ef2pi 12886 ef2kpi 12887 efper 12888 sinperlem 12889 sin2kpi 12892 cos2kpi 12893 sin2pim 12894 cos2pim 12895 ptolemy 12905 sincosq3sgn 12909 sincosq4sgn 12910 sinq12gt0 12911 cosq23lt0 12914 coseq00topi 12916 tangtx 12919 sincos4thpi 12921 sincos6thpi 12923 sincos3rdpi 12924 pigt3 12925 abssinper 12927 coskpi 12929 cosq34lt1 12931 ex-fl 12937 ex-ceil 12938 ex-exp 12939 ex-fac 12940 |
Copyright terms: Public domain | W3C validator |