Theorem cnre 8275

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

Syntax hints:   → wi 4   = wceq 1398   ∈ wcel 2205  ∃wrex 2523  (class class class)co 6052  ℂcc 8130  ℝcr 8131  ici 8134   + caddc 8135   · cmul 8137

This theorem was proved from axioms:  ax-cnre 8243

This theorem is referenced by:  mulrid  8276  cnegexlem2  8454  cnegex  8456  apirr  8884  apsym  8885  apcotr  8886  apadd1  8887  apneg  8890  mulext1  8891  apti  8901  recexap  8932  creur  9238  creui  9239  cju  9240  cnref1o  9989  replim  11552  cjap  11599