let m, n be Nat; :: thesis: ( ( m > 0 or n > 0 ) implies ex i, i1 being Integer st (i * m) + (i1 * n) = m gcd n )
defpred S₁[ Nat] means ( $1 > 0 & ex i, i1 being Integer st (i * m) + (i1 * n) = $1 );
assume A1: ( m > 0 or n > 0 ) ; :: thesis: ex i, i1 being Integer st (i * m) + (i1 * n) = m gcd n
A2: ex p being Nat st S₁[p]

proof

per cases ( m > 0 or n > 0 ) by A1;

suppose A3: m > 0 ; :: thesis: ex p being Nat st S₁[p]

(1 * m) + (0 * n) = m ;
hence ex p being Nat st S₁[p] by A3; :: thesis: verum

end;

suppose A4: n > 0 ; :: thesis: ex p being Nat st S₁[p]

(0 * m) + (1 * n) = n ;
hence ex p being Nat st S₁[p] by A4; :: thesis: verum

end;

end;

end;

ex p being Nat st
( S₁[p] & ( for n being Nat st S₁[n] holds
p <= n ) ) from NAT_1:sch 5(A2);
then consider p being Nat such that
A5: p > 0 and
A6: ex i, i0 being Integer st (i * m) + (i0 * n) = p and
A7: for k being Nat st k > 0 & ex i1, i2 being Integer st (i1 * m) + (i2 * n) = k holds
p <= k ;
consider i, i0 being Integer such that
A8: (i * m) + (i0 * n) = p by A6;
A9: for k being Nat st ex i1, i2 being Integer st (i1 * m) + (i2 * n) = k holds
p divides k

proof

let k be Nat; :: thesis: ( ex i1, i2 being Integer st (i1 * m) + (i2 * n) = k implies p divides k )
given i1, i2 being Integer such that A10: (i1 * m) + (i2 * n) = k ; :: thesis: p divides k
consider l, s being Nat such that
A11: k = (p * l) + s and
A12: s < p by A5, NAT_1:17;
reconsider l = l, s = s as Element of NAT by ORDINAL1:def 12;
s = 0

proof

s = k - (p * l) by A11;
then A13: s = ((i1 - (i * l)) * m) + ((i2 - (i0 * l)) * n) by A8, A10;
assume s <> 0 ; :: thesis: contradiction
hence contradiction by A7, A12, A13; :: thesis: verum

end;

hence p divides k by A11, NAT_D:def 3; :: thesis: verum

end;

A14: for s being Nat st s divides m & s divides n holds
s divides p

proof

let s be Nat; :: thesis: ( s divides m & s divides n implies s divides p )
assume that
A15: s divides m and
A16: s divides n ; :: thesis: s divides p
consider r being Nat such that
A17: n = s * r by A16, NAT_D:def 3;
reconsider p9 = p, s9 = s as Integer ;
consider l being Nat such that
A18: m = s * l by A15, NAT_D:def 3;
ex i4 being Integer st p9 = s9 * i4

proof

take (i * l) + (i0 * r) ; :: thesis: p9 = s9 * ((i * l) + (i0 * r))
thus p9 = s9 * ((i * l) + (i0 * r)) by A8, A18, A17; :: thesis: verum

end;

hence s divides p by INT_1:def 3; :: thesis: verum

end;

(0 * m) + (1 * n) = n ;
then A19: p divides n by A9;
(1 * m) + (0 * n) = m ;
then p divides m by A9;
then p = m gcd n by A19, A14, NAT_D:def 5;
hence ex i, i1 being Integer st (i * m) + (i1 * n) = m gcd n by A6; :: thesis: verum