Theorem cnre 8328

Description: Alias for ax-cnre 8296, for naming consistency. (Contributed by NM, 3-Jan-2013.)

Assertion

Ref	Expression
cnre	⊢ (𝐴 ∈ ℂ → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝐴 = (𝑥 + (i · 𝑦)))

Distinct variable group:   𝑥,𝐴,𝑦

Proof of Theorem cnre

Step	Hyp	Ref	Expression
1		ax-cnre 8296	1 ⊢ (𝐴 ∈ ℂ → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝐴 = (𝑥 + (i · 𝑦)))

This proof depends on syntax axioms:   → wi 4   = wceq 1402   ∈ wcel 2209  ∃wrex 2529  (class class class)co 6088  ℂcc 8183  ℝcr 8184  ici 8187   + caddc 8188   · cmul 8190

This proof depends on axioms:  ax-cnre 8296

This theorem is used by:  mulrid  8329  cnegexlem2  8509  cnegex  8511  apirr  8941  apsym  8942  apcotr  8943  apadd1  8944  apneg  8947  mulext1  8948  apti  8958  recexap  8989  creur  9297  creui  9298  cju  9299  cnref1o  10067  replim  11645  cjap  11693