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	|- ( ph -> P e. Prime )
	2sqcoprm.2	|- ( ph -> A e. ZZ )
	2sqcoprm.3	|- ( ph -> B e. ZZ )
	2sqcoprm.4	|- ( ph -> ( ( A ^ 2 ) + ( B ^ 2 ) ) = P )
Assertion	2sqn0	|- ( ph -> A =/= 0 )

Proof

Step	Hyp	Ref	Expression
1		2sqcoprm.1	|- ( ph -> P e. Prime )
2		2sqcoprm.2	|- ( ph -> A e. ZZ )
3		2sqcoprm.3	|- ( ph -> B e. ZZ )
4		2sqcoprm.4	|- ( ph -> ( ( A ^ 2 ) + ( B ^ 2 ) ) = P )
5	4 1	eqeltrd	|- ( ph -> ( ( A ^ 2 ) + ( B ^ 2 ) ) e. Prime )
6	5	adantr	|- ( ( ph /\ A = 0 ) -> ( ( A ^ 2 ) + ( B ^ 2 ) ) e. Prime )
7		sq0i	|- ( A = 0 -> ( A ^ 2 ) = 0 )
8	7	oveq1d	|- ( A = 0 -> ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( 0 + ( B ^ 2 ) ) )
9	3	zcnd	|- ( ph -> B e. CC )
10	9	sqcld	|- ( ph -> ( B ^ 2 ) e. CC )
11	10	addlidd	|- ( ph -> ( 0 + ( B ^ 2 ) ) = ( B ^ 2 ) )
12	8 11	sylan9eqr	|- ( ( ph /\ A = 0 ) -> ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( B ^ 2 ) )
13		sqnprm	|- ( B e. ZZ -> -. ( B ^ 2 ) e. Prime )
14	3 13	syl	|- ( ph -> -. ( B ^ 2 ) e. Prime )
15	14	adantr	|- ( ( ph /\ A = 0 ) -> -. ( B ^ 2 ) e. Prime )
16	12 15	eqneltrd	|- ( ( ph /\ A = 0 ) -> -. ( ( A ^ 2 ) + ( B ^ 2 ) ) e. Prime )
17	6 16	pm2.65da	|- ( ph -> -. A = 0 )
18	17	neqned	|- ( ph -> A =/= 0 )