Theorem cnre 7755

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

Syntax hints:   → wi 4   = wceq 1331   ∈ wcel 1480  ∃wrex 2415  (class class class)co 5767  ℂcc 7611  ℝcr 7612  ici 7615   + caddc 7616   · cmul 7618

This theorem was proved from axioms:  ax-cnre 7724

This theorem is referenced by:  mulid1  7756  cnegexlem2  7931  cnegex  7933  apirr  8360  apsym  8361  apcotr  8362  apadd1  8363  apneg  8366  mulext1  8367  apti  8377  recexap  8407  creur  8710  creui  8711  cju  8712  cnref1o  9433  replim  10624  cjap  10671