![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > ax-icn | GIF version |
Description: i is a complex number. Axiom for real and complex numbers, justified by theorem axicn 6749. (Contributed by NM, 1-Mar-1995.) |
Ref | Expression |
---|---|
ax-icn | ⊢ i ∈ ℂ |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ci 6713 | . 2 class i | |
2 | cc 6709 | . 2 class ℂ | |
3 | 1, 2 | wcel 1390 | 1 wff i ∈ ℂ |
Colors of variables: wff set class |
This axiom is referenced by: 0cn 6817 mulid1 6822 cnegexlem2 6984 cnegex 6986 0cnALT 6998 negicn 7009 ine0 7187 ixi 7367 rimul 7369 rereim 7370 apreap 7371 cru 7386 apreim 7387 mulreim 7388 apadd1 7392 apneg 7395 recextlem1 7414 recexaplem2 7415 recexap 7416 crap0 7691 cju 7694 it0e0 7923 2mulicn 7924 iap0 7925 2muliap0 7926 cnref1o 8357 irec 9005 i2 9006 i3 9007 i4 9008 imval 9078 imre 9079 reim 9080 crre 9085 crim 9086 remim 9088 mulreap 9092 cjreb 9094 recj 9095 reneg 9096 readd 9097 remullem 9099 imcj 9103 imneg 9104 imadd 9105 cjadd 9112 cjneg 9118 imval2 9122 rei 9127 imi 9128 cji 9130 cjreim 9131 cjreim2 9132 cjap 9134 cnrecnv 9138 rennim 9211 absi 9223 |
Copyright terms: Public domain | W3C validator |