defpred S₁[ Nat] means ex n being Element of NAT st $1 = F₁(n);
A4: ex k being Nat st S₁[k] by A2;
A5: for k being Nat st k <> 0 & S₁[k] holds
ex n being Nat st
( n < k & S₁[n] )

proof

let k be Nat; :: thesis: ( k <> 0 & S₁[k] implies ex n being Nat st
( n < k & S₁[n] ) )
assume that
A6: k <> 0 and
A7: ex n being Element of NAT st k = F₁(n) ; :: thesis: ex n being Nat st
( n < k & S₁[n] )
consider n being Element of NAT such that
A8: k = F₁(n) by A7;
reconsider Q = F₁((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 ( F₁((n + 1)) < k & ex m being Element of omega st F₁((n + 1)) = F₁(m) ) )

given m being Nat such that A10: n = m + 1 ; :: thesis: ( F₁((n + 1)) < k & ex m being Element of omega st F₁((n + 1)) = F₁(m) )
reconsider m1 = m as Element of NAT by ORDINAL1:def 12;
F₁((m1 + 2)) = F₁(m1) mod F₁((m1 + 1)) by A3;
hence F₁((n + 1)) < k by A6, A8, A10, Th1; :: thesis: ex m being Element of omega st F₁((n + 1)) = F₁(m)
take m = n + 1; :: thesis: F₁((n + 1)) = F₁(m)
thus F₁((n + 1)) = F₁(m) ; :: thesis: verum

end;

hence ex n being Nat st
( n < k & S₁[n] ) by A9, NAT_1:6; :: thesis: verum

end;

A11: S₁[ 0 ] from NAT_1:sch 7(A4, A5);
defpred S₂[ Nat] means 0 = F₁($1);
A12: ex n being Nat st S₂[n] by A11;
consider k being Nat such that
A13: ( S₂[k] & ( for n being Nat st S₂[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: ( F₁(n) = F₂() gcd F₃() & F₁((n + 1)) = 0 )
defpred S₃[ Nat] means ( F₁(n) divides F₁($1) & F₁(n) divides F₁(($1 + 1)) );
S₃[n] by A13, A14, Th6;
then A15: ex k being Nat st S₃[k] ;
A16: for k being Nat st k <> 0 & S₃[k] holds
ex m being Nat st
( m < k & S₃[m] )

proof

let l be Nat; :: thesis: ( l <> 0 & S₃[l] implies ex m being Nat st
( m < l & S₃[m] ) )
assume that
A17: l <> 0 and
A18: F₁(n) divides F₁(l) and
A19: F₁(n) divides F₁((l + 1)) ; :: thesis: ex m being Nat st
( m < l & S₃[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 & S₃[m] )
A21: m <= m + 1 by NAT_1:11;
m <> m + 1 ;
hence m < l by A20, A21, XXREAL_0:1; :: thesis: S₃[m]

A22: now :: thesis: ( F₁((m + 1)) = 0 implies F₁(n) divides F₁(m) )

assume A23: F₁((m + 1)) = 0 ; :: thesis: F₁(n) divides F₁(m)

now :: thesis: ( m + 1 <> k implies F₁(n) divides F₁(m) )

assume A24: m + 1 <> k ; :: thesis: F₁(n) divides F₁(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 S₄[ Nat] means ( k <= $1 implies F₁($1) = 0 );
A26: S₄[ 0 ] by A13;
A27: for m being Nat st S₄[m] holds
S₄[m + 1]

proof

let m be Nat; :: thesis: ( S₄[m] implies S₄[m + 1] )
assume that
A28: ( k <= m implies F₁(m) = 0 ) and
A29: k <= m + 1 ; :: thesis: F₁((m + 1)) = 0

now :: thesis: ( k <> m + 1 implies F₁((m + 1)) = 0 )

assume k <> m + 1 ; :: thesis: F₁((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;
F₁((l + 2)) = F₁(l) mod F₁((l + 1)) by A3;
hence F₁((m + 1)) = 0 by A28, A30, A31, Def2, NAT_1:13; :: thesis: verum

end;

hence F₁((m + 1)) = 0 by A13; :: thesis: verum

end;

for m being Nat holds S₄[m] from NAT_1:sch 2(A26, A27);
then F₁(m) = 0 by A25;
hence F₁(n) divides F₁(m) by Th6; :: thesis: verum

end;

hence F₁(n) divides F₁(m) by A14; :: thesis: verum

end;

now :: thesis: ( F₁((m + 1)) <> 0 implies F₁(n) divides F₁(m) )

assume A32: F₁((m + 1)) <> 0 ; :: thesis: F₁(n) divides F₁(m)
F₁((m + 2)) = F₁(m) mod F₁((m + 1)) by A3;
then A33: F₁(m) = (F₁((m + 1)) * (F₁(m) div F₁((m + 1)))) + F₁((m + 2)) by A32, INT_1:59;
F₁(n) divides F₁((m + 1)) * (F₁(m) div F₁((m + 1))) by A18, A20, Th9;
hence F₁(n) divides F₁(m) by A19, A20, A33, Th8; :: thesis: verum

end;

hence F₁(n) divides F₁(m) by A22; :: thesis: F₁(n) divides F₁((m + 1))
thus F₁(n) divides F₁((m + 1)) by A18, A20; :: thesis: verum

end;

now :: thesis: ( F₁(n) divides F₂() & F₁(n) divides F₃() & ( for m being Nat st m divides F₂() & m divides F₃() holds
m divides F₁(n) ) )

S₃[ 0 ] from NAT_1:sch 7(A15, A16);
hence ( F₁(n) divides F₂() & F₁(n) divides F₃() ) by A2; :: thesis: for m being Nat st m divides F₂() & m divides F₃() holds
m divides F₁(n)
let m be Nat; :: thesis: ( m divides F₂() & m divides F₃() implies m divides F₁(n) )
defpred S₄[ Nat] means ( m divides F₁($1) & m divides F₁(($1 + 1)) );
assume that
A34: m divides F₂() and
A35: m divides F₃() ; :: thesis: m divides F₁(n)
A36: S₄[ 0 ] by A2, A34, A35;
A37: for k being Nat st S₄[k] holds
S₄[k + 1]

proof

let k be Nat; :: thesis: ( S₄[k] implies S₄[k + 1] )
assume that
A38: m divides F₁(k) and
A39: m divides F₁((k + 1)) ; :: thesis: S₄[k + 1]
thus m divides F₁((k + 1)) by A39; :: thesis: m divides F₁(((k + 1) + 1))
F₁((k + 2)) = F₁(k) mod F₁((k + 1)) by A3;
hence m divides F₁(((k + 1) + 1)) by A38, A39, Th11; :: thesis: verum

end;

for k being Nat holds S₄[k] from NAT_1:sch 2(A36, A37);
hence m divides F₁(n) ; :: thesis: verum

end;

hence F₁(n) = F₂() gcd F₃() by Def5; :: thesis: F₁((n + 1)) = 0
thus F₁((n + 1)) = 0 by A13, A14; :: thesis: verum