Metamath Proof Explorer

Theorem lgsquad2lem1

Description: Lemma for lgsquad2 . (Contributed by Mario Carneiro, 19-Jun-2015)

Ref Expression
Hypotheses lgsquad2.1 
|- ( ph -> M e. NN )
lgsquad2.2 
|- ( ph -> -. 2 || M )
lgsquad2.3 
|- ( ph -> N e. NN )
lgsquad2.4 
|- ( ph -> -. 2 || N )
lgsquad2.5 
|- ( ph -> ( M gcd N ) = 1 )
lgsquad2lem1.a 
|- ( ph -> A e. NN )
lgsquad2lem1.b 
|- ( ph -> B e. NN )
lgsquad2lem1.m 
|- ( ph -> ( A x. B ) = M )
lgsquad2lem1.1 
|- ( ph -> ( ( A /L N ) x. ( N /L A ) ) = ( -u 1 ^ ( ( ( A - 1 ) / 2 ) x. ( ( N - 1 ) / 2 ) ) ) )
lgsquad2lem1.2 
|- ( ph -> ( ( B /L N ) x. ( N /L B ) ) = ( -u 1 ^ ( ( ( B - 1 ) / 2 ) x. ( ( N - 1 ) / 2 ) ) ) )
Assertion lgsquad2lem1 
|- ( ph -> ( ( M /L N ) x. ( N /L M ) ) = ( -u 1 ^ ( ( ( M - 1 ) / 2 ) x. ( ( N - 1 ) / 2 ) ) ) )

Proof

Step Hyp Ref Expression
1 lgsquad2.1 
 |-  ( ph -> M e. NN )
2 lgsquad2.2 
 |-  ( ph -> -. 2 || M )
3 lgsquad2.3 
 |-  ( ph -> N e. NN )
4 lgsquad2.4 
 |-  ( ph -> -. 2 || N )
5 lgsquad2.5 
 |-  ( ph -> ( M gcd N ) = 1 )
6 lgsquad2lem1.a 
 |-  ( ph -> A e. NN )
7 lgsquad2lem1.b 
 |-  ( ph -> B e. NN )
8 lgsquad2lem1.m 
 |-  ( ph -> ( A x. B ) = M )
9 lgsquad2lem1.1 
 |-  ( ph -> ( ( A /L N ) x. ( N /L A ) ) = ( -u 1 ^ ( ( ( A - 1 ) / 2 ) x. ( ( N - 1 ) / 2 ) ) ) )
10 lgsquad2lem1.2 
 |-  ( ph -> ( ( B /L N ) x. ( N /L B ) ) = ( -u 1 ^ ( ( ( B - 1 ) / 2 ) x. ( ( N - 1 ) / 2 ) ) ) )
11 6 nnzd 
 |-  ( ph -> A e. ZZ )
12 11 zcnd 
 |-  ( ph -> A e. CC )
13 ax-1cn 
 |-  1 e. CC
14 npcan 
 |-  ( ( A e. CC /\ 1 e. CC ) -> ( ( A - 1 ) + 1 ) = A )
15 12 13 14 sylancl 
 |-  ( ph -> ( ( A - 1 ) + 1 ) = A )
16 7 nnzd 
 |-  ( ph -> B e. ZZ )
17 16 zcnd 
 |-  ( ph -> B e. CC )
18 npcan 
 |-  ( ( B e. CC /\ 1 e. CC ) -> ( ( B - 1 ) + 1 ) = B )
19 17 13 18 sylancl 
 |-  ( ph -> ( ( B - 1 ) + 1 ) = B )
20 15 19 oveq12d 
 |-  ( ph -> ( ( ( A - 1 ) + 1 ) x. ( ( B - 1 ) + 1 ) ) = ( A x. B ) )
21 peano2zm 
 |-  ( A e. ZZ -> ( A - 1 ) e. ZZ )
22 11 21 syl 
 |-  ( ph -> ( A - 1 ) e. ZZ )
23 22 zcnd 
 |-  ( ph -> ( A - 1 ) e. CC )
24 13 a1i 
 |-  ( ph -> 1 e. CC )
25 peano2zm 
 |-  ( B e. ZZ -> ( B - 1 ) e. ZZ )
26 16 25 syl 
 |-  ( ph -> ( B - 1 ) e. ZZ )
27 26 zcnd 
 |-  ( ph -> ( B - 1 ) e. CC )
28 23 24 27 24 muladdd 
 |-  ( ph -> ( ( ( A - 1 ) + 1 ) x. ( ( B - 1 ) + 1 ) ) = ( ( ( ( A - 1 ) x. ( B - 1 ) ) + ( 1 x. 1 ) ) + ( ( ( A - 1 ) x. 1 ) + ( ( B - 1 ) x. 1 ) ) ) )
29 1t1e1 
 |-  ( 1 x. 1 ) = 1
30 29 a1i 
 |-  ( ph -> ( 1 x. 1 ) = 1 )
