defpred S₁[ Nat] means for a, b, c, d being Nat st a <= b & b <= c & 2 * c <= d & c > 0 & b - a = $1 holds
for f being FinSequence of REAL st len f = (b - a) + 1 & ( for i being Nat st i + 1 in dom f holds
f . (i + 1) = (c choose (a + i)) * (d |^ (c -' (a + i))) ) holds
( 0 <= 1 - ((c / d) |^ ((b + 1) -' a)) & 0 < Sum f & Sum f <= (((1 - ((c / d) |^ ((b + 1) -' a))) / (1 - (c / d))) * (c |^ a)) * (d |^ (c -' a)) );
A1: S₁[ 0 ]

proof

let a, b, c, d be Nat; :: thesis: ( a <= b & b <= c & 2 * c <= d & c > 0 & b - a = 0 implies for f being FinSequence of REAL st len f = (b - a) + 1 & ( for i being Nat st i + 1 in dom f holds
f . (i + 1) = (c choose (a + i)) * (d |^ (c -' (a + i))) ) holds
( 0 <= 1 - ((c / d) |^ ((b + 1) -' a)) & 0 < Sum f & Sum f <= (((1 - ((c / d) |^ ((b + 1) -' a))) / (1 - (c / d))) * (c |^ a)) * (d |^ (c -' a)) ) )
assume A2: ( a <= b & b <= c & 2 * c <= d & c > 0 & b - a = 0 ) ; :: thesis: for f being FinSequence of REAL st len f = (b - a) + 1 & ( for i being Nat st i + 1 in dom f holds
f . (i + 1) = (c choose (a + i)) * (d |^ (c -' (a + i))) ) holds
( 0 <= 1 - ((c / d) |^ ((b + 1) -' a)) & 0 < Sum f & Sum f <= (((1 - ((c / d) |^ ((b + 1) -' a))) / (1 - (c / d))) * (c |^ a)) * (d |^ (c -' a)) )
A3: d > 0 by A2;
let f be FinSequence of REAL ; :: thesis: ( len f = (b - a) + 1 & ( for i being Nat st i + 1 in dom f holds
f . (i + 1) = (c choose (a + i)) * (d |^ (c -' (a + i))) ) implies ( 0 <= 1 - ((c / d) |^ ((b + 1) -' a)) & 0 < Sum f & Sum f <= (((1 - ((c / d) |^ ((b + 1) -' a))) / (1 - (c / d))) * (c |^ a)) * (d |^ (c -' a)) ) )
assume that
A4: len f = (b - a) + 1 and
A5: for i being Nat st i + 1 in dom f holds
f . (i + 1) = (c choose (a + i)) * (d |^ (c -' (a + i))) ; :: thesis: ( 0 <= 1 - ((c / d) |^ ((b + 1) -' a)) & 0 < Sum f & Sum f <= (((1 - ((c / d) |^ ((b + 1) -' a))) / (1 - (c / d))) * (c |^ a)) * (d |^ (c -' a)) )
A6: f . 1 = (c choose (a + 0)) * (d |^ (c -' (a + 0))) by A5, FINSEQ_3:25, A2, A4;
then reconsider f1 = f . 1 as Nat ;
c -' a = c - a by A2, XREAL_1:233;
then A7: (c -' a) + a = c ;
A8: f = <*f1*> by A2, A4, FINSEQ_1:40;
A9: 1 - (c / d) > 0

proof

assume 1 - (c / d) <= 0 ; :: thesis: contradiction
then 1 <= c / d by XREAL_1:50;
then 1 * d <= (c / d) * d by XREAL_1:64;
then d <= c by XCMPLX_1:87;
then c + c <= c + 0 by A2, XXREAL_0:2;
hence contradiction by A2, XREAL_1:6; :: thesis: verum

end;

b + 1 > a by A2, NAT_1:13;
then (b + 1) -' a = (b + 1) - a by XREAL_1:233;
then A10: (1 - ((c / d) |^ ((b + 1) -' a))) / (1 - (c / d)) = 1 by A2, A9, XCMPLX_1:60;
( c choose a <= (c |^ a) / (a !) & (c |^ a) / (a !) <= (c |^ a) / 1 ) by NAT_1:14, XREAL_1:118, A2, HILB10_6:8;
then c choose a <= c |^ a by XXREAL_0:2;
hence ( 0 <= 1 - ((c / d) |^ ((b + 1) -' a)) & 0 < Sum f & Sum f <= (((1 - ((c / d) |^ ((b + 1) -' a))) / (1 - (c / d))) * (c |^ a)) * (d |^ (c -' a)) ) by A3, A6, A8, A7, A9, A10, XREAL_1:64; :: thesis: verum

end;

A11: for n being Nat st S₁[n] holds
S₁[n + 1]

proof

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A12: S₁[n] ; :: thesis: S₁[n + 1]
set n1 = n + 1;
let a, b, c, d be Nat; :: thesis: ( a <= b & b <= c & 2 * c <= d & c > 0 & b - a = n + 1 implies for f being FinSequence of REAL st len f = (b - a) + 1 & ( for i being Nat st i + 1 in dom f holds
f . (i + 1) = (c choose (a + i)) * (d |^ (c -' (a + i))) ) holds
( 0 <= 1 - ((c / d) |^ ((b + 1) -' a)) & 0 < Sum f & Sum f <= (((1 - ((c / d) |^ ((b + 1) -' a))) / (1 - (c / d))) * (c |^ a)) * (d |^ (c -' a)) ) )
assume A13: ( a <= b & b <= c & 2 * c <= d & c > 0 & b - a = n + 1 ) ; :: thesis: for f being FinSequence of REAL st len f = (b - a) + 1 & ( for i being Nat st i + 1 in dom f holds
f . (i + 1) = (c choose (a + i)) * (d |^ (c -' (a + i))) ) holds
( 0 <= 1 - ((c / d) |^ ((b + 1) -' a)) & 0 < Sum f & Sum f <= (((1 - ((c / d) |^ ((b + 1) -' a))) / (1 - (c / d))) * (c |^ a)) * (d |^ (c -' a)) )
A14: d > 0 by A13;
let f be FinSequence of REAL ; :: thesis: ( len f = (b - a) + 1 & ( for i being Nat st i + 1 in dom f holds
f . (i + 1) = (c choose (a + i)) * (d |^ (c -' (a + i))) ) implies ( 0 <= 1 - ((c / d) |^ ((b + 1) -' a)) & 0 < Sum f & Sum f <= (((1 - ((c / d) |^ ((b + 1) -' a))) / (1 - (c / d))) * (c |^ a)) * (d |^ (c -' a)) ) )
assume that
A15: len f = (b - a) + 1 and
A16: for i being Nat st i + 1 in dom f holds
f . (i + 1) = (c choose (a + i)) * (d |^ (c -' (a + i))) ; :: thesis: ( 0 <= 1 - ((c / d) |^ ((b + 1) -' a)) & 0 < Sum f & Sum f <= (((1 - ((c / d) |^ ((b + 1) -' a))) / (1 - (c / d))) * (c |^ a)) * (d |^ (c -' a)) )
set 1cd = 1 - (c / d);
b <> 0 by A13;
then reconsider B = b - 1 as Nat ;
set F = f | (n + 1);
f = (f | (n + 1)) ^ <*(f . ((n + 1) + 1))*> by A13, A15, FINSEQ_3:55;
then A17: Sum f = (Sum (f | (n + 1))) + (f . ((n + 1) + 1)) by RVSUM_1:74;
( c choose (a + (n + 1)) <= (c |^ (a + (n + 1))) / ((a + (n + 1)) !) & (c |^ (a + (n + 1))) / ((a + (n + 1)) !) <= (c |^ (a + (n + 1))) / 1 ) by NAT_1:14, XREAL_1:118, A13, HILB10_6:8;
then A18: c choose (a + (n + 1)) <= c |^ (a + (n + 1)) by XXREAL_0:2;
1 <= (n + 1) + 1 by NAT_1:11;
then A19: f . ((n + 1) + 1) = (c choose (a + (n + 1))) * (d |^ (c -' (a + (n + 1)))) by A16, A13, A15, FINSEQ_3:25;
then A20: f . ((n + 1) + 1) <= (c |^ (a + (n + 1))) * (d |^ (c -' (a + (n + 1)))) by A18, XREAL_1:64;
A21: n + 1 < (n + 1) + 1 by NAT_1:13;
A22: len (f | (n + 1)) = (B - a) + 1 by A21, A13, A15, FINSEQ_1:59;
A23: for i being Nat st i + 1 in dom (f | (n + 1)) holds
(f | (n + 1)) . (i + 1) = (c choose (a + i)) * (d |^ (c -' (a + i)))

proof

let i be Nat; :: thesis: ( i + 1 in dom (f | (n + 1)) implies (f | (n + 1)) . (i + 1) = (c choose (a + i)) * (d |^ (c -' (a + i))) )
assume A24: i + 1 in dom (f | (n + 1)) ; :: thesis: (f | (n + 1)) . (i + 1) = (c choose (a + i)) * (d |^ (c -' (a + i)))
( i + 1 in dom f & f . (i + 1) = (f | (n + 1)) . (i + 1) ) by A24, RELAT_1:57, FUNCT_1:47;
hence (f | (n + 1)) . (i + 1) = (c choose (a + i)) * (d |^ (c -' (a + i))) by A16; :: thesis: verum

end;

B + 1 <= c by A13;
then A25: B < c by NAT_1:13;
A26: ( a <= a + n & a + n < (a + n) + 1 ) by NAT_1:11, NAT_1:13;
A27: ( 0 < Sum (f | (n + 1)) & Sum (f | (n + 1)) <= (((1 - ((c / d) |^ ((B + 1) -' a))) / (1 - (c / d))) * (c |^ a)) * (d |^ (c -' a)) ) by A12, A26, A13, A22, A23, A25;
(c / d) * d = c by A14, XCMPLX_1:87;
then A28: c |^ (n + 1) = ((c / d) |^ (n + 1)) * (d |^ (n + 1)) by NEWTON:7;
( c -' (a + (n + 1)) = c - (a + (n + 1)) & c -' a = c - a ) by A13, XXREAL_0:2, XREAL_1:233;
then A29: c -' a = (n + 1) + (c -' (a + (n + 1))) ;
A30: 1 - (c / d) > 0

proof

assume 1 - (c / d) <= 0 ; :: thesis: contradiction
then 1 <= c / d by XREAL_1:50;
then 1 * d <= (c / d) * d by XREAL_1:64;
then d <= c by XCMPLX_1:87;
then c + c <= c + 0 by A13, XXREAL_0:2;
hence contradiction by A13, XREAL_1:6; :: thesis: verum

end;

A31: ((((1 - ((c / d) |^ ((B + 1) -' a))) / (1 - (c / d))) * (c |^ a)) * (d |^ (c -' a))) + (((c |^ a) * ((c / d) |^ (n + 1))) * (d |^ (c -' a))) = (((1 - ((c / d) |^ ((B + 1) -' a))) / (1 - (c / d))) + ((c / d) |^ (n + 1))) * ((c |^ a) * (d |^ (c -' a))) ;
A32: b -' a = n + 1 by A13, XREAL_1:233;
a < b + 1 by A13, NAT_1:13;
then A33: (b + 1) -' a = (b + 1) - a by XREAL_1:233;
A34: (1 - ((c / d) |^ ((B + 1) -' a))) + (((c / d) |^ (n + 1)) * (1 - (c / d))) = ((1 - ((c / d) |^ (n + 1))) + ((c / d) |^ (n + 1))) - (((c / d) |^ (n + 1)) * (c / d)) by A32
.= 1 - ((c / d) |^ ((n + 1) + 1)) by NEWTON:6
.= 1 - ((c / d) |^ ((b + 1) -' a)) by A33, A13 ;
A35: ((1 - ((c / d) |^ ((B + 1) -' a))) / (1 - (c / d))) + ((c / d) |^ (n + 1)) = ((1 - ((c / d) |^ ((B + 1) -' a))) / (1 - (c / d))) + ((((c / d) |^ (n + 1)) * (1 - (c / d))) / (1 - (c / d))) by A30, XCMPLX_1:89
.= ((1 - ((c / d) |^ ((B + 1) -' a))) + (((c / d) |^ (n + 1)) * (1 - (c / d)))) / (1 - (c / d)) by XCMPLX_1:62 ;
(c |^ (a + (n + 1))) * (d |^ (c -' (a + (n + 1)))) = ((c |^ a) * (((c / d) |^ (n + 1)) * (d |^ (n + 1)))) * (d |^ (c -' (a + (n + 1)))) by NEWTON:8, A28
.= ((c |^ a) * ((c / d) |^ (n + 1))) * ((d |^ (n + 1)) * (d |^ (c -' (a + (n + 1)))))
.= ((c |^ a) * ((c / d) |^ (n + 1))) * (d |^ (c -' a)) by A29, NEWTON:8 ;
hence ( 0 <= 1 - ((c / d) |^ ((b + 1) -' a)) & 0 < Sum f & Sum f <= (((1 - ((c / d) |^ ((b + 1) -' a))) / (1 - (c / d))) * (c |^ a)) * (d |^ (c -' a)) ) by A19, A35, A17, A27, A20, A30, A34, XREAL_1:7, A31; :: thesis: verum

end;

let a, b, c, d be Nat; :: thesis: ( a <= b & b <= c & 2 * c <= d & c > 0 implies for f being FinSequence of REAL st len f = (b - a) + 1 & ( for i being Nat st i + 1 in dom f holds
f . (i + 1) = (c choose (a + i)) * (d |^ (c -' (a + i))) ) holds
( 0 < Sum f & Sum f < (2 * (c |^ a)) * (d |^ (c -' a)) ) )
assume A36: ( a <= b & b <= c & 2 * c <= d & c > 0 ) ; :: thesis: for f being FinSequence of REAL st len f = (b - a) + 1 & ( for i being Nat st i + 1 in dom f holds
f . (i + 1) = (c choose (a + i)) * (d |^ (c -' (a + i))) ) holds
( 0 < Sum f & Sum f < (2 * (c |^ a)) * (d |^ (c -' a)) )
A37: d > 0 by A36;
let f be FinSequence of REAL ; :: thesis: ( len f = (b - a) + 1 & ( for i being Nat st i + 1 in dom f holds
f . (i + 1) = (c choose (a + i)) * (d |^ (c -' (a + i))) ) implies ( 0 < Sum f & Sum f < (2 * (c |^ a)) * (d |^ (c -' a)) ) )
assume A38: ( len f = (b - a) + 1 & ( for i being Nat st i + 1 in dom f holds
f . (i + 1) = (c choose (a + i)) * (d |^ (c -' (a + i))) ) ) ; :: thesis: ( 0 < Sum f & Sum f < (2 * (c |^ a)) * (d |^ (c -' a)) )
reconsider ba = b - a as Nat by A36, NAT_1:21;
for n being Nat holds S₁[n] from NAT_1:sch 2(A1, A11);
then A39: S₁[ba] ;
then A40: ( 0 < Sum f & Sum f <= (((1 - ((c / d) |^ ((b + 1) -' a))) / (1 - (c / d))) * (c |^ a)) * (d |^ (c -' a)) ) by A36, A38;
A41: 1 - ((c / d) |^ ((b + 1) -' a)) >= 0 by A36, A38, A39;
2 * c <= d * 1 by A36;
then c / d <= 1 / 2 by A37, XREAL_1:102;
then 1 - (c / d) >= 1 - (1 / 2) by XREAL_1:10;
then A42: (1 - ((c / d) |^ ((b + 1) -' a))) / (1 - (c / d)) <= (1 - ((c / d) |^ ((b + 1) -' a))) / (1 / 2) by A41, XREAL_1:118;
1 - ((c / d) |^ ((b + 1) -' a)) < 1 - 0 by A36, A37, XREAL_1:10;
then (1 - ((c / d) |^ ((b + 1) -' a))) * 2 < (1 - 0) * 2 by XREAL_1:68;
then (1 - ((c / d) |^ ((b + 1) -' a))) / (1 - (c / d)) < 2 by A42, XXREAL_0:2;
then ((1 - ((c / d) |^ ((b + 1) -' a))) / (1 - (c / d))) * ((c |^ a) * (d |^ (c -' a))) < 2 * ((c |^ a) * (d |^ (c -' a))) by A36, A37, XREAL_1:68;
hence ( 0 < Sum f & Sum f < (2 * (c |^ a)) * (d |^ (c -' a)) ) by A40, XXREAL_0:2; :: thesis: verum