Theorem maxadd1 | index | src |

theorem maxadd1 (a b c: nat): $ max a b + c = max (a + c) (b + c) $;
StepHypRefExpression
1 ifpos
a < b -> if (a < b) b a = b
2 1 conv max
a < b -> max a b = b
3 2 addeq1d
a < b -> max a b + c = b + c
4 ltadd1
a < b <-> a + c < b + c
5 ifpos
a + c < b + c -> if (a + c < b + c) (b + c) (a + c) = b + c
6 5 conv max
a + c < b + c -> max (a + c) (b + c) = b + c
7 4, 6 sylbi
a < b -> max (a + c) (b + c) = b + c
8 3, 7 eqtr4d
a < b -> max a b + c = max (a + c) (b + c)
9 ifneg
~a < b -> if (a < b) b a = a
10 9 conv max
~a < b -> max a b = a
11 10 addeq1d
~a < b -> max a b + c = a + c
12 noteq
(a < b <-> a + c < b + c) -> (~a < b <-> ~a + c < b + c)
13 12, 4 ax_mp
~a < b <-> ~a + c < b + c
14 ifneg
~a + c < b + c -> if (a + c < b + c) (b + c) (a + c) = a + c
15 14 conv max
~a + c < b + c -> max (a + c) (b + c) = a + c
16 13, 15 sylbi
~a < b -> max (a + c) (b + c) = a + c
17 11, 16 eqtr4d
~a < b -> max a b + c = max (a + c) (b + c)
18 8, 17 cases
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)