31 30 oveq2d 
 |-  ( ph -> ( ( ( A - 1 ) x. ( B - 1 ) ) + ( 1 x. 1 ) ) = ( ( ( A - 1 ) x. ( B - 1 ) ) + 1 ) )
32 23 mulid1d 
 |-  ( ph -> ( ( A - 1 ) x. 1 ) = ( A - 1 ) )
33 27 mulid1d 
 |-  ( ph -> ( ( B - 1 ) x. 1 ) = ( B - 1 ) )
34 32 33 oveq12d 
 |-  ( ph -> ( ( ( A - 1 ) x. 1 ) + ( ( B - 1 ) x. 1 ) ) = ( ( A - 1 ) + ( B - 1 ) ) )
35 31 34 oveq12d 
 |-  ( ph -> ( ( ( ( A - 1 ) x. ( B - 1 ) ) + ( 1 x. 1 ) ) + ( ( ( A - 1 ) x. 1 ) + ( ( B - 1 ) x. 1 ) ) ) = ( ( ( ( A - 1 ) x. ( B - 1 ) ) + 1 ) + ( ( A - 1 ) + ( B - 1 ) ) ) )
36 28 35 eqtrd 
 |-  ( ph -> ( ( ( A - 1 ) + 1 ) x. ( ( B - 1 ) + 1 ) ) = ( ( ( ( A - 1 ) x. ( B - 1 ) ) + 1 ) + ( ( A - 1 ) + ( B - 1 ) ) ) )
37 20 36 eqtr3d 
 |-  ( ph -> ( A x. B ) = ( ( ( ( A - 1 ) x. ( B - 1 ) ) + 1 ) + ( ( A - 1 ) + ( B - 1 ) ) ) )
38 8 37 eqtr3d 
 |-  ( ph -> M = ( ( ( ( A - 1 ) x. ( B - 1 ) ) + 1 ) + ( ( A - 1 ) + ( B - 1 ) ) ) )
39 38 oveq1d 
 |-  ( ph -> ( M - 1 ) = ( ( ( ( ( A - 1 ) x. ( B - 1 ) ) + 1 ) + ( ( A - 1 ) + ( B - 1 ) ) ) - 1 ) )
40 23 27 mulcld 
 |-  ( ph -> ( ( A - 1 ) x. ( B - 1 ) ) e. CC )
41 addcl 
 |-  ( ( ( ( A - 1 ) x. ( B - 1 ) ) e. CC /\ 1 e. CC ) -> ( ( ( A - 1 ) x. ( B - 1 ) ) + 1 ) e. CC )
42 40 13 41 sylancl 
 |-  ( ph -> ( ( ( A - 1 ) x. ( B - 1 ) ) + 1 ) e. CC )
43 23 27 addcld 
 |-  ( ph -> ( ( A - 1 ) + ( B - 1 ) ) e. CC )
44 42 43 24 addsubd 
 |-  ( ph -> ( ( ( ( ( A - 1 ) x. ( B - 1 ) ) + 1 ) + ( ( A - 1 ) + ( B - 1 ) ) ) - 1 ) = ( ( ( ( ( A - 1 ) x. ( B - 1 ) ) + 1 ) - 1 ) + ( ( A - 1 ) + ( B - 1 ) ) ) )
45 pncan 
 |-  ( ( ( ( A - 1 ) x. ( B - 1 ) ) e. CC /\ 1 e. CC ) -> ( ( ( ( A - 1 ) x. ( B - 1 ) ) + 1 ) - 1 ) = ( ( A - 1 ) x. ( B - 1 ) ) )
46 40 13 45 sylancl 
 |-  ( ph -> ( ( ( ( A - 1 ) x. ( B - 1 ) ) + 1 ) - 1 ) = ( ( A - 1 ) x. ( B - 1 ) ) )
47 46 oveq1d 
 |-  ( ph -> ( ( ( ( ( A - 1 ) x. ( B - 1 ) ) + 1 ) - 1 ) + ( ( A - 1 ) + ( B - 1 ) ) ) = ( ( ( A - 1 ) x. ( B - 1 ) ) + ( ( A - 1 ) + ( B - 1 ) ) ) )
48 39 44 47 3eqtrd 
 |-  ( ph -> ( M - 1 ) = ( ( ( A - 1 ) x. ( B - 1 ) ) + ( ( A - 1 ) + ( B - 1 ) ) ) )
49 48 oveq1d 
 |-  ( ph -> ( ( M - 1 ) / 2 ) = ( ( ( ( A - 1 ) x. ( B - 1 ) ) + ( ( A - 1 ) + ( B - 1 ) ) ) / 2 ) )
50 2cnd 
 |-  ( ph -> 2 e. CC )
51 2ne0 
 |-  2 =/= 0
52 51 a1i 
 |-  ( ph -> 2 =/= 0 )
