Theorem cnre 8322

Description: Alias for ax-cnre 8290, 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 8290	1 ⊢ (𝐴 ∈ ℂ → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝐴 = (𝑥 + (i · 𝑦)))

This proof depends on syntax axioms:   → wi 4   = wceq 1402   ∈ wcel 2209  ∃wrex 2529  (class class class)co 6085  ℂcc 8177  ℝcr 8178  ici 8181   + caddc 8182   · cmul 8184

This proof depends on axioms:  ax-cnre 8290

This theorem is used by:  mulrid  8323  cnegexlem2  8503  cnegex  8505  apirr  8935  apsym  8936  apcotr  8937  apadd1  8938  apneg  8941  mulext1  8942  apti  8952  recexap  8983  creur  9291  creui  9292  cju  9293  cnref1o  10061  replim  11638  cjap  11686