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	⊢ ( 𝜑 → 𝑃 ∈ ℙ )
	2sqcoprm.2	⊢ ( 𝜑 → 𝐴 ∈ ℤ )
	2sqcoprm.3	⊢ ( 𝜑 → 𝐵 ∈ ℤ )
	2sqcoprm.4	⊢ ( 𝜑 → ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = 𝑃 )
Assertion	2sqn0	⊢ ( 𝜑 → 𝐴 ≠ 0 )

Proof

Step	Hyp	Ref	Expression
1		2sqcoprm.1	⊢ ( 𝜑 → 𝑃 ∈ ℙ )
2		2sqcoprm.2	⊢ ( 𝜑 → 𝐴 ∈ ℤ )
3		2sqcoprm.3	⊢ ( 𝜑 → 𝐵 ∈ ℤ )
4		2sqcoprm.4	⊢ ( 𝜑 → ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = 𝑃 )
5	4 1	eqeltrd	⊢ ( 𝜑 → ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) ∈ ℙ )
6	5	adantr	⊢ ( ( 𝜑 ∧ 𝐴 = 0 ) → ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) ∈ ℙ )
7		sq0i	⊢ ( 𝐴 = 0 → ( 𝐴 ↑ 2 ) = 0 )
8	7	oveq1d	⊢ ( 𝐴 = 0 → ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 0 + ( 𝐵 ↑ 2 ) ) )
9	3	zcnd	⊢ ( 𝜑 → 𝐵 ∈ ℂ )
10	9	sqcld	⊢ ( 𝜑 → ( 𝐵 ↑ 2 ) ∈ ℂ )
11	10	addlidd	⊢ ( 𝜑 → ( 0 + ( 𝐵 ↑ 2 ) ) = ( 𝐵 ↑ 2 ) )
12	8 11	sylan9eqr	⊢ ( ( 𝜑 ∧ 𝐴 = 0 ) → ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐵 ↑ 2 ) )
13		sqnprm	⊢ ( 𝐵 ∈ ℤ → ¬ ( 𝐵 ↑ 2 ) ∈ ℙ )
14	3 13	syl	⊢ ( 𝜑 → ¬ ( 𝐵 ↑ 2 ) ∈ ℙ )
15	14	adantr	⊢ ( ( 𝜑 ∧ 𝐴 = 0 ) → ¬ ( 𝐵 ↑ 2 ) ∈ ℙ )
16	12 15	eqneltrd	⊢ ( ( 𝜑 ∧ 𝐴 = 0 ) → ¬ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) ∈ ℙ )
17	6 16	pm2.65da	⊢ ( 𝜑 → ¬ 𝐴 = 0 )
18	17	neqned	⊢ ( 𝜑 → 𝐴 ≠ 0 )