| 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 9180 |
. 2
| |
| 2 | 1 | recni 8158 |
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 8091 ax-1re 8093 ax-addrcl 8096 |
| 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 3203 df-ss 3210 df-2 9169 |
| This theorem is referenced by: 2ex 9182 2cnd 9183 2m1e1 9228 3m1e2 9230 2p2e4 9237 times2 9239 2div2e1 9243 1p2e3 9245 3p3e6 9253 4p3e7 9255 5p3e8 9258 6p3e9 9261 2t1e2 9264 2t2e4 9265 3t3e9 9268 2t0e0 9270 4d2e2 9271 2cnne0 9320 1mhlfehlf 9329 8th4div3 9330 halfpm6th 9331 2mulicn 9333 2muliap0 9335 halfcl 9337 half0 9339 2halves 9340 halfaddsub 9345 div4p1lem1div2 9365 3halfnz 9544 zneo 9548 nneoor 9549 zeo 9552 7p3e10 9652 4t4e16 9676 6t3e18 9682 7t7e49 9691 8t5e40 9695 9t9e81 9706 decbin0 9717 decbin2 9718 halfthird 9720 fztpval 10279 fz0tp 10318 fz0to4untppr 10320 fzo0to3tp 10425 2tnp1ge0ge0 10521 fldiv4lem1div2 10527 expubnd 10818 sq2 10857 sq4e2t8 10859 cu2 10860 subsq2 10869 binom2sub 10875 binom3 10879 zesq 10880 fac2 10953 fac3 10954 faclbnd2 10964 bcn2 10986 4bc2eq6 10996 crre 11368 addcj 11402 imval2 11405 resqrexlemover 11521 resqrexlemcalc1 11525 resqrexlemnm 11529 resqrexlemcvg 11530 amgm2 11629 arisum 12009 arisum2 12010 geo2sum2 12026 geo2lim 12027 geoihalfsum 12033 efcllemp 12169 ege2le3 12182 tanval2ap 12224 tanval3ap 12225 efi4p 12228 efival 12243 sinadd 12247 cosadd 12248 sinmul 12255 cosmul 12256 cos2tsin 12262 ef01bndlem 12267 sin01bnd 12268 cos01bnd 12269 cos1bnd 12270 cos2bnd 12271 cos01gt0 12274 sin02gt0 12275 sin4lt0 12278 cos12dec 12279 egt2lt3 12291 odd2np1lem 12383 odd2np1 12384 ltoddhalfle 12404 halfleoddlt 12405 opoe 12406 omoe 12407 opeo 12408 omeo 12409 nno 12417 nn0o 12418 flodddiv4 12447 bits0 12459 bitsfzolem 12465 0bits 12470 bitsinv1 12473 6gcd4e2 12516 3lcm2e6woprm 12608 6lcm4e12 12609 sqrt2irrlem 12683 oddpwdclemodd 12694 pythagtriplem1 12788 pythagtriplem12 12798 pythagtriplem14 12800 4sqlem11 12924 4sqlem12 12925 dec5dvds 12935 dec2nprm 12938 2exp5 12955 2exp6 12956 2exp7 12957 2exp8 12958 2exp11 12959 2exp16 12960 maxcncf 15289 mincncf 15290 coscn 15444 sinhalfpilem 15465 cospi 15474 ef2pi 15479 ef2kpi 15480 efper 15481 sinperlem 15482 sin2kpi 15485 cos2kpi 15486 sin2pim 15487 cos2pim 15488 ptolemy 15498 sincosq3sgn 15502 sincosq4sgn 15503 sinq12gt0 15504 cosq23lt0 15507 coseq00topi 15509 tangtx 15512 sincos4thpi 15514 sincos6thpi 15516 sincos3rdpi 15517 pigt3 15518 abssinper 15520 coskpi 15522 cosq34lt1 15524 logsqrt 15597 2logb9irrALT 15648 1sgm2ppw 15669 perfect1 15672 perfectlem1 15673 perfectlem2 15674 perfect 15675 lgsdir2lem2 15708 gausslemma2dlem6 15746 lgsquadlem1 15756 lgsquadlem2 15757 lgsquad2lem2 15761 m1lgs 15764 2lgslem3a 15772 2lgslem3b 15773 2lgslem3c 15774 2lgslem3d 15775 2lgsoddprmlem2 15785 2lgsoddprmlem3c 15788 2lgsoddprmlem3d 15789 ex-fl 16089 ex-ceil 16090 ex-exp 16091 ex-fac 16092 |
| Copyright terms: Public domain | W3C validator |