Theorem cnre 11306

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

This proof depends on syntax axioms:   → wi 4   = wceq 1569   ∈ wcel 2144  ∃wrex 3086  (class class class)co 7420  ℂcc 11199  ℝcr 11200  ici 11203   + caddc 11204   · cmul 11206

This proof depends on axioms:  ax-cnre 11274

This theorem is used by:  mulrid  11307  1re  11309  0re  11311  mul02  11489  cnegex  11492  0cnALT  11546  recex  11949  creur  12315  creui  12316  cju  12317  cnref1o  13114  replim  15284  ipasslem11  31443  sn-addlid  43531  sn-it0e0  43543  sn-negex12  43544  sn-mullid  43563  sn-0tie0  43591  sn-mul02  43592