Theorem cnre 11232

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∈ wcel 2145  ∃wrex 3088  (class class class)co 7416  ℂcc 11125  ℝcr 11126  ici 11129   + caddc 11130   · cmul 11132

This proof depends on axioms:  ax-cnre 11200

This theorem is used by:  mulrid  11233  1re  11235  0re  11237  mul02  11415  cnegex  11418  0cnALT  11472  recex  11873  creur  12239  creui  12240  cju  12241  cnref1o  13037  replim  15205  ipasslem11  31322  sn-addlid  43281  sn-it0e0  43293  sn-negex12  43294  sn-mullid  43313  sn-0tie0  43341  sn-mul02  43342