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

Theorem cnre 7463
Description: Alias for ax-cnre 7435, 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 7435 1 (𝐴 ∈ ℂ → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝐴 = (𝑥 + (i · 𝑦)))
Colors of variables: wff set class
Syntax hints:  wi 4   = wceq 1289  wcel 1438  wrex 2360  (class class class)co 5634  cc 7327  cr 7328  ici 7331   + caddc 7332   · cmul 7334
This theorem was proved from axioms:  ax-cnre 7435
This theorem is referenced by:  mulid1  7464  cnegexlem2  7637  cnegex  7639  apirr  8058  apsym  8059  apcotr  8060  apadd1  8061  apneg  8064  mulext1  8065  apti  8075  recexap  8096  creur  8391  creui  8392  cju  8393  cnref1o  9102  replim  10258  cjap  10305
  Copyright terms: Public domain W3C validator