Theorem bgcdbezout ≪ | index | src | ≫ 

theorem bgcdbezout (a b: nat) {x y: nat}:
  $ E. x E. y x * a = y * b + bgcd a b $;
StepHypRefExpression
1 anlr 
a = 0 /\ x = 0 /\ y = 0 -> x = 0
2 anll 
a = 0 /\ x = 0 /\ y = 0 -> a = 0
3 1, 2 muleqd 
a = 0 /\ x = 0 /\ y = 0 -> x * a = 0 * 0
4 mul01 
0 * 0 = 0
5 add0 
0 + 0 = 0
6 mul01 
0 * b = 0
7 muleq1 
y = 0 -> y * b = 0 * b
8 7 anwr 
a = 0 /\ x = 0 /\ y = 0 -> y * b = 0 * b
9 6, 8 syl6eq 
a = 0 /\ x = 0 /\ y = 0 -> y * b = 0
10 bgcd01 
bgcd 0 b = 0
11 2 bgcdeq1d 
a = 0 /\ x = 0 /\ y = 0 -> bgcd a b = bgcd 0 b
12 10, 11 syl6eq 
a = 0 /\ x = 0 /\ y = 0 -> bgcd a b = 0
13 9, 12 addeqd 
a = 0 /\ x = 0 /\ y = 0 -> y * b + bgcd a b = 0 + 0
14 5, 13 syl6eq 
a = 0 /\ x = 0 /\ y = 0 -> y * b + bgcd a b = 0
15 4, 14 syl6eqr 
a = 0 /\ x = 0 /\ y = 0 -> y * b + bgcd a b = 0 * 0
16 3, 15 eqtr4d 
a = 0 /\ x = 0 /\ y = 0 -> x * a = y * b + bgcd a b
17 16 iexde 
a = 0 /\ x = 0 -> E. y x * a = y * b + bgcd a b
18 17 iexde 
a = 0 -> E. x E. y x * a = y * b + bgcd a b
19 bgcdlem 
a != 0 -> 0 < bgcd a b /\ E. x E. y x * a = y * b + bgcd a b
20 19 conv ne 
~a = 0 -> 0 < bgcd a b /\ E. x E. y x * a = y * b + bgcd a b
21 20 anrd 
~a = 0 -> E. x E. y x * a = y * b + bgcd a b
22 18, 21 cases 
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, the0), axs_peano (peano1, peano2, peano5, addeq, muleq, add0, addS, mul0, mulS)