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 10561. (Contributed by NM, 1-Mar-1995.) |
Ref | Expression |
---|---|
ax-icn | ⊢ i ∈ ℂ |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ci 10528 | . 2 class i | |
2 | cc 10524 | . 2 class ℂ | |
3 | 1, 2 | wcel 2105 | 1 wff i ∈ ℂ |
Colors of variables: wff setvar class |
This axiom is referenced by: 0cn 10622 mulid1 10628 mul02lem2 10806 mul02 10807 addid1 10809 cnegex 10810 cnegex2 10811 0cnALT 10863 0cnALT2 10864 negicn 10876 ine0 11064 ixi 11258 recextlem1 11259 recextlem2 11260 recex 11261 rimul 11618 cru 11619 crne0 11620 cju 11623 it0e0 11848 2mulicn 11849 2muline0 11850 cnref1o 12374 irec 13554 i2 13555 i3 13556 i4 13557 iexpcyc 13559 crreczi 13579 imre 14457 reim 14458 crre 14463 crim 14464 remim 14466 mulre 14470 cjreb 14472 recj 14473 reneg 14474 readd 14475 remullem 14477 imcj 14481 imneg 14482 imadd 14483 cjadd 14490 cjneg 14496 imval2 14500 rei 14505 imi 14506 cji 14508 cjreim 14509 cjreim2 14510 rennim 14588 cnpart 14589 sqrtneglem 14616 sqrtneg 14617 sqrtm1 14625 absi 14636 absreimsq 14642 absreim 14643 absimle 14659 abs1m 14685 sqreulem 14709 sqreu 14710 bhmafibid1 14815 caucvgr 15022 sinf 15467 cosf 15468 tanval2 15476 tanval3 15477 resinval 15478 recosval 15479 efi4p 15480 resin4p 15481 recos4p 15482 resincl 15483 recoscl 15484 sinneg 15489 cosneg 15490 efival 15495 efmival 15496 sinhval 15497 coshval 15498 retanhcl 15502 tanhlt1 15503 tanhbnd 15504 efeul 15505 sinadd 15507 cosadd 15508 ef01bndlem 15527 sin01bnd 15528 cos01bnd 15529 absef 15540 absefib 15541 efieq1re 15542 demoivre 15543 demoivreALT 15544 nthruc 15595 igz 16260 4sqlem17 16287 cnsubrg 20535 cnrehmeo 23486 cmodscexp 23654 ncvspi 23689 cphipval2 23773 4cphipval2 23774 cphipval 23775 itg0 24309 itgz 24310 itgcl 24313 ibl0 24316 iblcnlem1 24317 itgcnlem 24319 itgneg 24333 iblss 24334 iblss2 24335 itgss 24341 itgeqa 24343 iblconst 24347 itgconst 24348 itgadd 24354 iblabs 24358 iblabsr 24359 iblmulc2 24360 itgmulc2 24363 itgsplit 24365 dvsincos 24507 iaa 24843 sincn 24961 coscn 24962 efhalfpi 24986 ef2kpi 24993 efper 24994 sinperlem 24995 efimpi 25006 pige3ALT 25034 sineq0 25038 efeq1 25040 tanregt0 25050 efif1olem4 25056 efifo 25058 eff1olem 25059 circgrp 25063 circsubm 25064 logneg 25098 logm1 25099 lognegb 25100 eflogeq 25112 efiarg 25117 cosargd 25118 logimul 25124 logneg2 25125 abslogle 25128 tanarg 25129 logcn 25157 logf1o2 25160 cxpsqrtlem 25212 cxpsqrt 25213 root1eq1 25263 cxpeq 25265 ang180lem1 25314 ang180lem2 25315 ang180lem3 25316 ang180lem4 25317 1cubrlem 25346 1cubr 25347 asinlem 25373 asinlem2 25374 asinlem3a 25375 asinlem3 25376 asinf 25377 atandm2 25382 atandm3 25383 atanf 25385 asinneg 25391 efiasin 25393 sinasin 25394 asinsinlem 25396 asinsin 25397 asin1 25399 asinbnd 25404 cosasin 25409 atanneg 25412 atancj 25415 efiatan 25417 atanlogaddlem 25418 atanlogadd 25419 atanlogsublem 25420 atanlogsub 25421 efiatan2 25422 2efiatan 25423 tanatan 25424 cosatan 25426 atantan 25428 atanbndlem 25430 atans2 25436 dvatan 25440 atantayl 25442 atantayl2 25443 log2cnv 25450 basellem3 25588 2sqlem2 25922 nvpi 28372 ipval2 28412 4ipval2 28413 ipval3 28414 ipidsq 28415 dipcl 28417 dipcj 28419 dip0r 28422 dipcn 28425 ip1ilem 28531 ipasslem10 28544 ipasslem11 28545 polid2i 28862 polidi 28863 lnopeq0lem1 29710 lnopeq0i 29712 lnophmlem2 29722 ccfldextdgrr 30957 cnre2csqima 31054 efmul2picn 31767 itgexpif 31777 vtscl 31809 vtsprod 31810 circlemeth 31811 logi 32864 iexpire 32865 itgaddnc 34834 iblabsnc 34838 iblmulc2nc 34839 itgmulc2nc 34842 ftc1anclem3 34851 ftc1anclem6 34854 ftc1anclem7 34855 ftc1anclem8 34856 ftc1anc 34857 dvasin 34860 areacirclem4 34867 cntotbnd 34957 sn-1ne2 39038 re1m1e0m0 39107 sn-addid2 39114 proot1ex 39681 sineq0ALT 41151 iblsplit 42131 sqrtnegnre 43388 requad01 43633 sinh-conventional 44736 |
Copyright terms: Public domain | W3C validator |