let nn' be Element of NAT ; :: thesis: ( nn' > 0 implies ( [\(log 2,nn')/] is Element of NAT & (6 * ([\(log 2,nn')/] + 1)) + 1 > 0 ) )
assume nn' > 0 ; :: thesis: ( [\(log 2,nn')/] is Element of NAT & (6 * ([\(log 2,nn')/] + 1)) + 1 > 0 )
then A1: nn' >= 0 + 1 by NAT_1:13;
log 2,1 = 0 by POWER:59;
then log 2,nn' >= 0 by A1, PRE_FF:12;
then [\(log 2,nn')/] >= [\0 /] by PRE_FF:11;
then [\(log 2,nn')/] >= 0 by INT_1:47;
then reconsider F = [\(log 2,nn')/] as Element of NAT by INT_1:16;
F is Element of NAT ;
hence [\(log 2,nn')/] is Element of NAT ; :: thesis: (6 * ([\(log 2,nn')/] + 1)) + 1 > 0
(6 * F) + (6 * 1) >= 0 by NAT_1:12;
hence (6 * ([\(log 2,nn')/] + 1)) + 1 > 0 by NAT_1:13; :: thesis: verum