let m be Nat; :: thesis: for n being non empty 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 empty 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 ;
set r = min C;
defpred S2[ Nat] means ( m divides Fib (n -' ((min C) * ($1 + 1))) & min C <= n / ($1 + 2) );
min C in C by XXREAL_2:def 7;
then A6: ex r9 being Element of NAT st
( r9 = min C & S1[r9] ) ;
then A7: n -' (min C) < n by NAT_2:9;
m <> 1 by A1, INT_2:def 4;
then A8: not m divides Fib ((min C) -' 1) by A6, Th70;
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 (min C)) * (Fib ((n -' ((k + 2) * (min C))) + 1)) by A6, NAT_D:9;
A11: n - ((min C) * (k + 2)) <> 0
proof
assume A12: n - ((min C) * (k + 2)) = 0 ; :: thesis: contradiction
then A13: ( min C divides n & k + 2 divides n ) by NAT_D:def 3;
per cases ( ( min C = 1 & k + 2 = n ) or ( min C = 1 & k + 2 = 1 ) or ( min C = n & k + 2 = n ) or ( min C = n & k + 2 = 1 ) ) by A2, A13, INT_2:def 4;
suppose ( min C = 1 & k + 2 = 1 ) ; :: thesis: contradiction
hence contradiction by A2, A12, INT_2:def 4; :: thesis: verum
end;
suppose ( min C = n & k + 2 = n ) ; :: thesis: contradiction
hence contradiction by A6; :: thesis: verum
end;
suppose ( min C = n & k + 2 = 1 ) ; :: thesis: contradiction
hence contradiction by A6; :: thesis: verum
end;
end;
end;
- (min C) < - 0 by A6, XREAL_1:24;
then (- (min C)) * (k + 2) < 0 * (k + 2) by XREAL_1:68;
then (- ((min C) * (k + 2))) + n < 0 + n by XREAL_1:6;
then A14: n -' ((k + 2) * (min C)) < n by A11, XREAL_0:def 2;
assume A15: S2[k] ; :: thesis: S2[k + 1]
then A16: (min C) * (k + 2) <= (n / (k + 2)) * (k + 2) by XREAL_1:64;
then A17: (min C) * (k + 2) <= n by XCMPLX_1:87;
then A18: n - ((min C) * (k + 2)) >= ((min C) * (k + 2)) - ((min C) * (k + 2)) by XREAL_1:9;
then A19: n -' ((k + 2) * (min C)) <> 0 by A11, XREAL_0:def 2;
(min C) + ((min C) * (k + 1)) <= n by A16, XCMPLX_1:87;
then (min C) * (k + 1) < n by A6, Th16;
then A20: ((k + 1) * (min C)) - ((k + 1) * (min C)) < n - ((k + 1) * (min C)) by XREAL_1:9;
(n - ((k + 1) * (min C))) - (min C) > 0 by A11, A18;
then (n -' ((k + 1) * (min C))) - (min C) > 0 by A20, XREAL_0:def 2;
then A21: (n -' ((k + 1) * (min C))) -' (min C) = (n -' ((k + 1) * (min C))) - (min C) by XREAL_0:def 2
.= (n - ((k + 1) * (min C))) - (min C) by A20, XREAL_0:def 2
.= n -' ((k + 2) * (min C)) by A18, XREAL_0:def 2 ;
n - ((min C) * (k + 1)) >= ((min C) + ((min C) * (k + 1))) - ((min C) * (k + 1)) by A17, XREAL_1:9;
then min C <= n -' ((min C) * (k + 1)) by XREAL_0:def 2;
then Fib (n -' ((k + 1) * (min C))) = Fib ((n -' ((k + 2) * (min C))) + (min C)) by A21, XREAL_1:235
.= ((Fib (min C)) * (Fib ((n -' ((k + 2) * (min C))) + 1))) + ((Fib ((min C) -' 1)) * (Fib (n -' ((k + 2) * (min C))))) by A6, Th42 ;
then A22: m divides (Fib ((min C) -' 1)) * (Fib (n -' ((k + 2) * (min C)))) by A15, A10, NAT_D:10;
then m divides Fib (n -' ((k + 2) * (min C))) by A1, A8, NEWTON:80;
then n -' ((k + 2) * (min C)) in C by A19, A14;
then n -' ((k + 2) * (min C)) >= min C by XXREAL_2:def 7;
then n >= (min C) + ((k + 2) * (min C)) by A17, NAT_D:54;
then n * (1 / ((1 + k) + 2)) >= ((min C) * ((1 + k) + 2)) * (1 / ((1 + k) + 2)) by XREAL_1:64;
then n * (1 / ((1 + k) + 2)) >= ((min C) * ((1 + k) + 2)) / ((1 + k) + 2) by XCMPLX_1:99;
then n / ((1 + k) + 2) >= ((min C) * ((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;
(min C) - (min C) < n - (min C) by A6, XREAL_1:9;
then A23: n -' (min C) <> 0 by XREAL_0:def 2;
A24: m divides (Fib (min C)) * (Fib ((n -' (min C)) + 1)) by A6, NAT_D:9;
Fib n = Fib ((n -' (min C)) + (min C)) by A6, XREAL_1:235
.= ((Fib (min C)) * (Fib ((n -' (min C)) + 1))) + ((Fib ((min C) -' 1)) * (Fib (n -' (min C)))) by A6, Th42 ;
then A25: m divides (Fib ((min C) -' 1)) * (Fib (n -' (min C))) by A3, A24, NAT_D:10;
then m divides Fib (n -' (min C)) by A1, A8, NEWTON:80;
then n -' (min C) in C by A7, A23;
then n -' (min C) >= min C by XXREAL_2:def 7;
then n >= (min C) + (min C) by A6, NAT_D:54;
then n / 2 >= (2 * (min C)) / 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 & min C <= n / (n + 2) ) by XREAL_1:29, XREAL_1:191;
then min C < 1 + 0 by XXREAL_0:2;
hence contradiction by A6, NAT_1:13; :: thesis: verum