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