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