A6: ( 0 < F4() & F4() < F3() ) by A1, A2;
deffunc H1( Nat, set ) -> Element of NAT = IFEQ $2,0 ,0 ,F2($1);
consider q being Function of NAT ,NAT such that
A7: q . 0 = F3() and
A8: for i being Nat holds q . (i + 1) = H1(i,q . i) from NAT_1:sch 12();
 deffunc H2( Element of NAT ) -> Element of NAT = q . $1;
q . (0 + 1) = IFEQ (q . 0 ),0 ,0 ,F2(0 ) by A8
.= F2(0 ) by A2, A7, FUNCOP_1:def 8 ;
then A9: ( H2( 0 ) = F3() & H2(1) = F4() ) by A4, A7;
A10: for k being Element of NAT st q . k > 0 holds
q . k = F1(k)
proof
let k be Element of NAT ; :: thesis: ( q . k > 0 implies q . k = F1(k) )
assume A11: q . k > 0 ; :: thesis: q . k = F1(k)
now
per cases ( k = 0 or k <> 0 ) ;
case k = 0 ; :: thesis: q . k = F1(k)
hence q . k = F1(k) by A3, A7; :: thesis: verum
end;
case k <> 0 ; :: thesis: q . k = F1(k)
then consider i being Nat such that
A12: k = i + 1 by NAT_1:6;
reconsider i = i as Element of NAT by ORDINAL1:def 13;
A13: now
assume A14: q . i = 0 ; :: thesis: contradiction
q . k = IFEQ (q . i),0 ,0 ,F2(i) by A8, A12
.= 0 by A14, FUNCOP_1:def 8 ;
hence contradiction by A11; :: thesis: verum
end;
q . k = IFEQ (q . i),0 ,0 ,F2(i) by A8, A12
.= F2(i) by A13, FUNCOP_1:def 8 ;
hence q . k = F1(k) by A5, A11, A12; :: thesis: verum
end;
end;
end;
hence q . k = F1(k) ; :: thesis: verum
end;
A15: for k being Element of NAT holds H2(k + 2) = H2(k) mod H2(k + 1)
proof
let k be Element of NAT ; :: thesis: H2(k + 2) = H2(k) mod H2(k + 1)
now
per cases ( q . (k + 1) <> 0 or q . (k + 1) = 0 ) ;
case A16: q . (k + 1) <> 0 ; :: thesis: H2(k + 2) = H2(k) mod H2(k + 1)
now
assume A17: F2(k) = 0 ; :: thesis: contradiction
A18: ( q . k = 0 or q . k <> 0 ) ;
q . (k + 1) = IFEQ (q . k),0 ,0 ,F2(k) by A8
.= 0 by A17, A18, FUNCOP_1:def 8 ;
hence contradiction by A16; :: thesis: verum
end;
then A19: F2(k) > 0 ;
A20: q . (k + (1 + 1)) = q . ((k + 1) + 1)
.= IFEQ (q . (k + 1)),0 ,0 ,F2((k + 1)) by A8
.= F2((k + 1)) by A16, FUNCOP_1:def 8
.= F1(k) mod F2(k) by A5, A19 ;
A21: now
assume A22: q . k = 0 ; :: thesis: contradiction
q . (k + 1) = IFEQ (q . k),0 ,0 ,F2(k) by A8
.= 0 by A22, FUNCOP_1:def 8 ;
hence contradiction by A16; :: thesis: verum
end;
then A23: q . k > 0 ;
q . (k + 1) = IFEQ (q . k),0 ,0 ,F2(k) by A8
.= F2(k) by A21, FUNCOP_1:def 8 ;
hence H2(k + 2) = H2(k) mod H2(k + 1) by A10, A20, A23; :: thesis: verum
end;
case A24: q . (k + 1) = 0 ; :: thesis: q . (k + 2) = (q . k) mod (q . (k + 1))
thus q . (k + 2) = q . ((k + 1) + 1)
.= IFEQ (q . (k + 1)),0 ,0 ,F2((k + 1)) by A8
.= 0 by A24, FUNCOP_1:def 8
.= (q . k) mod (q . (k + 1)) by A24, NAT_D:def 2 ; :: thesis: verum
end;
end;
end;
hence H2(k + 2) = H2(k) mod H2(k + 1) ; :: thesis: verum
end;
consider k being Element of NAT such that
A25: ( H2(k) = F3() gcd F4() & H2(k + 1) = 0 ) from NAT_D:sch 1(A6, A9, A15);
 take k ; :: thesis: ( F1(k) = F3() gcd F4() & F2(k) = 0 )
A26: F3() gcd F4() > 0 by A1, Th71;
thus F1(k) = F3() gcd F4() by A1, A10, A25, Th71; :: thesis: F2(k) = 0
thus F2(k) = IFEQ (q . k),0 ,0 ,F2(k) by A25, A26, FUNCOP_1:def 8
.= 0 by A8, A25 ; :: thesis: verum