let n, k, p be Nat; :: thesis: ( 0 < k & (2 * k) |^ k <= n & n |^ k < p implies ( ((p + 1) |^ n) mod (p |^ (k + 1)) > 0 & k ! < (((n + 1) |^ k) * (p |^ k)) / (((p + 1) |^ n) mod (p |^ (k + 1))) & (((n + 1) |^ k) * (p |^ k)) / (((p + 1) |^ n) mod (p |^ (k + 1))) < (k !) + 1 ) )
set k1 = k + 1;
set n1 = n + 1;
assume A1: ( 0 < k & (2 * k) |^ k <= n & n |^ k < p ) ; :: thesis: ( ((p + 1) |^ n) mod (p |^ (k + 1)) > 0 & k ! < (((n + 1) |^ k) * (p |^ k)) / (((p + 1) |^ n) mod (p |^ (k + 1))) & (((n + 1) |^ k) * (p |^ k)) / (((p + 1) |^ n) mod (p |^ (k + 1))) < (k !) + 1 )
then A2: 1 <= k by NAT_1:14;
(2 * k) |^ k >= (2 * k) |^ 1 by A1, NAT_6:1, NAT_1:14;
then A3: ( 2 * k <= n & k + 0 < k + k ) by A1, XXREAL_0:2, XREAL_1:8;
then A4: ( n <> 0 & k < n ) by XXREAL_0:2;
then A5: ( k <= n & 1 <= n & k + 1 <= n ) by NAT_1:13, NAT_1:14;
then A6: ( k < n + 1 & k + 1 <= n + 1 ) by NAT_1:13;
n |^ k >= 1 by A4, NAT_1:14;
then 1 < p by A1, XXREAL_0:2;
then A7: 1 + 1 <= p by NAT_1:13;
reconsider K = k - 1, nk = n - k as Nat by A3, XXREAL_0:2, A1, NAT_1:21;
set P = (1,p) In_Power n;
A8: len ((1,p) In_Power n) = n + 1 by NEWTON:def 4;
A9: Sum ((1,p) In_Power n) = (1 + p) |^ n by NEWTON:30;
A10: Sum (((1,p) In_Power n) | (k + 1)), Sum ((1,p) In_Power n) are_congruent_mod p |^ (k + 1)
proof
defpred S1[ Nat] means ( k + 1 <= $1 & $1 <= len ((1,p) In_Power n) implies Sum (((1,p) In_Power n) | (k + 1)), Sum (((1,p) In_Power n) | $1) are_congruent_mod p |^ (k + 1) );
A11: S1[ 0 ] ;
A12: for i being Nat st S1[i] holds
S1[i + 1]
proof
let i be Nat; :: thesis: ( S1[i] implies S1[i + 1] )
set i1 = i + 1;
assume that
A13: S1[i] and
A14: ( k + 1 <= i + 1 & i + 1 <= len ((1,p) In_Power n) ) ; :: thesis: Sum (((1,p) In_Power n) | (k + 1)), Sum (((1,p) In_Power n) | (i + 1)) are_congruent_mod p |^ (k + 1)
per cases ( k + 1 = i + 1 or k + 1 < i + 1 ) by A14, XXREAL_0:1;
suppose k + 1 = i + 1 ; :: thesis: Sum (((1,p) In_Power n) | (k + 1)), Sum (((1,p) In_Power n) | (i + 1)) are_congruent_mod p |^ (k + 1)
hence Sum (((1,p) In_Power n) | (k + 1)), Sum (((1,p) In_Power n) | (i + 1)) are_congruent_mod p |^ (k + 1) by INT_1:11; :: thesis: verum
end;
suppose A15: k + 1 < i + 1 ; :: thesis: Sum (((1,p) In_Power n) | (k + 1)), Sum (((1,p) In_Power n) | (i + 1)) are_congruent_mod p |^ (k + 1)
then A16: ( k + 1 <= i & i <= len ((1,p) In_Power n) ) by A14, NAT_1:13;
reconsider ni = n - i as Nat by A14, A8, NAT_1:21, XREAL_1:8;
A17: i + 1 in dom ((1,p) In_Power n) by A14, FINSEQ_3:25, NAT_1:11;
then A18: ((1,p) In_Power n) | (i + 1) = (((1,p) In_Power n) | i) ^ <*(((1,p) In_Power n) . (i + 1))*> by FINSEQ_5:10;
( (i + 1) - 1 = i & n - i = ni ) ;
then A19: ((1,p) In_Power n) . (i + 1) = ((n choose i) * (1 |^ ni)) * (p |^ i) by A17, NEWTON:def 4;
p |^ (k + 1) divides (((1,p) In_Power n) . (i + 1)) - 0 by A16, A19, INT_2:2, NEWTON:89;
then 0 ,((1,p) In_Power n) . (i + 1) are_congruent_mod p |^ (k + 1) by INT_1:14, INT_1:def 4;
then (Sum (((1,p) In_Power n) | (k + 1))) + 0,(Sum (((1,p) In_Power n) | i)) + (((1,p) In_Power n) . (i + 1)) are_congruent_mod p |^ (k + 1) by A13, A15, A14, NAT_1:13, INT_1:16;
hence Sum (((1,p) In_Power n) | (k + 1)), Sum (((1,p) In_Power n) | (i + 1)) are_congruent_mod p |^ (k + 1) by A18, RVSUM_1:74; :: thesis: verum
end;
end;
end;
for i being Nat holds S1[i] from NAT_1:sch 2(A11, A12);
 then Sum (((1,p) In_Power n) | (k + 1)), Sum (((1,p) In_Power n) | (len ((1,p) In_Power n))) are_congruent_mod p |^ (k + 1) by A6, A8;
