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 7795. (Contributed by NM, 1-Mar-1995.) |
Ref | Expression |
---|---|
ax-icn |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ci 7746 | . 2 | |
2 | cc 7742 | . 2 | |
3 | 1, 2 | wcel 2135 | 1 |
Colors of variables: wff set class |
This axiom is referenced by: 0cn 7882 mulid1 7887 cnegexlem2 8065 cnegex 8067 0cnALT 8079 negicn 8090 ine0 8283 ixi 8472 rimul 8474 rereim 8475 apreap 8476 cru 8491 apreim 8492 mulreim 8493 apadd1 8497 apneg 8500 aprcl 8535 recextlem1 8539 recexaplem2 8540 recexap 8541 crap0 8844 cju 8847 it0e0 9069 2mulicn 9070 iap0 9071 2muliap0 9072 cnref1o 9579 irec 10544 i2 10545 i3 10546 i4 10547 iexpcyc 10549 imval 10778 imre 10779 reim 10780 crre 10785 crim 10786 remim 10788 mulreap 10792 cjreb 10794 recj 10795 reneg 10796 readd 10797 remullem 10799 imcj 10803 imneg 10804 imadd 10805 cjadd 10812 cjneg 10818 imval2 10822 rei 10827 imi 10828 cji 10830 cjreim 10831 cjreim2 10832 cjap 10834 cnrecnv 10838 rennim 10930 absi 10987 absreimsq 10995 absreim 10996 absimle 11012 climcvg1nlem 11276 sinval 11629 cosval 11630 sinf 11631 cosf 11632 tanval2ap 11640 tanval3ap 11641 resinval 11642 recosval 11643 efi4p 11644 resin4p 11645 recos4p 11646 resincl 11647 recoscl 11648 sinneg 11653 cosneg 11654 efival 11659 efmival 11660 efeul 11661 sinadd 11663 cosadd 11664 ef01bndlem 11683 sin01bnd 11684 cos01bnd 11685 absef 11696 absefib 11697 efieq1re 11698 demoivre 11699 demoivreALT 11700 cnrehmeocntop 13140 sincn 13237 coscn 13238 efhalfpi 13267 ef2kpi 13274 efper 13275 sinperlem 13276 efimpi 13287 qdencn 13747 |
Copyright terms: Public domain | W3C validator |