Theorem cnre 8168

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

Syntax hints:   → wi 4   = wceq 1395   ∈ wcel 2200  ∃wrex 2509  (class class class)co 6013  ℂcc 8023  ℝcr 8024  ici 8027   + caddc 8028   · cmul 8030

This theorem was proved from axioms:  ax-cnre 8136

This theorem is referenced by:  mulrid  8169  cnegexlem2  8348  cnegex  8350  apirr  8778  apsym  8779  apcotr  8780  apadd1  8781  apneg  8784  mulext1  8785  apti  8795  recexap  8826  creur  9132  creui  9133  cju  9134  cnref1o  9878  replim  11413  cjap  11460