Theorem cnre 11119

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

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2113  ∃wrex 3058  (class class class)co 7355  ℂcc 11014  ℝcr 11015  ici 11018   + caddc 11019   · cmul 11021

This theorem was proved from axioms:  ax-cnre 11089

This theorem is referenced by:  mulrid  11120  1re  11122  0re  11124  mul02  11301  cnegex  11304  0cnALT  11358  recex  11759  creur  12129  creui  12130  cju  12131  cnref1o  12893  replim  15033  ipasslem11  30831  sn-addlid  42512  sn-it0e0  42524  sn-negex12  42525  sn-mullid  42544  sn-0tie0  42559  sn-mul02  42560