Theorem cnre 10036

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

Syntax hints:   → wi 4   = wceq 1483   ∈ wcel 1990  ∃wrex 2913  (class class class)co 6650  ℂcc 9934  ℝcr 9935  ici 9938   + caddc 9939   · cmul 9941

This theorem was proved from axioms:  ax-cnre 10009

This theorem is referenced by:  mulid1  10037  1re  10039  mul02  10214  cnegex  10217  recex  10659  creur  11014  creui  11015  cju  11016  cnref1o  11827  replim  13856  ipasslem11  27695