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  8502  cnegex  8504  apirr  8934  apsym  8935  apcotr  8936  apadd1  8937  apneg  8940  mulext1  8941  apti  8951  recexap  8982  creur  9290  creui  9291  cju  9292  cnref1o  10053  replim  11626  cjap  11674