MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  2sqlem3 Structured version   Visualization version   GIF version

Theorem 2sqlem3 25436
Description: Lemma for 2sqlem5 25438. (Contributed by Mario Carneiro, 20-Jun-2015.)
Hypotheses
Ref Expression
2sq.1 𝑆 = ran (𝑤 ∈ ℤ[i] ↦ ((abs‘𝑤)↑2))
2sqlem5.1 (𝜑𝑁 ∈ ℕ)
2sqlem5.2 (𝜑𝑃 ∈ ℙ)
2sqlem4.3 (𝜑𝐴 ∈ ℤ)
2sqlem4.4 (𝜑𝐵 ∈ ℤ)
2sqlem4.5 (𝜑𝐶 ∈ ℤ)
2sqlem4.6 (𝜑𝐷 ∈ ℤ)
2sqlem4.7 (𝜑 → (𝑁 · 𝑃) = ((𝐴↑2) + (𝐵↑2)))
2sqlem4.8 (𝜑𝑃 = ((𝐶↑2) + (𝐷↑2)))
2sqlem4.9 (𝜑𝑃 ∥ ((𝐶 · 𝐵) + (𝐴 · 𝐷)))
Assertion
Ref Expression
2sqlem3 (𝜑𝑁𝑆)

Proof of Theorem 2sqlem3
Dummy variable 𝑥 is distinct from all other variables.
StepHypRef Expression
1 2sqlem4.3 . . . . . . . 8 (𝜑𝐴 ∈ ℤ)
2 2sqlem4.4 . . . . . . . 8 (𝜑𝐵 ∈ ℤ)
3 gzreim 15922 . . . . . . . 8 ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (𝐴 + (i · 𝐵)) ∈ ℤ[i])
41, 2, 3syl2anc 579 . . . . . . 7 (𝜑 → (𝐴 + (i · 𝐵)) ∈ ℤ[i])
5 2sqlem4.5 . . . . . . . 8 (𝜑𝐶 ∈ ℤ)
6 2sqlem4.6 . . . . . . . 8 (𝜑𝐷 ∈ ℤ)
7 gzreim 15922 . . . . . . . 8 ((𝐶 ∈ ℤ ∧ 𝐷 ∈ ℤ) → (𝐶 + (i · 𝐷)) ∈ ℤ[i])
85, 6, 7syl2anc 579 . . . . . . 7 (𝜑 → (𝐶 + (i · 𝐷)) ∈ ℤ[i])
9 gzmulcl 15921 . . . . . . 7 (((𝐴 + (i · 𝐵)) ∈ ℤ[i] ∧ (𝐶 + (i · 𝐷)) ∈ ℤ[i]) → ((𝐴 + (i · 𝐵)) · (𝐶 + (i · 𝐷))) ∈ ℤ[i])
104, 8, 9syl2anc 579 . . . . . 6 (𝜑 → ((𝐴 + (i · 𝐵)) · (𝐶 + (i · 𝐷))) ∈ ℤ[i])
11 gzcn 15915 . . . . . 6 (((𝐴 + (i · 𝐵)) · (𝐶 + (i · 𝐷))) ∈ ℤ[i] → ((𝐴 + (i · 𝐵)) · (𝐶 + (i · 𝐷))) ∈ ℂ)
1210, 11syl 17 . . . . 5 (𝜑 → ((𝐴 + (i · 𝐵)) · (𝐶 + (i · 𝐷))) ∈ ℂ)
13 2sqlem5.2 . . . . . . 7 (𝜑𝑃 ∈ ℙ)
14 prmnn 15668 . . . . . . 7 (𝑃 ∈ ℙ → 𝑃 ∈ ℕ)
1513, 14syl 17 . . . . . 6 (𝜑𝑃 ∈ ℕ)
1615nncnd 11292 . . . . 5 (𝜑𝑃 ∈ ℂ)
1715nnne0d 11322 . . . . 5 (𝜑𝑃 ≠ 0)
1812, 16, 17divcld 11055 . . . 4 (𝜑 → (((𝐴 + (i · 𝐵)) · (𝐶 + (i · 𝐷))) / 𝑃) ∈ ℂ)
1915nnred 11291 . . . . . 6 (𝜑𝑃 ∈ ℝ)
2019, 12, 17redivd 14254 . . . . 5 (𝜑 → (ℜ‘(((𝐴 + (i · 𝐵)) · (𝐶 + (i · 𝐷))) / 𝑃)) = ((ℜ‘((𝐴 + (i · 𝐵)) · (𝐶 + (i · 𝐷)))) / 𝑃))
21 prmz 15669 . . . . . . . . . . . . . 14 (𝑃 ∈ ℙ → 𝑃 ∈ ℤ)
2213, 21syl 17 . . . . . . . . . . . . 13 (𝜑𝑃 ∈ ℤ)
23 dvdsmul2 15289 . . . . . . . . . . . . 13 ((𝑃 ∈ ℤ ∧ 𝑃 ∈ ℤ) → 𝑃 ∥ (𝑃 · 𝑃))
2422, 22, 23syl2anc 579 . . . . . . . . . . . 12 (𝜑𝑃 ∥ (𝑃 · 𝑃))
2516sqvald 13212 . . . . . . . . . . . 12 (𝜑 → (𝑃↑2) = (𝑃 · 𝑃))
2624, 25breqtrrd 4837 . . . . . . . . . . 11 (𝜑𝑃 ∥ (𝑃↑2))
27 2sqlem5.1 . . . . . . . . . . . . 13 (𝜑𝑁 ∈ ℕ)
2827nnzd 11728 . . . . . . . . . . . 12 (𝜑𝑁 ∈ ℤ)
29 zsqcl 13141 . . . . . . . . . . . . 13 (𝑃 ∈ ℤ → (𝑃↑2) ∈ ℤ)
3022, 29syl 17 . . . . . . . . . . . 12 (𝜑 → (𝑃↑2) ∈ ℤ)
31 dvdsmul2 15289 . . . . . . . . . . . 12 ((𝑁 ∈ ℤ ∧ (𝑃↑2) ∈ ℤ) → (𝑃↑2) ∥ (𝑁 · (𝑃↑2)))
3228, 30, 31syl2anc 579 . . . . . . . . . . 11 (𝜑 → (𝑃↑2) ∥ (𝑁 · (𝑃↑2)))
3328, 30zmulcld 11735 . . . . . . . . . . . 12 (𝜑 → (𝑁 · (𝑃↑2)) ∈ ℤ)
34 dvdstr 15303 . . . . . . . . . . . 12 ((𝑃 ∈ ℤ ∧ (𝑃↑2) ∈ ℤ ∧ (𝑁 · (𝑃↑2)) ∈ ℤ) → ((𝑃 ∥ (𝑃↑2) ∧ (𝑃↑2) ∥ (𝑁 · (𝑃↑2))) → 𝑃 ∥ (𝑁 · (𝑃↑2))))
3522, 30, 33, 34syl3anc 1490 . . . . . . . . . . 11 (𝜑 → ((𝑃 ∥ (𝑃↑2) ∧ (𝑃↑2) ∥ (𝑁 · (𝑃↑2))) → 𝑃 ∥ (𝑁 · (𝑃↑2))))
3626, 32, 35mp2and 690 . . . . . . . . . 10 (𝜑𝑃 ∥ (𝑁 · (𝑃↑2)))
37 gzcn 15915 . . . . . . . . . . . . . . . 16 ((𝐴 + (i · 𝐵)) ∈ ℤ[i] → (𝐴 + (i · 𝐵)) ∈ ℂ)
384, 37syl 17 . . . . . . . . . . . . . . 15 (𝜑 → (𝐴 + (i · 𝐵)) ∈ ℂ)
3938abscld 14460 . . . . . . . . . . . . . 14 (𝜑 → (abs‘(𝐴 + (i · 𝐵))) ∈ ℝ)
4039recnd 10322 . . . . . . . . . . . . 13 (𝜑 → (abs‘(𝐴 + (i · 𝐵))) ∈ ℂ)
41 gzcn 15915 . . . . . . . . . . . . . . . 16 ((𝐶 + (i · 𝐷)) ∈ ℤ[i] → (𝐶 + (i · 𝐷)) ∈ ℂ)
428, 41syl 17 . . . . . . . . . . . . . . 15 (𝜑 → (𝐶 + (i · 𝐷)) ∈ ℂ)
4342abscld 14460 . . . . . . . . . . . . . 14 (𝜑 → (abs‘(𝐶 + (i · 𝐷))) ∈ ℝ)
4443recnd 10322 . . . . . . . . . . . . 13 (𝜑 → (abs‘(𝐶 + (i · 𝐷))) ∈ ℂ)
4540, 44sqmuld 13227 . . . . . . . . . . . 12 (𝜑 → (((abs‘(𝐴 + (i · 𝐵))) · (abs‘(𝐶 + (i · 𝐷))))↑2) = (((abs‘(𝐴 + (i · 𝐵)))↑2) · ((abs‘(𝐶 + (i · 𝐷)))↑2)))
461zred 11729 . . . . . . . . . . . . . . . . 17 (𝜑𝐴 ∈ ℝ)
472zred 11729 . . . . . . . . . . . . . . . . 17 (𝜑𝐵 ∈ ℝ)
4846, 47crred 14256 . . . . . . . . . . . . . . . 16 (𝜑 → (ℜ‘(𝐴 + (i · 𝐵))) = 𝐴)
4948oveq1d 6857 . . . . . . . . . . . . . . 15 (𝜑 → ((ℜ‘(𝐴 + (i · 𝐵)))↑2) = (𝐴↑2))
5046, 47crimd 14257 . . . . . . . . . . . . . . . 16 (𝜑 → (ℑ‘(𝐴 + (i · 𝐵))) = 𝐵)
5150oveq1d 6857 . . . . . . . . . . . . . . 15 (𝜑 → ((ℑ‘(𝐴 + (i · 𝐵)))↑2) = (𝐵↑2))
5249, 51oveq12d 6860 . . . . . . . . . . . . . 14 (𝜑 → (((ℜ‘(𝐴 + (i · 𝐵)))↑2) + ((ℑ‘(𝐴 + (i · 𝐵)))↑2)) = ((𝐴↑2) + (𝐵↑2)))
5338absvalsq2d 14467 . . . . . . . . . . . . . 14 (𝜑 → ((abs‘(𝐴 + (i · 𝐵)))↑2) = (((ℜ‘(𝐴 + (i · 𝐵)))↑2) + ((ℑ‘(𝐴 + (i · 𝐵)))↑2)))
54 2sqlem4.7 . . . . . . . . . . . . . 14 (𝜑 → (𝑁 · 𝑃) = ((𝐴↑2) + (𝐵↑2)))
5552, 53, 543eqtr4d 2809 . . . . . . . . . . . . 13 (𝜑 → ((abs‘(𝐴 + (i · 𝐵)))↑2) = (𝑁 · 𝑃))
565zred 11729 . . . . . . . . . . . . . . . . 17 (𝜑𝐶 ∈ ℝ)
576zred 11729 . . . . . . . . . . . . . . . . 17 (𝜑𝐷 ∈ ℝ)
5856, 57crred 14256 . . . . . . . . . . . . . . . 16 (𝜑 → (ℜ‘(𝐶 + (i · 𝐷))) = 𝐶)
5958oveq1d 6857 . . . . . . . . . . . . . . 15 (𝜑 → ((ℜ‘(𝐶 + (i · 𝐷)))↑2) = (𝐶↑2))
6056, 57crimd 14257 . . . . . . . . . . . . . . . 16 (𝜑 → (ℑ‘(𝐶 + (i · 𝐷))) = 𝐷)
6160oveq1d 6857 . . . . . . . . . . . . . . 15 (𝜑 → ((ℑ‘(𝐶 + (i · 𝐷)))↑2) = (𝐷↑2))
6259, 61oveq12d 6860 . . . . . . . . . . . . . 14 (𝜑 → (((ℜ‘(𝐶 + (i · 𝐷)))↑2) + ((ℑ‘(𝐶 + (i · 𝐷)))↑2)) = ((𝐶↑2) + (𝐷↑2)))
6342absvalsq2d 14467 . . . . . . . . . . . . . 14 (𝜑 → ((abs‘(𝐶 + (i · 𝐷)))↑2) = (((ℜ‘(𝐶 + (i · 𝐷)))↑2) + ((ℑ‘(𝐶 + (i · 𝐷)))↑2)))
64 2sqlem4.8 . . . . . . . . . . . . . 14 (𝜑𝑃 = ((𝐶↑2) + (𝐷↑2)))
6562, 63, 643eqtr4d 2809 . . . . . . . . . . . . 13 (𝜑 → ((abs‘(𝐶 + (i · 𝐷)))↑2) = 𝑃)
6655, 65oveq12d 6860 . . . . . . . . . . . 12 (𝜑 → (((abs‘(𝐴 + (i · 𝐵)))↑2) · ((abs‘(𝐶 + (i · 𝐷)))↑2)) = ((𝑁 · 𝑃) · 𝑃))
6727nncnd 11292 . . . . . . . . . . . . 13 (𝜑𝑁 ∈ ℂ)
6867, 16, 16mulassd 10317 . . . . . . . . . . . 12 (𝜑 → ((𝑁 · 𝑃) · 𝑃) = (𝑁 · (𝑃 · 𝑃)))
6945, 66, 683eqtrd 2803 . . . . . . . . . . 11 (𝜑 → (((abs‘(𝐴 + (i · 𝐵))) · (abs‘(𝐶 + (i · 𝐷))))↑2) = (𝑁 · (𝑃 · 𝑃)))
7038, 42absmuld 14478 . . . . . . . . . . . 12 (𝜑 → (abs‘((𝐴 + (i · 𝐵)) · (𝐶 + (i · 𝐷)))) = ((abs‘(𝐴 + (i · 𝐵))) · (abs‘(𝐶 + (i · 𝐷)))))
7170oveq1d 6857 . . . . . . . . . . 11 (𝜑 → ((abs‘((𝐴 + (i · 𝐵)) · (𝐶 + (i · 𝐷))))↑2) = (((abs‘(𝐴 + (i · 𝐵))) · (abs‘(𝐶 + (i · 𝐷))))↑2))
7225oveq2d 6858 . . . . . . . . . . 11 (𝜑 → (𝑁 · (𝑃↑2)) = (𝑁 · (𝑃 · 𝑃)))
7369, 71, 723eqtr4d 2809 . . . . . . . . . 10 (𝜑 → ((abs‘((𝐴 + (i · 𝐵)) · (𝐶 + (i · 𝐷))))↑2) = (𝑁 · (𝑃↑2)))
7436, 73breqtrrd 4837 . . . . . . . . 9 (𝜑𝑃 ∥ ((abs‘((𝐴 + (i · 𝐵)) · (𝐶 + (i · 𝐷))))↑2))
7512absvalsq2d 14467 . . . . . . . . . 10 (𝜑 → ((abs‘((𝐴 + (i · 𝐵)) · (𝐶 + (i · 𝐷))))↑2) = (((ℜ‘((𝐴 + (i · 𝐵)) · (𝐶 + (i · 𝐷))))↑2) + ((ℑ‘((𝐴 + (i · 𝐵)) · (𝐶 + (i · 𝐷))))↑2)))
76 elgz 15914 . . . . . . . . . . . . . . 15 (((𝐴 + (i · 𝐵)) · (𝐶 + (i · 𝐷))) ∈ ℤ[i] ↔ (((𝐴 + (i · 𝐵)) · (𝐶 + (i · 𝐷))) ∈ ℂ ∧ (ℜ‘((𝐴 + (i · 𝐵)) · (𝐶 + (i · 𝐷)))) ∈ ℤ ∧ (ℑ‘((𝐴 + (i · 𝐵)) · (𝐶 + (i · 𝐷)))) ∈ ℤ))
7776simp2bi 1176 . . . . . . . . . . . . . 14 (((𝐴 + (i · 𝐵)) · (𝐶 + (i · 𝐷))) ∈ ℤ[i] → (ℜ‘((𝐴 + (i · 𝐵)) · (𝐶 + (i · 𝐷)))) ∈ ℤ)
7810, 77syl 17 . . . . . . . . . . . . 13 (𝜑 → (ℜ‘((𝐴 + (i · 𝐵)) · (𝐶 + (i · 𝐷)))) ∈ ℤ)
79 zsqcl 13141 . . . . . . . . . . . . 13 ((ℜ‘((𝐴 + (i · 𝐵)) · (𝐶 + (i · 𝐷)))) ∈ ℤ → ((ℜ‘((𝐴 + (i · 𝐵)) · (𝐶 + (i · 𝐷))))↑2) ∈ ℤ)
8078, 79syl 17 . . . . . . . . . . . 12 (𝜑 → ((ℜ‘((𝐴 + (i · 𝐵)) · (𝐶 + (i · 𝐷))))↑2) ∈ ℤ)
8180zcnd 11730 . . . . . . . . . . 11 (𝜑 → ((ℜ‘((𝐴 + (i · 𝐵)) · (𝐶 + (i · 𝐷))))↑2) ∈ ℂ)
8276simp3bi 1177 . . . . . . . . . . . . . 14 (((𝐴 + (i · 𝐵)) · (𝐶 + (i · 𝐷))) ∈ ℤ[i] → (ℑ‘((𝐴 + (i · 𝐵)) · (𝐶 + (i · 𝐷)))) ∈ ℤ)
8310, 82syl 17 . . . . . . . . . . . . 13 (𝜑 → (ℑ‘((𝐴 + (i · 𝐵)) · (𝐶 + (i · 𝐷)))) ∈ ℤ)
84 zsqcl 13141 . . . . . . . . . . . . 13 ((ℑ‘((𝐴 + (i · 𝐵)) · (𝐶 + (i · 𝐷)))) ∈ ℤ → ((ℑ‘((𝐴 + (i · 𝐵)) · (𝐶 + (i · 𝐷))))↑2) ∈ ℤ)
8583, 84syl 17 . . . . . . . . . . . 12 (𝜑 → ((ℑ‘((𝐴 + (i · 𝐵)) · (𝐶 + (i · 𝐷))))↑2) ∈ ℤ)
8685zcnd 11730 . . . . . . . . . . 11 (𝜑 → ((ℑ‘((𝐴 + (i · 𝐵)) · (𝐶 + (i · 𝐷))))↑2) ∈ ℂ)
8781, 86addcomd 10492 . . . . . . . . . 10 (𝜑 → (((ℜ‘((𝐴 + (i · 𝐵)) · (𝐶 + (i · 𝐷))))↑2) + ((ℑ‘((𝐴 + (i · 𝐵)) · (𝐶 + (i · 𝐷))))↑2)) = (((ℑ‘((𝐴 + (i · 𝐵)) · (𝐶 + (i · 𝐷))))↑2) + ((ℜ‘((𝐴 + (i · 𝐵)) · (𝐶 + (i · 𝐷))))↑2)))
8875, 87eqtrd 2799 . . . . . . . . 9 (𝜑 → ((abs‘((𝐴 + (i · 𝐵)) · (𝐶 + (i · 𝐷))))↑2) = (((ℑ‘((𝐴 + (i · 𝐵)) · (𝐶 + (i · 𝐷))))↑2) + ((ℜ‘((𝐴 + (i · 𝐵)) · (𝐶 + (i · 𝐷))))↑2)))
8974, 88breqtrd 4835 . . . . . . . 8 (𝜑𝑃 ∥ (((ℑ‘((𝐴 + (i · 𝐵)) · (𝐶 + (i · 𝐷))))↑2) + ((ℜ‘((𝐴 + (i · 𝐵)) · (𝐶 + (i · 𝐷))))↑2)))
90 2sqlem4.9 . . . . . . . . . . . 12 (𝜑𝑃 ∥ ((𝐶 · 𝐵) + (𝐴 · 𝐷)))
915zcnd 11730 . . . . . . . . . . . . . . 15 (𝜑𝐶 ∈ ℂ)
922zcnd 11730 . . . . . . . . . . . . . . 15 (𝜑𝐵 ∈ ℂ)
9391, 92mulcld 10314 . . . . . . . . . . . . . 14 (𝜑 → (𝐶 · 𝐵) ∈ ℂ)
941zcnd 11730 . . . . . . . . . . . . . . 15 (𝜑𝐴 ∈ ℂ)
956zcnd 11730 . . . . . . . . . . . . . . 15 (𝜑𝐷 ∈ ℂ)
9694, 95mulcld 10314 . . . . . . . . . . . . . 14 (𝜑 → (𝐴 · 𝐷) ∈ ℂ)
9793, 96addcomd 10492 . . . . . . . . . . . . 13 (𝜑 → ((𝐶 · 𝐵) + (𝐴 · 𝐷)) = ((𝐴 · 𝐷) + (𝐶 · 𝐵)))
9891, 92mulcomd 10315 . . . . . . . . . . . . . 14 (𝜑 → (𝐶 · 𝐵) = (𝐵 · 𝐶))
9998oveq2d 6858 . . . . . . . . . . . . 13 (𝜑 → ((𝐴 · 𝐷) + (𝐶 · 𝐵)) = ((𝐴 · 𝐷) + (𝐵 · 𝐶)))
10097, 99eqtrd 2799 . . . . . . . . . . . 12 (𝜑 → ((𝐶 · 𝐵) + (𝐴 · 𝐷)) = ((𝐴 · 𝐷) + (𝐵 · 𝐶)))
10190, 100breqtrd 4835 . . . . . . . . . . 11 (𝜑𝑃 ∥ ((𝐴 · 𝐷) + (𝐵 · 𝐶)))
10238, 42immuld 14244 . . . . . . . . . . . 12 (𝜑 → (ℑ‘((𝐴 + (i · 𝐵)) · (𝐶 + (i · 𝐷)))) = (((ℜ‘(𝐴 + (i · 𝐵))) · (ℑ‘(𝐶 + (i · 𝐷)))) + ((ℑ‘(𝐴 + (i · 𝐵))) · (ℜ‘(𝐶 + (i · 𝐷))))))
10348, 60oveq12d 6860 . . . . . . . . . . . . 13 (𝜑 → ((ℜ‘(𝐴 + (i · 𝐵))) · (ℑ‘(𝐶 + (i · 𝐷)))) = (𝐴 · 𝐷))
10450, 58oveq12d 6860 . . . . . . . . . . . . 13 (𝜑 → ((ℑ‘(𝐴 + (i · 𝐵))) · (ℜ‘(𝐶 + (i · 𝐷)))) = (𝐵 · 𝐶))
105103, 104oveq12d 6860 . . . . . . . . . . . 12 (𝜑 → (((ℜ‘(𝐴 + (i · 𝐵))) · (ℑ‘(𝐶 + (i · 𝐷)))) + ((ℑ‘(𝐴 + (i · 𝐵))) · (ℜ‘(𝐶 + (i · 𝐷))))) = ((𝐴 · 𝐷) + (𝐵 · 𝐶)))
106102, 105eqtrd 2799 . . . . . . . . . . 11 (𝜑 → (ℑ‘((𝐴 + (i · 𝐵)) · (𝐶 + (i · 𝐷)))) = ((𝐴 · 𝐷) + (𝐵 · 𝐶)))
107101, 106breqtrrd 4837 . . . . . . . . . 10 (𝜑𝑃 ∥ (ℑ‘((𝐴 + (i · 𝐵)) · (𝐶 + (i · 𝐷)))))
108 2nn 11345 . . . . . . . . . . . 12 2 ∈ ℕ
109108a1i 11 . . . . . . . . . . 11 (𝜑 → 2 ∈ ℕ)
110 prmdvdsexp 15706 . . . . . . . . . . 11 ((𝑃 ∈ ℙ ∧ (ℑ‘((𝐴 + (i · 𝐵)) · (𝐶 + (i · 𝐷)))) ∈ ℤ ∧ 2 ∈ ℕ) → (𝑃 ∥ ((ℑ‘((𝐴 + (i · 𝐵)) · (𝐶 + (i · 𝐷))))↑2) ↔ 𝑃 ∥ (ℑ‘((𝐴 + (i · 𝐵)) · (𝐶 + (i · 𝐷))))))
11113, 83, 109, 110syl3anc 1490 . . . . . . . . . 10 (𝜑 → (𝑃 ∥ ((ℑ‘((𝐴 + (i · 𝐵)) · (𝐶 + (i · 𝐷))))↑2) ↔ 𝑃 ∥ (ℑ‘((𝐴 + (i · 𝐵)) · (𝐶 + (i · 𝐷))))))
112107, 111mpbird 248 . . . . . . . . 9 (𝜑𝑃 ∥ ((ℑ‘((𝐴 + (i · 𝐵)) · (𝐶 + (i · 𝐷))))↑2))
113 dvdsadd2b 15313 . . . . . . . . 9 ((𝑃 ∈ ℤ ∧ ((ℜ‘((𝐴 + (i · 𝐵)) · (𝐶 + (i · 𝐷))))↑2) ∈ ℤ ∧ (((ℑ‘((𝐴 + (i · 𝐵)) · (𝐶 + (i · 𝐷))))↑2) ∈ ℤ ∧ 𝑃 ∥ ((ℑ‘((𝐴 + (i · 𝐵)) · (𝐶 + (i · 𝐷))))↑2))) → (𝑃 ∥ ((ℜ‘((𝐴 + (i · 𝐵)) · (𝐶 + (i · 𝐷))))↑2) ↔ 𝑃 ∥ (((ℑ‘((𝐴 + (i · 𝐵)) · (𝐶 + (i · 𝐷))))↑2) + ((ℜ‘((𝐴 + (i · 𝐵)) · (𝐶 + (i · 𝐷))))↑2))))
11422, 80, 85, 112, 113syl112anc 1493 . . . . . . . 8 (𝜑 → (𝑃 ∥ ((ℜ‘((𝐴 + (i · 𝐵)) · (𝐶 + (i · 𝐷))))↑2) ↔ 𝑃 ∥ (((ℑ‘((𝐴 + (i · 𝐵)) · (𝐶 + (i · 𝐷))))↑2) + ((ℜ‘((𝐴 + (i · 𝐵)) · (𝐶 + (i · 𝐷))))↑2))))
11589, 114mpbird 248 . . . . . . 7 (𝜑𝑃 ∥ ((ℜ‘((𝐴 + (i · 𝐵)) · (𝐶 + (i · 𝐷))))↑2))
116 prmdvdsexp 15706 . . . . . . . 8 ((𝑃 ∈ ℙ ∧ (ℜ‘((𝐴 + (i · 𝐵)) · (𝐶 + (i · 𝐷)))) ∈ ℤ ∧ 2 ∈ ℕ) → (𝑃 ∥ ((ℜ‘((𝐴 + (i · 𝐵)) · (𝐶 + (i · 𝐷))))↑2) ↔ 𝑃 ∥ (ℜ‘((𝐴 + (i · 𝐵)) · (𝐶 + (i · 𝐷))))))
11713, 78, 109, 116syl3anc 1490 . . . . . . 7 (𝜑 → (𝑃 ∥ ((ℜ‘((𝐴 + (i · 𝐵)) · (𝐶 + (i · 𝐷))))↑2) ↔ 𝑃 ∥ (ℜ‘((𝐴 + (i · 𝐵)) · (𝐶 + (i · 𝐷))))))
118115, 117mpbid 223 . . . . . 6 (𝜑𝑃 ∥ (ℜ‘((𝐴 + (i · 𝐵)) · (𝐶 + (i · 𝐷)))))
119 dvdsval2 15268 . . . . . . 7 ((𝑃 ∈ ℤ ∧ 𝑃 ≠ 0 ∧ (ℜ‘((𝐴 + (i · 𝐵)) · (𝐶 + (i · 𝐷)))) ∈ ℤ) → (𝑃 ∥ (ℜ‘((𝐴 + (i · 𝐵)) · (𝐶 + (i · 𝐷)))) ↔ ((ℜ‘((𝐴 + (i · 𝐵)) · (𝐶 + (i · 𝐷)))) / 𝑃) ∈ ℤ))
12022, 17, 78, 119syl3anc 1490 . . . . . 6 (𝜑 → (𝑃 ∥ (ℜ‘((𝐴 + (i · 𝐵)) · (𝐶 + (i · 𝐷)))) ↔ ((ℜ‘((𝐴 + (i · 𝐵)) · (𝐶 + (i · 𝐷)))) / 𝑃) ∈ ℤ))
121118, 120mpbid 223 . . . . 5 (𝜑 → ((ℜ‘((𝐴 + (i · 𝐵)) · (𝐶 + (i · 𝐷)))) / 𝑃) ∈ ℤ)
12220, 121eqeltrd 2844 . . . 4 (𝜑 → (ℜ‘(((𝐴 + (i · 𝐵)) · (𝐶 + (i · 𝐷))) / 𝑃)) ∈ ℤ)
12319, 12, 17imdivd 14255 . . . . 5 (𝜑 → (ℑ‘(((𝐴 + (i · 𝐵)) · (𝐶 + (i · 𝐷))) / 𝑃)) = ((ℑ‘((𝐴 + (i · 𝐵)) · (𝐶 + (i · 𝐷)))) / 𝑃))
124 dvdsval2 15268 . . . . . . 7 ((𝑃 ∈ ℤ ∧ 𝑃 ≠ 0 ∧ (ℑ‘((𝐴 + (i · 𝐵)) · (𝐶 + (i · 𝐷)))) ∈ ℤ) → (𝑃 ∥ (ℑ‘((𝐴 + (i · 𝐵)) · (𝐶 + (i · 𝐷)))) ↔ ((ℑ‘((𝐴 + (i · 𝐵)) · (𝐶 + (i · 𝐷)))) / 𝑃) ∈ ℤ))
12522, 17, 83, 124syl3anc 1490 . . . . . 6 (𝜑 → (𝑃 ∥ (ℑ‘((𝐴 + (i · 𝐵)) · (𝐶 + (i · 𝐷)))) ↔ ((ℑ‘((𝐴 + (i · 𝐵)) · (𝐶 + (i · 𝐷)))) / 𝑃) ∈ ℤ))
126107, 125mpbid 223 . . . . 5 (𝜑 → ((ℑ‘((𝐴 + (i · 𝐵)) · (𝐶 + (i · 𝐷)))) / 𝑃) ∈ ℤ)
127123, 126eqeltrd 2844 . . . 4 (𝜑 → (ℑ‘(((𝐴 + (i · 𝐵)) · (𝐶 + (i · 𝐷))) / 𝑃)) ∈ ℤ)
128 elgz 15914 . . . 4 ((((𝐴 + (i · 𝐵)) · (𝐶 + (i · 𝐷))) / 𝑃) ∈ ℤ[i] ↔ ((((𝐴 + (i · 𝐵)) · (𝐶 + (i · 𝐷))) / 𝑃) ∈ ℂ ∧ (ℜ‘(((𝐴 + (i · 𝐵)) · (𝐶 + (i · 𝐷))) / 𝑃)) ∈ ℤ ∧ (ℑ‘(((𝐴 + (i · 𝐵)) · (𝐶 + (i · 𝐷))) / 𝑃)) ∈ ℤ))
12918, 122, 127, 128syl3anbrc 1443 . . 3 (𝜑 → (((𝐴 + (i · 𝐵)) · (𝐶 + (i · 𝐷))) / 𝑃) ∈ ℤ[i])
13012, 16, 17absdivd 14479 . . . . . 6 (𝜑 → (abs‘(((𝐴 + (i · 𝐵)) · (𝐶 + (i · 𝐷))) / 𝑃)) = ((abs‘((𝐴 + (i · 𝐵)) · (𝐶 + (i · 𝐷)))) / (abs‘𝑃)))
13115nnnn0d 11598 . . . . . . . . 9 (𝜑𝑃 ∈ ℕ0)
132131nn0ge0d 11601 . . . . . . . 8 (𝜑 → 0 ≤ 𝑃)
13319, 132absidd 14446 . . . . . . 7 (𝜑 → (abs‘𝑃) = 𝑃)
134133oveq2d 6858 . . . . . 6 (𝜑 → ((abs‘((𝐴 + (i · 𝐵)) · (𝐶 + (i · 𝐷)))) / (abs‘𝑃)) = ((abs‘((𝐴 + (i · 𝐵)) · (𝐶 + (i · 𝐷)))) / 𝑃))
135130, 134eqtrd 2799 . . . . 5 (𝜑 → (abs‘(((𝐴 + (i · 𝐵)) · (𝐶 + (i · 𝐷))) / 𝑃)) = ((abs‘((𝐴 + (i · 𝐵)) · (𝐶 + (i · 𝐷)))) / 𝑃))
136135oveq1d 6857 . . . 4 (𝜑 → ((abs‘(((𝐴 + (i · 𝐵)) · (𝐶 + (i · 𝐷))) / 𝑃))↑2) = (((abs‘((𝐴 + (i · 𝐵)) · (𝐶 + (i · 𝐷)))) / 𝑃)↑2))
13712abscld 14460 . . . . . 6 (𝜑 → (abs‘((𝐴 + (i · 𝐵)) · (𝐶 + (i · 𝐷)))) ∈ ℝ)
138137recnd 10322 . . . . 5 (𝜑 → (abs‘((𝐴 + (i · 𝐵)) · (𝐶 + (i · 𝐷)))) ∈ ℂ)
139138, 16, 17sqdivd 13228 . . . 4 (𝜑 → (((abs‘((𝐴 + (i · 𝐵)) · (𝐶 + (i · 𝐷)))) / 𝑃)↑2) = (((abs‘((𝐴 + (i · 𝐵)) · (𝐶 + (i · 𝐷))))↑2) / (𝑃↑2)))
14073oveq1d 6857 . . . . 5 (𝜑 → (((abs‘((𝐴 + (i · 𝐵)) · (𝐶 + (i · 𝐷))))↑2) / (𝑃↑2)) = ((𝑁 · (𝑃↑2)) / (𝑃↑2)))
14115nnsqcld 13236 . . . . . . 7 (𝜑 → (𝑃↑2) ∈ ℕ)
142141nncnd 11292 . . . . . 6 (𝜑 → (𝑃↑2) ∈ ℂ)
143141nnne0d 11322 . . . . . 6 (𝜑 → (𝑃↑2) ≠ 0)
14467, 142, 143divcan4d 11061 . . . . 5 (𝜑 → ((𝑁 · (𝑃↑2)) / (𝑃↑2)) = 𝑁)
145140, 144eqtrd 2799 . . . 4 (𝜑 → (((abs‘((𝐴 + (i · 𝐵)) · (𝐶 + (i · 𝐷))))↑2) / (𝑃↑2)) = 𝑁)
146136, 139, 1453eqtrrd 2804 . . 3 (𝜑𝑁 = ((abs‘(((𝐴 + (i · 𝐵)) · (𝐶 + (i · 𝐷))) / 𝑃))↑2))
147 fveq2 6375 . . . . 5 (𝑥 = (((𝐴 + (i · 𝐵)) · (𝐶 + (i · 𝐷))) / 𝑃) → (abs‘𝑥) = (abs‘(((𝐴 + (i · 𝐵)) · (𝐶 + (i · 𝐷))) / 𝑃)))
148147oveq1d 6857 . . . 4 (𝑥 = (((𝐴 + (i · 𝐵)) · (𝐶 + (i · 𝐷))) / 𝑃) → ((abs‘𝑥)↑2) = ((abs‘(((𝐴 + (i · 𝐵)) · (𝐶 + (i · 𝐷))) / 𝑃))↑2))
149148rspceeqv 3479 . . 3 (((((𝐴 + (i · 𝐵)) · (𝐶 + (i · 𝐷))) / 𝑃) ∈ ℤ[i] ∧ 𝑁 = ((abs‘(((𝐴 + (i · 𝐵)) · (𝐶 + (i · 𝐷))) / 𝑃))↑2)) → ∃𝑥 ∈ ℤ[i] 𝑁 = ((abs‘𝑥)↑2))
150129, 146, 149syl2anc 579 . 2 (𝜑 → ∃𝑥 ∈ ℤ[i] 𝑁 = ((abs‘𝑥)↑2))
151 2sq.1 . . 3 𝑆 = ran (𝑤 ∈ ℤ[i] ↦ ((abs‘𝑤)↑2))
1521512sqlem1 25433 . 2 (𝑁𝑆 ↔ ∃𝑥 ∈ ℤ[i] 𝑁 = ((abs‘𝑥)↑2))
153150, 152sylibr 225 1 (𝜑𝑁𝑆)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 197  wa 384   = wceq 1652  wcel 2155  wne 2937  wrex 3056   class class class wbr 4809  cmpt 4888  ran crn 5278  cfv 6068  (class class class)co 6842  cc 10187  0cc0 10189  ici 10191   + caddc 10192   · cmul 10194   / cdiv 10938  cn 11274  2c2 11327  cz 11624  cexp 13067  cre 14122  cim 14123  abscabs 14259  cdvds 15265  cprime 15665  ℤ[i]cgz 15912
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2070  ax-7 2105  ax-8 2157  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-13 2352  ax-ext 2743  ax-sep 4941  ax-nul 4949  ax-pow 5001  ax-pr 5062  ax-un 7147  ax-cnex 10245  ax-resscn 10246  ax-1cn 10247  ax-icn 10248  ax-addcl 10249  ax-addrcl 10250  ax-mulcl 10251  ax-mulrcl 10252  ax-mulcom 10253  ax-addass 10254  ax-mulass 10255  ax-distr 10256  ax-i2m1 10257  ax-1ne0 10258  ax-1rid 10259  ax-rnegex 10260  ax-rrecex 10261  ax-cnre 10262  ax-pre-lttri 10263  ax-pre-lttrn 10264  ax-pre-ltadd 10265  ax-pre-mulgt0 10266  ax-pre-sup 10267
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-3or 1108  df-3an 1109  df-tru 1656  df-ex 1875  df-nf 1879  df-sb 2063  df-mo 2565  df-eu 2582  df-clab 2752  df-cleq 2758  df-clel 2761  df-nfc 2896  df-ne 2938  df-nel 3041  df-ral 3060  df-rex 3061  df-reu 3062  df-rmo 3063  df-rab 3064  df-v 3352  df-sbc 3597  df-csb 3692  df-dif 3735  df-un 3737  df-in 3739  df-ss 3746  df-pss 3748  df-nul 4080  df-if 4244  df-pw 4317  df-sn 4335  df-pr 4337  df-tp 4339  df-op 4341  df-uni 4595  df-iun 4678  df-br 4810  df-opab 4872  df-mpt 4889  df-tr 4912  df-id 5185  df-eprel 5190  df-po 5198  df-so 5199  df-fr 5236  df-we 5238  df-xp 5283  df-rel 5284  df-cnv 5285  df-co 5286  df-dm 5287  df-rn 5288  df-res 5289  df-ima 5290  df-pred 5865  df-ord 5911  df-on 5912  df-lim 5913  df-suc 5914  df-iota 6031  df-fun 6070  df-fn 6071  df-f 6072  df-f1 6073  df-fo 6074  df-f1o 6075  df-fv 6076  df-riota 6803  df-ov 6845  df-oprab 6846  df-mpt2 6847  df-om 7264  df-2nd 7367  df-wrecs 7610  df-recs 7672  df-rdg 7710  df-1o 7764  df-2o 7765  df-er 7947  df-en 8161  df-dom 8162  df-sdom 8163  df-fin 8164  df-sup 8555  df-inf 8556  df-pnf 10330  df-mnf 10331  df-xr 10332  df-ltxr 10333  df-le 10334  df-sub 10522  df-neg 10523  df-div 10939  df-nn 11275  df-2 11335  df-3 11336  df-n0 11539  df-z 11625  df-uz 11887  df-rp 12029  df-fl 12801  df-mod 12877  df-seq 13009  df-exp 13068  df-cj 14124  df-re 14125  df-im 14126  df-sqrt 14260  df-abs 14261  df-dvds 15266  df-gcd 15498  df-prm 15666  df-gz 15913
This theorem is referenced by:  2sqlem4  25437
  Copyright terms: Public domain W3C validator