Theorem cnre 7115

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

Syntax hints:   → wi 4   = wceq 1284   ∈ wcel 1433  ∃wrex 2349  (class class class)co 5532  ℂcc 6979  ℝcr 6980  ici 6983   + caddc 6984   · cmul 6986

This theorem was proved from axioms:  ax-cnre 7087

This theorem is referenced by:  mulid1  7116  cnegexlem2  7284  cnegex  7286  apirr  7705  apsym  7706  apcotr  7707  apadd1  7708  apneg  7711  mulext1  7712  apti  7722  recexap  7743  creur  8036  creui  8037  cju  8038  cnref1o  8733  replim  9746  cjap  9793