Theorem dvdgcd | index | src |

theorem dvdgcd (a b d: nat): $ d || gcd a b <-> d || a /\ d || b $;
StepHypRefExpression
1 bian1
x || a -> (x || a /\ x || b <-> x || b)
2 dvd02
x || 0
3 dvdeq2
a = 0 -> (x || a <-> x || 0)
4 2, 3 mpbiri
a = 0 -> x || a
5 1, 4 syl
a = 0 -> (x || a /\ x || b <-> x || b)
6 5 bicomd
a = 0 -> (x || b <-> x || a /\ x || b)
7 6 dvdgcdlem
a = 0 -> (d || gcd a b <-> d || a /\ d || b)
8 dvdbgcdb
a != 0 -> (x || bgcd a b <-> x || a /\ x || b)
9 8 conv ne
~a = 0 -> (x || bgcd a b <-> x || a /\ x || b)
10 9 dvdgcdlem
~a = 0 -> (d || gcd a b <-> d || a /\ d || b)
11 7, 10 cases
d || gcd a b <-> d || a /\ d || b

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)