Theorem dvdtr | index | src |

theorem dvdtr (a b c: nat): $ a || b -> b || c -> a || c $;
StepHypRefExpression
1 idvd
y * x * a = c -> a || c
2 mulass
y * x * a = y * (x * a)
3 muleq2
x * a = b -> y * (x * a) = y * b
4 2, 3 syl5eq
x * a = b -> y * x * a = y * b
5 4 anwl
x * a = b /\ y * b = c -> y * x * a = y * b
6 anr
x * a = b /\ y * b = c -> y * b = c
7 5, 6 eqtrd
x * a = b /\ y * b = c -> y * x * a = c
8 1, 7 syl
x * a = b /\ y * b = c -> a || c
9 8 eexda
x * a = b -> E. y y * b = c -> a || c
10 9 conv dvd
x * a = b -> b || c -> a || c
11 10 eex
E. x x * a = b -> b || c -> a || c
12 11 conv dvd
a || b -> b || c -> 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_peano (peano2, peano5, addeq, muleq, add0, addS, mul0, mulS)