let n be non empty natural number ; :: thesis: tau to_power n > tau_bar to_power n
set tb = tau_bar ;

per cases ( n is even or not n is even ) ;

suppose A1: n is even ; :: thesis: tau to_power n > tau_bar to_power n

n - 0 is Element of NAT by NAT_1:21;
then consider k being Element of NAT such that
A2: n = 2 * k by A1, ABIAN:def 2;
A3: k > 0 by A2;
A4: tau to_power n = (tau to_power 2) to_power k by A2, NEWTON:14
.= (tau ^2) to_power k by POWER:53 ;
tau_bar to_power n = (tau_bar to_power 2) to_power k by A2, NEWTON:14
.= (tau_bar ^2) to_power k by POWER:53 ;
hence tau to_power n > tau_bar to_power n by A3, A4, B0, POWER:42; :: thesis: verum

end;

suppose not n is even ; :: thesis: tau to_power n > tau_bar to_power n

then consider k being Element of NAT such that
A2: n = (2 * k) + 1 by ABIAN:9;
set kk = tau to_power (2 * k);
d1: (tau / tau_bar) to_power (2 * k) = ((tau / tau_bar) to_power 2) to_power k by NEWTON:14
.= ((tau / tau_bar) ^2) to_power k by POWER:53 ;
tau_bar to_power (2 * k) = (tau_bar to_power 2) to_power k by NEWTON:14
.= (tau_bar ^2) to_power k by POWER:53 ;
then D4: tau_bar to_power (2 * k) > 0 by POWER:39;
(tau / tau_bar) to_power (2 * k) > ((sqrt 5) - 3) / 2 by d1, D2, POWER:39;
then ((tau / tau_bar) to_power (2 * k)) * (((- 3) - (sqrt 5)) / 2) < (tau_bar / tau) * (((- 3) - (sqrt 5)) / 2) by d3, albet2, XREAL_1:71;
then ((tau / tau_bar) to_power (2 * k)) * (tau / tau_bar) < 1 by albet4, XCMPLX_1:113;
then ((tau to_power (2 * k)) / (tau_bar to_power (2 * k))) * (tau / tau_bar) < 1 by JakPower36;
then ((tau to_power (2 * k)) * (1 / (tau_bar to_power (2 * k)))) * (tau / tau_bar) < 1 by XCMPLX_1:100;
then (((tau to_power (2 * k)) * (1 / (tau_bar to_power (2 * k)))) * (tau / tau_bar)) * (tau_bar to_power (2 * k)) < 1 * (tau_bar to_power (2 * k)) by D4, XREAL_1:70;
then ((tau to_power (2 * k)) * (tau / tau_bar)) * ((tau_bar to_power (2 * k)) * (1 / (tau_bar to_power (2 * k)))) < 1 * (tau_bar to_power (2 * k)) ;
then ((tau to_power (2 * k)) * (tau / tau_bar)) * ((tau_bar to_power (2 * k)) / (tau_bar to_power (2 * k))) < 1 * (tau_bar to_power (2 * k)) by XCMPLX_1:100;
then ((tau to_power (2 * k)) * (tau / tau_bar)) * 1 < tau_bar to_power (2 * k) by D4, XCMPLX_1:60;
then ((tau to_power (2 * k)) * (tau * (1 / tau_bar))) * 1 < tau_bar to_power (2 * k) by XCMPLX_1:100;
then (((tau to_power (2 * k)) * (tau * (1 / tau_bar))) * 1) * tau_bar > (tau_bar to_power (2 * k)) * tau_bar by XREAL_1:71;
then ((tau to_power (2 * k)) * tau) * (((1 / tau_bar) * 1) * tau_bar) > (tau_bar to_power (2 * k)) * tau_bar ;
then ((tau to_power (2 * k)) * tau) * (tau_bar / tau_bar) > (tau_bar to_power (2 * k)) * tau_bar by XCMPLX_1:100;
then ((tau to_power (2 * k)) * tau) * 1 > (tau_bar to_power (2 * k)) * tau_bar by XCMPLX_1:60;
then (tau to_power (2 * k)) * tau > (tau_bar to_power (2 * k)) * (tau_bar to_power 1) by POWER:30;
then (tau to_power (2 * k)) * tau > tau_bar to_power ((2 * k) + 1) by JakPower32;
then (tau to_power (2 * k)) * (tau to_power 1) > tau_bar to_power ((2 * k) + 1) by POWER:30;
hence tau to_power n > tau_bar to_power n by A2, JakPower32; :: thesis: verum

end;

end;