Theorem cnre 8286

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

Syntax hints:   → wi 4   = wceq 1398   ∈ wcel 2205  ∃wrex 2523  (class class class)co 6058  ℂcc 8141  ℝcr 8142  ici 8145   + caddc 8146   · cmul 8148

This theorem was proved from axioms:  ax-cnre 8254

This theorem is referenced by:  mulrid  8287  cnegexlem2  8466  cnegex  8468  apirr  8897  apsym  8898  apcotr  8899  apadd1  8900  apneg  8903  mulext1  8904  apti  8914  recexap  8945  creur  9253  creui  9254  cju  9255  cnref1o  10004  replim  11572  cjap  11619