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 30180 |
. 2
⊢ (𝜑 → 𝐴 ≠ 0) |
6 | 2, 3 | gcdcld 15603 |
. . . 4
⊢ (𝜑 → (𝐴 gcd 𝐵) ∈
ℕ0) |
7 | 6 | adantr 474 |
. . 3
⊢ ((𝜑 ∧ 𝐴 ≠ 0) → (𝐴 gcd 𝐵) ∈
ℕ0) |
8 | 2 | adantr 474 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝐴 ≠ 0) → 𝐴 ∈ ℤ) |
9 | 3 | adantr 474 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝐴 ≠ 0) → 𝐵 ∈ ℤ) |
10 | | simpr 479 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝐴 ≠ 0) → 𝐴 ≠ 0) |
11 | 10 | neneqd 3004 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝐴 ≠ 0) → ¬ 𝐴 = 0) |
12 | 11 | intnanrd 485 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝐴 ≠ 0) → ¬ (𝐴 = 0 ∧ 𝐵 = 0)) |
13 | | gcdn0cl 15597 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ ¬
(𝐴 = 0 ∧ 𝐵 = 0)) → (𝐴 gcd 𝐵) ∈ ℕ) |
14 | 8, 9, 12, 13 | syl21anc 871 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝐴 ≠ 0) → (𝐴 gcd 𝐵) ∈ ℕ) |
15 | 14 | nnsqcld 13325 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐴 ≠ 0) → ((𝐴 gcd 𝐵)↑2) ∈ ℕ) |
16 | 6 | nn0zd 11808 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐴 gcd 𝐵) ∈ ℤ) |
17 | | sqnprm 15785 |
. . . . . . . . . . 11
⊢ ((𝐴 gcd 𝐵) ∈ ℤ → ¬ ((𝐴 gcd 𝐵)↑2) ∈ ℙ) |
18 | 16, 17 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → ¬ ((𝐴 gcd 𝐵)↑2) ∈ ℙ) |
19 | | zsqcl 13228 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐴 gcd 𝐵) ∈ ℤ → ((𝐴 gcd 𝐵)↑2) ∈ ℤ) |
20 | 16, 19 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ((𝐴 gcd 𝐵)↑2) ∈ ℤ) |
21 | | zsqcl 13228 |
. . . . . . . . . . . . . . . 16
⊢ (𝐴 ∈ ℤ → (𝐴↑2) ∈
ℤ) |
22 | 2, 21 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝐴↑2) ∈ ℤ) |
23 | | zsqcl 13228 |
. . . . . . . . . . . . . . . 16
⊢ (𝐵 ∈ ℤ → (𝐵↑2) ∈
ℤ) |
24 | 3, 23 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝐵↑2) ∈ ℤ) |
25 | | gcddvds 15598 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → ((𝐴 gcd 𝐵) ∥ 𝐴 ∧ (𝐴 gcd 𝐵) ∥ 𝐵)) |
26 | 2, 3, 25 | syl2anc 579 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ((𝐴 gcd 𝐵) ∥ 𝐴 ∧ (𝐴 gcd 𝐵) ∥ 𝐵)) |
27 | 26 | simpld 490 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝐴 gcd 𝐵) ∥ 𝐴) |
28 | | dvdssqim 15646 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐴 gcd 𝐵) ∈ ℤ ∧ 𝐴 ∈ ℤ) → ((𝐴 gcd 𝐵) ∥ 𝐴 → ((𝐴 gcd 𝐵)↑2) ∥ (𝐴↑2))) |
29 | 28 | imp 397 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐴 gcd 𝐵) ∈ ℤ ∧ 𝐴 ∈ ℤ) ∧ (𝐴 gcd 𝐵) ∥ 𝐴) → ((𝐴 gcd 𝐵)↑2) ∥ (𝐴↑2)) |
30 | 16, 2, 27, 29 | syl21anc 871 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ((𝐴 gcd 𝐵)↑2) ∥ (𝐴↑2)) |
31 | 26 | simprd 491 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝐴 gcd 𝐵) ∥ 𝐵) |
32 | | dvdssqim 15646 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐴 gcd 𝐵) ∈ ℤ ∧ 𝐵 ∈ ℤ) → ((𝐴 gcd 𝐵) ∥ 𝐵 → ((𝐴 gcd 𝐵)↑2) ∥ (𝐵↑2))) |
33 | 32 | imp 397 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐴 gcd 𝐵) ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ (𝐴 gcd 𝐵) ∥ 𝐵) → ((𝐴 gcd 𝐵)↑2) ∥ (𝐵↑2)) |
34 | 16, 3, 31, 33 | syl21anc 871 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ((𝐴 gcd 𝐵)↑2) ∥ (𝐵↑2)) |
35 | | dvds2add 15392 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐴 gcd 𝐵)↑2) ∈ ℤ ∧ (𝐴↑2) ∈ ℤ ∧
(𝐵↑2) ∈ ℤ)
→ ((((𝐴 gcd 𝐵)↑2) ∥ (𝐴↑2) ∧ ((𝐴 gcd 𝐵)↑2) ∥ (𝐵↑2)) → ((𝐴 gcd 𝐵)↑2) ∥ ((𝐴↑2) + (𝐵↑2)))) |
36 | 35 | imp 397 |
. . . . . . . . . . . . . . 15
⊢
(((((𝐴 gcd 𝐵)↑2) ∈ ℤ ∧
(𝐴↑2) ∈ ℤ
∧ (𝐵↑2) ∈
ℤ) ∧ (((𝐴 gcd
𝐵)↑2) ∥ (𝐴↑2) ∧ ((𝐴 gcd 𝐵)↑2) ∥ (𝐵↑2))) → ((𝐴 gcd 𝐵)↑2) ∥ ((𝐴↑2) + (𝐵↑2))) |
37 | 20, 22, 24, 30, 34, 36 | syl32anc 1501 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((𝐴 gcd 𝐵)↑2) ∥ ((𝐴↑2) + (𝐵↑2))) |
38 | 37, 4 | breqtrd 4899 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((𝐴 gcd 𝐵)↑2) ∥ 𝑃) |
39 | 38 | adantr 474 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ ((𝐴 gcd 𝐵)↑2) ∈
(ℤ≥‘2)) → ((𝐴 gcd 𝐵)↑2) ∥ 𝑃) |
40 | | simpr 479 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ ((𝐴 gcd 𝐵)↑2) ∈
(ℤ≥‘2)) → ((𝐴 gcd 𝐵)↑2) ∈
(ℤ≥‘2)) |
41 | 1 | adantr 474 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ ((𝐴 gcd 𝐵)↑2) ∈
(ℤ≥‘2)) → 𝑃 ∈ ℙ) |
42 | | dvdsprm 15786 |
. . . . . . . . . . . . 13
⊢ ((((𝐴 gcd 𝐵)↑2) ∈
(ℤ≥‘2) ∧ 𝑃 ∈ ℙ) → (((𝐴 gcd 𝐵)↑2) ∥ 𝑃 ↔ ((𝐴 gcd 𝐵)↑2) = 𝑃)) |
43 | 40, 41, 42 | syl2anc 579 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ ((𝐴 gcd 𝐵)↑2) ∈
(ℤ≥‘2)) → (((𝐴 gcd 𝐵)↑2) ∥ 𝑃 ↔ ((𝐴 gcd 𝐵)↑2) = 𝑃)) |
44 | 39, 43 | mpbid 224 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ ((𝐴 gcd 𝐵)↑2) ∈
(ℤ≥‘2)) → ((𝐴 gcd 𝐵)↑2) = 𝑃) |
45 | 44, 41 | eqeltrd 2906 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ ((𝐴 gcd 𝐵)↑2) ∈
(ℤ≥‘2)) → ((𝐴 gcd 𝐵)↑2) ∈ ℙ) |
46 | 18, 45 | mtand 850 |
. . . . . . . . 9
⊢ (𝜑 → ¬ ((𝐴 gcd 𝐵)↑2) ∈
(ℤ≥‘2)) |
47 | | eluz2b3 12045 |
. . . . . . . . 9
⊢ (((𝐴 gcd 𝐵)↑2) ∈
(ℤ≥‘2) ↔ (((𝐴 gcd 𝐵)↑2) ∈ ℕ ∧ ((𝐴 gcd 𝐵)↑2) ≠ 1)) |
48 | 46, 47 | sylnib 320 |
. . . . . . . 8
⊢ (𝜑 → ¬ (((𝐴 gcd 𝐵)↑2) ∈ ℕ ∧ ((𝐴 gcd 𝐵)↑2) ≠ 1)) |
49 | | imnan 390 |
. . . . . . . 8
⊢ ((((𝐴 gcd 𝐵)↑2) ∈ ℕ → ¬
((𝐴 gcd 𝐵)↑2) ≠ 1) ↔ ¬ (((𝐴 gcd 𝐵)↑2) ∈ ℕ ∧ ((𝐴 gcd 𝐵)↑2) ≠ 1)) |
50 | 48, 49 | sylibr 226 |
. . . . . . 7
⊢ (𝜑 → (((𝐴 gcd 𝐵)↑2) ∈ ℕ → ¬
((𝐴 gcd 𝐵)↑2) ≠ 1)) |
51 | 50 | adantr 474 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐴 ≠ 0) → (((𝐴 gcd 𝐵)↑2) ∈ ℕ → ¬
((𝐴 gcd 𝐵)↑2) ≠ 1)) |
52 | 15, 51 | mpd 15 |
. . . . 5
⊢ ((𝜑 ∧ 𝐴 ≠ 0) → ¬ ((𝐴 gcd 𝐵)↑2) ≠ 1) |
53 | | df-ne 3000 |
. . . . 5
⊢ (((𝐴 gcd 𝐵)↑2) ≠ 1 ↔ ¬ ((𝐴 gcd 𝐵)↑2) = 1) |
54 | 52, 53 | sylnib 320 |
. . . 4
⊢ ((𝜑 ∧ 𝐴 ≠ 0) → ¬ ¬ ((𝐴 gcd 𝐵)↑2) = 1) |
55 | 54 | notnotrd 131 |
. . 3
⊢ ((𝜑 ∧ 𝐴 ≠ 0) → ((𝐴 gcd 𝐵)↑2) = 1) |
56 | | nn0sqeq1 30049 |
. . 3
⊢ (((𝐴 gcd 𝐵) ∈ ℕ0 ∧ ((𝐴 gcd 𝐵)↑2) = 1) → (𝐴 gcd 𝐵) = 1) |
57 | 7, 55, 56 | syl2anc 579 |
. 2
⊢ ((𝜑 ∧ 𝐴 ≠ 0) → (𝐴 gcd 𝐵) = 1) |
58 | 5, 57 | mpdan 678 |
1
⊢ (𝜑 → (𝐴 gcd 𝐵) = 1) |