let n be Nat; :: thesis: ( n > 0 implies [\(log (2,n))/] + 1 = [\(log (2,((2 * n) + 1)))/] )
assume A1: n > 0 ; :: thesis: [\(log (2,n))/] + 1 = [\(log (2,((2 * n) + 1)))/]
then [\(log (2,((2 * n) + 1)))/] = [\(log (2,(2 * n)))/] by Th13
.= [\((log (2,2)) + (log (2,n)))/] by A1, POWER:53
.= [\((log (2,n)) + 1)/] by POWER:52
.= [\(log (2,n))/] + 1 by INT_1:28 ;
hence [\(log (2,n))/] + 1 = [\(log (2,((2 * n) + 1)))/] ; :: thesis: verum