Theorem cnre 11332

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∈ wcel 2147  ∃wrex 3090  (class class class)co 7443  ℂcc 11225  ℝcr 11226  ici 11229   + caddc 11230   · cmul 11232

This proof depends on axioms:  ax-cnre 11300

This theorem is used by:  mulrid  11333  1re  11335  0re  11337  mul02  11515  cnegex  11518  0cnALT  11572  recex  11975  creur  12341  creui  12342  cju  12343  cnref1o  13140  replim  15312  ipasslem11  31472  sn-addlid  43648  sn-it0e0  43660  sn-negex12  43661  sn-mullid  43680  sn-0tie0  43708  sn-mul02  43709