Theorem cnre 8022

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

Syntax hints:   → wi 4   = wceq 1364   ∈ wcel 2167  ∃wrex 2476  (class class class)co 5922  ℂcc 7877  ℝcr 7878  ici 7881   + caddc 7882   · cmul 7884

This theorem was proved from axioms:  ax-cnre 7990

This theorem is referenced by:  mulrid  8023  cnegexlem2  8202  cnegex  8204  apirr  8632  apsym  8633  apcotr  8634  apadd1  8635  apneg  8638  mulext1  8639  apti  8649  recexap  8680  creur  8986  creui  8987  cju  8988  cnref1o  9725  replim  11024  cjap  11071