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

Theorem cnre 7177
Description: Alias for ax-cnre 7149, 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 7149 1 (𝐴 ∈ ℂ → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝐴 = (𝑥 + (i · 𝑦)))
Colors of variables: wff set class
Syntax hints:  wi 4   = wceq 1285  wcel 1434  wrex 2350  (class class class)co 5543  cc 7041  cr 7042  ici 7045   + caddc 7046   · cmul 7048
This theorem was proved from axioms:  ax-cnre 7149
This theorem is referenced by:  mulid1  7178  cnegexlem2  7351  cnegex  7353  apirr  7772  apsym  7773  apcotr  7774  apadd1  7775  apneg  7778  mulext1  7779  apti  7789  recexap  7810  creur  8103  creui  8104  cju  8105  cnref1o  8814  replim  9884  cjap  9931
  Copyright terms: Public domain W3C validator