let n be Element of NAT ; :: thesis: ( n > 0 implies ( log (2,(2 * n)) = 1 + (log (2,n)) & log (2,(2 * n)) = (log (2,n)) + 1 ) )
assume n > 0 ; :: thesis: ( log (2,(2 * n)) = 1 + (log (2,n)) & log (2,(2 * n)) = (log (2,n)) + 1 )
hence log (2,(2 * n)) = (log (2,2)) + (log (2,n)) by POWER:53
.= 1 + (log (2,n)) by POWER:52 ;
:: thesis: log (2,(2 * n)) = (log (2,n)) + 1
hence log (2,(2 * n)) = (log (2,n)) + 1 ; :: thesis: verum