Theorem prlem2 ≪ | index | src | ≫ 

theorem prlem2 (a b c d: nat): $ a, c <= b, d -> a + c <= b + d $;
StepHypRefExpression
1 lenlt 
a + c <= b + d <-> ~b + d < a + c
2 ltnle 
(a + c) * suc (a + c) // 2 < (b + d) * suc (b + d) // 2 + suc (b + d) <-> ~(b + d) * suc (b + d) // 2 + suc (b + d) <= (a + c) * suc (a + c) // 2
3 letr 
(a + c) * suc (a + c) // 2 <= a, c -> a, c <= b, d -> (a + c) * suc (a + c) // 2 <= b, d
4 leaddid1 
(a + c) * suc (a + c) // 2 <= (a + c) * suc (a + c) // 2 + c
5 4 conv pr 
(a + c) * suc (a + c) // 2 <= a, c
6 3, 5 ax_mp 
a, c <= b, d -> (a + c) * suc (a + c) // 2 <= b, d
7 ltadd2 
d < suc (b + d) <-> (b + d) * suc (b + d) // 2 + d < (b + d) * suc (b + d) // 2 + suc (b + d)
8 7 conv pr 
d < suc (b + d) <-> b, d < (b + d) * suc (b + d) // 2 + suc (b + d)
9 leltsuc 
d <= b + d <-> d < suc (b + d)
10 leaddid2 
d <= b + d
11 9, 10 mpbi 
d < suc (b + d)
12 8, 11 mpbi 
b, d < (b + d) * suc (b + d) // 2 + suc (b + d)
13 12 a1i 
a, c <= b, d -> b, d < (b + d) * suc (b + d) // 2 + suc (b + d)
14 6, 13 lelttrd 
a, c <= b, d -> (a + c) * suc (a + c) // 2 < (b + d) * suc (b + d) // 2 + suc (b + d)
15 2, 14 sylib 
a, c <= b, d -> ~(b + d) * suc (b + d) // 2 + suc (b + d) <= (a + c) * suc (a + c) // 2
16 lemul2 
0 < 2 ->
  ((b + d) * suc (b + d) // 2 + suc (b + d) <= (a + c) * suc (a + c) // 2 <-> 2 * ((b + d) * suc (b + d) // 2 + suc (b + d)) <= 2 * ((a + c) * suc (a + c) // 2)
  )
