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
|- ( 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 2sqcoprm
|- ( ph -> ( A gcd B ) = 1 )

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 1 2 3 4 2sqn0
 |-  ( ph -> A =/= 0 )
6 2 3 gcdcld
 |-  ( ph -> ( A gcd B ) e. NN0 )
7 6 adantr
 |-  ( ( ph /\ A =/= 0 ) -> ( A gcd B ) e. NN0 )
8 2 adantr
 |-  ( ( ph /\ A =/= 0 ) -> A e. ZZ )
9 3 adantr
 |-  ( ( ph /\ A =/= 0 ) -> B e. ZZ )
10 simpr
 |-  ( ( ph /\ A =/= 0 ) -> A =/= 0 )
11 10 neneqd
 |-  ( ( ph /\ A =/= 0 ) -> -. A = 0 )
12 11 intnanrd
 |-  ( ( ph /\ A =/= 0 ) -> -. ( A = 0 /\ B = 0 ) )
13 gcdn0cl
 |-  ( ( ( A e. ZZ /\ B e. ZZ ) /\ -. ( A = 0 /\ B = 0 ) ) -> ( A gcd B ) e. NN )
14 8 9 12 13 syl21anc
 |-  ( ( ph /\ A =/= 0 ) -> ( A gcd B ) e. NN )
15 14 nnsqcld
 |-  ( ( ph /\ A =/= 0 ) -> ( ( A gcd B ) ^ 2 ) e. NN )
16 6 nn0zd
 |-  ( ph -> ( A gcd B ) e. ZZ )
17 sqnprm
 |-  ( ( A gcd B ) e. ZZ -> -. ( ( A gcd B ) ^ 2 ) e. Prime )
18 16 17 syl
 |-  ( ph -> -. ( ( A gcd B ) ^ 2 ) e. Prime )
19 zsqcl
 |-  ( ( A gcd B ) e. ZZ -> ( ( A gcd B ) ^ 2 ) e. ZZ )
20 16 19 syl
 |-  ( ph -> ( ( A gcd B ) ^ 2 ) e. ZZ )
21 zsqcl
 |-  ( A e. ZZ -> ( A ^ 2 ) e. ZZ )
22 2 21 syl
 |-  ( ph -> ( A ^ 2 ) e. ZZ )
23 zsqcl
 |-  ( B e. ZZ -> ( B ^ 2 ) e. ZZ )
24 3 23 syl
 |-  ( ph -> ( B ^ 2 ) e. ZZ )
25 gcddvds
 |-  ( ( A e. ZZ /\ B e. ZZ ) -> ( ( A gcd B ) || A /\ ( A gcd B ) || B ) )
26 2 3 25 syl2anc
 |-  ( ph -> ( ( A gcd B ) || A /\ ( A gcd B ) || B ) )
27 26 simpld
 |-  ( ph -> ( A gcd B ) || A )
28 dvdssqim
 |-  ( ( ( A gcd B ) e. ZZ /\ A e. ZZ ) -> ( ( A gcd B ) || A -> ( ( A gcd B ) ^ 2 ) || ( A ^ 2 ) ) )
29 28 imp
 |-  ( ( ( ( A gcd B ) e. ZZ /\ A e. ZZ ) /\ ( A gcd B ) || A ) -> ( ( A gcd B ) ^ 2 ) || ( A ^ 2 ) )
30 16 2 27 29 syl21anc
 |-  ( ph -> ( ( A gcd B ) ^ 2 ) || ( A ^ 2 ) )
31 26 simprd
 |-  ( ph -> ( A gcd B ) || B )
32 dvdssqim
 |-  ( ( ( A gcd B ) e. ZZ /\ B e. ZZ ) -> ( ( A gcd B ) || B -> ( ( A gcd B ) ^ 2 ) || ( B ^ 2 ) ) )
33 32 imp
 |-  ( ( ( ( A gcd B ) e. ZZ /\ B e. ZZ ) /\ ( A gcd B ) || B ) -> ( ( A gcd B ) ^ 2 ) || ( B ^ 2 ) )
34 16 3 31 33 syl21anc
 |-  ( ph -> ( ( A gcd B ) ^ 2 ) || ( B ^ 2 ) )
35 20 22 24 30 34 dvds2addd
 |-  ( ph -> ( ( A gcd B ) ^ 2 ) || ( ( A ^ 2 ) + ( B ^ 2 ) ) )
36 35 4 breqtrd
 |-  ( ph -> ( ( A gcd B ) ^ 2 ) || P )
37 36 adantr
 |-  ( ( ph /\ ( ( A gcd B ) ^ 2 ) e. ( ZZ>= ` 2 ) ) -> ( ( A gcd B ) ^ 2 ) || P )
38 simpr
 |-  ( ( ph /\ ( ( A gcd B ) ^ 2 ) e. ( ZZ>= ` 2 ) ) -> ( ( A gcd B ) ^ 2 ) e. ( ZZ>= ` 2 ) )
39 1 adantr
 |-  ( ( ph /\ ( ( A gcd B ) ^ 2 ) e. ( ZZ>= ` 2 ) ) -> P e. Prime )
