Theorem bgcd01 ≪ | index | src | ≫ 

theorem bgcd01 (b: nat): $ bgcd 0 b = 0 $;
StepHypRefExpression
1 least0 
~E. d d e. {d2 | 0 < d2 /\ E. x E. y x * 0 = y * b + d2} -> least {d2 | 0 < d2 /\ E. x E. y x * 0 = y * b + d2} = 0
2 1 conv bgcd 
~E. d d e. {d2 | 0 < d2 /\ E. x E. y x * 0 = y * b + d2} -> bgcd 0 b = 0
3 lteq2 
d2 = d -> (0 < d2 <-> 0 < d)
4 mul02 
x * 0 = 0
5 4 a1i 
d2 = d -> x * 0 = 0
6 addeq2 
d2 = d -> y * b + d2 = y * b + d
7 5, 6 eqeqd 
d2 = d -> (x * 0 = y * b + d2 <-> 0 = y * b + d)
8 7 exeqd 
d2 = d -> (E. y x * 0 = y * b + d2 <-> E. y 0 = y * b + d)
9 8 exeqd 
d2 = d -> (E. x E. y x * 0 = y * b + d2 <-> E. x E. y 0 = y * b + d)
10 3, 9 aneqd 
d2 = d -> (0 < d2 /\ E. x E. y x * 0 = y * b + d2 <-> 0 < d /\ E. x E. y 0 = y * b + d)
11 10 elabe 
d e. {d2 | 0 < d2 /\ E. x E. y x * 0 = y * b + d2} <-> 0 < d /\ E. x E. y 0 = y * b + d
12 absurd 
~0 = y * b + d -> 0 = y * b + d -> F.
13 ltne 
0 < y * b + d -> 0 != y * b + d
14 13 conv ne 
0 < y * b + d -> ~0 = y * b + d
15 leaddid2 
d <= y * b + d
16 ltletr 
0 < d -> d <= y * b + d -> 0 < y * b + d
17 15, 16 mpi 
0 < d -> 0 < y * b + d
18 14, 17 syl 
0 < d -> ~0 = y * b + d
19 12, 18 syl 
0 < d -> 0 = y * b + d -> F.
20 19 eexd 
0 < d -> E. y 0 = y * b + d -> F.
21 20 eexd 
0 < d -> E. x E. y 0 = y * b + d -> F.
22 21 imp 
0 < d /\ E. x E. y 0 = y * b + d -> F.
23 11, 22 sylbi 
d e. {d2 | 0 < d2 /\ E. x E. y x * 0 = y * b + d2} -> F.
24 notfal 
~F.
25 23, 24 mt 
~d e. {d2 | 0 < d2 /\ E. x E. y x * 0 = y * b + d2}
26 25 ngen 
~E. d d e. {d2 | 0 < d2 /\ E. x E. y x * 0 = y * b + d2}
27 2, 26 ax_mp 
bgcd 0 b = 0

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, add0, addS, mul0)