set T = tau ;
set S = 1 / (sqrt 5);
reconsider T = tau as non zero Real by Th33;
let n, r be non zero Element of NAT ; ( r <= n implies ((Fib n) ^2) - ((Fib (n + r)) * (Fib (n -' r))) = ((- 1) |^ (n -' r)) * ((Fib r) ^2) )
assume A1:
r <= n
; ((Fib n) ^2) - ((Fib (n + r)) * (Fib (n -' r))) = ((- 1) |^ (n -' r)) * ((Fib r) ^2)
set Y = n -' r;
set X = n + r;
A2: (n + r) + (n -' r) =
(r + n) + (n - r)
by A1, XREAL_1:233
.=
((r + n) + n) - r
.=
(r + (2 * n)) -' r
by NAT_1:12, XREAL_1:233
.=
(r -' r) + (2 * n)
by NAT_D:38
.=
0 + (2 * n)
by XREAL_1:232
.=
2 * n
;
A3: (n + r) - (n -' r) =
(n + r) - (n - r)
by A1, XREAL_1:233
.=
2 * r
;
set tyu = T to_power (- (n -' r));
set txu = T to_power (- (n + r));
set tnu = T to_power (- n);
set ty = T to_power (n -' r);
set tx = T to_power (n + r);
set tn = T to_power n;
A4:
( - T <> 0 & - 1 = (2 * (- 1)) + 1 )
;
((Fib n) ^2) - ((Fib (n + r)) * (Fib (n -' r))) =
((((T to_power n) - (tau_bar to_power n)) / (sqrt 5)) ^2) - ((Fib (n + r)) * (Fib (n -' r)))
by FIB_NUM:7
.=
((((T to_power n) - (tau_bar to_power n)) / (sqrt 5)) ^2) - ((((T to_power (n + r)) - (tau_bar to_power (n + r))) / (sqrt 5)) * (Fib (n -' r)))
by FIB_NUM:7
.=
((((T to_power n) - (tau_bar to_power n)) / (sqrt 5)) ^2) - ((((T to_power (n + r)) - (tau_bar to_power (n + r))) / (sqrt 5)) * (((T to_power (n -' r)) - (tau_bar to_power (n -' r))) / (sqrt 5)))
by FIB_NUM:7
.=
((((T to_power n) - (tau_bar to_power n)) * (1 / (sqrt 5))) ^2) - ((((T to_power (n + r)) - (tau_bar to_power (n + r))) / (sqrt 5)) * (((T to_power (n -' r)) - (tau_bar to_power (n -' r))) / (sqrt 5)))
by XCMPLX_1:99
.=
((((T to_power n) - (tau_bar to_power n)) * (1 / (sqrt 5))) ^2) - ((((T to_power (n + r)) - (tau_bar to_power (n + r))) * (1 / (sqrt 5))) * (((T to_power (n -' r)) - (tau_bar to_power (n -' r))) / (sqrt 5)))
by XCMPLX_1:99
.=
((((T to_power n) - (tau_bar to_power n)) * (1 / (sqrt 5))) ^2) - ((((T to_power (n + r)) - (tau_bar to_power (n + r))) * (1 / (sqrt 5))) * (((T to_power (n -' r)) - (tau_bar to_power (n -' r))) * (1 / (sqrt 5))))
by XCMPLX_1:99
.=
((1 / (sqrt 5)) ^2) * (((((T to_power n) ^2) - ((2 * (T to_power n)) * (((- T) to_power (- 1)) to_power n))) + ((((- T) to_power (- 1)) to_power n) ^2)) - (((T to_power (n + r)) - (((- T) to_power (- 1)) to_power (n + r))) * ((T to_power (n -' r)) - (((- T) to_power (- 1)) to_power (n -' r)))))
by Th34
.=
((1 / (sqrt 5)) ^2) * (((((T to_power n) ^2) - ((2 * (T to_power n)) * ((- T) to_power ((- 1) * n)))) + ((((- T) to_power (- 1)) to_power n) ^2)) - (((T to_power (n + r)) - (((- T) to_power (- 1)) to_power (n + r))) * ((T to_power (n -' r)) - (((- T) to_power (- 1)) to_power (n -' r)))))
by A4, Th6
.=
((1 / (sqrt 5)) ^2) * (((((T to_power n) ^2) - ((2 * (T to_power n)) * ((- T) to_power (- n)))) + (((- T) to_power ((- 1) * n)) ^2)) - (((T to_power (n + r)) - (((- T) to_power (- 1)) to_power (n + r))) * ((T to_power (n -' r)) - (((- T) to_power (- 1)) to_power (n -' r)))))
by A4, Th6
.=
((1 / (sqrt 5)) ^2) * (((((T to_power n) ^2) - ((2 * (T to_power n)) * ((- T) to_power (- n)))) + (((- T) to_power (- n)) ^2)) - (((T to_power (n + r)) - ((- T) to_power ((- 1) * (n + r)))) * ((T to_power (n -' r)) - (((- T) to_power (- 1)) to_power (n -' r)))))
by Th35
.=
((1 / (sqrt 5)) ^2) * (((((T to_power n) ^2) - ((2 * (T to_power n)) * ((- T) to_power (- n)))) + (((- T) to_power (- n)) ^2)) - (((T to_power (n + r)) - ((- T) to_power (- (n + r)))) * ((T to_power (n -' r)) - ((- T) to_power ((- 1) * (n -' r))))))
by Th35
.=
((1 / (sqrt 5)) ^2) * ((((((((T to_power n) ^2) - ((2 * (T to_power n)) * (((- 1) * T) to_power (- n)))) + ((((- 1) * T) to_power (- n)) ^2)) - ((T to_power (n + r)) * (T to_power (n -' r)))) + ((T to_power (n + r)) * (((- 1) * T) to_power (- (n -' r))))) + ((((- 1) * T) to_power (- (n + r))) * (T to_power (n -' r)))) - ((((- 1) * T) to_power (- (n + r))) * (((- 1) * T) to_power (- (n -' r)))))
.=
((1 / (sqrt 5)) ^2) * ((((((((T to_power n) ^2) - ((2 * (T to_power n)) * (((- 1) * T) to_power (- n)))) + ((((- 1) * T) to_power (- n)) ^2)) - ((T to_power (n + r)) * (T to_power (n -' r)))) + ((T to_power (n + r)) * (((- 1) * T) to_power (- (n -' r))))) + ((((- 1) * T) to_power (- (n + r))) * (T to_power (n -' r)))) - ((((- 1) * T) to_power (- (n + r))) * (((- 1) to_power (- (n -' r))) * (T to_power (- (n -' r))))))
by Th4
.=
((1 / (sqrt 5)) ^2) * ((((((((T to_power n) ^2) - ((2 * (T to_power n)) * (((- 1) to_power (- n)) * (T to_power (- n))))) + ((((- 1) * T) to_power (- n)) ^2)) - ((T to_power (n + r)) * (T to_power (n -' r)))) + ((T to_power (n + r)) * (((- 1) * T) to_power (- (n -' r))))) + ((((- 1) * T) to_power (- (n + r))) * (T to_power (n -' r)))) - ((((- 1) * T) to_power (- (n + r))) * (((- 1) to_power (- (n -' r))) * (T to_power (- (n -' r))))))
by Th4
.=
((1 / (sqrt 5)) ^2) * ((((((((T to_power n) ^2) - ((2 * (T to_power n)) * (((- 1) to_power (- n)) * (T to_power (- n))))) + ((((- 1) to_power (- n)) * (T to_power (- n))) ^2)) - ((T to_power (n + r)) * (T to_power (n -' r)))) + ((T to_power (n + r)) * (((- 1) * T) to_power (- (n -' r))))) + ((((- 1) * T) to_power (- (n + r))) * (T to_power (n -' r)))) - ((((- 1) * T) to_power (- (n + r))) * (((- 1) to_power (- (n -' r))) * (T to_power (- (n -' r))))))
by Th4
.=
((1 / (sqrt 5)) ^2) * ((((((((T to_power n) ^2) - ((2 * (T to_power n)) * (((- 1) to_power (- n)) * (T to_power (- n))))) + ((((- 1) to_power (- n)) * (T to_power (- n))) ^2)) - ((T to_power (n + r)) * (T to_power (n -' r)))) + ((T to_power (n + r)) * (((- 1) to_power (- (n -' r))) * (T to_power (- (n -' r)))))) + ((((- 1) * T) to_power (- (n + r))) * (T to_power (n -' r)))) - ((((- 1) * T) to_power (- (n + r))) * (((- 1) to_power (- (n -' r))) * (T to_power (- (n -' r))))))
by Th4
.=
((1 / (sqrt 5)) ^2) * ((((((((T to_power n) ^2) - ((2 * (T to_power n)) * (((- 1) to_power (- n)) * (T to_power (- n))))) + ((((- 1) to_power (- n)) * (T to_power (- n))) ^2)) - ((T to_power (n + r)) * (T to_power (n -' r)))) + ((T to_power (n + r)) * (((- 1) to_power (- (n -' r))) * (T to_power (- (n -' r)))))) + ((((- 1) to_power (- (n + r))) * (T to_power (- (n + r)))) * (T to_power (n -' r)))) - ((((- 1) * T) to_power (- (n + r))) * (((- 1) to_power (- (n -' r))) * (T to_power (- (n -' r))))))
by Th4
.=
((1 / (sqrt 5)) ^2) * ((((((((T to_power n) ^2) - ((2 * (T to_power n)) * (((- 1) to_power (- n)) * (T to_power (- n))))) + ((((- 1) to_power (- n)) * (T to_power (- n))) ^2)) - ((T to_power (n + r)) * (T to_power (n -' r)))) + ((T to_power (n + r)) * (((- 1) to_power (- (n -' r))) * (T to_power (- (n -' r)))))) + ((((- 1) to_power (- (n + r))) * (T to_power (- (n + r)))) * (T to_power (n -' r)))) - ((((- 1) to_power (- (n + r))) * (T to_power (- (n + r)))) * (((- 1) to_power (- (n -' r))) * (T to_power (- (n -' r))))))
by Th4
.=
((1 / (sqrt 5)) ^2) * ((((((((T to_power n) ^2) - ((2 * ((T to_power n) * (T to_power (- n)))) * ((- 1) to_power (- n)))) + ((((- 1) to_power (- n)) ^2) * ((T to_power (- n)) ^2))) - ((T to_power (n + r)) * (T to_power (n -' r)))) + (((T to_power (n + r)) * ((- 1) to_power (- (n -' r)))) * (T to_power (- (n -' r))))) + ((((- 1) to_power (- (n + r))) * (T to_power (- (n + r)))) * (T to_power (n -' r)))) - (((((- 1) to_power (- (n + r))) * (T to_power (- (n + r)))) * ((- 1) to_power (- (n -' r)))) * (T to_power (- (n -' r)))))
.=
((1 / (sqrt 5)) ^2) * ((((((((T to_power n) ^2) - ((2 * 1) * ((- 1) to_power (- n)))) + ((((- 1) to_power (- n)) ^2) * ((T to_power (- n)) ^2))) - ((T to_power (n + r)) * (T to_power (n -' r)))) + (((T to_power (n + r)) * ((- 1) to_power (- (n -' r)))) * (T to_power (- (n -' r))))) + ((((- 1) to_power (- (n + r))) * (T to_power (- (n + r)))) * (T to_power (n -' r)))) - (((((- 1) to_power (- (n + r))) * (T to_power (- (n + r)))) * ((- 1) to_power (- (n -' r)))) * (T to_power (- (n -' r)))))
by Th10
.=
((1 / (sqrt 5)) ^2) * ((((((((T to_power n) ^2) - (2 * ((- 1) to_power (- n)))) + (1 * ((T to_power (- n)) ^2))) - ((T to_power (n + r)) * (T to_power (n -' r)))) + (((T to_power (n + r)) * (T to_power (- (n -' r)))) * ((- 1) to_power (- (n -' r))))) + ((((- 1) to_power (- (n + r))) * (T to_power (- (n + r)))) * (T to_power (n -' r)))) - (((((- 1) to_power (- (n + r))) * ((- 1) to_power (- (n -' r)))) * (T to_power (- (n + r)))) * (T to_power (- (n -' r)))))
by Th7
.=
((1 / (sqrt 5)) ^2) * ((((((((T to_power n) ^2) - (2 * ((- 1) to_power (- n)))) + ((T to_power (- n)) ^2)) - ((T to_power (n + r)) * (T to_power (n -' r)))) + (((T to_power (n + r)) * (1 / (T to_power (n -' r)))) * ((- 1) to_power (- (n -' r))))) + ((((- 1) to_power (- (n + r))) * (T to_power (- (n + r)))) * (T to_power (n -' r)))) - (((((- 1) to_power (- (n + r))) * ((- 1) to_power (- (n -' r)))) * (T to_power (- (n + r)))) * (T to_power (- (n -' r)))))
by Th33, POWER:28
.=
((1 / (sqrt 5)) ^2) * ((((((((T to_power n) ^2) - (2 * ((- 1) to_power (- n)))) + ((T to_power (- n)) ^2)) - ((T to_power (n + r)) * (T to_power (n -' r)))) + (((T to_power (n + r)) / (T to_power (n -' r))) * ((- 1) to_power (- (n -' r))))) + ((((- 1) to_power (- (n + r))) * (T to_power (- (n + r)))) * (T to_power (n -' r)))) - (((((- 1) to_power (- (n + r))) * ((- 1) to_power (- (n -' r)))) * (T to_power (- (n + r)))) * (T to_power (- (n -' r)))))
by XCMPLX_1:99
.=
((1 / (sqrt 5)) ^2) * ((((((((T to_power n) ^2) - (2 * ((- 1) to_power (- n)))) + ((T to_power (- n)) ^2)) - ((T to_power (n + r)) * (T to_power (n -' r)))) + ((T to_power ((n + r) - (n -' r))) * ((- 1) to_power (- (n -' r))))) + ((((- 1) to_power (- (n + r))) * (T to_power (- (n + r)))) * (T to_power (n -' r)))) - (((((- 1) to_power (- (n + r))) * ((- 1) to_power (- (n -' r)))) * (T to_power (- (n + r)))) * (T to_power (- (n -' r)))))
by Th33, POWER:29
.=
((1 / (sqrt 5)) ^2) * ((((((((T to_power n) ^2) - (2 * ((- 1) to_power (- n)))) + ((T to_power (- n)) ^2)) - (T to_power ((n + r) + (n -' r)))) + ((T to_power ((n + r) - (n -' r))) * ((- 1) to_power (- (n -' r))))) + (((- 1) to_power (- (n + r))) * ((T to_power (n -' r)) * (T to_power (- (n + r)))))) - ((((- 1) to_power (- (n + r))) * ((- 1) to_power (- (n -' r)))) * ((T to_power (- (n + r))) * (T to_power (- (n -' r))))))
by Th33, POWER:27
.=
((1 / (sqrt 5)) ^2) * ((((((((T to_power n) ^2) - (2 * ((- 1) to_power (- n)))) + ((T to_power (- n)) ^2)) - (T to_power ((n + r) + (n -' r)))) + ((T to_power ((n + r) - (n -' r))) * ((- 1) to_power (- (n -' r))))) + (((- 1) to_power (- (n + r))) * ((T to_power (n -' r)) * (1 / (T to_power (n + r)))))) - ((((- 1) to_power (- (n + r))) * ((- 1) to_power (- (n -' r)))) * ((T to_power (- (n + r))) * (T to_power (- (n -' r))))))
by Th33, POWER:28
.=
((1 / (sqrt 5)) ^2) * ((((((((T to_power n) ^2) - (2 * ((- 1) to_power (- n)))) + ((T to_power (- n)) ^2)) - (T to_power ((n + r) + (n -' r)))) + ((T to_power ((n + r) - (n -' r))) * ((- 1) to_power (- (n -' r))))) + (((- 1) to_power (- (n + r))) * ((T to_power (n -' r)) / (T to_power (n + r))))) - ((((- 1) to_power (- (n + r))) * ((- 1) to_power (- (n -' r)))) * ((T to_power (- (n + r))) * (T to_power (- (n -' r))))))
by XCMPLX_1:99
.=
((1 / (sqrt 5)) ^2) * ((((((((T to_power n) ^2) - (2 * ((- 1) to_power (- n)))) + ((T to_power (- n)) ^2)) - (T to_power ((n + r) + (n -' r)))) + ((T to_power ((n + r) - (n -' r))) * ((- 1) to_power (- (n -' r))))) + (((- 1) to_power (- (n + r))) * (T to_power ((n -' r) - (n + r))))) - ((((- 1) to_power (- (n + r))) * ((- 1) to_power (- (n -' r)))) * ((T to_power (- (n + r))) * (T to_power (- (n -' r))))))
by Th33, POWER:29
.=
((1 / (sqrt 5)) ^2) * ((((((((T to_power n) ^2) - (2 * ((- 1) to_power (- n)))) + ((T to_power (- n)) ^2)) - (T to_power ((n + r) + (n -' r)))) + ((T to_power ((n + r) - (n -' r))) * ((- 1) to_power (- (n -' r))))) + (((- 1) to_power (- (n + r))) * (T to_power ((n -' r) - (n + r))))) - (((- 1) to_power ((- (n + r)) - (n -' r))) * ((T to_power (- (n + r))) * (T to_power (- (n -' r))))))
by Th8
.=
((1 / (sqrt 5)) ^2) * ((((((((T to_power n) ^2) - (2 * ((- 1) to_power (- n)))) + ((T to_power (- n)) ^2)) - (T to_power (2 * n))) + ((T to_power (2 * r)) * ((- 1) to_power (- (n -' r))))) + (((- 1) to_power (- (n + r))) * (T to_power (- (2 * r))))) - (((- 1) to_power (- (2 * n))) * (T to_power (- (2 * n)))))
by A2, Th8
.=
((1 / (sqrt 5)) ^2) * ((((((((T to_power n) ^2) - (2 * ((- 1) to_power (- n)))) + ((T to_power (- n)) ^2)) - (T to_power (2 * n))) + ((T to_power (2 * r)) * ((- 1) to_power (- (n -' r))))) + (((- 1) to_power (- (n + r))) * (T to_power (- (2 * r))))) - (1 * (T to_power (- (2 * n)))))
by Th9
.=
((1 / (sqrt 5)) ^2) * ((((((((T to_power n) to_power 2) - (2 * ((- 1) to_power (- n)))) + ((T to_power (- n)) ^2)) - (T to_power (2 * n))) + ((T to_power (2 * r)) * ((- 1) to_power (- (n -' r))))) + (((- 1) to_power (- (n + r))) * (T to_power (- (2 * r))))) - (1 * (T to_power (- (2 * n)))))
by POWER:46
.=
((1 / (sqrt 5)) ^2) * (((((((T to_power (2 * n)) - (2 * ((- 1) to_power (- n)))) + ((T to_power (- n)) ^2)) - (T to_power (2 * n))) + ((T to_power (2 * r)) * ((- 1) to_power (- (n -' r))))) + (((- 1) to_power (- (n + r))) * (T to_power (- (2 * r))))) - (T to_power (- (2 * n))))
by Th33, POWER:33
.=
((1 / (sqrt 5)) ^2) * (((((((T to_power (2 * n)) - (2 * ((- 1) to_power n))) + ((T to_power (- n)) ^2)) - (T to_power (2 * n))) + ((T to_power (2 * r)) * ((- 1) to_power (- (n -' r))))) + (((- 1) to_power (- (n + r))) * (T to_power (- (2 * r))))) - (T to_power (- (2 * n))))
by Th11
.=
((1 / (sqrt 5)) ^2) * (((((((T to_power (2 * n)) - (T to_power (2 * n))) - (2 * ((- 1) to_power n))) + ((T to_power (- n)) ^2)) + ((T to_power (2 * r)) * ((- 1) to_power (n -' r)))) + (((- 1) to_power (- (n + r))) * (T to_power (- (2 * r))))) - (T to_power (- (2 * n))))
by Th11
.=
((1 / (sqrt 5)) ^2) * (((((- (2 * ((- 1) to_power n))) + ((T to_power (- n)) ^2)) + ((T to_power (2 * r)) * ((- 1) to_power (n -' r)))) + (((- 1) to_power (n + r)) * (T to_power (- (2 * r))))) - (T to_power (2 * (- n))))
by Th11
.=
((1 / (sqrt 5)) ^2) * (((((- (2 * ((- 1) to_power n))) + ((T to_power (- n)) ^2)) + ((T to_power (2 * r)) * ((- 1) to_power (n -' r)))) + (((- 1) to_power (n + r)) * (T to_power (- (2 * r))))) - ((T to_power (- n)) to_power 2))
by Th33, POWER:33
.=
((1 / (sqrt 5)) ^2) * (((((- (2 * ((- 1) to_power n))) + ((T to_power (2 * r)) * ((- 1) to_power (n -' r)))) + (((- 1) to_power (n + r)) * (T to_power (- (2 * r))))) + ((T to_power (- n)) ^2)) - ((T to_power (- n)) ^2))
by POWER:46
.=
((1 / (sqrt 5)) ^2) * (((- (2 * ((- 1) to_power ((n -' r) + r)))) + (((- 1) to_power (n -' r)) * (T to_power (2 * r)))) + (((- 1) to_power ((2 * r) + (n -' r))) * (T to_power (- (2 * r)))))
by A3
.=
((1 / (sqrt 5)) ^2) * (((- (2 * (((- 1) to_power r) * ((- 1) to_power (n -' r))))) + (((- 1) to_power (n -' r)) * (T to_power (2 * r)))) + (((- 1) to_power ((2 * r) + (n -' r))) * (T to_power (- (2 * r)))))
by Th5
.=
((1 / (sqrt 5)) ^2) * (((- (2 * (((- 1) to_power r) * ((- 1) to_power (n -' r))))) + (((- 1) to_power (n -' r)) * (T to_power (2 * r)))) + ((((- 1) to_power (2 * r)) * ((- 1) to_power (n -' r))) * (T to_power (- (2 * r)))))
by Th5
.=
(((1 / (sqrt 5)) ^2) * (((- (2 * ((- 1) to_power r))) + (T to_power (2 * r))) + ((T to_power (- (2 * r))) * ((- 1) to_power (2 * r))))) * ((- 1) to_power (n -' r))
.=
(((1 / (sqrt 5)) ^2) * (((- (2 * ((- 1) to_power r))) + (T to_power (2 * r))) + ((T to_power (- (2 * r))) * 1))) * ((- 1) to_power (n -' r))
by Th3
.=
(((1 / (sqrt 5)) ^2) * (((T to_power (2 * r)) - (2 * ((- 1) to_power r))) + (T to_power (2 * (- r))))) * ((- 1) to_power (n -' r))
.=
(((1 / (sqrt 5)) ^2) * ((((T to_power r) to_power 2) - (2 * ((- 1) to_power r))) + (T to_power ((- r) * 2)))) * ((- 1) to_power (n -' r))
by Th33, POWER:33
.=
(((1 / (sqrt 5)) ^2) * ((((T to_power r) ^2) - (2 * ((- 1) to_power r))) + (T to_power ((- r) * 2)))) * ((- 1) to_power (n -' r))
by POWER:46
.=
((- 1) to_power (n -' r)) * (((1 / (sqrt 5)) ^2) * ((((T to_power r) ^2) - (2 * ((- 1) to_power r))) + ((T to_power (- r)) to_power 2)))
by Th33, POWER:33
.=
((- 1) to_power (n -' r)) * (((1 / (sqrt 5)) ^2) * ((((T to_power r) ^2) - (2 * ((- 1) to_power r))) + ((T to_power (- r)) ^2)))
by POWER:46
.=
((- 1) to_power (n -' r)) * (((1 / (sqrt 5)) ^2) * (((tau to_power r) - (tau_bar to_power r)) ^2))
by Th37
.=
((- 1) to_power (n -' r)) * ((((tau to_power r) - (tau_bar to_power r)) * (1 / (sqrt 5))) ^2)
.=
((- 1) to_power (n -' r)) * ((((tau to_power r) - (tau_bar to_power r)) / (sqrt 5)) ^2)
by XCMPLX_1:99
.=
((- 1) |^ (n -' r)) * ((((T to_power r) - (tau_bar to_power r)) / (sqrt 5)) ^2)
by POWER:41
.=
((- 1) |^ (n -' r)) * ((Fib r) ^2)
by FIB_NUM:7
;
hence
((Fib n) ^2) - ((Fib (n + r)) * (Fib (n -' r))) = ((- 1) |^ (n -' r)) * ((Fib r) ^2)
; verum