let n be non zero Nat; :: thesis: tau to_power n > tau_bar to_power n
set tb = tau_bar ;
per cases ( n is even or n is odd ) ;
suppose A1: n is even ; :: thesis: tau to_power n > tau_bar to_power n
consider k being 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:9
.= (tau ^2) to_power k by POWER:46 ;
tau_bar to_power n = (tau_bar to_power 2) to_power k by A2, NEWTON:9
.= (tau_bar ^2) to_power k by POWER:46 ;
hence tau to_power n > tau_bar to_power n by A3, A4, Lm14, POWER:37; :: thesis: verum
end;
suppose n is odd ; :: thesis: tau to_power n > tau_bar to_power n
then consider k being Nat such that
A5: n = (2 * k) + 1 by ABIAN:9;
set kk = tau to_power (2 * k);
A6: (tau / tau_bar) to_power (2 * k) = ((tau / tau_bar) to_power 2) to_power k by NEWTON:9
.= ((tau / tau_bar) ^2) to_power k by POWER:46 ;
tau_bar to_power (2 * k) = (tau_bar to_power 2) to_power k by NEWTON:9
.= (tau_bar ^2) to_power k by POWER:46 ;
then A7: tau_bar to_power (2 * k) > 0 by POWER:34;
(tau / tau_bar) to_power (2 * k) > ((sqrt 5) - 3) / 2 by A6, Lm15, POWER:34;
then ((tau / tau_bar) to_power (2 * k)) * (((- 3) - (sqrt 5)) / 2) < (tau_bar / tau) * (((- 3) - (sqrt 5)) / 2) by Lm13, Lm4, XREAL_1:69;
then ((tau / tau_bar) to_power (2 * k)) * (tau / tau_bar) < 1 by Lm5, XCMPLX_1:112;
then ((tau to_power (2 * k)) / (tau_bar to_power (2 * k))) * (tau / tau_bar) < 1 by Th1;
then ((tau to_power (2 * k)) * (1 / (tau_bar to_power (2 * k)))) * (tau / tau_bar) < 1 by XCMPLX_1:99;
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 A7, XREAL_1:68;
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:99;
then ((tau to_power (2 * k)) * (tau / tau_bar)) * 1 < tau_bar to_power (2 * k) by A7, XCMPLX_1:60;
then ((tau to_power (2 * k)) * (tau * (1 / tau_bar))) * 1 < tau_bar to_power (2 * k) by XCMPLX_1:99;
then (((tau to_power (2 * k)) * (tau * (1 / tau_bar))) * 1) * tau_bar > (tau_bar to_power (2 * k)) * tau_bar by XREAL_1:69;
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:99;
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) ;
then (tau to_power (2 * k)) * tau > tau_bar to_power ((2 * k) + 1) by Th2;
then (tau to_power (2 * k)) * (tau to_power 1) > tau_bar to_power ((2 * k) + 1) ;
hence tau to_power n > tau_bar to_power n by A5, Th2; :: thesis: verum
end;
end;