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 )
assume A1: ( m > 0 or n > 0 ) ; :: thesis: 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 );
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]

ex i, i1 being Element of NAT st (i * m) + (i1 * n) = m

proof

(1 * m) + (0 * n) = m ;
hence ex i, i1 being Element of NAT st (i * m) + (i1 * n) = m ; :: thesis: verum

end;

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]

ex i, i1 being Element of NAT st (i * m) + (i1 * n) = n

proof

(0 * m) + (1 * n) = n ;
hence ex i, i1 being Element of NAT st (i * m) + (i1 * n) = n ; :: thesis: verum

end;

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 13;
s = 0

proof

assume s <> 0 ; :: thesis: contradiction
then A13: s > 0 ;
ex i3, i4 being Integer st (i3 * m) + (i4 * n) = s

proof

s = k - (p * l) by A11;
then s = ((i1 - (i * l)) * m) + ((i2 - (i0 * l)) * n) by A8, A10;
hence ex i3, i4 being Integer st (i3 * m) + (i4 * n) = s ; :: thesis: verum

end;

hence contradiction by A7, A12, A13; :: thesis: verum

end;

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

end;

p = m gcd n

proof

A14: ex i, i1 being Integer st (i * m) + (i1 * n) = m

proof

(1 * m) + (0 * n) = m ;
hence ex i, i1 being Integer st (i * m) + (i1 * n) = m ; :: thesis: verum

end;

A15: ex i, i1 being Integer st (i * m) + (i1 * n) = n

proof

(0 * m) + (1 * n) = n ;
hence ex i, i1 being Integer st (i * m) + (i1 * n) = n ; :: thesis: verum

end;

A16: p divides m by A9, A14;
A17: p divides n by A9, A15;
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
A18: s divides m and
A19: s divides n ; :: thesis: s divides p
consider l being Nat such that
A20: m = s * l by A18, NAT_D:def 3;
consider r being Nat such that
A21: n = s * r by A19, NAT_D:def 3;
reconsider p' = p, s' = s as Integer ;
ex i4 being Integer st p' = s' * i4

proof

take (i * l) + (i0 * r) ; :: thesis: p' = s' * ((i * l) + (i0 * r))
thus p' = s' * ((i * l) + (i0 * r)) by A8, A20, A21; :: thesis: verum

end;

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

end;

hence p = m gcd n by A16, A17, NAT_D:def 5; :: thesis: verum

end;

hence ex i, i1 being Integer st (i * m) + (i1 * n) = m gcd n by A6; :: thesis: verum