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 7871 | . 2 | |
2 | 1 | a1i 9 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wcel 2128 cc 7731 cc0 7733 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-5 1427 ax-gen 1429 ax-ie1 1473 ax-ie2 1474 ax-4 1490 ax-17 1506 ax-ial 1514 ax-ext 2139 ax-1cn 7826 ax-icn 7828 ax-addcl 7829 ax-mulcl 7831 ax-i2m1 7838 |
This theorem depends on definitions: df-bi 116 df-cleq 2150 df-clel 2153 |
This theorem is referenced by: mulap0r 8491 mulap0 8529 mul0eqap 8545 diveqap0 8556 eqneg 8606 div2subap 8710 prodgt0 8724 un0addcl 9124 un0mulcl 9125 modsumfzodifsn 10299 ser0 10417 ser0f 10418 abs00ap 10966 abs00 10968 abssubne0 10995 mul0inf 11144 clim0c 11187 sumrbdclem 11278 summodclem2a 11282 zsumdc 11285 fsum3 11288 isumz 11290 isumss 11292 fisumss 11293 fsum3cvg2 11295 fsum3ser 11298 fsumcl2lem 11299 fsumcl 11301 fsumadd 11307 fsumsplit 11308 sumsnf 11310 sumsplitdc 11333 fsummulc2 11349 ef0lem 11561 ef4p 11595 tanvalap 11609 modprm0 12133 fsumcncntop 12998 limcimolemlt 13075 dvmptcmulcn 13125 dveflem 13129 dvef 13130 ptolemy 13187 apdiff 13661 iswomni0 13664 |
Copyright terms: Public domain | W3C validator |