let a, b, n be Element of NAT ; :: thesis: ((GenFib (a,b,(n + 2))) * (GenFib (a,b,n))) - ((GenFib (a,b,(n + 1))) |^ 2) = ((- 1) to_power n) * (((GenFib (a,b,2)) |^ 2) - ((GenFib (a,b,1)) * (GenFib (a,b,3))))
defpred S1[ Nat] means ((GenFib (a,b,($1 + 2))) * (GenFib (a,b,$1))) - ((GenFib (a,b,($1 + 1))) |^ 2) = ((- 1) to_power $1) * (((GenFib (a,b,2)) |^ 2) - ((GenFib (a,b,1)) * (GenFib (a,b,3))));
A1: GenFib (a,b,2) = GenFib (a,b,(0 + 2))
.= (GenFib (a,b,0)) + (GenFib (a,b,(0 + 1))) by Th34
.= a + (GenFib (a,b,1)) by Th32
.= a + b by Th32 ;
A2: GenFib (a,b,3) = GenFib (a,b,(1 + 2))
.= (GenFib (a,b,1)) + (GenFib (a,b,(1 + 1))) by Th32
.= b + (a + b) by A1, Th32
.= (2 * b) + a ;
then ((GenFib (a,b,(1 + 2))) * (GenFib (a,b,1))) - ((GenFib (a,b,(1 + 1))) |^ 2) = (((2 * b) + a) * b) - ((a + b) |^ 2) by A1, Th32
.= (((2 * b) * b) + (a * b)) - ((a + b) * (a + b)) by WSIERP_1:1
.= (- 1) * (((a + b) * (a + b)) - (b * ((2 * b) + a)))
.= ((- 1) to_power 1) * (((a + b) * (a + b)) - (b * ((2 * b) + a))) by POWER:25
.= ((- 1) to_power 1) * (((a + b) |^ 2) - (b * (GenFib (a,b,3)))) by A2, WSIERP_1:1
.= ((- 1) to_power 1) * (((GenFib (a,b,2)) |^ 2) - ((GenFib (a,b,1)) * (GenFib (a,b,3)))) by A1, Th32 ;
then A3: S1[1] ;
A4: for k being Nat st S1[k] & S1[k + 1] holds
S1[k + 2]
proof
let k be Nat; :: thesis: ( S1[k] & S1[k + 1] implies S1[k + 2] )
assume that
A5: S1[k] and
A6: S1[k + 1] ; :: thesis: S1[k + 2]
set d = (GenFib (a,b,(k + 2))) * (GenFib (a,b,k));
A7: ((- 1) to_power (k + 1)) + ((- 1) to_power k) = (((- 1) to_power k) * ((- 1) to_power 1)) + ((- 1) to_power k) by FIB_NUM2:5
.= (((- 1) to_power k) * (- 1)) + ((- 1) to_power k) by POWER:25
.= 0 ;
(GenFib (a,b,2)) |^ 2 = (GenFib (a,b,(0 + 2))) |^ 2
.= ((GenFib (a,b,0)) + (GenFib (a,b,(0 + 1)))) |^ 2 by Th34
.= (a + (GenFib (a,b,1))) |^ 2 by Th32
.= (a + b) |^ 2 by Th32 ;
then A8: ((GenFib (a,b,2)) |^ 2) - ((GenFib (a,b,1)) * (GenFib (a,b,3))) = ((a + b) |^ 2) - (b * (GenFib (a,b,(1 + 2)))) by Th32
.= ((a + b) |^ 2) - (b * ((GenFib (a,b,1)) + (GenFib (a,b,(1 + 1))))) by Th34
.= ((a + b) |^ 2) - (b * (b + (GenFib (a,b,(0 + 2))))) by Th32
.= ((a + b) |^ 2) - (b * (b + ((GenFib (a,b,0)) + (GenFib (a,b,(0 + 1)))))) by Th34
.= ((a + b) |^ 2) - (b * (b + (a + (GenFib (a,b,1))))) by Th32
.= ((a + b) |^ 2) - (b * (b + (a + b))) by Th32
.= ((((a + b) |^ 2) - (b * b)) - (b * a)) - (b * b)
.= ((((((a * a) + (a * b)) + (b * a)) + (b * b)) - (b * b)) - (b * a)) - (b * b) by Th5
.= ((a * a) + (a * b)) - (b * b) ;
then ((GenFib (a,b,(k + 2))) * (GenFib (a,b,k))) - ((GenFib (a,b,(k + 1))) |^ 2) = ((- 1) to_power k) * (((a * a) + (a * b)) - (b * b)) by A5;
then A9: (((- 1) to_power (k + 1)) * (((a * a) + (a * b)) - (b * b))) + (((GenFib (a,b,(k + 2))) * (GenFib (a,b,k))) - ((GenFib (a,b,(k + 1))) |^ 2)) = (((- 1) to_power (k + 1)) + ((- 1) to_power k)) * (((a * a) + (a * b)) - (b * b))
.= (((a * a) + (a * b)) - (b * b)) * 0 by A7 ;
set c = (GenFib (a,b,((k + 2) + 1))) * (GenFib (a,b,(k + 1)));
A10: ((GenFib (a,b,((k + 2) + 1))) * (GenFib (a,b,(k + 1)))) - ((GenFib (a,b,((k + 1) + 1))) |^ 2) = ((- 1) to_power (k + 1)) * (((GenFib (a,b,2)) |^ 2) - ((GenFib (a,b,1)) * (GenFib (a,b,3)))) by A6;
A11: (((GenFib (a,b,((k + 2) + 1))) * (GenFib (a,b,(k + 1)))) + ((GenFib (a,b,(k + 2))) * (GenFib (a,b,k)))) - (((GenFib (a,b,(k + 1))) + (GenFib (a,b,((k + 1) + 1)))) |^ 2) = (((GenFib (a,b,((k + 2) + 1))) * (GenFib (a,b,(k + 1)))) + ((GenFib (a,b,(k + 2))) * (GenFib (a,b,k)))) - ((((GenFib (a,b,(k + 1))) |^ 2) + ((2 * (GenFib (a,b,(k + 1)))) * (GenFib (a,b,((k + 1) + 1))))) + ((GenFib (a,b,((k + 1) + 1))) |^ 2)) by Th33
.= (((((- 1) to_power (k + 1)) * (((GenFib (a,b,2)) |^ 2) - ((GenFib (a,b,1)) * (GenFib (a,b,3))))) + ((GenFib (a,b,(k + 2))) * (GenFib (a,b,k)))) - ((GenFib (a,b,(k + 1))) |^ 2)) - ((2 * (GenFib (a,b,(k + 1)))) * (GenFib (a,b,((k + 1) + 1)))) by A10
.= (((((- 1) to_power (k + 1)) * (((a * a) + (a * b)) - (b * b))) + ((GenFib (a,b,(k + 2))) * (GenFib (a,b,k)))) - ((GenFib (a,b,(k + 1))) |^ 2)) - ((2 * (GenFib (a,b,(k + 1)))) * (GenFib (a,b,((k + 1) + 1)))) by A8
.= - ((2 * (GenFib (a,b,(k + 1)))) * (GenFib (a,b,((k + 1) + 1)))) by A9 ;
((GenFib (a,b,((k + 2) + 2))) * (GenFib (a,b,(k + 2)))) - ((GenFib (a,b,((k + 2) + 1))) |^ 2) = (((GenFib (a,b,(k + 2))) + (GenFib (a,b,((k + 2) + 1)))) * (GenFib (a,b,(k + 2)))) - ((GenFib (a,b,((k + 2) + 1))) |^ 2) by Th34
.= (((GenFib (a,b,((k + 2) + 1))) + (GenFib (a,b,(k + 2)))) * ((GenFib (a,b,k)) + (GenFib (a,b,(k + 1))))) - ((GenFib (a,b,((k + 1) + 2))) |^ 2) by Th34
.= (((((GenFib (a,b,((k + 2) + 1))) * (GenFib (a,b,k))) + ((GenFib (a,b,((k + 2) + 1))) * (GenFib (a,b,(k + 1))))) + ((GenFib (a,b,(k + 2))) * (GenFib (a,b,k)))) + ((GenFib (a,b,(k + 2))) * (GenFib (a,b,(k + 1))))) - (((GenFib (a,b,(k + 1))) + (GenFib (a,b,((k + 1) + 1)))) |^ 2) by Th32
.= (((GenFib (a,b,((k + 2) + 1))) * (GenFib (a,b,k))) + ((GenFib (a,b,(k + 2))) * (GenFib (a,b,(k + 1))))) + ((((GenFib (a,b,((k + 2) + 1))) * (GenFib (a,b,(k + 1)))) + ((GenFib (a,b,(k + 2))) * (GenFib (a,b,k)))) - (((GenFib (a,b,(k + 1))) + (GenFib (a,b,((k + 1) + 1)))) |^ 2))
.= (((GenFib (a,b,((k + 2) + 1))) * (GenFib (a,b,k))) + ((GenFib (a,b,(k + 2))) * (GenFib (a,b,(k + 1))))) + (- ((2 * (GenFib (a,b,(k + 1)))) * (GenFib (a,b,(k + 2))))) by A11
.= ((GenFib (a,b,((k + 1) + 2))) * (GenFib (a,b,k))) - ((GenFib (a,b,(k + 2))) * (GenFib (a,b,(k + 1))))
.= (((GenFib (a,b,(k + 1))) + (GenFib (a,b,((k + 1) + 1)))) * (GenFib (a,b,k))) - ((GenFib (a,b,(k + 2))) * (GenFib (a,b,(k + 1)))) by Th34
.= (((GenFib (a,b,(k + 1))) * (GenFib (a,b,k))) + ((GenFib (a,b,(k + 2))) * (GenFib (a,b,k)))) - (((GenFib (a,b,k)) + (GenFib (a,b,(k + 1)))) * (GenFib (a,b,(k + 1)))) by Th34
.= ((GenFib (a,b,(k + 2))) * (GenFib (a,b,k))) - ((GenFib (a,b,(k + 1))) * (GenFib (a,b,(k + 1))))
.= (((- 1) to_power k) * 1) * (((GenFib (a,b,2)) |^ 2) - ((GenFib (a,b,1)) * (GenFib (a,b,3)))) by A5, WSIERP_1:1
.= (((- 1) to_power k) * (1 to_power 2)) * (((GenFib (a,b,2)) |^ 2) - ((GenFib (a,b,1)) * (GenFib (a,b,3)))) by POWER:26
.= (((- 1) to_power k) * ((- 1) to_power 2)) * (((GenFib (a,b,2)) |^ 2) - ((GenFib (a,b,1)) * (GenFib (a,b,3)))) by Th3
.= ((- 1) to_power (k + 2)) * (((GenFib (a,b,2)) |^ 2) - ((GenFib (a,b,1)) * (GenFib (a,b,3)))) by FIB_NUM2:5 ;
hence S1[k + 2] ; :: thesis: verum
end;
((GenFib (a,b,(0 + 2))) * (GenFib (a,b,0))) - ((GenFib (a,b,(0 + 1))) |^ 2) = ((GenFib (a,b,2)) * a) - ((GenFib (a,b,1)) |^ 2) by Th32
.= ((a + b) * a) - (b |^ 2) by A1, Th32
.= ((a * a) + (b * a)) - (b * b) by WSIERP_1:1
.= ((a + b) * (a + b)) - (b * ((2 * b) + a))
.= 1 * (((GenFib (a,b,2)) |^ 2) - (b * (GenFib (a,b,3)))) by A1, A2, WSIERP_1:1
.= ((- 1) to_power 0) * (((GenFib (a,b,2)) |^ 2) - (b * (GenFib (a,b,3)))) by POWER:24
.= ((- 1) to_power 0) * (((GenFib (a,b,2)) |^ 2) - ((GenFib (a,b,1)) * (GenFib (a,b,3)))) by Th32 ;
then A12: S1[ 0 ] ;
for k being Nat holds S1[k] from FIB_NUM:sch 1(A12, A3, A4);
 hence ((GenFib (a,b,(n + 2))) * (GenFib (a,b,n))) - ((GenFib (a,b,(n + 1))) |^ 2) = ((- 1) to_power n) * (((GenFib (a,b,2)) |^ 2) - ((GenFib (a,b,1)) * (GenFib (a,b,3)))) ; :: thesis: verum