ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  cnre GIF version

Theorem cnre 7762
Description: Alias for ax-cnre 7731, for naming consistency. (Contributed by NM, 3-Jan-2013.)
Assertion
Ref Expression
cnre (𝐴 ∈ ℂ → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝐴 = (𝑥 + (i · 𝑦)))
Distinct variable group:   𝑥,𝐴,𝑦

Proof of Theorem cnre
StepHypRef Expression
1 ax-cnre 7731 1 (𝐴 ∈ ℂ → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝐴 = (𝑥 + (i · 𝑦)))
Colors of variables: wff set class
Syntax hints:  wi 4   = wceq 1331  wcel 1480  wrex 2417  (class class class)co 5774  cc 7618  cr 7619  ici 7622   + caddc 7623   · cmul 7625
This theorem was proved from axioms:  ax-cnre 7731
This theorem is referenced by:  mulid1  7763  cnegexlem2  7938  cnegex  7940  apirr  8367  apsym  8368  apcotr  8369  apadd1  8370  apneg  8373  mulext1  8374  apti  8384  recexap  8414  creur  8717  creui  8718  cju  8719  cnref1o  9440  replim  10631  cjap  10678
  Copyright terms: Public domain W3C validator