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 | |
|
2sqcoprm.2 | |
||
2sqcoprm.3 | |
||
2sqcoprm.4 | |
||
Assertion | 2sqcoprm | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 2sqcoprm.1 | |
|
2 | 2sqcoprm.2 | |
|
3 | 2sqcoprm.3 | |
|
4 | 2sqcoprm.4 | |
|
5 | 1 2 3 4 | 2sqn0 | |
6 | 2 3 | gcdcld | |
7 | 6 | adantr | |
8 | 2 | adantr | |
9 | 3 | adantr | |
10 | simpr | |
|
11 | 10 | neneqd | |
12 | 11 | intnanrd | |
13 | gcdn0cl | |
|
14 | 8 9 12 13 | syl21anc | |
15 | 14 | nnsqcld | |
16 | 6 | nn0zd | |
17 | sqnprm | |
|
18 | 16 17 | syl | |
19 | zsqcl | |
|
20 | 16 19 | syl | |
21 | zsqcl | |
|
22 | 2 21 | syl | |
23 | zsqcl | |
|
24 | 3 23 | syl | |
25 | gcddvds | |
|
26 | 2 3 25 | syl2anc | |
27 | 26 | simpld | |
28 | dvdssqim | |
|
29 | 28 | imp | |
30 | 16 2 27 29 | syl21anc | |
31 | 26 | simprd | |
32 | dvdssqim | |
|
33 | 32 | imp | |
34 | 16 3 31 33 | syl21anc | |
35 | 20 22 24 30 34 | dvds2addd | |
36 | 35 4 | breqtrd | |
37 | 36 | adantr | |
38 | simpr | |
|
39 | 1 | adantr | |
40 | dvdsprm | |
|
41 | 38 39 40 | syl2anc | |
42 | 37 41 | mpbid | |
43 | 42 39 | eqeltrd | |
44 | 18 43 | mtand | |
45 | eluz2b3 | |
|
46 | 44 45 | sylnib | |
47 | imnan | |
|
48 | 46 47 | sylibr | |
49 | 48 | adantr | |
50 | 15 49 | mpd | |
51 | df-ne | |
|
52 | 50 51 | sylnib | |
53 | 52 | notnotrd | |
54 | nn0sqeq1 | |
|
55 | 7 53 54 | syl2anc | |
56 | 5 55 | mpdan | |