53 40 43 50 52 divdird 
 |-  ( ph -> ( ( ( ( A - 1 ) x. ( B - 1 ) ) + ( ( A - 1 ) + ( B - 1 ) ) ) / 2 ) = ( ( ( ( A - 1 ) x. ( B - 1 ) ) / 2 ) + ( ( ( A - 1 ) + ( B - 1 ) ) / 2 ) ) )
54 23 27 50 52 divassd 
 |-  ( ph -> ( ( ( A - 1 ) x. ( B - 1 ) ) / 2 ) = ( ( A - 1 ) x. ( ( B - 1 ) / 2 ) ) )
55 23 50 52 divcan2d 
 |-  ( ph -> ( 2 x. ( ( A - 1 ) / 2 ) ) = ( A - 1 ) )
56 55 oveq1d 
 |-  ( ph -> ( ( 2 x. ( ( A - 1 ) / 2 ) ) x. ( ( B - 1 ) / 2 ) ) = ( ( A - 1 ) x. ( ( B - 1 ) / 2 ) ) )
57 dvdsmul1 
 |-  ( ( A e. ZZ /\ B e. ZZ ) -> A || ( A x. B ) )
58 11 16 57 syl2anc 
 |-  ( ph -> A || ( A x. B ) )
59 58 8 breqtrd 
 |-  ( ph -> A || M )
60 2z 
 |-  2 e. ZZ
61 1 nnzd 
 |-  ( ph -> M e. ZZ )
62 dvdstr 
 |-  ( ( 2 e. ZZ /\ A e. ZZ /\ M e. ZZ ) -> ( ( 2 || A /\ A || M ) -> 2 || M ) )
63 60 11 61 62 mp3an2i 
 |-  ( ph -> ( ( 2 || A /\ A || M ) -> 2 || M ) )
64 59 63 mpan2d 
 |-  ( ph -> ( 2 || A -> 2 || M ) )
65 2 64 mtod 
 |-  ( ph -> -. 2 || A )
66 1zzd 
 |-  ( ph -> 1 e. ZZ )
67 2prm 
 |-  2 e. Prime
68 nprmdvds1 
 |-  ( 2 e. Prime -> -. 2 || 1 )
69 67 68 mp1i 
 |-  ( ph -> -. 2 || 1 )
70 omoe 
 |-  ( ( ( A e. ZZ /\ -. 2 || A ) /\ ( 1 e. ZZ /\ -. 2 || 1 ) ) -> 2 || ( A - 1 ) )
71 11 65 66 69 70 syl22anc 
 |-  ( ph -> 2 || ( A - 1 ) )
72 dvdsval2 
 |-  ( ( 2 e. ZZ /\ 2 =/= 0 /\ ( A - 1 ) e. ZZ ) -> ( 2 || ( A - 1 ) <-> ( ( A - 1 ) / 2 ) e. ZZ ) )
73 60 52 22 72 mp3an2i 
 |-  ( ph -> ( 2 || ( A - 1 ) <-> ( ( A - 1 ) / 2 ) e. ZZ ) )
74 71 73 mpbid 
 |-  ( ph -> ( ( A - 1 ) / 2 ) e. ZZ )
75 74 zcnd 
 |-  ( ph -> ( ( A - 1 ) / 2 ) e. CC )
76 dvdsmul2 
 |-  ( ( A e. ZZ /\ B e. ZZ ) -> B || ( A x. B ) )
77 11 16 76 syl2anc 
 |-  ( ph -> B || ( A x. B ) )
78 77 8 breqtrd 
 |-  ( ph -> B || M )
79 dvdstr 
 |-  ( ( 2 e. ZZ /\ B e. ZZ /\ M e. ZZ ) -> ( ( 2 || B /\ B || M ) -> 2 || M ) )
80 60 16 61 79 mp3an2i 
 |-  ( ph -> ( ( 2 || B /\ B || M ) -> 2 || M ) )
81 78 80 mpan2d 
 |-  ( ph -> ( 2 || B -> 2 || M ) )
82 2 81 mtod 
 |-  ( ph -> -. 2 || B )
83 omoe 
 |-  ( ( ( B e. ZZ /\ -. 2 || B ) /\ ( 1 e. ZZ /\ -. 2 || 1 ) ) -> 2 || ( B - 1 ) )
84 16 82 66 69 83 syl22anc 
 |-  ( ph -> 2 || ( B - 1 ) )
85 dvdsval2 
 |-  ( ( 2 e. ZZ /\ 2 =/= 0 /\ ( B - 1 ) e. ZZ ) -> ( 2 || ( B - 1 ) <-> ( ( B - 1 ) / 2 ) e. ZZ ) )
86 60 52 26 85 mp3an2i 
 |-  ( ph -> ( 2 || ( B - 1 ) <-> ( ( B - 1 ) / 2 ) e. ZZ ) )
87 84 86 mpbid 
 |-  ( ph -> ( ( B - 1 ) / 2 ) e. ZZ )
