defpred S1[ Nat] means ex n being Element of NAT st $1 = F1(n);
A4: ex k being Nat st S1[k] by A2;
A5: for k being Nat st k <> 0 & S1[k] holds
ex n being Nat st
( n < k & S1[n] )
proof
let k be Nat; :: thesis: ( k <> 0 & S1[k] implies ex n being Nat st
( n < k & S1[n] ) )
assume that
A6: k <> 0 and
A7: ex n being Element of NAT st k = F1(n) ; :: thesis: ex n being Nat st
( n < k & S1[n] )
consider n being Element of NAT such that
A8: k = F1(n) by A7;
reconsider Q = F1((n + 1)) as Element of NAT by ORDINAL1:def 12;
A9: ( n = 0 implies Q < k ) by A1, A2, A8;
now :: thesis: ( ex m being Nat st n = m + 1 implies ( F1((n + 1)) < k & ex m being Element of omega st F1((n + 1)) = F1(m) ) )
given m being Nat such that A10: n = m + 1 ; :: thesis: ( F1((n + 1)) < k & ex m being Element of omega st F1((n + 1)) = F1(m) )
reconsider m1 = m as Element of NAT by ORDINAL1:def 12;
F1((m1 + 2)) = F1(m1) mod F1((m1 + 1)) by A3;
hence F1((n + 1)) < k by A6, A8, A10, Th1; :: thesis: ex m being Element of omega st F1((n + 1)) = F1(m)
take m = n + 1; :: thesis: F1((n + 1)) = F1(m)
thus F1((n + 1)) = F1(m) ; :: thesis: verum
end;
hence ex n being Nat st
( n < k & S1[n] ) by A9, NAT_1:6; :: thesis: verum
end;
A11: S1[ 0 ] from NAT_1:sch 7(A4, A5);
 defpred S2[ Nat] means 0 = F1($1);
A12: ex n being Nat st S2[n] by A11;
consider k being Nat such that
A13: ( S2[k] & ( for n being Nat st S2[n] holds
k <= n ) ) from NAT_1:sch 5(A12);
 consider n being Nat such that
