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

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

In [2]:
%proving transitivity_less_eq_less

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

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

defaults.assumptions:
In [4]:
less_eq_def

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

spec_l_e_d:
In [6]:
spec_l_e_d.derive_right_via_equality()

In [7]:
xeq_y = Less(x,z).prove(assumptions = (Equals(x,y), Less(y,z)))

xeq_y: ,  ⊢
In [8]:
xless_y = Less(x,z).prove(assumptions = (Less(x,y), Less(y,z)))

xless_y: ,  ⊢
In [9]:
spec_l_e_d.rhs.derive_via_dilemma(Less(x,z))

In [10]:
%qed

proveit.numbers.ordering.transitivity_less_eq_less has been proven.

Out[10]:
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, 17,  ⊢
: , : , :
11instantiation16, 17, 18,  ⊢
: , : , :
12conjecture
proveit.logic.booleans.in_bool_if_true
13instantiation19, 20, 21
: , :
14axiom
proveit.numbers.ordering.transitivity_less_less
15assumption
16theorem
proveit.logic.equality.sub_left_side_into
17assumption
18assumption
19theorem
proveit.logic.equality.rhs_via_equality
20assumption
21instantiation22
: , :
22axiom
proveit.numbers.ordering.less_eq_def