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 ⊢ ( 𝜑 → 𝑃 ∈ ℙ )
2sqcoprm.2 ⊢ ( 𝜑 → 𝐴 ∈ ℤ )
2sqcoprm.3 ⊢ ( 𝜑 → 𝐵 ∈ ℤ )
2sqcoprm.4 ⊢ ( 𝜑 → ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = 𝑃 )
Assertion 2sqcoprm ( 𝜑 → ( 𝐴 gcd 𝐵 ) = 1 )

Proof

Step Hyp Ref Expression
1 2sqcoprm.1 ⊢ ( 𝜑 → 𝑃 ∈ ℙ )
2 2sqcoprm.2 ⊢ ( 𝜑 → 𝐴 ∈ ℤ )
3 2sqcoprm.3 ⊢ ( 𝜑 → 𝐵 ∈ ℤ )
4 2sqcoprm.4 ⊢ ( 𝜑 → ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = 𝑃 )
5 1 2 3 4 2sqn0 ⊢ ( 𝜑 → 𝐴 ≠ 0 )
6 2 3 gcdcld ⊢ ( 𝜑 → ( 𝐴 gcd 𝐵 ) ∈ ℕ0 )
7 6 adantr ⊢ ( ( 𝜑 ∧ 𝐴 ≠ 0 ) → ( 𝐴 gcd 𝐵 ) ∈ ℕ0 )
8 2 adantr ⊢ ( ( 𝜑 ∧ 𝐴 ≠ 0 ) → 𝐴 ∈ ℤ )
9 3 adantr ⊢ ( ( 𝜑 ∧ 𝐴 ≠ 0 ) → 𝐵 ∈ ℤ )
10 simpr ⊢ ( ( 𝜑 ∧ 𝐴 ≠ 0 ) → 𝐴 ≠ 0 )
11 10 neneqd ⊢ ( ( 𝜑 ∧ 𝐴 ≠ 0 ) → ¬ 𝐴 = 0 )
12 11 intnanrd ⊢ ( ( 𝜑 ∧ 𝐴 ≠ 0 ) → ¬ ( 𝐴 = 0 ∧ 𝐵 = 0 ) )
13 gcdn0cl ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ¬ ( 𝐴 = 0 ∧ 𝐵 = 0 ) ) → ( 𝐴 gcd 𝐵 ) ∈ ℕ )
14 8 9 12 13 syl21anc ⊢ ( ( 𝜑 ∧ 𝐴 ≠ 0 ) → ( 𝐴 gcd 𝐵 ) ∈ ℕ )
15 14 nnsqcld ⊢ ( ( 𝜑 ∧ 𝐴 ≠ 0 ) → ( ( 𝐴 gcd 𝐵 ) ↑ 2 ) ∈ ℕ )
16 6 nn0zd ⊢ ( 𝜑 → ( 𝐴 gcd 𝐵 ) ∈ ℤ )
17 sqnprm ⊢ ( ( 𝐴 gcd 𝐵 ) ∈ ℤ → ¬ ( ( 𝐴 gcd 𝐵 ) ↑ 2 ) ∈ ℙ )
18 16 17 syl ⊢ ( 𝜑 → ¬ ( ( 𝐴 gcd 𝐵 ) ↑ 2 ) ∈ ℙ )
19 zsqcl ⊢ ( ( 𝐴 gcd 𝐵 ) ∈ ℤ → ( ( 𝐴 gcd 𝐵 ) ↑ 2 ) ∈ ℤ )
20 16 19 syl ⊢ ( 𝜑 → ( ( 𝐴 gcd 𝐵 ) ↑ 2 ) ∈ ℤ )
21 zsqcl ⊢ ( 𝐴 ∈ ℤ → ( 𝐴 ↑ 2 ) ∈ ℤ )
22 2 21 syl ⊢ ( 𝜑 → ( 𝐴 ↑ 2 ) ∈ ℤ )
23 zsqcl ⊢ ( 𝐵 ∈ ℤ → ( 𝐵 ↑ 2 ) ∈ ℤ )
24 3 23 syl ⊢ ( 𝜑 → ( 𝐵 ↑ 2 ) ∈ ℤ )
25 gcddvds ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → ( ( 𝐴 gcd 𝐵 ) ∥ 𝐴 ∧ ( 𝐴 gcd 𝐵 ) ∥ 𝐵 ) )
26 2 3 25 syl2anc ⊢ ( 𝜑 → ( ( 𝐴 gcd 𝐵 ) ∥ 𝐴 ∧ ( 𝐴 gcd 𝐵 ) ∥ 𝐵 ) )
27 26 simpld ⊢ ( 𝜑 → ( 𝐴 gcd 𝐵 ) ∥ 𝐴 )
28 dvdssqim ⊢ ( ( ( 𝐴 gcd 𝐵 ) ∈ ℤ ∧ 𝐴 ∈ ℤ ) → ( ( 𝐴 gcd 𝐵 ) ∥ 𝐴 → ( ( 𝐴 gcd 𝐵 ) ↑ 2 ) ∥ ( 𝐴 ↑ 2 ) ) )
29 28 imp ⊢ ( ( ( ( 𝐴 gcd 𝐵 ) ∈ ℤ ∧ 𝐴 ∈ ℤ ) ∧ ( 𝐴 gcd 𝐵 ) ∥ 𝐴 ) → ( ( 𝐴 gcd 𝐵 ) ↑ 2 ) ∥ ( 𝐴 ↑ 2 ) )
30 16 2 27 29 syl21anc ⊢ ( 𝜑 → ( ( 𝐴 gcd 𝐵 ) ↑ 2 ) ∥ ( 𝐴 ↑ 2 ) )
31 26 simprd ⊢ ( 𝜑 → ( 𝐴 gcd 𝐵 ) ∥ 𝐵 )
32 dvdssqim ⊢ ( ( ( 𝐴 gcd 𝐵 ) ∈ ℤ ∧ 𝐵 ∈ ℤ ) → ( ( 𝐴 gcd 𝐵 ) ∥ 𝐵 → ( ( 𝐴 gcd 𝐵 ) ↑ 2 ) ∥ ( 𝐵 ↑ 2 ) ) )
33 32 imp ⊢ ( ( ( ( 𝐴 gcd 𝐵 ) ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( 𝐴 gcd 𝐵 ) ∥ 𝐵 ) → ( ( 𝐴 gcd 𝐵 ) ↑ 2 ) ∥ ( 𝐵 ↑ 2 ) )
34 16 3 31 33 syl21anc ⊢ ( 𝜑 → ( ( 𝐴 gcd 𝐵 ) ↑ 2 ) ∥ ( 𝐵 ↑ 2 ) )
35 20 22 24 30 34 dvds2addd ⊢ ( 𝜑 → ( ( 𝐴 gcd 𝐵 ) ↑ 2 ) ∥ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) )
36 35 4 breqtrd ⊢ ( 𝜑 → ( ( 𝐴 gcd 𝐵 ) ↑ 2 ) ∥ 𝑃 )
37 36 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝐴 gcd 𝐵 ) ↑ 2 ) ∈ ( ℤ≥ ‘ 2 ) ) → ( ( 𝐴 gcd 𝐵 ) ↑ 2 ) ∥ 𝑃 )
38 simpr ⊢ ( ( 𝜑 ∧ ( ( 𝐴 gcd 𝐵 ) ↑ 2 ) ∈ ( ℤ≥ ‘ 2 ) ) → ( ( 𝐴 gcd 𝐵 ) ↑ 2 ) ∈ ( ℤ≥ ‘ 2 ) )
39 1 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝐴 gcd 𝐵 ) ↑ 2 ) ∈ ( ℤ≥ ‘ 2 ) ) → 𝑃 ∈ ℙ )
40 dvdsprm ⊢ ( ( ( ( 𝐴 gcd 𝐵 ) ↑ 2 ) ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑃 ∈ ℙ ) → ( ( ( 𝐴 gcd 𝐵 ) ↑ 2 ) ∥ 𝑃 ↔ ( ( 𝐴 gcd 𝐵 ) ↑ 2 ) = 𝑃 ) )
41 38 39 40 syl2anc ⊢ ( ( 𝜑 ∧ ( ( 𝐴 gcd 𝐵 ) ↑ 2 ) ∈ ( ℤ≥ ‘ 2 ) ) → ( ( ( 𝐴 gcd 𝐵 ) ↑ 2 ) ∥ 𝑃 ↔ ( ( 𝐴 gcd 𝐵 ) ↑ 2 ) = 𝑃 ) )
42 37 41 mpbid ⊢ ( ( 𝜑 ∧ ( ( 𝐴 gcd 𝐵 ) ↑ 2 ) ∈ ( ℤ≥ ‘ 2 ) ) → ( ( 𝐴 gcd 𝐵 ) ↑ 2 ) = 𝑃 )
43 42 39 eqeltrd ⊢ ( ( 𝜑 ∧ ( ( 𝐴 gcd 𝐵 ) ↑ 2 ) ∈ ( ℤ≥ ‘ 2 ) ) → ( ( 𝐴 gcd 𝐵 ) ↑ 2 ) ∈ ℙ )
44 18 43 mtand ⊢ ( 𝜑 → ¬ ( ( 𝐴 gcd 𝐵 ) ↑ 2 ) ∈ ( ℤ≥ ‘ 2 ) )
45 eluz2b3 ⊢ ( ( ( 𝐴 gcd 𝐵 ) ↑ 2 ) ∈ ( ℤ≥ ‘ 2 ) ↔ ( ( ( 𝐴 gcd 𝐵 ) ↑ 2 ) ∈ ℕ ∧ ( ( 𝐴 gcd 𝐵 ) ↑ 2 ) ≠ 1 ) )
46 44 45 sylnib ⊢ ( 𝜑 → ¬ ( ( ( 𝐴 gcd 𝐵 ) ↑ 2 ) ∈ ℕ ∧ ( ( 𝐴 gcd 𝐵 ) ↑ 2 ) ≠ 1 ) )
47 imnan ⊢ ( ( ( ( 𝐴 gcd 𝐵 ) ↑ 2 ) ∈ ℕ → ¬ ( ( 𝐴 gcd 𝐵 ) ↑ 2 ) ≠ 1 ) ↔ ¬ ( ( ( 𝐴 gcd 𝐵 ) ↑ 2 ) ∈ ℕ ∧ ( ( 𝐴 gcd 𝐵 ) ↑ 2 ) ≠ 1 ) )
48 46 47 sylibr ⊢ ( 𝜑 → ( ( ( 𝐴 gcd 𝐵 ) ↑ 2 ) ∈ ℕ → ¬ ( ( 𝐴 gcd 𝐵 ) ↑ 2 ) ≠ 1 ) )
49 48 adantr ⊢ ( ( 𝜑 ∧ 𝐴 ≠ 0 ) → ( ( ( 𝐴 gcd 𝐵 ) ↑ 2 ) ∈ ℕ → ¬ ( ( 𝐴 gcd 𝐵 ) ↑ 2 ) ≠ 1 ) )
50 15 49 mpd ⊢ ( ( 𝜑 ∧ 𝐴 ≠ 0 ) → ¬ ( ( 𝐴 gcd 𝐵 ) ↑ 2 ) ≠ 1 )
51 df-ne ⊢ ( ( ( 𝐴 gcd 𝐵 ) ↑ 2 ) ≠ 1 ↔ ¬ ( ( 𝐴 gcd 𝐵 ) ↑ 2 ) = 1 )
52 50 51 sylnib ⊢ ( ( 𝜑 ∧ 𝐴 ≠ 0 ) → ¬ ¬ ( ( 𝐴 gcd 𝐵 ) ↑ 2 ) = 1 )
53 52 notnotrd ⊢ ( ( 𝜑 ∧ 𝐴 ≠ 0 ) → ( ( 𝐴 gcd 𝐵 ) ↑ 2 ) = 1 )
54 nn0sqeq1 ⊢ ( ( ( 𝐴 gcd 𝐵 ) ∈ ℕ0 ∧ ( ( 𝐴 gcd 𝐵 ) ↑ 2 ) = 1 ) → ( 𝐴 gcd 𝐵 ) = 1 )
55 7 53 54 syl2anc ⊢ ( ( 𝜑 ∧ 𝐴 ≠ 0 ) → ( 𝐴 gcd 𝐵 ) = 1 )
56 5 55 mpdan ⊢ ( 𝜑 → ( 𝐴 gcd 𝐵 ) = 1 )