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 7639. (Contributed by NM, 1-Mar-1995.) |
Ref | Expression |
---|---|
ax-icn |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ci 7590 | . 2 | |
2 | cc 7586 | . 2 | |
3 | 1, 2 | wcel 1465 | 1 |
Colors of variables: wff set class |
This axiom is referenced by: 0cn 7726 mulid1 7731 cnegexlem2 7906 cnegex 7908 0cnALT 7920 negicn 7931 ine0 8124 ixi 8312 rimul 8314 rereim 8315 apreap 8316 cru 8331 apreim 8332 mulreim 8333 apadd1 8337 apneg 8340 aprcl 8375 recextlem1 8379 recexaplem2 8380 recexap 8381 crap0 8680 cju 8683 it0e0 8899 2mulicn 8900 iap0 8901 2muliap0 8902 cnref1o 9396 irec 10347 i2 10348 i3 10349 i4 10350 iexpcyc 10352 imval 10577 imre 10578 reim 10579 crre 10584 crim 10585 remim 10587 mulreap 10591 cjreb 10593 recj 10594 reneg 10595 readd 10596 remullem 10598 imcj 10602 imneg 10603 imadd 10604 cjadd 10611 cjneg 10617 imval2 10621 rei 10626 imi 10627 cji 10629 cjreim 10630 cjreim2 10631 cjap 10633 cnrecnv 10637 rennim 10729 absi 10786 absreimsq 10794 absreim 10795 absimle 10811 climcvg1nlem 11073 sinval 11323 cosval 11324 sinf 11325 cosf 11326 tanval2ap 11334 tanval3ap 11335 resinval 11336 recosval 11337 efi4p 11338 resin4p 11339 recos4p 11340 resincl 11341 recoscl 11342 sinneg 11347 cosneg 11348 efival 11353 efmival 11354 efeul 11355 sinadd 11357 cosadd 11358 ef01bndlem 11377 sin01bnd 11378 cos01bnd 11379 absef 11390 absefib 11391 efieq1re 11392 demoivre 11393 demoivreALT 11394 cnrehmeocntop 12673 sincn 12769 coscn 12770 efhalfpi 12791 ef2kpi 12798 efper 12799 sinperlem 12800 efimpi 12811 qdencn 13118 |
Copyright terms: Public domain | W3C validator |