Solution (source code)

= Solution

We can use reduction instead of expanding a very large rational addition formula. Modulo $2$, both $P_1$ and $P_2$ reduce to $(0,0)$, which generates the three-element reduced group. The reduction <homomorphism> therefore gives
$$
\overline{P_1+5P_2}=6(0,0)=O.
$$
The <rational point> $P_2$ is not any of the three torsion points just found, so it has <infinite order>. In particular $R=P_1+5P_2\ne O$: otherwise multiplication by three would give $15P_2=O$.

If $R$ had integral coordinates, its affine integral representative would reduce to an affine point modulo $2$, not to the point at infinity. This contradicts its reduction to $O$. Thus
$$
\boxed{P_1+5P_2\text{ does not have integral coordinates}.}
$$
Indeed, it is not even integral at $2$. This is a <reduction certificate for a nonintegral elliptic point>, with the crucial nonidentity condition verified by the torsion calculation.