Lemma 1 ([The three ranks]). There is an exact sequence 0⟶A()⊗_2/_2 ⟶_ 2^∞ (A/) ⟶(A/)[2^∞]⟶0. Consequently s_2(A)=r(A)+_ _2 (A/)[2^∞]. If a(A)∈0,1 , then r(A)=a(A) and the whole group (A/) is finite. In that case s_2(A)=a(A) .

The Kummer sequences for multiplication by 2^n , with the local Kummer conditions imposed, give 0⟶A()/2^n A() ⟶_ 2^n (A/) ⟶(A/)[2^n]⟶0. Their direct limit is the displayed sequence. Taking _2 -coranks proves the identity. The analytic-rank-zero and analytic-rank-one assertions are the Gross--Zagier--Kolyvagin theorem ; see also the precise unrestricted forward statement in .