![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > 0cnd | Unicode version |
Description: 0 is a complex number, deductive form. (Contributed by David A. Wheeler, 8-Dec-2018.) |
Ref | Expression |
---|---|
0cnd |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 0cn 7948 |
. 2
![]() ![]() ![]() ![]() | |
2 | 1 | a1i 9 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-5 1447 ax-gen 1449 ax-ie1 1493 ax-ie2 1494 ax-4 1510 ax-17 1526 ax-ial 1534 ax-ext 2159 ax-1cn 7903 ax-icn 7905 ax-addcl 7906 ax-mulcl 7908 ax-i2m1 7915 |
This theorem depends on definitions: df-bi 117 df-cleq 2170 df-clel 2173 |
This theorem is referenced by: mulap0r 8571 mulap0 8610 mul0eqap 8626 diveqap0 8638 eqneg 8688 div2subap 8793 prodgt0 8808 un0addcl 9208 un0mulcl 9209 modsumfzodifsn 10395 ser0 10513 ser0f 10514 abs00ap 11070 abs00 11072 abssubne0 11099 mul0inf 11248 clim0c 11293 sumrbdclem 11384 summodclem2a 11388 zsumdc 11391 fsum3 11394 isumz 11396 isumss 11398 fisumss 11399 fsum3cvg2 11401 fsum3ser 11404 fsumcl2lem 11405 fsumcl 11407 fsumadd 11413 fsumsplit 11414 sumsnf 11416 sumsplitdc 11439 fsummulc2 11455 ef0lem 11667 ef4p 11701 tanvalap 11715 modprm0 12253 pcmpt2 12341 4sqlem10 12384 fsumcncntop 14026 limcimolemlt 14103 dvmptcmulcn 14153 dveflem 14157 dvef 14158 ptolemy 14215 lgsdir2 14404 lgsdir 14406 apdiff 14766 iswomni0 14769 |
Copyright terms: Public domain | W3C validator |