Theorem dfbgcd ≪ | index | src | ≫ 

theorem dfbgcd (a b: nat) {d x y: nat}:
  $ bgcd a b = least {d | 0 < d /\ E. x E. y x * a = y * b + d} $;
StepHypRefExpression
1 leasteq 
{d2 | 0 < d2 /\ E. z E. w z * a = w * b + d2} == {d | 0 < d /\ E. x E. y x * a = y * b + d} ->
  least {d2 | 0 < d2 /\ E. z E. w z * a = w * b + d2} = least {d | 0 < d /\ E. x E. y x * a = y * b + d}
2 1 conv bgcd 
{d2 | 0 < d2 /\ E. z E. w z * a = w * b + d2} == {d | 0 < d /\ E. x E. y x * a = y * b + d} -> bgcd a b = least {d | 0 < d /\ E. x E. y x * a = y * b + d}
3 lteq2 
d2 = d -> (0 < d2 <-> 0 < d)
4 anlr 
d2 = d /\ z = x /\ w = y -> z = x
5 4 muleq1d 
d2 = d /\ z = x /\ w = y -> z * a = x * a
6 muleq1 
w = y -> w * b = y * b
7 6 anwr 
d2 = d /\ z = x /\ w = y -> w * b = y * b
8 anll 
d2 = d /\ z = x /\ w = y -> d2 = d
9 7, 8 addeqd 
d2 = d /\ z = x /\ w = y -> w * b + d2 = y * b + d
10 5, 9 eqeqd 
d2 = d /\ z = x /\ w = y -> (z * a = w * b + d2 <-> x * a = y * b + d)
11 10 cbvexd 
d2 = d /\ z = x -> (E. w z * a = w * b + d2 <-> E. y x * a = y * b + d)
12 11 cbvexd 
d2 = d -> (E. z E. w z * a = w * b + d2 <-> E. x E. y x * a = y * b + d)
13 3, 12 aneqd 
d2 = d -> (0 < d2 /\ E. z E. w z * a = w * b + d2 <-> 0 < d /\ E. x E. y x * a = y * b + d)
14 13 cbvab 
{d2 | 0 < d2 /\ E. z E. w z * a = w * b + d2} == {d | 0 < d /\ E. x E. y x * a = y * b + d}
15 2, 14 ax_mp 
bgcd a b = least {d | 0 < d /\ E. x E. y x * a = y * b + d}

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 (peano2, addeq, muleq)