Metamath Proof Explorer


Theorem 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 φP
2sqcoprm.2 φA
2sqcoprm.3 φB
2sqcoprm.4 φA2+B2=P
Assertion 2sqcoprm φAgcdB=1

Proof

Step Hyp Ref Expression
1 2sqcoprm.1 φP
2 2sqcoprm.2 φA
3 2sqcoprm.3 φB
4 2sqcoprm.4 φA2+B2=P
5 1 2 3 4 2sqn0 φA0
6 2 3 gcdcld φAgcdB0
7 6 adantr φA0AgcdB0
8 2 adantr φA0A
9 3 adantr φA0B
10 simpr φA0A0
11 10 neneqd φA0¬A=0
12 11 intnanrd φA0¬A=0B=0
13 gcdn0cl AB¬A=0B=0AgcdB
14 8 9 12 13 syl21anc φA0AgcdB
15 14 nnsqcld φA0AgcdB2
16 6 nn0zd φAgcdB
17 sqnprm AgcdB¬AgcdB2
18 16 17 syl φ¬AgcdB2
19 zsqcl AgcdBAgcdB2
20 16 19 syl φAgcdB2
21 zsqcl AA2
22 2 21 syl φA2
23 zsqcl BB2
24 3 23 syl φB2
25 gcddvds ABAgcdBAAgcdBB
26 2 3 25 syl2anc φAgcdBAAgcdBB
27 26 simpld φAgcdBA
28 dvdssqim AgcdBAAgcdBAAgcdB2A2
29 28 imp AgcdBAAgcdBAAgcdB2A2
30 16 2 27 29 syl21anc φAgcdB2A2
31 26 simprd φAgcdBB
32 dvdssqim AgcdBBAgcdBBAgcdB2B2
33 32 imp AgcdBBAgcdBBAgcdB2B2
34 16 3 31 33 syl21anc φAgcdB2B2
35 20 22 24 30 34 dvds2addd φAgcdB2A2+B2
36 35 4 breqtrd φAgcdB2P
37 36 adantr φAgcdB22AgcdB2P
38 simpr φAgcdB22AgcdB22
39 1 adantr φAgcdB22P
40 dvdsprm AgcdB22PAgcdB2PAgcdB2=P
41 38 39 40 syl2anc φAgcdB22AgcdB2PAgcdB2=P
42 37 41 mpbid φAgcdB22AgcdB2=P
43 42 39 eqeltrd φAgcdB22AgcdB2
44 18 43 mtand φ¬AgcdB22
45 eluz2b3 AgcdB22AgcdB2AgcdB21
46 44 45 sylnib φ¬AgcdB2AgcdB21
47 imnan AgcdB2¬AgcdB21¬AgcdB2AgcdB21
48 46 47 sylibr φAgcdB2¬AgcdB21
49 48 adantr φA0AgcdB2¬AgcdB21
50 15 49 mpd φA0¬AgcdB21
51 df-ne AgcdB21¬AgcdB2=1
52 50 51 sylnib φA0¬¬AgcdB2=1
53 52 notnotrd φA0AgcdB2=1
54 nn0sqeq1 AgcdB0AgcdB2=1AgcdB=1
55 7 53 54 syl2anc φA0AgcdB=1
56 5 55 mpdan φAgcdB=1