Theorem cnre 11101

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

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2110  ∃wrex 3054  (class class class)co 7341  ℂcc 10996  ℝcr 10997  ici 11000   + caddc 11001   · cmul 11003

This theorem was proved from axioms:  ax-cnre 11071

This theorem is referenced by:  mulrid  11102  1re  11104  0re  11106  mul02  11283  cnegex  11286  0cnALT  11340  recex  11741  creur  12111  creui  12112  cju  12113  cnref1o  12875  replim  15015  ipasslem11  30810  sn-addlid  42416  sn-it0e0  42428  sn-negex12  42429  sn-mullid  42448  sn-0tie0  42463  sn-mul02  42464