# Proof of proveit.numbers.ordering.transitivity_less_eq_less_eq theorem¶

In [1]:
import proveit
from proveit import defaults
from proveit import x, y, z
from proveit.logic import Equals
from proveit.numbers import LessEq, Less
from proveit.numbers.ordering  import less_eq_def
from proveit.numbers.ordering import transitivity_less_less_eq
theory = proveit.Theory() # the theorem's theory

In [2]:
%proving transitivity_less_eq_less_eq

With these allowed/disallowed theorem/theory presumptions (e.g., to avoid circular dependencies), we begin our proof of
transitivity_less_eq_less_eq:
(see dependencies)
transitivity_less_eq_less_eq may now be readily provable (assuming required theorems are usable).  Simply execute "%qed".

In [3]:
defaults.assumptions = transitivity_less_eq_less_eq.all_conditions()

defaults.assumptions:
In [4]:
less_eq_def

In [5]:
x_leq_y__expanded = less_eq_def.instantiate({x:x, y:y}).derive_right_via_equality()

x_leq_y__expanded:
In [6]:
x_less_y, x_eq_y = x_leq_y__expanded.operands

x_less_y:
x_eq_y:
In [7]:
transitivity_less_less_eq

In [8]:
x_less_z = transitivity_less_less_eq.instantiate({x:x, y:y, z:z}, assumptions=defaults.assumptions+(x_less_y,))

x_less_z: ,  ⊢
In [9]:
x_less_z.derive_relaxed()

In [10]:
x_eq_y.sub_left_side_into(LessEq(y, z), assumptions=defaults.assumptions+(x_eq_y,))

In [11]:
x_leq_y__expanded.derive_via_dilemma(LessEq(x, z))

In [12]:
%qed

proveit.numbers.ordering.transitivity_less_eq_less_eq has been proven.

Out[12]:
step typerequirementsstatement
0generalization1
1instantiation2, 3, 4, 13, 5, 6,  ⊢
: , : , :
2theorem
proveit.logic.booleans.disjunction.singular_constructive_dilemma
3instantiation7, 9
: , :
4instantiation8, 9
: , :
5deduction10
6deduction11
7axiom
proveit.logic.booleans.disjunction.left_in_bool
8axiom
proveit.logic.booleans.disjunction.right_in_bool
9instantiation12, 13
:
10instantiation14, 15,  ⊢
: , :
11instantiation16, 23, 17,  ⊢
: , : , :
12conjecture
proveit.logic.booleans.in_bool_if_true
13instantiation18, 19, 20
: , :
14conjecture
proveit.numbers.ordering.relax_less
15instantiation21, 22, 23,  ⊢
: , : , :
16theorem
proveit.logic.equality.sub_left_side_into
17assumption
18theorem
proveit.logic.equality.rhs_via_equality
19assumption
20instantiation24
: , :
21conjecture
proveit.numbers.ordering.transitivity_less_less_eq
22assumption
23assumption
24axiom
proveit.numbers.ordering.less_eq_def