![]() |
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 11140. (Contributed by NM, 1-Mar-1995.) |
Ref | Expression |
---|---|
ax-icn | ⊢ i ∈ ℂ |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ci 11107 | . 2 class i | |
2 | cc 11103 | . 2 class ℂ | |
3 | 1, 2 | wcel 2107 | 1 wff i ∈ ℂ |
Colors of variables: wff setvar class |
This axiom is referenced by: 0cn 11201 mulrid 11207 mul02lem2 11386 mul02 11387 addrid 11389 cnegex 11390 cnegex2 11391 0cnALT 11443 0cnALT2 11444 negicn 11456 ine0 11644 ixi 11838 recextlem1 11839 recextlem2 11840 recex 11841 rimul 12198 cru 12199 crne0 12200 cju 12203 it0e0 12429 2mulicn 12430 2muline0 12431 cnref1o 12964 irec 14160 i2 14161 i3 14162 i4 14163 iexpcyc 14166 crreczi 14186 imre 15050 reim 15051 crre 15056 crim 15057 remim 15059 mulre 15063 cjreb 15065 recj 15066 reneg 15067 readd 15068 remullem 15070 imcj 15074 imneg 15075 imadd 15076 cjadd 15083 cjneg 15089 imval2 15093 rei 15098 imi 15099 cji 15101 cjreim 15102 cjreim2 15103 rennim 15181 cnpart 15182 sqrtneglem 15208 sqrtneg 15209 sqrtm1 15217 absi 15228 absreimsq 15234 absreim 15235 absimle 15251 abs1m 15277 sqreulem 15301 sqreu 15302 bhmafibid1 15407 caucvgr 15617 sinf 16062 cosf 16063 tanval2 16071 tanval3 16072 resinval 16073 recosval 16074 efi4p 16075 resin4p 16076 recos4p 16077 resincl 16078 recoscl 16079 sinneg 16084 cosneg 16085 efival 16090 efmival 16091 sinhval 16092 coshval 16093 retanhcl 16097 tanhlt1 16098 tanhbnd 16099 efeul 16100 sinadd 16102 cosadd 16103 ef01bndlem 16122 sin01bnd 16123 cos01bnd 16124 absef 16135 absefib 16136 efieq1re 16137 demoivre 16138 demoivreALT 16139 nthruc 16190 igz 16862 4sqlem17 16889 cnsubrg 20989 cnrehmeo 24450 cmodscexp 24618 ncvspi 24654 cphipval2 24739 4cphipval2 24740 cphipval 24741 itg0 25278 itgz 25279 itgcl 25282 ibl0 25285 iblcnlem1 25286 itgcnlem 25288 itgneg 25302 iblss 25303 iblss2 25304 itgss 25310 itgeqa 25312 iblconst 25316 itgconst 25317 itgadd 25323 iblabs 25327 iblabsr 25328 iblmulc2 25329 itgmulc2 25332 itgsplit 25334 dvsincos 25479 iaa 25819 sincn 25937 coscn 25938 efhalfpi 25962 ef2kpi 25969 efper 25970 sinperlem 25971 efimpi 25982 pige3ALT 26010 sineq0 26014 efeq1 26018 tanregt0 26029 efif1olem4 26035 efifo 26037 eff1olem 26038 circgrp 26042 circsubm 26043 logneg 26077 logm1 26078 lognegb 26079 eflogeq 26091 efiarg 26096 cosargd 26097 logimul 26103 logneg2 26104 abslogle 26107 tanarg 26108 logcn 26136 logf1o2 26139 cxpsqrtlem 26191 cxpsqrt 26192 root1eq1 26242 cxpeq 26244 ang180lem1 26293 ang180lem2 26294 ang180lem3 26295 ang180lem4 26296 1cubrlem 26325 1cubr 26326 asinlem 26352 asinlem2 26353 asinlem3a 26354 asinlem3 26355 asinf 26356 atandm2 26361 atandm3 26362 atanf 26364 asinneg 26370 efiasin 26372 sinasin 26373 asinsinlem 26375 asinsin 26376 asin1 26378 asinbnd 26383 cosasin 26388 atanneg 26391 atancj 26394 efiatan 26396 atanlogaddlem 26397 atanlogadd 26398 atanlogsublem 26399 atanlogsub 26400 efiatan2 26401 2efiatan 26402 tanatan 26403 cosatan 26405 atantan 26407 atanbndlem 26409 atans2 26415 dvatan 26419 atantayl 26421 atantayl2 26422 log2cnv 26428 basellem3 26566 2sqlem2 26900 nvpi 29897 ipval2 29937 4ipval2 29938 ipval3 29939 ipidsq 29940 dipcl 29942 dipcj 29944 dip0r 29947 dipcn 29950 ip1ilem 30056 ipasslem10 30069 ipasslem11 30070 polid2i 30387 polidi 30388 lnopeq0lem1 31235 lnopeq0i 31237 lnophmlem2 31247 ccfldextdgrr 32690 cnre2csqima 32828 efmul2picn 33545 itgexpif 33555 vtscl 33587 vtsprod 33588 circlemeth 33589 logi 34641 iexpire 34642 gg-cnrehmeo 35108 itgaddnc 36485 iblabsnc 36489 iblmulc2nc 36490 itgmulc2nc 36493 ftc1anclem3 36500 ftc1anclem6 36503 ftc1anclem7 36504 ftc1anclem8 36505 ftc1anc 36506 dvasin 36509 areacirclem4 36516 cntotbnd 36601 sn-1ne2 41128 re1m1e0m0 41213 sn-addlid 41220 sn-it0e0 41231 sn-negex12 41232 reixi 41238 sn-1ticom 41250 sn-mullid 41251 it1ei 41252 ipiiie0 41253 sn-0tie0 41255 sn-mul02 41256 sn-inelr 41281 itrere 41282 retire 41283 cnreeu 41284 proot1ex 41875 sqrtcval 42324 sqrtcval2 42325 resqrtvalex 42328 imsqrtvalex 42329 sineq0ALT 43630 iblsplit 44616 sqrtnegnre 45949 requad01 46223 sinh-conventional 47685 |
Copyright terms: Public domain | W3C validator |