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 Th15
.= [\((log 2,2) + (log 2,n))/] by A1, POWER:61
.= [\((log 2,n) + 1)/] by POWER:60
.= [\(log 2,n)/] + 1 by INT_1:51 ;
hence [\(log 2,n)/] + 1 = [\(log 2,((2 * n) + 1))/] ; :: thesis: verum