This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ∈ ℂ

Proof

Step Hyp Ref Expression
1 ax-icn ⊢ i ∈ ℂ
2 cnegex ⊢ ( i ∈ ℂ → ∃ 𝑥 ∈ ℂ ( i + 𝑥 ) = 0 )
3 1 2 ax-mp ⊢ ∃ 𝑥 ∈ ℂ ( i + 𝑥 ) = 0
4 addcl ⊢ ( ( i ∈ ℂ ∧ 𝑥 ∈ ℂ ) → ( i + 𝑥 ) ∈ ℂ )
5 1 4 mpan ⊢ ( 𝑥 ∈ ℂ → ( i + 𝑥 ) ∈ ℂ )
6 eleq1 ⊢ ( ( i + 𝑥 ) = 0 → ( ( i + 𝑥 ) ∈ ℂ ↔ 0 ∈ ℂ ) )
7 5 6 syl5ibcom ⊢ ( 𝑥 ∈ ℂ → ( ( i + 𝑥 ) = 0 → 0 ∈ ℂ ) )
8 7 rexlimiv ⊢ ( ∃ 𝑥 ∈ ℂ ( i + 𝑥 ) = 0 → 0 ∈ ℂ )
9 3 8 ax-mp ⊢ 0 ∈ ℂ