Theorem cnre 8329

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

This proof depends on syntax axioms:   → wi 4   = wceq 1402   ∈ wcel 2209  ∃wrex 2529  (class class class)co 6088  ℂcc 8184  ℝcr 8185  ici 8188   + caddc 8189   · cmul 8191

This proof depends on axioms:  ax-cnre 8297

This theorem is used by:  mulrid  8330  cnegexlem2  8510  cnegex  8512  apirr  8942  apsym  8943  apcotr  8944  apadd1  8945  apneg  8948  mulext1  8949  apti  8959  recexap  8990  creur  9298  creui  9299  cju  9300  cnref1o  10069  replim  11647  cjap  11695