88 87 zcnd 
 |-  ( ph -> ( ( B - 1 ) / 2 ) e. CC )
89 50 75 88 mulassd 
 |-  ( ph -> ( ( 2 x. ( ( A - 1 ) / 2 ) ) x. ( ( B - 1 ) / 2 ) ) = ( 2 x. ( ( ( A - 1 ) / 2 ) x. ( ( B - 1 ) / 2 ) ) ) )
90 54 56 89 3eqtr2d 
 |-  ( ph -> ( ( ( A - 1 ) x. ( B - 1 ) ) / 2 ) = ( 2 x. ( ( ( A - 1 ) / 2 ) x. ( ( B - 1 ) / 2 ) ) ) )
91 23 27 50 52 divdird 
 |-  ( ph -> ( ( ( A - 1 ) + ( B - 1 ) ) / 2 ) = ( ( ( A - 1 ) / 2 ) + ( ( B - 1 ) / 2 ) ) )
92 90 91 oveq12d 
 |-  ( ph -> ( ( ( ( A - 1 ) x. ( B - 1 ) ) / 2 ) + ( ( ( A - 1 ) + ( B - 1 ) ) / 2 ) ) = ( ( 2 x. ( ( ( A - 1 ) / 2 ) x. ( ( B - 1 ) / 2 ) ) ) + ( ( ( A - 1 ) / 2 ) + ( ( B - 1 ) / 2 ) ) ) )
93 49 53 92 3eqtrd 
 |-  ( ph -> ( ( M - 1 ) / 2 ) = ( ( 2 x. ( ( ( A - 1 ) / 2 ) x. ( ( B - 1 ) / 2 ) ) ) + ( ( ( A - 1 ) / 2 ) + ( ( B - 1 ) / 2 ) ) ) )
94 93 oveq1d 
 |-  ( ph -> ( ( ( M - 1 ) / 2 ) x. ( ( N - 1 ) / 2 ) ) = ( ( ( 2 x. ( ( ( A - 1 ) / 2 ) x. ( ( B - 1 ) / 2 ) ) ) + ( ( ( A - 1 ) / 2 ) + ( ( B - 1 ) / 2 ) ) ) x. ( ( N - 1 ) / 2 ) ) )
95 60 a1i 
 |-  ( ph -> 2 e. ZZ )
96 74 87 zmulcld 
 |-  ( ph -> ( ( ( A - 1 ) / 2 ) x. ( ( B - 1 ) / 2 ) ) e. ZZ )
97 95 96 zmulcld 
 |-  ( ph -> ( 2 x. ( ( ( A - 1 ) / 2 ) x. ( ( B - 1 ) / 2 ) ) ) e. ZZ )
98 97 zcnd 
 |-  ( ph -> ( 2 x. ( ( ( A - 1 ) / 2 ) x. ( ( B - 1 ) / 2 ) ) ) e. CC )
99 74 87 zaddcld 
 |-  ( ph -> ( ( ( A - 1 ) / 2 ) + ( ( B - 1 ) / 2 ) ) e. ZZ )
100 99 zcnd 
 |-  ( ph -> ( ( ( A - 1 ) / 2 ) + ( ( B - 1 ) / 2 ) ) e. CC )
101 3 nnzd 
 |-  ( ph -> N e. ZZ )
102 omoe 
 |-  ( ( ( N e. ZZ /\ -. 2 || N ) /\ ( 1 e. ZZ /\ -. 2 || 1 ) ) -> 2 || ( N - 1 ) )
103 101 4 66 69 102 syl22anc 
 |-  ( ph -> 2 || ( N - 1 ) )
104 peano2zm 
 |-  ( N e. ZZ -> ( N - 1 ) e. ZZ )
105 101 104 syl 
 |-  ( ph -> ( N - 1 ) e. ZZ )
106 dvdsval2 
 |-  ( ( 2 e. ZZ /\ 2 =/= 0 /\ ( N - 1 ) e. ZZ ) -> ( 2 || ( N - 1 ) <-> ( ( N - 1 ) / 2 ) e. ZZ ) )
107 60 52 105 106 mp3an2i 
 |-  ( ph -> ( 2 || ( N - 1 ) <-> ( ( N - 1 ) / 2 ) e. ZZ ) )
108 103 107 mpbid 
 |-  ( ph -> ( ( N - 1 ) / 2 ) e. ZZ )
109 108 zcnd 
 |-  ( ph -> ( ( N - 1 ) / 2 ) e. CC )
110 98 100 109 adddird 
 |-  ( ph -> ( ( ( 2 x. ( ( ( A - 1 ) / 2 ) x. ( ( B - 1 ) / 2 ) ) ) + ( ( ( A - 1 ) / 2 ) + ( ( B - 1 ) / 2 ) ) ) x. ( ( N - 1 ) / 2 ) ) = ( ( ( 2 x. ( ( ( A - 1 ) / 2 ) x. ( ( B - 1 ) / 2 ) ) ) x. ( ( N - 1 ) / 2 ) ) + ( ( ( ( A - 1 ) / 2 ) + ( ( B - 1 ) / 2 ) ) x. ( ( N - 1 ) / 2 ) ) ) )
