let n be Nat; :: thesis: (|.tau_bar.| to_power n) * (1 / (sqrt 5)) < 1 / 2
A1: 2 < sqrt 5 by SQUARE_1:20, SQUARE_1:27;
then A2: 2 / 2 < (sqrt 5) / 2 by XREAL_1:74;
set b = tau_bar ;
A3: sqrt 5 <> 0 by SQUARE_1:17, SQUARE_1:27;
A4: sqrt 5 > 0 by SQUARE_1:25;
per cases ( n <> 0 or n = 0 ) ;
suppose A5: n <> 0 ; :: thesis: (|.tau_bar.| to_power n) * (1 / (sqrt 5)) < 1 / 2
( |.tau_bar.| < 1 & |.tau_bar.| > 0 ) by Th5;
then |.tau_bar.| to_power n < 1 to_power n by A5, POWER:37;
then |.tau_bar.| to_power n < 1 ;
then |.tau_bar.| to_power n < (sqrt 5) / 2 by A2, XXREAL_0:2;
then (|.tau_bar.| to_power n) / ((sqrt 5) / 1) < ((sqrt 5) / 2) / ((sqrt 5) / 1) by A4, XREAL_1:74;
then (|.tau_bar.| to_power n) / (sqrt 5) < (1 * (sqrt 5)) / (2 * (sqrt 5)) by XCMPLX_1:84;
then (|.tau_bar.| to_power n) * (1 / (sqrt 5)) < (1 * (sqrt 5)) / (2 * (sqrt 5)) by XCMPLX_1:99;
hence (|.tau_bar.| to_power n) * (1 / (sqrt 5)) < 1 / 2 by A3, XCMPLX_1:91; :: thesis: verum
end;
suppose n = 0 ; :: thesis: (|.tau_bar.| to_power n) * (1 / (sqrt 5)) < 1 / 2
then |.tau_bar.| to_power n = 1 by POWER:24;
hence (|.tau_bar.| to_power n) * (1 / (sqrt 5)) < 1 / 2 by A1, XREAL_1:76; :: thesis: verum
end;
end;