Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > ax-icn | Unicode version |
Description: is a complex number. Axiom for real and complex numbers, justified by Theorem axicn 7825. (Contributed by NM, 1-Mar-1995.) |
Ref | Expression |
---|---|
ax-icn |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ci 7776 | . 2 | |
2 | cc 7772 | . 2 | |
3 | 1, 2 | wcel 2141 | 1 |
Colors of variables: wff set class |
This axiom is referenced by: 0cn 7912 mulid1 7917 cnegexlem2 8095 cnegex 8097 0cnALT 8109 negicn 8120 ine0 8313 ixi 8502 rimul 8504 rereim 8505 apreap 8506 cru 8521 apreim 8522 mulreim 8523 apadd1 8527 apneg 8530 aprcl 8565 recextlem1 8569 recexaplem2 8570 recexap 8571 crap0 8874 cju 8877 it0e0 9099 2mulicn 9100 iap0 9101 2muliap0 9102 cnref1o 9609 irec 10575 i2 10576 i3 10577 i4 10578 iexpcyc 10580 imval 10814 imre 10815 reim 10816 crre 10821 crim 10822 remim 10824 mulreap 10828 cjreb 10830 recj 10831 reneg 10832 readd 10833 remullem 10835 imcj 10839 imneg 10840 imadd 10841 cjadd 10848 cjneg 10854 imval2 10858 rei 10863 imi 10864 cji 10866 cjreim 10867 cjreim2 10868 cjap 10870 cnrecnv 10874 rennim 10966 absi 11023 absreimsq 11031 absreim 11032 absimle 11048 climcvg1nlem 11312 sinval 11665 cosval 11666 sinf 11667 cosf 11668 tanval2ap 11676 tanval3ap 11677 resinval 11678 recosval 11679 efi4p 11680 resin4p 11681 recos4p 11682 resincl 11683 recoscl 11684 sinneg 11689 cosneg 11690 efival 11695 efmival 11696 efeul 11697 sinadd 11699 cosadd 11700 ef01bndlem 11719 sin01bnd 11720 cos01bnd 11721 absef 11732 absefib 11733 efieq1re 11734 demoivre 11735 demoivreALT 11736 igz 12326 cnrehmeocntop 13387 sincn 13484 coscn 13485 efhalfpi 13514 ef2kpi 13521 efper 13522 sinperlem 13523 efimpi 13534 2sqlem2 13745 qdencn 14059 |
Copyright terms: Public domain | W3C validator |