111 96 zcnd 
 |-  ( ph -> ( ( ( A - 1 ) / 2 ) x. ( ( B - 1 ) / 2 ) ) e. CC )
112 50 111 109 mulassd 
 |-  ( ph -> ( ( 2 x. ( ( ( A - 1 ) / 2 ) x. ( ( B - 1 ) / 2 ) ) ) x. ( ( N - 1 ) / 2 ) ) = ( 2 x. ( ( ( ( A - 1 ) / 2 ) x. ( ( B - 1 ) / 2 ) ) x. ( ( N - 1 ) / 2 ) ) ) )
113 112 oveq1d 
 |-  ( ph -> ( ( ( 2 x. ( ( ( A - 1 ) / 2 ) x. ( ( B - 1 ) / 2 ) ) ) x. ( ( N - 1 ) / 2 ) ) + ( ( ( ( A - 1 ) / 2 ) + ( ( B - 1 ) / 2 ) ) x. ( ( N - 1 ) / 2 ) ) ) = ( ( 2 x. ( ( ( ( A - 1 ) / 2 ) x. ( ( B - 1 ) / 2 ) ) x. ( ( N - 1 ) / 2 ) ) ) + ( ( ( ( A - 1 ) / 2 ) + ( ( B - 1 ) / 2 ) ) x. ( ( N - 1 ) / 2 ) ) ) )
114 94 110 113 3eqtrd 
 |-  ( ph -> ( ( ( M - 1 ) / 2 ) x. ( ( N - 1 ) / 2 ) ) = ( ( 2 x. ( ( ( ( A - 1 ) / 2 ) x. ( ( B - 1 ) / 2 ) ) x. ( ( N - 1 ) / 2 ) ) ) + ( ( ( ( A - 1 ) / 2 ) + ( ( B - 1 ) / 2 ) ) x. ( ( N - 1 ) / 2 ) ) ) )
115 114 oveq2d 
 |-  ( ph -> ( -u 1 ^ ( ( ( M - 1 ) / 2 ) x. ( ( N - 1 ) / 2 ) ) ) = ( -u 1 ^ ( ( 2 x. ( ( ( ( A - 1 ) / 2 ) x. ( ( B - 1 ) / 2 ) ) x. ( ( N - 1 ) / 2 ) ) ) + ( ( ( ( A - 1 ) / 2 ) + ( ( B - 1 ) / 2 ) ) x. ( ( N - 1 ) / 2 ) ) ) ) )
116 neg1cn 
 |-  -u 1 e. CC
117 116 a1i 
 |-  ( ph -> -u 1 e. CC )
118 neg1ne0 
 |-  -u 1 =/= 0
119 118 a1i 
 |-  ( ph -> -u 1 =/= 0 )
120 96 108 zmulcld 
 |-  ( ph -> ( ( ( ( A - 1 ) / 2 ) x. ( ( B - 1 ) / 2 ) ) x. ( ( N - 1 ) / 2 ) ) e. ZZ )
121 95 120 zmulcld 
 |-  ( ph -> ( 2 x. ( ( ( ( A - 1 ) / 2 ) x. ( ( B - 1 ) / 2 ) ) x. ( ( N - 1 ) / 2 ) ) ) e. ZZ )
122 99 108 zmulcld 
 |-  ( ph -> ( ( ( ( A - 1 ) / 2 ) + ( ( B - 1 ) / 2 ) ) x. ( ( N - 1 ) / 2 ) ) e. ZZ )
123 expaddz 
 |-  ( ( ( -u 1 e. CC /\ -u 1 =/= 0 ) /\ ( ( 2 x. ( ( ( ( A - 1 ) / 2 ) x. ( ( B - 1 ) / 2 ) ) x. ( ( N - 1 ) / 2 ) ) ) e. ZZ /\ ( ( ( ( A - 1 ) / 2 ) + ( ( B - 1 ) / 2 ) ) x. ( ( N - 1 ) / 2 ) ) e. ZZ ) ) -> ( -u 1 ^ ( ( 2 x. ( ( ( ( A - 1 ) / 2 ) x. ( ( B - 1 ) / 2 ) ) x. ( ( N - 1 ) / 2 ) ) ) + ( ( ( ( A - 1 ) / 2 ) + ( ( B - 1 ) / 2 ) ) x. ( ( N - 1 ) / 2 ) ) ) ) = ( ( -u 1 ^ ( 2 x. ( ( ( ( A - 1 ) / 2 ) x. ( ( B - 1 ) / 2 ) ) x. ( ( N - 1 ) / 2 ) ) ) ) x. ( -u 1 ^ ( ( ( ( A - 1 ) / 2 ) + ( ( B - 1 ) / 2 ) ) x. ( ( N - 1 ) / 2 ) ) ) ) )
