# Metamath Proof Explorer

## Theorem 2sqlem3

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

Ref Expression
Hypotheses 2sq.1 ${⊢}{S}=\mathrm{ran}\left({w}\in ℤ\left[i\right]⟼{\left|{w}\right|}^{2}\right)$
2sqlem5.1 ${⊢}{\phi }\to {N}\in ℕ$
2sqlem5.2 ${⊢}{\phi }\to {P}\in ℙ$
2sqlem4.3 ${⊢}{\phi }\to {A}\in ℤ$
2sqlem4.4 ${⊢}{\phi }\to {B}\in ℤ$
2sqlem4.5 ${⊢}{\phi }\to {C}\in ℤ$
2sqlem4.6 ${⊢}{\phi }\to {D}\in ℤ$
2sqlem4.7 ${⊢}{\phi }\to {N}{P}={{A}}^{2}+{{B}}^{2}$
2sqlem4.8 ${⊢}{\phi }\to {P}={{C}}^{2}+{{D}}^{2}$
2sqlem4.9 ${⊢}{\phi }\to {P}\parallel \left({C}{B}+{A}{D}\right)$
Assertion 2sqlem3 ${⊢}{\phi }\to {N}\in {S}$

### Proof

Step Hyp Ref Expression
1 2sq.1 ${⊢}{S}=\mathrm{ran}\left({w}\in ℤ\left[i\right]⟼{\left|{w}\right|}^{2}\right)$
2 2sqlem5.1 ${⊢}{\phi }\to {N}\in ℕ$
3 2sqlem5.2 ${⊢}{\phi }\to {P}\in ℙ$
4 2sqlem4.3 ${⊢}{\phi }\to {A}\in ℤ$
5 2sqlem4.4 ${⊢}{\phi }\to {B}\in ℤ$
6 2sqlem4.5 ${⊢}{\phi }\to {C}\in ℤ$
7 2sqlem4.6 ${⊢}{\phi }\to {D}\in ℤ$
8 2sqlem4.7 ${⊢}{\phi }\to {N}{P}={{A}}^{2}+{{B}}^{2}$
9 2sqlem4.8 ${⊢}{\phi }\to {P}={{C}}^{2}+{{D}}^{2}$
10 2sqlem4.9 ${⊢}{\phi }\to {P}\parallel \left({C}{B}+{A}{D}\right)$
11 gzreim ${⊢}\left({A}\in ℤ\wedge {B}\in ℤ\right)\to {A}+\mathrm{i}{B}\in ℤ\left[i\right]$
12 4 5 11 syl2anc ${⊢}{\phi }\to {A}+\mathrm{i}{B}\in ℤ\left[i\right]$
13 gzreim ${⊢}\left({C}\in ℤ\wedge {D}\in ℤ\right)\to {C}+\mathrm{i}{D}\in ℤ\left[i\right]$
14 6 7 13 syl2anc ${⊢}{\phi }\to {C}+\mathrm{i}{D}\in ℤ\left[i\right]$
15 gzmulcl ${⊢}\left({A}+\mathrm{i}{B}\in ℤ\left[i\right]\wedge {C}+\mathrm{i}{D}\in ℤ\left[i\right]\right)\to \left({A}+\mathrm{i}{B}\right)\left({C}+\mathrm{i}{D}\right)\in ℤ\left[i\right]$
16 12 14 15 syl2anc ${⊢}{\phi }\to \left({A}+\mathrm{i}{B}\right)\left({C}+\mathrm{i}{D}\right)\in ℤ\left[i\right]$
17 gzcn ${⊢}\left({A}+\mathrm{i}{B}\right)\left({C}+\mathrm{i}{D}\right)\in ℤ\left[i\right]\to \left({A}+\mathrm{i}{B}\right)\left({C}+\mathrm{i}{D}\right)\in ℂ$
18 16 17 syl ${⊢}{\phi }\to \left({A}+\mathrm{i}{B}\right)\left({C}+\mathrm{i}{D}\right)\in ℂ$
19 prmnn ${⊢}{P}\in ℙ\to {P}\in ℕ$
20 3 19 syl ${⊢}{\phi }\to {P}\in ℕ$
21 20 nncnd ${⊢}{\phi }\to {P}\in ℂ$
22 20 nnne0d ${⊢}{\phi }\to {P}\ne 0$
23 18 21 22 divcld ${⊢}{\phi }\to \frac{\left({A}+\mathrm{i}{B}\right)\left({C}+\mathrm{i}{D}\right)}{{P}}\in ℂ$
24 20 nnred ${⊢}{\phi }\to {P}\in ℝ$
25 24 18 22 redivd ${⊢}{\phi }\to \Re \left(\frac{\left({A}+\mathrm{i}{B}\right)\left({C}+\mathrm{i}{D}\right)}{{P}}\right)=\frac{\Re \left(\left({A}+\mathrm{i}{B}\right)\left({C}+\mathrm{i}{D}\right)\right)}{{P}}$
26 prmz ${⊢}{P}\in ℙ\to {P}\in ℤ$
27 3 26 syl ${⊢}{\phi }\to {P}\in ℤ$
28 dvdsmul2 ${⊢}\left({P}\in ℤ\wedge {P}\in ℤ\right)\to {P}\parallel {P}{P}$
29 27 27 28 syl2anc ${⊢}{\phi }\to {P}\parallel {P}{P}$
30 21 sqvald ${⊢}{\phi }\to {{P}}^{2}={P}{P}$
31 29 30 breqtrrd ${⊢}{\phi }\to {P}\parallel {{P}}^{2}$
32 2 nnzd ${⊢}{\phi }\to {N}\in ℤ$
33 zsqcl ${⊢}{P}\in ℤ\to {{P}}^{2}\in ℤ$
34 27 33 syl ${⊢}{\phi }\to {{P}}^{2}\in ℤ$
35 dvdsmul2 ${⊢}\left({N}\in ℤ\wedge {{P}}^{2}\in ℤ\right)\to {{P}}^{2}\parallel {N}{{P}}^{2}$
36 32 34 35 syl2anc ${⊢}{\phi }\to {{P}}^{2}\parallel {N}{{P}}^{2}$
37 32 34 zmulcld ${⊢}{\phi }\to {N}{{P}}^{2}\in ℤ$
38 dvdstr ${⊢}\left({P}\in ℤ\wedge {{P}}^{2}\in ℤ\wedge {N}{{P}}^{2}\in ℤ\right)\to \left(\left({P}\parallel {{P}}^{2}\wedge {{P}}^{2}\parallel {N}{{P}}^{2}\right)\to {P}\parallel {N}{{P}}^{2}\right)$
39 27 34 37 38 syl3anc ${⊢}{\phi }\to \left(\left({P}\parallel {{P}}^{2}\wedge {{P}}^{2}\parallel {N}{{P}}^{2}\right)\to {P}\parallel {N}{{P}}^{2}\right)$
40 31 36 39 mp2and ${⊢}{\phi }\to {P}\parallel {N}{{P}}^{2}$
41 gzcn ${⊢}{A}+\mathrm{i}{B}\in ℤ\left[i\right]\to {A}+\mathrm{i}{B}\in ℂ$
42 12 41 syl ${⊢}{\phi }\to {A}+\mathrm{i}{B}\in ℂ$
43 42 abscld ${⊢}{\phi }\to \left|{A}+\mathrm{i}{B}\right|\in ℝ$
44 43 recnd ${⊢}{\phi }\to \left|{A}+\mathrm{i}{B}\right|\in ℂ$
45 gzcn ${⊢}{C}+\mathrm{i}{D}\in ℤ\left[i\right]\to {C}+\mathrm{i}{D}\in ℂ$
46 14 45 syl ${⊢}{\phi }\to {C}+\mathrm{i}{D}\in ℂ$
47 46 abscld ${⊢}{\phi }\to \left|{C}+\mathrm{i}{D}\right|\in ℝ$
48 47 recnd ${⊢}{\phi }\to \left|{C}+\mathrm{i}{D}\right|\in ℂ$
49 44 48 sqmuld ${⊢}{\phi }\to {\left|{A}+\mathrm{i}{B}\right|\left|{C}+\mathrm{i}{D}\right|}^{2}={\left|{A}+\mathrm{i}{B}\right|}^{2}{\left|{C}+\mathrm{i}{D}\right|}^{2}$
50 4 zred ${⊢}{\phi }\to {A}\in ℝ$
51 5 zred ${⊢}{\phi }\to {B}\in ℝ$
52 50 51 crred ${⊢}{\phi }\to \Re \left({A}+\mathrm{i}{B}\right)={A}$
53 52 oveq1d ${⊢}{\phi }\to {\Re \left({A}+\mathrm{i}{B}\right)}^{2}={{A}}^{2}$
54 50 51 crimd ${⊢}{\phi }\to \Im \left({A}+\mathrm{i}{B}\right)={B}$
55 54 oveq1d ${⊢}{\phi }\to {\Im \left({A}+\mathrm{i}{B}\right)}^{2}={{B}}^{2}$
56 53 55 oveq12d ${⊢}{\phi }\to {\Re \left({A}+\mathrm{i}{B}\right)}^{2}+{\Im \left({A}+\mathrm{i}{B}\right)}^{2}={{A}}^{2}+{{B}}^{2}$
57 42 absvalsq2d ${⊢}{\phi }\to {\left|{A}+\mathrm{i}{B}\right|}^{2}={\Re \left({A}+\mathrm{i}{B}\right)}^{2}+{\Im \left({A}+\mathrm{i}{B}\right)}^{2}$
58 56 57 8 3eqtr4d ${⊢}{\phi }\to {\left|{A}+\mathrm{i}{B}\right|}^{2}={N}{P}$
59 6 zred ${⊢}{\phi }\to {C}\in ℝ$
60 7 zred ${⊢}{\phi }\to {D}\in ℝ$
61 59 60 crred ${⊢}{\phi }\to \Re \left({C}+\mathrm{i}{D}\right)={C}$
62 61 oveq1d ${⊢}{\phi }\to {\Re \left({C}+\mathrm{i}{D}\right)}^{2}={{C}}^{2}$
63 59 60 crimd ${⊢}{\phi }\to \Im \left({C}+\mathrm{i}{D}\right)={D}$
64 63 oveq1d ${⊢}{\phi }\to {\Im \left({C}+\mathrm{i}{D}\right)}^{2}={{D}}^{2}$
65 62 64 oveq12d ${⊢}{\phi }\to {\Re \left({C}+\mathrm{i}{D}\right)}^{2}+{\Im \left({C}+\mathrm{i}{D}\right)}^{2}={{C}}^{2}+{{D}}^{2}$
66 46 absvalsq2d ${⊢}{\phi }\to {\left|{C}+\mathrm{i}{D}\right|}^{2}={\Re \left({C}+\mathrm{i}{D}\right)}^{2}+{\Im \left({C}+\mathrm{i}{D}\right)}^{2}$
67 65 66 9 3eqtr4d ${⊢}{\phi }\to {\left|{C}+\mathrm{i}{D}\right|}^{2}={P}$
68 58 67 oveq12d ${⊢}{\phi }\to {\left|{A}+\mathrm{i}{B}\right|}^{2}{\left|{C}+\mathrm{i}{D}\right|}^{2}={N}{P}{P}$
69 2 nncnd ${⊢}{\phi }\to {N}\in ℂ$
70 69 21 21 mulassd ${⊢}{\phi }\to {N}{P}{P}={N}{P}{P}$
71 49 68 70 3eqtrd ${⊢}{\phi }\to {\left|{A}+\mathrm{i}{B}\right|\left|{C}+\mathrm{i}{D}\right|}^{2}={N}{P}{P}$
72 42 46 absmuld ${⊢}{\phi }\to \left|\left({A}+\mathrm{i}{B}\right)\left({C}+\mathrm{i}{D}\right)\right|=\left|{A}+\mathrm{i}{B}\right|\left|{C}+\mathrm{i}{D}\right|$
73 72 oveq1d ${⊢}{\phi }\to {\left|\left({A}+\mathrm{i}{B}\right)\left({C}+\mathrm{i}{D}\right)\right|}^{2}={\left|{A}+\mathrm{i}{B}\right|\left|{C}+\mathrm{i}{D}\right|}^{2}$
74 30 oveq2d ${⊢}{\phi }\to {N}{{P}}^{2}={N}{P}{P}$
75 71 73 74 3eqtr4d ${⊢}{\phi }\to {\left|\left({A}+\mathrm{i}{B}\right)\left({C}+\mathrm{i}{D}\right)\right|}^{2}={N}{{P}}^{2}$
76 40 75 breqtrrd ${⊢}{\phi }\to {P}\parallel {\left|\left({A}+\mathrm{i}{B}\right)\left({C}+\mathrm{i}{D}\right)\right|}^{2}$
77 18 absvalsq2d ${⊢}{\phi }\to {\left|\left({A}+\mathrm{i}{B}\right)\left({C}+\mathrm{i}{D}\right)\right|}^{2}={\Re \left(\left({A}+\mathrm{i}{B}\right)\left({C}+\mathrm{i}{D}\right)\right)}^{2}+{\Im \left(\left({A}+\mathrm{i}{B}\right)\left({C}+\mathrm{i}{D}\right)\right)}^{2}$
78 elgz ${⊢}\left({A}+\mathrm{i}{B}\right)\left({C}+\mathrm{i}{D}\right)\in ℤ\left[i\right]↔\left(\left({A}+\mathrm{i}{B}\right)\left({C}+\mathrm{i}{D}\right)\in ℂ\wedge \Re \left(\left({A}+\mathrm{i}{B}\right)\left({C}+\mathrm{i}{D}\right)\right)\in ℤ\wedge \Im \left(\left({A}+\mathrm{i}{B}\right)\left({C}+\mathrm{i}{D}\right)\right)\in ℤ\right)$
79 78 simp2bi ${⊢}\left({A}+\mathrm{i}{B}\right)\left({C}+\mathrm{i}{D}\right)\in ℤ\left[i\right]\to \Re \left(\left({A}+\mathrm{i}{B}\right)\left({C}+\mathrm{i}{D}\right)\right)\in ℤ$
80 16 79 syl ${⊢}{\phi }\to \Re \left(\left({A}+\mathrm{i}{B}\right)\left({C}+\mathrm{i}{D}\right)\right)\in ℤ$
81 zsqcl ${⊢}\Re \left(\left({A}+\mathrm{i}{B}\right)\left({C}+\mathrm{i}{D}\right)\right)\in ℤ\to {\Re \left(\left({A}+\mathrm{i}{B}\right)\left({C}+\mathrm{i}{D}\right)\right)}^{2}\in ℤ$
82 80 81 syl ${⊢}{\phi }\to {\Re \left(\left({A}+\mathrm{i}{B}\right)\left({C}+\mathrm{i}{D}\right)\right)}^{2}\in ℤ$
83 82 zcnd ${⊢}{\phi }\to {\Re \left(\left({A}+\mathrm{i}{B}\right)\left({C}+\mathrm{i}{D}\right)\right)}^{2}\in ℂ$
84 78 simp3bi ${⊢}\left({A}+\mathrm{i}{B}\right)\left({C}+\mathrm{i}{D}\right)\in ℤ\left[i\right]\to \Im \left(\left({A}+\mathrm{i}{B}\right)\left({C}+\mathrm{i}{D}\right)\right)\in ℤ$
85 16 84 syl ${⊢}{\phi }\to \Im \left(\left({A}+\mathrm{i}{B}\right)\left({C}+\mathrm{i}{D}\right)\right)\in ℤ$
86 zsqcl ${⊢}\Im \left(\left({A}+\mathrm{i}{B}\right)\left({C}+\mathrm{i}{D}\right)\right)\in ℤ\to {\Im \left(\left({A}+\mathrm{i}{B}\right)\left({C}+\mathrm{i}{D}\right)\right)}^{2}\in ℤ$
87 85 86 syl ${⊢}{\phi }\to {\Im \left(\left({A}+\mathrm{i}{B}\right)\left({C}+\mathrm{i}{D}\right)\right)}^{2}\in ℤ$
88 87 zcnd ${⊢}{\phi }\to {\Im \left(\left({A}+\mathrm{i}{B}\right)\left({C}+\mathrm{i}{D}\right)\right)}^{2}\in ℂ$
89 83 88 addcomd ${⊢}{\phi }\to {\Re \left(\left({A}+\mathrm{i}{B}\right)\left({C}+\mathrm{i}{D}\right)\right)}^{2}+{\Im \left(\left({A}+\mathrm{i}{B}\right)\left({C}+\mathrm{i}{D}\right)\right)}^{2}={\Im \left(\left({A}+\mathrm{i}{B}\right)\left({C}+\mathrm{i}{D}\right)\right)}^{2}+{\Re \left(\left({A}+\mathrm{i}{B}\right)\left({C}+\mathrm{i}{D}\right)\right)}^{2}$
90 77 89 eqtrd ${⊢}{\phi }\to {\left|\left({A}+\mathrm{i}{B}\right)\left({C}+\mathrm{i}{D}\right)\right|}^{2}={\Im \left(\left({A}+\mathrm{i}{B}\right)\left({C}+\mathrm{i}{D}\right)\right)}^{2}+{\Re \left(\left({A}+\mathrm{i}{B}\right)\left({C}+\mathrm{i}{D}\right)\right)}^{2}$
91 76 90 breqtrd ${⊢}{\phi }\to {P}\parallel \left({\Im \left(\left({A}+\mathrm{i}{B}\right)\left({C}+\mathrm{i}{D}\right)\right)}^{2}+{\Re \left(\left({A}+\mathrm{i}{B}\right)\left({C}+\mathrm{i}{D}\right)\right)}^{2}\right)$
92 6 zcnd ${⊢}{\phi }\to {C}\in ℂ$
93 5 zcnd ${⊢}{\phi }\to {B}\in ℂ$
94 92 93 mulcld ${⊢}{\phi }\to {C}{B}\in ℂ$
95 4 zcnd ${⊢}{\phi }\to {A}\in ℂ$
96 7 zcnd ${⊢}{\phi }\to {D}\in ℂ$
97 95 96 mulcld ${⊢}{\phi }\to {A}{D}\in ℂ$
98 94 97 addcomd ${⊢}{\phi }\to {C}{B}+{A}{D}={A}{D}+{C}{B}$
99 92 93 mulcomd ${⊢}{\phi }\to {C}{B}={B}{C}$
100 99 oveq2d ${⊢}{\phi }\to {A}{D}+{C}{B}={A}{D}+{B}{C}$
101 98 100 eqtrd ${⊢}{\phi }\to {C}{B}+{A}{D}={A}{D}+{B}{C}$
102 10 101 breqtrd ${⊢}{\phi }\to {P}\parallel \left({A}{D}+{B}{C}\right)$
103 42 46 immuld ${⊢}{\phi }\to \Im \left(\left({A}+\mathrm{i}{B}\right)\left({C}+\mathrm{i}{D}\right)\right)=\Re \left({A}+\mathrm{i}{B}\right)\Im \left({C}+\mathrm{i}{D}\right)+\Im \left({A}+\mathrm{i}{B}\right)\Re \left({C}+\mathrm{i}{D}\right)$
104 52 63 oveq12d ${⊢}{\phi }\to \Re \left({A}+\mathrm{i}{B}\right)\Im \left({C}+\mathrm{i}{D}\right)={A}{D}$
105 54 61 oveq12d ${⊢}{\phi }\to \Im \left({A}+\mathrm{i}{B}\right)\Re \left({C}+\mathrm{i}{D}\right)={B}{C}$
106 104 105 oveq12d ${⊢}{\phi }\to \Re \left({A}+\mathrm{i}{B}\right)\Im \left({C}+\mathrm{i}{D}\right)+\Im \left({A}+\mathrm{i}{B}\right)\Re \left({C}+\mathrm{i}{D}\right)={A}{D}+{B}{C}$
107 103 106 eqtrd ${⊢}{\phi }\to \Im \left(\left({A}+\mathrm{i}{B}\right)\left({C}+\mathrm{i}{D}\right)\right)={A}{D}+{B}{C}$
108 102 107 breqtrrd ${⊢}{\phi }\to {P}\parallel \Im \left(\left({A}+\mathrm{i}{B}\right)\left({C}+\mathrm{i}{D}\right)\right)$
109 2nn ${⊢}2\in ℕ$
110 109 a1i ${⊢}{\phi }\to 2\in ℕ$
111 prmdvdsexp ${⊢}\left({P}\in ℙ\wedge \Im \left(\left({A}+\mathrm{i}{B}\right)\left({C}+\mathrm{i}{D}\right)\right)\in ℤ\wedge 2\in ℕ\right)\to \left({P}\parallel {\Im \left(\left({A}+\mathrm{i}{B}\right)\left({C}+\mathrm{i}{D}\right)\right)}^{2}↔{P}\parallel \Im \left(\left({A}+\mathrm{i}{B}\right)\left({C}+\mathrm{i}{D}\right)\right)\right)$
112 3 85 110 111 syl3anc ${⊢}{\phi }\to \left({P}\parallel {\Im \left(\left({A}+\mathrm{i}{B}\right)\left({C}+\mathrm{i}{D}\right)\right)}^{2}↔{P}\parallel \Im \left(\left({A}+\mathrm{i}{B}\right)\left({C}+\mathrm{i}{D}\right)\right)\right)$
113 108 112 mpbird ${⊢}{\phi }\to {P}\parallel {\Im \left(\left({A}+\mathrm{i}{B}\right)\left({C}+\mathrm{i}{D}\right)\right)}^{2}$
114 dvdsadd2b ${⊢}\left({P}\in ℤ\wedge {\Re \left(\left({A}+\mathrm{i}{B}\right)\left({C}+\mathrm{i}{D}\right)\right)}^{2}\in ℤ\wedge \left({\Im \left(\left({A}+\mathrm{i}{B}\right)\left({C}+\mathrm{i}{D}\right)\right)}^{2}\in ℤ\wedge {P}\parallel {\Im \left(\left({A}+\mathrm{i}{B}\right)\left({C}+\mathrm{i}{D}\right)\right)}^{2}\right)\right)\to \left({P}\parallel {\Re \left(\left({A}+\mathrm{i}{B}\right)\left({C}+\mathrm{i}{D}\right)\right)}^{2}↔{P}\parallel \left({\Im \left(\left({A}+\mathrm{i}{B}\right)\left({C}+\mathrm{i}{D}\right)\right)}^{2}+{\Re \left(\left({A}+\mathrm{i}{B}\right)\left({C}+\mathrm{i}{D}\right)\right)}^{2}\right)\right)$
115 27 82 87 113 114 syl112anc ${⊢}{\phi }\to \left({P}\parallel {\Re \left(\left({A}+\mathrm{i}{B}\right)\left({C}+\mathrm{i}{D}\right)\right)}^{2}↔{P}\parallel \left({\Im \left(\left({A}+\mathrm{i}{B}\right)\left({C}+\mathrm{i}{D}\right)\right)}^{2}+{\Re \left(\left({A}+\mathrm{i}{B}\right)\left({C}+\mathrm{i}{D}\right)\right)}^{2}\right)\right)$
116 91 115 mpbird ${⊢}{\phi }\to {P}\parallel {\Re \left(\left({A}+\mathrm{i}{B}\right)\left({C}+\mathrm{i}{D}\right)\right)}^{2}$
117 prmdvdsexp ${⊢}\left({P}\in ℙ\wedge \Re \left(\left({A}+\mathrm{i}{B}\right)\left({C}+\mathrm{i}{D}\right)\right)\in ℤ\wedge 2\in ℕ\right)\to \left({P}\parallel {\Re \left(\left({A}+\mathrm{i}{B}\right)\left({C}+\mathrm{i}{D}\right)\right)}^{2}↔{P}\parallel \Re \left(\left({A}+\mathrm{i}{B}\right)\left({C}+\mathrm{i}{D}\right)\right)\right)$
118 3 80 110 117 syl3anc ${⊢}{\phi }\to \left({P}\parallel {\Re \left(\left({A}+\mathrm{i}{B}\right)\left({C}+\mathrm{i}{D}\right)\right)}^{2}↔{P}\parallel \Re \left(\left({A}+\mathrm{i}{B}\right)\left({C}+\mathrm{i}{D}\right)\right)\right)$
119 116 118 mpbid ${⊢}{\phi }\to {P}\parallel \Re \left(\left({A}+\mathrm{i}{B}\right)\left({C}+\mathrm{i}{D}\right)\right)$
120 dvdsval2 ${⊢}\left({P}\in ℤ\wedge {P}\ne 0\wedge \Re \left(\left({A}+\mathrm{i}{B}\right)\left({C}+\mathrm{i}{D}\right)\right)\in ℤ\right)\to \left({P}\parallel \Re \left(\left({A}+\mathrm{i}{B}\right)\left({C}+\mathrm{i}{D}\right)\right)↔\frac{\Re \left(\left({A}+\mathrm{i}{B}\right)\left({C}+\mathrm{i}{D}\right)\right)}{{P}}\in ℤ\right)$
121 27 22 80 120 syl3anc ${⊢}{\phi }\to \left({P}\parallel \Re \left(\left({A}+\mathrm{i}{B}\right)\left({C}+\mathrm{i}{D}\right)\right)↔\frac{\Re \left(\left({A}+\mathrm{i}{B}\right)\left({C}+\mathrm{i}{D}\right)\right)}{{P}}\in ℤ\right)$
122 119 121 mpbid ${⊢}{\phi }\to \frac{\Re \left(\left({A}+\mathrm{i}{B}\right)\left({C}+\mathrm{i}{D}\right)\right)}{{P}}\in ℤ$
123 25 122 eqeltrd ${⊢}{\phi }\to \Re \left(\frac{\left({A}+\mathrm{i}{B}\right)\left({C}+\mathrm{i}{D}\right)}{{P}}\right)\in ℤ$
124 24 18 22 imdivd ${⊢}{\phi }\to \Im \left(\frac{\left({A}+\mathrm{i}{B}\right)\left({C}+\mathrm{i}{D}\right)}{{P}}\right)=\frac{\Im \left(\left({A}+\mathrm{i}{B}\right)\left({C}+\mathrm{i}{D}\right)\right)}{{P}}$
125 dvdsval2 ${⊢}\left({P}\in ℤ\wedge {P}\ne 0\wedge \Im \left(\left({A}+\mathrm{i}{B}\right)\left({C}+\mathrm{i}{D}\right)\right)\in ℤ\right)\to \left({P}\parallel \Im \left(\left({A}+\mathrm{i}{B}\right)\left({C}+\mathrm{i}{D}\right)\right)↔\frac{\Im \left(\left({A}+\mathrm{i}{B}\right)\left({C}+\mathrm{i}{D}\right)\right)}{{P}}\in ℤ\right)$
126 27 22 85 125 syl3anc ${⊢}{\phi }\to \left({P}\parallel \Im \left(\left({A}+\mathrm{i}{B}\right)\left({C}+\mathrm{i}{D}\right)\right)↔\frac{\Im \left(\left({A}+\mathrm{i}{B}\right)\left({C}+\mathrm{i}{D}\right)\right)}{{P}}\in ℤ\right)$
127 108 126 mpbid ${⊢}{\phi }\to \frac{\Im \left(\left({A}+\mathrm{i}{B}\right)\left({C}+\mathrm{i}{D}\right)\right)}{{P}}\in ℤ$
128 124 127 eqeltrd ${⊢}{\phi }\to \Im \left(\frac{\left({A}+\mathrm{i}{B}\right)\left({C}+\mathrm{i}{D}\right)}{{P}}\right)\in ℤ$
129 elgz ${⊢}\frac{\left({A}+\mathrm{i}{B}\right)\left({C}+\mathrm{i}{D}\right)}{{P}}\in ℤ\left[i\right]↔\left(\frac{\left({A}+\mathrm{i}{B}\right)\left({C}+\mathrm{i}{D}\right)}{{P}}\in ℂ\wedge \Re \left(\frac{\left({A}+\mathrm{i}{B}\right)\left({C}+\mathrm{i}{D}\right)}{{P}}\right)\in ℤ\wedge \Im \left(\frac{\left({A}+\mathrm{i}{B}\right)\left({C}+\mathrm{i}{D}\right)}{{P}}\right)\in ℤ\right)$
130 23 123 128 129 syl3anbrc ${⊢}{\phi }\to \frac{\left({A}+\mathrm{i}{B}\right)\left({C}+\mathrm{i}{D}\right)}{{P}}\in ℤ\left[i\right]$
131 18 21 22 absdivd ${⊢}{\phi }\to \left|\frac{\left({A}+\mathrm{i}{B}\right)\left({C}+\mathrm{i}{D}\right)}{{P}}\right|=\frac{\left|\left({A}+\mathrm{i}{B}\right)\left({C}+\mathrm{i}{D}\right)\right|}{\left|{P}\right|}$
132 20 nnnn0d ${⊢}{\phi }\to {P}\in {ℕ}_{0}$
133 132 nn0ge0d ${⊢}{\phi }\to 0\le {P}$
134 24 133 absidd ${⊢}{\phi }\to \left|{P}\right|={P}$
135 134 oveq2d ${⊢}{\phi }\to \frac{\left|\left({A}+\mathrm{i}{B}\right)\left({C}+\mathrm{i}{D}\right)\right|}{\left|{P}\right|}=\frac{\left|\left({A}+\mathrm{i}{B}\right)\left({C}+\mathrm{i}{D}\right)\right|}{{P}}$
136 131 135 eqtrd ${⊢}{\phi }\to \left|\frac{\left({A}+\mathrm{i}{B}\right)\left({C}+\mathrm{i}{D}\right)}{{P}}\right|=\frac{\left|\left({A}+\mathrm{i}{B}\right)\left({C}+\mathrm{i}{D}\right)\right|}{{P}}$
137 136 oveq1d ${⊢}{\phi }\to {\left|\frac{\left({A}+\mathrm{i}{B}\right)\left({C}+\mathrm{i}{D}\right)}{{P}}\right|}^{2}={\left(\frac{\left|\left({A}+\mathrm{i}{B}\right)\left({C}+\mathrm{i}{D}\right)\right|}{{P}}\right)}^{2}$
138 18 abscld ${⊢}{\phi }\to \left|\left({A}+\mathrm{i}{B}\right)\left({C}+\mathrm{i}{D}\right)\right|\in ℝ$
139 138 recnd ${⊢}{\phi }\to \left|\left({A}+\mathrm{i}{B}\right)\left({C}+\mathrm{i}{D}\right)\right|\in ℂ$
140 139 21 22 sqdivd ${⊢}{\phi }\to {\left(\frac{\left|\left({A}+\mathrm{i}{B}\right)\left({C}+\mathrm{i}{D}\right)\right|}{{P}}\right)}^{2}=\frac{{\left|\left({A}+\mathrm{i}{B}\right)\left({C}+\mathrm{i}{D}\right)\right|}^{2}}{{{P}}^{2}}$
141 75 oveq1d ${⊢}{\phi }\to \frac{{\left|\left({A}+\mathrm{i}{B}\right)\left({C}+\mathrm{i}{D}\right)\right|}^{2}}{{{P}}^{2}}=\frac{{N}{{P}}^{2}}{{{P}}^{2}}$
142 20 nnsqcld ${⊢}{\phi }\to {{P}}^{2}\in ℕ$
143 142 nncnd ${⊢}{\phi }\to {{P}}^{2}\in ℂ$
144 142 nnne0d ${⊢}{\phi }\to {{P}}^{2}\ne 0$
145 69 143 144 divcan4d ${⊢}{\phi }\to \frac{{N}{{P}}^{2}}{{{P}}^{2}}={N}$
146 141 145 eqtrd ${⊢}{\phi }\to \frac{{\left|\left({A}+\mathrm{i}{B}\right)\left({C}+\mathrm{i}{D}\right)\right|}^{2}}{{{P}}^{2}}={N}$
147 137 140 146 3eqtrrd ${⊢}{\phi }\to {N}={\left|\frac{\left({A}+\mathrm{i}{B}\right)\left({C}+\mathrm{i}{D}\right)}{{P}}\right|}^{2}$
148 fveq2 ${⊢}{x}=\frac{\left({A}+\mathrm{i}{B}\right)\left({C}+\mathrm{i}{D}\right)}{{P}}\to \left|{x}\right|=\left|\frac{\left({A}+\mathrm{i}{B}\right)\left({C}+\mathrm{i}{D}\right)}{{P}}\right|$
149 148 oveq1d ${⊢}{x}=\frac{\left({A}+\mathrm{i}{B}\right)\left({C}+\mathrm{i}{D}\right)}{{P}}\to {\left|{x}\right|}^{2}={\left|\frac{\left({A}+\mathrm{i}{B}\right)\left({C}+\mathrm{i}{D}\right)}{{P}}\right|}^{2}$
150 149 rspceeqv ${⊢}\left(\frac{\left({A}+\mathrm{i}{B}\right)\left({C}+\mathrm{i}{D}\right)}{{P}}\in ℤ\left[i\right]\wedge {N}={\left|\frac{\left({A}+\mathrm{i}{B}\right)\left({C}+\mathrm{i}{D}\right)}{{P}}\right|}^{2}\right)\to \exists {x}\in ℤ\left[i\right]\phantom{\rule{.4em}{0ex}}{N}={\left|{x}\right|}^{2}$
151 130 147 150 syl2anc ${⊢}{\phi }\to \exists {x}\in ℤ\left[i\right]\phantom{\rule{.4em}{0ex}}{N}={\left|{x}\right|}^{2}$
152 1 2sqlem1 ${⊢}{N}\in {S}↔\exists {x}\in ℤ\left[i\right]\phantom{\rule{.4em}{0ex}}{N}={\left|{x}\right|}^{2}$
153 151 152 sylibr ${⊢}{\phi }\to {N}\in {S}$