Theorem cnre 7955

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

Syntax hints:   → wi 4   = wceq 1353   ∈ wcel 2148  ∃wrex 2456  (class class class)co 5877  ℂcc 7811  ℝcr 7812  ici 7815   + caddc 7816   · cmul 7818

This theorem was proved from axioms:  ax-cnre 7924

This theorem is referenced by:  mulrid  7956  cnegexlem2  8135  cnegex  8137  apirr  8564  apsym  8565  apcotr  8566  apadd1  8567  apneg  8570  mulext1  8571  apti  8581  recexap  8612  creur  8918  creui  8919  cju  8920  cnref1o  9652  replim  10870  cjap  10917