| Step | Hyp | Ref
| Expression |
| 1 | | 4sq.1 |
. . . 4
⊢ 𝑆 = {𝑛 ∣ ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ ∃𝑧 ∈ ℤ ∃𝑤 ∈ ℤ 𝑛 = (((𝑥↑2) + (𝑦↑2)) + ((𝑧↑2) + (𝑤↑2)))} |
| 2 | 1 | 4sqlem2 16987 |
. . 3
⊢ (𝐴 ∈ 𝑆 ↔ ∃𝑎 ∈ ℤ ∃𝑏 ∈ ℤ ∃𝑐 ∈ ℤ ∃𝑑 ∈ ℤ 𝐴 = (((𝑎↑2) + (𝑏↑2)) + ((𝑐↑2) + (𝑑↑2)))) |
| 3 | | gzreim 16977 |
. . . . . . . 8
⊢ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) → (𝑎 + (i · 𝑏)) ∈
ℤ[i]) |
| 4 | 3 | adantr 480 |
. . . . . . 7
⊢ (((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) ∧ (𝑐 ∈ ℤ ∧ 𝑑 ∈ ℤ)) → (𝑎 + (i · 𝑏)) ∈
ℤ[i]) |
| 5 | | gzreim 16977 |
. . . . . . . 8
⊢ ((𝑐 ∈ ℤ ∧ 𝑑 ∈ ℤ) → (𝑐 + (i · 𝑑)) ∈
ℤ[i]) |
| 6 | 5 | adantl 481 |
. . . . . . 7
⊢ (((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) ∧ (𝑐 ∈ ℤ ∧ 𝑑 ∈ ℤ)) → (𝑐 + (i · 𝑑)) ∈
ℤ[i]) |
| 7 | | gzcn 16970 |
. . . . . . . . . . . 12
⊢ ((𝑎 + (i · 𝑏)) ∈ ℤ[i] →
(𝑎 + (i · 𝑏)) ∈
ℂ) |
| 8 | 3, 7 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) → (𝑎 + (i · 𝑏)) ∈
ℂ) |
| 9 | 8 | absvalsq2d 15482 |
. . . . . . . . . 10
⊢ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) →
((abs‘(𝑎 + (i
· 𝑏)))↑2) =
(((ℜ‘(𝑎 + (i
· 𝑏)))↑2) +
((ℑ‘(𝑎 + (i
· 𝑏)))↑2))) |
| 10 | | zre 12617 |
. . . . . . . . . . . . 13
⊢ (𝑎 ∈ ℤ → 𝑎 ∈
ℝ) |
| 11 | | zre 12617 |
. . . . . . . . . . . . 13
⊢ (𝑏 ∈ ℤ → 𝑏 ∈
ℝ) |
| 12 | | crre 15153 |
. . . . . . . . . . . . 13
⊢ ((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) →
(ℜ‘(𝑎 + (i
· 𝑏))) = 𝑎) |
| 13 | 10, 11, 12 | syl2an 596 |
. . . . . . . . . . . 12
⊢ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) →
(ℜ‘(𝑎 + (i
· 𝑏))) = 𝑎) |
| 14 | 13 | oveq1d 7446 |
. . . . . . . . . . 11
⊢ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) →
((ℜ‘(𝑎 + (i
· 𝑏)))↑2) =
(𝑎↑2)) |
| 15 | | crim 15154 |
. . . . . . . . . . . . 13
⊢ ((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) →
(ℑ‘(𝑎 + (i
· 𝑏))) = 𝑏) |
| 16 | 10, 11, 15 | syl2an 596 |
. . . . . . . . . . . 12
⊢ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) →
(ℑ‘(𝑎 + (i
· 𝑏))) = 𝑏) |
| 17 | 16 | oveq1d 7446 |
. . . . . . . . . . 11
⊢ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) →
((ℑ‘(𝑎 + (i
· 𝑏)))↑2) =
(𝑏↑2)) |
| 18 | 14, 17 | oveq12d 7449 |
. . . . . . . . . 10
⊢ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) →
(((ℜ‘(𝑎 + (i
· 𝑏)))↑2) +
((ℑ‘(𝑎 + (i
· 𝑏)))↑2)) =
((𝑎↑2) + (𝑏↑2))) |
| 19 | 9, 18 | eqtrd 2777 |
. . . . . . . . 9
⊢ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) →
((abs‘(𝑎 + (i
· 𝑏)))↑2) =
((𝑎↑2) + (𝑏↑2))) |
| 20 | | gzcn 16970 |
. . . . . . . . . . . 12
⊢ ((𝑐 + (i · 𝑑)) ∈ ℤ[i] →
(𝑐 + (i · 𝑑)) ∈
ℂ) |
| 21 | 5, 20 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝑐 ∈ ℤ ∧ 𝑑 ∈ ℤ) → (𝑐 + (i · 𝑑)) ∈
ℂ) |
| 22 | 21 | absvalsq2d 15482 |
. . . . . . . . . 10
⊢ ((𝑐 ∈ ℤ ∧ 𝑑 ∈ ℤ) →
((abs‘(𝑐 + (i
· 𝑑)))↑2) =
(((ℜ‘(𝑐 + (i
· 𝑑)))↑2) +
((ℑ‘(𝑐 + (i
· 𝑑)))↑2))) |
| 23 | | zre 12617 |
. . . . . . . . . . . . 13
⊢ (𝑐 ∈ ℤ → 𝑐 ∈
ℝ) |
| 24 | | zre 12617 |
. . . . . . . . . . . . 13
⊢ (𝑑 ∈ ℤ → 𝑑 ∈
ℝ) |
| 25 | | crre 15153 |
. . . . . . . . . . . . 13
⊢ ((𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ) →
(ℜ‘(𝑐 + (i
· 𝑑))) = 𝑐) |
| 26 | 23, 24, 25 | syl2an 596 |
. . . . . . . . . . . 12
⊢ ((𝑐 ∈ ℤ ∧ 𝑑 ∈ ℤ) →
(ℜ‘(𝑐 + (i
· 𝑑))) = 𝑐) |
| 27 | 26 | oveq1d 7446 |
. . . . . . . . . . 11
⊢ ((𝑐 ∈ ℤ ∧ 𝑑 ∈ ℤ) →
((ℜ‘(𝑐 + (i
· 𝑑)))↑2) =
(𝑐↑2)) |
| 28 | | crim 15154 |
. . . . . . . . . . . . 13
⊢ ((𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ) →
(ℑ‘(𝑐 + (i
· 𝑑))) = 𝑑) |
| 29 | 23, 24, 28 | syl2an 596 |
. . . . . . . . . . . 12
⊢ ((𝑐 ∈ ℤ ∧ 𝑑 ∈ ℤ) →
(ℑ‘(𝑐 + (i
· 𝑑))) = 𝑑) |
| 30 | 29 | oveq1d 7446 |
. . . . . . . . . . 11
⊢ ((𝑐 ∈ ℤ ∧ 𝑑 ∈ ℤ) →
((ℑ‘(𝑐 + (i
· 𝑑)))↑2) =
(𝑑↑2)) |
| 31 | 27, 30 | oveq12d 7449 |
. . . . . . . . . 10
⊢ ((𝑐 ∈ ℤ ∧ 𝑑 ∈ ℤ) →
(((ℜ‘(𝑐 + (i
· 𝑑)))↑2) +
((ℑ‘(𝑐 + (i
· 𝑑)))↑2)) =
((𝑐↑2) + (𝑑↑2))) |
| 32 | 22, 31 | eqtrd 2777 |
. . . . . . . . 9
⊢ ((𝑐 ∈ ℤ ∧ 𝑑 ∈ ℤ) →
((abs‘(𝑐 + (i
· 𝑑)))↑2) =
((𝑐↑2) + (𝑑↑2))) |
| 33 | 19, 32 | oveqan12d 7450 |
. . . . . . . 8
⊢ (((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) ∧ (𝑐 ∈ ℤ ∧ 𝑑 ∈ ℤ)) →
(((abs‘(𝑎 + (i
· 𝑏)))↑2) +
((abs‘(𝑐 + (i
· 𝑑)))↑2)) =
(((𝑎↑2) + (𝑏↑2)) + ((𝑐↑2) + (𝑑↑2)))) |
| 34 | 33 | eqcomd 2743 |
. . . . . . 7
⊢ (((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) ∧ (𝑐 ∈ ℤ ∧ 𝑑 ∈ ℤ)) →
(((𝑎↑2) + (𝑏↑2)) + ((𝑐↑2) + (𝑑↑2))) = (((abs‘(𝑎 + (i · 𝑏)))↑2) + ((abs‘(𝑐 + (i · 𝑑)))↑2))) |
| 35 | | fveq2 6906 |
. . . . . . . . . . 11
⊢ (𝑢 = (𝑎 + (i · 𝑏)) → (abs‘𝑢) = (abs‘(𝑎 + (i · 𝑏)))) |
| 36 | 35 | oveq1d 7446 |
. . . . . . . . . 10
⊢ (𝑢 = (𝑎 + (i · 𝑏)) → ((abs‘𝑢)↑2) = ((abs‘(𝑎 + (i · 𝑏)))↑2)) |
| 37 | 36 | oveq1d 7446 |
. . . . . . . . 9
⊢ (𝑢 = (𝑎 + (i · 𝑏)) → (((abs‘𝑢)↑2) + ((abs‘𝑣)↑2)) = (((abs‘(𝑎 + (i · 𝑏)))↑2) + ((abs‘𝑣)↑2))) |
| 38 | 37 | eqeq2d 2748 |
. . . . . . . 8
⊢ (𝑢 = (𝑎 + (i · 𝑏)) → ((((𝑎↑2) + (𝑏↑2)) + ((𝑐↑2) + (𝑑↑2))) = (((abs‘𝑢)↑2) + ((abs‘𝑣)↑2)) ↔ (((𝑎↑2) + (𝑏↑2)) + ((𝑐↑2) + (𝑑↑2))) = (((abs‘(𝑎 + (i · 𝑏)))↑2) + ((abs‘𝑣)↑2)))) |
| 39 | | fveq2 6906 |
. . . . . . . . . . 11
⊢ (𝑣 = (𝑐 + (i · 𝑑)) → (abs‘𝑣) = (abs‘(𝑐 + (i · 𝑑)))) |
| 40 | 39 | oveq1d 7446 |
. . . . . . . . . 10
⊢ (𝑣 = (𝑐 + (i · 𝑑)) → ((abs‘𝑣)↑2) = ((abs‘(𝑐 + (i · 𝑑)))↑2)) |
| 41 | 40 | oveq2d 7447 |
. . . . . . . . 9
⊢ (𝑣 = (𝑐 + (i · 𝑑)) → (((abs‘(𝑎 + (i · 𝑏)))↑2) + ((abs‘𝑣)↑2)) = (((abs‘(𝑎 + (i · 𝑏)))↑2) + ((abs‘(𝑐 + (i · 𝑑)))↑2))) |
| 42 | 41 | eqeq2d 2748 |
. . . . . . . 8
⊢ (𝑣 = (𝑐 + (i · 𝑑)) → ((((𝑎↑2) + (𝑏↑2)) + ((𝑐↑2) + (𝑑↑2))) = (((abs‘(𝑎 + (i · 𝑏)))↑2) + ((abs‘𝑣)↑2)) ↔ (((𝑎↑2) + (𝑏↑2)) + ((𝑐↑2) + (𝑑↑2))) = (((abs‘(𝑎 + (i · 𝑏)))↑2) + ((abs‘(𝑐 + (i · 𝑑)))↑2)))) |
| 43 | 38, 42 | rspc2ev 3635 |
. . . . . . 7
⊢ (((𝑎 + (i · 𝑏)) ∈ ℤ[i] ∧
(𝑐 + (i · 𝑑)) ∈ ℤ[i] ∧
(((𝑎↑2) + (𝑏↑2)) + ((𝑐↑2) + (𝑑↑2))) = (((abs‘(𝑎 + (i · 𝑏)))↑2) + ((abs‘(𝑐 + (i · 𝑑)))↑2))) → ∃𝑢 ∈ ℤ[i] ∃𝑣 ∈ ℤ[i] (((𝑎↑2) + (𝑏↑2)) + ((𝑐↑2) + (𝑑↑2))) = (((abs‘𝑢)↑2) + ((abs‘𝑣)↑2))) |
| 44 | 4, 6, 34, 43 | syl3anc 1373 |
. . . . . 6
⊢ (((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) ∧ (𝑐 ∈ ℤ ∧ 𝑑 ∈ ℤ)) →
∃𝑢 ∈ ℤ[i]
∃𝑣 ∈ ℤ[i]
(((𝑎↑2) + (𝑏↑2)) + ((𝑐↑2) + (𝑑↑2))) = (((abs‘𝑢)↑2) + ((abs‘𝑣)↑2))) |
| 45 | | eqeq1 2741 |
. . . . . . 7
⊢ (𝐴 = (((𝑎↑2) + (𝑏↑2)) + ((𝑐↑2) + (𝑑↑2))) → (𝐴 = (((abs‘𝑢)↑2) + ((abs‘𝑣)↑2)) ↔ (((𝑎↑2) + (𝑏↑2)) + ((𝑐↑2) + (𝑑↑2))) = (((abs‘𝑢)↑2) + ((abs‘𝑣)↑2)))) |
| 46 | 45 | 2rexbidv 3222 |
. . . . . 6
⊢ (𝐴 = (((𝑎↑2) + (𝑏↑2)) + ((𝑐↑2) + (𝑑↑2))) → (∃𝑢 ∈ ℤ[i] ∃𝑣 ∈ ℤ[i] 𝐴 = (((abs‘𝑢)↑2) + ((abs‘𝑣)↑2)) ↔ ∃𝑢 ∈ ℤ[i] ∃𝑣 ∈ ℤ[i] (((𝑎↑2) + (𝑏↑2)) + ((𝑐↑2) + (𝑑↑2))) = (((abs‘𝑢)↑2) + ((abs‘𝑣)↑2)))) |
| 47 | 44, 46 | syl5ibrcom 247 |
. . . . 5
⊢ (((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) ∧ (𝑐 ∈ ℤ ∧ 𝑑 ∈ ℤ)) → (𝐴 = (((𝑎↑2) + (𝑏↑2)) + ((𝑐↑2) + (𝑑↑2))) → ∃𝑢 ∈ ℤ[i] ∃𝑣 ∈ ℤ[i] 𝐴 = (((abs‘𝑢)↑2) + ((abs‘𝑣)↑2)))) |
| 48 | 47 | rexlimdvva 3213 |
. . . 4
⊢ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) →
(∃𝑐 ∈ ℤ
∃𝑑 ∈ ℤ
𝐴 = (((𝑎↑2) + (𝑏↑2)) + ((𝑐↑2) + (𝑑↑2))) → ∃𝑢 ∈ ℤ[i] ∃𝑣 ∈ ℤ[i] 𝐴 = (((abs‘𝑢)↑2) + ((abs‘𝑣)↑2)))) |
| 49 | 48 | rexlimivv 3201 |
. . 3
⊢
(∃𝑎 ∈
ℤ ∃𝑏 ∈
ℤ ∃𝑐 ∈
ℤ ∃𝑑 ∈
ℤ 𝐴 = (((𝑎↑2) + (𝑏↑2)) + ((𝑐↑2) + (𝑑↑2))) → ∃𝑢 ∈ ℤ[i] ∃𝑣 ∈ ℤ[i] 𝐴 = (((abs‘𝑢)↑2) + ((abs‘𝑣)↑2))) |
| 50 | 2, 49 | sylbi 217 |
. 2
⊢ (𝐴 ∈ 𝑆 → ∃𝑢 ∈ ℤ[i] ∃𝑣 ∈ ℤ[i] 𝐴 = (((abs‘𝑢)↑2) + ((abs‘𝑣)↑2))) |
| 51 | 1 | 4sqlem4a 16989 |
. . . 4
⊢ ((𝑢 ∈ ℤ[i] ∧ 𝑣 ∈ ℤ[i]) →
(((abs‘𝑢)↑2) +
((abs‘𝑣)↑2))
∈ 𝑆) |
| 52 | | eleq1a 2836 |
. . . 4
⊢
((((abs‘𝑢)↑2) + ((abs‘𝑣)↑2)) ∈ 𝑆 → (𝐴 = (((abs‘𝑢)↑2) + ((abs‘𝑣)↑2)) → 𝐴 ∈ 𝑆)) |
| 53 | 51, 52 | syl 17 |
. . 3
⊢ ((𝑢 ∈ ℤ[i] ∧ 𝑣 ∈ ℤ[i]) →
(𝐴 = (((abs‘𝑢)↑2) + ((abs‘𝑣)↑2)) → 𝐴 ∈ 𝑆)) |
| 54 | 53 | rexlimivv 3201 |
. 2
⊢
(∃𝑢 ∈
ℤ[i] ∃𝑣 ∈
ℤ[i] 𝐴 =
(((abs‘𝑢)↑2) +
((abs‘𝑣)↑2))
→ 𝐴 ∈ 𝑆) |
| 55 | 50, 54 | impbii 209 |
1
⊢ (𝐴 ∈ 𝑆 ↔ ∃𝑢 ∈ ℤ[i] ∃𝑣 ∈ ℤ[i] 𝐴 = (((abs‘𝑢)↑2) + ((abs‘𝑣)↑2))) |