This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem 4sqlem17

Description: Lemma for 4sq . (Contributed by Mario Carneiro, 16-Jul-2014) (Revised by AV, 14-Sep-2020)

Ref Expression
Hypotheses 4sq.1 
|- S = { n | E. x e. ZZ E. y e. ZZ E. z e. ZZ E. w e. ZZ n = ( ( ( x ^ 2 ) + ( y ^ 2 ) ) + ( ( z ^ 2 ) + ( w ^ 2 ) ) ) }
4sq.2 
|- ( ph -> N e. NN )
4sq.3 
|- ( ph -> P = ( ( 2 x. N ) + 1 ) )
4sq.4 
|- ( ph -> P e. Prime )
4sq.5 
|- ( ph -> ( 0 ... ( 2 x. N ) ) C_ S )
4sq.6 
|- T = { i e. NN | ( i x. P ) e. S }
4sq.7 
|- M = inf ( T , RR , < )
4sq.m 
|- ( ph -> M e. ( ZZ>= ` 2 ) )
4sq.a 
|- ( ph -> A e. ZZ )
4sq.b 
|- ( ph -> B e. ZZ )
4sq.c 
|- ( ph -> C e. ZZ )
4sq.d 
|- ( ph -> D e. ZZ )
4sq.e 
|- E = ( ( ( A + ( M / 2 ) ) mod M ) - ( M / 2 ) )
4sq.f 
|- F = ( ( ( B + ( M / 2 ) ) mod M ) - ( M / 2 ) )
4sq.g 
|- G = ( ( ( C + ( M / 2 ) ) mod M ) - ( M / 2 ) )
4sq.h 
|- H = ( ( ( D + ( M / 2 ) ) mod M ) - ( M / 2 ) )
4sq.r 
|- R = ( ( ( ( E ^ 2 ) + ( F ^ 2 ) ) + ( ( G ^ 2 ) + ( H ^ 2 ) ) ) / M )
4sq.p 
|- ( ph -> ( M x. P ) = ( ( ( A ^ 2 ) + ( B ^ 2 ) ) + ( ( C ^ 2 ) + ( D ^ 2 ) ) ) )
Assertion 4sqlem17 
|- -. ph

Proof

Step Hyp Ref Expression
1 4sq.1 
 |-  S = { n | E. x e. ZZ E. y e. ZZ E. z e. ZZ E. w e. ZZ n = ( ( ( x ^ 2 ) + ( y ^ 2 ) ) + ( ( z ^ 2 ) + ( w ^ 2 ) ) ) }
2 4sq.2 
 |-  ( ph -> N e. NN )
3 4sq.3 
 |-  ( ph -> P = ( ( 2 x. N ) + 1 ) )
4 4sq.4 
 |-  ( ph -> P e. Prime )
5 4sq.5 
 |-  ( ph -> ( 0 ... ( 2 x. N ) ) C_ S )
6 4sq.6 
 |-  T = { i e. NN | ( i x. P ) e. S }
7 4sq.7 
 |-  M = inf ( T , RR , < )
8 4sq.m 
 |-  ( ph -> M e. ( ZZ>= ` 2 ) )
9 4sq.a 
 |-  ( ph -> A e. ZZ )
10 4sq.b 
 |-  ( ph -> B e. ZZ )
11 4sq.c 
 |-  ( ph -> C e. ZZ )
12 4sq.d 
 |-  ( ph -> D e. ZZ )
13 4sq.e 
 |-  E = ( ( ( A + ( M / 2 ) ) mod M ) - ( M / 2 ) )
14 4sq.f 
 |-  F = ( ( ( B + ( M / 2 ) ) mod M ) - ( M / 2 ) )
15 4sq.g 
 |-  G = ( ( ( C + ( M / 2 ) ) mod M ) - ( M / 2 ) )
16 4sq.h 
 |-  H = ( ( ( D + ( M / 2 ) ) mod M ) - ( M / 2 ) )
17 4sq.r 
 |-  R = ( ( ( ( E ^ 2 ) + ( F ^ 2 ) ) + ( ( G ^ 2 ) + ( H ^ 2 ) ) ) / M )
