Metamath Proof Explorer

Theorem 2sqlem3

Description: Lemma for 2sqlem5 . (Contributed by Mario Carneiro, 20-Jun-2015)

Ref Expression
Hypotheses 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 2sqlem3 ( 𝜑 → 𝑁 ∈ 𝑆 )

Proof

Step Hyp Ref Expression
1 2sq.1 ⊢ 𝑆 = ran ( 𝑤 ∈ ℤ[i] ↦ ( ( abs ‘ 𝑤 ) ↑ 2 ) )
2 2sqlem5.1 ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
3 2sqlem5.2 ⊢ ( 𝜑 → 𝑃 ∈ ℙ )
4 2sqlem4.3 ⊢ ( 𝜑 → 𝐴 ∈ ℤ )
5 2sqlem4.4 ⊢ ( 𝜑 → 𝐵 ∈ ℤ )
6 2sqlem4.5 ⊢ ( 𝜑 → 𝐶 ∈ ℤ )
7 2sqlem4.6 ⊢ ( 𝜑 → 𝐷 ∈ ℤ )
8 2sqlem4.7 ⊢ ( 𝜑 → ( 𝑁 · 𝑃 ) = ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) )
9 2sqlem4.8 ⊢ ( 𝜑 → 𝑃 = ( ( 𝐶 ↑ 2 ) + ( 𝐷 ↑ 2 ) ) )
10 2sqlem4.9 ⊢ ( 𝜑 → 𝑃 ∥ ( ( 𝐶 · 𝐵 ) + ( 𝐴 · 𝐷 ) ) )
11 gzreim ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → ( 𝐴 + ( i · 𝐵 ) ) ∈ ℤ[i] )
12 4 5 11 syl2anc ⊢ ( 𝜑 → ( 𝐴 + ( i · 𝐵 ) ) ∈ ℤ[i] )
13 gzreim ⊢ ( ( 𝐶 ∈ ℤ ∧ 𝐷 ∈ ℤ ) → ( 𝐶 + ( i · 𝐷 ) ) ∈ ℤ[i] )
14 6 7 13 syl2anc ⊢ ( 𝜑 → ( 𝐶 + ( i · 𝐷 ) ) ∈ ℤ[i] )
15 gzmulcl ⊢ ( ( ( 𝐴 + ( i · 𝐵 ) ) ∈ ℤ[i] ∧ ( 𝐶 + ( i · 𝐷 ) ) ∈ ℤ[i] ) → ( ( 𝐴 + ( i · 𝐵 ) ) · ( 𝐶 + ( i · 𝐷 ) ) ) ∈ ℤ[i] )
16 12 14 15 syl2anc ⊢ ( 𝜑 → ( ( 𝐴 + ( i · 𝐵 ) ) · ( 𝐶 + ( i · 𝐷 ) ) ) ∈ ℤ[i] )
17 gzcn ⊢ ( ( ( 𝐴 + ( i · 𝐵 ) ) · ( 𝐶 + ( i · 𝐷 ) ) ) ∈ ℤ[i] → ( ( 𝐴 + ( i · 𝐵 ) ) · ( 𝐶 + ( i · 𝐷 ) ) ) ∈ ℂ )
18 16 17 syl ⊢ ( 𝜑 → ( ( 𝐴 + ( i · 𝐵 ) ) · ( 𝐶 + ( i · 𝐷 ) ) ) ∈ ℂ )
19 prmnn ⊢ ( 𝑃 ∈ ℙ → 𝑃 ∈ ℕ )
20 3 19 syl ⊢ ( 𝜑 → 𝑃 ∈ ℕ )
21 20 nncnd ⊢ ( 𝜑 → 𝑃 ∈ ℂ )
22 20 nnne0d ⊢ ( 𝜑 → 𝑃 ≠ 0 )
23 18 21 22 divcld ⊢ ( 𝜑 → ( ( ( 𝐴 + ( i · 𝐵 ) ) · ( 𝐶 + ( i · 𝐷 ) ) ) / 𝑃 ) ∈ ℂ )
24 20 nnred ⊢ ( 𝜑 → 𝑃 ∈ ℝ )
25 24 18 22 redivd ⊢ ( 𝜑 → ( ℜ ‘ ( ( ( 𝐴 + ( i · 𝐵 ) ) · ( 𝐶 + ( i · 𝐷 ) ) ) / 𝑃 ) ) = ( ( ℜ ‘ ( ( 𝐴 + ( i · 𝐵 ) ) · ( 𝐶 + ( i · 𝐷 ) ) ) ) / 𝑃 ) )
26 prmz ⊢ ( 𝑃 ∈ ℙ → 𝑃 ∈ ℤ )
27 3 26 syl ⊢ ( 𝜑 → 𝑃 ∈ ℤ )
28 zsqcl ⊢ ( 𝑃 ∈ ℤ → ( 𝑃 ↑ 2 ) ∈ ℤ )
29 27 28 syl ⊢ ( 𝜑 → ( 𝑃 ↑ 2 ) ∈ ℤ )
30 2 nnzd ⊢ ( 𝜑 → 𝑁 ∈ ℤ )
31 30 29 zmulcld ⊢ ( 𝜑 → ( 𝑁 · ( 𝑃 ↑ 2 ) ) ∈ ℤ )
32 dvdsmul2 ⊢ ( ( 𝑃 ∈ ℤ ∧ 𝑃 ∈ ℤ ) → 𝑃 ∥ ( 𝑃 · 𝑃 ) )
33 27 27 32 syl2anc ⊢ ( 𝜑 → 𝑃 ∥ ( 𝑃 · 𝑃 ) )
34 21 sqvald ⊢ ( 𝜑 → ( 𝑃 ↑ 2 ) = ( 𝑃 · 𝑃 ) )
35 33 34 breqtrrd ⊢ ( 𝜑 → 𝑃 ∥ ( 𝑃 ↑ 2 ) )
36 dvdsmul2 ⊢ ( ( 𝑁 ∈ ℤ ∧ ( 𝑃 ↑ 2 ) ∈ ℤ ) → ( 𝑃 ↑ 2 ) ∥ ( 𝑁 · ( 𝑃 ↑ 2 ) ) )
37 30 29 36 syl2anc ⊢ ( 𝜑 → ( 𝑃 ↑ 2 ) ∥ ( 𝑁 · ( 𝑃 ↑ 2 ) ) )
38 27 29 31 35 37 dvdstrd ⊢ ( 𝜑 → 𝑃 ∥ ( 𝑁 · ( 𝑃 ↑ 2 ) ) )
39 gzcn ⊢ ( ( 𝐴 + ( i · 𝐵 ) ) ∈ ℤ[i] → ( 𝐴 + ( i · 𝐵 ) ) ∈ ℂ )
40 12 39 syl ⊢ ( 𝜑 → ( 𝐴 + ( i · 𝐵 ) ) ∈ ℂ )
41 40 abscld ⊢ ( 𝜑 → ( abs ‘ ( 𝐴 + ( i · 𝐵 ) ) ) ∈ ℝ )
42 41 recnd ⊢ ( 𝜑 → ( abs ‘ ( 𝐴 + ( i · 𝐵 ) ) ) ∈ ℂ )
43 gzcn ⊢ ( ( 𝐶 + ( i · 𝐷 ) ) ∈ ℤ[i] → ( 𝐶 + ( i · 𝐷 ) ) ∈ ℂ )
44 14 43 syl ⊢ ( 𝜑 → ( 𝐶 + ( i · 𝐷 ) ) ∈ ℂ )
45 44 abscld ⊢ ( 𝜑 → ( abs ‘ ( 𝐶 + ( i · 𝐷 ) ) ) ∈ ℝ )
46 45 recnd ⊢ ( 𝜑 → ( abs ‘ ( 𝐶 + ( i · 𝐷 ) ) ) ∈ ℂ )
47 42 46 sqmuld ⊢ ( 𝜑 → ( ( ( abs ‘ ( 𝐴 + ( i · 𝐵 ) ) ) · ( abs ‘ ( 𝐶 + ( i · 𝐷 ) ) ) ) ↑ 2 ) = ( ( ( abs ‘ ( 𝐴 + ( i · 𝐵 ) ) ) ↑ 2 ) · ( ( abs ‘ ( 𝐶 + ( i · 𝐷 ) ) ) ↑ 2 ) ) )
48 4 zred ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
49 5 zred ⊢ ( 𝜑 → 𝐵 ∈ ℝ )
50 48 49 crred ⊢ ( 𝜑 → ( ℜ ‘ ( 𝐴 + ( i · 𝐵 ) ) ) = 𝐴 )
51 50 oveq1d ⊢ ( 𝜑 → ( ( ℜ ‘ ( 𝐴 + ( i · 𝐵 ) ) ) ↑ 2 ) = ( 𝐴 ↑ 2 ) )
52 48 49 crimd ⊢ ( 𝜑 → ( ℑ ‘ ( 𝐴 + ( i · 𝐵 ) ) ) = 𝐵 )
53 52 oveq1d ⊢ ( 𝜑 → ( ( ℑ ‘ ( 𝐴 + ( i · 𝐵 ) ) ) ↑ 2 ) = ( 𝐵 ↑ 2 ) )
54 51 53 oveq12d ⊢ ( 𝜑 → ( ( ( ℜ ‘ ( 𝐴 + ( i · 𝐵 ) ) ) ↑ 2 ) + ( ( ℑ ‘ ( 𝐴 + ( i · 𝐵 ) ) ) ↑ 2 ) ) = ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) )
55 40 absvalsq2d ⊢ ( 𝜑 → ( ( abs ‘ ( 𝐴 + ( i · 𝐵 ) ) ) ↑ 2 ) = ( ( ( ℜ ‘ ( 𝐴 + ( i · 𝐵 ) ) ) ↑ 2 ) + ( ( ℑ ‘ ( 𝐴 + ( i · 𝐵 ) ) ) ↑ 2 ) ) )
56 54 55 8 3eqtr4d ⊢ ( 𝜑 → ( ( abs ‘ ( 𝐴 + ( i · 𝐵 ) ) ) ↑ 2 ) = ( 𝑁 · 𝑃 ) )
57 6 zred ⊢ ( 𝜑 → 𝐶 ∈ ℝ )
58 7 zred ⊢ ( 𝜑 → 𝐷 ∈ ℝ )
59 57 58 crred ⊢ ( 𝜑 → ( ℜ ‘ ( 𝐶 + ( i · 𝐷 ) ) ) = 𝐶 )
60 59 oveq1d ⊢ ( 𝜑 → ( ( ℜ ‘ ( 𝐶 + ( i · 𝐷 ) ) ) ↑ 2 ) = ( 𝐶 ↑ 2 ) )
61 57 58 crimd ⊢ ( 𝜑 → ( ℑ ‘ ( 𝐶 + ( i · 𝐷 ) ) ) = 𝐷 )
62 61 oveq1d ⊢ ( 𝜑 → ( ( ℑ ‘ ( 𝐶 + ( i · 𝐷 ) ) ) ↑ 2 ) = ( 𝐷 ↑ 2 ) )
63 60 62 oveq12d ⊢ ( 𝜑 → ( ( ( ℜ ‘ ( 𝐶 + ( i · 𝐷 ) ) ) ↑ 2 ) + ( ( ℑ ‘ ( 𝐶 + ( i · 𝐷 ) ) ) ↑ 2 ) ) = ( ( 𝐶 ↑ 2 ) + ( 𝐷 ↑ 2 ) ) )
64 44 absvalsq2d ⊢ ( 𝜑 → ( ( abs ‘ ( 𝐶 + ( i · 𝐷 ) ) ) ↑ 2 ) = ( ( ( ℜ ‘ ( 𝐶 + ( i · 𝐷 ) ) ) ↑ 2 ) + ( ( ℑ ‘ ( 𝐶 + ( i · 𝐷 ) ) ) ↑ 2 ) ) )
65 63 64 9 3eqtr4d ⊢ ( 𝜑 → ( ( abs ‘ ( 𝐶 + ( i · 𝐷 ) ) ) ↑ 2 ) = 𝑃 )
66 56 65 oveq12d ⊢ ( 𝜑 → ( ( ( abs ‘ ( 𝐴 + ( i · 𝐵 ) ) ) ↑ 2 ) · ( ( abs ‘ ( 𝐶 + ( i · 𝐷 ) ) ) ↑ 2 ) ) = ( ( 𝑁 · 𝑃 ) · 𝑃 ) )
67 2 nncnd ⊢ ( 𝜑 → 𝑁 ∈ ℂ )
68 67 21 21 mulassd ⊢ ( 𝜑 → ( ( 𝑁 · 𝑃 ) · 𝑃 ) = ( 𝑁 · ( 𝑃 · 𝑃 ) ) )
69 47 66 68 3eqtrd ⊢ ( 𝜑 → ( ( ( abs ‘ ( 𝐴 + ( i · 𝐵 ) ) ) · ( abs ‘ ( 𝐶 + ( i · 𝐷 ) ) ) ) ↑ 2 ) = ( 𝑁 · ( 𝑃 · 𝑃 ) ) )
70 40 44 absmuld ⊢ ( 𝜑 → ( abs ‘ ( ( 𝐴 + ( i · 𝐵 ) ) · ( 𝐶 + ( i · 𝐷 ) ) ) ) = ( ( abs ‘ ( 𝐴 + ( i · 𝐵 ) ) ) · ( abs ‘ ( 𝐶 + ( i · 𝐷 ) ) ) ) )
71 70 oveq1d ⊢ ( 𝜑 → ( ( abs ‘ ( ( 𝐴 + ( i · 𝐵 ) ) · ( 𝐶 + ( i · 𝐷 ) ) ) ) ↑ 2 ) = ( ( ( abs ‘ ( 𝐴 + ( i · 𝐵 ) ) ) · ( abs ‘ ( 𝐶 + ( i · 𝐷 ) ) ) ) ↑ 2 ) )
72 34 oveq2d ⊢ ( 𝜑 → ( 𝑁 · ( 𝑃 ↑ 2 ) ) = ( 𝑁 · ( 𝑃 · 𝑃 ) ) )
73 69 71 72 3eqtr4d ⊢ ( 𝜑 → ( ( abs ‘ ( ( 𝐴 + ( i · 𝐵 ) ) · ( 𝐶 + ( i · 𝐷 ) ) ) ) ↑ 2 ) = ( 𝑁 · ( 𝑃 ↑ 2 ) ) )
74 38 73 breqtrrd ⊢ ( 𝜑 → 𝑃 ∥ ( ( abs ‘ ( ( 𝐴 + ( i · 𝐵 ) ) · ( 𝐶 + ( i · 𝐷 ) ) ) ) ↑ 2 ) )
75 18 absvalsq2d ⊢ ( 𝜑 → ( ( abs ‘ ( ( 𝐴 + ( i · 𝐵 ) ) · ( 𝐶 + ( i · 𝐷 ) ) ) ) ↑ 2 ) = ( ( ( ℜ ‘ ( ( 𝐴 + ( i · 𝐵 ) ) · ( 𝐶 + ( i · 𝐷 ) ) ) ) ↑ 2 ) + ( ( ℑ ‘ ( ( 𝐴 + ( i · 𝐵 ) ) · ( 𝐶 + ( i · 𝐷 ) ) ) ) ↑ 2 ) ) )
76 elgz ⊢ ( ( ( 𝐴 + ( i · 𝐵 ) ) · ( 𝐶 + ( i · 𝐷 ) ) ) ∈ ℤ[i] ↔ ( ( ( 𝐴 + ( i · 𝐵 ) ) · ( 𝐶 + ( i · 𝐷 ) ) ) ∈ ℂ ∧ ( ℜ ‘ ( ( 𝐴 + ( i · 𝐵 ) ) · ( 𝐶 + ( i · 𝐷 ) ) ) ) ∈ ℤ ∧ ( ℑ ‘ ( ( 𝐴 + ( i · 𝐵 ) ) · ( 𝐶 + ( i · 𝐷 ) ) ) ) ∈ ℤ ) )
77 76 simp2bi ⊢ ( ( ( 𝐴 + ( i · 𝐵 ) ) · ( 𝐶 + ( i · 𝐷 ) ) ) ∈ ℤ[i] → ( ℜ ‘ ( ( 𝐴 + ( i · 𝐵 ) ) · ( 𝐶 + ( i · 𝐷 ) ) ) ) ∈ ℤ )
78 16 77 syl ⊢ ( 𝜑 → ( ℜ ‘ ( ( 𝐴 + ( i · 𝐵 ) ) · ( 𝐶 + ( i · 𝐷 ) ) ) ) ∈ ℤ )
79 zsqcl ⊢ ( ( ℜ ‘ ( ( 𝐴 + ( i · 𝐵 ) ) · ( 𝐶 + ( i · 𝐷 ) ) ) ) ∈ ℤ → ( ( ℜ ‘ ( ( 𝐴 + ( i · 𝐵 ) ) · ( 𝐶 + ( i · 𝐷 ) ) ) ) ↑ 2 ) ∈ ℤ )
80 78 79 syl ⊢ ( 𝜑 → ( ( ℜ ‘ ( ( 𝐴 + ( i · 𝐵 ) ) · ( 𝐶 + ( i · 𝐷 ) ) ) ) ↑ 2 ) ∈ ℤ )
81 80 zcnd ⊢ ( 𝜑 → ( ( ℜ ‘ ( ( 𝐴 + ( i · 𝐵 ) ) · ( 𝐶 + ( i · 𝐷 ) ) ) ) ↑ 2 ) ∈ ℂ )
82 76 simp3bi ⊢ ( ( ( 𝐴 + ( i · 𝐵 ) ) · ( 𝐶 + ( i · 𝐷 ) ) ) ∈ ℤ[i] → ( ℑ ‘ ( ( 𝐴 + ( i · 𝐵 ) ) · ( 𝐶 + ( i · 𝐷 ) ) ) ) ∈ ℤ )
83 16 82 syl ⊢ ( 𝜑 → ( ℑ ‘ ( ( 𝐴 + ( i · 𝐵 ) ) · ( 𝐶 + ( i · 𝐷 ) ) ) ) ∈ ℤ )
84 zsqcl ⊢ ( ( ℑ ‘ ( ( 𝐴 + ( i · 𝐵 ) ) · ( 𝐶 + ( i · 𝐷 ) ) ) ) ∈ ℤ → ( ( ℑ ‘ ( ( 𝐴 + ( i · 𝐵 ) ) · ( 𝐶 + ( i · 𝐷 ) ) ) ) ↑ 2 ) ∈ ℤ )
85 83 84 syl ⊢ ( 𝜑 → ( ( ℑ ‘ ( ( 𝐴 + ( i · 𝐵 ) ) · ( 𝐶 + ( i · 𝐷 ) ) ) ) ↑ 2 ) ∈ ℤ )
86 85 zcnd ⊢ ( 𝜑 → ( ( ℑ ‘ ( ( 𝐴 + ( i · 𝐵 ) ) · ( 𝐶 + ( i · 𝐷 ) ) ) ) ↑ 2 ) ∈ ℂ )
87 81 86 addcomd ⊢ ( 𝜑 → ( ( ( ℜ ‘ ( ( 𝐴 + ( i · 𝐵 ) ) · ( 𝐶 + ( i · 𝐷 ) ) ) ) ↑ 2 ) + ( ( ℑ ‘ ( ( 𝐴 + ( i · 𝐵 ) ) · ( 𝐶 + ( i · 𝐷 ) ) ) ) ↑ 2 ) ) = ( ( ( ℑ ‘ ( ( 𝐴 + ( i · 𝐵 ) ) · ( 𝐶 + ( i · 𝐷 ) ) ) ) ↑ 2 ) + ( ( ℜ ‘ ( ( 𝐴 + ( i · 𝐵 ) ) · ( 𝐶 + ( i · 𝐷 ) ) ) ) ↑ 2 ) ) )
88 75 87 eqtrd ⊢ ( 𝜑 → ( ( abs ‘ ( ( 𝐴 + ( i · 𝐵 ) ) · ( 𝐶 + ( i · 𝐷 ) ) ) ) ↑ 2 ) = ( ( ( ℑ ‘ ( ( 𝐴 + ( i · 𝐵 ) ) · ( 𝐶 + ( i · 𝐷 ) ) ) ) ↑ 2 ) + ( ( ℜ ‘ ( ( 𝐴 + ( i · 𝐵 ) ) · ( 𝐶 + ( i · 𝐷 ) ) ) ) ↑ 2 ) ) )
89 74 88 breqtrd ⊢ ( 𝜑 → 𝑃 ∥ ( ( ( ℑ ‘ ( ( 𝐴 + ( i · 𝐵 ) ) · ( 𝐶 + ( i · 𝐷 ) ) ) ) ↑ 2 ) + ( ( ℜ ‘ ( ( 𝐴 + ( i · 𝐵 ) ) · ( 𝐶 + ( i · 𝐷 ) ) ) ) ↑ 2 ) ) )
90 6 zcnd ⊢ ( 𝜑 → 𝐶 ∈ ℂ )
91 5 zcnd ⊢ ( 𝜑 → 𝐵 ∈ ℂ )
92 90 91 mulcld ⊢ ( 𝜑 → ( 𝐶 · 𝐵 ) ∈ ℂ )
93 4 zcnd ⊢ ( 𝜑 → 𝐴 ∈ ℂ )
94 7 zcnd ⊢ ( 𝜑 → 𝐷 ∈ ℂ )
95 93 94 mulcld ⊢ ( 𝜑 → ( 𝐴 · 𝐷 ) ∈ ℂ )
96 92 95 addcomd ⊢ ( 𝜑 → ( ( 𝐶 · 𝐵 ) + ( 𝐴 · 𝐷 ) ) = ( ( 𝐴 · 𝐷 ) + ( 𝐶 · 𝐵 ) ) )
97 90 91 mulcomd ⊢ ( 𝜑 → ( 𝐶 · 𝐵 ) = ( 𝐵 · 𝐶 ) )
98 97 oveq2d ⊢ ( 𝜑 → ( ( 𝐴 · 𝐷 ) + ( 𝐶 · 𝐵 ) ) = ( ( 𝐴 · 𝐷 ) + ( 𝐵 · 𝐶 ) ) )
99 96 98 eqtrd ⊢ ( 𝜑 → ( ( 𝐶 · 𝐵 ) + ( 𝐴 · 𝐷 ) ) = ( ( 𝐴 · 𝐷 ) + ( 𝐵 · 𝐶 ) ) )
100 10 99 breqtrd ⊢ ( 𝜑 → 𝑃 ∥ ( ( 𝐴 · 𝐷 ) + ( 𝐵 · 𝐶 ) ) )
101 40 44 immuld ⊢ ( 𝜑 → ( ℑ ‘ ( ( 𝐴 + ( i · 𝐵 ) ) · ( 𝐶 + ( i · 𝐷 ) ) ) ) = ( ( ( ℜ ‘ ( 𝐴 + ( i · 𝐵 ) ) ) · ( ℑ ‘ ( 𝐶 + ( i · 𝐷 ) ) ) ) + ( ( ℑ ‘ ( 𝐴 + ( i · 𝐵 ) ) ) · ( ℜ ‘ ( 𝐶 + ( i · 𝐷 ) ) ) ) ) )
102 50 61 oveq12d ⊢ ( 𝜑 → ( ( ℜ ‘ ( 𝐴 + ( i · 𝐵 ) ) ) · ( ℑ ‘ ( 𝐶 + ( i · 𝐷 ) ) ) ) = ( 𝐴 · 𝐷 ) )
103 52 59 oveq12d ⊢ ( 𝜑 → ( ( ℑ ‘ ( 𝐴 + ( i · 𝐵 ) ) ) · ( ℜ ‘ ( 𝐶 + ( i · 𝐷 ) ) ) ) = ( 𝐵 · 𝐶 ) )
104 102 103 oveq12d ⊢ ( 𝜑 → ( ( ( ℜ ‘ ( 𝐴 + ( i · 𝐵 ) ) ) · ( ℑ ‘ ( 𝐶 + ( i · 𝐷 ) ) ) ) + ( ( ℑ ‘ ( 𝐴 + ( i · 𝐵 ) ) ) · ( ℜ ‘ ( 𝐶 + ( i · 𝐷 ) ) ) ) ) = ( ( 𝐴 · 𝐷 ) + ( 𝐵 · 𝐶 ) ) )
105 101 104 eqtrd ⊢ ( 𝜑 → ( ℑ ‘ ( ( 𝐴 + ( i · 𝐵 ) ) · ( 𝐶 + ( i · 𝐷 ) ) ) ) = ( ( 𝐴 · 𝐷 ) + ( 𝐵 · 𝐶 ) ) )
106 100 105 breqtrrd ⊢ ( 𝜑 → 𝑃 ∥ ( ℑ ‘ ( ( 𝐴 + ( i · 𝐵 ) ) · ( 𝐶 + ( i · 𝐷 ) ) ) ) )
107 2nn ⊢ 2 ∈ ℕ
108 107 a1i ⊢ ( 𝜑 → 2 ∈ ℕ )
109 prmdvdsexp ⊢ ( ( 𝑃 ∈ ℙ ∧ ( ℑ ‘ ( ( 𝐴 + ( i · 𝐵 ) ) · ( 𝐶 + ( i · 𝐷 ) ) ) ) ∈ ℤ ∧ 2 ∈ ℕ ) → ( 𝑃 ∥ ( ( ℑ ‘ ( ( 𝐴 + ( i · 𝐵 ) ) · ( 𝐶 + ( i · 𝐷 ) ) ) ) ↑ 2 ) ↔ 𝑃 ∥ ( ℑ ‘ ( ( 𝐴 + ( i · 𝐵 ) ) · ( 𝐶 + ( i · 𝐷 ) ) ) ) ) )
110 3 83 108 109 syl3anc ⊢ ( 𝜑 → ( 𝑃 ∥ ( ( ℑ ‘ ( ( 𝐴 + ( i · 𝐵 ) ) · ( 𝐶 + ( i · 𝐷 ) ) ) ) ↑ 2 ) ↔ 𝑃 ∥ ( ℑ ‘ ( ( 𝐴 + ( i · 𝐵 ) ) · ( 𝐶 + ( i · 𝐷 ) ) ) ) ) )
111 106 110 mpbird ⊢ ( 𝜑 → 𝑃 ∥ ( ( ℑ ‘ ( ( 𝐴 + ( i · 𝐵 ) ) · ( 𝐶 + ( i · 𝐷 ) ) ) ) ↑ 2 ) )
112 dvdsadd2b ⊢ ( ( 𝑃 ∈ ℤ ∧ ( ( ℜ ‘ ( ( 𝐴 + ( i · 𝐵 ) ) · ( 𝐶 + ( i · 𝐷 ) ) ) ) ↑ 2 ) ∈ ℤ ∧ ( ( ( ℑ ‘ ( ( 𝐴 + ( i · 𝐵 ) ) · ( 𝐶 + ( i · 𝐷 ) ) ) ) ↑ 2 ) ∈ ℤ ∧ 𝑃 ∥ ( ( ℑ ‘ ( ( 𝐴 + ( i · 𝐵 ) ) · ( 𝐶 + ( i · 𝐷 ) ) ) ) ↑ 2 ) ) ) → ( 𝑃 ∥ ( ( ℜ ‘ ( ( 𝐴 + ( i · 𝐵 ) ) · ( 𝐶 + ( i · 𝐷 ) ) ) ) ↑ 2 ) ↔ 𝑃 ∥ ( ( ( ℑ ‘ ( ( 𝐴 + ( i · 𝐵 ) ) · ( 𝐶 + ( i · 𝐷 ) ) ) ) ↑ 2 ) + ( ( ℜ ‘ ( ( 𝐴 + ( i · 𝐵 ) ) · ( 𝐶 + ( i · 𝐷 ) ) ) ) ↑ 2 ) ) ) )
113 27 80 85 111 112 syl112anc ⊢ ( 𝜑 → ( 𝑃 ∥ ( ( ℜ ‘ ( ( 𝐴 + ( i · 𝐵 ) ) · ( 𝐶 + ( i · 𝐷 ) ) ) ) ↑ 2 ) ↔ 𝑃 ∥ ( ( ( ℑ ‘ ( ( 𝐴 + ( i · 𝐵 ) ) · ( 𝐶 + ( i · 𝐷 ) ) ) ) ↑ 2 ) + ( ( ℜ ‘ ( ( 𝐴 + ( i · 𝐵 ) ) · ( 𝐶 + ( i · 𝐷 ) ) ) ) ↑ 2 ) ) ) )
114 89 113 mpbird ⊢ ( 𝜑 → 𝑃 ∥ ( ( ℜ ‘ ( ( 𝐴 + ( i · 𝐵 ) ) · ( 𝐶 + ( i · 𝐷 ) ) ) ) ↑ 2 ) )
115 prmdvdsexp ⊢ ( ( 𝑃 ∈ ℙ ∧ ( ℜ ‘ ( ( 𝐴 + ( i · 𝐵 ) ) · ( 𝐶 + ( i · 𝐷 ) ) ) ) ∈ ℤ ∧ 2 ∈ ℕ ) → ( 𝑃 ∥ ( ( ℜ ‘ ( ( 𝐴 + ( i · 𝐵 ) ) · ( 𝐶 + ( i · 𝐷 ) ) ) ) ↑ 2 ) ↔ 𝑃 ∥ ( ℜ ‘ ( ( 𝐴 + ( i · 𝐵 ) ) · ( 𝐶 + ( i · 𝐷 ) ) ) ) ) )
116 3 78 108 115 syl3anc ⊢ ( 𝜑 → ( 𝑃 ∥ ( ( ℜ ‘ ( ( 𝐴 + ( i · 𝐵 ) ) · ( 𝐶 + ( i · 𝐷 ) ) ) ) ↑ 2 ) ↔ 𝑃 ∥ ( ℜ ‘ ( ( 𝐴 + ( i · 𝐵 ) ) · ( 𝐶 + ( i · 𝐷 ) ) ) ) ) )
117 114 116 mpbid ⊢ ( 𝜑 → 𝑃 ∥ ( ℜ ‘ ( ( 𝐴 + ( i · 𝐵 ) ) · ( 𝐶 + ( i · 𝐷 ) ) ) ) )
118 dvdsval2 ⊢ ( ( 𝑃 ∈ ℤ ∧ 𝑃 ≠ 0 ∧ ( ℜ ‘ ( ( 𝐴 + ( i · 𝐵 ) ) · ( 𝐶 + ( i · 𝐷 ) ) ) ) ∈ ℤ ) → ( 𝑃 ∥ ( ℜ ‘ ( ( 𝐴 + ( i · 𝐵 ) ) · ( 𝐶 + ( i · 𝐷 ) ) ) ) ↔ ( ( ℜ ‘ ( ( 𝐴 + ( i · 𝐵 ) ) · ( 𝐶 + ( i · 𝐷 ) ) ) ) / 𝑃 ) ∈ ℤ ) )
119 27 22 78 118 syl3anc ⊢ ( 𝜑 → ( 𝑃 ∥ ( ℜ ‘ ( ( 𝐴 + ( i · 𝐵 ) ) · ( 𝐶 + ( i · 𝐷 ) ) ) ) ↔ ( ( ℜ ‘ ( ( 𝐴 + ( i · 𝐵 ) ) · ( 𝐶 + ( i · 𝐷 ) ) ) ) / 𝑃 ) ∈ ℤ ) )
120 117 119 mpbid ⊢ ( 𝜑 → ( ( ℜ ‘ ( ( 𝐴 + ( i · 𝐵 ) ) · ( 𝐶 + ( i · 𝐷 ) ) ) ) / 𝑃 ) ∈ ℤ )
121 25 120 eqeltrd ⊢ ( 𝜑 → ( ℜ ‘ ( ( ( 𝐴 + ( i · 𝐵 ) ) · ( 𝐶 + ( i · 𝐷 ) ) ) / 𝑃 ) ) ∈ ℤ )
122 24 18 22 imdivd ⊢ ( 𝜑 → ( ℑ ‘ ( ( ( 𝐴 + ( i · 𝐵 ) ) · ( 𝐶 + ( i · 𝐷 ) ) ) / 𝑃 ) ) = ( ( ℑ ‘ ( ( 𝐴 + ( i · 𝐵 ) ) · ( 𝐶 + ( i · 𝐷 ) ) ) ) / 𝑃 ) )
123 dvdsval2 ⊢ ( ( 𝑃 ∈ ℤ ∧ 𝑃 ≠ 0 ∧ ( ℑ ‘ ( ( 𝐴 + ( i · 𝐵 ) ) · ( 𝐶 + ( i · 𝐷 ) ) ) ) ∈ ℤ ) → ( 𝑃 ∥ ( ℑ ‘ ( ( 𝐴 + ( i · 𝐵 ) ) · ( 𝐶 + ( i · 𝐷 ) ) ) ) ↔ ( ( ℑ ‘ ( ( 𝐴 + ( i · 𝐵 ) ) · ( 𝐶 + ( i · 𝐷 ) ) ) ) / 𝑃 ) ∈ ℤ ) )
124 27 22 83 123 syl3anc ⊢ ( 𝜑 → ( 𝑃 ∥ ( ℑ ‘ ( ( 𝐴 + ( i · 𝐵 ) ) · ( 𝐶 + ( i · 𝐷 ) ) ) ) ↔ ( ( ℑ ‘ ( ( 𝐴 + ( i · 𝐵 ) ) · ( 𝐶 + ( i · 𝐷 ) ) ) ) / 𝑃 ) ∈ ℤ ) )
125 106 124 mpbid ⊢ ( 𝜑 → ( ( ℑ ‘ ( ( 𝐴 + ( i · 𝐵 ) ) · ( 𝐶 + ( i · 𝐷 ) ) ) ) / 𝑃 ) ∈ ℤ )
126 122 125 eqeltrd ⊢ ( 𝜑 → ( ℑ ‘ ( ( ( 𝐴 + ( i · 𝐵 ) ) · ( 𝐶 + ( i · 𝐷 ) ) ) / 𝑃 ) ) ∈ ℤ )
127 elgz ⊢ ( ( ( ( 𝐴 + ( i · 𝐵 ) ) · ( 𝐶 + ( i · 𝐷 ) ) ) / 𝑃 ) ∈ ℤ[i] ↔ ( ( ( ( 𝐴 + ( i · 𝐵 ) ) · ( 𝐶 + ( i · 𝐷 ) ) ) / 𝑃 ) ∈ ℂ ∧ ( ℜ ‘ ( ( ( 𝐴 + ( i · 𝐵 ) ) · ( 𝐶 + ( i · 𝐷 ) ) ) / 𝑃 ) ) ∈ ℤ ∧ ( ℑ ‘ ( ( ( 𝐴 + ( i · 𝐵 ) ) · ( 𝐶 + ( i · 𝐷 ) ) ) / 𝑃 ) ) ∈ ℤ ) )
128 23 121 126 127 syl3anbrc ⊢ ( 𝜑 → ( ( ( 𝐴 + ( i · 𝐵 ) ) · ( 𝐶 + ( i · 𝐷 ) ) ) / 𝑃 ) ∈ ℤ[i] )
129 18 21 22 absdivd ⊢ ( 𝜑 → ( abs ‘ ( ( ( 𝐴 + ( i · 𝐵 ) ) · ( 𝐶 + ( i · 𝐷 ) ) ) / 𝑃 ) ) = ( ( abs ‘ ( ( 𝐴 + ( i · 𝐵 ) ) · ( 𝐶 + ( i · 𝐷 ) ) ) ) / ( abs ‘ 𝑃 ) ) )
130 20 nnnn0d ⊢ ( 𝜑 → 𝑃 ∈ ℕ0 )
131 130 nn0ge0d ⊢ ( 𝜑 → 0 ≤ 𝑃 )
132 24 131 absidd ⊢ ( 𝜑 → ( abs ‘ 𝑃 ) = 𝑃 )
133 132 oveq2d ⊢ ( 𝜑 → ( ( abs ‘ ( ( 𝐴 + ( i · 𝐵 ) ) · ( 𝐶 + ( i · 𝐷 ) ) ) ) / ( abs ‘ 𝑃 ) ) = ( ( abs ‘ ( ( 𝐴 + ( i · 𝐵 ) ) · ( 𝐶 + ( i · 𝐷 ) ) ) ) / 𝑃 ) )
134 129 133 eqtrd ⊢ ( 𝜑 → ( abs ‘ ( ( ( 𝐴 + ( i · 𝐵 ) ) · ( 𝐶 + ( i · 𝐷 ) ) ) / 𝑃 ) ) = ( ( abs ‘ ( ( 𝐴 + ( i · 𝐵 ) ) · ( 𝐶 + ( i · 𝐷 ) ) ) ) / 𝑃 ) )
135 134 oveq1d ⊢ ( 𝜑 → ( ( abs ‘ ( ( ( 𝐴 + ( i · 𝐵 ) ) · ( 𝐶 + ( i · 𝐷 ) ) ) / 𝑃 ) ) ↑ 2 ) = ( ( ( abs ‘ ( ( 𝐴 + ( i · 𝐵 ) ) · ( 𝐶 + ( i · 𝐷 ) ) ) ) / 𝑃 ) ↑ 2 ) )
136 18 abscld ⊢ ( 𝜑 → ( abs ‘ ( ( 𝐴 + ( i · 𝐵 ) ) · ( 𝐶 + ( i · 𝐷 ) ) ) ) ∈ ℝ )
137 136 recnd ⊢ ( 𝜑 → ( abs ‘ ( ( 𝐴 + ( i · 𝐵 ) ) · ( 𝐶 + ( i · 𝐷 ) ) ) ) ∈ ℂ )
138 137 21 22 sqdivd ⊢ ( 𝜑 → ( ( ( abs ‘ ( ( 𝐴 + ( i · 𝐵 ) ) · ( 𝐶 + ( i · 𝐷 ) ) ) ) / 𝑃 ) ↑ 2 ) = ( ( ( abs ‘ ( ( 𝐴 + ( i · 𝐵 ) ) · ( 𝐶 + ( i · 𝐷 ) ) ) ) ↑ 2 ) / ( 𝑃 ↑ 2 ) ) )
139 73 oveq1d ⊢ ( 𝜑 → ( ( ( abs ‘ ( ( 𝐴 + ( i · 𝐵 ) ) · ( 𝐶 + ( i · 𝐷 ) ) ) ) ↑ 2 ) / ( 𝑃 ↑ 2 ) ) = ( ( 𝑁 · ( 𝑃 ↑ 2 ) ) / ( 𝑃 ↑ 2 ) ) )
140 20 nnsqcld ⊢ ( 𝜑 → ( 𝑃 ↑ 2 ) ∈ ℕ )
141 140 nncnd ⊢ ( 𝜑 → ( 𝑃 ↑ 2 ) ∈ ℂ )
142 140 nnne0d ⊢ ( 𝜑 → ( 𝑃 ↑ 2 ) ≠ 0 )
143 67 141 142 divcan4d ⊢ ( 𝜑 → ( ( 𝑁 · ( 𝑃 ↑ 2 ) ) / ( 𝑃 ↑ 2 ) ) = 𝑁 )
144 139 143 eqtrd ⊢ ( 𝜑 → ( ( ( abs ‘ ( ( 𝐴 + ( i · 𝐵 ) ) · ( 𝐶 + ( i · 𝐷 ) ) ) ) ↑ 2 ) / ( 𝑃 ↑ 2 ) ) = 𝑁 )
145 135 138 144 3eqtrrd ⊢ ( 𝜑 → 𝑁 = ( ( abs ‘ ( ( ( 𝐴 + ( i · 𝐵 ) ) · ( 𝐶 + ( i · 𝐷 ) ) ) / 𝑃 ) ) ↑ 2 ) )
146 fveq2 ⊢ ( 𝑥 = ( ( ( 𝐴 + ( i · 𝐵 ) ) · ( 𝐶 + ( i · 𝐷 ) ) ) / 𝑃 ) → ( abs ‘ 𝑥 ) = ( abs ‘ ( ( ( 𝐴 + ( i · 𝐵 ) ) · ( 𝐶 + ( i · 𝐷 ) ) ) / 𝑃 ) ) )
147 146 oveq1d ⊢ ( 𝑥 = ( ( ( 𝐴 + ( i · 𝐵 ) ) · ( 𝐶 + ( i · 𝐷 ) ) ) / 𝑃 ) → ( ( abs ‘ 𝑥 ) ↑ 2 ) = ( ( abs ‘ ( ( ( 𝐴 + ( i · 𝐵 ) ) · ( 𝐶 + ( i · 𝐷 ) ) ) / 𝑃 ) ) ↑ 2 ) )
148 147 rspceeqv ⊢ ( ( ( ( ( 𝐴 + ( i · 𝐵 ) ) · ( 𝐶 + ( i · 𝐷 ) ) ) / 𝑃 ) ∈ ℤ[i] ∧ 𝑁 = ( ( abs ‘ ( ( ( 𝐴 + ( i · 𝐵 ) ) · ( 𝐶 + ( i · 𝐷 ) ) ) / 𝑃 ) ) ↑ 2 ) ) → ∃ 𝑥 ∈ ℤ[i] 𝑁 = ( ( abs ‘ 𝑥 ) ↑ 2 ) )
149 128 145 148 syl2anc ⊢ ( 𝜑 → ∃ 𝑥 ∈ ℤ[i] 𝑁 = ( ( abs ‘ 𝑥 ) ↑ 2 ) )
150 1 2sqlem1 ⊢ ( 𝑁 ∈ 𝑆 ↔ ∃ 𝑥 ∈ ℤ[i] 𝑁 = ( ( abs ‘ 𝑥 ) ↑ 2 ) )
151 149 150 sylibr ⊢ ( 𝜑 → 𝑁 ∈ 𝑆 )