hence Sum (((1,p) In_Power n) | (k + 1)), Sum ((1,p) In_Power n) are_congruent_mod p |^ (k + 1) ; :: thesis: verum
end;
A20: Sum (((1,p) In_Power n) | (k + 1)) <> 0
proof
assume Sum (((1,p) In_Power n) | (k + 1)) = 0 ; :: thesis: contradiction
then p |^ (k + 1) divides 0 - (Sum ((1,p) In_Power n)) by A10, INT_1:def 4;
then p |^ (k + 1) divides - ((1 + p) |^ n) by A9;
then A21: p |^ (k + 1) divides (1 + p) |^ n by INT_2:10;
(1 + p) |^ n,p |^ n are_coprime by PEPIN:1, WSIERP_1:11;
then A22: ((1 + p) |^ n) gcd (p |^ n) = 1 by INT_2:def 3;
p |^ (k + 1) divides p |^ n by A5, NEWTON:89;
then p |^ (k + 1) divides 1 by A21, A22, INT_2:def 2;
then ( p |^ (k + 1) = 1 & p |^ (k + 1) > k + 1 ) by A7, NEWTON:86, INT_2:13;
hence contradiction by NAT_1:14; :: thesis: verum
end;
A23: Sum (((1,p) In_Power n) | (k + 1)) < p |^ (k + 1)
proof
defpred S1[ Nat] means ( $1 <= k + 1 implies Sum (((1,p) In_Power n) | $1) < p |^ $1 );
(n |^ k) + 1 <= p by A1, NAT_1:13;
then A24: n |^ k <= p - 1 by XREAL_1:19;
reconsider p1 = p - 1 as Nat by A1;
A25: S1[ 0 ] ;
A26: for i being Nat st S1[i] holds
S1[i + 1]
proof
let i be Nat; :: thesis: ( S1[i] implies S1[i + 1] )
set i1 = i + 1;
assume A27: ( S1[i] & i + 1 <= k + 1 ) ; :: thesis: Sum (((1,p) In_Power n) | (i + 1)) < p |^ (i + 1)
then A28: i < k + 1 by NAT_1:13;
A29: i + 1 <= n + 1 by A6, A27, XXREAL_0:2;
then A30: i <= n by XREAL_1:8;
reconsider ni = n - i as Nat by A29, XREAL_1:8, NAT_1:21;
( 1 <= i + 1 & i + 1 <= len ((1,p) In_Power n) ) by A6, A8, A27, XXREAL_0:2, NAT_1:11;
then A31: i + 1 in dom ((1,p) In_Power n) by FINSEQ_3:25;
then A32: ((1,p) In_Power n) | (i + 1) = (((1,p) In_Power n) | i) ^ <*(((1,p) In_Power n) . (i + 1))*> by FINSEQ_5:10;
( (i + 1) - 1 = i & n - i = ni ) ;
then A33: ((1,p) In_Power n) . (i + 1) = ((n choose i) * (1 |^ ni)) * (p |^ i) by A31, NEWTON:def 4;
i <= k by A28, NAT_1:13;
then A34: n |^ i <= n |^ k by A4, NAT_6:1;
n choose i <= n |^ i by A30, HILB10_4:13;
then n choose i <= n |^ k by A34, XXREAL_0:2;
then n choose i <= p - 1 by A24, XXREAL_0:2;
then ((1,p) In_Power n) . (i + 1) <= p1 * (p |^ i) by A33, XREAL_1:66;
then A35: (Sum (((1,p) In_Power n) | i)) + (((1,p) In_Power n) . (i + 1)) < (p |^ i) + (p1 * (p |^ i)) by NAT_1:13, A27, XREAL_1:8;
(p |^ i) + (p1 * (p |^ i)) = p * (p |^ i)
.= p |^ (i + 1) by NEWTON:6 ;
hence Sum (((1,p) In_Power n) | (i + 1)) < p |^ (i + 1) by A32, RVSUM_1:74, A35; :: thesis: verum
end;
for i being Nat holds S1[i] from NAT_1:sch 2(A25, A26);
 hence Sum (((1,p) In_Power n) | (k + 1)) < p |^ (k + 1) ; :: thesis: verum
