thus ( x = 0 implies ex y being non zero Nat st y = 1 ) ; :: thesis: ( not x = 0 implies ex b₁ being non zero Nat ex n being Nat st
( 2 to_power n <= x & x < 2 to_power (n + 1) & b₁ = n + 1 ) )
thus ( not x = 0 implies ex y being non zero Nat ex n being Nat st
( 2 to_power n <= x & x < 2 to_power (n + 1) & y = n + 1 ) ) :: thesis: verum

proof

assume x <> 0 ; :: thesis: ex y being non zero Nat ex n being Nat st
( 2 to_power n <= x & x < 2 to_power (n + 1) & y = n + 1 )
then consider n being Nat such that
A1: ( 2 to_power n <= x & x < 2 to_power (n + 1) ) by LM001;
take y = n + 1; :: thesis: ex n being Nat st
( 2 to_power n <= x & x < 2 to_power (n + 1) & y = n + 1 )
thus ex n being Nat st
( 2 to_power n <= x & x < 2 to_power (n + 1) & y = n + 1 ) by A1; :: thesis: verum

end;