let r be Nat; (((tau to_power r) ^2) - (2 * ((- 1) to_power r))) + ((tau to_power (- r)) ^2) = ((tau to_power r) - (tau_bar to_power r)) ^2
(- 1) / tau < 0
by Th33;
then
- (1 / tau) < 0
by XCMPLX_1:187;
then A1:
1 / tau > - 0
;
((tau to_power r) - (tau_bar to_power r)) ^2 =
(((tau to_power r) ^2) - ((2 * (tau to_power r)) * ((- (1 / tau)) to_power r))) + (((- (1 / tau)) to_power r) ^2)
by Th36
.=
(((tau to_power r) ^2) - ((2 * (tau to_power r)) * (((- 1) * (1 / tau)) #Z r))) + (((- (1 / tau)) to_power r) ^2)
by POWER:def 2
.=
(((tau to_power r) ^2) - ((2 * (tau to_power r)) * (((- 1) #Z r) * ((1 / tau) #Z r)))) + (((- (1 / tau)) to_power r) ^2)
by PREPOWER:40
.=
(((tau to_power r) ^2) - ((2 * (tau to_power r)) * (((1 / tau) |^ r) * ((- 1) #Z r)))) + (((- (1 / tau)) to_power r) ^2)
by PREPOWER:36
.=
(((tau to_power r) ^2) - ((2 * (tau |^ r)) * (((1 / tau) |^ r) * ((- 1) #Z r)))) + (((- (1 / tau)) to_power r) ^2)
by POWER:41
.=
(((tau to_power r) ^2) - ((2 * ((tau |^ r) * ((1 / tau) |^ r))) * ((- 1) #Z r))) + (((- (1 / tau)) to_power r) ^2)
.=
(((tau to_power r) ^2) - ((2 * ((tau * (1 / tau)) |^ r)) * ((- 1) #Z r))) + (((- (1 / tau)) to_power r) ^2)
by NEWTON:7
.=
(((tau to_power r) ^2) - ((2 * (1 |^ r)) * ((- 1) #Z r))) + (((- (1 / tau)) to_power r) ^2)
by Th33, XCMPLX_1:106
.=
(((tau to_power r) ^2) - ((2 * 1) * ((- 1) #Z r))) + (((- (1 / tau)) to_power r) ^2)
.=
(((tau to_power r) ^2) - (2 * ((- 1) to_power r))) + (((- (1 / tau)) to_power r) ^2)
by POWER:def 2
.=
(((tau to_power r) ^2) - (2 * ((- 1) to_power r))) + (((- (1 / tau)) #Z r) ^2)
by POWER:def 2
.=
(((tau to_power r) ^2) - (2 * ((- 1) to_power r))) + (((- (1 / tau)) * (- (1 / tau))) #Z r)
by PREPOWER:40
.=
(((tau to_power r) ^2) - (2 * ((- 1) to_power r))) + (((- (1 / tau)) ^2) |^ r)
by PREPOWER:36
.=
(((tau to_power r) ^2) - (2 * ((- 1) to_power r))) + (((1 / tau) ^2) to_power r)
by POWER:41
.=
(((tau to_power r) ^2) - (2 * ((- 1) to_power r))) + (((1 / tau) to_power r) ^2)
by A1, POWER:30
.=
(((tau to_power r) ^2) - (2 * ((- 1) to_power r))) + ((tau to_power (- r)) ^2)
by Th33, POWER:32
;
hence
(((tau to_power r) ^2) - (2 * ((- 1) to_power r))) + ((tau to_power (- r)) ^2) = ((tau to_power r) - (tau_bar to_power r)) ^2
; verum