# Demonstrations for the theory of proveit.numbers.negation¶

In [1]:
import proveit
from proveit import defaults
from proveit import a, b, c, d, x
from proveit.logic import InSet
from proveit.numbers import zero, one, Neg, Mult, Add, subtract
from proveit.numbers.number_sets import (
Natural, NaturalPos,
Integer, IntegerNonZero, IntegerNeg, IntegerNonPos,
Rational, RationalNonZero, RationalPos, RationalNeg,
RationalNonNeg, RationalNonPos,
Real, RealNonZero, RealPos, RealNeg, RealNonNeg, RealNonPos,
Complex, ComplexNonZero)
%begin demonstrations

In [2]:
defaults.assumptions = [InSet(a, Complex), InSet(b, Complex),
InSet(c, Complex), InSet(d, Complex)]

defaults.assumptions:

### Simplification / evaluation¶

In [3]:
Neg(zero).evaluation()

In [4]:
Neg(Neg(one)).evaluation()

In [5]:
Neg(Neg(c)).simplification()


### Factorization¶

In [6]:
Neg(a).factorization(a, auto_simplify=False)

In [7]:
Neg(Mult(a, b, c, d)).factorization(b, auto_simplify=False)

, , ,  ⊢

### Distribution¶

In [8]:
Neg(Add(a, b, c)).distribution()

, ,  ⊢
In [9]:
Neg(Add(Neg(a), b, Neg(c))).distribution()

, ,  ⊢
In [10]:
Neg(Add(Neg(a), c)).distribution()

In [11]:
Neg(subtract(d, c)).distribution()


### Closure demonstrations¶

In [12]:
InSet(Neg(x), Natural).prove(assumptions=[InSet(x, IntegerNonPos)])

In [13]:
InSet(Neg(x), NaturalPos).prove(assumptions=[InSet(x, IntegerNeg)])

In [14]:
InSet(Neg(x), Integer).prove(assumptions=[InSet(x, Integer)])

In [15]:
InSet(Neg(x), IntegerNonZero).prove(assumptions=[InSet(x, IntegerNonZero)])

In [16]:
InSet(Neg(x), IntegerNeg).prove(assumptions=[InSet(x, NaturalPos)])

In [17]:
InSet(Neg(x), IntegerNonPos).prove(assumptions=[InSet(x, Natural)])

In [18]:
InSet(Neg(x), Rational).prove(assumptions=[InSet(x, Rational)])

In [19]:
InSet(Neg(x), RationalNonZero).prove(assumptions=[InSet(x, RationalNonZero)])

In [20]:
InSet(Neg(x), RationalPos).prove(assumptions=[InSet(x, RationalNeg)])

In [21]:
InSet(Neg(x), RationalNeg).prove(assumptions=[InSet(x, RationalPos)])

In [22]:
InSet(Neg(x), RationalNonNeg).prove(assumptions=[InSet(x, RationalNonPos)])

In [23]:
InSet(Neg(x), RationalNonPos).prove(assumptions=[InSet(x, RationalNonNeg)])

In [24]:
InSet(Neg(x), Real).prove(assumptions=[InSet(x, Real)])

In [25]:
InSet(Neg(x), RealNonZero).prove(assumptions=[InSet(x, RealNonZero)])

In [26]:
InSet(Neg(x), RealPos).prove(assumptions=[InSet(x, RealNeg)])

In [27]:
InSet(Neg(x), RealNeg).prove(assumptions=[InSet(x, RealPos)])

In [28]:
InSet(Neg(x), RealNonNeg).prove(assumptions=[InSet(x, RealNonPos)])

In [29]:
InSet(Neg(x), RealNonPos).prove(assumptions=[InSet(x, RealNonNeg)])


### Bounding demonstrations¶

In [30]:
import sys
from proveit import a, b, c, d, x, y
from proveit.numbers import greater, greater_eq, Less, LessEq

In [31]:
defaults.assumptions = [InSet(a, Real), InSet(b, Real), InSet(c, Real), InSet(d, Real),
greater(a, b), LessEq(c, d)]

defaults.assumptions:
In [32]:
Neg(a).bound_via_operand_bound(greater(a, b))

, ,  ⊢
In [33]:
Neg(c).bound_via_operand_bound(LessEq(c, d))

, ,  ⊢
In [34]:
%end demonstrations