Theorem bgcd02 ≪ | index | src | ≫ 

theorem bgcd02 (a: nat): $ bgcd a 0 = a $;
StepHypRefExpression
1 bgcd01 
bgcd 0 0 = 0
2 bgcdeq1 
a = 0 -> bgcd a 0 = bgcd 0 0
3 1, 2 syl6eq 
a = 0 -> bgcd a 0 = 0
4 id 
a = 0 -> a = 0
5 3, 4 eqtr4d 
a = 0 -> bgcd a 0 = a
6 lt01 
0 < a <-> a != 0
7 6 conv ne 
0 < a <-> ~a = 0
8 7 bi2i 
~a = 0 -> 0 < a
9 eqtr 
1 * a = a -> a = 0 * 0 + a -> 1 * a = 0 * 0 + a
10 mul11 
1 * a = a
11 9, 10 ax_mp 
a = 0 * 0 + a -> 1 * a = 0 * 0 + a
12 eqcom 
0 * 0 + a = a -> a = 0 * 0 + a
13 eqtr 
0 * 0 + a = 0 + a -> 0 + a = a -> 0 * 0 + a = a
14 addeq1 
0 * 0 = 0 -> 0 * 0 + a = 0 + a
15 mul01 
0 * 0 = 0
16 14, 15 ax_mp 
0 * 0 + a = 0 + a
17 13, 16 ax_mp 
0 + a = a -> 0 * 0 + a = a
18 add01 
0 + a = a
19 17, 18 ax_mp 
0 * 0 + a = a
20 12, 19 ax_mp 
a = 0 * 0 + a
21 11, 20 ax_mp 
1 * a = 0 * 0 + a
22 21 a1i 
~a = 0 -> 1 * a = 0 * 0 + a
23 8, 22 bgcdled 
~a = 0 -> bgcd a 0 <= a
24 bgcdbezout 
E. x E. y x * a = y * 0 + bgcd a 0
25 10 a1i 
~a = 0 /\ x * a = y * 0 + bgcd a 0 -> 1 * a = a
26 add01 
0 + bgcd a 0 = bgcd a 0
27 addeq1 
y * 0 = 0 -> y * 0 + bgcd a 0 = 0 + bgcd a 0
28 mul0 
y * 0 = 0
29 27, 28 ax_mp 
y * 0 + bgcd a 0 = 0 + bgcd a 0
30 anr 
~a = 0 /\ x * a = y * 0 + bgcd a 0 -> x * a = y * 0 + bgcd a 0
31 29, 30 syl6eq 
~a = 0 /\ x * a = y * 0 + bgcd a 0 -> x * a = 0 + bgcd a 0
32 26, 31 syl6eq 
~a = 0 /\ x * a = y * 0 + bgcd a 0 -> x * a = bgcd a 0
33 25, 32 leeqd 
~a = 0 /\ x * a = y * 0 + bgcd a 0 -> (1 * a <= x * a <-> a <= bgcd a 0)
34 lemul1a 
1 <= x -> 1 * a <= x * a
35 lt01 
0 < x <-> x != 0
36 35 conv d1, lt 
1 <= x <-> x != 0
37 ltner 
0 < bgcd a 0 -> bgcd a 0 != 0
38 37 conv ne 
0 < bgcd a 0 -> ~bgcd a 0 = 0
39 bgcdpos 
a != 0 -> 0 < bgcd a 0
40 39 conv ne 
~a = 0 -> 0 < bgcd a 0
41 38, 40 syl 
~a = 0 -> ~bgcd a 0 = 0
42 41 anwl 
~a = 0 /\ x * a = y * 0 + bgcd a 0 -> ~bgcd a 0 = 0
43 32 anwl 
~a = 0 /\ x * a = y * 0 + bgcd a 0 /\ x = 0 -> x * a = bgcd a 0
44 mul01 
0 * a = 0
45 muleq1 
x = 0 -> x * a = 0 * a
46 45 anwr 
~a = 0 /\ x * a = y * 0 + bgcd a 0 /\ x = 0 -> x * a = 0 * a
47 44, 46 syl6eq 
~a = 0 /\ x * a = y * 0 + bgcd a 0 /\ x = 0 -> x * a = 0
48 43, 47 eqtr3d 
~a = 0 /\ x * a = y * 0 + bgcd a 0 /\ x = 0 -> bgcd a 0 = 0
49 42, 48 mtand 
~a = 0 /\ x * a = y * 0 + bgcd a 0 -> ~x = 0
50 49 conv ne 
~a = 0 /\ x * a = y * 0 + bgcd a 0 -> x != 0
51 36, 50 sylibr 
~a = 0 /\ x * a = y * 0 + bgcd a 0 -> 1 <= x
52 34, 51 syl 
~a = 0 /\ x * a = y * 0 + bgcd a 0 -> 1 * a <= x * a
53 33, 52 mpbid 
~a = 0 /\ x * a = y * 0 + bgcd a 0 -> a <= bgcd a 0
54 53 eexda 
~a = 0 -> E. y x * a = y * 0 + bgcd a 0 -> a <= bgcd a 0
55 54 eexd 
~a = 0 -> E. x E. y x * a = y * 0 + bgcd a 0 -> a <= bgcd a 0
56 24, 55 mpi 
~a = 0 -> a <= bgcd a 0
57 23, 56 leasymd 
~a = 0 -> bgcd a 0 = a
58 5, 57 cases 
bgcd a 0 = 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)