let n be Nat; :: thesis: ( n <> 0 implies tau_bar to_power n < 1 / 2 )
assume n <> 0 ; :: thesis: tau_bar to_power n < 1 / 2
then n + 1 > 0 + 1 by XREAL_1:8;
then n + 1 >= 1 + 1 by NAT_1:13;
then A1: ( n + 1 = 2 or n >= 2 ) by NAT_1:8;

per cases ( n = 1 or n >= 2 ) by A1;

suppose n = 1 ; :: thesis: tau_bar to_power n < 1 / 2

hence tau_bar to_power n < 1 / 2 ; :: thesis: verum

end;

suppose n >= 2 ; :: thesis: tau_bar to_power n < 1 / 2

then ( n <> 0 & n <> 1 ) ;
then A2: n is non trivial Nat by NAT_2:def 1;
tau_bar to_power n < 1 / 2

proof

defpred S₁[ Nat] means |.tau_bar.| to_power $1 < 1 / 2;
A3: |.tau_bar.| to_power 2 = (- tau_bar) to_power 2 by ABSVALUE:def 1
.= (- tau_bar) ^2 by POWER:46
.= (((1 ^2) - ((2 * 1) * (sqrt 5))) + ((sqrt 5) ^2)) / 4 by FIB_NUM:def 2
.= ((1 - (2 * (sqrt 5))) + 5) / 4 by SQUARE_1:def 2
.= (3 - (sqrt 5)) / 2 ;
sqrt 5 > 2 by SQUARE_1:20, SQUARE_1:27;
then - (sqrt 5) < - 2 by XREAL_1:24;
then (- (sqrt 5)) + 3 < (- 2) + 3 by XREAL_1:8;
then A4: S₁[2] by A3, XREAL_1:74;
A5: for k being non trivial Nat st S₁[k] holds
S₁[k + 1]

proof

let k be non trivial Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume S₁[k] ; :: thesis: S₁[k + 1]
then (|.tau_bar.| to_power k) * |.tau_bar.| < (1 / 2) * |.tau_bar.| by XREAL_1:68;
then A6: (|.tau_bar.| to_power k) * (|.tau_bar.| to_power 1) < (1 / 2) * |.tau_bar.| ;
(1 / 2) * |.tau_bar.| < (1 / 2) * 1 by Th5, XREAL_1:68;
then (|.tau_bar.| to_power k) * (|.tau_bar.| to_power 1) < 1 / 2 by A6, XXREAL_0:2;
hence S₁[k + 1] by Th2; :: thesis: verum

end;

A7: for n being non trivial Nat holds S₁[n] from NAT_2:sch 2(A4, A5);
for n being non trivial Nat holds tau_bar to_power n < 1 / 2

proof

let n be non trivial Nat; :: thesis: tau_bar to_power n < 1 / 2
|.tau_bar.| to_power n < 1 / 2 by A7;
then ( |.(tau_bar to_power n).| < 1 / 2 & tau_bar to_power n <= |.(tau_bar to_power n).| ) by ABSVALUE:4, SERIES_1:2;
hence tau_bar to_power n < 1 / 2 by XXREAL_0:2; :: thesis: verum

end;

hence tau_bar to_power n < 1 / 2 by A2; :: thesis: verum

end;

hence tau_bar to_power n < 1 / 2 ; :: thesis: verum

end;

end;