Theorem cnre 11211

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

Syntax hints:   → wi 4   = wceq 1542   ∈ wcel 2107  ∃wrex 3071  (class class class)co 7409  ℂcc 11108  ℝcr 11109  ici 11112   + caddc 11113   · cmul 11115

This theorem was proved from axioms:  ax-cnre 11183

This theorem is referenced by:  mulrid  11212  1re  11214  0re  11216  mul02  11392  cnegex  11395  0cnALT  11448  recex  11846  creur  12206  creui  12207  cju  12208  cnref1o  12969  replim  15063  ipasslem11  30093  sn-addlid  41277  sn-it0e0  41288  sn-negex12  41289  sn-mullid  41308  sn-0tie0  41312  sn-mul02  41313