124 117 119 121 122 123 syl22anc 
 |-  ( ph -> ( -u 1 ^ ( ( 2 x. ( ( ( ( A - 1 ) / 2 ) x. ( ( B - 1 ) / 2 ) ) x. ( ( N - 1 ) / 2 ) ) ) + ( ( ( ( A - 1 ) / 2 ) + ( ( B - 1 ) / 2 ) ) x. ( ( N - 1 ) / 2 ) ) ) ) = ( ( -u 1 ^ ( 2 x. ( ( ( ( A - 1 ) / 2 ) x. ( ( B - 1 ) / 2 ) ) x. ( ( N - 1 ) / 2 ) ) ) ) x. ( -u 1 ^ ( ( ( ( A - 1 ) / 2 ) + ( ( B - 1 ) / 2 ) ) x. ( ( N - 1 ) / 2 ) ) ) ) )
125 expmulz 
 |-  ( ( ( -u 1 e. CC /\ -u 1 =/= 0 ) /\ ( 2 e. ZZ /\ ( ( ( ( A - 1 ) / 2 ) x. ( ( B - 1 ) / 2 ) ) x. ( ( N - 1 ) / 2 ) ) e. ZZ ) ) -> ( -u 1 ^ ( 2 x. ( ( ( ( A - 1 ) / 2 ) x. ( ( B - 1 ) / 2 ) ) x. ( ( N - 1 ) / 2 ) ) ) ) = ( ( -u 1 ^ 2 ) ^ ( ( ( ( A - 1 ) / 2 ) x. ( ( B - 1 ) / 2 ) ) x. ( ( N - 1 ) / 2 ) ) ) )
126 117 119 95 120 125 syl22anc 
 |-  ( ph -> ( -u 1 ^ ( 2 x. ( ( ( ( A - 1 ) / 2 ) x. ( ( B - 1 ) / 2 ) ) x. ( ( N - 1 ) / 2 ) ) ) ) = ( ( -u 1 ^ 2 ) ^ ( ( ( ( A - 1 ) / 2 ) x. ( ( B - 1 ) / 2 ) ) x. ( ( N - 1 ) / 2 ) ) ) )
127 neg1sqe1 
 |-  ( -u 1 ^ 2 ) = 1
128 127 oveq1i 
 |-  ( ( -u 1 ^ 2 ) ^ ( ( ( ( A - 1 ) / 2 ) x. ( ( B - 1 ) / 2 ) ) x. ( ( N - 1 ) / 2 ) ) ) = ( 1 ^ ( ( ( ( A - 1 ) / 2 ) x. ( ( B - 1 ) / 2 ) ) x. ( ( N - 1 ) / 2 ) ) )
129 1exp 
 |-  ( ( ( ( ( A - 1 ) / 2 ) x. ( ( B - 1 ) / 2 ) ) x. ( ( N - 1 ) / 2 ) ) e. ZZ -> ( 1 ^ ( ( ( ( A - 1 ) / 2 ) x. ( ( B - 1 ) / 2 ) ) x. ( ( N - 1 ) / 2 ) ) ) = 1 )
130 120 129 syl 
 |-  ( ph -> ( 1 ^ ( ( ( ( A - 1 ) / 2 ) x. ( ( B - 1 ) / 2 ) ) x. ( ( N - 1 ) / 2 ) ) ) = 1 )
131 128 130 eqtrid 
 |-  ( ph -> ( ( -u 1 ^ 2 ) ^ ( ( ( ( A - 1 ) / 2 ) x. ( ( B - 1 ) / 2 ) ) x. ( ( N - 1 ) / 2 ) ) ) = 1 )
132 126 131 eqtrd 
 |-  ( ph -> ( -u 1 ^ ( 2 x. ( ( ( ( A - 1 ) / 2 ) x. ( ( B - 1 ) / 2 ) ) x. ( ( N - 1 ) / 2 ) ) ) ) = 1 )
133 132 oveq1d 
 |-  ( ph -> ( ( -u 1 ^ ( 2 x. ( ( ( ( A - 1 ) / 2 ) x. ( ( B - 1 ) / 2 ) ) x. ( ( N - 1 ) / 2 ) ) ) ) x. ( -u 1 ^ ( ( ( ( A - 1 ) / 2 ) + ( ( B - 1 ) / 2 ) ) x. ( ( N - 1 ) / 2 ) ) ) ) = ( 1 x. ( -u 1 ^ ( ( ( ( A - 1 ) / 2 ) + ( ( B - 1 ) / 2 ) ) x. ( ( N - 1 ) / 2 ) ) ) ) )
