Theorem bgcddvd1 ≪ | index | src | ≫ 

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

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)