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 )