let nn, nn9 be Element of NAT ; :: thesis: ( nn = (2 * nn9) + 1 & nn9 > 0 implies 6 + ((6 * ([\(log (2,nn9))/] + 1)) + 1) = (6 * ([\(log (2,nn))/] + 1)) + 1 )
assume A1: ( nn = (2 * nn9) + 1 & nn9 > 0 ) ; :: thesis: 6 + ((6 * ([\(log (2,nn9))/] + 1)) + 1) = (6 * ([\(log (2,nn))/] + 1)) + 1
set F = [\(log (2,nn9))/];
thus 6 + ((6 * ([\(log (2,nn9))/] + 1)) + 1) = (6 * (1 + ([\(log (2,nn9))/] + 1))) + 1
.= (6 * ([\(log (2,nn))/] + 1)) + 1 by A1, PRE_FF:14 ; :: thesis: verum