defpred S_{1}[ Element of NAT , Element of NAT ] means (Fib $1) gcd (Fib $2) = Fib ($1 gcd $2);

A1: for k being Element of NAT st ( for m, n being Element of NAT st m < k & n < k holds

S_{1}[m,n] ) holds

for m being Element of NAT st m <= k holds

S_{1}[k,m]
_{1}[m,n] holds

S_{1}[n,m]
;

thus for m, n being Element of NAT holds S_{1}[m,n]
from FIB_NUM:sch 2(A14, A1); :: thesis: verum

A1: for k being Element of NAT st ( for m, n being Element of NAT st m < k & n < k holds

S

for m being Element of NAT st m <= k holds

S

proof

A14:
for m, n being Element of NAT st S
let k be Element of NAT ; :: thesis: ( ( for m, n being Element of NAT st m < k & n < k holds

S_{1}[m,n] ) implies for m being Element of NAT st m <= k holds

S_{1}[k,m] )

assume A2: for m, n being Element of NAT st m < k & n < k holds

S_{1}[m,n]
; :: thesis: for m being Element of NAT st m <= k holds

S_{1}[k,m]

let m be Element of NAT ; :: thesis: ( m <= k implies S_{1}[k,m] )

assume A3: m <= k ; :: thesis: S_{1}[k,m]

end;S

S

assume A2: for m, n being Element of NAT st m < k & n < k holds

S

S

let m be Element of NAT ; :: thesis: ( m <= k implies S

assume A3: m <= k ; :: thesis: S

per cases
( m = k or m < k )
by A3, XXREAL_0:1;

end;

suppose A5:
m < k
; :: thesis: S_{1}[k,m]

thus
S_{1}[k,m]
:: thesis: verum

end;proof
end;

per cases
( m = 0 or m > 0 )
;

end;

suppose A6:
m = 0
; :: thesis: S_{1}[k,m]

then
(Fib k) gcd (Fib m) = Fib k
by NEWTON:52, PRE_FF:1;

hence S_{1}[k,m]
by A6, NEWTON:52; :: thesis: verum

end;hence S

suppose A7:
m > 0
; :: thesis: S_{1}[k,m]

thus
S_{1}[k,m]
:: thesis: verum

end;proof

consider r being Nat such that

A8: k = m + r by A3, NAT_1:10;

reconsider r = r as Element of NAT by ORDINAL1:def 12;

A9: r <= k by A8, NAT_1:11;

r <> 0 by A5, A8;

then consider rr being Nat such that

A10: r = rr + 1 by NAT_1:6;

reconsider rr = rr as Element of NAT by ORDINAL1:def 12;

Fib k = ((Fib (rr + 1)) * (Fib (m + 1))) + ((Fib rr) * (Fib m)) by A8, A10, Th4;

then A11: (Fib k) gcd (Fib m) = (Fib m) gcd ((Fib (m + 1)) * (Fib r)) by A10, EULER_1:8;

(Fib m) gcd (Fib (m + 1)) = 1 by Lm7;

then A12: (Fib k) gcd (Fib m) = (Fib m) gcd (Fib r) by A11, Th2;

r <> k by A7, A8;

then A13: r < k by A9, XXREAL_0:1;

k gcd m = m gcd r by A8, Th1;

hence S_{1}[k,m]
by A2, A5, A12, A13; :: thesis: verum

end;A8: k = m + r by A3, NAT_1:10;

reconsider r = r as Element of NAT by ORDINAL1:def 12;

A9: r <= k by A8, NAT_1:11;

r <> 0 by A5, A8;

then consider rr being Nat such that

A10: r = rr + 1 by NAT_1:6;

reconsider rr = rr as Element of NAT by ORDINAL1:def 12;

Fib k = ((Fib (rr + 1)) * (Fib (m + 1))) + ((Fib rr) * (Fib m)) by A8, A10, Th4;

then A11: (Fib k) gcd (Fib m) = (Fib m) gcd ((Fib (m + 1)) * (Fib r)) by A10, EULER_1:8;

(Fib m) gcd (Fib (m + 1)) = 1 by Lm7;

then A12: (Fib k) gcd (Fib m) = (Fib m) gcd (Fib r) by A11, Th2;

r <> k by A7, A8;

then A13: r < k by A9, XXREAL_0:1;

k gcd m = m gcd r by A8, Th1;

hence S

S

thus for m, n being Element of NAT holds S