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

Theorem 2sqlem3 24889
Description: Lemma for 2sqlem5 24891. (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 15429 . . . . . . . 8 ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (𝐴 + (i · 𝐵)) ∈ ℤ[i])
41, 2, 3syl2anc 690 . . . . . . 7 (𝜑 → (𝐴 + (i · 𝐵)) ∈ ℤ[i])
5 2sqlem4.5 . . . . . . . 8 (𝜑𝐶 ∈ ℤ)
6 2sqlem4.6 . . . . . . . 8 (𝜑𝐷 ∈ ℤ)
7 gzreim 15429 . . . . . . . 8 ((𝐶 ∈ ℤ ∧ 𝐷 ∈ ℤ) → (𝐶 + (i · 𝐷)) ∈ ℤ[i])
85, 6, 7syl2anc 690 . . . . . . 7 (𝜑 → (𝐶 + (i · 𝐷)) ∈ ℤ[i])
9 gzmulcl 15428 . . . . . . 7 (((𝐴 + (i · 𝐵)) ∈ ℤ[i] ∧ (𝐶 + (i · 𝐷)) ∈ ℤ[i]) → ((𝐴 + (i · 𝐵)) · (𝐶 + (i · 𝐷))) ∈ ℤ[i])
104, 8, 9syl2anc 690 . . . . . 6 (𝜑 → ((𝐴 + (i · 𝐵)) · (𝐶 + (i · 𝐷))) ∈ ℤ[i])
11 gzcn 15422 . . . . . 6 (((𝐴 + (i · 𝐵)) · (𝐶 + (i · 𝐷))) ∈ ℤ[i] → ((𝐴 + (i · 𝐵)) · (𝐶 + (i · 𝐷))) ∈ ℂ)
1210, 11syl 17 . . . . 5 (𝜑 → ((𝐴 + (i · 𝐵)) · (𝐶 + (i · 𝐷))) ∈ ℂ)
13 2sqlem5.2 . . . . . . 7 (𝜑𝑃 ∈ ℙ)
14 prmnn 15174 . . . . . . 7 (𝑃 ∈ ℙ → 𝑃 ∈ ℕ)
1513, 14syl 17 . . . . . 6 (𝜑𝑃 ∈ ℕ)
1615nncnd 10885 . . . . 5 (𝜑𝑃 ∈ ℂ)
1715nnne0d 10914 . . . . 5 (𝜑𝑃 ≠ 0)
1812, 16, 17divcld 10652 . . . 4 (𝜑 → (((𝐴 + (i · 𝐵)) · (𝐶 + (i · 𝐷))) / 𝑃) ∈ ℂ)
1915nnred 10884 . . . . . 6 (𝜑𝑃 ∈ ℝ)
2019, 12, 17redivd 13765 . . . . 5 (𝜑 → (ℜ‘(((𝐴 + (i · 𝐵)) · (𝐶 + (i · 𝐷))) / 𝑃)) = ((ℜ‘((𝐴 + (i · 𝐵)) · (𝐶 + (i · 𝐷)))) / 𝑃))
21 prmz 15175 . . . . . . . . . . . . . 14 (𝑃 ∈ ℙ → 𝑃 ∈ ℤ)
2213, 21syl 17 . . . . . . . . . . . . 13 (𝜑𝑃 ∈ ℤ)
23 dvdsmul2 14790 . . . . . . . . . . . . 13 ((𝑃 ∈ ℤ ∧ 𝑃 ∈ ℤ) → 𝑃 ∥ (𝑃 · 𝑃))
2422, 22, 23syl2anc 690 . . . . . . . . . . . 12 (𝜑𝑃 ∥ (𝑃 · 𝑃))
2516sqvald 12824 . . . . . . . . . . . 12 (𝜑 → (𝑃↑2) = (𝑃 · 𝑃))
2624, 25breqtrrd 4605 . . . . . . . . . . 11 (𝜑𝑃 ∥ (𝑃↑2))
27 2sqlem5.1 . . . . . . . . . . . . 13 (𝜑𝑁 ∈ ℕ)
2827nnzd 11315 . . . . . . . . . . . 12 (𝜑𝑁 ∈ ℤ)
29 zsqcl 12753 . . . . . . . . . . . . 13 (𝑃 ∈ ℤ → (𝑃↑2) ∈ ℤ)
3022, 29syl 17 . . . . . . . . . . . 12 (𝜑 → (𝑃↑2) ∈ ℤ)
31 dvdsmul2 14790 . . . . . . . . . . . 12 ((𝑁 ∈ ℤ ∧ (𝑃↑2) ∈ ℤ) → (𝑃↑2) ∥ (𝑁 · (𝑃↑2)))
3228, 30, 31syl2anc 690 . . . . . . . . . . 11 (𝜑 → (𝑃↑2) ∥ (𝑁 · (𝑃↑2)))
3328, 30zmulcld 11322 . . . . . . . . . . . 12 (𝜑 → (𝑁 · (𝑃↑2)) ∈ ℤ)
34 dvdstr 14804 . . . . . . . . . . . 12 ((𝑃 ∈ ℤ ∧ (𝑃↑2) ∈ ℤ ∧ (𝑁 · (𝑃↑2)) ∈ ℤ) → ((𝑃 ∥ (𝑃↑2) ∧ (𝑃↑2) ∥ (𝑁 · (𝑃↑2))) → 𝑃 ∥ (𝑁 · (𝑃↑2))))
3522, 30, 33, 34syl3anc 1317 . . . . . . . . . . 11 (𝜑 → ((𝑃 ∥ (𝑃↑2) ∧ (𝑃↑2) ∥ (𝑁 · (𝑃↑2))) → 𝑃 ∥ (𝑁 · (𝑃↑2))))
3626, 32, 35mp2and 710 . . . . . . . . . 10 (𝜑𝑃 ∥ (𝑁 · (𝑃↑2)))
37 gzcn 15422 . . . . . . . . . . . . . . . 16 ((𝐴 + (i · 𝐵)) ∈ ℤ[i] → (𝐴 + (i · 𝐵)) ∈ ℂ)
384, 37syl 17 . . . . . . . . . . . . . . 15 (𝜑 → (𝐴 + (i · 𝐵)) ∈ ℂ)
3938abscld 13971 . . . . . . . . . . . . . 14 (𝜑 → (abs‘(𝐴 + (i · 𝐵))) ∈ ℝ)
4039recnd 9924 . . . . . . . . . . . . 13 (𝜑 → (abs‘(𝐴 + (i · 𝐵))) ∈ ℂ)
41 gzcn 15422 . . . . . . . . . . . . . . . 16 ((𝐶 + (i · 𝐷)) ∈ ℤ[i] → (𝐶 + (i · 𝐷)) ∈ ℂ)
428, 41syl 17 . . . . . . . . . . . . . . 15 (𝜑 → (𝐶 + (i · 𝐷)) ∈ ℂ)
4342abscld 13971 . . . . . . . . . . . . . 14 (𝜑 → (abs‘(𝐶 + (i · 𝐷))) ∈ ℝ)
4443recnd 9924 . . . . . . . . . . . . 13 (𝜑 → (abs‘(𝐶 + (i · 𝐷))) ∈ ℂ)
4540, 44sqmuld 12839 . . . . . . . . . . . 12 (𝜑 → (((abs‘(𝐴 + (i · 𝐵))) · (abs‘(𝐶 + (i · 𝐷))))↑2) = (((abs‘(𝐴 + (i · 𝐵)))↑2) · ((abs‘(𝐶 + (i · 𝐷)))↑2)))
461zred 11316 . . . . . . . . . . . . . . . . 17 (𝜑𝐴 ∈ ℝ)
472zred 11316 . . . . . . . . . . . . . . . . 17 (𝜑𝐵 ∈ ℝ)
4846, 47crred 13767 . . . . . . . . . . . . . . . 16 (𝜑 → (ℜ‘(𝐴 + (i · 𝐵))) = 𝐴)
4948oveq1d 6541 . . . . . . . . . . . . . . 15 (𝜑 → ((ℜ‘(𝐴 + (i · 𝐵)))↑2) = (𝐴↑2))
5046, 47crimd 13768 . . . . . . . . . . . . . . . 16 (𝜑 → (ℑ‘(𝐴 + (i · 𝐵))) = 𝐵)
5150oveq1d 6541 . . . . . . . . . . . . . . 15 (𝜑 → ((ℑ‘(𝐴 + (i · 𝐵)))↑2) = (𝐵↑2))
5249, 51oveq12d 6544 . . . . . . . . . . . . . 14 (𝜑 → (((ℜ‘(𝐴 + (i · 𝐵)))↑2) + ((ℑ‘(𝐴 + (i · 𝐵)))↑2)) = ((𝐴↑2) + (𝐵↑2)))
5338absvalsq2d 13978 . . . . . . . . . . . . . 14 (𝜑 → ((abs‘(𝐴 + (i · 𝐵)))↑2) = (((ℜ‘(𝐴 + (i · 𝐵)))↑2) + ((ℑ‘(𝐴 + (i · 𝐵)))↑2)))
54 2sqlem4.7 . . . . . . . . . . . . . 14 (𝜑 → (𝑁 · 𝑃) = ((𝐴↑2) + (𝐵↑2)))
5552, 53, 543eqtr4d 2653 . . . . . . . . . . . . 13 (𝜑 → ((abs‘(𝐴 + (i · 𝐵)))↑2) = (𝑁 · 𝑃))
565zred 11316 . . . . . . . . . . . . . . . . 17 (𝜑𝐶 ∈ ℝ)
576zred 11316 . . . . . . . . . . . . . . . . 17 (𝜑𝐷 ∈ ℝ)
5856, 57crred 13767 . . . . . . . . . . . . . . . 16 (𝜑 → (ℜ‘(𝐶 + (i · 𝐷))) = 𝐶)
5958oveq1d 6541 . . . . . . . . . . . . . . 15 (𝜑 → ((ℜ‘(𝐶 + (i · 𝐷)))↑2) = (𝐶↑2))
6056, 57crimd 13768 . . . . . . . . . . . . . . . 16 (𝜑 → (ℑ‘(𝐶 + (i · 𝐷))) = 𝐷)
6160oveq1d 6541 . . . . . . . . . . . . . . 15 (𝜑 → ((ℑ‘(𝐶 + (i · 𝐷)))↑2) = (𝐷↑2))
6259, 61oveq12d 6544 . . . . . . . . . . . . . 14 (𝜑 → (((ℜ‘(𝐶 + (i · 𝐷)))↑2) + ((ℑ‘(𝐶 + (i · 𝐷)))↑2)) = ((𝐶↑2) + (𝐷↑2)))
6342absvalsq2d 13978 . . . . . . . . . . . . . 14 (𝜑 → ((abs‘(𝐶 + (i · 𝐷)))↑2) = (((ℜ‘(𝐶 + (i · 𝐷)))↑2) + ((ℑ‘(𝐶 + (i · 𝐷)))↑2)))
64 2sqlem4.8 . . . . . . . . . . . . . 14 (𝜑𝑃 = ((𝐶↑2) + (𝐷↑2)))
6562, 63, 643eqtr4d 2653 . . . . . . . . . . . . 13 (𝜑 → ((abs‘(𝐶 + (i · 𝐷)))↑2) = 𝑃)
6655, 65oveq12d 6544 . . . . . . . . . . . 12 (𝜑 → (((abs‘(𝐴 + (i · 𝐵)))↑2) · ((abs‘(𝐶 + (i · 𝐷)))↑2)) = ((𝑁 · 𝑃) · 𝑃))
6727nncnd 10885 . . . . . . . . . . . . 13 (𝜑𝑁 ∈ ℂ)
6867, 16, 16mulassd 9919 . . . . . . . . . . . 12 (𝜑 → ((𝑁 · 𝑃) · 𝑃) = (𝑁 · (𝑃 · 𝑃)))
6945, 66, 683eqtrd 2647 . . . . . . . . . . 11 (𝜑 → (((abs‘(𝐴 + (i · 𝐵))) · (abs‘(𝐶 + (i · 𝐷))))↑2) = (𝑁 · (𝑃 · 𝑃)))
7038, 42absmuld 13989 . . . . . . . . . . . 12 (𝜑 → (abs‘((𝐴 + (i · 𝐵)) · (𝐶 + (i · 𝐷)))) = ((abs‘(𝐴 + (i · 𝐵))) · (abs‘(𝐶 + (i · 𝐷)))))
7170oveq1d 6541 . . . . . . . . . . 11 (𝜑 → ((abs‘((𝐴 + (i · 𝐵)) · (𝐶 + (i · 𝐷))))↑2) = (((abs‘(𝐴 + (i · 𝐵))) · (abs‘(𝐶 + (i · 𝐷))))↑2))
7225oveq2d 6542 . . . . . . . . . . 11 (𝜑 → (𝑁 · (𝑃↑2)) = (𝑁 · (𝑃 · 𝑃)))
7369, 71, 723eqtr4d 2653 . . . . . . . . . 10 (𝜑 → ((abs‘((𝐴 + (i · 𝐵)) · (𝐶 + (i · 𝐷))))↑2) = (𝑁 · (𝑃↑2)))
7436, 73breqtrrd 4605 . . . . . . . . 9 (𝜑𝑃 ∥ ((abs‘((𝐴 + (i · 𝐵)) · (𝐶 + (i · 𝐷))))↑2))
7512absvalsq2d 13978 . . . . . . . . . 10 (𝜑 → ((abs‘((𝐴 + (i · 𝐵)) · (𝐶 + (i · 𝐷))))↑2) = (((ℜ‘((𝐴 + (i · 𝐵)) · (𝐶 + (i · 𝐷))))↑2) + ((ℑ‘((𝐴 + (i · 𝐵)) · (𝐶 + (i · 𝐷))))↑2)))
76 elgz 15421 . . . . . . . . . . . . . . 15 (((𝐴 + (i · 𝐵)) · (𝐶 + (i · 𝐷))) ∈ ℤ[i] ↔ (((𝐴 + (i · 𝐵)) · (𝐶 + (i · 𝐷))) ∈ ℂ ∧ (ℜ‘((𝐴 + (i · 𝐵)) · (𝐶 + (i · 𝐷)))) ∈ ℤ ∧ (ℑ‘((𝐴 + (i · 𝐵)) · (𝐶 + (i · 𝐷)))) ∈ ℤ))
7776simp2bi 1069 . . . . . . . . . . . . . 14 (((𝐴 + (i · 𝐵)) · (𝐶 + (i · 𝐷))) ∈ ℤ[i] → (ℜ‘((𝐴 + (i · 𝐵)) · (𝐶 + (i · 𝐷)))) ∈ ℤ)
7810, 77syl 17 . . . . . . . . . . . . 13 (𝜑 → (ℜ‘((𝐴 + (i · 𝐵)) · (𝐶 + (i · 𝐷)))) ∈ ℤ)
79 zsqcl 12753 . . . . . . . . . . . . 13 ((ℜ‘((𝐴 + (i · 𝐵)) · (𝐶 + (i · 𝐷)))) ∈ ℤ → ((ℜ‘((𝐴 + (i · 𝐵)) · (𝐶 + (i · 𝐷))))↑2) ∈ ℤ)
8078, 79syl 17 . . . . . . . . . . . 12 (𝜑 → ((ℜ‘((𝐴 + (i · 𝐵)) · (𝐶 + (i · 𝐷))))↑2) ∈ ℤ)
8180zcnd 11317 . . . . . . . . . . 11 (𝜑 → ((ℜ‘((𝐴 + (i · 𝐵)) · (𝐶 + (i · 𝐷))))↑2) ∈ ℂ)
8276simp3bi 1070 . . . . . . . . . . . . . 14 (((𝐴 + (i · 𝐵)) · (𝐶 + (i · 𝐷))) ∈ ℤ[i] → (ℑ‘((𝐴 + (i · 𝐵)) · (𝐶 + (i · 𝐷)))) ∈ ℤ)
8310, 82syl 17 . . . . . . . . . . . . 13 (𝜑 → (ℑ‘((𝐴 + (i · 𝐵)) · (𝐶 + (i · 𝐷)))) ∈ ℤ)
84 zsqcl 12753 . . . . . . . . . . . . 13 ((ℑ‘((𝐴 + (i · 𝐵)) · (𝐶 + (i · 𝐷)))) ∈ ℤ → ((ℑ‘((𝐴 + (i · 𝐵)) · (𝐶 + (i · 𝐷))))↑2) ∈ ℤ)
8583, 84syl 17 . . . . . . . . . . . 12 (𝜑 → ((ℑ‘((𝐴 + (i · 𝐵)) · (𝐶 + (i · 𝐷))))↑2) ∈ ℤ)
8685zcnd 11317 . . . . . . . . . . 11 (𝜑 → ((ℑ‘((𝐴 + (i · 𝐵)) · (𝐶 + (i · 𝐷))))↑2) ∈ ℂ)
8781, 86addcomd 10089 . . . . . . . . . 10 (𝜑 → (((ℜ‘((𝐴 + (i · 𝐵)) · (𝐶 + (i · 𝐷))))↑2) + ((ℑ‘((𝐴 + (i · 𝐵)) · (𝐶 + (i · 𝐷))))↑2)) = (((ℑ‘((𝐴 + (i · 𝐵)) · (𝐶 + (i · 𝐷))))↑2) + ((ℜ‘((𝐴 + (i · 𝐵)) · (𝐶 + (i · 𝐷))))↑2)))
8875, 87eqtrd 2643 . . . . . . . . 9 (𝜑 → ((abs‘((𝐴 + (i · 𝐵)) · (𝐶 + (i · 𝐷))))↑2) = (((ℑ‘((𝐴 + (i · 𝐵)) · (𝐶 + (i · 𝐷))))↑2) + ((ℜ‘((𝐴 + (i · 𝐵)) · (𝐶 + (i · 𝐷))))↑2)))
8974, 88breqtrd 4603 . . . . . . . 8 (𝜑𝑃 ∥ (((ℑ‘((𝐴 + (i · 𝐵)) · (𝐶 + (i · 𝐷))))↑2) + ((ℜ‘((𝐴 + (i · 𝐵)) · (𝐶 + (i · 𝐷))))↑2)))
90 2sqlem4.9 . . . . . . . . . . . 12 (𝜑𝑃 ∥ ((𝐶 · 𝐵) + (𝐴 · 𝐷)))
915zcnd 11317 . . . . . . . . . . . . . . 15 (𝜑𝐶 ∈ ℂ)
922zcnd 11317 . . . . . . . . . . . . . . 15 (𝜑𝐵 ∈ ℂ)
9391, 92mulcld 9916 . . . . . . . . . . . . . 14 (𝜑 → (𝐶 · 𝐵) ∈ ℂ)
941zcnd 11317 . . . . . . . . . . . . . . 15 (𝜑𝐴 ∈ ℂ)
956zcnd 11317 . . . . . . . . . . . . . . 15 (𝜑𝐷 ∈ ℂ)
9694, 95mulcld 9916 . . . . . . . . . . . . . 14 (𝜑 → (𝐴 · 𝐷) ∈ ℂ)
9793, 96addcomd 10089 . . . . . . . . . . . . 13 (𝜑 → ((𝐶 · 𝐵) + (𝐴 · 𝐷)) = ((𝐴 · 𝐷) + (𝐶 · 𝐵)))
9891, 92mulcomd 9917 . . . . . . . . . . . . . 14 (𝜑 → (𝐶 · 𝐵) = (𝐵 · 𝐶))
9998oveq2d 6542 . . . . . . . . . . . . 13 (𝜑 → ((𝐴 · 𝐷) + (𝐶 · 𝐵)) = ((𝐴 · 𝐷) + (𝐵 · 𝐶)))
10097, 99eqtrd 2643 . . . . . . . . . . . 12 (𝜑 → ((𝐶 · 𝐵) + (𝐴 · 𝐷)) = ((𝐴 · 𝐷) + (𝐵 · 𝐶)))
10190, 100breqtrd 4603 . . . . . . . . . . 11 (𝜑𝑃 ∥ ((𝐴 · 𝐷) + (𝐵 · 𝐶)))
10238, 42immuld 13755 . . . . . . . . . . . 12 (𝜑 → (ℑ‘((𝐴 + (i · 𝐵)) · (𝐶 + (i · 𝐷)))) = (((ℜ‘(𝐴 + (i · 𝐵))) · (ℑ‘(𝐶 + (i · 𝐷)))) + ((ℑ‘(𝐴 + (i · 𝐵))) · (ℜ‘(𝐶 + (i · 𝐷))))))
10348, 60oveq12d 6544 . . . . . . . . . . . . 13 (𝜑 → ((ℜ‘(𝐴 + (i · 𝐵))) · (ℑ‘(𝐶 + (i · 𝐷)))) = (𝐴 · 𝐷))
10450, 58oveq12d 6544 . . . . . . . . . . . . 13 (𝜑 → ((ℑ‘(𝐴 + (i · 𝐵))) · (ℜ‘(𝐶 + (i · 𝐷)))) = (𝐵 · 𝐶))
105103, 104oveq12d 6544 . . . . . . . . . . . 12 (𝜑 → (((ℜ‘(𝐴 + (i · 𝐵))) · (ℑ‘(𝐶 + (i · 𝐷)))) + ((ℑ‘(𝐴 + (i · 𝐵))) · (ℜ‘(𝐶 + (i · 𝐷))))) = ((𝐴 · 𝐷) + (𝐵 · 𝐶)))
106102, 105eqtrd 2643 . . . . . . . . . . 11 (𝜑 → (ℑ‘((𝐴 + (i · 𝐵)) · (𝐶 + (i · 𝐷)))) = ((𝐴 · 𝐷) + (𝐵 · 𝐶)))
107101, 106breqtrrd 4605 . . . . . . . . . 10 (𝜑𝑃 ∥ (ℑ‘((𝐴 + (i · 𝐵)) · (𝐶 + (i · 𝐷)))))
108 2nn 11034 . . . . . . . . . . . 12 2 ∈ ℕ
109108a1i 11 . . . . . . . . . . 11 (𝜑 → 2 ∈ ℕ)
110 prmdvdsexp 15213 . . . . . . . . . . 11 ((𝑃 ∈ ℙ ∧ (ℑ‘((𝐴 + (i · 𝐵)) · (𝐶 + (i · 𝐷)))) ∈ ℤ ∧ 2 ∈ ℕ) → (𝑃 ∥ ((ℑ‘((𝐴 + (i · 𝐵)) · (𝐶 + (i · 𝐷))))↑2) ↔ 𝑃 ∥ (ℑ‘((𝐴 + (i · 𝐵)) · (𝐶 + (i · 𝐷))))))
11113, 83, 109, 110syl3anc 1317 . . . . . . . . . 10 (𝜑 → (𝑃 ∥ ((ℑ‘((𝐴 + (i · 𝐵)) · (𝐶 + (i · 𝐷))))↑2) ↔ 𝑃 ∥ (ℑ‘((𝐴 + (i · 𝐵)) · (𝐶 + (i · 𝐷))))))
112107, 111mpbird 245 . . . . . . . . 9 (𝜑𝑃 ∥ ((ℑ‘((𝐴 + (i · 𝐵)) · (𝐶 + (i · 𝐷))))↑2))
113 dvdsadd2b 14814 . . . . . . . . 9 ((𝑃 ∈ ℤ ∧ ((ℜ‘((𝐴 + (i · 𝐵)) · (𝐶 + (i · 𝐷))))↑2) ∈ ℤ ∧ (((ℑ‘((𝐴 + (i · 𝐵)) · (𝐶 + (i · 𝐷))))↑2) ∈ ℤ ∧ 𝑃 ∥ ((ℑ‘((𝐴 + (i · 𝐵)) · (𝐶 + (i · 𝐷))))↑2))) → (𝑃 ∥ ((ℜ‘((𝐴 + (i · 𝐵)) · (𝐶 + (i · 𝐷))))↑2) ↔ 𝑃 ∥ (((ℑ‘((𝐴 + (i · 𝐵)) · (𝐶 + (i · 𝐷))))↑2) + ((ℜ‘((𝐴 + (i · 𝐵)) · (𝐶 + (i · 𝐷))))↑2))))
11422, 80, 85, 112, 113syl112anc 1321 . . . . . . . 8 (𝜑 → (𝑃 ∥ ((ℜ‘((𝐴 + (i · 𝐵)) · (𝐶 + (i · 𝐷))))↑2) ↔ 𝑃 ∥ (((ℑ‘((𝐴 + (i · 𝐵)) · (𝐶 + (i · 𝐷))))↑2) + ((ℜ‘((𝐴 + (i · 𝐵)) · (𝐶 + (i · 𝐷))))↑2))))
11589, 114mpbird 245 . . . . . . 7 (𝜑𝑃 ∥ ((ℜ‘((𝐴 + (i · 𝐵)) · (𝐶 + (i · 𝐷))))↑2))
116 prmdvdsexp 15213 . . . . . . . 8 ((𝑃 ∈ ℙ ∧ (ℜ‘((𝐴 + (i · 𝐵)) · (𝐶 + (i · 𝐷)))) ∈ ℤ ∧ 2 ∈ ℕ) → (𝑃 ∥ ((ℜ‘((𝐴 + (i · 𝐵)) · (𝐶 + (i · 𝐷))))↑2) ↔ 𝑃 ∥ (ℜ‘((𝐴 + (i · 𝐵)) · (𝐶 + (i · 𝐷))))))
11713, 78, 109, 116syl3anc 1317 . . . . . . 7 (𝜑 → (𝑃 ∥ ((ℜ‘((𝐴 + (i · 𝐵)) · (𝐶 + (i · 𝐷))))↑2) ↔ 𝑃 ∥ (ℜ‘((𝐴 + (i · 𝐵)) · (𝐶 + (i · 𝐷))))))
118115, 117mpbid 220 . . . . . 6 (𝜑𝑃 ∥ (ℜ‘((𝐴 + (i · 𝐵)) · (𝐶 + (i · 𝐷)))))
119 dvdsval2 14772 . . . . . . 7 ((𝑃 ∈ ℤ ∧ 𝑃 ≠ 0 ∧ (ℜ‘((𝐴 + (i · 𝐵)) · (𝐶 + (i · 𝐷)))) ∈ ℤ) → (𝑃 ∥ (ℜ‘((𝐴 + (i · 𝐵)) · (𝐶 + (i · 𝐷)))) ↔ ((ℜ‘((𝐴 + (i · 𝐵)) · (𝐶 + (i · 𝐷)))) / 𝑃) ∈ ℤ))
12022, 17, 78, 119syl3anc 1317 . . . . . 6 (𝜑 → (𝑃 ∥ (ℜ‘((𝐴 + (i · 𝐵)) · (𝐶 + (i · 𝐷)))) ↔ ((ℜ‘((𝐴 + (i · 𝐵)) · (𝐶 + (i · 𝐷)))) / 𝑃) ∈ ℤ))
121118, 120mpbid 220 . . . . 5 (𝜑 → ((ℜ‘((𝐴 + (i · 𝐵)) · (𝐶 + (i · 𝐷)))) / 𝑃) ∈ ℤ)
12220, 121eqeltrd 2687 . . . 4 (𝜑 → (ℜ‘(((𝐴 + (i · 𝐵)) · (𝐶 + (i · 𝐷))) / 𝑃)) ∈ ℤ)
12319, 12, 17imdivd 13766 . . . . 5 (𝜑 → (ℑ‘(((𝐴 + (i · 𝐵)) · (𝐶 + (i · 𝐷))) / 𝑃)) = ((ℑ‘((𝐴 + (i · 𝐵)) · (𝐶 + (i · 𝐷)))) / 𝑃))
124 dvdsval2 14772 . . . . . . 7 ((𝑃 ∈ ℤ ∧ 𝑃 ≠ 0 ∧ (ℑ‘((𝐴 + (i · 𝐵)) · (𝐶 + (i · 𝐷)))) ∈ ℤ) → (𝑃 ∥ (ℑ‘((𝐴 + (i · 𝐵)) · (𝐶 + (i · 𝐷)))) ↔ ((ℑ‘((𝐴 + (i · 𝐵)) · (𝐶 + (i · 𝐷)))) / 𝑃) ∈ ℤ))
12522, 17, 83, 124syl3anc 1317 . . . . . 6 (𝜑 → (𝑃 ∥ (ℑ‘((𝐴 + (i · 𝐵)) · (𝐶 + (i · 𝐷)))) ↔ ((ℑ‘((𝐴 + (i · 𝐵)) · (𝐶 + (i · 𝐷)))) / 𝑃) ∈ ℤ))
126107, 125mpbid 220 . . . . 5 (𝜑 → ((ℑ‘((𝐴 + (i · 𝐵)) · (𝐶 + (i · 𝐷)))) / 𝑃) ∈ ℤ)
127123, 126eqeltrd 2687 . . . 4 (𝜑 → (ℑ‘(((𝐴 + (i · 𝐵)) · (𝐶 + (i · 𝐷))) / 𝑃)) ∈ ℤ)
128 elgz 15421 . . . 4 ((((𝐴 + (i · 𝐵)) · (𝐶 + (i · 𝐷))) / 𝑃) ∈ ℤ[i] ↔ ((((𝐴 + (i · 𝐵)) · (𝐶 + (i · 𝐷))) / 𝑃) ∈ ℂ ∧ (ℜ‘(((𝐴 + (i · 𝐵)) · (𝐶 + (i · 𝐷))) / 𝑃)) ∈ ℤ ∧ (ℑ‘(((𝐴 + (i · 𝐵)) · (𝐶 + (i · 𝐷))) / 𝑃)) ∈ ℤ))
12918, 122, 127, 128syl3anbrc 1238 . . 3 (𝜑 → (((𝐴 + (i · 𝐵)) · (𝐶 + (i · 𝐷))) / 𝑃) ∈ ℤ[i])
13012, 16, 17absdivd 13990 . . . . . 6 (𝜑 → (abs‘(((𝐴 + (i · 𝐵)) · (𝐶 + (i · 𝐷))) / 𝑃)) = ((abs‘((𝐴 + (i · 𝐵)) · (𝐶 + (i · 𝐷)))) / (abs‘𝑃)))
13115nnnn0d 11200 . . . . . . . . 9 (𝜑𝑃 ∈ ℕ0)
132131nn0ge0d 11203 . . . . . . . 8 (𝜑 → 0 ≤ 𝑃)
13319, 132absidd 13957 . . . . . . 7 (𝜑 → (abs‘𝑃) = 𝑃)
134133oveq2d 6542 . . . . . 6 (𝜑 → ((abs‘((𝐴 + (i · 𝐵)) · (𝐶 + (i · 𝐷)))) / (abs‘𝑃)) = ((abs‘((𝐴 + (i · 𝐵)) · (𝐶 + (i · 𝐷)))) / 𝑃))
135130, 134eqtrd 2643 . . . . 5 (𝜑 → (abs‘(((𝐴 + (i · 𝐵)) · (𝐶 + (i · 𝐷))) / 𝑃)) = ((abs‘((𝐴 + (i · 𝐵)) · (𝐶 + (i · 𝐷)))) / 𝑃))
136135oveq1d 6541 . . . 4 (𝜑 → ((abs‘(((𝐴 + (i · 𝐵)) · (𝐶 + (i · 𝐷))) / 𝑃))↑2) = (((abs‘((𝐴 + (i · 𝐵)) · (𝐶 + (i · 𝐷)))) / 𝑃)↑2))
13712abscld 13971 . . . . . 6 (𝜑 → (abs‘((𝐴 + (i · 𝐵)) · (𝐶 + (i · 𝐷)))) ∈ ℝ)
138137recnd 9924 . . . . 5 (𝜑 → (abs‘((𝐴 + (i · 𝐵)) · (𝐶 + (i · 𝐷)))) ∈ ℂ)
139138, 16, 17sqdivd 12840 . . . 4 (𝜑 → (((abs‘((𝐴 + (i · 𝐵)) · (𝐶 + (i · 𝐷)))) / 𝑃)↑2) = (((abs‘((𝐴 + (i · 𝐵)) · (𝐶 + (i · 𝐷))))↑2) / (𝑃↑2)))
14073oveq1d 6541 . . . . 5 (𝜑 → (((abs‘((𝐴 + (i · 𝐵)) · (𝐶 + (i · 𝐷))))↑2) / (𝑃↑2)) = ((𝑁 · (𝑃↑2)) / (𝑃↑2)))
14115nnsqcld 12848 . . . . . . 7 (𝜑 → (𝑃↑2) ∈ ℕ)
142141nncnd 10885 . . . . . 6 (𝜑 → (𝑃↑2) ∈ ℂ)
143141nnne0d 10914 . . . . . 6 (𝜑 → (𝑃↑2) ≠ 0)
14467, 142, 143divcan4d 10658 . . . . 5 (𝜑 → ((𝑁 · (𝑃↑2)) / (𝑃↑2)) = 𝑁)
145140, 144eqtrd 2643 . . . 4 (𝜑 → (((abs‘((𝐴 + (i · 𝐵)) · (𝐶 + (i · 𝐷))))↑2) / (𝑃↑2)) = 𝑁)
146136, 139, 1453eqtrrd 2648 . . 3 (𝜑𝑁 = ((abs‘(((𝐴 + (i · 𝐵)) · (𝐶 + (i · 𝐷))) / 𝑃))↑2))
147 fveq2 6087 . . . . . 6 (𝑥 = (((𝐴 + (i · 𝐵)) · (𝐶 + (i · 𝐷))) / 𝑃) → (abs‘𝑥) = (abs‘(((𝐴 + (i · 𝐵)) · (𝐶 + (i · 𝐷))) / 𝑃)))
148147oveq1d 6541 . . . . 5 (𝑥 = (((𝐴 + (i · 𝐵)) · (𝐶 + (i · 𝐷))) / 𝑃) → ((abs‘𝑥)↑2) = ((abs‘(((𝐴 + (i · 𝐵)) · (𝐶 + (i · 𝐷))) / 𝑃))↑2))
149148eqeq2d 2619 . . . 4 (𝑥 = (((𝐴 + (i · 𝐵)) · (𝐶 + (i · 𝐷))) / 𝑃) → (𝑁 = ((abs‘𝑥)↑2) ↔ 𝑁 = ((abs‘(((𝐴 + (i · 𝐵)) · (𝐶 + (i · 𝐷))) / 𝑃))↑2)))
150149rspcev 3281 . . 3 (((((𝐴 + (i · 𝐵)) · (𝐶 + (i · 𝐷))) / 𝑃) ∈ ℤ[i] ∧ 𝑁 = ((abs‘(((𝐴 + (i · 𝐵)) · (𝐶 + (i · 𝐷))) / 𝑃))↑2)) → ∃𝑥 ∈ ℤ[i] 𝑁 = ((abs‘𝑥)↑2))
151129, 146, 150syl2anc 690 . 2 (𝜑 → ∃𝑥 ∈ ℤ[i] 𝑁 = ((abs‘𝑥)↑2))
152 2sq.1 . . 3 𝑆 = ran (𝑤 ∈ ℤ[i] ↦ ((abs‘𝑤)↑2))
1531522sqlem1 24886 . 2 (𝑁𝑆 ↔ ∃𝑥 ∈ ℤ[i] 𝑁 = ((abs‘𝑥)↑2))
154151, 153sylibr 222 1 (𝜑𝑁𝑆)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 194  wa 382   = wceq 1474  wcel 1976  wne 2779  wrex 2896   class class class wbr 4577  cmpt 4637  ran crn 5028  cfv 5789  (class class class)co 6526  cc 9790  0cc0 9792  ici 9794   + caddc 9795   · cmul 9797   / cdiv 10535  cn 10869  2c2 10919  cz 11212  cexp 12679  cre 13633  cim 13634  abscabs 13770  cdvds 14769  cprime 15171  ℤ[i]cgz 15419
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-8 1978  ax-9 1985  ax-10 2005  ax-11 2020  ax-12 2033  ax-13 2233  ax-ext 2589  ax-sep 4703  ax-nul 4711  ax-pow 4763  ax-pr 4827  ax-un 6824  ax-cnex 9848  ax-resscn 9849  ax-1cn 9850  ax-icn 9851  ax-addcl 9852  ax-addrcl 9853  ax-mulcl 9854  ax-mulrcl 9855  ax-mulcom 9856  ax-addass 9857  ax-mulass 9858  ax-distr 9859  ax-i2m1 9860  ax-1ne0 9861  ax-1rid 9862  ax-rnegex 9863  ax-rrecex 9864  ax-cnre 9865  ax-pre-lttri 9866  ax-pre-lttrn 9867  ax-pre-ltadd 9868  ax-pre-mulgt0 9869  ax-pre-sup 9870
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3or 1031  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-eu 2461  df-mo 2462  df-clab 2596  df-cleq 2602  df-clel 2605  df-nfc 2739  df-ne 2781  df-nel 2782  df-ral 2900  df-rex 2901  df-reu 2902  df-rmo 2903  df-rab 2904  df-v 3174  df-sbc 3402  df-csb 3499  df-dif 3542  df-un 3544  df-in 3546  df-ss 3553  df-pss 3555  df-nul 3874  df-if 4036  df-pw 4109  df-sn 4125  df-pr 4127  df-tp 4129  df-op 4131  df-uni 4367  df-int 4405  df-iun 4451  df-br 4578  df-opab 4638  df-mpt 4639  df-tr 4675  df-eprel 4938  df-id 4942  df-po 4948  df-so 4949  df-fr 4986  df-we 4988  df-xp 5033  df-rel 5034  df-cnv 5035  df-co 5036  df-dm 5037  df-rn 5038  df-res 5039  df-ima 5040  df-pred 5582  df-ord 5628  df-on 5629  df-lim 5630  df-suc 5631  df-iota 5753  df-fun 5791  df-fn 5792  df-f 5793  df-f1 5794  df-fo 5795  df-f1o 5796  df-fv 5797  df-riota 6488  df-ov 6529  df-oprab 6530  df-mpt2 6531  df-om 6935  df-2nd 7037  df-wrecs 7271  df-recs 7332  df-rdg 7370  df-1o 7424  df-2o 7425  df-oadd 7428  df-er 7606  df-en 7819  df-dom 7820  df-sdom 7821  df-fin 7822  df-sup 8208  df-inf 8209  df-pnf 9932  df-mnf 9933  df-xr 9934  df-ltxr 9935  df-le 9936  df-sub 10119  df-neg 10120  df-div 10536  df-nn 10870  df-2 10928  df-3 10929  df-n0 11142  df-z 11213  df-uz 11522  df-rp 11667  df-fl 12412  df-mod 12488  df-seq 12621  df-exp 12680  df-cj 13635  df-re 13636  df-im 13637  df-sqrt 13771  df-abs 13772  df-dvds 14770  df-gcd 15003  df-prm 15172  df-gz 15420
This theorem is referenced by:  2sqlem4  24890
  Copyright terms: Public domain W3C validator