Theorem bgcddvd2 ≪ | index | src | ≫ 

theorem bgcddvd2 (a b: nat): $ a != 0 -> bgcd a b || b $;
StepHypRefExpression
1 dvd02 
bgcd a b || 0
2 dvdeq2 
b = 0 -> (bgcd a b || b <-> bgcd a b || 0)
3 1, 2 mpbiri 
b = 0 -> bgcd a b || b
4 3 anwr 
a != 0 /\ b = 0 -> bgcd a b || b
5 bgcdbezout 
E. x E. y x * a = y * b + bgcd a b
6 modeq0 
b % bgcd a b = 0 <-> bgcd a b || b
7 modlt 
bgcd a b != 0 -> b % bgcd a b < bgcd a b
8 lt01 
0 < bgcd a b <-> bgcd a b != 0
9 bgcdpos 
a != 0 -> 0 < bgcd a b
10 8, 9 sylib 
a != 0 -> bgcd a b != 0
11 7, 10 syl 
a != 0 -> b % bgcd a b < bgcd a b
12 11 anwll 
a != 0 /\ ~b = 0 /\ x * a = y * b + bgcd a b -> b % bgcd a b < bgcd a b
13 ltnle 
b % bgcd a b < bgcd a b <-> ~bgcd a b <= b % bgcd a b
14 lt01 
0 < b % bgcd a b <-> b % bgcd a b != 0
15 anr 
a != 0 /\ ~b = 0 /\ x * a = y * b + bgcd a b /\ ~b % bgcd a b = 0 -> ~b % bgcd a b = 0
16 15 conv ne 
a != 0 /\ ~b = 0 /\ x * a = y * b + bgcd a b /\ ~b % bgcd a b = 0 -> b % bgcd a b != 0
17 14, 16 sylibr 
a != 0 /\ ~b = 0 /\ x * a = y * b + bgcd a b /\ ~b % bgcd a b = 0 -> 0 < b % bgcd a b
18 an3l 
a != 0 /\ ~b = 0 /\ x * a = y * b + bgcd a b /\ ~b % bgcd a b = 0 -> a != 0
19 anlr 
a != 0 /\ ~b = 0 /\ x * a = y * b + bgcd a b /\ ~b % bgcd a b = 0 -> x * a = y * b + bgcd a b
20 anllr 
a != 0 /\ ~b = 0 /\ x * a = y * b + bgcd a b /\ ~b % bgcd a b = 0 -> ~b = 0
21 20 conv ne 
a != 0 /\ ~b = 0 /\ x * a = y * b + bgcd a b /\ ~b % bgcd a b = 0 -> b != 0
22 divmod 
bgcd a b * (b // bgcd a b) + b % bgcd a b = b
23 22 a1i 
a != 0 /\ ~b = 0 /\ x * a = y * b + bgcd a b /\ ~b % bgcd a b = 0 -> bgcd a b * (b // bgcd a b) + b % bgcd a b = b
24 lemax1 
x * (b // bgcd a b) <= max (x * (b // bgcd a b)) (suc (y * (b // bgcd a b)))
25 24 a1i 
a != 0 /\ ~b = 0 /\ x * a = y * b + bgcd a b /\ ~b % bgcd a b = 0 -> x * (b // bgcd a b) <= max (x * (b // bgcd a b)) (suc (y * (b // bgcd a b)))
26 lemax2 
suc (y * (b // bgcd a b)) <= max (x * (b // bgcd a b)) (suc (y * (b // bgcd a b)))
27 26 conv lt 
y * (b // bgcd a b) < max (x * (b // bgcd a b)) (suc (y * (b // bgcd a b)))
28 27 a1i 
a != 0 /\ ~b = 0 /\ x * a = y * b + bgcd a b /\ ~b % bgcd a b = 0 -> y * (b // bgcd a b) < max (x * (b // bgcd a b)) (suc (y * (b // bgcd a b)))
29 18, 19, 21, 23, 25, 28 bgcddvd2lem 
a != 0 /\ ~b = 0 /\ x * a = y * b + bgcd a b /\ ~b % bgcd a b = 0 ->
  (max (x * (b // bgcd a b)) (suc (y * (b // bgcd a b))) * b - x * (b // bgcd a b)) * a =
    (max (x * (b // bgcd a b)) (suc (y * (b // bgcd a b))) * a - suc (y * (b // bgcd a b))) * b + b % bgcd a b
30 17, 29 bgcdled 
a != 0 /\ ~b = 0 /\ x * a = y * b + bgcd a b /\ ~b % bgcd a b = 0 -> bgcd a b <= b % bgcd a b
31 30 exp 
a != 0 /\ ~b = 0 /\ x * a = y * b + bgcd a b -> ~b % bgcd a b = 0 -> bgcd a b <= b % bgcd a b
32 31 con1d 
a != 0 /\ ~b = 0 /\ x * a = y * b + bgcd a b -> ~bgcd a b <= b % bgcd a b -> b % bgcd a b = 0
33 13, 32 syl5bi 
a != 0 /\ ~b = 0 /\ x * a = y * b + bgcd a b -> b % bgcd a b < bgcd a b -> b % bgcd a b = 0
34 12, 33 mpd 
a != 0 /\ ~b = 0 /\ x * a = y * b + bgcd a b -> b % bgcd a b = 0
35 6, 34 sylib 
a != 0 /\ ~b = 0 /\ x * a = y * b + bgcd a b -> bgcd a b || b
36 35 eexda 
a != 0 /\ ~b = 0 -> E. y x * a = y * b + bgcd a b -> bgcd a b || b
37 36 eexd 
a != 0 /\ ~b = 0 -> E. x E. y x * a = y * b + bgcd a b -> bgcd a b || b
38 5, 37 mpi 
a != 0 /\ ~b = 0 -> bgcd a b || b
39 4, 38 casesda 
a != 0 -> bgcd a b || 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)