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 7726 | . 2 | |
2 | 1 | a1i 9 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wcel 1465 cc 7586 cc0 7588 |
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 1408 ax-gen 1410 ax-ie1 1454 ax-ie2 1455 ax-4 1472 ax-17 1491 ax-ial 1499 ax-ext 2099 ax-1cn 7681 ax-icn 7683 ax-addcl 7684 ax-mulcl 7686 ax-i2m1 7693 |
This theorem depends on definitions: df-bi 116 df-cleq 2110 df-clel 2113 |
This theorem is referenced by: mulap0r 8344 mulap0 8382 mul0eqap 8398 diveqap0 8409 eqneg 8459 div2subap 8563 prodgt0 8574 un0addcl 8968 un0mulcl 8969 modsumfzodifsn 10124 ser0 10242 ser0f 10243 abs00ap 10789 abs00 10791 abssubne0 10818 mul0inf 10967 clim0c 11010 sumrbdclem 11100 summodclem2a 11105 zsumdc 11108 fsum3 11111 isumz 11113 isumss 11115 fisumss 11116 fsum3cvg2 11118 fsum3ser 11121 fsumcl2lem 11122 fsumcl 11124 fsumadd 11130 fsumsplit 11131 sumsnf 11133 sumsplitdc 11156 fsummulc2 11172 ef0lem 11280 ef4p 11314 tanvalap 11329 fsumcncntop 12636 limcimolemlt 12713 dvmptcmulcn 12763 dveflem 12766 dvef 12767 ptolemy 12816 |
Copyright terms: Public domain | W3C validator |