Theorem cnre 8068

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

Syntax hints:   → wi 4   = wceq 1373   ∈ wcel 2176  ∃wrex 2485  (class class class)co 5944  ℂcc 7923  ℝcr 7924  ici 7927   + caddc 7928   · cmul 7930

This theorem was proved from axioms:  ax-cnre 8036

This theorem is referenced by:  mulrid  8069  cnegexlem2  8248  cnegex  8250  apirr  8678  apsym  8679  apcotr  8680  apadd1  8681  apneg  8684  mulext1  8685  apti  8695  recexap  8726  creur  9032  creui  9033  cju  9034  cnref1o  9772  replim  11170  cjap  11217