Theorem cnre 8316

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

Syntax hints:   → wi 4   = wceq 1402   ∈ wcel 2209  ∃wrex 2529  (class class class)co 6079  ℂcc 8171  ℝcr 8172  ici 8175   + caddc 8176   · cmul 8178

This theorem was proved from axioms:  ax-cnre 8284

This theorem is referenced by:  mulrid  8317  cnegexlem2  8496  cnegex  8498  apirr  8927  apsym  8928  apcotr  8929  apadd1  8930  apneg  8933  mulext1  8934  apti  8944  recexap  8975  creur  9283  creui  9284  cju  9285  cnref1o  10034  replim  11607  cjap  11655