Theorem cnre 11237

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

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2109  ∃wrex 3061  (class class class)co 7410  ℂcc 11132  ℝcr 11133  ici 11136   + caddc 11137   · cmul 11139

This theorem was proved from axioms:  ax-cnre 11207

This theorem is referenced by:  mulrid  11238  1re  11240  0re  11242  mul02  11418  cnegex  11421  0cnALT  11475  recex  11874  creur  12239  creui  12240  cju  12241  cnref1o  13006  replim  15140  ipasslem11  30826  sn-addlid  42414  sn-it0e0  42425  sn-negex12  42426  sn-mullid  42445  sn-0tie0  42449  sn-mul02  42450