Theorem cnre 8138

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

Syntax hints:   → wi 4   = wceq 1395   ∈ wcel 2200  ∃wrex 2509  (class class class)co 6000  ℂcc 7993  ℝcr 7994  ici 7997   + caddc 7998   · cmul 8000

This theorem was proved from axioms:  ax-cnre 8106

This theorem is referenced by:  mulrid  8139  cnegexlem2  8318  cnegex  8320  apirr  8748  apsym  8749  apcotr  8750  apadd1  8751  apneg  8754  mulext1  8755  apti  8765  recexap  8796  creur  9102  creui  9103  cju  9104  cnref1o  9842  replim  11365  cjap  11412