Step | Hyp | Ref
| Expression |
1 | | 2sqlem9.4 |
. . 3
⊢ (𝜑 → 𝑁 ∈ 𝑌) |
2 | | eqeq1 2614 |
. . . . . . . 8
⊢ (𝑧 = 𝑁 → (𝑧 = ((𝑥↑2) + (𝑦↑2)) ↔ 𝑁 = ((𝑥↑2) + (𝑦↑2)))) |
3 | 2 | anbi2d 736 |
. . . . . . 7
⊢ (𝑧 = 𝑁 → (((𝑥 gcd 𝑦) = 1 ∧ 𝑧 = ((𝑥↑2) + (𝑦↑2))) ↔ ((𝑥 gcd 𝑦) = 1 ∧ 𝑁 = ((𝑥↑2) + (𝑦↑2))))) |
4 | 3 | 2rexbidv 3039 |
. . . . . 6
⊢ (𝑧 = 𝑁 → (∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ ((𝑥 gcd 𝑦) = 1 ∧ 𝑧 = ((𝑥↑2) + (𝑦↑2))) ↔ ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ ((𝑥 gcd 𝑦) = 1 ∧ 𝑁 = ((𝑥↑2) + (𝑦↑2))))) |
5 | | oveq1 6556 |
. . . . . . . . 9
⊢ (𝑥 = 𝑢 → (𝑥 gcd 𝑦) = (𝑢 gcd 𝑦)) |
6 | 5 | eqeq1d 2612 |
. . . . . . . 8
⊢ (𝑥 = 𝑢 → ((𝑥 gcd 𝑦) = 1 ↔ (𝑢 gcd 𝑦) = 1)) |
7 | | oveq1 6556 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑢 → (𝑥↑2) = (𝑢↑2)) |
8 | 7 | oveq1d 6564 |
. . . . . . . . 9
⊢ (𝑥 = 𝑢 → ((𝑥↑2) + (𝑦↑2)) = ((𝑢↑2) + (𝑦↑2))) |
9 | 8 | eqeq2d 2620 |
. . . . . . . 8
⊢ (𝑥 = 𝑢 → (𝑁 = ((𝑥↑2) + (𝑦↑2)) ↔ 𝑁 = ((𝑢↑2) + (𝑦↑2)))) |
10 | 6, 9 | anbi12d 743 |
. . . . . . 7
⊢ (𝑥 = 𝑢 → (((𝑥 gcd 𝑦) = 1 ∧ 𝑁 = ((𝑥↑2) + (𝑦↑2))) ↔ ((𝑢 gcd 𝑦) = 1 ∧ 𝑁 = ((𝑢↑2) + (𝑦↑2))))) |
11 | | oveq2 6557 |
. . . . . . . . 9
⊢ (𝑦 = 𝑣 → (𝑢 gcd 𝑦) = (𝑢 gcd 𝑣)) |
12 | 11 | eqeq1d 2612 |
. . . . . . . 8
⊢ (𝑦 = 𝑣 → ((𝑢 gcd 𝑦) = 1 ↔ (𝑢 gcd 𝑣) = 1)) |
13 | | oveq1 6556 |
. . . . . . . . . 10
⊢ (𝑦 = 𝑣 → (𝑦↑2) = (𝑣↑2)) |
14 | 13 | oveq2d 6565 |
. . . . . . . . 9
⊢ (𝑦 = 𝑣 → ((𝑢↑2) + (𝑦↑2)) = ((𝑢↑2) + (𝑣↑2))) |
15 | 14 | eqeq2d 2620 |
. . . . . . . 8
⊢ (𝑦 = 𝑣 → (𝑁 = ((𝑢↑2) + (𝑦↑2)) ↔ 𝑁 = ((𝑢↑2) + (𝑣↑2)))) |
16 | 12, 15 | anbi12d 743 |
. . . . . . 7
⊢ (𝑦 = 𝑣 → (((𝑢 gcd 𝑦) = 1 ∧ 𝑁 = ((𝑢↑2) + (𝑦↑2))) ↔ ((𝑢 gcd 𝑣) = 1 ∧ 𝑁 = ((𝑢↑2) + (𝑣↑2))))) |
17 | 10, 16 | cbvrex2v 3156 |
. . . . . 6
⊢
(∃𝑥 ∈
ℤ ∃𝑦 ∈
ℤ ((𝑥 gcd 𝑦) = 1 ∧ 𝑁 = ((𝑥↑2) + (𝑦↑2))) ↔ ∃𝑢 ∈ ℤ ∃𝑣 ∈ ℤ ((𝑢 gcd 𝑣) = 1 ∧ 𝑁 = ((𝑢↑2) + (𝑣↑2)))) |
18 | 4, 17 | syl6bb 275 |
. . . . 5
⊢ (𝑧 = 𝑁 → (∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ ((𝑥 gcd 𝑦) = 1 ∧ 𝑧 = ((𝑥↑2) + (𝑦↑2))) ↔ ∃𝑢 ∈ ℤ ∃𝑣 ∈ ℤ ((𝑢 gcd 𝑣) = 1 ∧ 𝑁 = ((𝑢↑2) + (𝑣↑2))))) |
19 | | 2sqlem7.2 |
. . . . 5
⊢ 𝑌 = {𝑧 ∣ ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ ((𝑥 gcd 𝑦) = 1 ∧ 𝑧 = ((𝑥↑2) + (𝑦↑2)))} |
20 | 18, 19 | elab2g 3322 |
. . . 4
⊢ (𝑁 ∈ 𝑌 → (𝑁 ∈ 𝑌 ↔ ∃𝑢 ∈ ℤ ∃𝑣 ∈ ℤ ((𝑢 gcd 𝑣) = 1 ∧ 𝑁 = ((𝑢↑2) + (𝑣↑2))))) |
21 | 20 | ibi 255 |
. . 3
⊢ (𝑁 ∈ 𝑌 → ∃𝑢 ∈ ℤ ∃𝑣 ∈ ℤ ((𝑢 gcd 𝑣) = 1 ∧ 𝑁 = ((𝑢↑2) + (𝑣↑2)))) |
22 | 1, 21 | syl 17 |
. 2
⊢ (𝜑 → ∃𝑢 ∈ ℤ ∃𝑣 ∈ ℤ ((𝑢 gcd 𝑣) = 1 ∧ 𝑁 = ((𝑢↑2) + (𝑣↑2)))) |
23 | | simpr 476 |
. . . . . 6
⊢ ((((𝜑 ∧ (𝑢 ∈ ℤ ∧ 𝑣 ∈ ℤ)) ∧ ((𝑢 gcd 𝑣) = 1 ∧ 𝑁 = ((𝑢↑2) + (𝑣↑2)))) ∧ 𝑀 = 1) → 𝑀 = 1) |
24 | | 1z 11284 |
. . . . . . . . 9
⊢ 1 ∈
ℤ |
25 | | zgz 15475 |
. . . . . . . . 9
⊢ (1 ∈
ℤ → 1 ∈ ℤ[i]) |
26 | 24, 25 | ax-mp 5 |
. . . . . . . 8
⊢ 1 ∈
ℤ[i] |
27 | | sq1 12820 |
. . . . . . . . 9
⊢
(1↑2) = 1 |
28 | 27 | eqcomi 2619 |
. . . . . . . 8
⊢ 1 =
(1↑2) |
29 | | fveq2 6103 |
. . . . . . . . . . . 12
⊢ (𝑥 = 1 → (abs‘𝑥) =
(abs‘1)) |
30 | | abs1 13885 |
. . . . . . . . . . . 12
⊢
(abs‘1) = 1 |
31 | 29, 30 | syl6eq 2660 |
. . . . . . . . . . 11
⊢ (𝑥 = 1 → (abs‘𝑥) = 1) |
32 | 31 | oveq1d 6564 |
. . . . . . . . . 10
⊢ (𝑥 = 1 → ((abs‘𝑥)↑2) =
(1↑2)) |
33 | 32 | eqeq2d 2620 |
. . . . . . . . 9
⊢ (𝑥 = 1 → (1 =
((abs‘𝑥)↑2)
↔ 1 = (1↑2))) |
34 | 33 | rspcev 3282 |
. . . . . . . 8
⊢ ((1
∈ ℤ[i] ∧ 1 = (1↑2)) → ∃𝑥 ∈ ℤ[i] 1 = ((abs‘𝑥)↑2)) |
35 | 26, 28, 34 | mp2an 704 |
. . . . . . 7
⊢
∃𝑥 ∈
ℤ[i] 1 = ((abs‘𝑥)↑2) |
36 | | 2sq.1 |
. . . . . . . 8
⊢ 𝑆 = ran (𝑤 ∈ ℤ[i] ↦ ((abs‘𝑤)↑2)) |
37 | 36 | 2sqlem1 24942 |
. . . . . . 7
⊢ (1 ∈
𝑆 ↔ ∃𝑥 ∈ ℤ[i] 1 =
((abs‘𝑥)↑2)) |
38 | 35, 37 | mpbir 220 |
. . . . . 6
⊢ 1 ∈
𝑆 |
39 | 23, 38 | syl6eqel 2696 |
. . . . 5
⊢ ((((𝜑 ∧ (𝑢 ∈ ℤ ∧ 𝑣 ∈ ℤ)) ∧ ((𝑢 gcd 𝑣) = 1 ∧ 𝑁 = ((𝑢↑2) + (𝑣↑2)))) ∧ 𝑀 = 1) → 𝑀 ∈ 𝑆) |
40 | | 2sqlem9.5 |
. . . . . . . 8
⊢ (𝜑 → ∀𝑏 ∈ (1...(𝑀 − 1))∀𝑎 ∈ 𝑌 (𝑏 ∥ 𝑎 → 𝑏 ∈ 𝑆)) |
41 | 40 | ad2antrr 758 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑢 ∈ ℤ ∧ 𝑣 ∈ ℤ)) ∧ (((𝑢 gcd 𝑣) = 1 ∧ 𝑁 = ((𝑢↑2) + (𝑣↑2))) ∧ 𝑀 ≠ 1)) → ∀𝑏 ∈ (1...(𝑀 − 1))∀𝑎 ∈ 𝑌 (𝑏 ∥ 𝑎 → 𝑏 ∈ 𝑆)) |
42 | | 2sqlem9.7 |
. . . . . . . 8
⊢ (𝜑 → 𝑀 ∥ 𝑁) |
43 | 42 | ad2antrr 758 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑢 ∈ ℤ ∧ 𝑣 ∈ ℤ)) ∧ (((𝑢 gcd 𝑣) = 1 ∧ 𝑁 = ((𝑢↑2) + (𝑣↑2))) ∧ 𝑀 ≠ 1)) → 𝑀 ∥ 𝑁) |
44 | 36, 19 | 2sqlem7 24949 |
. . . . . . . . . 10
⊢ 𝑌 ⊆ (𝑆 ∩ ℕ) |
45 | | inss2 3796 |
. . . . . . . . . 10
⊢ (𝑆 ∩ ℕ) ⊆
ℕ |
46 | 44, 45 | sstri 3577 |
. . . . . . . . 9
⊢ 𝑌 ⊆
ℕ |
47 | 46, 1 | sseldi 3566 |
. . . . . . . 8
⊢ (𝜑 → 𝑁 ∈ ℕ) |
48 | 47 | ad2antrr 758 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑢 ∈ ℤ ∧ 𝑣 ∈ ℤ)) ∧ (((𝑢 gcd 𝑣) = 1 ∧ 𝑁 = ((𝑢↑2) + (𝑣↑2))) ∧ 𝑀 ≠ 1)) → 𝑁 ∈ ℕ) |
49 | | 2sqlem9.6 |
. . . . . . . . 9
⊢ (𝜑 → 𝑀 ∈ ℕ) |
50 | 49 | ad2antrr 758 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑢 ∈ ℤ ∧ 𝑣 ∈ ℤ)) ∧ (((𝑢 gcd 𝑣) = 1 ∧ 𝑁 = ((𝑢↑2) + (𝑣↑2))) ∧ 𝑀 ≠ 1)) → 𝑀 ∈ ℕ) |
51 | | simprr 792 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑢 ∈ ℤ ∧ 𝑣 ∈ ℤ)) ∧ (((𝑢 gcd 𝑣) = 1 ∧ 𝑁 = ((𝑢↑2) + (𝑣↑2))) ∧ 𝑀 ≠ 1)) → 𝑀 ≠ 1) |
52 | | eluz2b3 11638 |
. . . . . . . 8
⊢ (𝑀 ∈
(ℤ≥‘2) ↔ (𝑀 ∈ ℕ ∧ 𝑀 ≠ 1)) |
53 | 50, 51, 52 | sylanbrc 695 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑢 ∈ ℤ ∧ 𝑣 ∈ ℤ)) ∧ (((𝑢 gcd 𝑣) = 1 ∧ 𝑁 = ((𝑢↑2) + (𝑣↑2))) ∧ 𝑀 ≠ 1)) → 𝑀 ∈
(ℤ≥‘2)) |
54 | | simplrl 796 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑢 ∈ ℤ ∧ 𝑣 ∈ ℤ)) ∧ (((𝑢 gcd 𝑣) = 1 ∧ 𝑁 = ((𝑢↑2) + (𝑣↑2))) ∧ 𝑀 ≠ 1)) → 𝑢 ∈ ℤ) |
55 | | simplrr 797 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑢 ∈ ℤ ∧ 𝑣 ∈ ℤ)) ∧ (((𝑢 gcd 𝑣) = 1 ∧ 𝑁 = ((𝑢↑2) + (𝑣↑2))) ∧ 𝑀 ≠ 1)) → 𝑣 ∈ ℤ) |
56 | | simprll 798 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑢 ∈ ℤ ∧ 𝑣 ∈ ℤ)) ∧ (((𝑢 gcd 𝑣) = 1 ∧ 𝑁 = ((𝑢↑2) + (𝑣↑2))) ∧ 𝑀 ≠ 1)) → (𝑢 gcd 𝑣) = 1) |
57 | | simprlr 799 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑢 ∈ ℤ ∧ 𝑣 ∈ ℤ)) ∧ (((𝑢 gcd 𝑣) = 1 ∧ 𝑁 = ((𝑢↑2) + (𝑣↑2))) ∧ 𝑀 ≠ 1)) → 𝑁 = ((𝑢↑2) + (𝑣↑2))) |
58 | | eqid 2610 |
. . . . . . 7
⊢ (((𝑢 + (𝑀 / 2)) mod 𝑀) − (𝑀 / 2)) = (((𝑢 + (𝑀 / 2)) mod 𝑀) − (𝑀 / 2)) |
59 | | eqid 2610 |
. . . . . . 7
⊢ (((𝑣 + (𝑀 / 2)) mod 𝑀) − (𝑀 / 2)) = (((𝑣 + (𝑀 / 2)) mod 𝑀) − (𝑀 / 2)) |
60 | | eqid 2610 |
. . . . . . 7
⊢ ((((𝑢 + (𝑀 / 2)) mod 𝑀) − (𝑀 / 2)) / ((((𝑢 + (𝑀 / 2)) mod 𝑀) − (𝑀 / 2)) gcd (((𝑣 + (𝑀 / 2)) mod 𝑀) − (𝑀 / 2)))) = ((((𝑢 + (𝑀 / 2)) mod 𝑀) − (𝑀 / 2)) / ((((𝑢 + (𝑀 / 2)) mod 𝑀) − (𝑀 / 2)) gcd (((𝑣 + (𝑀 / 2)) mod 𝑀) − (𝑀 / 2)))) |
61 | | eqid 2610 |
. . . . . . 7
⊢ ((((𝑣 + (𝑀 / 2)) mod 𝑀) − (𝑀 / 2)) / ((((𝑢 + (𝑀 / 2)) mod 𝑀) − (𝑀 / 2)) gcd (((𝑣 + (𝑀 / 2)) mod 𝑀) − (𝑀 / 2)))) = ((((𝑣 + (𝑀 / 2)) mod 𝑀) − (𝑀 / 2)) / ((((𝑢 + (𝑀 / 2)) mod 𝑀) − (𝑀 / 2)) gcd (((𝑣 + (𝑀 / 2)) mod 𝑀) − (𝑀 / 2)))) |
62 | 36, 19, 41, 43, 48, 53, 54, 55, 56, 57, 58, 59, 60, 61 | 2sqlem8 24951 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑢 ∈ ℤ ∧ 𝑣 ∈ ℤ)) ∧ (((𝑢 gcd 𝑣) = 1 ∧ 𝑁 = ((𝑢↑2) + (𝑣↑2))) ∧ 𝑀 ≠ 1)) → 𝑀 ∈ 𝑆) |
63 | 62 | anassrs 678 |
. . . . 5
⊢ ((((𝜑 ∧ (𝑢 ∈ ℤ ∧ 𝑣 ∈ ℤ)) ∧ ((𝑢 gcd 𝑣) = 1 ∧ 𝑁 = ((𝑢↑2) + (𝑣↑2)))) ∧ 𝑀 ≠ 1) → 𝑀 ∈ 𝑆) |
64 | 39, 63 | pm2.61dane 2869 |
. . . 4
⊢ (((𝜑 ∧ (𝑢 ∈ ℤ ∧ 𝑣 ∈ ℤ)) ∧ ((𝑢 gcd 𝑣) = 1 ∧ 𝑁 = ((𝑢↑2) + (𝑣↑2)))) → 𝑀 ∈ 𝑆) |
65 | 64 | ex 449 |
. . 3
⊢ ((𝜑 ∧ (𝑢 ∈ ℤ ∧ 𝑣 ∈ ℤ)) → (((𝑢 gcd 𝑣) = 1 ∧ 𝑁 = ((𝑢↑2) + (𝑣↑2))) → 𝑀 ∈ 𝑆)) |
66 | 65 | rexlimdvva 3020 |
. 2
⊢ (𝜑 → (∃𝑢 ∈ ℤ ∃𝑣 ∈ ℤ ((𝑢 gcd 𝑣) = 1 ∧ 𝑁 = ((𝑢↑2) + (𝑣↑2))) → 𝑀 ∈ 𝑆)) |
67 | 22, 66 | mpd 15 |
1
⊢ (𝜑 → 𝑀 ∈ 𝑆) |