| 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 9203 |
. 2
| |
| 2 | 1 | recni 8181 |
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 1493 ax-7 1494 ax-gen 1495 ax-ie1 1539 ax-ie2 1540 ax-8 1550 ax-11 1552 ax-4 1556 ax-17 1572 ax-i9 1576 ax-ial 1580 ax-i5r 1581 ax-ext 2211 ax-resscn 8114 ax-1re 8116 ax-addrcl 8119 |
| This theorem depends on definitions: df-bi 117 df-nf 1507 df-sb 1809 df-clab 2216 df-cleq 2222 df-clel 2225 df-in 3204 df-ss 3211 df-2 9192 |
| This theorem is referenced by: 2ex 9205 2cnd 9206 2m1e1 9251 3m1e2 9253 2p2e4 9260 times2 9262 2div2e1 9266 1p2e3 9268 3p3e6 9276 4p3e7 9278 5p3e8 9281 6p3e9 9284 2t1e2 9287 2t2e4 9288 3t3e9 9291 2t0e0 9293 4d2e2 9294 2cnne0 9343 1mhlfehlf 9352 8th4div3 9353 halfpm6th 9354 2mulicn 9356 2muliap0 9358 halfcl 9360 half0 9362 2halves 9363 halfaddsub 9368 div4p1lem1div2 9388 3halfnz 9567 zneo 9571 nneoor 9572 zeo 9575 7p3e10 9675 4t4e16 9699 6t3e18 9705 7t7e49 9714 8t5e40 9718 9t9e81 9729 decbin0 9740 decbin2 9741 halfthird 9743 fztpval 10308 fz0tp 10347 fz0to4untppr 10349 fzo0to3tp 10454 2tnp1ge0ge0 10551 fldiv4lem1div2 10557 expubnd 10848 sq2 10887 sq4e2t8 10889 cu2 10890 subsq2 10899 binom2sub 10905 binom3 10909 zesq 10910 fac2 10983 fac3 10984 faclbnd2 10994 bcn2 11016 4bc2eq6 11026 crre 11408 addcj 11442 imval2 11445 resqrexlemover 11561 resqrexlemcalc1 11565 resqrexlemnm 11569 resqrexlemcvg 11570 amgm2 11669 arisum 12049 arisum2 12050 geo2sum2 12066 geo2lim 12067 geoihalfsum 12073 efcllemp 12209 ege2le3 12222 tanval2ap 12264 tanval3ap 12265 efi4p 12268 efival 12283 sinadd 12287 cosadd 12288 sinmul 12295 cosmul 12296 cos2tsin 12302 ef01bndlem 12307 sin01bnd 12308 cos01bnd 12309 cos1bnd 12310 cos2bnd 12311 cos01gt0 12314 sin02gt0 12315 sin4lt0 12318 cos12dec 12319 egt2lt3 12331 odd2np1lem 12423 odd2np1 12424 ltoddhalfle 12444 halfleoddlt 12445 opoe 12446 omoe 12447 opeo 12448 omeo 12449 nno 12457 nn0o 12458 flodddiv4 12487 bits0 12499 bitsfzolem 12505 0bits 12510 bitsinv1 12513 6gcd4e2 12556 3lcm2e6woprm 12648 6lcm4e12 12649 sqrt2irrlem 12723 oddpwdclemodd 12734 pythagtriplem1 12828 pythagtriplem12 12838 pythagtriplem14 12840 4sqlem11 12964 4sqlem12 12965 dec5dvds 12975 dec2nprm 12978 2exp5 12995 2exp6 12996 2exp7 12997 2exp8 12998 2exp11 12999 2exp16 13000 maxcncf 15329 mincncf 15330 coscn 15484 sinhalfpilem 15505 cospi 15514 ef2pi 15519 ef2kpi 15520 efper 15521 sinperlem 15522 sin2kpi 15525 cos2kpi 15526 sin2pim 15527 cos2pim 15528 ptolemy 15538 sincosq3sgn 15542 sincosq4sgn 15543 sinq12gt0 15544 cosq23lt0 15547 coseq00topi 15549 tangtx 15552 sincos4thpi 15554 sincos6thpi 15556 sincos3rdpi 15557 pigt3 15558 abssinper 15560 coskpi 15562 cosq34lt1 15564 logsqrt 15637 2logb9irrALT 15688 1sgm2ppw 15709 perfect1 15712 perfectlem1 15713 perfectlem2 15714 perfect 15715 lgsdir2lem2 15748 gausslemma2dlem6 15786 lgsquadlem1 15796 lgsquadlem2 15797 lgsquad2lem2 15801 m1lgs 15804 2lgslem3a 15812 2lgslem3b 15813 2lgslem3c 15814 2lgslem3d 15815 2lgsoddprmlem2 15825 2lgsoddprmlem3c 15828 2lgsoddprmlem3d 15829 clwwlknonex2 16234 ex-fl 16257 ex-ceil 16258 ex-exp 16259 ex-fac 16260 |
| Copyright terms: Public domain | W3C validator |