# Proof of proveit.numbers.ordering.transitivity_less_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 Less
from proveit.numbers.ordering  import less_eq_def
theory = proveit.Theory() # the theorem's theory

In [2]:
%proving transitivity_less_less_eq

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

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

defaults.assumptions:
In [4]:
spec_l_e_d = less_eq_def.instantiate({x:y, y:z})

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

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

yeq_z: ,  ⊢
In [7]:
yless_z = Less(x,z).prove(assumptions = (Less(y,z), Less(x,y)))

yless_z: ,  ⊢
In [8]:
spec_l_e_d.rhs.derive_via_dilemma(Less(x,z))

In [9]:
%qed

proveit.numbers.ordering.transitivity_less_less_eq has been proven.

Out[9]:
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, 17, 15,  ⊢
: , : , :
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_right_side_into
17assumption
18assumption
19theorem
proveit.logic.equality.rhs_via_equality
20assumption
21instantiation22
: , :
22axiom
proveit.numbers.ordering.less_eq_def