18 4sq.p 
 |-  ( ph -> ( M x. P ) = ( ( ( A ^ 2 ) + ( B ^ 2 ) ) + ( ( C ^ 2 ) + ( D ^ 2 ) ) ) )
19 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 4sqlem16 
 |-  ( ph -> ( R <_ M /\ ( ( R = 0 \/ R = M ) -> ( M ^ 2 ) || ( M x. P ) ) ) )
20 19 simpld 
 |-  ( ph -> R <_ M )
21 6 ssrab3 
 |-  T C_ NN
22 nnuz 
 |-  NN = ( ZZ>= ` 1 )
23 21 22 sseqtri 
 |-  T C_ ( ZZ>= ` 1 )
24 1 2 3 4 5 6 7 4sqlem13 
 |-  ( ph -> ( T =/= (/) /\ M < P ) )
25 24 simpld 
 |-  ( ph -> T =/= (/) )
26 infssuzcl 
 |-  ( ( T C_ ( ZZ>= ` 1 ) /\ T =/= (/) ) -> inf ( T , RR , < ) e. T )
27 23 25 26 sylancr 
 |-  ( ph -> inf ( T , RR , < ) e. T )
28 7 27 eqeltrid 
 |-  ( ph -> M e. T )
29 21 28 sselid 
 |-  ( ph -> M e. NN )
30 29 nnred 
 |-  ( ph -> M e. RR )
31 24 simprd 
 |-  ( ph -> M < P )
32 30 31 ltned 
 |-  ( ph -> M =/= P )
33 29 nncnd 
 |-  ( ph -> M e. CC )
34 33 sqvald 
 |-  ( ph -> ( M ^ 2 ) = ( M x. M ) )
35 34 breq1d 
 |-  ( ph -> ( ( M ^ 2 ) || ( M x. P ) <-> ( M x. M ) || ( M x. P ) ) )
36 29 nnzd 
 |-  ( ph -> M e. ZZ )
37 prmz 
 |-  ( P e. Prime -> P e. ZZ )
38 4 37 syl 
 |-  ( ph -> P e. ZZ )
39 29 nnne0d 
 |-  ( ph -> M =/= 0 )
40 dvdscmulr 
 |-  ( ( M e. ZZ /\ P e. ZZ /\ ( M e. ZZ /\ M =/= 0 ) ) -> ( ( M x. M ) || ( M x. P ) <-> M || P ) )
41 36 38 36 39 40 syl112anc 
 |-  ( ph -> ( ( M x. M ) || ( M x. P ) <-> M || P ) )
42 dvdsprm 
 |-  ( ( M e. ( ZZ>= ` 2 ) /\ P e. Prime ) -> ( M || P <-> M = P ) )
43 8 4 42 syl2anc 
 |-  ( ph -> ( M || P <-> M = P ) )
44 35 41 43 3bitrd 
 |-  ( ph -> ( ( M ^ 2 ) || ( M x. P ) <-> M = P ) )
45 44 necon3bbid 
 |-  ( ph -> ( -. ( M ^ 2 ) || ( M x. P ) <-> M =/= P ) )
46 32 45 mpbird 
 |-  ( ph -> -. ( M ^ 2 ) || ( M x. P ) )
47 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 4sqlem14 
 |-  ( ph -> R e. NN0 )
48 elnn0 
 |-  ( R e. NN0 <-> ( R e. NN \/ R = 0 ) )
49 47 48 sylib 
 |-  ( ph -> ( R e. NN \/ R = 0 ) )
50 49 ord 
 |-  ( ph -> ( -. R e. NN -> R = 0 ) )
51 orc 
 |-  ( R = 0 -> ( R = 0 \/ R = M ) )
52 19 simprd 
 |-  ( ph -> ( ( R = 0 \/ R = M ) -> ( M ^ 2 ) || ( M x. P ) ) )
53 51 52 syl5 
 |-  ( ph -> ( R = 0 -> ( M ^ 2 ) || ( M x. P ) ) )