A14: k = n + 1 by A1, A2, A13, NAT_1:6;
reconsider n = n as Element of NAT by ORDINAL1:def 12;
take n ; :: thesis: ( F1(n) = F2() gcd F3() & F1((n + 1)) = 0 )
defpred S3[ Nat] means ( F1(n) divides F1($1) & F1(n) divides F1(($1 + 1)) );
S3[n] by A13, A14, Th6;
then A15: ex k being Nat st S3[k] ;
A16: for k being Nat st k <> 0 & S3[k] holds
ex m being Nat st
( m < k & S3[m] )
proof
let l be Nat; :: thesis: ( l <> 0 & S3[l] implies ex m being Nat st
( m < l & S3[m] ) )
assume that
A17: l <> 0 and
A18: F1(n) divides F1(l) and
A19: F1(n) divides F1((l + 1)) ; :: thesis: ex m being Nat st
( m < l & S3[m] )
consider m being Nat such that
A20: l = m + 1 by A17, NAT_1:6;
reconsider m = m as Element of NAT by ORDINAL1:def 12;
take m ; :: thesis: ( m < l & S3[m] )
A21: m <= m + 1 by NAT_1:11;
m <> m + 1 ;
hence m < l by A20, A21, XXREAL_0:1; :: thesis: S3[m]
A22: now :: thesis: ( F1((m + 1)) = 0 implies F1(n) divides F1(m) )
assume A23: F1((m + 1)) = 0 ; :: thesis: F1(n) divides F1(m)
now :: thesis: ( m + 1 <> k implies F1(n) divides F1(m) )
assume A24: m + 1 <> k ; :: thesis: F1(n) divides F1(m)
k <= m + 1 by A13, A23;
then k < m + 1 by A24, XXREAL_0:1;
then A25: k <= m by NAT_1:13;
defpred S4[ Nat] means ( k <= $1 implies F1($1) = 0 );
A26: S4[ 0 ] by A13;
A27: for m being Nat st S4[m] holds
S4[m + 1]
proof
let m be Nat; :: thesis: ( S4[m] implies S4[m + 1] )
assume that
A28: ( k <= m implies F1(m) = 0 ) and
A29: k <= m + 1 ; :: thesis: F1((m + 1)) = 0
now :: thesis: ( k <> m + 1 implies F1((m + 1)) = 0 )
assume k <> m + 1 ; :: thesis: F1((m + 1)) = 0
then A30: k < m + 1 by A29, XXREAL_0:1;
then consider l being Nat such that
A31: m = l + 1 by A1, A2, A28, NAT_1:6, NAT_1:13;
reconsider l = l as Element of NAT by ORDINAL1:def 12;
F1((l + 2)) = F1(l) mod F1((l + 1)) by A3;
hence F1((m + 1)) = 0 by A28, A30, A31, Def2, NAT_1:13; :: thesis: verum
end;
hence F1((m + 1)) = 0 by A13; :: thesis: verum
end;
for m being Nat holds S4[m] from NAT_1:sch 2(A26, A27);
then F1(m) = 0 by A25;
hence F1(n) divides F1(m) by Th6; :: thesis: verum
end;
hence F1(n) divides F1(m) by A14; :: thesis: verum
end;
now :: thesis: ( F1((m + 1)) <> 0 implies F1(n) divides F1(m) )
assume A32: F1((m + 1)) <> 0 ; :: thesis: F1(n) divides F1(m)
F1((m + 2)) = F1(m) mod F1((m + 1)) by A3;
then A33: F1(m) = (F1((m + 1)) * (F1(m) div F1((m + 1)))) + F1((m + 2)) by A32, INT_1:59;
F1(n) divides F1((m + 1)) * (F1(m) div F1((m + 1))) by A18, A20, Th9;
hence F1(n) divides F1(m) by A19, A20, A33, Th8; :: thesis: verum
end;
hence F1(n) divides F1(m) by A22; :: thesis: F1(n) divides F1((m + 1))
thus F1(n) divides F1((m + 1)) by A18, A20; :: thesis: verum
end;
now :: thesis: ( F1(n) divides F2() & F1(n) divides F3() & ( for m being Nat st m divides F2() & m divides F3() holds
m divides F1(n) ) )
S3[ 0 ] from NAT_1:sch 7(A15, A16);
hence ( F1(n) divides F2() & F1(n) divides F3() ) by A2; :: thesis: for m being Nat st m divides F2() & m divides F3() holds
m divides F1(n)
let m be Nat; :: thesis: ( m divides F2() & m divides F3() implies m divides F1(n) )
defpred S4[ Nat] means ( m divides F1($1) & m divides F1(($1 + 1)) );
assume that
A34: m divides F2() and
A35: m divides F3() ; :: thesis: m divides F1(n)
A36: S4[ 0 ] by A2, A34, A35;
A37: for k being Nat st S4[k] holds
S4[k + 1]
proof
let k be Nat; :: thesis: ( S4[k] implies S4[k + 1] )
assume that
A38: m divides F1(k) and
A39: m divides F1((k + 1)) ; :: thesis: S4[k + 1]
thus m divides F1((k + 1)) by A39; :: thesis: m divides F1(((k + 1) + 1))
F1((k + 2)) = F1(k) mod F1((k + 1)) by A3;
hence m divides F1(((k + 1) + 1)) by A38, A39, Th11; :: thesis: verum
end;
for k being Nat holds S4[k] from NAT_1:sch 2(A36, A37);
hence m divides F1(n) ; :: thesis: verum
end;
hence F1(n) = F2() gcd F3() by Def5; :: thesis: F1((n + 1)) = 0
thus F1((n + 1)) = 0 by A13, A14; :: thesis: verum