let m be Nat; :: thesis: for n being non zero Nat st m is prime & n is prime & m divides Fib n holds
for r being Nat st r < n & r <> 0 holds
not m divides Fib r
let n be non zero Nat; :: thesis: ( m is prime & n is prime & m divides Fib n implies for r being Nat st r < n & r <> 0 holds
not m divides Fib r )
assume A1: m is prime ; :: thesis: ( not n is prime or not m divides Fib n or for r being Nat st r < n & r <> 0 holds
not m divides Fib r )
defpred S1[ Element of NAT ] means ( $1 < n & $1 <> 0 & m divides Fib $1 );
assume A2: n is prime ; :: thesis: ( not m divides Fib n or for r being Nat st r < n & r <> 0 holds
not m divides Fib r )
reconsider C = { x where x is Element of NAT : S1[x] } as Subset of NAT from DOMAIN_1:sch 7();
 assume A3: m divides Fib n ; :: thesis: for r being Nat st r < n & r <> 0 holds
not m divides Fib r
assume A4: ex r being Nat st
( r < n & r <> 0 & m divides Fib r ) ; :: thesis: contradiction
C is non empty Subset of NAT
proof
consider r being Nat such that
A5: ( r < n & r <> 0 & m divides Fib r ) by A4;
r in NAT by ORDINAL1:def 12;
then r in C by A5;
hence C is non empty Subset of NAT ; :: thesis: verum
end;
then reconsider C = C as non empty Subset of NAT ;
reconsider r = min C as Nat by TARSKI:1;
defpred S2[ Nat] means ( m divides Fib (n -' (r * ($1 + 1))) & r <= n / ($1 + 2) );
r in C by XXREAL_2:def 7;
then A6: ex r9 being Element of NAT st
( r9 = r & S1[r9] ) ;
then A7: n -' r < n by NAT_2:9;
m <> 1 by A1, INT_2:def 4;
then A8: not m divides Fib (r -' 1) by A6, Th68;
A9: for k being Nat st S2[k] holds
S2[k + 1]
proof
let k be Nat; :: thesis: ( S2[k] implies S2[k + 1] )
A10: m divides (Fib r) * (Fib ((n -' ((k + 2) * r)) + 1)) by A6, NAT_D:9;
A11: n - (r * (k + 2)) <> 0
proof
assume A12: n - (r * (k + 2)) = 0 ; :: thesis: contradiction
then A13: ( r divides n & k + 2 divides n ) by NAT_D:def 3;
per cases ( ( r = 1 & k + 2 = n ) or ( r = 1 & k + 2 = 1 ) or ( r = n & k + 2 = n ) or ( r = n & k + 2 = 1 ) ) by A2, A13, INT_2:def 4;
suppose ( r = 1 & k + 2 = 1 ) ; :: thesis: contradiction
hence contradiction by A2, A12, INT_2:def 4; :: thesis: verum
end;
suppose ( r = n & k + 2 = n ) ; :: thesis: contradiction
hence contradiction by A6; :: thesis: verum
end;
suppose ( r = n & k + 2 = 1 ) ; :: thesis: contradiction
hence contradiction by A6; :: thesis: verum
end;
end;
end;
- r < - 0 by A6;
then (- r) * (k + 2) < 0 * (k + 2) ;
then (- (r * (k + 2))) + n < 0 + n by XREAL_1:6;
then A14: n -' ((k + 2) * r) < n by A11, XREAL_0:def 2;
assume A15: S2[k] ; :: thesis: S2[k + 1]
then A16: r * (k + 2) <= (n / (k + 2)) * (k + 2) by XREAL_1:64;
then A17: r * (k + 2) <= n by XCMPLX_1:87;
then A18: n - (r * (k + 2)) >= (r * (k + 2)) - (r * (k + 2)) by XREAL_1:9;
then A19: n -' ((k + 2) * r) <> 0 by A11, XREAL_0:def 2;
r + (r * (k + 1)) <= n by A16, XCMPLX_1:87;
then r * (k + 1) < n by A6, Th14;
then A20: ((k + 1) * r) - ((k + 1) * r) < n - ((k + 1) * r) by XREAL_1:9;
(n - ((k + 1) * r)) - r > 0 by A11, A18;
then (n -' ((k + 1) * r)) - r > 0 by A20, XREAL_0:def 2;
then A21: (n -' ((k + 1) * r)) -' r = (n -' ((k + 1) * r)) - r by XREAL_0:def 2
.= (n - ((k + 1) * r)) - r by A20, XREAL_0:def 2
.= n -' ((k + 2) * r) by A18, XREAL_0:def 2 ;
n - (r * (k + 1)) >= (r + (r * (k + 1))) - (r * (k + 1)) by A17, XREAL_1:9;
then r <= n -' (r * (k + 1)) by XREAL_0:def 2;
then Fib (n -' ((k + 1) * r)) = Fib ((n -' ((k + 2) * r)) + r) by A21, XREAL_1:235
.= ((Fib r) * (Fib ((n -' ((k + 2) * r)) + 1))) + ((Fib (r -' 1)) * (Fib (n -' ((k + 2) * r)))) by A6, Th40 ;
then A22: m divides (Fib (r -' 1)) * (Fib (n -' ((k + 2) * r))) by A15, A10, NAT_D:10;
then m divides Fib (n -' ((k + 2) * r)) by A1, A8, NEWTON:80;
then n -' ((k + 2) * r) in C by A19, A14;
then n -' ((k + 2) * r) >= r by XXREAL_2:def 7;
then n >= r + ((k + 2) * r) by A17, NAT_D:54;
then n * (1 / ((1 + k) + 2)) >= (r * ((1 + k) + 2)) * (1 / ((1 + k) + 2)) by XREAL_1:64;
then n * (1 / ((1 + k) + 2)) >= (r * ((1 + k) + 2)) / ((1 + k) + 2) by XCMPLX_1:99;
then n / ((1 + k) + 2) >= (r * ((1 + k) + 2)) / ((1 + k) + 2) by XCMPLX_1:99;
hence S2[k + 1] by A1, A8, A22, NEWTON:80, XCMPLX_1:89; :: thesis: verum
end;
r - r < n - r by A6, XREAL_1:9;
then A23: n -' r <> 0 by XREAL_0:def 2;
A24: m divides (Fib r) * (Fib ((n -' r) + 1)) by A6, NAT_D:9;
Fib n = Fib ((n -' r) + r) by A6, XREAL_1:235
.= ((Fib r) * (Fib ((n -' r) + 1))) + ((Fib (r -' 1)) * (Fib (n -' r))) by A6, Th40 ;
then A25: m divides (Fib (r -' 1)) * (Fib (n -' r)) by A3, A24, NAT_D:10;
then m divides Fib (n -' r) by A1, A8, NEWTON:80;
then n -' r in C by A7, A23;
then n -' r >= r by XXREAL_2:def 7;
then n >= r + r by A6, NAT_D:54;
then n / 2 >= (2 * r) / 2 by XREAL_1:72;
then A26: S2[ 0 ] by A1, A8, A25, NEWTON:80;
for k being Nat holds S2[k] from NAT_1:sch 2(A26, A9);
 then ( n / (n + 2) < 1 & r <= n / (n + 2) ) by XREAL_1:29, XREAL_1:191;
then r < 1 + 0 by XXREAL_0:2;
hence contradiction by A6, NAT_1:13; :: thesis: verum