Metamath Proof Explorer

Theorem 2sqlem3

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

Ref Expression
Hypotheses 2sq.1 
|- S = ran ( w e. Z[i] |-> ( ( abs ` w ) ^ 2 ) )
2sqlem5.1 
|- ( ph -> N e. NN )
2sqlem5.2 
|- ( ph -> P e. Prime )
2sqlem4.3 
|- ( ph -> A e. ZZ )
2sqlem4.4 
|- ( ph -> B e. ZZ )
2sqlem4.5 
|- ( ph -> C e. ZZ )
2sqlem4.6 
|- ( ph -> D e. ZZ )
2sqlem4.7 
|- ( ph -> ( N x. P ) = ( ( A ^ 2 ) + ( B ^ 2 ) ) )
2sqlem4.8 
|- ( ph -> P = ( ( C ^ 2 ) + ( D ^ 2 ) ) )
2sqlem4.9 
|- ( ph -> P || ( ( C x. B ) + ( A x. D ) ) )
Assertion 2sqlem3 
|- ( ph -> N e. S )

Proof

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