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

Theorem negcl 7974
Description: Closure law for negative. (Contributed by NM, 6-Aug-2003.)
Assertion
Ref Expression
negcl (𝐴 ∈ ℂ → -𝐴 ∈ ℂ)

Proof of Theorem negcl
StepHypRef Expression
1 df-neg 7948 . 2 -𝐴 = (0 − 𝐴)
2 0cn 7770 . . 3 0 ∈ ℂ
3 subcl 7973 . . 3 ((0 ∈ ℂ ∧ 𝐴 ∈ ℂ) → (0 − 𝐴) ∈ ℂ)
42, 3mpan 420 . 2 (𝐴 ∈ ℂ → (0 − 𝐴) ∈ ℂ)
51, 4eqeltrid 2226 1 (𝐴 ∈ ℂ → -𝐴 ∈ ℂ)
Colors of variables: wff set class
Syntax hints:  wi 4  wcel 1480  (class class class)co 5774  cc 7630  0cc0 7632  cmin 7945  -cneg 7946
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 603  ax-in2 604  ax-io 698  ax-5 1423  ax-7 1424  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-8 1482  ax-10 1483  ax-11 1484  ax-i12 1485  ax-bndl 1486  ax-4 1487  ax-14 1492  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-ext 2121  ax-sep 4046  ax-pow 4098  ax-pr 4131  ax-setind 4452  ax-resscn 7724  ax-1cn 7725  ax-icn 7727  ax-addcl 7728  ax-addrcl 7729  ax-mulcl 7730  ax-addcom 7732  ax-addass 7734  ax-distr 7736  ax-i2m1 7737  ax-0id 7740  ax-rnegex 7741  ax-cnre 7743
This theorem depends on definitions:  df-bi 116  df-3an 964  df-tru 1334  df-fal 1337  df-nf 1437  df-sb 1736  df-eu 2002  df-mo 2003  df-clab 2126  df-cleq 2132  df-clel 2135  df-nfc 2270  df-ne 2309  df-ral 2421  df-rex 2422  df-reu 2423  df-rab 2425  df-v 2688  df-sbc 2910  df-dif 3073  df-un 3075  df-in 3077  df-ss 3084  df-pw 3512  df-sn 3533  df-pr 3534  df-op 3536  df-uni 3737  df-br 3930  df-opab 3990  df-id 4215  df-xp 4545  df-rel 4546  df-cnv 4547  df-co 4548  df-dm 4549  df-iota 5088  df-fun 5125  df-fv 5131  df-riota 5730  df-ov 5777  df-oprab 5778  df-mpo 5779  df-sub 7947  df-neg 7948
This theorem is referenced by:  negicn  7975  negcon1  8026  negdi  8031  negdi2  8032  negsubdi2  8033  neg2sub  8034  negcli  8042  negcld  8072  mulneg2  8170  mul2neg  8172  mulsub  8175  apsub1  8416  subap0  8417  divnegap  8478  divsubdirap  8480  divsubdivap  8500  eqneg  8504  div2negap  8507  divneg2ap  8508  zeo  9168  sqneg  10364  binom2sub  10417  shftval4  10612  shftcan1  10618  shftcan2  10619  crim  10642  resub  10654  imsub  10662  cjneg  10674  cjsub  10676  absneg  10834  abs2dif2  10891  subcn2  11092  efcan  11394  efap0  11395  efne0  11396  efneg  11397  efsub  11399  sinneg  11444  cosneg  11445  tannegap  11446  efmival  11451  sinsub  11458  cossub  11459  sincossq  11466  sin2pim  12916  cos2pim  12917  rpcxpsub  13008
  Copyright terms: Public domain W3C validator