Proof of Theorem 2sqcoprm
Step | Hyp | Ref
| Expression |
1 | | 2sqcoprm.1 |
. . 3
⊢ (𝜑 → 𝑃 ∈ ℙ) |
2 | | 2sqcoprm.2 |
. . 3
⊢ (𝜑 → 𝐴 ∈ ℤ) |
3 | | 2sqcoprm.3 |
. . 3
⊢ (𝜑 → 𝐵 ∈ ℤ) |
4 | | 2sqcoprm.4 |
. . 3
⊢ (𝜑 → ((𝐴↑2) + (𝐵↑2)) = 𝑃) |
5 | 1, 2, 3, 4 | 2sqn0 26170 |
. 2
⊢ (𝜑 → 𝐴 ≠ 0) |
6 | 2, 3 | gcdcld 15951 |
. . . 4
⊢ (𝜑 → (𝐴 gcd 𝐵) ∈
ℕ0) |
7 | 6 | adantr 484 |
. . 3
⊢ ((𝜑 ∧ 𝐴 ≠ 0) → (𝐴 gcd 𝐵) ∈
ℕ0) |
8 | 2 | adantr 484 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝐴 ≠ 0) → 𝐴 ∈ ℤ) |
9 | 3 | adantr 484 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝐴 ≠ 0) → 𝐵 ∈ ℤ) |
10 | | simpr 488 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝐴 ≠ 0) → 𝐴 ≠ 0) |
11 | 10 | neneqd 2939 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝐴 ≠ 0) → ¬ 𝐴 = 0) |
12 | 11 | intnanrd 493 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝐴 ≠ 0) → ¬ (𝐴 = 0 ∧ 𝐵 = 0)) |
13 | | gcdn0cl 15945 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ ¬
(𝐴 = 0 ∧ 𝐵 = 0)) → (𝐴 gcd 𝐵) ∈ ℕ) |
14 | 8, 9, 12, 13 | syl21anc 837 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝐴 ≠ 0) → (𝐴 gcd 𝐵) ∈ ℕ) |
15 | 14 | nnsqcld 13697 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐴 ≠ 0) → ((𝐴 gcd 𝐵)↑2) ∈ ℕ) |
16 | 6 | nn0zd 12166 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐴 gcd 𝐵) ∈ ℤ) |
17 | | sqnprm 16143 |
. . . . . . . . . . 11
⊢ ((𝐴 gcd 𝐵) ∈ ℤ → ¬ ((𝐴 gcd 𝐵)↑2) ∈ ℙ) |
18 | 16, 17 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → ¬ ((𝐴 gcd 𝐵)↑2) ∈ ℙ) |
19 | | zsqcl 13586 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐴 gcd 𝐵) ∈ ℤ → ((𝐴 gcd 𝐵)↑2) ∈ ℤ) |
20 | 16, 19 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ((𝐴 gcd 𝐵)↑2) ∈ ℤ) |
21 | | zsqcl 13586 |
. . . . . . . . . . . . . . . 16
⊢ (𝐴 ∈ ℤ → (𝐴↑2) ∈
ℤ) |
22 | 2, 21 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝐴↑2) ∈ ℤ) |
23 | | zsqcl 13586 |
. . . . . . . . . . . . . . . 16
⊢ (𝐵 ∈ ℤ → (𝐵↑2) ∈
ℤ) |
24 | 3, 23 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝐵↑2) ∈ ℤ) |
25 | | gcddvds 15946 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → ((𝐴 gcd 𝐵) ∥ 𝐴 ∧ (𝐴 gcd 𝐵) ∥ 𝐵)) |
26 | 2, 3, 25 | syl2anc 587 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ((𝐴 gcd 𝐵) ∥ 𝐴 ∧ (𝐴 gcd 𝐵) ∥ 𝐵)) |
27 | 26 | simpld 498 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝐴 gcd 𝐵) ∥ 𝐴) |
28 | | dvdssqim 16000 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐴 gcd 𝐵) ∈ ℤ ∧ 𝐴 ∈ ℤ) → ((𝐴 gcd 𝐵) ∥ 𝐴 → ((𝐴 gcd 𝐵)↑2) ∥ (𝐴↑2))) |
29 | 28 | imp 410 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐴 gcd 𝐵) ∈ ℤ ∧ 𝐴 ∈ ℤ) ∧ (𝐴 gcd 𝐵) ∥ 𝐴) → ((𝐴 gcd 𝐵)↑2) ∥ (𝐴↑2)) |
30 | 16, 2, 27, 29 | syl21anc 837 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ((𝐴 gcd 𝐵)↑2) ∥ (𝐴↑2)) |
31 | 26 | simprd 499 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝐴 gcd 𝐵) ∥ 𝐵) |
32 | | dvdssqim 16000 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐴 gcd 𝐵) ∈ ℤ ∧ 𝐵 ∈ ℤ) → ((𝐴 gcd 𝐵) ∥ 𝐵 → ((𝐴 gcd 𝐵)↑2) ∥ (𝐵↑2))) |
33 | 32 | imp 410 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐴 gcd 𝐵) ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ (𝐴 gcd 𝐵) ∥ 𝐵) → ((𝐴 gcd 𝐵)↑2) ∥ (𝐵↑2)) |
34 | 16, 3, 31, 33 | syl21anc 837 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ((𝐴 gcd 𝐵)↑2) ∥ (𝐵↑2)) |
35 | 20, 22, 24, 30, 34 | dvds2addd 15737 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((𝐴 gcd 𝐵)↑2) ∥ ((𝐴↑2) + (𝐵↑2))) |
36 | 35, 4 | breqtrd 5056 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((𝐴 gcd 𝐵)↑2) ∥ 𝑃) |
37 | 36 | adantr 484 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ ((𝐴 gcd 𝐵)↑2) ∈
(ℤ≥‘2)) → ((𝐴 gcd 𝐵)↑2) ∥ 𝑃) |
38 | | simpr 488 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ ((𝐴 gcd 𝐵)↑2) ∈
(ℤ≥‘2)) → ((𝐴 gcd 𝐵)↑2) ∈
(ℤ≥‘2)) |
39 | 1 | adantr 484 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ ((𝐴 gcd 𝐵)↑2) ∈
(ℤ≥‘2)) → 𝑃 ∈ ℙ) |
40 | | dvdsprm 16144 |
. . . . . . . . . . . . 13
⊢ ((((𝐴 gcd 𝐵)↑2) ∈
(ℤ≥‘2) ∧ 𝑃 ∈ ℙ) → (((𝐴 gcd 𝐵)↑2) ∥ 𝑃 ↔ ((𝐴 gcd 𝐵)↑2) = 𝑃)) |
41 | 38, 39, 40 | syl2anc 587 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ ((𝐴 gcd 𝐵)↑2) ∈
(ℤ≥‘2)) → (((𝐴 gcd 𝐵)↑2) ∥ 𝑃 ↔ ((𝐴 gcd 𝐵)↑2) = 𝑃)) |
42 | 37, 41 | mpbid 235 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ ((𝐴 gcd 𝐵)↑2) ∈
(ℤ≥‘2)) → ((𝐴 gcd 𝐵)↑2) = 𝑃) |
43 | 42, 39 | eqeltrd 2833 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ ((𝐴 gcd 𝐵)↑2) ∈
(ℤ≥‘2)) → ((𝐴 gcd 𝐵)↑2) ∈ ℙ) |
44 | 18, 43 | mtand 816 |
. . . . . . . . 9
⊢ (𝜑 → ¬ ((𝐴 gcd 𝐵)↑2) ∈
(ℤ≥‘2)) |
45 | | eluz2b3 12404 |
. . . . . . . . 9
⊢ (((𝐴 gcd 𝐵)↑2) ∈
(ℤ≥‘2) ↔ (((𝐴 gcd 𝐵)↑2) ∈ ℕ ∧ ((𝐴 gcd 𝐵)↑2) ≠ 1)) |
46 | 44, 45 | sylnib 331 |
. . . . . . . 8
⊢ (𝜑 → ¬ (((𝐴 gcd 𝐵)↑2) ∈ ℕ ∧ ((𝐴 gcd 𝐵)↑2) ≠ 1)) |
47 | | imnan 403 |
. . . . . . . 8
⊢ ((((𝐴 gcd 𝐵)↑2) ∈ ℕ → ¬
((𝐴 gcd 𝐵)↑2) ≠ 1) ↔ ¬ (((𝐴 gcd 𝐵)↑2) ∈ ℕ ∧ ((𝐴 gcd 𝐵)↑2) ≠ 1)) |
48 | 46, 47 | sylibr 237 |
. . . . . . 7
⊢ (𝜑 → (((𝐴 gcd 𝐵)↑2) ∈ ℕ → ¬
((𝐴 gcd 𝐵)↑2) ≠ 1)) |
49 | 48 | adantr 484 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐴 ≠ 0) → (((𝐴 gcd 𝐵)↑2) ∈ ℕ → ¬
((𝐴 gcd 𝐵)↑2) ≠ 1)) |
50 | 15, 49 | mpd 15 |
. . . . 5
⊢ ((𝜑 ∧ 𝐴 ≠ 0) → ¬ ((𝐴 gcd 𝐵)↑2) ≠ 1) |
51 | | df-ne 2935 |
. . . . 5
⊢ (((𝐴 gcd 𝐵)↑2) ≠ 1 ↔ ¬ ((𝐴 gcd 𝐵)↑2) = 1) |
52 | 50, 51 | sylnib 331 |
. . . 4
⊢ ((𝜑 ∧ 𝐴 ≠ 0) → ¬ ¬ ((𝐴 gcd 𝐵)↑2) = 1) |
53 | 52 | notnotrd 135 |
. . 3
⊢ ((𝜑 ∧ 𝐴 ≠ 0) → ((𝐴 gcd 𝐵)↑2) = 1) |
54 | | nn0sqeq1 14726 |
. . 3
⊢ (((𝐴 gcd 𝐵) ∈ ℕ0 ∧ ((𝐴 gcd 𝐵)↑2) = 1) → (𝐴 gcd 𝐵) = 1) |
55 | 7, 53, 54 | syl2anc 587 |
. 2
⊢ ((𝜑 ∧ 𝐴 ≠ 0) → (𝐴 gcd 𝐵) = 1) |
56 | 5, 55 | mpdan 687 |
1
⊢ (𝜑 → (𝐴 gcd 𝐵) = 1) |