134 124 133 eqtrd 
 |-  ( ph -> ( -u 1 ^ ( ( 2 x. ( ( ( ( A - 1 ) / 2 ) x. ( ( B - 1 ) / 2 ) ) x. ( ( N - 1 ) / 2 ) ) ) + ( ( ( ( A - 1 ) / 2 ) + ( ( B - 1 ) / 2 ) ) x. ( ( N - 1 ) / 2 ) ) ) ) = ( 1 x. ( -u 1 ^ ( ( ( ( A - 1 ) / 2 ) + ( ( B - 1 ) / 2 ) ) x. ( ( N - 1 ) / 2 ) ) ) ) )
135 117 119 122 expclzd 
 |-  ( ph -> ( -u 1 ^ ( ( ( ( A - 1 ) / 2 ) + ( ( B - 1 ) / 2 ) ) x. ( ( N - 1 ) / 2 ) ) ) e. CC )
136 135 mulid2d 
 |-  ( ph -> ( 1 x. ( -u 1 ^ ( ( ( ( A - 1 ) / 2 ) + ( ( B - 1 ) / 2 ) ) x. ( ( N - 1 ) / 2 ) ) ) ) = ( -u 1 ^ ( ( ( ( A - 1 ) / 2 ) + ( ( B - 1 ) / 2 ) ) x. ( ( N - 1 ) / 2 ) ) ) )
137 75 88 109 adddird 
 |-  ( ph -> ( ( ( ( A - 1 ) / 2 ) + ( ( B - 1 ) / 2 ) ) x. ( ( N - 1 ) / 2 ) ) = ( ( ( ( A - 1 ) / 2 ) x. ( ( N - 1 ) / 2 ) ) + ( ( ( B - 1 ) / 2 ) x. ( ( N - 1 ) / 2 ) ) ) )
138 137 oveq2d 
 |-  ( ph -> ( -u 1 ^ ( ( ( ( A - 1 ) / 2 ) + ( ( B - 1 ) / 2 ) ) x. ( ( N - 1 ) / 2 ) ) ) = ( -u 1 ^ ( ( ( ( A - 1 ) / 2 ) x. ( ( N - 1 ) / 2 ) ) + ( ( ( B - 1 ) / 2 ) x. ( ( N - 1 ) / 2 ) ) ) ) )
139 136 138 eqtrd 
 |-  ( ph -> ( 1 x. ( -u 1 ^ ( ( ( ( A - 1 ) / 2 ) + ( ( B - 1 ) / 2 ) ) x. ( ( N - 1 ) / 2 ) ) ) ) = ( -u 1 ^ ( ( ( ( A - 1 ) / 2 ) x. ( ( N - 1 ) / 2 ) ) + ( ( ( B - 1 ) / 2 ) x. ( ( N - 1 ) / 2 ) ) ) ) )
140 115 134 139 3eqtrd 
 |-  ( ph -> ( -u 1 ^ ( ( ( M - 1 ) / 2 ) x. ( ( N - 1 ) / 2 ) ) ) = ( -u 1 ^ ( ( ( ( A - 1 ) / 2 ) x. ( ( N - 1 ) / 2 ) ) + ( ( ( B - 1 ) / 2 ) x. ( ( N - 1 ) / 2 ) ) ) ) )
141 9 10 oveq12d 
 |-  ( ph -> ( ( ( A /L N ) x. ( N /L A ) ) x. ( ( B /L N ) x. ( N /L B ) ) ) = ( ( -u 1 ^ ( ( ( A - 1 ) / 2 ) x. ( ( N - 1 ) / 2 ) ) ) x. ( -u 1 ^ ( ( ( B - 1 ) / 2 ) x. ( ( N - 1 ) / 2 ) ) ) ) )
142 74 108 zmulcld 
 |-  ( ph -> ( ( ( A - 1 ) / 2 ) x. ( ( N - 1 ) / 2 ) ) e. ZZ )
143 87 108 zmulcld 
 |-  ( ph -> ( ( ( B - 1 ) / 2 ) x. ( ( N - 1 ) / 2 ) ) e. ZZ )
144 expaddz 
 |-  ( ( ( -u 1 e. CC /\ -u 1 =/= 0 ) /\ ( ( ( ( A - 1 ) / 2 ) x. ( ( N - 1 ) / 2 ) ) e. ZZ /\ ( ( ( B - 1 ) / 2 ) x. ( ( N - 1 ) / 2 ) ) e. ZZ ) ) -> ( -u 1 ^ ( ( ( ( A - 1 ) / 2 ) x. ( ( N - 1 ) / 2 ) ) + ( ( ( B - 1 ) / 2 ) x. ( ( N - 1 ) / 2 ) ) ) ) = ( ( -u 1 ^ ( ( ( A - 1 ) / 2 ) x. ( ( N - 1 ) / 2 ) ) ) x. ( -u 1 ^ ( ( ( B - 1 ) / 2 ) x. ( ( N - 1 ) / 2 ) ) ) ) )
