A module over the integers spanned by a family has rank at most the number of members that are not torsion

Let $M$ be an abelian group, regarded as a module over $\mathbb{Z}$, spanned by a finite family $(a_i)$, and let $J$ be a finite set of indices such that every $a_i$ with $i \notin J$ is torsion, that is, some nonzero integer multiple of it vanishes. Then the rank of $M$, as a cardinal, is at most the cardinality of $J$.

The members outside $J$ contribute nothing: the submodule spanned by the members inside $J$ has torsion quotient, so that quotient has rank zero, and rank is additive across it because $\mathbb{Z}$ is a domain and so satisfies rank-nullity. No hypothesis is placed on the members inside $J$ -- they need not be independent, nor of infinite order -- so the statement is an inequality and not an equality.

Three further points. The rank is the cardinal-valued one, so the inequality has content even when $M$ is not of finite rank; the natural-number valued finrank form follows in one step, and is strictly weaker, since truncating an infinite rank to zero would make it say nothing exactly where it matters. The set $J$ carries no minimality, no non-vanishing and no non-torsion requirement: $J$ empty is admissible, and then the hypotheses force the rank to be $0$; $J$ everything is admissible too, and then the torsion hypothesis is empty. And no finiteness is imposed on the index type -- the family may be infinite, so long as the members outside $J$ are torsion.