54 50 53 syld 
 |-  ( ph -> ( -. R e. NN -> ( M ^ 2 ) || ( M x. P ) ) )
55 46 54 mt3d 
 |-  ( ph -> R e. NN )
56 gzreim 
 |-  ( ( A e. ZZ /\ B e. ZZ ) -> ( A + ( _i x. B ) ) e. Z[i] )
57 9 10 56 syl2anc 
 |-  ( ph -> ( A + ( _i x. B ) ) e. Z[i] )
58 gzcn 
 |-  ( ( A + ( _i x. B ) ) e. Z[i] -> ( A + ( _i x. B ) ) e. CC )
59 57 58 syl 
 |-  ( ph -> ( A + ( _i x. B ) ) e. CC )
60 59 absvalsq2d 
 |-  ( ph -> ( ( abs ` ( A + ( _i x. B ) ) ) ^ 2 ) = ( ( ( Re ` ( A + ( _i x. B ) ) ) ^ 2 ) + ( ( Im ` ( A + ( _i x. B ) ) ) ^ 2 ) ) )
61 9 zred 
 |-  ( ph -> A e. RR )
62 10 zred 
 |-  ( ph -> B e. RR )
63 61 62 crred 
 |-  ( ph -> ( Re ` ( A + ( _i x. B ) ) ) = A )
64 63 oveq1d 
 |-  ( ph -> ( ( Re ` ( A + ( _i x. B ) ) ) ^ 2 ) = ( A ^ 2 ) )
65 61 62 crimd 
 |-  ( ph -> ( Im ` ( A + ( _i x. B ) ) ) = B )
66 65 oveq1d 
 |-  ( ph -> ( ( Im ` ( A + ( _i x. B ) ) ) ^ 2 ) = ( B ^ 2 ) )
67 64 66 oveq12d 
 |-  ( ph -> ( ( ( Re ` ( A + ( _i x. B ) ) ) ^ 2 ) + ( ( Im ` ( A + ( _i x. B ) ) ) ^ 2 ) ) = ( ( A ^ 2 ) + ( B ^ 2 ) ) )
68 60 67 eqtrd 
 |-  ( ph -> ( ( abs ` ( A + ( _i x. B ) ) ) ^ 2 ) = ( ( A ^ 2 ) + ( B ^ 2 ) ) )
69 gzreim 
 |-  ( ( C e. ZZ /\ D e. ZZ ) -> ( C + ( _i x. D ) ) e. Z[i] )
70 11 12 69 syl2anc 
 |-  ( ph -> ( C + ( _i x. D ) ) e. Z[i] )
71 gzcn 
 |-  ( ( C + ( _i x. D ) ) e. Z[i] -> ( C + ( _i x. D ) ) e. CC )
72 70 71 syl 
 |-  ( ph -> ( C + ( _i x. D ) ) e. CC )
73 72 absvalsq2d 
 |-  ( ph -> ( ( abs ` ( C + ( _i x. D ) ) ) ^ 2 ) = ( ( ( Re ` ( C + ( _i x. D ) ) ) ^ 2 ) + ( ( Im ` ( C + ( _i x. D ) ) ) ^ 2 ) ) )
74 11 zred 
 |-  ( ph -> C e. RR )
75 12 zred 
 |-  ( ph -> D e. RR )
76 74 75 crred 
 |-  ( ph -> ( Re ` ( C + ( _i x. D ) ) ) = C )
77 76 oveq1d 
 |-  ( ph -> ( ( Re ` ( C + ( _i x. D ) ) ) ^ 2 ) = ( C ^ 2 ) )
78 74 75 crimd 
 |-  ( ph -> ( Im ` ( C + ( _i x. D ) ) ) = D )
79 78 oveq1d 
 |-  ( ph -> ( ( Im ` ( C + ( _i x. D ) ) ) ^ 2 ) = ( D ^ 2 ) )
80 77 79 oveq12d 
 |-  ( ph -> ( ( ( Re ` ( C + ( _i x. D ) ) ) ^ 2 ) + ( ( Im ` ( C + ( _i x. D ) ) ) ^ 2 ) ) = ( ( C ^ 2 ) + ( D ^ 2 ) ) )
81 73 80 eqtrd 
 |-  ( ph -> ( ( abs ` ( C + ( _i x. D ) ) ) ^ 2 ) = ( ( C ^ 2 ) + ( D ^ 2 ) ) )
82 68 81 oveq12d 
 |-  ( ph -> ( ( ( abs ` ( A + ( _i x. B ) ) ) ^ 2 ) + ( ( abs ` ( C + ( _i x. D ) ) ) ^ 2 ) ) = ( ( ( A ^ 2 ) + ( B ^ 2 ) ) + ( ( C ^ 2 ) + ( D ^ 2 ) ) ) )
83 18 82 eqtr4d 
 |-  ( ph -> ( M x. P ) = ( ( ( abs ` ( A + ( _i x. B ) ) ) ^ 2 ) + ( ( abs ` ( C + ( _i x. D ) ) ) ^ 2 ) ) )
84 83 oveq1d 
 |-  ( ph -> ( ( M x. P ) / M ) = ( ( ( ( abs ` ( A + ( _i x. B ) ) ) ^ 2 ) + ( ( abs ` ( C + ( _i x. D ) ) ) ^ 2 ) ) / M ) )
85 prmnn 
 |-  ( P e. Prime -> P e. NN )
86 4 85 syl 
 |-  ( ph -> P e. NN )
87 86 nncnd 
 |-  ( ph -> P e. CC )
88 87 33 39 divcan3d 
 |-  ( ph -> ( ( M x. P ) / M ) = P )
89 84 88 eqtr3d 
 |-  ( ph -> ( ( ( ( abs ` ( A + ( _i x. B ) ) ) ^ 2 ) + ( ( abs ` ( C + ( _i x. D ) ) ) ^ 2 ) ) / M ) = P )
90 9 29 13 4sqlem5 
 |-  ( ph -> ( E e. ZZ /\ ( ( A - E ) / M ) e. ZZ ) )
91 90 simpld 
 |-  ( ph -> E e. ZZ )
92 10 29 14 4sqlem5 
 |-  ( ph -> ( F e. ZZ /\ ( ( B - F ) / M ) e. ZZ ) )
93 92 simpld 
 |-  ( ph -> F e. ZZ )
94 gzreim 
 |-  ( ( E e. ZZ /\ F e. ZZ ) -> ( E + ( _i x. F ) ) e. Z[i] )
95 91 93 94 syl2anc 
 |-  ( ph -> ( E + ( _i x. F ) ) e. Z[i] )
96 gzcn 
 |-  ( ( E + ( _i x. F ) ) e. Z[i] -> ( E + ( _i x. F ) ) e. CC )
97 95 96 syl 
 |-  ( ph -> ( E + ( _i x. F ) ) e. CC )
98 97 absvalsq2d 
 |-  ( ph -> ( ( abs ` ( E + ( _i x. F ) ) ) ^ 2 ) = ( ( ( Re ` ( E + ( _i x. F ) ) ) ^ 2 ) + ( ( Im ` ( E + ( _i x. F ) ) ) ^ 2 ) ) )
99 91 zred 
 |-  ( ph -> E e. RR )
100 93 zred 
 |-  ( ph -> F e. RR )
101 99 100 crred 
 |-  ( ph -> ( Re ` ( E + ( _i x. F ) ) ) = E )
102 101 oveq1d 
 |-  ( ph -> ( ( Re ` ( E + ( _i x. F ) ) ) ^ 2 ) = ( E ^ 2 ) )
103 99 100 crimd 
 |-  ( ph -> ( Im ` ( E + ( _i x. F ) ) ) = F )
104 103 oveq1d 
 |-  ( ph -> ( ( Im ` ( E + ( _i x. F ) ) ) ^ 2 ) = ( F ^ 2 ) )
105 102 104 oveq12d 
 |-  ( ph -> ( ( ( Re ` ( E + ( _i x. F ) ) ) ^ 2 ) + ( ( Im ` ( E + ( _i x. F ) ) ) ^ 2 ) ) = ( ( E ^ 2 ) + ( F ^ 2 ) ) )
106 98 105 eqtrd 
 |-  ( ph -> ( ( abs ` ( E + ( _i x. F ) ) ) ^ 2 ) = ( ( E ^ 2 ) + ( F ^ 2 ) ) )
107 11 29 15 4sqlem5 
 |-  ( ph -> ( G e. ZZ /\ ( ( C - G ) / M ) e. ZZ ) )
108 107 simpld 
 |-  ( ph -> G e. ZZ )
109 12 29 16 4sqlem5 
 |-  ( ph -> ( H e. ZZ /\ ( ( D - H ) / M ) e. ZZ ) )
110 109 simpld 
 |-  ( ph -> H e. ZZ )
111 gzreim 
 |-  ( ( G e. ZZ /\ H e. ZZ ) -> ( G + ( _i x. H ) ) e. Z[i] )
112 108 110 111 syl2anc 
 |-  ( ph -> ( G + ( _i x. H ) ) e. Z[i] )
113 gzcn 
 |-  ( ( G + ( _i x. H ) ) e. Z[i] -> ( G + ( _i x. H ) ) e. CC )
114 112 113 syl 
 |-  ( ph -> ( G + ( _i x. H ) ) e. CC )
115 114 absvalsq2d 
 |-  ( ph -> ( ( abs ` ( G + ( _i x. H ) ) ) ^ 2 ) = ( ( ( Re ` ( G + ( _i x. H ) ) ) ^ 2 ) + ( ( Im ` ( G + ( _i x. H ) ) ) ^ 2 ) ) )
116 108 zred 
 |-  ( ph -> G e. RR )
117 110 zred 
 |-  ( ph -> H e. RR )
118 116 117 crred 
 |-  ( ph -> ( Re ` ( G + ( _i x. H ) ) ) = G )
119 118 oveq1d 
 |-  ( ph -> ( ( Re ` ( G + ( _i x. H ) ) ) ^ 2 ) = ( G ^ 2 ) )
120 116 117 crimd 
 |-  ( ph -> ( Im ` ( G + ( _i x. H ) ) ) = H )
121 120 oveq1d 
 |-  ( ph -> ( ( Im ` ( G + ( _i x. H ) ) ) ^ 2 ) = ( H ^ 2 ) )
122 119 121 oveq12d 
 |-  ( ph -> ( ( ( Re ` ( G + ( _i x. H ) ) ) ^ 2 ) + ( ( Im ` ( G + ( _i x. H ) ) ) ^ 2 ) ) = ( ( G ^ 2 ) + ( H ^ 2 ) ) )
123 115 122 eqtrd 
 |-  ( ph -> ( ( abs ` ( G + ( _i x. H ) ) ) ^ 2 ) = ( ( G ^ 2 ) + ( H ^ 2 ) ) )
124 106 123 oveq12d 
 |-  ( ph -> ( ( ( abs ` ( E + ( _i x. F ) ) ) ^ 2 ) + ( ( abs ` ( G + ( _i x. H ) ) ) ^ 2 ) ) = ( ( ( E ^ 2 ) + ( F ^ 2 ) ) + ( ( G ^ 2 ) + ( H ^ 2 ) ) ) )
125 124 oveq1d 
 |-  ( ph -> ( ( ( ( abs ` ( E + ( _i x. F ) ) ) ^ 2 ) + ( ( abs ` ( G + ( _i x. H ) ) ) ^ 2 ) ) / M ) = ( ( ( ( E ^ 2 ) + ( F ^ 2 ) ) + ( ( G ^ 2 ) + ( H ^ 2 ) ) ) / M ) )
126 125 17 eqtr4di 
 |-  ( ph -> ( ( ( ( abs ` ( E + ( _i x. F ) ) ) ^ 2 ) + ( ( abs ` ( G + ( _i x. H ) ) ) ^ 2 ) ) / M ) = R )
127 89 126 oveq12d 
 |-  ( ph -> ( ( ( ( ( abs ` ( A + ( _i x. B ) ) ) ^ 2 ) + ( ( abs ` ( C + ( _i x. D ) ) ) ^ 2 ) ) / M ) x. ( ( ( ( abs ` ( E + ( _i x. F ) ) ) ^ 2 ) + ( ( abs ` ( G + ( _i x. H ) ) ) ^ 2 ) ) / M ) ) = ( P x. R ) )
128 55 nncnd 
 |-  ( ph -> R e. CC )
129 87 128 mulcomd 
 |-  ( ph -> ( P x. R ) = ( R x. P ) )
130 127 129 eqtrd 
 |-  ( ph -> ( ( ( ( ( abs ` ( A + ( _i x. B ) ) ) ^ 2 ) + ( ( abs ` ( C + ( _i x. D ) ) ) ^ 2 ) ) / M ) x. ( ( ( ( abs ` ( E + ( _i x. F ) ) ) ^ 2 ) + ( ( abs ` ( G + ( _i x. H ) ) ) ^ 2 ) ) / M ) ) = ( R x. P ) )
131 eqid 
 |-  ( ( ( abs ` ( A + ( _i x. B ) ) ) ^ 2 ) + ( ( abs ` ( C + ( _i x. D ) ) ) ^ 2 ) ) = ( ( ( abs ` ( A + ( _i x. B ) ) ) ^ 2 ) + ( ( abs ` ( C + ( _i x. D ) ) ) ^ 2 ) )
132 eqid 
 |-  ( ( ( abs ` ( E + ( _i x. F ) ) ) ^ 2 ) + ( ( abs ` ( G + ( _i x. H ) ) ) ^ 2 ) ) = ( ( ( abs ` ( E + ( _i x. F ) ) ) ^ 2 ) + ( ( abs ` ( G + ( _i x. H ) ) ) ^ 2 ) )
133 9 zcnd 
 |-  ( ph -> A e. CC )
134 ax-icn 
 |-  _i e. CC
135 10 zcnd 
 |-  ( ph -> B e. CC )
136 mulcl 
 |-  ( ( _i e. CC /\ B e. CC ) -> ( _i x. B ) e. CC )
137 134 135 136 sylancr 
 |-  ( ph -> ( _i x. B ) e. CC )
138 91 zcnd 
 |-  ( ph -> E e. CC )
139 93 zcnd 
 |-  ( ph -> F e. CC )
140 mulcl 
 |-  ( ( _i e. CC /\ F e. CC ) -> ( _i x. F ) e. CC )
141 134 139 140 sylancr 
 |-  ( ph -> ( _i x. F ) e. CC )
142 133 137 138 141 addsub4d 
 |-  ( ph -> ( ( A + ( _i x. B ) ) - ( E + ( _i x. F ) ) ) = ( ( A - E ) + ( ( _i x. B ) - ( _i x. F ) ) ) )
143 134 a1i 
 |-  ( ph -> _i e. CC )
144 143 135 139 subdid 
 |-  ( ph -> ( _i x. ( B - F ) ) = ( ( _i x. B ) - ( _i x. F ) ) )
145 144 oveq2d 
 |-  ( ph -> ( ( A - E ) + ( _i x. ( B - F ) ) ) = ( ( A - E ) + ( ( _i x. B ) - ( _i x. F ) ) ) )
146 142 145 eqtr4d 
 |-  ( ph -> ( ( A + ( _i x. B ) ) - ( E + ( _i x. F ) ) ) = ( ( A - E ) + ( _i x. ( B - F ) ) ) )
147 146 oveq1d 
 |-  ( ph -> ( ( ( A + ( _i x. B ) ) - ( E + ( _i x. F ) ) ) / M ) = ( ( ( A - E ) + ( _i x. ( B - F ) ) ) / M ) )
148 133 138 subcld 
 |-  ( ph -> ( A - E ) e. CC )
149 135 139 subcld 
 |-  ( ph -> ( B - F ) e. CC )
150 mulcl 
 |-  ( ( _i e. CC /\ ( B - F ) e. CC ) -> ( _i x. ( B - F ) ) e. CC )
151 134 149 150 sylancr 
 |-  ( ph -> ( _i x. ( B - F ) ) e. CC )
152 148 151 33 39 divdird 
 |-  ( ph -> ( ( ( A - E ) + ( _i x. ( B - F ) ) ) / M ) = ( ( ( A - E ) / M ) + ( ( _i x. ( B - F ) ) / M ) ) )
153 143 149 33 39 divassd 
 |-  ( ph -> ( ( _i x. ( B - F ) ) / M ) = ( _i x. ( ( B - F ) / M ) ) )
154 153 oveq2d 
 |-  ( ph -> ( ( ( A - E ) / M ) + ( ( _i x. ( B - F ) ) / M ) ) = ( ( ( A - E ) / M ) + ( _i x. ( ( B - F ) / M ) ) ) )
155 147 152 154 3eqtrd 
 |-  ( ph -> ( ( ( A + ( _i x. B ) ) - ( E + ( _i x. F ) ) ) / M ) = ( ( ( A - E ) / M ) + ( _i x. ( ( B - F ) / M ) ) ) )
156 90 simprd 
 |-  ( ph -> ( ( A - E ) / M ) e. ZZ )
157 92 simprd 
 |-  ( ph -> ( ( B - F ) / M ) e. ZZ )
158 gzreim 
 |-  ( ( ( ( A - E ) / M ) e. ZZ /\ ( ( B - F ) / M ) e. ZZ ) -> ( ( ( A - E ) / M ) + ( _i x. ( ( B - F ) / M ) ) ) e. Z[i] )
159 156 157 158 syl2anc 
 |-  ( ph -> ( ( ( A - E ) / M ) + ( _i x. ( ( B - F ) / M ) ) ) e. Z[i] )
160 155 159 eqeltrd 
 |-  ( ph -> ( ( ( A + ( _i x. B ) ) - ( E + ( _i x. F ) ) ) / M ) e. Z[i] )
161 11 zcnd 
 |-  ( ph -> C e. CC )
162 12 zcnd 
 |-  ( ph -> D e. CC )
163 mulcl 
 |-  ( ( _i e. CC /\ D e. CC ) -> ( _i x. D ) e. CC )
164 134 162 163 sylancr 
 |-  ( ph -> ( _i x. D ) e. CC )
165 108 zcnd 
 |-  ( ph -> G e. CC )
166 110 zcnd 
 |-  ( ph -> H e. CC )
167 mulcl 
 |-  ( ( _i e. CC /\ H e. CC ) -> ( _i x. H ) e. CC )
168 134 166 167 sylancr 
 |-  ( ph -> ( _i x. H ) e. CC )
169 161 164 165 168 addsub4d 
 |-  ( ph -> ( ( C + ( _i x. D ) ) - ( G + ( _i x. H ) ) ) = ( ( C - G ) + ( ( _i x. D ) - ( _i x. H ) ) ) )
170 143 162 166 subdid 
 |-  ( ph -> ( _i x. ( D - H ) ) = ( ( _i x. D ) - ( _i x. H ) ) )
171 170 oveq2d 
 |-  ( ph -> ( ( C - G ) + ( _i x. ( D - H ) ) ) = ( ( C - G ) + ( ( _i x. D ) - ( _i x. H ) ) ) )
172 169 171 eqtr4d 
 |-  ( ph -> ( ( C + ( _i x. D ) ) - ( G + ( _i x. H ) ) ) = ( ( C - G ) + ( _i x. ( D - H ) ) ) )
173 172 oveq1d 
 |-  ( ph -> ( ( ( C + ( _i x. D ) ) - ( G + ( _i x. H ) ) ) / M ) = ( ( ( C - G ) + ( _i x. ( D - H ) ) ) / M ) )
174 161 165 subcld 
 |-  ( ph -> ( C - G ) e. CC )
175 162 166 subcld 
 |-  ( ph -> ( D - H ) e. CC )
176 mulcl 
 |-  ( ( _i e. CC /\ ( D - H ) e. CC ) -> ( _i x. ( D - H ) ) e. CC )
177 134 175 176 sylancr 
 |-  ( ph -> ( _i x. ( D - H ) ) e. CC )
178 174 177 33 39 divdird 
 |-  ( ph -> ( ( ( C - G ) + ( _i x. ( D - H ) ) ) / M ) = ( ( ( C - G ) / M ) + ( ( _i x. ( D - H ) ) / M ) ) )
179 143 175 33 39 divassd 
 |-  ( ph -> ( ( _i x. ( D - H ) ) / M ) = ( _i x. ( ( D - H ) / M ) ) )
180 179 oveq2d 
 |-  ( ph -> ( ( ( C - G ) / M ) + ( ( _i x. ( D - H ) ) / M ) ) = ( ( ( C - G ) / M ) + ( _i x. ( ( D - H ) / M ) ) ) )
181 173 178 180 3eqtrd 
 |-  ( ph -> ( ( ( C + ( _i x. D ) ) - ( G + ( _i x. H ) ) ) / M ) = ( ( ( C - G ) / M ) + ( _i x. ( ( D - H ) / M ) ) ) )
182 107 simprd 
 |-  ( ph -> ( ( C - G ) / M ) e. ZZ )
183 109 simprd 
 |-  ( ph -> ( ( D - H ) / M ) e. ZZ )
184 gzreim 
 |-  ( ( ( ( C - G ) / M ) e. ZZ /\ ( ( D - H ) / M ) e. ZZ ) -> ( ( ( C - G ) / M ) + ( _i x. ( ( D - H ) / M ) ) ) e. Z[i] )
185 182 183 184 syl2anc 
 |-  ( ph -> ( ( ( C - G ) / M ) + ( _i x. ( ( D - H ) / M ) ) ) e. Z[i] )
186 181 185 eqeltrd 
 |-  ( ph -> ( ( ( C + ( _i x. D ) ) - ( G + ( _i x. H ) ) ) / M ) e. Z[i] )
187 86 nnnn0d 
 |-  ( ph -> P e. NN0 )
188 89 187 eqeltrd 
 |-  ( ph -> ( ( ( ( abs ` ( A + ( _i x. B ) ) ) ^ 2 ) + ( ( abs ` ( C + ( _i x. D ) ) ) ^ 2 ) ) / M ) e. NN0 )
189 1 57 70 95 112 131 132 29 160 186 188 mul4sqlem 
 |-  ( ph -> ( ( ( ( ( abs ` ( A + ( _i x. B ) ) ) ^ 2 ) + ( ( abs ` ( C + ( _i x. D ) ) ) ^ 2 ) ) / M ) x. ( ( ( ( abs ` ( E + ( _i x. F ) ) ) ^ 2 ) + ( ( abs ` ( G + ( _i x. H ) ) ) ^ 2 ) ) / M ) ) e. S )
190 130 189 eqeltrrd 
 |-  ( ph -> ( R x. P ) e. S )
191 oveq1 
 |-  ( i = R -> ( i x. P ) = ( R x. P ) )
192 191 eleq1d 
 |-  ( i = R -> ( ( i x. P ) e. S <-> ( R x. P ) e. S ) )
193 192 6 elrab2 
 |-  ( R e. T <-> ( R e. NN /\ ( R x. P ) e. S ) )
194 55 190 193 sylanbrc 
 |-  ( ph -> R e. T )
195 infssuzle 
 |-  ( ( T C_ ( ZZ>= ` 1 ) /\ R e. T ) -> inf ( T , RR , < ) <_ R )
196 23 194 195 sylancr 
 |-  ( ph -> inf ( T , RR , < ) <_ R )
197 7 196 eqbrtrid 
 |-  ( ph -> M <_ R )
198 55 nnred 
 |-  ( ph -> R e. RR )
199 198 30 letri3d 
 |-  ( ph -> ( R = M <-> ( R <_ M /\ M <_ R ) ) )
200 20 197 199 mpbir2and 
 |-  ( ph -> R = M )
201 200 olcd 
 |-  ( ph -> ( R = 0 \/ R = M ) )
202 201 52 mpd 
 |-  ( ph -> ( M ^ 2 ) || ( M x. P ) )
203 202 46 pm2.65i 
 |-  -. ph