Theorem cnre 11211

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

This proof depends on syntax axioms:   → wi 4   = wceq 1569   ∈ wcel 2142  ∃wrex 3088  (class class class)co 7412  ℂcc 11104  ℝcr 11105  ici 11108   + caddc 11109   · cmul 11111

This proof depends on axioms:  ax-cnre 11179

This theorem is used by:  mulrid  11212  1re  11214  0re  11216  mul02  11394  cnegex  11397  0cnALT  11451  recex  11852  creur  12218  creui  12219  cju  12220  cnref1o  13015  replim  15174  ipasslem11  31203  sn-addlid  43193  sn-it0e0  43205  sn-negex12  43206  sn-mullid  43225  sn-0tie0  43253  sn-mul02  43254