end;
(Sum (((1,p) In_Power n) | (k + 1))) mod (p |^ (k + 1)) = (Sum ((1,p) In_Power n)) mod (p |^ (k + 1)) by A10, NAT_D:64;
then (Sum ((1,p) In_Power n)) mod (p |^ (k + 1)) = Sum (((1,p) In_Power n) | (k + 1)) by A23, NAT_D:24;
then A36: ((1 + p) |^ n) mod (p |^ (k + 1)) = Sum (((1,p) In_Power n) | (k + 1)) by NEWTON:30;
( 1 <= k + 1 & k + 1 <= len ((1,p) In_Power n) ) by A5, NAT_1:13, A8, NAT_1:11;
then A37: k + 1 in dom ((1,p) In_Power n) by FINSEQ_3:25;
then ((1,p) In_Power n) | (k + 1) = (((1,p) In_Power n) | k) ^ <*(((1,p) In_Power n) . (k + 1))*> by FINSEQ_5:10;
then A38: Sum (((1,p) In_Power n) | (k + 1)) = (Sum (((1,p) In_Power n) | k)) + (((1,p) In_Power n) . (k + 1)) by RVSUM_1:74;
( (k + 1) - 1 = k & n - k = nk ) ;
then A39: ((1,p) In_Power n) . (k + 1) = ((n choose k) * (1 |^ nk)) * (p |^ k) by A37, NEWTON:def 4;
n choose k <= (n |^ k) / (k !) by A4, Th8;
then ((1,p) In_Power n) . (k + 1) <= ((n |^ k) / (k !)) * (p |^ k) by A39, XREAL_1:66;
then A40: ((1,p) In_Power n) . (k + 1) <= ((p |^ k) * (n |^ k)) / (k !) by XCMPLX_1:74;
A41: Sum (((1,p) In_Power n) | k) <= (((n |^ k) / (k !)) * (p |^ K)) * k
proof
defpred S1[ Nat] means ( $1 <= k implies Sum (((1,p) In_Power n) | $1) <= (((n |^ k) / (k !)) * (p |^ K)) * $1 );
A42: S1[ 0 ] ;
A43: for i being Nat st S1[i] holds
S1[i + 1]
proof
let i be Nat; :: thesis: ( S1[i] implies S1[i + 1] )
set i1 = i + 1;
assume A44: ( S1[i] & i + 1 <= k ) ; :: thesis: Sum (((1,p) In_Power n) | (i + 1)) <= (((n |^ k) / (k !)) * (p |^ K)) * (i + 1)
then A45: ( i < k & k = K + 1 ) by NAT_1:13;
then reconsider ni = n - i as Nat by NAT_1:21, A4, XXREAL_0:2;
A46: i + 1 <= n + 1 by A44, A6, XXREAL_0:2;
1 <= i + 1 by NAT_1:11;
then A47: i + 1 in dom ((1,p) In_Power n) by A46, A8, FINSEQ_3:25;
then ((1,p) In_Power n) | (i + 1) = (((1,p) In_Power n) | i) ^ <*(((1,p) In_Power n) . (i + 1))*> by FINSEQ_5:10;
then A48: Sum (((1,p) In_Power n) | (i + 1)) = (Sum (((1,p) In_Power n) | i)) + (((1,p) In_Power n) . (i + 1)) by RVSUM_1:74;
( (i + 1) - 1 = i & n - i = ni ) ;
then A49: ((1,p) In_Power n) . (i + 1) = ((n choose i) * (1 |^ ni)) * (p |^ i) by A47, NEWTON:def 4;
A50: i <= K by A45, NAT_1:13;
then A51: p |^ i <= p |^ K by NAT_6:1, A1;
2 * K <= (2 * K) + 2 by NAT_1:11;
then 2 * K <= n by A3, XXREAL_0:2;
then 2 * K < n + 1 by NAT_1:13;
then A52: n choose i <= n choose K by Th9, A50;
A53: ( (n |^ K) * k <= (n |^ K) * n & (n |^ K) * n = n |^ (K + 1) ) by A4, XREAL_1:66, NEWTON:6;
A54: (K !) * (K + 1) = k ! by NEWTON:15;
k / k = 1 by A1, XCMPLX_1:60;
then (n |^ K) / (K !) = ((n |^ K) / (K !)) * (k / k)
.= ((n |^ K) * k) / (k !) by A54, XCMPLX_1:76 ;
then A55: (n |^ K) / (K !) <= (n |^ (K + 1)) / (k !) by A53, XREAL_1:72;
( K + 1 = k & k <= n ) by A3, XXREAL_0:2;
then K < n by NAT_1:13;
then n choose K <= (n |^ K) / (K !) by Th8;
then n choose i <= (n |^ K) / (K !) by A52, XXREAL_0:2;
then n choose i <= (n |^ k) / (k !) by A55, XXREAL_0:2;
then ((1,p) In_Power n) . (i + 1) <= ((n |^ k) / (k !)) * (p |^ K) by A49, A51, XREAL_1:66;
then Sum (((1,p) In_Power n) | (i + 1)) <= ((((n |^ k) / (k !)) * (p |^ K)) * i) + (((n |^ k) / (k !)) * (p |^ K)) by A48, A44, NAT_1:13, XREAL_1:7;
hence Sum (((1,p) In_Power n) | (i + 1)) <= (((n |^ k) / (k !)) * (p |^ K)) * (i + 1) ; :: thesis: verum
end;
for i being Nat holds S1[i] from NAT_1:sch 2(A42, A43);
 hence Sum (((1,p) In_Power n) | k) <= (((n |^ k) / (k !)) * (p |^ K)) * k ; :: thesis: verum
