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

Theorem cnre 7952
Description: Alias for ax-cnre 7921, 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 7921 1 (𝐴 ∈ ℂ → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝐴 = (𝑥 + (i · 𝑦)))
Colors of variables: wff set class
Syntax hints:  wi 4   = wceq 1353  wcel 2148  wrex 2456  (class class class)co 5874  cc 7808  cr 7809  ici 7812   + caddc 7813   · cmul 7815
This theorem was proved from axioms:  ax-cnre 7921
This theorem is referenced by:  mulrid  7953  cnegexlem2  8131  cnegex  8133  apirr  8560  apsym  8561  apcotr  8562  apadd1  8563  apneg  8566  mulext1  8567  apti  8577  recexap  8608  creur  8914  creui  8915  cju  8916  cnref1o  9648  replim  10863  cjap  10910
  Copyright terms: Public domain W3C validator