Theorem 2sqn0

Description: If the sum of two squares is prime, none of the original number is zero. (Contributed by Thierry Arnoux, 4-Feb-2020)

	Ref	Expression
Hypotheses	2sqcoprm.1	$$⊢\phi \to P\in \mathbb{P}$$
	2sqcoprm.2	$$⊢\phi \to A\in \mathbb{Z}$$
	2sqcoprm.3	$$⊢\phi \to B\in \mathbb{Z}$$
	2sqcoprm.4	$$⊢\phi \to A^2+B^2=P$$
Assertion	2sqn0	$$⊢\phi \to A\ne 0$$

Proof

Step	Hyp	Ref	Expression
1		2sqcoprm.1	$$⊢\phi \to P\in \mathbb{P}$$
2		2sqcoprm.2	$$⊢\phi \to A\in \mathbb{Z}$$
3		2sqcoprm.3	$$⊢\phi \to B\in \mathbb{Z}$$
4		2sqcoprm.4	$$⊢\phi \to A^2+B^2=P$$
5	4 1	eqeltrd	$$⊢\phi \to A^2+B^2\in \mathbb{P}$$
6	5	adantr	$$⊢\left(\phi \wedge A=0\right)\to A^2+B^2\in \mathbb{P}$$
7		sq0i	$$⊢A=0\to A^2=0$$
8	7	oveq1d	$$⊢A=0\to A^2+B^2=0+B^2$$
9	3	zcnd	$$⊢\phi \to B\in ℂ$$
10	9	sqcld	$$⊢\phi \to B^2\in ℂ$$
11	10	addid2d	$$⊢\phi \to 0+B^2=B^2$$
12	8 11	sylan9eqr	$$⊢\left(\phi \wedge A=0\right)\to A^2+B^2=B^2$$
13		sqnprm	$$⊢B\in \mathbb{Z}\to \neg B^2\in \mathbb{P}$$
14	3 13	syl	$$⊢\phi \to \neg B^2\in \mathbb{P}$$
15	14	adantr	$$⊢\left(\phi \wedge A=0\right)\to \neg B^2\in \mathbb{P}$$
16	12 15	eqneltrd	$$⊢\left(\phi \wedge A=0\right)\to \neg A^2+B^2\in \mathbb{P}$$
17	6 16	pm2.65da	$$⊢\phi \to \neg A=0$$
18	17	neqned	$$⊢\phi \to A\ne 0$$