Theorem cnre 11168

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

Syntax hints:   → wi 4   = wceq 1554   ∈ wcel 2136  ∃wrex 3080  (class class class)co 7385  ℂcc 11061  ℝcr 11062  ici 11065   + caddc 11066   · cmul 11068

This theorem was proved from axioms:  ax-cnre 11136

This theorem is referenced by:  mulrid  11169  1re  11171  0re  11173  mul02  11351  cnegex  11354  0cnALT  11408  recex  11809  creur  12179  creui  12180  cju  12181  cnref1o  12976  replim  15119  ipasslem11  30982  sn-addlid  42961  sn-it0e0  42973  sn-negex12  42974  sn-mullid  42993  sn-0tie0  43021  sn-mul02  43022