Theorem minadd1 | index | src |

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