![]() |
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 8987 |
. 2
![]() ![]() ![]() ![]() | |
2 | 1 | recni 7968 |
1
![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() ![]() |
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 7902 ax-1re 7904 ax-addrcl 7907 |
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 3135 df-ss 3142 df-2 8976 |
This theorem is referenced by: 2ex 8989 2cnd 8990 2m1e1 9035 3m1e2 9037 2p2e4 9044 times2 9046 2div2e1 9049 1p2e3 9051 3p3e6 9059 4p3e7 9061 5p3e8 9064 6p3e9 9067 2t1e2 9070 2t2e4 9071 3t3e9 9074 2t0e0 9076 4d2e2 9077 2cnne0 9126 1mhlfehlf 9135 8th4div3 9136 halfpm6th 9137 2mulicn 9139 2muliap0 9141 halfcl 9143 half0 9145 2halves 9146 halfaddsub 9151 div4p1lem1div2 9170 3halfnz 9348 zneo 9352 nneoor 9353 zeo 9356 7p3e10 9456 4t4e16 9480 6t3e18 9486 7t7e49 9495 8t5e40 9499 9t9e81 9510 decbin0 9521 decbin2 9522 halfthird 9524 fztpval 10080 fz0tp 10119 fz0to4untppr 10121 fzo0to3tp 10216 2tnp1ge0ge0 10298 expubnd 10574 sq2 10612 sq4e2t8 10614 cu2 10615 subsq2 10624 binom2sub 10630 binom3 10634 zesq 10635 fac2 10706 fac3 10707 faclbnd2 10717 bcn2 10739 4bc2eq6 10749 crre 10861 addcj 10895 imval2 10898 resqrexlemover 11014 resqrexlemcalc1 11018 resqrexlemnm 11022 resqrexlemcvg 11023 amgm2 11122 arisum 11501 arisum2 11502 geo2sum2 11518 geo2lim 11519 geoihalfsum 11525 efcllemp 11661 ege2le3 11674 tanval2ap 11716 tanval3ap 11717 efi4p 11720 efival 11735 sinadd 11739 cosadd 11740 sinmul 11747 cosmul 11748 cos2tsin 11754 ef01bndlem 11759 sin01bnd 11760 cos01bnd 11761 cos1bnd 11762 cos2bnd 11763 cos01gt0 11765 sin02gt0 11766 sin4lt0 11769 cos12dec 11770 egt2lt3 11782 odd2np1lem 11871 odd2np1 11872 ltoddhalfle 11892 halfleoddlt 11893 opoe 11894 omoe 11895 opeo 11896 omeo 11897 nno 11905 nn0o 11906 flodddiv4 11933 6gcd4e2 11990 3lcm2e6woprm 12080 6lcm4e12 12081 sqrt2irrlem 12155 oddpwdclemodd 12166 pythagtriplem1 12259 pythagtriplem12 12269 pythagtriplem14 12271 coscn 14084 sinhalfpilem 14105 cospi 14114 ef2pi 14119 ef2kpi 14120 efper 14121 sinperlem 14122 sin2kpi 14125 cos2kpi 14126 sin2pim 14127 cos2pim 14128 ptolemy 14138 sincosq3sgn 14142 sincosq4sgn 14143 sinq12gt0 14144 cosq23lt0 14147 coseq00topi 14149 tangtx 14152 sincos4thpi 14154 sincos6thpi 14156 sincos3rdpi 14157 pigt3 14158 abssinper 14160 coskpi 14162 cosq34lt1 14164 logsqrt 14236 2logb9irrALT 14285 lgsdir2lem2 14323 ex-fl 14359 ex-ceil 14360 ex-exp 14361 ex-fac 14362 |
Copyright terms: Public domain | W3C validator |