2sqcoprm

Description: If the sum of two squares is prime, the two original numbers are coprime. (Contributed by Thierry Arnoux, 2-Feb-2020)

	Ref	Expression
Hypotheses	2sqcoprm.1	$⊢ φ \to P \in ℙ$
	2sqcoprm.2	$⊢ φ \to A \in ℤ$
	2sqcoprm.3	$⊢ φ \to B \in ℤ$
	2sqcoprm.4	$⊢ φ \to A^{2} + B^{2} = P$
Assertion	2sqcoprm	$⊢ φ \to A \gcd B = 1$

Proof

Step	Hyp	Ref	Expression
1		2sqcoprm.1	$⊢ φ \to P \in ℙ$
2		2sqcoprm.2	$⊢ φ \to A \in ℤ$
3		2sqcoprm.3	$⊢ φ \to B \in ℤ$
4		2sqcoprm.4	$⊢ φ \to A^{2} + B^{2} = P$
5	1 2 3 4	2sqn0	$⊢ φ \to A \neq 0$
6	2 3	gcdcld	$⊢ φ \to A \gcd B \in ℕ_{0}$
7	6	adantr	$⊢ (φ \land A \neq 0) \to A \gcd B \in ℕ_{0}$
8	2	adantr	$⊢ (φ \land A \neq 0) \to A \in ℤ$
9	3	adantr	$⊢ (φ \land A \neq 0) \to B \in ℤ$
10		simpr	$⊢ (φ \land A \neq 0) \to A \neq 0$
11	10	neneqd	$⊢ (φ \land A \neq 0) \to \neg A = 0$
12	11	intnanrd	$⊢ (φ \land A \neq 0) \to \neg (A = 0 \land B = 0)$
13		gcdn0cl	$⊢ ((A \in ℤ \land B \in ℤ) \land \neg (A = 0 \land B = 0)) \to A \gcd B \in ℕ$
14	8 9 12 13	syl21anc	$⊢ (φ \land A \neq 0) \to A \gcd B \in ℕ$
15	14	nnsqcld	$⊢ (φ \land A \neq 0) \to {(A \gcd B)}^{2} \in ℕ$
16	6	nn0zd	$⊢ φ \to A \gcd B \in ℤ$
17		sqnprm	$⊢ A \gcd B \in ℤ \to \neg {(A \gcd B)}^{2} \in ℙ$
18	16 17	syl	$⊢ φ \to \neg {(A \gcd B)}^{2} \in ℙ$
19		zsqcl	$⊢ A \gcd B \in ℤ \to {(A \gcd B)}^{2} \in ℤ$
20	16 19	syl	$⊢ φ \to {(A \gcd B)}^{2} \in ℤ$
21		zsqcl	$⊢ A \in ℤ \to A^{2} \in ℤ$
22	2 21	syl	$⊢ φ \to A^{2} \in ℤ$
23		zsqcl	$⊢ B \in ℤ \to B^{2} \in ℤ$
24	3 23	syl	$⊢ φ \to B^{2} \in ℤ$
25		gcddvds	$⊢ (A \in ℤ \land B \in ℤ) \to ((A \gcd B) ∥ A \land (A \gcd B) ∥ B)$
26	2 3 25	syl2anc	$⊢ φ \to ((A \gcd B) ∥ A \land (A \gcd B) ∥ B)$
27	26	simpld	$⊢ φ \to (A \gcd B) ∥ A$
28		dvdssqim	$⊢ (A \gcd B \in ℤ \land A \in ℤ) \to ((A \gcd B) ∥ A \to {(A \gcd B)}^{2} ∥ A^{2})$
29	28	imp	$⊢ ((A \gcd B \in ℤ \land A \in ℤ) \land (A \gcd B) ∥ A) \to {(A \gcd B)}^{2} ∥ A^{2}$
30	16 2 27 29	syl21anc	$⊢ φ \to {(A \gcd B)}^{2} ∥ A^{2}$
31	26	simprd	$⊢ φ \to (A \gcd B) ∥ B$
32		dvdssqim	$⊢ (A \gcd B \in ℤ \land B \in ℤ) \to ((A \gcd B) ∥ B \to {(A \gcd B)}^{2} ∥ B^{2})$
33	32	imp	$⊢ ((A \gcd B \in ℤ \land B \in ℤ) \land (A \gcd B) ∥ B) \to {(A \gcd B)}^{2} ∥ B^{2}$
34	16 3 31 33	syl21anc	$⊢ φ \to {(A \gcd B)}^{2} ∥ B^{2}$
35	20 22 24 30 34	dvds2addd	$⊢ φ \to {(A \gcd B)}^{2} ∥ (A^{2} + B^{2})$
36	35 4	breqtrd	$⊢ φ \to {(A \gcd B)}^{2} ∥ P$
37	36	adantr	$⊢ (φ \land {(A \gcd B)}^{2} \in ℤ_{\geq 2}) \to {(A \gcd B)}^{2} ∥ P$
38		simpr	$⊢ (φ \land {(A \gcd B)}^{2} \in ℤ_{\geq 2}) \to {(A \gcd B)}^{2} \in ℤ_{\geq 2}$
39	1	adantr	$⊢ (φ \land {(A \gcd B)}^{2} \in ℤ_{\geq 2}) \to P \in ℙ$
40		dvdsprm	$⊢ ({(A \gcd B)}^{2} \in ℤ_{\geq 2} \land P \in ℙ) \to ({(A \gcd B)}^{2} ∥ P \leftrightarrow {(A \gcd B)}^{2} = P)$
41	38 39 40	syl2anc	$⊢ (φ \land {(A \gcd B)}^{2} \in ℤ_{\geq 2}) \to ({(A \gcd B)}^{2} ∥ P \leftrightarrow {(A \gcd B)}^{2} = P)$
42	37 41	mpbid	$⊢ (φ \land {(A \gcd B)}^{2} \in ℤ_{\geq 2}) \to {(A \gcd B)}^{2} = P$
43	42 39	eqeltrd	$⊢ (φ \land {(A \gcd B)}^{2} \in ℤ_{\geq 2}) \to {(A \gcd B)}^{2} \in ℙ$
44	18 43	mtand	$⊢ φ \to \neg {(A \gcd B)}^{2} \in ℤ_{\geq 2}$
45		eluz2b3	$⊢ {(A \gcd B)}^{2} \in ℤ_{\geq 2} \leftrightarrow ({(A \gcd B)}^{2} \in ℕ \land {(A \gcd B)}^{2} \neq 1)$
46	44 45	sylnib	$⊢ φ \to \neg ({(A \gcd B)}^{2} \in ℕ \land {(A \gcd B)}^{2} \neq 1)$
47		imnan	$⊢ ({(A \gcd B)}^{2} \in ℕ \to \neg {(A \gcd B)}^{2} \neq 1) \leftrightarrow \neg ({(A \gcd B)}^{2} \in ℕ \land {(A \gcd B)}^{2} \neq 1)$
48	46 47	sylibr	$⊢ φ \to ({(A \gcd B)}^{2} \in ℕ \to \neg {(A \gcd B)}^{2} \neq 1)$
49	48	adantr	$⊢ (φ \land A \neq 0) \to ({(A \gcd B)}^{2} \in ℕ \to \neg {(A \gcd B)}^{2} \neq 1)$
50	15 49	mpd	$⊢ (φ \land A \neq 0) \to \neg {(A \gcd B)}^{2} \neq 1$
51		df-ne	$⊢ {(A \gcd B)}^{2} \neq 1 \leftrightarrow \neg {(A \gcd B)}^{2} = 1$
52	50 51	sylnib	$⊢ (φ \land A \neq 0) \to \neg \neg {(A \gcd B)}^{2} = 1$
53	52	notnotrd	$⊢ (φ \land A \neq 0) \to {(A \gcd B)}^{2} = 1$
54		nn0sqeq1	$⊢ (A \gcd B \in ℕ_{0} \land {(A \gcd B)}^{2} = 1) \to A \gcd B = 1$
55	7 53 54	syl2anc	$⊢ (φ \land A \neq 0) \to A \gcd B = 1$
56	5 55	mpdan	$⊢ φ \to A \gcd B = 1$

Metamath Proof Explorer

Theorem 2sqcoprm

Proof