Theorem cnre 9915

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

Syntax hints:   → wi 4   = wceq 1475   ∈ wcel 1977  ∃wrex 2897  (class class class)co 6549  ℂcc 9813  ℝcr 9814  ici 9817   + caddc 9818   · cmul 9820

This theorem was proved from axioms:  ax-cnre 9888

This theorem is referenced by:  mulid1  9916  1re  9918  mul02  10093  cnegex  10096  recex  10538  creur  10891  creui  10892  cju  10893  cnref1o  11703  replim  13704  ipasslem11  27079