Check whether loop invariants are correct?

Question

I'm trying to prove some code is correct, using Hoare logic. How do I check whether my loop invariants are correct?

I'm asked to prove (using Hoare Logic) that the following program is valid:

x=1; 
i=N;
while (i!=0){ 
    i--;
    x*=A;
}

with the pre-condition that N>=0 and post-condition that x=A^N.

This is my attempt:

{ N>=0 }
x=1; 
i=N;
{i >= 0}
while (i!=0){
    {i>=0}
    {x = product(i in (0:N-i); A)}    (loop invariant)
    i--;
    x*=A;
}
{x = A^N}

The curly brackets represent invariants that are supposed to hold at that point in the code. The 2 loop invariants seem to hold for every instance of the loop.

Is my attempt correct? Are my loop invariants sufficient? Do I have too many?

I know that {i>=0} is given by the definition of the loop. Should I remove that loop invariant then, since it is the case by default?

EDIT: My new attempt

{N>=0}
x=1;
{x = A^(N-N)=A^0=1} 
i=N;
{x = A^(N-i)}
while (i!=0){
    {i>=0} 
    i--;
    {x = product(i in (0:N-i-1);A)} 
    x*=A;
    {x = product(i in (0:N-i);A)}
}
{x=A^N}