# Metamath Proof Explorer

## Theorem 0cnALT2

Description: Alternate proof of 0cnALT which is shorter, but depends on ax-8 , ax-13 , ax-sep , ax-nul , ax-pow , ax-pr , ax-un , and every complex number axiom except ax-pre-mulgt0 and ax-pre-sup . (Contributed by NM, 19-Feb-2005) (Revised by Mario Carneiro, 27-May-2016) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion 0cnALT2 ${⊢}0\in ℂ$

### Proof

Step Hyp Ref Expression
1 ax-icn ${⊢}\mathrm{i}\in ℂ$
2 cnegex ${⊢}\mathrm{i}\in ℂ\to \exists {x}\in ℂ\phantom{\rule{.4em}{0ex}}\mathrm{i}+{x}=0$
3 1 2 ax-mp ${⊢}\exists {x}\in ℂ\phantom{\rule{.4em}{0ex}}\mathrm{i}+{x}=0$
4 addcl ${⊢}\left(\mathrm{i}\in ℂ\wedge {x}\in ℂ\right)\to \mathrm{i}+{x}\in ℂ$
5 1 4 mpan ${⊢}{x}\in ℂ\to \mathrm{i}+{x}\in ℂ$
6 eleq1 ${⊢}\mathrm{i}+{x}=0\to \left(\mathrm{i}+{x}\in ℂ↔0\in ℂ\right)$
7 5 6 syl5ibcom ${⊢}{x}\in ℂ\to \left(\mathrm{i}+{x}=0\to 0\in ℂ\right)$
8 7 rexlimiv ${⊢}\exists {x}\in ℂ\phantom{\rule{.4em}{0ex}}\mathrm{i}+{x}=0\to 0\in ℂ$
9 3 8 ax-mp ${⊢}0\in ℂ$