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