logo

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