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

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

Proof

Step Hyp Ref Expression
1 ax-icn ⊢ i ∈ ℂ
2 cnre ⊢ ( i ∈ ℂ → ∃ 𝑥 ∈ ℝ ∃ 𝑦 ∈ ℝ i = ( 𝑥 + ( i · 𝑦 ) ) )
3 ax-rnegex ⊢ ( 𝑥 ∈ ℝ → ∃ 𝑧 ∈ ℝ ( 𝑥 + 𝑧 ) = 0 )
4 readdcl ⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑧 ∈ ℝ ) → ( 𝑥 + 𝑧 ) ∈ ℝ )
5 eleq1 ⊢ ( ( 𝑥 + 𝑧 ) = 0 → ( ( 𝑥 + 𝑧 ) ∈ ℝ ↔ 0 ∈ ℝ ) )
6 4 5 syl5ibcom ⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑧 ∈ ℝ ) → ( ( 𝑥 + 𝑧 ) = 0 → 0 ∈ ℝ ) )
7 6 rexlimdva ⊢ ( 𝑥 ∈ ℝ → ( ∃ 𝑧 ∈ ℝ ( 𝑥 + 𝑧 ) = 0 → 0 ∈ ℝ ) )
8 3 7 mpd ⊢ ( 𝑥 ∈ ℝ → 0 ∈ ℝ )
9 8 adantr ⊢ ( ( 𝑥 ∈ ℝ ∧ ∃ 𝑦 ∈ ℝ i = ( 𝑥 + ( i · 𝑦 ) ) ) → 0 ∈ ℝ )
10 9 rexlimiva ⊢ ( ∃ 𝑥 ∈ ℝ ∃ 𝑦 ∈ ℝ i = ( 𝑥 + ( i · 𝑦 ) ) → 0 ∈ ℝ )
11 1 2 10 mp2b ⊢ 0 ∈ ℝ
12 11 recni ⊢ 0 ∈ ℂ