Theorem leappend2 ≪ | index | src | ≫ 

theorem leappend2 (a b c: nat): $ b <= c <-> a ++ b <= a ++ c $;
StepHypRefExpression
1 id 
_1 = a -> _1 = a
2 1 appendeq1d 
_1 = a -> _1 ++ b = a ++ b
3 1 appendeq1d 
_1 = a -> _1 ++ c = a ++ c
4 2, 3 leeqd 
_1 = a -> (_1 ++ b <= _1 ++ c <-> a ++ b <= a ++ c)
5 4 bieq2d 
_1 = a -> (b <= c <-> _1 ++ b <= _1 ++ c <-> (b <= c <-> a ++ b <= a ++ c))
6 id 
_1 = 0 -> _1 = 0
7 6 appendeq1d 
_1 = 0 -> _1 ++ b = 0 ++ b
8 6 appendeq1d 
_1 = 0 -> _1 ++ c = 0 ++ c
9 7, 8 leeqd 
_1 = 0 -> (_1 ++ b <= _1 ++ c <-> 0 ++ b <= 0 ++ c)
10 9 bieq2d 
_1 = 0 -> (b <= c <-> _1 ++ b <= _1 ++ c <-> (b <= c <-> 0 ++ b <= 0 ++ c))
11 id 
_1 = a2 -> _1 = a2
12 11 appendeq1d 
_1 = a2 -> _1 ++ b = a2 ++ b
13 11 appendeq1d 
_1 = a2 -> _1 ++ c = a2 ++ c
14 12, 13 leeqd 
_1 = a2 -> (_1 ++ b <= _1 ++ c <-> a2 ++ b <= a2 ++ c)
15 14 bieq2d 
_1 = a2 -> (b <= c <-> _1 ++ b <= _1 ++ c <-> (b <= c <-> a2 ++ b <= a2 ++ c))
16 id 
_1 = a1 : a2 -> _1 = a1 : a2
17 16 appendeq1d 
_1 = a1 : a2 -> _1 ++ b = a1 : a2 ++ b
18 16 appendeq1d 
_1 = a1 : a2 -> _1 ++ c = a1 : a2 ++ c
19 17, 18 leeqd 
_1 = a1 : a2 -> (_1 ++ b <= _1 ++ c <-> a1 : a2 ++ b <= a1 : a2 ++ c)
20 19 bieq2d 
_1 = a1 : a2 -> (b <= c <-> _1 ++ b <= _1 ++ c <-> (b <= c <-> a1 : a2 ++ b <= a1 : a2 ++ c))
21 bicom 
(0 ++ b <= 0 ++ c <-> b <= c) -> (b <= c <-> 0 ++ b <= 0 ++ c)
22 leeq 
0 ++ b = b -> 0 ++ c = c -> (0 ++ b <= 0 ++ c <-> b <= c)
23 append0 
0 ++ b = b
24 22, 23 ax_mp 
0 ++ c = c -> (0 ++ b <= 0 ++ c <-> b <= c)
25 append0 
0 ++ c = c
26 24, 25 ax_mp 
0 ++ b <= 0 ++ c <-> b <= c
27 21, 26 ax_mp 
b <= c <-> 0 ++ b <= 0 ++ c
28 bitr4 
(a2 ++ b <= a2 ++ c <-> a1 : (a2 ++ b) <= a1 : (a2 ++ c)) ->
  (a1 : a2 ++ b <= a1 : a2 ++ c <-> a1 : (a2 ++ b) <= a1 : (a2 ++ c)) ->
  (a2 ++ b <= a2 ++ c <-> a1 : a2 ++ b <= a1 : a2 ++ c)
29 lecons2 
a2 ++ b <= a2 ++ c <-> a1 : (a2 ++ b) <= a1 : (a2 ++ c)
30 28, 29 ax_mp 
(a1 : a2 ++ b <= a1 : a2 ++ c <-> a1 : (a2 ++ b) <= a1 : (a2 ++ c)) -> (a2 ++ b <= a2 ++ c <-> a1 : a2 ++ b <= a1 : a2 ++ c)
31 leeq 
a1 : a2 ++ b = a1 : (a2 ++ b) -> a1 : a2 ++ c = a1 : (a2 ++ c) -> (a1 : a2 ++ b <= a1 : a2 ++ c <-> a1 : (a2 ++ b) <= a1 : (a2 ++ c))
32 appendS 
a1 : a2 ++ b = a1 : (a2 ++ b)
33 31, 32 ax_mp 
a1 : a2 ++ c = a1 : (a2 ++ c) -> (a1 : a2 ++ b <= a1 : a2 ++ c <-> a1 : (a2 ++ b) <= a1 : (a2 ++ c))
34 appendS 
a1 : a2 ++ c = a1 : (a2 ++ c)
35 33, 34 ax_mp 
a1 : a2 ++ b <= a1 : a2 ++ c <-> a1 : (a2 ++ b) <= a1 : (a2 ++ c)
36 30, 35 ax_mp 
a2 ++ b <= a2 ++ c <-> a1 : a2 ++ b <= a1 : a2 ++ c
37 id 
(b <= c <-> a2 ++ b <= a2 ++ c) -> (b <= c <-> a2 ++ b <= a2 ++ c)
38 36, 37 syl6bb 
(b <= c <-> a2 ++ b <= a2 ++ c) -> (b <= c <-> a1 : a2 ++ b <= a1 : a2 ++ c)
39 5, 10, 15, 20, 27, 38 listind 
b <= c <-> a ++ b <= a ++ c

Axiom use

axs_prop_calc (ax_1, ax_2, ax_3, ax_mp, itru), axs_pred_calc (ax_gen, ax_4, ax_5, ax_6, ax_7, ax_10, ax_11, ax_12), axs_set (elab, ax_8), axs_the (theid, the0), axs_peano (peano1, peano2, peano5, addeq, muleq, add0, addS, mul0, mulS)