| 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 11190. (Contributed by NM, 1-Mar-1995.) |
| Ref | Expression |
|---|---|
| ax-icn | ⊢ i ∈ ℂ |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | ci 11157 | . 2 class i | |
| 2 | cc 11153 | . 2 class ℂ | |
| 3 | 1, 2 | wcel 2108 | 1 wff i ∈ ℂ |
| Colors of variables: wff setvar class |
| This axiom is referenced by: 0cn 11253 mulrid 11259 mul02lem2 11438 mul02 11439 addrid 11441 cnegex 11442 cnegex2 11443 0cnALT 11496 0cnALT2 11497 negicn 11509 ine0 11698 ixi 11892 recextlem1 11893 recextlem2 11894 recex 11895 rimul 12257 cru 12258 crne0 12259 cju 12262 it0e0 12488 2mulicn 12489 2muline0 12490 cnref1o 13027 irec 14240 i2 14241 i3 14242 i4 14243 iexpcyc 14246 crreczi 14267 imre 15147 reim 15148 crre 15153 crim 15154 remim 15156 mulre 15160 cjreb 15162 recj 15163 reneg 15164 readd 15165 remullem 15167 imcj 15171 imneg 15172 imadd 15173 cjadd 15180 cjneg 15186 imval2 15190 rei 15195 imi 15196 cji 15198 cjreim 15199 cjreim2 15200 rennim 15278 cnpart 15279 sqrtneglem 15305 sqrtneg 15306 sqrtm1 15314 absi 15325 absreimsq 15331 absreim 15332 absimle 15348 abs1m 15374 sqreulem 15398 sqreu 15399 bhmafibid1 15504 caucvgr 15712 sinf 16160 cosf 16161 tanval2 16169 tanval3 16170 resinval 16171 recosval 16172 efi4p 16173 resin4p 16174 recos4p 16175 resincl 16176 recoscl 16177 sinneg 16182 cosneg 16183 efival 16188 efmival 16189 sinhval 16190 coshval 16191 retanhcl 16195 tanhlt1 16196 tanhbnd 16197 efeul 16198 sinadd 16200 cosadd 16201 ef01bndlem 16220 sin01bnd 16221 cos01bnd 16222 absef 16233 absefib 16234 efieq1re 16235 demoivre 16236 demoivreALT 16237 nthruc 16288 igz 16972 4sqlem17 16999 cnsubrg 21445 cnrehmeo 24984 cnrehmeoOLD 24985 cmodscexp 25154 ncvspi 25190 cphipval2 25275 4cphipval2 25276 cphipval 25277 itg0 25815 itgz 25816 itgcl 25819 ibl0 25822 iblcnlem1 25823 itgcnlem 25825 itgneg 25839 iblss 25840 iblss2 25841 itgss 25847 itgeqa 25849 iblconst 25853 itgconst 25854 itgadd 25860 iblabs 25864 iblabsr 25865 iblmulc2 25866 itgmulc2 25869 itgsplit 25871 dvsincos 26019 iaa 26367 sincn 26488 coscn 26489 efhalfpi 26513 ef2kpi 26520 efper 26521 sinperlem 26522 efimpi 26533 pige3ALT 26562 sineq0 26566 efeq1 26570 tanregt0 26581 efif1olem4 26587 efifo 26589 eff1olem 26590 circgrp 26594 circsubm 26595 logi 26629 logneg 26630 logm1 26631 lognegb 26632 eflogeq 26644 efiarg 26649 cosargd 26650 logimul 26656 logneg2 26657 abslogle 26660 tanarg 26661 logcn 26689 logf1o2 26692 cxpsqrtlem 26744 cxpsqrt 26745 root1eq1 26798 cxpeq 26800 ang180lem1 26852 ang180lem2 26853 ang180lem3 26854 ang180lem4 26855 1cubrlem 26884 1cubr 26885 asinlem 26911 asinlem2 26912 asinlem3a 26913 asinlem3 26914 asinf 26915 atandm2 26920 atandm3 26921 atanf 26923 asinneg 26929 efiasin 26931 sinasin 26932 asinsinlem 26934 asinsin 26935 asin1 26937 asinbnd 26942 cosasin 26947 atanneg 26950 atancj 26953 efiatan 26955 atanlogaddlem 26956 atanlogadd 26957 atanlogsublem 26958 atanlogsub 26959 efiatan2 26960 2efiatan 26961 tanatan 26962 cosatan 26964 atantan 26966 atanbndlem 26968 atans2 26974 dvatan 26978 atantayl 26980 atantayl2 26981 log2cnv 26987 basellem3 27126 2sqlem2 27462 nvpi 30686 ipval2 30726 4ipval2 30727 ipval3 30728 ipidsq 30729 dipcl 30731 dipcj 30733 dip0r 30736 dipcn 30739 ip1ilem 30845 ipasslem10 30858 ipasslem11 30859 polid2i 31176 polidi 31177 lnopeq0lem1 32024 lnopeq0i 32026 lnophmlem2 32036 re0cj 32753 ccfldextdgrr 33722 constrelextdg2 33788 cnre2csqima 33910 efmul2picn 34611 itgexpif 34621 vtscl 34653 vtsprod 34654 circlemeth 34655 iexpire 35735 itgaddnc 37687 iblabsnc 37691 iblmulc2nc 37692 itgmulc2nc 37695 ftc1anclem3 37702 ftc1anclem6 37705 ftc1anclem7 37706 ftc1anclem8 37707 ftc1anc 37708 dvasin 37711 areacirclem4 37718 cntotbnd 37803 sn-1ne2 42300 0tie0 42350 it1ei 42351 1tiei 42352 itrere 42353 retire 42354 ef11d 42375 cxp112d 42377 cxp111d 42378 cxpi11d 42379 re1m1e0m0 42427 sn-addlid 42434 sn-it0e0 42445 sn-negex12 42446 reixi 42452 sn-1ticom 42464 sn-mullid 42465 sn-it1ei 42466 ipiiie0 42467 sn-0tie0 42469 sn-mul02 42470 sn-inelr 42497 sn-itrere 42498 sn-retire 42499 cnreeu 42500 proot1ex 43208 sqrtcval 43654 sqrtcval2 43655 resqrtvalex 43658 imsqrtvalex 43659 sineq0ALT 44957 iblsplit 45981 sqrtnegnre 47319 requad01 47608 sinh-conventional 49258 |
| Copyright terms: Public domain | W3C validator |