Theorem cnre 7786

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

Syntax hints:   → wi 4   = wceq 1332   ∈ wcel 1481  ∃wrex 2418  (class class class)co 5782  ℂcc 7642  ℝcr 7643  ici 7646   + caddc 7647   · cmul 7649

This theorem was proved from axioms:  ax-cnre 7755

This theorem is referenced by:  mulid1  7787  cnegexlem2  7962  cnegex  7964  apirr  8391  apsym  8392  apcotr  8393  apadd1  8394  apneg  8397  mulext1  8398  apti  8408  recexap  8438  creur  8741  creui  8742  cju  8743  cnref1o  9469  replim  10663  cjap  10710