# Metamath Proof Explorer

## Theorem 0cnALT

Description: Alternate proof of 0cn which does not reference ax-1cn . (Contributed by NM, 19-Feb-2005) (Revised by Mario Carneiro, 27-May-2016) Reduce dependencies on axioms. (Revised by Steven Nguyen, 7-Jan-2022) (Proof modification is discouraged.) (New usage is discouraged.)

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

### Proof

Step Hyp Ref Expression
1 ax-icn ${⊢}\mathrm{i}\in ℂ$
2 cnre ${⊢}\mathrm{i}\in ℂ\to \exists {x}\in ℝ\phantom{\rule{.4em}{0ex}}\exists {y}\in ℝ\phantom{\rule{.4em}{0ex}}\mathrm{i}={x}+\mathrm{i}{y}$
3 ax-rnegex ${⊢}{x}\in ℝ\to \exists {z}\in ℝ\phantom{\rule{.4em}{0ex}}{x}+{z}=0$
4 readdcl ${⊢}\left({x}\in ℝ\wedge {z}\in ℝ\right)\to {x}+{z}\in ℝ$
5 eleq1 ${⊢}{x}+{z}=0\to \left({x}+{z}\in ℝ↔0\in ℝ\right)$
6 4 5 syl5ibcom ${⊢}\left({x}\in ℝ\wedge {z}\in ℝ\right)\to \left({x}+{z}=0\to 0\in ℝ\right)$
7 6 rexlimdva ${⊢}{x}\in ℝ\to \left(\exists {z}\in ℝ\phantom{\rule{.4em}{0ex}}{x}+{z}=0\to 0\in ℝ\right)$
8 3 7 mpd ${⊢}{x}\in ℝ\to 0\in ℝ$
9 8 adantr ${⊢}\left({x}\in ℝ\wedge \exists {y}\in ℝ\phantom{\rule{.4em}{0ex}}\mathrm{i}={x}+\mathrm{i}{y}\right)\to 0\in ℝ$
10 9 rexlimiva ${⊢}\exists {x}\in ℝ\phantom{\rule{.4em}{0ex}}\exists {y}\in ℝ\phantom{\rule{.4em}{0ex}}\mathrm{i}={x}+\mathrm{i}{y}\to 0\in ℝ$
11 1 2 10 mp2b ${⊢}0\in ℝ$
12 11 recni ${⊢}0\in ℂ$