145 117 119 142 143 144 syl22anc 
 |-  ( ph -> ( -u 1 ^ ( ( ( ( A - 1 ) / 2 ) x. ( ( N - 1 ) / 2 ) ) + ( ( ( B - 1 ) / 2 ) x. ( ( N - 1 ) / 2 ) ) ) ) = ( ( -u 1 ^ ( ( ( A - 1 ) / 2 ) x. ( ( N - 1 ) / 2 ) ) ) x. ( -u 1 ^ ( ( ( B - 1 ) / 2 ) x. ( ( N - 1 ) / 2 ) ) ) ) )
146 141 145 eqtr4d 
 |-  ( ph -> ( ( ( A /L N ) x. ( N /L A ) ) x. ( ( B /L N ) x. ( N /L B ) ) ) = ( -u 1 ^ ( ( ( ( A - 1 ) / 2 ) x. ( ( N - 1 ) / 2 ) ) + ( ( ( B - 1 ) / 2 ) x. ( ( N - 1 ) / 2 ) ) ) ) )
147 lgscl 
 |-  ( ( A e. ZZ /\ N e. ZZ ) -> ( A /L N ) e. ZZ )
148 11 101 147 syl2anc 
 |-  ( ph -> ( A /L N ) e. ZZ )
149 148 zcnd 
 |-  ( ph -> ( A /L N ) e. CC )
150 lgscl 
 |-  ( ( B e. ZZ /\ N e. ZZ ) -> ( B /L N ) e. ZZ )
151 16 101 150 syl2anc 
 |-  ( ph -> ( B /L N ) e. ZZ )
152 151 zcnd 
 |-  ( ph -> ( B /L N ) e. CC )
153 lgscl 
 |-  ( ( N e. ZZ /\ A e. ZZ ) -> ( N /L A ) e. ZZ )
154 101 11 153 syl2anc 
 |-  ( ph -> ( N /L A ) e. ZZ )
155 154 zcnd 
 |-  ( ph -> ( N /L A ) e. CC )
156 lgscl 
 |-  ( ( N e. ZZ /\ B e. ZZ ) -> ( N /L B ) e. ZZ )
157 101 16 156 syl2anc 
 |-  ( ph -> ( N /L B ) e. ZZ )
158 157 zcnd 
 |-  ( ph -> ( N /L B ) e. CC )
159 149 152 155 158 mul4d 
 |-  ( ph -> ( ( ( A /L N ) x. ( B /L N ) ) x. ( ( N /L A ) x. ( N /L B ) ) ) = ( ( ( A /L N ) x. ( N /L A ) ) x. ( ( B /L N ) x. ( N /L B ) ) ) )
160 6 nnne0d 
 |-  ( ph -> A =/= 0 )
161 7 nnne0d 
 |-  ( ph -> B =/= 0 )
162 lgsdir 
 |-  ( ( ( A e. ZZ /\ B e. ZZ /\ N e. ZZ ) /\ ( A =/= 0 /\ B =/= 0 ) ) -> ( ( A x. B ) /L N ) = ( ( A /L N ) x. ( B /L N ) ) )
163 11 16 101 160 161 162 syl32anc 
 |-  ( ph -> ( ( A x. B ) /L N ) = ( ( A /L N ) x. ( B /L N ) ) )
164 8 oveq1d 
 |-  ( ph -> ( ( A x. B ) /L N ) = ( M /L N ) )
165 163 164 eqtr3d 
 |-  ( ph -> ( ( A /L N ) x. ( B /L N ) ) = ( M /L N ) )
166 lgsdi 
 |-  ( ( ( N e. ZZ /\ A e. ZZ /\ B e. ZZ ) /\ ( A =/= 0 /\ B =/= 0 ) ) -> ( N /L ( A x. B ) ) = ( ( N /L A ) x. ( N /L B ) ) )
167 101 11 16 160 161 166 syl32anc 
 |-  ( ph -> ( N /L ( A x. B ) ) = ( ( N /L A ) x. ( N /L B ) ) )
168 8 oveq2d 
 |-  ( ph -> ( N /L ( A x. B ) ) = ( N /L M ) )
169 167 168 eqtr3d 
 |-  ( ph -> ( ( N /L A ) x. ( N /L B ) ) = ( N /L M ) )
170 165 169 oveq12d 
 |-  ( ph -> ( ( ( A /L N ) x. ( B /L N ) ) x. ( ( N /L A ) x. ( N /L B ) ) ) = ( ( M /L N ) x. ( N /L M ) ) )
171 159 170 eqtr3d 
 |-  ( ph -> ( ( ( A /L N ) x. ( N /L A ) ) x. ( ( B /L N ) x. ( N /L B ) ) ) = ( ( M /L N ) x. ( N /L M ) ) )
172 140 146 171 3eqtr2rd 
 |-  ( ph -> ( ( M /L N ) x. ( N /L M ) ) = ( -u 1 ^ ( ( ( M - 1 ) / 2 ) x. ( ( N - 1 ) / 2 ) ) ) )