![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > 0cnd | GIF version |
Description: 0 is a complex number, deductive form. (Contributed by David A. Wheeler, 8-Dec-2018.) |
Ref | Expression |
---|---|
0cnd | ⊢ (𝜑 → 0 ∈ ℂ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 0cn 7927 | . 2 ⊢ 0 ∈ ℂ | |
2 | 1 | a1i 9 | 1 ⊢ (𝜑 → 0 ∈ ℂ) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∈ wcel 2148 ℂcc 7787 0cc0 7789 |
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 7882 ax-icn 7884 ax-addcl 7885 ax-mulcl 7887 ax-i2m1 7894 |
This theorem depends on definitions: df-bi 117 df-cleq 2170 df-clel 2173 |
This theorem is referenced by: mulap0r 8549 mulap0 8587 mul0eqap 8603 diveqap0 8615 eqneg 8665 div2subap 8770 prodgt0 8785 un0addcl 9185 un0mulcl 9186 modsumfzodifsn 10369 ser0 10487 ser0f 10488 abs00ap 11042 abs00 11044 abssubne0 11071 mul0inf 11220 clim0c 11265 sumrbdclem 11356 summodclem2a 11360 zsumdc 11363 fsum3 11366 isumz 11368 isumss 11370 fisumss 11371 fsum3cvg2 11373 fsum3ser 11376 fsumcl2lem 11377 fsumcl 11379 fsumadd 11385 fsumsplit 11386 sumsnf 11388 sumsplitdc 11411 fsummulc2 11427 ef0lem 11639 ef4p 11673 tanvalap 11687 modprm0 12224 pcmpt2 12312 4sqlem10 12355 fsumcncntop 13689 limcimolemlt 13766 dvmptcmulcn 13816 dveflem 13820 dvef 13821 ptolemy 13878 lgsdir2 14067 lgsdir 14069 apdiff 14419 iswomni0 14422 |
Copyright terms: Public domain | W3C validator |