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:59;
then log 2,nn9 >= 0 by A1, PRE_FF:12;
then [\(log 2,nn9)/] >= [\0 /] by PRE_FF:11;
then [\(log 2,nn9)/] >= 0 by INT_1:47;
then reconsider F = [\(log 2,nn9)/] as Element of NAT by INT_1:16;
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 by NAT_1:12;
hence (6 * ([\(log 2,nn9)/] + 1)) + 1 > 0 by NAT_1:13; :: thesis: verum