Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > ax-icn | Structured version Visualization version GIF version |
Description: i is a complex number. Axiom 3 of 22 for real and complex numbers, justified by theorem axicn 10572. (Contributed by NM, 1-Mar-1995.) |
Ref | Expression |
---|---|
ax-icn | ⊢ i ∈ ℂ |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ci 10539 | . 2 class i | |
2 | cc 10535 | . 2 class ℂ | |
3 | 1, 2 | wcel 2114 | 1 wff i ∈ ℂ |
Colors of variables: wff setvar class |
This axiom is referenced by: 0cn 10633 mulid1 10639 mul02lem2 10817 mul02 10818 addid1 10820 cnegex 10821 cnegex2 10822 0cnALT 10874 0cnALT2 10875 negicn 10887 ine0 11075 ixi 11269 recextlem1 11270 recextlem2 11271 recex 11272 rimul 11629 cru 11630 crne0 11631 cju 11634 it0e0 11860 2mulicn 11861 2muline0 11862 cnref1o 12385 irec 13565 i2 13566 i3 13567 i4 13568 iexpcyc 13570 crreczi 13590 imre 14467 reim 14468 crre 14473 crim 14474 remim 14476 mulre 14480 cjreb 14482 recj 14483 reneg 14484 readd 14485 remullem 14487 imcj 14491 imneg 14492 imadd 14493 cjadd 14500 cjneg 14506 imval2 14510 rei 14515 imi 14516 cji 14518 cjreim 14519 cjreim2 14520 rennim 14598 cnpart 14599 sqrtneglem 14626 sqrtneg 14627 sqrtm1 14635 absi 14646 absreimsq 14652 absreim 14653 absimle 14669 abs1m 14695 sqreulem 14719 sqreu 14720 bhmafibid1 14825 caucvgr 15032 sinf 15477 cosf 15478 tanval2 15486 tanval3 15487 resinval 15488 recosval 15489 efi4p 15490 resin4p 15491 recos4p 15492 resincl 15493 recoscl 15494 sinneg 15499 cosneg 15500 efival 15505 efmival 15506 sinhval 15507 coshval 15508 retanhcl 15512 tanhlt1 15513 tanhbnd 15514 efeul 15515 sinadd 15517 cosadd 15518 ef01bndlem 15537 sin01bnd 15538 cos01bnd 15539 absef 15550 absefib 15551 efieq1re 15552 demoivre 15553 demoivreALT 15554 nthruc 15605 igz 16270 4sqlem17 16297 cnsubrg 20605 cnrehmeo 23557 cmodscexp 23725 ncvspi 23760 cphipval2 23844 4cphipval2 23845 cphipval 23846 itg0 24380 itgz 24381 itgcl 24384 ibl0 24387 iblcnlem1 24388 itgcnlem 24390 itgneg 24404 iblss 24405 iblss2 24406 itgss 24412 itgeqa 24414 iblconst 24418 itgconst 24419 itgadd 24425 iblabs 24429 iblabsr 24430 iblmulc2 24431 itgmulc2 24434 itgsplit 24436 dvsincos 24578 iaa 24914 sincn 25032 coscn 25033 efhalfpi 25057 ef2kpi 25064 efper 25065 sinperlem 25066 efimpi 25077 pige3ALT 25105 sineq0 25109 efeq1 25113 tanregt0 25123 efif1olem4 25129 efifo 25131 eff1olem 25132 circgrp 25136 circsubm 25137 logneg 25171 logm1 25172 lognegb 25173 eflogeq 25185 efiarg 25190 cosargd 25191 logimul 25197 logneg2 25198 abslogle 25201 tanarg 25202 logcn 25230 logf1o2 25233 cxpsqrtlem 25285 cxpsqrt 25286 root1eq1 25336 cxpeq 25338 ang180lem1 25387 ang180lem2 25388 ang180lem3 25389 ang180lem4 25390 1cubrlem 25419 1cubr 25420 asinlem 25446 asinlem2 25447 asinlem3a 25448 asinlem3 25449 asinf 25450 atandm2 25455 atandm3 25456 atanf 25458 asinneg 25464 efiasin 25466 sinasin 25467 asinsinlem 25469 asinsin 25470 asin1 25472 asinbnd 25477 cosasin 25482 atanneg 25485 atancj 25488 efiatan 25490 atanlogaddlem 25491 atanlogadd 25492 atanlogsublem 25493 atanlogsub 25494 efiatan2 25495 2efiatan 25496 tanatan 25497 cosatan 25499 atantan 25501 atanbndlem 25503 atans2 25509 dvatan 25513 atantayl 25515 atantayl2 25516 log2cnv 25522 basellem3 25660 2sqlem2 25994 nvpi 28444 ipval2 28484 4ipval2 28485 ipval3 28486 ipidsq 28487 dipcl 28489 dipcj 28491 dip0r 28494 dipcn 28497 ip1ilem 28603 ipasslem10 28616 ipasslem11 28617 polid2i 28934 polidi 28935 lnopeq0lem1 29782 lnopeq0i 29784 lnophmlem2 29794 ccfldextdgrr 31057 cnre2csqima 31154 efmul2picn 31867 itgexpif 31877 vtscl 31909 vtsprod 31910 circlemeth 31911 logi 32966 iexpire 32967 itgaddnc 34967 iblabsnc 34971 iblmulc2nc 34972 itgmulc2nc 34975 ftc1anclem3 34984 ftc1anclem6 34987 ftc1anclem7 34988 ftc1anclem8 34989 ftc1anc 34990 dvasin 34993 areacirclem4 35000 cntotbnd 35089 sn-1ne2 39207 re1m1e0m0 39276 sn-addid2 39283 proot1ex 39850 sineq0ALT 41320 iblsplit 42300 sqrtnegnre 43556 requad01 43835 sinh-conventional 44887 |
Copyright terms: Public domain | W3C validator |