Theorem cnre 8175

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

Syntax hints:   → wi 4   = wceq 1397   ∈ wcel 2202  ∃wrex 2511  (class class class)co 6018  ℂcc 8030  ℝcr 8031  ici 8034   + caddc 8035   · cmul 8037

This theorem was proved from axioms:  ax-cnre 8143

This theorem is referenced by:  mulrid  8176  cnegexlem2  8355  cnegex  8357  apirr  8785  apsym  8786  apcotr  8787  apadd1  8788  apneg  8791  mulext1  8792  apti  8802  recexap  8833  creur  9139  creui  9140  cju  9141  cnref1o  9885  replim  11421  cjap  11468