| Step | Hyp | Ref
| Expression |
| 1 | | 2sq.1 |
. . . 4
⊢ 𝑆 = ran (𝑤 ∈ ℤ[i] ↦ ((abs‘𝑤)↑2)) |
| 2 | 1 | 2sqlem1 27461 |
. . 3
⊢ (𝐴 ∈ 𝑆 ↔ ∃𝑧 ∈ ℤ[i] 𝐴 = ((abs‘𝑧)↑2)) |
| 3 | | elgz 16969 |
. . . . . . 7
⊢ (𝑧 ∈ ℤ[i] ↔ (𝑧 ∈ ℂ ∧
(ℜ‘𝑧) ∈
ℤ ∧ (ℑ‘𝑧) ∈ ℤ)) |
| 4 | 3 | simp2bi 1147 |
. . . . . 6
⊢ (𝑧 ∈ ℤ[i] →
(ℜ‘𝑧) ∈
ℤ) |
| 5 | 3 | simp3bi 1148 |
. . . . . 6
⊢ (𝑧 ∈ ℤ[i] →
(ℑ‘𝑧) ∈
ℤ) |
| 6 | | gzcn 16970 |
. . . . . . 7
⊢ (𝑧 ∈ ℤ[i] → 𝑧 ∈
ℂ) |
| 7 | 6 | absvalsq2d 15482 |
. . . . . 6
⊢ (𝑧 ∈ ℤ[i] →
((abs‘𝑧)↑2) =
(((ℜ‘𝑧)↑2)
+ ((ℑ‘𝑧)↑2))) |
| 8 | | oveq1 7438 |
. . . . . . . . 9
⊢ (𝑥 = (ℜ‘𝑧) → (𝑥↑2) = ((ℜ‘𝑧)↑2)) |
| 9 | 8 | oveq1d 7446 |
. . . . . . . 8
⊢ (𝑥 = (ℜ‘𝑧) → ((𝑥↑2) + (𝑦↑2)) = (((ℜ‘𝑧)↑2) + (𝑦↑2))) |
| 10 | 9 | eqeq2d 2748 |
. . . . . . 7
⊢ (𝑥 = (ℜ‘𝑧) → (((abs‘𝑧)↑2) = ((𝑥↑2) + (𝑦↑2)) ↔ ((abs‘𝑧)↑2) =
(((ℜ‘𝑧)↑2)
+ (𝑦↑2)))) |
| 11 | | oveq1 7438 |
. . . . . . . . 9
⊢ (𝑦 = (ℑ‘𝑧) → (𝑦↑2) = ((ℑ‘𝑧)↑2)) |
| 12 | 11 | oveq2d 7447 |
. . . . . . . 8
⊢ (𝑦 = (ℑ‘𝑧) → (((ℜ‘𝑧)↑2) + (𝑦↑2)) = (((ℜ‘𝑧)↑2) +
((ℑ‘𝑧)↑2))) |
| 13 | 12 | eqeq2d 2748 |
. . . . . . 7
⊢ (𝑦 = (ℑ‘𝑧) → (((abs‘𝑧)↑2) =
(((ℜ‘𝑧)↑2)
+ (𝑦↑2)) ↔
((abs‘𝑧)↑2) =
(((ℜ‘𝑧)↑2)
+ ((ℑ‘𝑧)↑2)))) |
| 14 | 10, 13 | rspc2ev 3635 |
. . . . . 6
⊢
(((ℜ‘𝑧)
∈ ℤ ∧ (ℑ‘𝑧) ∈ ℤ ∧ ((abs‘𝑧)↑2) =
(((ℜ‘𝑧)↑2)
+ ((ℑ‘𝑧)↑2))) → ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ ((abs‘𝑧)↑2) = ((𝑥↑2) + (𝑦↑2))) |
| 15 | 4, 5, 7, 14 | syl3anc 1373 |
. . . . 5
⊢ (𝑧 ∈ ℤ[i] →
∃𝑥 ∈ ℤ
∃𝑦 ∈ ℤ
((abs‘𝑧)↑2) =
((𝑥↑2) + (𝑦↑2))) |
| 16 | | eqeq1 2741 |
. . . . . 6
⊢ (𝐴 = ((abs‘𝑧)↑2) → (𝐴 = ((𝑥↑2) + (𝑦↑2)) ↔ ((abs‘𝑧)↑2) = ((𝑥↑2) + (𝑦↑2)))) |
| 17 | 16 | 2rexbidv 3222 |
. . . . 5
⊢ (𝐴 = ((abs‘𝑧)↑2) → (∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ 𝐴 = ((𝑥↑2) + (𝑦↑2)) ↔ ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ ((abs‘𝑧)↑2) = ((𝑥↑2) + (𝑦↑2)))) |
| 18 | 15, 17 | syl5ibrcom 247 |
. . . 4
⊢ (𝑧 ∈ ℤ[i] → (𝐴 = ((abs‘𝑧)↑2) → ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ 𝐴 = ((𝑥↑2) + (𝑦↑2)))) |
| 19 | 18 | rexlimiv 3148 |
. . 3
⊢
(∃𝑧 ∈
ℤ[i] 𝐴 =
((abs‘𝑧)↑2)
→ ∃𝑥 ∈
ℤ ∃𝑦 ∈
ℤ 𝐴 = ((𝑥↑2) + (𝑦↑2))) |
| 20 | 2, 19 | sylbi 217 |
. 2
⊢ (𝐴 ∈ 𝑆 → ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ 𝐴 = ((𝑥↑2) + (𝑦↑2))) |
| 21 | | gzreim 16977 |
. . . . . 6
⊢ ((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) → (𝑥 + (i · 𝑦)) ∈
ℤ[i]) |
| 22 | | zcn 12618 |
. . . . . . . . 9
⊢ (𝑥 ∈ ℤ → 𝑥 ∈
ℂ) |
| 23 | | ax-icn 11214 |
. . . . . . . . . 10
⊢ i ∈
ℂ |
| 24 | | zcn 12618 |
. . . . . . . . . 10
⊢ (𝑦 ∈ ℤ → 𝑦 ∈
ℂ) |
| 25 | | mulcl 11239 |
. . . . . . . . . 10
⊢ ((i
∈ ℂ ∧ 𝑦
∈ ℂ) → (i · 𝑦) ∈ ℂ) |
| 26 | 23, 24, 25 | sylancr 587 |
. . . . . . . . 9
⊢ (𝑦 ∈ ℤ → (i
· 𝑦) ∈
ℂ) |
| 27 | | addcl 11237 |
. . . . . . . . 9
⊢ ((𝑥 ∈ ℂ ∧ (i
· 𝑦) ∈ ℂ)
→ (𝑥 + (i ·
𝑦)) ∈
ℂ) |
| 28 | 22, 26, 27 | syl2an 596 |
. . . . . . . 8
⊢ ((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) → (𝑥 + (i · 𝑦)) ∈
ℂ) |
| 29 | 28 | absvalsq2d 15482 |
. . . . . . 7
⊢ ((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) →
((abs‘(𝑥 + (i
· 𝑦)))↑2) =
(((ℜ‘(𝑥 + (i
· 𝑦)))↑2) +
((ℑ‘(𝑥 + (i
· 𝑦)))↑2))) |
| 30 | | zre 12617 |
. . . . . . . . . 10
⊢ (𝑥 ∈ ℤ → 𝑥 ∈
ℝ) |
| 31 | | zre 12617 |
. . . . . . . . . 10
⊢ (𝑦 ∈ ℤ → 𝑦 ∈
ℝ) |
| 32 | | crre 15153 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) →
(ℜ‘(𝑥 + (i
· 𝑦))) = 𝑥) |
| 33 | 30, 31, 32 | syl2an 596 |
. . . . . . . . 9
⊢ ((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) →
(ℜ‘(𝑥 + (i
· 𝑦))) = 𝑥) |
| 34 | 33 | oveq1d 7446 |
. . . . . . . 8
⊢ ((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) →
((ℜ‘(𝑥 + (i
· 𝑦)))↑2) =
(𝑥↑2)) |
| 35 | | crim 15154 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) →
(ℑ‘(𝑥 + (i
· 𝑦))) = 𝑦) |
| 36 | 30, 31, 35 | syl2an 596 |
. . . . . . . . 9
⊢ ((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) →
(ℑ‘(𝑥 + (i
· 𝑦))) = 𝑦) |
| 37 | 36 | oveq1d 7446 |
. . . . . . . 8
⊢ ((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) →
((ℑ‘(𝑥 + (i
· 𝑦)))↑2) =
(𝑦↑2)) |
| 38 | 34, 37 | oveq12d 7449 |
. . . . . . 7
⊢ ((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) →
(((ℜ‘(𝑥 + (i
· 𝑦)))↑2) +
((ℑ‘(𝑥 + (i
· 𝑦)))↑2)) =
((𝑥↑2) + (𝑦↑2))) |
| 39 | 29, 38 | eqtr2d 2778 |
. . . . . 6
⊢ ((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) → ((𝑥↑2) + (𝑦↑2)) = ((abs‘(𝑥 + (i · 𝑦)))↑2)) |
| 40 | | fveq2 6906 |
. . . . . . . 8
⊢ (𝑧 = (𝑥 + (i · 𝑦)) → (abs‘𝑧) = (abs‘(𝑥 + (i · 𝑦)))) |
| 41 | 40 | oveq1d 7446 |
. . . . . . 7
⊢ (𝑧 = (𝑥 + (i · 𝑦)) → ((abs‘𝑧)↑2) = ((abs‘(𝑥 + (i · 𝑦)))↑2)) |
| 42 | 41 | rspceeqv 3645 |
. . . . . 6
⊢ (((𝑥 + (i · 𝑦)) ∈ ℤ[i] ∧
((𝑥↑2) + (𝑦↑2)) = ((abs‘(𝑥 + (i · 𝑦)))↑2)) → ∃𝑧 ∈ ℤ[i] ((𝑥↑2) + (𝑦↑2)) = ((abs‘𝑧)↑2)) |
| 43 | 21, 39, 42 | syl2anc 584 |
. . . . 5
⊢ ((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) →
∃𝑧 ∈ ℤ[i]
((𝑥↑2) + (𝑦↑2)) = ((abs‘𝑧)↑2)) |
| 44 | 1 | 2sqlem1 27461 |
. . . . 5
⊢ (((𝑥↑2) + (𝑦↑2)) ∈ 𝑆 ↔ ∃𝑧 ∈ ℤ[i] ((𝑥↑2) + (𝑦↑2)) = ((abs‘𝑧)↑2)) |
| 45 | 43, 44 | sylibr 234 |
. . . 4
⊢ ((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) → ((𝑥↑2) + (𝑦↑2)) ∈ 𝑆) |
| 46 | | eleq1 2829 |
. . . 4
⊢ (𝐴 = ((𝑥↑2) + (𝑦↑2)) → (𝐴 ∈ 𝑆 ↔ ((𝑥↑2) + (𝑦↑2)) ∈ 𝑆)) |
| 47 | 45, 46 | syl5ibrcom 247 |
. . 3
⊢ ((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) → (𝐴 = ((𝑥↑2) + (𝑦↑2)) → 𝐴 ∈ 𝑆)) |
| 48 | 47 | rexlimivv 3201 |
. 2
⊢
(∃𝑥 ∈
ℤ ∃𝑦 ∈
ℤ 𝐴 = ((𝑥↑2) + (𝑦↑2)) → 𝐴 ∈ 𝑆) |
| 49 | 20, 48 | impbii 209 |
1
⊢ (𝐴 ∈ 𝑆 ↔ ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ 𝐴 = ((𝑥↑2) + (𝑦↑2))) |