Theorem maxadd1 | index | src |

theorem maxadd1 (a b c: nat): $ max a b + c = max (a + c) (b + c) $;
StepHypRefExpression
1
a < b -> if (a < b) b a = b
2
conv max
a < b -> max a b = b
3
a < b -> max a b + c = b + c
4
a < b <-> a + c < b + c
5
a + c < b + c -> if (a + c < b + c) (b + c) (a + c) = b + c
6
conv max
a + c < b + c -> max (a + c) (b + c) = b + c
7
4, 6
a < b -> max (a + c) (b + c) = b + c
8
3, 7
a < b -> max a b + c = max (a + c) (b + c)
9
~a < b -> if (a < b) b a = a
10
conv max
~a < b -> max a b = a
11
~a < b -> max a b + c = a + c
13
~a < b <-> ~a + c < b + c
14
~a + c < b + c -> if (a + c < b + c) (b + c) (a + c) = a + c
15
conv max
~a + c < b + c -> max (a + c) (b + c) = a + c
16
~a < b -> max (a + c) (b + c) = a + c
17
~a < b -> max a b + c = max (a + c) (b + c)
18
8, 17
max a b + c = max (a + c) (b + 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), axs_peano (peano2, peano5, addeq, add0, addS)