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 Th35, XREAL_1:143;
then
- (1 / tau ) < 0
by XCMPLX_1:188;
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 Th38
.=
(((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:50
.=
(((tau to_power r) ^2 ) - ((2 * (tau to_power r)) * (((1 / tau ) |^ r) * ((- 1) #Z r)))) + (((- (1 / tau )) to_power r) ^2 )
by PREPOWER:46
.=
(((tau to_power r) ^2 ) - ((2 * (tau |^ r)) * (((1 / tau ) |^ r) * ((- 1) #Z r)))) + (((- (1 / tau )) to_power r) ^2 )
by POWER:46
.=
(((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:12
.=
(((tau to_power r) ^2 ) - ((2 * (1 |^ r)) * ((- 1) #Z r))) + (((- (1 / tau )) to_power r) ^2 )
by Th35, XCMPLX_1:107
.=
(((tau to_power r) ^2 ) - ((2 * 1) * ((- 1) #Z r))) + (((- (1 / tau )) to_power r) ^2 )
by NEWTON:15
.=
(((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:50
.=
(((tau to_power r) ^2 ) - (2 * ((- 1) to_power r))) + (((- (1 / tau )) ^2 ) |^ r)
by PREPOWER:46
.=
(((tau to_power r) ^2 ) - (2 * ((- 1) to_power r))) + (((1 / tau ) ^2 ) to_power r)
by POWER:46
.=
(((tau to_power r) ^2 ) - (2 * ((- 1) to_power r))) + (((1 / tau ) to_power r) ^2 )
by A1, POWER:35
.=
(((tau to_power r) ^2 ) - (2 * ((- 1) to_power r))) + ((tau to_power (- r)) ^2 )
by Th35, POWER:37
;
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