end;
(p |^ K) * p = p |^ (K + 1) by NEWTON:6;
then ((p |^ K) * k) * p = k * (p |^ k) ;
then A56: ((p |^ K) * k) * (n |^ k) < k * (p |^ k) by A1, XREAL_1:68;
(((n |^ k) / (k !)) * (p |^ K)) * k = ((n |^ k) / (k !)) * ((p |^ K) * k)
.= (((p |^ K) * k) * (n |^ k)) / (k !) by XCMPLX_1:74 ;
then (((n |^ k) / (k !)) * (p |^ K)) * k < (k * (p |^ k)) / (k !) by A56, XREAL_1:74;
then Sum (((1,p) In_Power n) | k) < (k * (p |^ k)) / (k !) by A41, XXREAL_0:2;
then (Sum (((1,p) In_Power n) | k)) + (((1,p) In_Power n) . (k + 1)) < ((k * (p |^ k)) / (k !)) + (((p |^ k) * (n |^ k)) / (k !)) by A40, XREAL_1:8;
then Sum (((1,p) In_Power n) | (k + 1)) < ((k * (p |^ k)) + ((p |^ k) * (n |^ k))) / (k !) by A38, XCMPLX_1:62;
then (k !) * (Sum (((1,p) In_Power n) | (k + 1))) < (k !) * (((k * (p |^ k)) + ((p |^ k) * (n |^ k))) / (k !)) by XREAL_1:68;
then A57: (k !) * (Sum (((1,p) In_Power n) | (k + 1))) < (k + (n |^ k)) * (p |^ k) by XCMPLX_1:87;
k + (n |^ k) <= (1 + n) |^ k by A4, Lm2;
then (k + (n |^ k)) * (p |^ k) <= ((1 + n) |^ k) * (p |^ k) by XREAL_1:66;
then (k !) * (Sum (((1,p) In_Power n) | (k + 1))) < ((1 + n) |^ k) * (p |^ k) by A57, XXREAL_0:2;
hence ( ((p + 1) |^ n) mod (p |^ (k + 1)) > 0 & k ! < (((n + 1) |^ k) * (p |^ k)) / (((p + 1) |^ n) mod (p |^ (k + 1))) ) by A36, A20, XREAL_1:81; :: thesis: (((n + 1) |^ k) * (p |^ k)) / (((p + 1) |^ n) mod (p |^ (k + 1))) < (k !) + 1
A58: (n + 1) - k > 0 by A6, XREAL_1:50;
n choose k >= (((n + 1) - k) |^ k) / (k !) by Th7, A4;
then A59: ((n + 1) |^ k) / (n choose k) <= ((n + 1) |^ k) / ((((n + 1) - k) |^ k) / (k !)) by A58, XREAL_1:118;
A60: ((n + 1) |^ k) / ((((n + 1) - k) |^ k) / (k !)) = (k !) * (((n + 1) |^ k) / (((n + 1) - k) |^ k)) by XCMPLX_1:81;
A61: ( (n + 1) / (n + 1) > k / (n + 1) & (n + 1) / (n + 1) = 1 ) by A6, XCMPLX_1:60, XREAL_1:74;
((n + 1) - k) / (n + 1) = ((n + 1) / (n + 1)) - (k / (n + 1)) by XCMPLX_1:120
.= 1 - (k / (n + 1)) by XCMPLX_1:60 ;
then (((n + 1) - k) |^ k) / ((n + 1) |^ k) = (1 - (k / (n + 1))) |^ k by PREPOWER:8;
then A62: ((n + 1) |^ k) / (((n + 1) - k) |^ k) = 1 / ((1 - (k / (n + 1))) |^ k) by XCMPLX_1:57;
A63: ( k * k <= n & (2 * k) * k <= n + 1 )
proof
A64: ( 4 * (k * k) >= 1 * (k * k) & 4 * (k * k) >= 2 * (k * k) ) by XREAL_1:64;
per cases ( k = 1 or k > 1 ) by A2, XXREAL_0:1;
suppose k = 1 ; :: thesis: ( k * k <= n & (2 * k) * k <= n + 1 )
hence ( k * k <= n & (2 * k) * k <= n + 1 ) by A5, NAT_1:13; :: thesis: verum
end;
suppose k > 1 ; :: thesis: ( k * k <= n & (2 * k) * k <= n + 1 )
then k >= 1 + 1 by NAT_1:13;
then ( (2 * k) |^ k >= (2 * k) |^ 2 & (2 * k) |^ 2 = (2 * k) * (2 * k) ) by NAT_6:1, NEWTON:81;
then A65: n >= (2 * k) * (2 * k) by A1, XXREAL_0:2;
then n + 1 >= 4 * (k * k) by NAT_1:13;
hence ( k * k <= n & (2 * k) * k <= n + 1 ) by A64, A65, XXREAL_0:2; :: thesis: verum
end;
end;
end;
then k * k < n + 1 by NAT_1:13;
then 1 > (k * k) / (n + 1) by A61, XREAL_1:74;
then A66: 0 < 1 - ((k * k) / (n + 1)) by XREAL_1:50;
1 - ((k * k) / (n + 1)) <= (1 - (k / (n + 1))) |^ k by Lm3, A6;
then ((n + 1) |^ k) / (((n + 1) - k) |^ k) <= 1 / (1 - ((k * k) / (n + 1))) by A62, A66, XREAL_1:118;
then (k !) * (((n + 1) |^ k) / (((n + 1) - k) |^ k)) <= (k !) * (1 / (1 - ((k * k) / (n + 1)))) by XREAL_1:64;
then A67: ((n + 1) |^ k) / (n choose k) <= (k !) * (1 / (1 - ((k * k) / (n + 1)))) by A59, A60, XXREAL_0:2;
( n + 1 > (2 * k) |^ k & (2 * k) * k > 0 & (2 * k) |^ k > 0 ) by A1, NAT_1:13;
then ((2 * k) * k) / (n + 1) < ((2 * k) * k) / ((2 * k) |^ k) by XREAL_1:76;
then A68: 1 + (((2 * k) * k) / (n + 1)) < 1 + (((2 * k) * k) / ((2 * k) |^ k)) by XREAL_1:8;
1 / (1 - ((k * k) / (n + 1))) <= 1 + ((2 * (k * k)) / (n + 1)) by Lm5, A1, A63;
then 1 / (1 - ((k * k) / (n + 1))) < 1 + ((2 * (k * k)) / ((2 * k) |^ k)) by A68, XXREAL_0:2;
then (k !) * (1 / (1 - ((k * k) / (n + 1)))) < (k !) * (1 + ((2 * (k * k)) / ((2 * k) |^ k))) by XREAL_1:68;
then A69: ((n + 1) |^ k) / (n choose k) < (k !) * (1 + ((2 * (k * k)) / ((2 * k) |^ k))) by A67, XXREAL_0:2;
A70: (k !) * (1 + (1 / (k !))) = ((k !) * 1) + ((k !) * (1 / (k !)))
.= (k !) + ((k !) / (k !)) by XCMPLX_1:74
.= (k !) + 1 by XCMPLX_1:60 ;
A71: n choose k <> 0 by CATALAN2:26, A4;
A72: k * k = k ^2 by SQUARE_1:def 1;
1 * ((2 * k) |^ k) >= (2 * (k ^2)) * (k !)
proof
per cases ( k = 1 or k > 1 ) by A2, XXREAL_0:1;
suppose k = 1 ; :: thesis: 1 * ((2 * k) |^ k) >= (2 * (k ^2)) * (k !)
hence 1 * ((2 * k) |^ k) >= (2 * (k ^2)) * (k !) by A72, NEWTON:13; :: thesis: verum
end;
suppose k > 1 ; :: thesis: 1 * ((2 * k) |^ k) >= (2 * (k ^2)) * (k !)
then A73: k >= 1 + 1 by NAT_1:13;
then reconsider k2 = k - 2 as Nat by NAT_1:21;
k -' 2 = k2 by A73, XREAL_1:233;
then k ! <= (2 !) * (k |^ k2) by A73, Th10;
then (k !) * k <= (2 * (k |^ k2)) * k by XREAL_1:64, NEWTON:14;
then ((k !) * k) * k <= ((2 * (k |^ k2)) * k) * k by XREAL_1:64;
then A74: (((k !) * k) * k) * 2 <= (((2 * (k |^ k2)) * k) * k) * 2 by XREAL_1:64;
A75: k |^ ((k2 + 1) + 1) = k * (k |^ (k2 + 1)) by NEWTON:6
.= (k * (k |^ k2)) * k by NEWTON:6 ;
( 2 * 2 = 2 |^ 2 & 2 |^ 2 <= 2 |^ k ) by A73, NAT_6:1, NEWTON:81;
then (2 * 2) * (((k |^ k2) * k) * k) <= (2 |^ k) * (k |^ k) by A75, XREAL_1:64;
then ( (((k !) * k) * k) * 2 <= (2 |^ k) * (k |^ k) & (2 |^ k) * (k |^ k) = (2 * k) |^ k ) by A74, XXREAL_0:2, NEWTON:7;
hence 1 * ((2 * k) |^ k) >= (2 * (k ^2)) * (k !) by A72; :: thesis: verum
end;
end;
end;
then 1 / (k !) >= (2 * (k ^2)) / ((2 * k) |^ k) by A1, XREAL_1:102;
then 1 + (1 / (k !)) >= 1 + ((2 * (k ^2)) / ((2 * k) |^ k)) by XREAL_1:6;
then (k !) * (1 + (1 / (k !))) >= (k !) * (1 + ((2 * (k ^2)) / ((2 * k) |^ k))) by XREAL_1:66;
then A76: ((n + 1) |^ k) / (n choose k) < (k !) + 1 by A72, A70, A69, XXREAL_0:2;
Sum (((1,p) In_Power n) | (k + 1)) >= (((1,p) In_Power n) . (k + 1)) + 0 by A38, XREAL_1:7;
then A77: (((n + 1) |^ k) * (p |^ k)) / ((n choose k) * (p |^ k)) >= (((n + 1) |^ k) * (p |^ k)) / (Sum (((1,p) In_Power n) | (k + 1))) by A39, A71, A1, XREAL_1:118;
((n + 1) |^ k) / (n choose k) = (((n + 1) |^ k) * (p |^ k)) / ((n choose k) * (p |^ k)) by XCMPLX_1:91, A1;
hence (((n + 1) |^ k) * (p |^ k)) / (((p + 1) |^ n) mod (p |^ (k + 1))) < (k !) + 1 by A36, A76, A77, XXREAL_0:2; :: thesis: verum