let n be Element of NAT ; ( n > 0 implies ( log (2,(2 * n)) = 1 + (log (2,n)) & log (2,(2 * n)) = (log (2,n)) + 1 ) )
assume
n > 0
; ( 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
;
log (2,(2 * n)) = (log (2,n)) + 1
hence
log (2,(2 * n)) = (log (2,n)) + 1
; verum