Theorem cnre 7952

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

Syntax hints:   → wi 4   = wceq 1353   ∈ wcel 2148  ∃wrex 2456  (class class class)co 5874  ℂcc 7808  ℝcr 7809  ici 7812   + caddc 7813   · cmul 7815

This theorem was proved from axioms:  ax-cnre 7921

This theorem is referenced by:  mulrid  7953  cnegexlem2  8131  cnegex  8133  apirr  8560  apsym  8561  apcotr  8562  apadd1  8563  apneg  8566  mulext1  8567  apti  8577  recexap  8608  creur  8914  creui  8915  cju  8916  cnref1o  9648  replim  10863  cjap  10910