let nn, nn9 be Element of NAT ; ( nn = 2 * nn9 & nn9 > 0 implies 6 + ((6 * ([\(log (2,nn9))/] + 1)) + 1) = (6 * ([\(log (2,nn))/] + 1)) + 1 )
assume A1:
( nn = 2 * nn9 & nn9 > 0 )
; 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 * (1 + [\((log (2,nn9)) + 1)/])) + 1
by INT_1:28
.=
(6 * ([\(log (2,nn))/] + 1)) + 1
by A1, Lm4
; verum