17 d0lt2 
0 < 2
18 16, 17 ax_mp 
(b + d) * suc (b + d) // 2 + suc (b + d) <= (a + c) * suc (a + c) // 2 <-> 2 * ((b + d) * suc (b + d) // 2 + suc (b + d)) <= 2 * ((a + c) * suc (a + c) // 2)
19 addmul 
(b + d + 2) * suc (b + d) = (b + d) * suc (b + d) + 2 * suc (b + d)
20 muladd 
2 * ((b + d) * suc (b + d) // 2 + suc (b + d)) = 2 * ((b + d) * suc (b + d) // 2) + 2 * suc (b + d)
21 muldiv3 
2 || (b + d) * suc (b + d) -> 2 * ((b + d) * suc (b + d) // 2) = (b + d) * suc (b + d)
22 prlem1 
2 || (b + d) * suc (b + d)
23 21, 22 ax_mp 
2 * ((b + d) * suc (b + d) // 2) = (b + d) * suc (b + d)
24 23 a1i 
a, c <= b, d /\ b + d < a + c -> 2 * ((b + d) * suc (b + d) // 2) = (b + d) * suc (b + d)
25 24 addeq1d 
a, c <= b, d /\ b + d < a + c -> 2 * ((b + d) * suc (b + d) // 2) + 2 * suc (b + d) = (b + d) * suc (b + d) + 2 * suc (b + d)
26 20, 25 syl5eq 
a, c <= b, d /\ b + d < a + c -> 2 * ((b + d) * suc (b + d) // 2 + suc (b + d)) = (b + d) * suc (b + d) + 2 * suc (b + d)
27 19, 26 syl6eqr 
a, c <= b, d /\ b + d < a + c -> 2 * ((b + d) * suc (b + d) // 2 + suc (b + d)) = (b + d + 2) * suc (b + d)
28 eqtr 
2 * ((a + c) * suc (a + c) // 2) = (a + c) * suc (a + c) ->
  (a + c) * suc (a + c) = suc (a + c) * (a + c) ->
  2 * ((a + c) * suc (a + c) // 2) = suc (a + c) * (a + c)
29 muldiv3 
2 || (a + c) * suc (a + c) -> 2 * ((a + c) * suc (a + c) // 2) = (a + c) * suc (a + c)
30 prlem1 
2 || (a + c) * suc (a + c)
31 29, 30 ax_mp 
2 * ((a + c) * suc (a + c) // 2) = (a + c) * suc (a + c)
32 28, 31 ax_mp 
(a + c) * suc (a + c) = suc (a + c) * (a + c) -> 2 * ((a + c) * suc (a + c) // 2) = suc (a + c) * (a + c)
33 mulcom 
(a + c) * suc (a + c) = suc (a + c) * (a + c)
34 32, 33 ax_mp 
2 * ((a + c) * suc (a + c) // 2) = suc (a + c) * (a + c)
35 34 a1i 
a, c <= b, d /\ b + d < a + c -> 2 * ((a + c) * suc (a + c) // 2) = suc (a + c) * (a + c)
36 27, 35 leeqd 
a, c <= b, d /\ b + d < a + c ->
  (2 * ((b + d) * suc (b + d) // 2 + suc (b + d)) <= 2 * ((a + c) * suc (a + c) // 2) <-> (b + d + 2) * suc (b + d) <= suc (a + c) * (a + c))
37 leeq1 
b + d + 2 = suc (b + d + 1) -> (b + d + 2 <= suc (a + c) <-> suc (b + d + 1) <= suc (a + c))
38 addS 
b + d + suc 1 = suc (b + d + 1)
39 38 conv d2 
b + d + 2 = suc (b + d + 1)
40 37, 39 ax_mp 
b + d + 2 <= suc (a + c) <-> suc (b + d + 1) <= suc (a + c)
41 lesuc 
b + d + 1 <= a + c <-> suc (b + d + 1) <= suc (a + c)
42 leeq1 
b + d + 1 = suc (b + d) -> (b + d + 1 <= a + c <-> suc (b + d) <= a + c)
43 add12 
b + d + 1 = suc (b + d)
44 42, 43 ax_mp 
b + d + 1 <= a + c <-> suc (b + d) <= a + c
45 anr 
a, c <= b, d /\ b + d < a + c -> b + d < a + c
46 45 conv lt 
a, c <= b, d /\ b + d < a + c -> suc (b + d) <= a + c
47 44, 46 sylibr 
a, c <= b, d /\ b + d < a + c -> b + d + 1 <= a + c
48 41, 47 sylib 
a, c <= b, d /\ b + d < a + c -> suc (b + d + 1) <= suc (a + c)
49 40, 48 sylibr 
a, c <= b, d /\ b + d < a + c -> b + d + 2 <= suc (a + c)
50 49, 46 lemuld 
a, c <= b, d /\ b + d < a + c -> (b + d + 2) * suc (b + d) <= suc (a + c) * (a + c)
51 36, 50 mpbird 
a, c <= b, d /\ b + d < a + c -> 2 * ((b + d) * suc (b + d) // 2 + suc (b + d)) <= 2 * ((a + c) * suc (a + c) // 2)
52 18, 51 sylibr 
a, c <= b, d /\ b + d < a + c -> (b + d) * suc (b + d) // 2 + suc (b + d) <= (a + c) * suc (a + c) // 2
53 52 exp 
a, c <= b, d -> b + d < a + c -> (b + d) * suc (b + d) // 2 + suc (b + d) <= (a + c) * suc (a + c) // 2
54 15, 53 mtd 
a, c <= b, d -> ~b + d < a + c
55 1, 54 sylibr 
a, c <= b, d -> a + c <= b + d

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)