let nn9 be Element of NAT ; :: thesis: ( nn9 > 0 implies ( [\(log (2,nn9))/] is Element of NAT & (6 * ([\(log (2,nn9))/] + 1)) + 1 > 0 ) )
assume nn9 > 0 ; :: thesis: ( [\(log (2,nn9))/] is Element of NAT & (6 * ([\(log (2,nn9))/] + 1)) + 1 > 0 )
then A1: nn9 >= 0 + 1 by NAT_1:13;
log (2,1) = 0 by POWER:51;
then log (2,nn9) >= 0 by A1, PRE_FF:10;
then [\(log (2,nn9))/] >= [\0/] by PRE_FF:9;
then [\(log (2,nn9))/] >= 0 by INT_1:25;
then reconsider F = [\(log (2,nn9))/] as Element of NAT by INT_1:3;
F is Element of NAT ;
hence [\(log (2,nn9))/] is Element of NAT ; :: thesis: (6 * ([\(log (2,nn9))/] + 1)) + 1 > 0
(6 * F) + (6 * 1) >= 0 ;
hence (6 * ([\(log (2,nn9))/] + 1)) + 1 > 0 ; :: thesis: verum