defpred S1[ 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
S1[m,n] ) holds
for m being Element of NAT st m <= k holds
S1[k,m]
proof
let k be
Element of
NAT ;
( ( for m, n being Element of NAT st m < k & n < k holds
S1[m,n] ) implies for m being Element of NAT st m <= k holds
S1[k,m] )
assume A2:
for
m,
n being
Element of
NAT st
m < k &
n < k holds
S1[
m,
n]
;
for m being Element of NAT st m <= k holds
S1[k,m]
let m be
Element of
NAT ;
( m <= k implies S1[k,m] )
assume A3:
m <= k
;
S1[k,m]
per cases
( m = k or m < k )
by A3, XXREAL_0:1;
suppose A5:
m < k
;
S1[k,m]thus
S1[
k,
m]
verumproof
per cases
( m = 0 or m > 0 )
;
suppose A7:
m > 0
;
S1[k,m]thus
S1[
k,
m]
verumproof
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
S1[
k,
m]
by A2, A5, A12, A13;
verum
end; end;
end; end;
end;
A14:
for m, n being Element of NAT st S1[m,n] holds
S1[n,m]
;
thus
for m, n being Element of NAT holds S1[m,n]
from FIB_NUM:sch 2(A14, A1); verum