let a, b be Integer; :: thesis: for A, B being sequence of NAT st A . 0 = |.a.| & B . 0 = |.b.| & ( for i being Nat holds

( A . (i + 1) = B . i & B . (i + 1) = (A . i) mod (B . i) ) ) holds

for i being Nat st B . i <> 0 holds

(A . 0) gcd (B . 0) = (A . i) gcd (B . i)

let A, B be sequence of NAT; :: thesis: ( A . 0 = |.a.| & B . 0 = |.b.| & ( for i being Nat holds

( A . (i + 1) = B . i & B . (i + 1) = (A . i) mod (B . i) ) ) implies for i being Nat st B . i <> 0 holds

(A . 0) gcd (B . 0) = (A . i) gcd (B . i) )

assume A1: ( A . 0 = |.a.| & B . 0 = |.b.| & ( for i being Nat holds

( A . (i + 1) = B . i & B . (i + 1) = (A . i) mod (B . i) ) ) ) ; :: thesis: for i being Nat st B . i <> 0 holds

(A . 0) gcd (B . 0) = (A . i) gcd (B . i)

defpred S_{1}[ Nat] means ( B . $1 <> 0 implies (A . 0) gcd (B . 0) = (A . $1) gcd (B . $1) );

A2: S_{1}[ 0 ]
;

A3: for i being Nat st S_{1}[i] holds

S_{1}[i + 1]
_{1}[i]
from NAT_1:sch 2(A2, A3);

hence for i being Nat st B . i <> 0 holds

(A . 0) gcd (B . 0) = (A . i) gcd (B . i) ; :: thesis: verum

( A . (i + 1) = B . i & B . (i + 1) = (A . i) mod (B . i) ) ) holds

for i being Nat st B . i <> 0 holds

(A . 0) gcd (B . 0) = (A . i) gcd (B . i)

let A, B be sequence of NAT; :: thesis: ( A . 0 = |.a.| & B . 0 = |.b.| & ( for i being Nat holds

( A . (i + 1) = B . i & B . (i + 1) = (A . i) mod (B . i) ) ) implies for i being Nat st B . i <> 0 holds

(A . 0) gcd (B . 0) = (A . i) gcd (B . i) )

assume A1: ( A . 0 = |.a.| & B . 0 = |.b.| & ( for i being Nat holds

( A . (i + 1) = B . i & B . (i + 1) = (A . i) mod (B . i) ) ) ) ; :: thesis: for i being Nat st B . i <> 0 holds

(A . 0) gcd (B . 0) = (A . i) gcd (B . i)

defpred S

A2: S

A3: for i being Nat st S

S

proof

for i being Nat holds S
let i be Nat; :: thesis: ( S_{1}[i] implies S_{1}[i + 1] )

assume A4: S_{1}[i]
; :: thesis: S_{1}[i + 1]

( B . (i + 1) <> 0 implies (A . 0) gcd (B . 0) = (A . (i + 1)) gcd (B . (i + 1)) )_{1}[i + 1]
; :: thesis: verum

end;assume A4: S

( B . (i + 1) <> 0 implies (A . 0) gcd (B . 0) = (A . (i + 1)) gcd (B . (i + 1)) )

proof

hence
S
assume A5:
B . (i + 1) <> 0
; :: thesis: (A . 0) gcd (B . 0) = (A . (i + 1)) gcd (B . (i + 1))

B . i <> 0

end;B . i <> 0

proof

hence
(A . 0) gcd (B . 0) = (A . (i + 1)) gcd (B . (i + 1))
by A4, A1, Lm3; :: thesis: verum
assume A6:
B . i = 0
; :: thesis: contradiction

B . (i + 1) = (A . i) mod (B . i) by A1;

hence contradiction by A5, A6, INT_1:def 10; :: thesis: verum

end;B . (i + 1) = (A . i) mod (B . i) by A1;

hence contradiction by A5, A6, INT_1:def 10; :: thesis: verum

hence for i being Nat st B . i <> 0 holds

(A . 0) gcd (B . 0) = (A . i) gcd (B . i) ; :: thesis: verum