Theorem leappend2 ≪ | index | src | ≫ 

theorem leappend2 (a b c: nat): $ b <= c <-> a ++ b <= a ++ c $;
StepHypRefExpression
1 biidd 
_1 = a -> (b <= c <-> b <= c)
2 id 
_1 = a -> _1 = a
3 eqidd 
_1 = a -> b = b
4 2, 3 appendeqd 
_1 = a -> _1 ++ b = a ++ b
5 eqidd 
_1 = a -> c = c
6 2, 5 appendeqd 
_1 = a -> _1 ++ c = a ++ c
7 4, 6 leeqd 
_1 = a -> (_1 ++ b <= _1 ++ c <-> a ++ b <= a ++ c)
8 1, 7 bieqd 
_1 = a -> (b <= c <-> _1 ++ b <= _1 ++ c <-> (b <= c <-> a ++ b <= a ++ c))
9 biidd 
_1 = 0 -> (b <= c <-> b <= c)
10 id 
_1 = 0 -> _1 = 0
11 eqidd 
_1 = 0 -> b = b
12 10, 11 appendeqd 
_1 = 0 -> _1 ++ b = 0 ++ b
13 eqidd 
_1 = 0 -> c = c
14 10, 13 appendeqd 
_1 = 0 -> _1 ++ c = 0 ++ c
15 12, 14 leeqd 
_1 = 0 -> (_1 ++ b <= _1 ++ c <-> 0 ++ b <= 0 ++ c)
16 9, 15 bieqd 
_1 = 0 -> (b <= c <-> _1 ++ b <= _1 ++ c <-> (b <= c <-> 0 ++ b <= 0 ++ c))
17 biidd 
_1 = a2 -> (b <= c <-> b <= c)
18 id 
_1 = a2 -> _1 = a2
19 eqidd 
_1 = a2 -> b = b
20 18, 19 appendeqd 
_1 = a2 -> _1 ++ b = a2 ++ b
21 eqidd 
_1 = a2 -> c = c
22 18, 21 appendeqd 
_1 = a2 -> _1 ++ c = a2 ++ c
23 20, 22 leeqd 
_1 = a2 -> (_1 ++ b <= _1 ++ c <-> a2 ++ b <= a2 ++ c)
24 17, 23 bieqd 
_1 = a2 -> (b <= c <-> _1 ++ b <= _1 ++ c <-> (b <= c <-> a2 ++ b <= a2 ++ c))
25 biidd 
_1 = a1 : a2 -> (b <= c <-> b <= c)
26 id 
_1 = a1 : a2 -> _1 = a1 : a2
27 eqidd 
_1 = a1 : a2 -> b = b
28 26, 27 appendeqd 
_1 = a1 : a2 -> _1 ++ b = a1 : a2 ++ b
29 eqidd 
_1 = a1 : a2 -> c = c
30 26, 29 appendeqd 
_1 = a1 : a2 -> _1 ++ c = a1 : a2 ++ c
31 28, 30 leeqd 
_1 = a1 : a2 -> (_1 ++ b <= _1 ++ c <-> a1 : a2 ++ b <= a1 : a2 ++ c)
32 25, 31 bieqd 
_1 = a1 : a2 -> (b <= c <-> _1 ++ b <= _1 ++ c <-> (b <= c <-> a1 : a2 ++ b <= a1 : a2 ++ c))
33 bicom 
(0 ++ b <= 0 ++ c <-> b <= c) -> (b <= c <-> 0 ++ b <= 0 ++ c)
34 leeq 
0 ++ b = b -> 0 ++ c = c -> (0 ++ b <= 0 ++ c <-> b <= c)
35 append0 
0 ++ b = b
36 34, 35 ax_mp 
0 ++ c = c -> (0 ++ b <= 0 ++ c <-> b <= c)
37 append0 
0 ++ c = c
38 36, 37 ax_mp 
0 ++ b <= 0 ++ c <-> b <= c
39 33, 38 ax_mp 
b <= c <-> 0 ++ b <= 0 ++ c
40 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)
41 lecons2 
a2 ++ b <= a2 ++ c <-> a1 : (a2 ++ b) <= a1 : (a2 ++ c)
42 40, 41 ax_mp 
(a1 : a2 ++ b <= a1 : a2 ++ c <-> a1 : (a2 ++ b) <= a1 : (a2 ++ c)) -> (a2 ++ b <= a2 ++ c <-> a1 : a2 ++ b <= a1 : a2 ++ c)
43 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))
44 appendS 
a1 : a2 ++ b = a1 : (a2 ++ b)
45 43, 44 ax_mp 
a1 : a2 ++ c = a1 : (a2 ++ c) -> (a1 : a2 ++ b <= a1 : a2 ++ c <-> a1 : (a2 ++ b) <= a1 : (a2 ++ c))
46 appendS 
a1 : a2 ++ c = a1 : (a2 ++ c)
47 45, 46 ax_mp 
a1 : a2 ++ b <= a1 : a2 ++ c <-> a1 : (a2 ++ b) <= a1 : (a2 ++ c)
48 42, 47 ax_mp 
a2 ++ b <= a2 ++ c <-> a1 : a2 ++ b <= a1 : a2 ++ c
49 id 
(b <= c <-> a2 ++ b <= a2 ++ c) -> (b <= c <-> a2 ++ b <= a2 ++ c)
50 48, 49 syl6bb 
(b <= c <-> a2 ++ b <= a2 ++ c) -> (b <= c <-> a1 : a2 ++ b <= a1 : a2 ++ c)
51 8, 16, 24, 32, 39, 50 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)