Theorem bgcdled ≪ | index | src | ≫

theorem bgcdled (G: wff) (a b d x y: nat):
  $ G -> 0 < d $ >
  $ G -> x * a = y * b + d $ >
  $ G -> bgcd a b <= d $;

Step	Hyp	Ref	Expression
1		leastle	d e. {d2 \| 0 < d2 /\ E. z E. w z * a = w * b + d2} -> least {d2 \| 0 < d2 /\ E. z E. w z * a = w * b + d2} <= d
2	1	conv bgcd	d e. {d2 \| 0 < d2 /\ E. z E. w z * a = w * b + d2} -> bgcd a b <= d
3		lteq2	d2 = d -> (0 < d2 <-> 0 < d)
4		addeq2	d2 = d -> w * b + d2 = w * b + d
5	4	eqeq2d	d2 = d -> (z * a = w * b + d2 <-> z * a = w * b + d)
6	5	exeqd	d2 = d -> (E. w z * a = w * b + d2 <-> E. w z * a = w * b + d)
7	6	exeqd	d2 = d -> (E. z E. w z * a = w * b + d2 <-> E. z E. w z * a = w * b + d)
8	3, 7	aneqd	d2 = d -> (0 < d2 /\ E. z E. w z * a = w * b + d2 <-> 0 < d /\ E. z E. w z * a = w * b + d)
9	8	elabe	d e. {d2 \| 0 < d2 /\ E. z E. w z * a = w * b + d2} <-> 0 < d /\ E. z E. w z * a = w * b + d
10		hyp h	G -> 0 < d
11		anlr	G /\ z = x /\ w = y -> z = x
12	11	muleq1d	G /\ z = x /\ w = y -> z * a = x * a
13		muleq1	w = y -> w * b = y * b
14	13	anwr	G /\ z = x /\ w = y -> w * b = y * b
15	14	addeq1d	G /\ z = x /\ w = y -> w * b + d = y * b + d
16	12, 15	eqeqd	G /\ z = x /\ w = y -> (z * a = w * b + d <-> x * a = y * b + d)
17		hyp h2	G -> x * a = y * b + d
18	17	anwll	G /\ z = x /\ w = y -> x * a = y * b + d
19	16, 18	mpbird	G /\ z = x /\ w = y -> z * a = w * b + d
20	19	iexde	G /\ z = x -> E. w z * a = w * b + d
21	20	iexde	G -> E. z E. w z * a = w * b + d
22	10, 21	iand	G -> 0 < d /\ E. z E. w z * a = w * b + d
23	9, 22	sylibr	G -> d e. {d2 \| 0 < d2 /\ E. z E. w z * a = w * b + d2}
24	2, 23	syl	G -> bgcd a 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), axs_peano (peano1, peano2, peano5, addeq, muleq, add0, addS)