Theorem cnre 7023

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

Syntax hints:   → wi 4   = wceq 1243   ∈ wcel 1393  ∃wrex 2307  (class class class)co 5512  ℂcc 6887  ℝcr 6888  ici 6891   + caddc 6892   · cmul 6894

This theorem was proved from axioms:  ax-cnre 6995

This theorem is referenced by:  mulid1  7024  cnegexlem2  7187  cnegex  7189  apirr  7596  apsym  7597  apcotr  7598  apadd1  7599  apneg  7602  mulext1  7603  apti  7613  recexap  7634  creur  7911  creui  7912  cju  7913  cnref1o  8582  replim  9459  cjap  9506