let n be natural number ; :: 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:10;
then n + 1 >= 1 + 1 by NAT_1:13;
then C1: ( n + 1 = 2 or n >= 2 ) by NAT_1:8;

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

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

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

end;

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

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

proof

defpred S₁[ Nat] means (abs tau_bar ) to_power $1 < 1 / 2;
C1: (abs tau_bar ) to_power 2 = (- tau_bar ) to_power 2 by ABSVALUE:def 1
.= (- tau_bar ) ^2 by POWER:53
.= (((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 4
.= (3 - (sqrt 5)) / 2 ;
sqrt 5 > 2 by SQUARE_1:85, SQUARE_1:95;
then - (sqrt 5) < - 2 by XREAL_1:26;
then (- (sqrt 5)) + 3 < (- 2) + 3 by XREAL_1:10;
then B1: S₁[2] by C1, XREAL_1:76;
B2: 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 ((abs tau_bar ) to_power k) * (abs tau_bar ) < (1 / 2) * (abs tau_bar ) by XREAL_1:70;
then b3: ((abs tau_bar ) to_power k) * ((abs tau_bar ) to_power 1) < (1 / 2) * (abs tau_bar ) by POWER:30;
(1 / 2) * (abs tau_bar ) < (1 / 2) * 1 by hop3, XREAL_1:70;
then ((abs tau_bar ) to_power k) * ((abs tau_bar ) to_power 1) < 1 / 2 by b3, XXREAL_0:2;
hence S₁[k + 1] by JakPower32; :: thesis: verum

end;

bb4: for n being non trivial Nat holds S₁[n] from NAT_2:sch 2(B1, B2);
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
(abs tau_bar ) to_power n < 1 / 2 by bb4;
then ( abs (tau_bar to_power n) < 1 / 2 & tau_bar to_power n <= abs (tau_bar to_power n) ) by ABSVALUE:11, 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 B0; :: thesis: verum

end;

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

end;

end;