Step | Hyp | Ref
| Expression |
1 | | 2sqlem9.4 |
. . 3
⊢ (𝜑 → 𝑁 ∈ 𝑌) |
2 | | eqeq1 2743 |
. . . . . . . 8
⊢ (𝑧 = 𝑁 → (𝑧 = ((𝑥↑2) + (𝑦↑2)) ↔ 𝑁 = ((𝑥↑2) + (𝑦↑2)))) |
3 | 2 | anbi2d 632 |
. . . . . . 7
⊢ (𝑧 = 𝑁 → (((𝑥 gcd 𝑦) = 1 ∧ 𝑧 = ((𝑥↑2) + (𝑦↑2))) ↔ ((𝑥 gcd 𝑦) = 1 ∧ 𝑁 = ((𝑥↑2) + (𝑦↑2))))) |
4 | 3 | 2rexbidv 3211 |
. . . . . 6
⊢ (𝑧 = 𝑁 → (∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ ((𝑥 gcd 𝑦) = 1 ∧ 𝑧 = ((𝑥↑2) + (𝑦↑2))) ↔ ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ ((𝑥 gcd 𝑦) = 1 ∧ 𝑁 = ((𝑥↑2) + (𝑦↑2))))) |
5 | | oveq1 7190 |
. . . . . . . . 9
⊢ (𝑥 = 𝑢 → (𝑥 gcd 𝑦) = (𝑢 gcd 𝑦)) |
6 | 5 | eqeq1d 2741 |
. . . . . . . 8
⊢ (𝑥 = 𝑢 → ((𝑥 gcd 𝑦) = 1 ↔ (𝑢 gcd 𝑦) = 1)) |
7 | | oveq1 7190 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑢 → (𝑥↑2) = (𝑢↑2)) |
8 | 7 | oveq1d 7198 |
. . . . . . . . 9
⊢ (𝑥 = 𝑢 → ((𝑥↑2) + (𝑦↑2)) = ((𝑢↑2) + (𝑦↑2))) |
9 | 8 | eqeq2d 2750 |
. . . . . . . 8
⊢ (𝑥 = 𝑢 → (𝑁 = ((𝑥↑2) + (𝑦↑2)) ↔ 𝑁 = ((𝑢↑2) + (𝑦↑2)))) |
10 | 6, 9 | anbi12d 634 |
. . . . . . 7
⊢ (𝑥 = 𝑢 → (((𝑥 gcd 𝑦) = 1 ∧ 𝑁 = ((𝑥↑2) + (𝑦↑2))) ↔ ((𝑢 gcd 𝑦) = 1 ∧ 𝑁 = ((𝑢↑2) + (𝑦↑2))))) |
11 | | oveq2 7191 |
. . . . . . . . 9
⊢ (𝑦 = 𝑣 → (𝑢 gcd 𝑦) = (𝑢 gcd 𝑣)) |
12 | 11 | eqeq1d 2741 |
. . . . . . . 8
⊢ (𝑦 = 𝑣 → ((𝑢 gcd 𝑦) = 1 ↔ (𝑢 gcd 𝑣) = 1)) |
13 | | oveq1 7190 |
. . . . . . . . . 10
⊢ (𝑦 = 𝑣 → (𝑦↑2) = (𝑣↑2)) |
14 | 13 | oveq2d 7199 |
. . . . . . . . 9
⊢ (𝑦 = 𝑣 → ((𝑢↑2) + (𝑦↑2)) = ((𝑢↑2) + (𝑣↑2))) |
15 | 14 | eqeq2d 2750 |
. . . . . . . 8
⊢ (𝑦 = 𝑣 → (𝑁 = ((𝑢↑2) + (𝑦↑2)) ↔ 𝑁 = ((𝑢↑2) + (𝑣↑2)))) |
16 | 12, 15 | anbi12d 634 |
. . . . . . 7
⊢ (𝑦 = 𝑣 → (((𝑢 gcd 𝑦) = 1 ∧ 𝑁 = ((𝑢↑2) + (𝑦↑2))) ↔ ((𝑢 gcd 𝑣) = 1 ∧ 𝑁 = ((𝑢↑2) + (𝑣↑2))))) |
17 | 10, 16 | cbvrex2vw 3364 |
. . . . . 6
⊢
(∃𝑥 ∈
ℤ ∃𝑦 ∈
ℤ ((𝑥 gcd 𝑦) = 1 ∧ 𝑁 = ((𝑥↑2) + (𝑦↑2))) ↔ ∃𝑢 ∈ ℤ ∃𝑣 ∈ ℤ ((𝑢 gcd 𝑣) = 1 ∧ 𝑁 = ((𝑢↑2) + (𝑣↑2)))) |
18 | 4, 17 | bitrdi 290 |
. . . . 5
⊢ (𝑧 = 𝑁 → (∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ ((𝑥 gcd 𝑦) = 1 ∧ 𝑧 = ((𝑥↑2) + (𝑦↑2))) ↔ ∃𝑢 ∈ ℤ ∃𝑣 ∈ ℤ ((𝑢 gcd 𝑣) = 1 ∧ 𝑁 = ((𝑢↑2) + (𝑣↑2))))) |
19 | | 2sqlem7.2 |
. . . . 5
⊢ 𝑌 = {𝑧 ∣ ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ ((𝑥 gcd 𝑦) = 1 ∧ 𝑧 = ((𝑥↑2) + (𝑦↑2)))} |
20 | 18, 19 | elab2g 3580 |
. . . 4
⊢ (𝑁 ∈ 𝑌 → (𝑁 ∈ 𝑌 ↔ ∃𝑢 ∈ ℤ ∃𝑣 ∈ ℤ ((𝑢 gcd 𝑣) = 1 ∧ 𝑁 = ((𝑢↑2) + (𝑣↑2))))) |
21 | 20 | ibi 270 |
. . 3
⊢ (𝑁 ∈ 𝑌 → ∃𝑢 ∈ ℤ ∃𝑣 ∈ ℤ ((𝑢 gcd 𝑣) = 1 ∧ 𝑁 = ((𝑢↑2) + (𝑣↑2)))) |
22 | 1, 21 | syl 17 |
. 2
⊢ (𝜑 → ∃𝑢 ∈ ℤ ∃𝑣 ∈ ℤ ((𝑢 gcd 𝑣) = 1 ∧ 𝑁 = ((𝑢↑2) + (𝑣↑2)))) |
23 | | simpr 488 |
. . . . . 6
⊢ ((((𝜑 ∧ (𝑢 ∈ ℤ ∧ 𝑣 ∈ ℤ)) ∧ ((𝑢 gcd 𝑣) = 1 ∧ 𝑁 = ((𝑢↑2) + (𝑣↑2)))) ∧ 𝑀 = 1) → 𝑀 = 1) |
24 | | 1z 12106 |
. . . . . . . . 9
⊢ 1 ∈
ℤ |
25 | | zgz 16382 |
. . . . . . . . 9
⊢ (1 ∈
ℤ → 1 ∈ ℤ[i]) |
26 | 24, 25 | ax-mp 5 |
. . . . . . . 8
⊢ 1 ∈
ℤ[i] |
27 | | sq1 13663 |
. . . . . . . . 9
⊢
(1↑2) = 1 |
28 | 27 | eqcomi 2748 |
. . . . . . . 8
⊢ 1 =
(1↑2) |
29 | | fveq2 6687 |
. . . . . . . . . . 11
⊢ (𝑥 = 1 → (abs‘𝑥) =
(abs‘1)) |
30 | | abs1 14760 |
. . . . . . . . . . 11
⊢
(abs‘1) = 1 |
31 | 29, 30 | eqtrdi 2790 |
. . . . . . . . . 10
⊢ (𝑥 = 1 → (abs‘𝑥) = 1) |
32 | 31 | oveq1d 7198 |
. . . . . . . . 9
⊢ (𝑥 = 1 → ((abs‘𝑥)↑2) =
(1↑2)) |
33 | 32 | rspceeqv 3544 |
. . . . . . . 8
⊢ ((1
∈ ℤ[i] ∧ 1 = (1↑2)) → ∃𝑥 ∈ ℤ[i] 1 = ((abs‘𝑥)↑2)) |
34 | 26, 28, 33 | mp2an 692 |
. . . . . . 7
⊢
∃𝑥 ∈
ℤ[i] 1 = ((abs‘𝑥)↑2) |
35 | | 2sq.1 |
. . . . . . . 8
⊢ 𝑆 = ran (𝑤 ∈ ℤ[i] ↦ ((abs‘𝑤)↑2)) |
36 | 35 | 2sqlem1 26166 |
. . . . . . 7
⊢ (1 ∈
𝑆 ↔ ∃𝑥 ∈ ℤ[i] 1 =
((abs‘𝑥)↑2)) |
37 | 34, 36 | mpbir 234 |
. . . . . 6
⊢ 1 ∈
𝑆 |
38 | 23, 37 | eqeltrdi 2842 |
. . . . 5
⊢ ((((𝜑 ∧ (𝑢 ∈ ℤ ∧ 𝑣 ∈ ℤ)) ∧ ((𝑢 gcd 𝑣) = 1 ∧ 𝑁 = ((𝑢↑2) + (𝑣↑2)))) ∧ 𝑀 = 1) → 𝑀 ∈ 𝑆) |
39 | | 2sqlem9.5 |
. . . . . . . 8
⊢ (𝜑 → ∀𝑏 ∈ (1...(𝑀 − 1))∀𝑎 ∈ 𝑌 (𝑏 ∥ 𝑎 → 𝑏 ∈ 𝑆)) |
40 | 39 | ad2antrr 726 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑢 ∈ ℤ ∧ 𝑣 ∈ ℤ)) ∧ (((𝑢 gcd 𝑣) = 1 ∧ 𝑁 = ((𝑢↑2) + (𝑣↑2))) ∧ 𝑀 ≠ 1)) → ∀𝑏 ∈ (1...(𝑀 − 1))∀𝑎 ∈ 𝑌 (𝑏 ∥ 𝑎 → 𝑏 ∈ 𝑆)) |
41 | | 2sqlem9.7 |
. . . . . . . 8
⊢ (𝜑 → 𝑀 ∥ 𝑁) |
42 | 41 | ad2antrr 726 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑢 ∈ ℤ ∧ 𝑣 ∈ ℤ)) ∧ (((𝑢 gcd 𝑣) = 1 ∧ 𝑁 = ((𝑢↑2) + (𝑣↑2))) ∧ 𝑀 ≠ 1)) → 𝑀 ∥ 𝑁) |
43 | 35, 19 | 2sqlem7 26173 |
. . . . . . . . . 10
⊢ 𝑌 ⊆ (𝑆 ∩ ℕ) |
44 | | inss2 4130 |
. . . . . . . . . 10
⊢ (𝑆 ∩ ℕ) ⊆
ℕ |
45 | 43, 44 | sstri 3896 |
. . . . . . . . 9
⊢ 𝑌 ⊆
ℕ |
46 | 45, 1 | sseldi 3885 |
. . . . . . . 8
⊢ (𝜑 → 𝑁 ∈ ℕ) |
47 | 46 | ad2antrr 726 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑢 ∈ ℤ ∧ 𝑣 ∈ ℤ)) ∧ (((𝑢 gcd 𝑣) = 1 ∧ 𝑁 = ((𝑢↑2) + (𝑣↑2))) ∧ 𝑀 ≠ 1)) → 𝑁 ∈ ℕ) |
48 | | 2sqlem9.6 |
. . . . . . . . 9
⊢ (𝜑 → 𝑀 ∈ ℕ) |
49 | 48 | ad2antrr 726 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑢 ∈ ℤ ∧ 𝑣 ∈ ℤ)) ∧ (((𝑢 gcd 𝑣) = 1 ∧ 𝑁 = ((𝑢↑2) + (𝑣↑2))) ∧ 𝑀 ≠ 1)) → 𝑀 ∈ ℕ) |
50 | | simprr 773 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑢 ∈ ℤ ∧ 𝑣 ∈ ℤ)) ∧ (((𝑢 gcd 𝑣) = 1 ∧ 𝑁 = ((𝑢↑2) + (𝑣↑2))) ∧ 𝑀 ≠ 1)) → 𝑀 ≠ 1) |
51 | | eluz2b3 12417 |
. . . . . . . 8
⊢ (𝑀 ∈
(ℤ≥‘2) ↔ (𝑀 ∈ ℕ ∧ 𝑀 ≠ 1)) |
52 | 49, 50, 51 | sylanbrc 586 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑢 ∈ ℤ ∧ 𝑣 ∈ ℤ)) ∧ (((𝑢 gcd 𝑣) = 1 ∧ 𝑁 = ((𝑢↑2) + (𝑣↑2))) ∧ 𝑀 ≠ 1)) → 𝑀 ∈
(ℤ≥‘2)) |
53 | | simplrl 777 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑢 ∈ ℤ ∧ 𝑣 ∈ ℤ)) ∧ (((𝑢 gcd 𝑣) = 1 ∧ 𝑁 = ((𝑢↑2) + (𝑣↑2))) ∧ 𝑀 ≠ 1)) → 𝑢 ∈ ℤ) |
54 | | simplrr 778 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑢 ∈ ℤ ∧ 𝑣 ∈ ℤ)) ∧ (((𝑢 gcd 𝑣) = 1 ∧ 𝑁 = ((𝑢↑2) + (𝑣↑2))) ∧ 𝑀 ≠ 1)) → 𝑣 ∈ ℤ) |
55 | | simprll 779 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑢 ∈ ℤ ∧ 𝑣 ∈ ℤ)) ∧ (((𝑢 gcd 𝑣) = 1 ∧ 𝑁 = ((𝑢↑2) + (𝑣↑2))) ∧ 𝑀 ≠ 1)) → (𝑢 gcd 𝑣) = 1) |
56 | | simprlr 780 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑢 ∈ ℤ ∧ 𝑣 ∈ ℤ)) ∧ (((𝑢 gcd 𝑣) = 1 ∧ 𝑁 = ((𝑢↑2) + (𝑣↑2))) ∧ 𝑀 ≠ 1)) → 𝑁 = ((𝑢↑2) + (𝑣↑2))) |
57 | | eqid 2739 |
. . . . . . 7
⊢ (((𝑢 + (𝑀 / 2)) mod 𝑀) − (𝑀 / 2)) = (((𝑢 + (𝑀 / 2)) mod 𝑀) − (𝑀 / 2)) |
58 | | eqid 2739 |
. . . . . . 7
⊢ (((𝑣 + (𝑀 / 2)) mod 𝑀) − (𝑀 / 2)) = (((𝑣 + (𝑀 / 2)) mod 𝑀) − (𝑀 / 2)) |
59 | | eqid 2739 |
. . . . . . 7
⊢ ((((𝑢 + (𝑀 / 2)) mod 𝑀) − (𝑀 / 2)) / ((((𝑢 + (𝑀 / 2)) mod 𝑀) − (𝑀 / 2)) gcd (((𝑣 + (𝑀 / 2)) mod 𝑀) − (𝑀 / 2)))) = ((((𝑢 + (𝑀 / 2)) mod 𝑀) − (𝑀 / 2)) / ((((𝑢 + (𝑀 / 2)) mod 𝑀) − (𝑀 / 2)) gcd (((𝑣 + (𝑀 / 2)) mod 𝑀) − (𝑀 / 2)))) |
60 | | eqid 2739 |
. . . . . . 7
⊢ ((((𝑣 + (𝑀 / 2)) mod 𝑀) − (𝑀 / 2)) / ((((𝑢 + (𝑀 / 2)) mod 𝑀) − (𝑀 / 2)) gcd (((𝑣 + (𝑀 / 2)) mod 𝑀) − (𝑀 / 2)))) = ((((𝑣 + (𝑀 / 2)) mod 𝑀) − (𝑀 / 2)) / ((((𝑢 + (𝑀 / 2)) mod 𝑀) − (𝑀 / 2)) gcd (((𝑣 + (𝑀 / 2)) mod 𝑀) − (𝑀 / 2)))) |
61 | 35, 19, 40, 42, 47, 52, 53, 54, 55, 56, 57, 58, 59, 60 | 2sqlem8 26175 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑢 ∈ ℤ ∧ 𝑣 ∈ ℤ)) ∧ (((𝑢 gcd 𝑣) = 1 ∧ 𝑁 = ((𝑢↑2) + (𝑣↑2))) ∧ 𝑀 ≠ 1)) → 𝑀 ∈ 𝑆) |
62 | 61 | anassrs 471 |
. . . . 5
⊢ ((((𝜑 ∧ (𝑢 ∈ ℤ ∧ 𝑣 ∈ ℤ)) ∧ ((𝑢 gcd 𝑣) = 1 ∧ 𝑁 = ((𝑢↑2) + (𝑣↑2)))) ∧ 𝑀 ≠ 1) → 𝑀 ∈ 𝑆) |
63 | 38, 62 | pm2.61dane 3022 |
. . . 4
⊢ (((𝜑 ∧ (𝑢 ∈ ℤ ∧ 𝑣 ∈ ℤ)) ∧ ((𝑢 gcd 𝑣) = 1 ∧ 𝑁 = ((𝑢↑2) + (𝑣↑2)))) → 𝑀 ∈ 𝑆) |
64 | 63 | ex 416 |
. . 3
⊢ ((𝜑 ∧ (𝑢 ∈ ℤ ∧ 𝑣 ∈ ℤ)) → (((𝑢 gcd 𝑣) = 1 ∧ 𝑁 = ((𝑢↑2) + (𝑣↑2))) → 𝑀 ∈ 𝑆)) |
65 | 64 | rexlimdvva 3205 |
. 2
⊢ (𝜑 → (∃𝑢 ∈ ℤ ∃𝑣 ∈ ℤ ((𝑢 gcd 𝑣) = 1 ∧ 𝑁 = ((𝑢↑2) + (𝑣↑2))) → 𝑀 ∈ 𝑆)) |
66 | 22, 65 | mpd 15 |
1
⊢ (𝜑 → 𝑀 ∈ 𝑆) |