40 dvdsprm
 |-  ( ( ( ( A gcd B ) ^ 2 ) e. ( ZZ>= ` 2 ) /\ P e. Prime ) -> ( ( ( A gcd B ) ^ 2 ) || P <-> ( ( A gcd B ) ^ 2 ) = P ) )
41 38 39 40 syl2anc
 |-  ( ( ph /\ ( ( A gcd B ) ^ 2 ) e. ( ZZ>= ` 2 ) ) -> ( ( ( A gcd B ) ^ 2 ) || P <-> ( ( A gcd B ) ^ 2 ) = P ) )
42 37 41 mpbid
 |-  ( ( ph /\ ( ( A gcd B ) ^ 2 ) e. ( ZZ>= ` 2 ) ) -> ( ( A gcd B ) ^ 2 ) = P )
43 42 39 eqeltrd
 |-  ( ( ph /\ ( ( A gcd B ) ^ 2 ) e. ( ZZ>= ` 2 ) ) -> ( ( A gcd B ) ^ 2 ) e. Prime )
44 18 43 mtand
 |-  ( ph -> -. ( ( A gcd B ) ^ 2 ) e. ( ZZ>= ` 2 ) )
45 eluz2b3
 |-  ( ( ( A gcd B ) ^ 2 ) e. ( ZZ>= ` 2 ) <-> ( ( ( A gcd B ) ^ 2 ) e. NN /\ ( ( A gcd B ) ^ 2 ) =/= 1 ) )
46 44 45 sylnib
 |-  ( ph -> -. ( ( ( A gcd B ) ^ 2 ) e. NN /\ ( ( A gcd B ) ^ 2 ) =/= 1 ) )
47 imnan
 |-  ( ( ( ( A gcd B ) ^ 2 ) e. NN -> -. ( ( A gcd B ) ^ 2 ) =/= 1 ) <-> -. ( ( ( A gcd B ) ^ 2 ) e. NN /\ ( ( A gcd B ) ^ 2 ) =/= 1 ) )
48 46 47 sylibr
 |-  ( ph -> ( ( ( A gcd B ) ^ 2 ) e. NN -> -. ( ( A gcd B ) ^ 2 ) =/= 1 ) )
49 48 adantr
 |-  ( ( ph /\ A =/= 0 ) -> ( ( ( A gcd B ) ^ 2 ) e. NN -> -. ( ( A gcd B ) ^ 2 ) =/= 1 ) )
50 15 49 mpd
 |-  ( ( ph /\ A =/= 0 ) -> -. ( ( A gcd B ) ^ 2 ) =/= 1 )
51 df-ne
 |-  ( ( ( A gcd B ) ^ 2 ) =/= 1 <-> -. ( ( A gcd B ) ^ 2 ) = 1 )
52 50 51 sylnib
 |-  ( ( ph /\ A =/= 0 ) -> -. -. ( ( A gcd B ) ^ 2 ) = 1 )
53 52 notnotrd
 |-  ( ( ph /\ A =/= 0 ) -> ( ( A gcd B ) ^ 2 ) = 1 )
54 nn0sqeq1
 |-  ( ( ( A gcd B ) e. NN0 /\ ( ( A gcd B ) ^ 2 ) = 1 ) -> ( A gcd B ) = 1 )
55 7 53 54 syl2anc
 |-  ( ( ph /\ A =/= 0 ) -> ( A gcd B ) = 1 )
56 5 55 mpdan
 |-  ( ph -> ( A gcd B ) = 1 )