Theorem cnre 11139

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

Syntax hints:   → wi 4   = wceq 1547   ∈ wcel 2119  ∃wrex 3064  (class class class)co 7363  ℂcc 11034  ℝcr 11035  ici 11038   + caddc 11039   · cmul 11041

This theorem was proved from axioms:  ax-cnre 11109

This theorem is referenced by:  mulrid  11140  1re  11142  0re  11144  mul02  11322  cnegex  11325  0cnALT  11379  recex  11780  creur  12151  creui  12152  cju  12153  cnref1o  12933  replim  15076  ipasslem11  30936  sn-addlid  42882  sn-it0e0  42894  sn-negex12  42895  sn-mullid  42914  sn-0tie0  42942  sn-mul02  42943