Theorem bgcdlem ≪ | index | src | ≫ 

theorem bgcdlem (a b: nat) {x y: nat}:
  $ a != 0 -> 0 < bgcd a b /\ E. x E. y x * a = y * b + bgcd a b $;
StepHypRefExpression
1 lteq2 
d = bgcd a b -> (0 < d <-> 0 < bgcd a b)
2 anlr 
d = bgcd a b /\ z = x /\ w = y -> z = x
3 2 muleq1d 
d = bgcd a b /\ z = x /\ w = y -> z * a = x * a
4 muleq1 
w = y -> w * b = y * b
5 4 anwr 
d = bgcd a b /\ z = x /\ w = y -> w * b = y * b
6 anll 
d = bgcd a b /\ z = x /\ w = y -> d = bgcd a b
7 5, 6 addeqd 
d = bgcd a b /\ z = x /\ w = y -> w * b + d = y * b + bgcd a b
8 3, 7 eqeqd 
d = bgcd a b /\ z = x /\ w = y -> (z * a = w * b + d <-> x * a = y * b + bgcd a b)
9 8 cbvexd 
d = bgcd a b /\ z = x -> (E. w z * a = w * b + d <-> E. y x * a = y * b + bgcd a b)
10 9 cbvexd 
d = bgcd a b -> (E. z E. w z * a = w * b + d <-> E. x E. y x * a = y * b + bgcd a b)
11 1, 10 aneqd 
d = bgcd a b -> (0 < d /\ E. z E. w z * a = w * b + d <-> 0 < bgcd a b /\ E. x E. y x * a = y * b + bgcd a b)
12 11 elabe 
bgcd a b e. {d | 0 < d /\ E. z E. w z * a = w * b + d} <-> 0 < bgcd a b /\ E. x E. y x * a = y * b + bgcd a b
13 leastel 
a e. {d | 0 < d /\ E. z E. w z * a = w * b + d} -> least {d | 0 < d /\ E. z E. w z * a = w * b + d} e. {d | 0 < d /\ E. z E. w z * a = w * b + d}
14 13 conv bgcd 
a e. {d | 0 < d /\ E. z E. w z * a = w * b + d} -> bgcd a b e. {d | 0 < d /\ E. z E. w z * a = w * b + d}
15 lteq2 
d = a -> (0 < d <-> 0 < a)
16 addeq2 
d = a -> w * b + d = w * b + a
17 16 eqeq2d 
d = a -> (z * a = w * b + d <-> z * a = w * b + a)
18 17 exeqd 
d = a -> (E. w z * a = w * b + d <-> E. w z * a = w * b + a)
19 18 exeqd 
d = a -> (E. z E. w z * a = w * b + d <-> E. z E. w z * a = w * b + a)
20 15, 19 aneqd 
d = a -> (0 < d /\ E. z E. w z * a = w * b + d <-> 0 < a /\ E. z E. w z * a = w * b + a)
21 20 elabe 
a e. {d | 0 < d /\ E. z E. w z * a = w * b + d} <-> 0 < a /\ E. z E. w z * a = w * b + a
22 bi2 
(0 < a <-> a != 0) -> a != 0 -> 0 < a
23 lt01 
0 < a <-> a != 0
24 22, 23 ax_mp 
a != 0 -> 0 < a
25 mul11 
1 * a = a
26 anlr 
a != 0 /\ z = 1 /\ w = 0 -> z = 1
27 26 muleq1d 
a != 0 /\ z = 1 /\ w = 0 -> z * a = 1 * a
28 25, 27 syl6eq 
a != 0 /\ z = 1 /\ w = 0 -> z * a = a
29 add01 
0 + a = a
30 mul01 
0 * b = 0
31 muleq1 
w = 0 -> w * b = 0 * b
32 31 anwr 
a != 0 /\ z = 1 /\ w = 0 -> w * b = 0 * b
33 30, 32 syl6eq 
a != 0 /\ z = 1 /\ w = 0 -> w * b = 0
34 33 addeq1d 
a != 0 /\ z = 1 /\ w = 0 -> w * b + a = 0 + a
35 29, 34 syl6eq 
a != 0 /\ z = 1 /\ w = 0 -> w * b + a = a
36 28, 35 eqtr4d 
a != 0 /\ z = 1 /\ w = 0 -> z * a = w * b + a
37 36 iexde 
a != 0 /\ z = 1 -> E. w z * a = w * b + a
38 37 iexde 
a != 0 -> E. z E. w z * a = w * b + a
39 24, 38 iand 
a != 0 -> 0 < a /\ E. z E. w z * a = w * b + a
40 21, 39 sylibr 
a != 0 -> a e. {d | 0 < d /\ E. z E. w z * a = w * b + d}
41 14, 40 syl 
a != 0 -> bgcd a b e. {d | 0 < d /\ E. z E. w z * a = w * b + d}
42 12, 41 sylib 
a != 0 -> 0 < bgcd a b /\ E. x E. y x * a = y * b + bgcd a 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), axs_peano (peano1, peano2, peano5, addeq, muleq, add0, addS, mul0, mulS)