Metamath Proof Explorer

Theorem lgsquad2lem2

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 )
lgsquad2lem2.f 
|- ( ( ph /\ ( m e. ( Prime \ { 2 } ) /\ ( m gcd N ) = 1 ) ) -> ( ( m /L N ) x. ( N /L m ) ) = ( -u 1 ^ ( ( ( m - 1 ) / 2 ) x. ( ( N - 1 ) / 2 ) ) ) )
lgsquad2lem2.s 
|- ( ps <-> A. x e. ( 1 ... k ) ( ( x gcd ( 2 x. N ) ) = 1 -> ( ( x /L N ) x. ( N /L x ) ) = ( -u 1 ^ ( ( ( x - 1 ) / 2 ) x. ( ( N - 1 ) / 2 ) ) ) ) )
Assertion lgsquad2lem2 
|- ( 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 lgsquad2lem2.f 
 |-  ( ( ph /\ ( m e. ( Prime \ { 2 } ) /\ ( m gcd N ) = 1 ) ) -> ( ( m /L N ) x. ( N /L m ) ) = ( -u 1 ^ ( ( ( m - 1 ) / 2 ) x. ( ( N - 1 ) / 2 ) ) ) )
7 lgsquad2lem2.s 
 |-  ( ps <-> A. x e. ( 1 ... k ) ( ( x gcd ( 2 x. N ) ) = 1 -> ( ( x /L N ) x. ( N /L x ) ) = ( -u 1 ^ ( ( ( x - 1 ) / 2 ) x. ( ( N - 1 ) / 2 ) ) ) ) )
8 2nn 
 |-  2 e. NN
9 8 a1i 
 |-  ( ph -> 2 e. NN )
10 1 nnzd 
 |-  ( ph -> M e. ZZ )
11 2z 
 |-  2 e. ZZ
12 gcdcom 
 |-  ( ( M e. ZZ /\ 2 e. ZZ ) -> ( M gcd 2 ) = ( 2 gcd M ) )
13 10 11 12 sylancl 
 |-  ( ph -> ( M gcd 2 ) = ( 2 gcd M ) )
14 2prm 
 |-  2 e. Prime
15 coprm 
 |-  ( ( 2 e. Prime /\ M e. ZZ ) -> ( -. 2 || M <-> ( 2 gcd M ) = 1 ) )
16 14 10 15 sylancr 
 |-  ( ph -> ( -. 2 || M <-> ( 2 gcd M ) = 1 ) )
17 2 16 mpbid 
 |-  ( ph -> ( 2 gcd M ) = 1 )
18 13 17 eqtrd 
 |-  ( ph -> ( M gcd 2 ) = 1 )
19 rpmulgcd 
 |-  ( ( ( M e. NN /\ 2 e. NN /\ N e. NN ) /\ ( M gcd 2 ) = 1 ) -> ( M gcd ( 2 x. N ) ) = ( M gcd N ) )
20 1 9 3 18 19 syl31anc 
 |-  ( ph -> ( M gcd ( 2 x. N ) ) = ( M gcd N ) )
21 20 5 eqtrd 
 |-  ( ph -> ( M gcd ( 2 x. N ) ) = 1 )
22 oveq1 
 |-  ( m = 1 -> ( m /L N ) = ( 1 /L N ) )
23 oveq2 
 |-  ( m = 1 -> ( N /L m ) = ( N /L 1 ) )
24 22 23 oveq12d 
 |-  ( m = 1 -> ( ( m /L N ) x. ( N /L m ) ) = ( ( 1 /L N ) x. ( N /L 1 ) ) )
25 oveq1 
 |-  ( m = 1 -> ( m - 1 ) = ( 1 - 1 ) )
26 1m1e0 
 |-  ( 1 - 1 ) = 0
27 25 26 eqtrdi 
 |-  ( m = 1 -> ( m - 1 ) = 0 )
28 27 oveq1d 
 |-  ( m = 1 -> ( ( m - 1 ) / 2 ) = ( 0 / 2 ) )
29 2cn 
 |-  2 e. CC
30 2ne0 
 |-  2 =/= 0
31 29 30 div0i 
 |-  ( 0 / 2 ) = 0
32 28 31 eqtrdi 
 |-  ( m = 1 -> ( ( m - 1 ) / 2 ) = 0 )
33 32 oveq1d 
 |-  ( m = 1 -> ( ( ( m - 1 ) / 2 ) x. ( ( N - 1 ) / 2 ) ) = ( 0 x. ( ( N - 1 ) / 2 ) ) )
34 33 oveq2d 
 |-  ( m = 1 -> ( -u 1 ^ ( ( ( m - 1 ) / 2 ) x. ( ( N - 1 ) / 2 ) ) ) = ( -u 1 ^ ( 0 x. ( ( N - 1 ) / 2 ) ) ) )
35 24 34 eqeq12d 
 |-  ( m = 1 -> ( ( ( m /L N ) x. ( N /L m ) ) = ( -u 1 ^ ( ( ( m - 1 ) / 2 ) x. ( ( N - 1 ) / 2 ) ) ) <-> ( ( 1 /L N ) x. ( N /L 1 ) ) = ( -u 1 ^ ( 0 x. ( ( N - 1 ) / 2 ) ) ) ) )
36 35 imbi2d 
 |-  ( m = 1 -> ( ( ( m gcd ( 2 x. N ) ) = 1 -> ( ( m /L N ) x. ( N /L m ) ) = ( -u 1 ^ ( ( ( m - 1 ) / 2 ) x. ( ( N - 1 ) / 2 ) ) ) ) <-> ( ( m gcd ( 2 x. N ) ) = 1 -> ( ( 1 /L N ) x. ( N /L 1 ) ) = ( -u 1 ^ ( 0 x. ( ( N - 1 ) / 2 ) ) ) ) ) )
37 36 imbi2d 
 |-  ( m = 1 -> ( ( ph -> ( ( m gcd ( 2 x. N ) ) = 1 -> ( ( m /L N ) x. ( N /L m ) ) = ( -u 1 ^ ( ( ( m - 1 ) / 2 ) x. ( ( N - 1 ) / 2 ) ) ) ) ) <-> ( ph -> ( ( m gcd ( 2 x. N ) ) = 1 -> ( ( 1 /L N ) x. ( N /L 1 ) ) = ( -u 1 ^ ( 0 x. ( ( N - 1 ) / 2 ) ) ) ) ) ) )
38 oveq1 
 |-  ( m = x -> ( m gcd ( 2 x. N ) ) = ( x gcd ( 2 x. N ) ) )
39 38 eqeq1d 
 |-  ( m = x -> ( ( m gcd ( 2 x. N ) ) = 1 <-> ( x gcd ( 2 x. N ) ) = 1 ) )
40 oveq1 
 |-  ( m = x -> ( m /L N ) = ( x /L N ) )
41 oveq2 
 |-  ( m = x -> ( N /L m ) = ( N /L x ) )
42 40 41 oveq12d 
 |-  ( m = x -> ( ( m /L N ) x. ( N /L m ) ) = ( ( x /L N ) x. ( N /L x ) ) )
43 oveq1 
 |-  ( m = x -> ( m - 1 ) = ( x - 1 ) )
44 43 oveq1d 
 |-  ( m = x -> ( ( m - 1 ) / 2 ) = ( ( x - 1 ) / 2 ) )
45 44 oveq1d 
 |-  ( m = x -> ( ( ( m - 1 ) / 2 ) x. ( ( N - 1 ) / 2 ) ) = ( ( ( x - 1 ) / 2 ) x. ( ( N - 1 ) / 2 ) ) )
46 45 oveq2d 
 |-  ( m = x -> ( -u 1 ^ ( ( ( m - 1 ) / 2 ) x. ( ( N - 1 ) / 2 ) ) ) = ( -u 1 ^ ( ( ( x - 1 ) / 2 ) x. ( ( N - 1 ) / 2 ) ) ) )
47 42 46 eqeq12d 
 |-  ( m = x -> ( ( ( m /L N ) x. ( N /L m ) ) = ( -u 1 ^ ( ( ( m - 1 ) / 2 ) x. ( ( N - 1 ) / 2 ) ) ) <-> ( ( x /L N ) x. ( N /L x ) ) = ( -u 1 ^ ( ( ( x - 1 ) / 2 ) x. ( ( N - 1 ) / 2 ) ) ) ) )
48 39 47 imbi12d 
 |-  ( m = x -> ( ( ( m gcd ( 2 x. N ) ) = 1 -> ( ( m /L N ) x. ( N /L m ) ) = ( -u 1 ^ ( ( ( m - 1 ) / 2 ) x. ( ( N - 1 ) / 2 ) ) ) ) <-> ( ( x gcd ( 2 x. N ) ) = 1 -> ( ( x /L N ) x. ( N /L x ) ) = ( -u 1 ^ ( ( ( x - 1 ) / 2 ) x. ( ( N - 1 ) / 2 ) ) ) ) ) )
49 48 imbi2d 
 |-  ( m = x -> ( ( ph -> ( ( m gcd ( 2 x. N ) ) = 1 -> ( ( m /L N ) x. ( N /L m ) ) = ( -u 1 ^ ( ( ( m - 1 ) / 2 ) x. ( ( N - 1 ) / 2 ) ) ) ) ) <-> ( ph -> ( ( x gcd ( 2 x. N ) ) = 1 -> ( ( x /L N ) x. ( N /L x ) ) = ( -u 1 ^ ( ( ( x - 1 ) / 2 ) x. ( ( N - 1 ) / 2 ) ) ) ) ) ) )
50 oveq1 
 |-  ( m = y -> ( m gcd ( 2 x. N ) ) = ( y gcd ( 2 x. N ) ) )
51 50 eqeq1d 
 |-  ( m = y -> ( ( m gcd ( 2 x. N ) ) = 1 <-> ( y gcd ( 2 x. N ) ) = 1 ) )
52 oveq1 
 |-  ( m = y -> ( m /L N ) = ( y /L N ) )
53 oveq2 
 |-  ( m = y -> ( N /L m ) = ( N /L y ) )
54 52 53 oveq12d 
 |-  ( m = y -> ( ( m /L N ) x. ( N /L m ) ) = ( ( y /L N ) x. ( N /L y ) ) )
55 oveq1 
 |-  ( m = y -> ( m - 1 ) = ( y - 1 ) )
56 55 oveq1d 
 |-  ( m = y -> ( ( m - 1 ) / 2 ) = ( ( y - 1 ) / 2 ) )
57 56 oveq1d 
 |-  ( m = y -> ( ( ( m - 1 ) / 2 ) x. ( ( N - 1 ) / 2 ) ) = ( ( ( y - 1 ) / 2 ) x. ( ( N - 1 ) / 2 ) ) )
58 57 oveq2d 
 |-  ( m = y -> ( -u 1 ^ ( ( ( m - 1 ) / 2 ) x. ( ( N - 1 ) / 2 ) ) ) = ( -u 1 ^ ( ( ( y - 1 ) / 2 ) x. ( ( N - 1 ) / 2 ) ) ) )
59 54 58 eqeq12d 
 |-  ( m = y -> ( ( ( m /L N ) x. ( N /L m ) ) = ( -u 1 ^ ( ( ( m - 1 ) / 2 ) x. ( ( N - 1 ) / 2 ) ) ) <-> ( ( y /L N ) x. ( N /L y ) ) = ( -u 1 ^ ( ( ( y - 1 ) / 2 ) x. ( ( N - 1 ) / 2 ) ) ) ) )
60 51 59 imbi12d 
 |-  ( m = y -> ( ( ( m gcd ( 2 x. N ) ) = 1 -> ( ( m /L N ) x. ( N /L m ) ) = ( -u 1 ^ ( ( ( m - 1 ) / 2 ) x. ( ( N - 1 ) / 2 ) ) ) ) <-> ( ( y gcd ( 2 x. N ) ) = 1 -> ( ( y /L N ) x. ( N /L y ) ) = ( -u 1 ^ ( ( ( y - 1 ) / 2 ) x. ( ( N - 1 ) / 2 ) ) ) ) ) )
61 60 imbi2d 
 |-  ( m = y -> ( ( ph -> ( ( m gcd ( 2 x. N ) ) = 1 -> ( ( m /L N ) x. ( N /L m ) ) = ( -u 1 ^ ( ( ( m - 1 ) / 2 ) x. ( ( N - 1 ) / 2 ) ) ) ) ) <-> ( ph -> ( ( y gcd ( 2 x. N ) ) = 1 -> ( ( y /L N ) x. ( N /L y ) ) = ( -u 1 ^ ( ( ( y - 1 ) / 2 ) x. ( ( N - 1 ) / 2 ) ) ) ) ) ) )
62 oveq1 
 |-  ( m = ( x x. y ) -> ( m gcd ( 2 x. N ) ) = ( ( x x. y ) gcd ( 2 x. N ) ) )
63 62 eqeq1d 
 |-  ( m = ( x x. y ) -> ( ( m gcd ( 2 x. N ) ) = 1 <-> ( ( x x. y ) gcd ( 2 x. N ) ) = 1 ) )
64 oveq1 
 |-  ( m = ( x x. y ) -> ( m /L N ) = ( ( x x. y ) /L N ) )
65 oveq2 
 |-  ( m = ( x x. y ) -> ( N /L m ) = ( N /L ( x x. y ) ) )
66 64 65 oveq12d 
 |-  ( m = ( x x. y ) -> ( ( m /L N ) x. ( N /L m ) ) = ( ( ( x x. y ) /L N ) x. ( N /L ( x x. y ) ) ) )
67 oveq1 
 |-  ( m = ( x x. y ) -> ( m - 1 ) = ( ( x x. y ) - 1 ) )
68 67 oveq1d 
 |-  ( m = ( x x. y ) -> ( ( m - 1 ) / 2 ) = ( ( ( x x. y ) - 1 ) / 2 ) )
69 68 oveq1d 
 |-  ( m = ( x x. y ) -> ( ( ( m - 1 ) / 2 ) x. ( ( N - 1 ) / 2 ) ) = ( ( ( ( x x. y ) - 1 ) / 2 ) x. ( ( N - 1 ) / 2 ) ) )
70 69 oveq2d 
 |-  ( m = ( x x. y ) -> ( -u 1 ^ ( ( ( m - 1 ) / 2 ) x. ( ( N - 1 ) / 2 ) ) ) = ( -u 1 ^ ( ( ( ( x x. y ) - 1 ) / 2 ) x. ( ( N - 1 ) / 2 ) ) ) )
71 66 70 eqeq12d 
 |-  ( m = ( x x. y ) -> ( ( ( m /L N ) x. ( N /L m ) ) = ( -u 1 ^ ( ( ( m - 1 ) / 2 ) x. ( ( N - 1 ) / 2 ) ) ) <-> ( ( ( x x. y ) /L N ) x. ( N /L ( x x. y ) ) ) = ( -u 1 ^ ( ( ( ( x x. y ) - 1 ) / 2 ) x. ( ( N - 1 ) / 2 ) ) ) ) )
72 63 71 imbi12d 
 |-  ( m = ( x x. y ) -> ( ( ( m gcd ( 2 x. N ) ) = 1 -> ( ( m /L N ) x. ( N /L m ) ) = ( -u 1 ^ ( ( ( m - 1 ) / 2 ) x. ( ( N - 1 ) / 2 ) ) ) ) <-> ( ( ( x x. y ) gcd ( 2 x. N ) ) = 1 -> ( ( ( x x. y ) /L N ) x. ( N /L ( x x. y ) ) ) = ( -u 1 ^ ( ( ( ( x x. y ) - 1 ) / 2 ) x. ( ( N - 1 ) / 2 ) ) ) ) ) )
73 72 imbi2d 
 |-  ( m = ( x x. y ) -> ( ( ph -> ( ( m gcd ( 2 x. N ) ) = 1 -> ( ( m /L N ) x. ( N /L m ) ) = ( -u 1 ^ ( ( ( m - 1 ) / 2 ) x. ( ( N - 1 ) / 2 ) ) ) ) ) <-> ( ph -> ( ( ( x x. y ) gcd ( 2 x. N ) ) = 1 -> ( ( ( x x. y ) /L N ) x. ( N /L ( x x. y ) ) ) = ( -u 1 ^ ( ( ( ( x x. y ) - 1 ) / 2 ) x. ( ( N - 1 ) / 2 ) ) ) ) ) ) )
74 oveq1 
 |-  ( m = M -> ( m gcd ( 2 x. N ) ) = ( M gcd ( 2 x. N ) ) )
75 74 eqeq1d 
 |-  ( m = M -> ( ( m gcd ( 2 x. N ) ) = 1 <-> ( M gcd ( 2 x. N ) ) = 1 ) )
76 oveq1 
 |-  ( m = M -> ( m /L N ) = ( M /L N ) )
77 oveq2 
 |-  ( m = M -> ( N /L m ) = ( N /L M ) )
78 76 77 oveq12d 
 |-  ( m = M -> ( ( m /L N ) x. ( N /L m ) ) = ( ( M /L N ) x. ( N /L M ) ) )
79 oveq1 
 |-  ( m = M -> ( m - 1 ) = ( M - 1 ) )
80 79 oveq1d 
 |-  ( m = M -> ( ( m - 1 ) / 2 ) = ( ( M - 1 ) / 2 ) )
81 80 oveq1d 
 |-  ( m = M -> ( ( ( m - 1 ) / 2 ) x. ( ( N - 1 ) / 2 ) ) = ( ( ( M - 1 ) / 2 ) x. ( ( N - 1 ) / 2 ) ) )
82 81 oveq2d 
 |-  ( m = M -> ( -u 1 ^ ( ( ( m - 1 ) / 2 ) x. ( ( N - 1 ) / 2 ) ) ) = ( -u 1 ^ ( ( ( M - 1 ) / 2 ) x. ( ( N - 1 ) / 2 ) ) ) )
83 78 82 eqeq12d 
 |-  ( m = M -> ( ( ( m /L N ) x. ( N /L m ) ) = ( -u 1 ^ ( ( ( m - 1 ) / 2 ) x. ( ( N - 1 ) / 2 ) ) ) <-> ( ( M /L N ) x. ( N /L M ) ) = ( -u 1 ^ ( ( ( M - 1 ) / 2 ) x. ( ( N - 1 ) / 2 ) ) ) ) )
84 75 83 imbi12d 
 |-  ( m = M -> ( ( ( m gcd ( 2 x. N ) ) = 1 -> ( ( m /L N ) x. ( N /L m ) ) = ( -u 1 ^ ( ( ( m - 1 ) / 2 ) x. ( ( N - 1 ) / 2 ) ) ) ) <-> ( ( M gcd ( 2 x. N ) ) = 1 -> ( ( M /L N ) x. ( N /L M ) ) = ( -u 1 ^ ( ( ( M - 1 ) / 2 ) x. ( ( N - 1 ) / 2 ) ) ) ) ) )
85 84 imbi2d 
 |-  ( m = M -> ( ( ph -> ( ( m gcd ( 2 x. N ) ) = 1 -> ( ( m /L N ) x. ( N /L m ) ) = ( -u 1 ^ ( ( ( m - 1 ) / 2 ) x. ( ( N - 1 ) / 2 ) ) ) ) ) <-> ( ph -> ( ( M gcd ( 2 x. N ) ) = 1 -> ( ( M /L N ) x. ( N /L M ) ) = ( -u 1 ^ ( ( ( M - 1 ) / 2 ) x. ( ( N - 1 ) / 2 ) ) ) ) ) ) )
86 1t1e1 
 |-  ( 1 x. 1 ) = 1
87 neg1cn 
 |-  -u 1 e. CC
88 exp0 
 |-  ( -u 1 e. CC -> ( -u 1 ^ 0 ) = 1 )
89 87 88 ax-mp 
 |-  ( -u 1 ^ 0 ) = 1
90 86 89 eqtr4i 
 |-  ( 1 x. 1 ) = ( -u 1 ^ 0 )
91 sq1 
 |-  ( 1 ^ 2 ) = 1
92 91 oveq1i 
 |-  ( ( 1 ^ 2 ) /L N ) = ( 1 /L N )
93 1z 
 |-  1 e. ZZ
94 ax-1ne0 
 |-  1 =/= 0
95 93 94 pm3.2i 
 |-  ( 1 e. ZZ /\ 1 =/= 0 )
96 3 nnzd 
 |-  ( ph -> N e. ZZ )
97 1gcd 
 |-  ( N e. ZZ -> ( 1 gcd N ) = 1 )
98 96 97 syl 
 |-  ( ph -> ( 1 gcd N ) = 1 )
99 lgssq 
 |-  ( ( ( 1 e. ZZ /\ 1 =/= 0 ) /\ N e. ZZ /\ ( 1 gcd N ) = 1 ) -> ( ( 1 ^ 2 ) /L N ) = 1 )
100 95 96 98 99 mp3an2i 
 |-  ( ph -> ( ( 1 ^ 2 ) /L N ) = 1 )
101 92 100 eqtr3id 
 |-  ( ph -> ( 1 /L N ) = 1 )
102 91 oveq2i 
 |-  ( N /L ( 1 ^ 2 ) ) = ( N /L 1 )
103 1nn 
 |-  1 e. NN
104 103 a1i 
 |-  ( ph -> 1 e. NN )
105 gcd1 
 |-  ( N e. ZZ -> ( N gcd 1 ) = 1 )
106 96 105 syl 
 |-  ( ph -> ( N gcd 1 ) = 1 )
107 lgssq2 
 |-  ( ( N e. ZZ /\ 1 e. NN /\ ( N gcd 1 ) = 1 ) -> ( N /L ( 1 ^ 2 ) ) = 1 )
108 96 104 106 107 syl3anc 
 |-  ( ph -> ( N /L ( 1 ^ 2 ) ) = 1 )
109 102 108 eqtr3id 
 |-  ( ph -> ( N /L 1 ) = 1 )
110 101 109 oveq12d 
 |-  ( ph -> ( ( 1 /L N ) x. ( N /L 1 ) ) = ( 1 x. 1 ) )
111 nnm1nn0 
 |-  ( N e. NN -> ( N - 1 ) e. NN0 )
112 3 111 syl 
 |-  ( ph -> ( N - 1 ) e. NN0 )
113 112 nn0cnd 
 |-  ( ph -> ( N - 1 ) e. CC )
114 113 halfcld 
 |-  ( ph -> ( ( N - 1 ) / 2 ) e. CC )
115 114 mul02d 
 |-  ( ph -> ( 0 x. ( ( N - 1 ) / 2 ) ) = 0 )
116 115 oveq2d 
 |-  ( ph -> ( -u 1 ^ ( 0 x. ( ( N - 1 ) / 2 ) ) ) = ( -u 1 ^ 0 ) )
117 90 110 116 3eqtr4a 
 |-  ( ph -> ( ( 1 /L N ) x. ( N /L 1 ) ) = ( -u 1 ^ ( 0 x. ( ( N - 1 ) / 2 ) ) ) )
118 117 a1d 
 |-  ( ph -> ( ( m gcd ( 2 x. N ) ) = 1 -> ( ( 1 /L N ) x. ( N /L 1 ) ) = ( -u 1 ^ ( 0 x. ( ( N - 1 ) / 2 ) ) ) ) )
119 simprl 
 |-  ( ( ph /\ ( m e. Prime /\ ( m gcd ( 2 x. N ) ) = 1 ) ) -> m e. Prime )
120 prmz 
 |-  ( m e. Prime -> m e. ZZ )
121 120 ad2antrl 
 |-  ( ( ph /\ ( m e. Prime /\ ( m gcd ( 2 x. N ) ) = 1 ) ) -> m e. ZZ )
122 11 a1i 
 |-  ( ( ph /\ ( m e. Prime /\ ( m gcd ( 2 x. N ) ) = 1 ) ) -> 2 e. ZZ )
123 3 adantr 
 |-  ( ( ph /\ ( m e. Prime /\ ( m gcd ( 2 x. N ) ) = 1 ) ) -> N e. NN )
124 123 nnzd 
 |-  ( ( ph /\ ( m e. Prime /\ ( m gcd ( 2 x. N ) ) = 1 ) ) -> N e. ZZ )
125 zmulcl 
 |-  ( ( 2 e. ZZ /\ N e. ZZ ) -> ( 2 x. N ) e. ZZ )
126 11 124 125 sylancr 
 |-  ( ( ph /\ ( m e. Prime /\ ( m gcd ( 2 x. N ) ) = 1 ) ) -> ( 2 x. N ) e. ZZ )
127 simprr 
 |-  ( ( ph /\ ( m e. Prime /\ ( m gcd ( 2 x. N ) ) = 1 ) ) -> ( m gcd ( 2 x. N ) ) = 1 )
128 dvdsmul1 
 |-  ( ( 2 e. ZZ /\ N e. ZZ ) -> 2 || ( 2 x. N ) )
129 11 124 128 sylancr 
 |-  ( ( ph /\ ( m e. Prime /\ ( m gcd ( 2 x. N ) ) = 1 ) ) -> 2 || ( 2 x. N ) )
130 rpdvds 
 |-  ( ( ( m e. ZZ /\ 2 e. ZZ /\ ( 2 x. N ) e. ZZ ) /\ ( ( m gcd ( 2 x. N ) ) = 1 /\ 2 || ( 2 x. N ) ) ) -> ( m gcd 2 ) = 1 )
131 121 122 126 127 129 130 syl32anc 
 |-  ( ( ph /\ ( m e. Prime /\ ( m gcd ( 2 x. N ) ) = 1 ) ) -> ( m gcd 2 ) = 1 )
132 prmrp 
 |-  ( ( m e. Prime /\ 2 e. Prime ) -> ( ( m gcd 2 ) = 1 <-> m =/= 2 ) )
133 119 14 132 sylancl 
 |-  ( ( ph /\ ( m e. Prime /\ ( m gcd ( 2 x. N ) ) = 1 ) ) -> ( ( m gcd 2 ) = 1 <-> m =/= 2 ) )
134 131 133 mpbid 
 |-  ( ( ph /\ ( m e. Prime /\ ( m gcd ( 2 x. N ) ) = 1 ) ) -> m =/= 2 )
135 eldifsn 
 |-  ( m e. ( Prime \ { 2 } ) <-> ( m e. Prime /\ m =/= 2 ) )
136 119 134 135 sylanbrc 
 |-  ( ( ph /\ ( m e. Prime /\ ( m gcd ( 2 x. N ) ) = 1 ) ) -> m e. ( Prime \ { 2 } ) )
137 prmnn 
 |-  ( m e. Prime -> m e. NN )
138 137 ad2antrl 
 |-  ( ( ph /\ ( m e. Prime /\ ( m gcd ( 2 x. N ) ) = 1 ) ) -> m e. NN )
139 8 a1i 
 |-  ( ( ph /\ ( m e. Prime /\ ( m gcd ( 2 x. N ) ) = 1 ) ) -> 2 e. NN )
140 rpmulgcd 
 |-  ( ( ( m e. NN /\ 2 e. NN /\ N e. NN ) /\ ( m gcd 2 ) = 1 ) -> ( m gcd ( 2 x. N ) ) = ( m gcd N ) )
141 138 139 123 131 140 syl31anc 
 |-  ( ( ph /\ ( m e. Prime /\ ( m gcd ( 2 x. N ) ) = 1 ) ) -> ( m gcd ( 2 x. N ) ) = ( m gcd N ) )
142 141 127 eqtr3d 
 |-  ( ( ph /\ ( m e. Prime /\ ( m gcd ( 2 x. N ) ) = 1 ) ) -> ( m gcd N ) = 1 )
143 136 142 jca 
 |-  ( ( ph /\ ( m e. Prime /\ ( m gcd ( 2 x. N ) ) = 1 ) ) -> ( m e. ( Prime \ { 2 } ) /\ ( m gcd N ) = 1 ) )
144 143 6 syldan 
 |-  ( ( ph /\ ( m e. Prime /\ ( m gcd ( 2 x. N ) ) = 1 ) ) -> ( ( m /L N ) x. ( N /L m ) ) = ( -u 1 ^ ( ( ( m - 1 ) / 2 ) x. ( ( N - 1 ) / 2 ) ) ) )
145 144 exp32 
 |-  ( ph -> ( m e. Prime -> ( ( m gcd ( 2 x. N ) ) = 1 -> ( ( m /L N ) x. ( N /L m ) ) = ( -u 1 ^ ( ( ( m - 1 ) / 2 ) x. ( ( N - 1 ) / 2 ) ) ) ) ) )
146 145 com12 
 |-  ( m e. Prime -> ( ph -> ( ( m gcd ( 2 x. N ) ) = 1 -> ( ( m /L N ) x. ( N /L m ) ) = ( -u 1 ^ ( ( ( m - 1 ) / 2 ) x. ( ( N - 1 ) / 2 ) ) ) ) ) )
147 jcab 
 |-  ( ( ph -> ( ( ( x gcd ( 2 x. N ) ) = 1 -> ( ( x /L N ) x. ( N /L x ) ) = ( -u 1 ^ ( ( ( x - 1 ) / 2 ) x. ( ( N - 1 ) / 2 ) ) ) ) /\ ( ( y gcd ( 2 x. N ) ) = 1 -> ( ( y /L N ) x. ( N /L y ) ) = ( -u 1 ^ ( ( ( y - 1 ) / 2 ) x. ( ( N - 1 ) / 2 ) ) ) ) ) ) <-> ( ( ph -> ( ( x gcd ( 2 x. N ) ) = 1 -> ( ( x /L N ) x. ( N /L x ) ) = ( -u 1 ^ ( ( ( x - 1 ) / 2 ) x. ( ( N - 1 ) / 2 ) ) ) ) ) /\ ( ph -> ( ( y gcd ( 2 x. N ) ) = 1 -> ( ( y /L N ) x. ( N /L y ) ) = ( -u 1 ^ ( ( ( y - 1 ) / 2 ) x. ( ( N - 1 ) / 2 ) ) ) ) ) ) )
148 simplrl 
 |-  ( ( ( ph /\ ( x e. ( ZZ>= ` 2 ) /\ y e. ( ZZ>= ` 2 ) ) ) /\ ( ( ( x x. y ) gcd ( 2 x. N ) ) = 1 /\ ( ( ( x gcd ( 2 x. N ) ) = 1 -> ( ( x /L N ) x. ( N /L x ) ) = ( -u 1 ^ ( ( ( x - 1 ) / 2 ) x. ( ( N - 1 ) / 2 ) ) ) ) /\ ( ( y gcd ( 2 x. N ) ) = 1 -> ( ( y /L N ) x. ( N /L y ) ) = ( -u 1 ^ ( ( ( y - 1 ) / 2 ) x. ( ( N - 1 ) / 2 ) ) ) ) ) ) ) -> x e. ( ZZ>= ` 2 ) )
149 eluz2nn 
 |-  ( x e. ( ZZ>= ` 2 ) -> x e. NN )
150 148 149 syl 
 |-  ( ( ( ph /\ ( x e. ( ZZ>= ` 2 ) /\ y e. ( ZZ>= ` 2 ) ) ) /\ ( ( ( x x. y ) gcd ( 2 x. N ) ) = 1 /\ ( ( ( x gcd ( 2 x. N ) ) = 1 -> ( ( x /L N ) x. ( N /L x ) ) = ( -u 1 ^ ( ( ( x - 1 ) / 2 ) x. ( ( N - 1 ) / 2 ) ) ) ) /\ ( ( y gcd ( 2 x. N ) ) = 1 -> ( ( y /L N ) x. ( N /L y ) ) = ( -u 1 ^ ( ( ( y - 1 ) / 2 ) x. ( ( N - 1 ) / 2 ) ) ) ) ) ) ) -> x e. NN )
151 simplrr 
 |-  ( ( ( ph /\ ( x e. ( ZZ>= ` 2 ) /\ y e. ( ZZ>= ` 2 ) ) ) /\ ( ( ( x x. y ) gcd ( 2 x. N ) ) = 1 /\ ( ( ( x gcd ( 2 x. N ) ) = 1 -> ( ( x /L N ) x. ( N /L x ) ) = ( -u 1 ^ ( ( ( x - 1 ) / 2 ) x. ( ( N - 1 ) / 2 ) ) ) ) /\ ( ( y gcd ( 2 x. N ) ) = 1 -> ( ( y /L N ) x. ( N /L y ) ) = ( -u 1 ^ ( ( ( y - 1 ) / 2 ) x. ( ( N - 1 ) / 2 ) ) ) ) ) ) ) -> y e. ( ZZ>= ` 2 ) )
152 eluz2nn 
 |-  ( y e. ( ZZ>= ` 2 ) -> y e. NN )
153 151 152 syl 
 |-  ( ( ( ph /\ ( x e. ( ZZ>= ` 2 ) /\ y e. ( ZZ>= ` 2 ) ) ) /\ ( ( ( x x. y ) gcd ( 2 x. N ) ) = 1 /\ ( ( ( x gcd ( 2 x. N ) ) = 1 -> ( ( x /L N ) x. ( N /L x ) ) = ( -u 1 ^ ( ( ( x - 1 ) / 2 ) x. ( ( N - 1 ) / 2 ) ) ) ) /\ ( ( y gcd ( 2 x. N ) ) = 1 -> ( ( y /L N ) x. ( N /L y ) ) = ( -u 1 ^ ( ( ( y - 1 ) / 2 ) x. ( ( N - 1 ) / 2 ) ) ) ) ) ) ) -> y e. NN )
154 150 153 nnmulcld 
 |-  ( ( ( ph /\ ( x e. ( ZZ>= ` 2 ) /\ y e. ( ZZ>= ` 2 ) ) ) /\ ( ( ( x x. y ) gcd ( 2 x. N ) ) = 1 /\ ( ( ( x gcd ( 2 x. N ) ) = 1 -> ( ( x /L N ) x. ( N /L x ) ) = ( -u 1 ^ ( ( ( x - 1 ) / 2 ) x. ( ( N - 1 ) / 2 ) ) ) ) /\ ( ( y gcd ( 2 x. N ) ) = 1 -> ( ( y /L N ) x. ( N /L y ) ) = ( -u 1 ^ ( ( ( y - 1 ) / 2 ) x. ( ( N - 1 ) / 2 ) ) ) ) ) ) ) -> ( x x. y ) e. NN )
155 n2dvds1 
 |-  -. 2 || 1
156 96 ad2antrr 
 |-  ( ( ( ph /\ ( x e. ( ZZ>= ` 2 ) /\ y e. ( ZZ>= ` 2 ) ) ) /\ ( ( x x. y ) gcd ( 2 x. N ) ) = 1 ) -> N e. ZZ )
157 11 156 128 sylancr 
 |-  ( ( ( ph /\ ( x e. ( ZZ>= ` 2 ) /\ y e. ( ZZ>= ` 2 ) ) ) /\ ( ( x x. y ) gcd ( 2 x. N ) ) = 1 ) -> 2 || ( 2 x. N ) )
158 eluzelz 
 |-  ( x e. ( ZZ>= ` 2 ) -> x e. ZZ )
159 eluzelz 
 |-  ( y e. ( ZZ>= ` 2 ) -> y e. ZZ )
160 158 159 anim12i 
 |-  ( ( x e. ( ZZ>= ` 2 ) /\ y e. ( ZZ>= ` 2 ) ) -> ( x e. ZZ /\ y e. ZZ ) )
161 160 ad2antlr 
 |-  ( ( ( ph /\ ( x e. ( ZZ>= ` 2 ) /\ y e. ( ZZ>= ` 2 ) ) ) /\ ( ( x x. y ) gcd ( 2 x. N ) ) = 1 ) -> ( x e. ZZ /\ y e. ZZ ) )
162 zmulcl 
 |-  ( ( x e. ZZ /\ y e. ZZ ) -> ( x x. y ) e. ZZ )
163 161 162 syl 
 |-  ( ( ( ph /\ ( x e. ( ZZ>= ` 2 ) /\ y e. ( ZZ>= ` 2 ) ) ) /\ ( ( x x. y ) gcd ( 2 x. N ) ) = 1 ) -> ( x x. y ) e. ZZ )
164 11 156 125 sylancr 
 |-  ( ( ( ph /\ ( x e. ( ZZ>= ` 2 ) /\ y e. ( ZZ>= ` 2 ) ) ) /\ ( ( x x. y ) gcd ( 2 x. N ) ) = 1 ) -> ( 2 x. N ) e. ZZ )
165 dvdsgcd 
 |-  ( ( 2 e. ZZ /\ ( x x. y ) e. ZZ /\ ( 2 x. N ) e. ZZ ) -> ( ( 2 || ( x x. y ) /\ 2 || ( 2 x. N ) ) -> 2 || ( ( x x. y ) gcd ( 2 x. N ) ) ) )
166 11 163 164 165 mp3an2i 
 |-  ( ( ( ph /\ ( x e. ( ZZ>= ` 2 ) /\ y e. ( ZZ>= ` 2 ) ) ) /\ ( ( x x. y ) gcd ( 2 x. N ) ) = 1 ) -> ( ( 2 || ( x x. y ) /\ 2 || ( 2 x. N ) ) -> 2 || ( ( x x. y ) gcd ( 2 x. N ) ) ) )
167 157 166 mpan2d 
 |-  ( ( ( ph /\ ( x e. ( ZZ>= ` 2 ) /\ y e. ( ZZ>= ` 2 ) ) ) /\ ( ( x x. y ) gcd ( 2 x. N ) ) = 1 ) -> ( 2 || ( x x. y ) -> 2 || ( ( x x. y ) gcd ( 2 x. N ) ) ) )
168 simpr 
 |-  ( ( ( ph /\ ( x e. ( ZZ>= ` 2 ) /\ y e. ( ZZ>= ` 2 ) ) ) /\ ( ( x x. y ) gcd ( 2 x. N ) ) = 1 ) -> ( ( x x. y ) gcd ( 2 x. N ) ) = 1 )
169 168 breq2d 
 |-  ( ( ( ph /\ ( x e. ( ZZ>= ` 2 ) /\ y e. ( ZZ>= ` 2 ) ) ) /\ ( ( x x. y ) gcd ( 2 x. N ) ) = 1 ) -> ( 2 || ( ( x x. y ) gcd ( 2 x. N ) ) <-> 2 || 1 ) )
170 167 169 sylibd 
 |-  ( ( ( ph /\ ( x e. ( ZZ>= ` 2 ) /\ y e. ( ZZ>= ` 2 ) ) ) /\ ( ( x x. y ) gcd ( 2 x. N ) ) = 1 ) -> ( 2 || ( x x. y ) -> 2 || 1 ) )
171 155 170 mtoi 
 |-  ( ( ( ph /\ ( x e. ( ZZ>= ` 2 ) /\ y e. ( ZZ>= ` 2 ) ) ) /\ ( ( x x. y ) gcd ( 2 x. N ) ) = 1 ) -> -. 2 || ( x x. y ) )
172 171 adantrr 
 |-  ( ( ( ph /\ ( x e. ( ZZ>= ` 2 ) /\ y e. ( ZZ>= ` 2 ) ) ) /\ ( ( ( x x. y ) gcd ( 2 x. N ) ) = 1 /\ ( ( ( x gcd ( 2 x. N ) ) = 1 -> ( ( x /L N ) x. ( N /L x ) ) = ( -u 1 ^ ( ( ( x - 1 ) / 2 ) x. ( ( N - 1 ) / 2 ) ) ) ) /\ ( ( y gcd ( 2 x. N ) ) = 1 -> ( ( y /L N ) x. ( N /L y ) ) = ( -u 1 ^ ( ( ( y - 1 ) / 2 ) x. ( ( N - 1 ) / 2 ) ) ) ) ) ) ) -> -. 2 || ( x x. y ) )
173 3 ad2antrr 
 |-  ( ( ( ph /\ ( x e. ( ZZ>= ` 2 ) /\ y e. ( ZZ>= ` 2 ) ) ) /\ ( ( ( x x. y ) gcd ( 2 x. N ) ) = 1 /\ ( ( ( x gcd ( 2 x. N ) ) = 1 -> ( ( x /L N ) x. ( N /L x ) ) = ( -u 1 ^ ( ( ( x - 1 ) / 2 ) x. ( ( N - 1 ) / 2 ) ) ) ) /\ ( ( y gcd ( 2 x. N ) ) = 1 -> ( ( y /L N ) x. ( N /L y ) ) = ( -u 1 ^ ( ( ( y - 1 ) / 2 ) x. ( ( N - 1 ) / 2 ) ) ) ) ) ) ) -> N e. NN )
174 4 ad2antrr 
 |-  ( ( ( ph /\ ( x e. ( ZZ>= ` 2 ) /\ y e. ( ZZ>= ` 2 ) ) ) /\ ( ( ( x x. y ) gcd ( 2 x. N ) ) = 1 /\ ( ( ( x gcd ( 2 x. N ) ) = 1 -> ( ( x /L N ) x. ( N /L x ) ) = ( -u 1 ^ ( ( ( x - 1 ) / 2 ) x. ( ( N - 1 ) / 2 ) ) ) ) /\ ( ( y gcd ( 2 x. N ) ) = 1 -> ( ( y /L N ) x. ( N /L y ) ) = ( -u 1 ^ ( ( ( y - 1 ) / 2 ) x. ( ( N - 1 ) / 2 ) ) ) ) ) ) ) -> -. 2 || N )
175 dvdsmul2 
 |-  ( ( 2 e. ZZ /\ N e. ZZ ) -> N || ( 2 x. N ) )
176 11 156 175 sylancr 
 |-  ( ( ( ph /\ ( x e. ( ZZ>= ` 2 ) /\ y e. ( ZZ>= ` 2 ) ) ) /\ ( ( x x. y ) gcd ( 2 x. N ) ) = 1 ) -> N || ( 2 x. N ) )
177 rpdvds 
 |-  ( ( ( ( x x. y ) e. ZZ /\ N e. ZZ /\ ( 2 x. N ) e. ZZ ) /\ ( ( ( x x. y ) gcd ( 2 x. N ) ) = 1 /\ N || ( 2 x. N ) ) ) -> ( ( x x. y ) gcd N ) = 1 )
178 163 156 164 168 176 177 syl32anc 
 |-  ( ( ( ph /\ ( x e. ( ZZ>= ` 2 ) /\ y e. ( ZZ>= ` 2 ) ) ) /\ ( ( x x. y ) gcd ( 2 x. N ) ) = 1 ) -> ( ( x x. y ) gcd N ) = 1 )
179 178 adantrr 
 |-  ( ( ( ph /\ ( x e. ( ZZ>= ` 2 ) /\ y e. ( ZZ>= ` 2 ) ) ) /\ ( ( ( x x. y ) gcd ( 2 x. N ) ) = 1 /\ ( ( ( x gcd ( 2 x. N ) ) = 1 -> ( ( x /L N ) x. ( N /L x ) ) = ( -u 1 ^ ( ( ( x - 1 ) / 2 ) x. ( ( N - 1 ) / 2 ) ) ) ) /\ ( ( y gcd ( 2 x. N ) ) = 1 -> ( ( y /L N ) x. ( N /L y ) ) = ( -u 1 ^ ( ( ( y - 1 ) / 2 ) x. ( ( N - 1 ) / 2 ) ) ) ) ) ) ) -> ( ( x x. y ) gcd N ) = 1 )
180 eqidd 
 |-  ( ( ( ph /\ ( x e. ( ZZ>= ` 2 ) /\ y e. ( ZZ>= ` 2 ) ) ) /\ ( ( ( x x. y ) gcd ( 2 x. N ) ) = 1 /\ ( ( ( x gcd ( 2 x. N ) ) = 1 -> ( ( x /L N ) x. ( N /L x ) ) = ( -u 1 ^ ( ( ( x - 1 ) / 2 ) x. ( ( N - 1 ) / 2 ) ) ) ) /\ ( ( y gcd ( 2 x. N ) ) = 1 -> ( ( y /L N ) x. ( N /L y ) ) = ( -u 1 ^ ( ( ( y - 1 ) / 2 ) x. ( ( N - 1 ) / 2 ) ) ) ) ) ) ) -> ( x x. y ) = ( x x. y ) )
181 161 simpld 
 |-  ( ( ( ph /\ ( x e. ( ZZ>= ` 2 ) /\ y e. ( ZZ>= ` 2 ) ) ) /\ ( ( x x. y ) gcd ( 2 x. N ) ) = 1 ) -> x e. ZZ )
182 181 164 gcdcomd 
 |-  ( ( ( ph /\ ( x e. ( ZZ>= ` 2 ) /\ y e. ( ZZ>= ` 2 ) ) ) /\ ( ( x x. y ) gcd ( 2 x. N ) ) = 1 ) -> ( x gcd ( 2 x. N ) ) = ( ( 2 x. N ) gcd x ) )
183 164 163 gcdcomd 
 |-  ( ( ( ph /\ ( x e. ( ZZ>= ` 2 ) /\ y e. ( ZZ>= ` 2 ) ) ) /\ ( ( x x. y ) gcd ( 2 x. N ) ) = 1 ) -> ( ( 2 x. N ) gcd ( x x. y ) ) = ( ( x x. y ) gcd ( 2 x. N ) ) )
184 183 168 eqtrd 
 |-  ( ( ( ph /\ ( x e. ( ZZ>= ` 2 ) /\ y e. ( ZZ>= ` 2 ) ) ) /\ ( ( x x. y ) gcd ( 2 x. N ) ) = 1 ) -> ( ( 2 x. N ) gcd ( x x. y ) ) = 1 )
185 dvdsmul1 
 |-  ( ( x e. ZZ /\ y e. ZZ ) -> x || ( x x. y ) )
186 161 185 syl 
 |-  ( ( ( ph /\ ( x e. ( ZZ>= ` 2 ) /\ y e. ( ZZ>= ` 2 ) ) ) /\ ( ( x x. y ) gcd ( 2 x. N ) ) = 1 ) -> x || ( x x. y ) )
187 rpdvds 
 |-  ( ( ( ( 2 x. N ) e. ZZ /\ x e. ZZ /\ ( x x. y ) e. ZZ ) /\ ( ( ( 2 x. N ) gcd ( x x. y ) ) = 1 /\ x || ( x x. y ) ) ) -> ( ( 2 x. N ) gcd x ) = 1 )
188 164 181 163 184 186 187 syl32anc 
 |-  ( ( ( ph /\ ( x e. ( ZZ>= ` 2 ) /\ y e. ( ZZ>= ` 2 ) ) ) /\ ( ( x x. y ) gcd ( 2 x. N ) ) = 1 ) -> ( ( 2 x. N ) gcd x ) = 1 )
189 182 188 eqtrd 
 |-  ( ( ( ph /\ ( x e. ( ZZ>= ` 2 ) /\ y e. ( ZZ>= ` 2 ) ) ) /\ ( ( x x. y ) gcd ( 2 x. N ) ) = 1 ) -> ( x gcd ( 2 x. N ) ) = 1 )
190 189 adantrr 
 |-  ( ( ( ph /\ ( x e. ( ZZ>= ` 2 ) /\ y e. ( ZZ>= ` 2 ) ) ) /\ ( ( ( x x. y ) gcd ( 2 x. N ) ) = 1 /\ ( ( ( x gcd ( 2 x. N ) ) = 1 -> ( ( x /L N ) x. ( N /L x ) ) = ( -u 1 ^ ( ( ( x - 1 ) / 2 ) x. ( ( N - 1 ) / 2 ) ) ) ) /\ ( ( y gcd ( 2 x. N ) ) = 1 -> ( ( y /L N ) x. ( N /L y ) ) = ( -u 1 ^ ( ( ( y - 1 ) / 2 ) x. ( ( N - 1 ) / 2 ) ) ) ) ) ) ) -> ( x gcd ( 2 x. N ) ) = 1 )
191 simprrl 
 |-  ( ( ( ph /\ ( x e. ( ZZ>= ` 2 ) /\ y e. ( ZZ>= ` 2 ) ) ) /\ ( ( ( x x. y ) gcd ( 2 x. N ) ) = 1 /\ ( ( ( x gcd ( 2 x. N ) ) = 1 -> ( ( x /L N ) x. ( N /L x ) ) = ( -u 1 ^ ( ( ( x - 1 ) / 2 ) x. ( ( N - 1 ) / 2 ) ) ) ) /\ ( ( y gcd ( 2 x. N ) ) = 1 -> ( ( y /L N ) x. ( N /L y ) ) = ( -u 1 ^ ( ( ( y - 1 ) / 2 ) x. ( ( N - 1 ) / 2 ) ) ) ) ) ) ) -> ( ( x gcd ( 2 x. N ) ) = 1 -> ( ( x /L N ) x. ( N /L x ) ) = ( -u 1 ^ ( ( ( x - 1 ) / 2 ) x. ( ( N - 1 ) / 2 ) ) ) ) )
192 190 191 mpd 
 |-  ( ( ( ph /\ ( x e. ( ZZ>= ` 2 ) /\ y e. ( ZZ>= ` 2 ) ) ) /\ ( ( ( x x. y ) gcd ( 2 x. N ) ) = 1 /\ ( ( ( x gcd ( 2 x. N ) ) = 1 -> ( ( x /L N ) x. ( N /L x ) ) = ( -u 1 ^ ( ( ( x - 1 ) / 2 ) x. ( ( N - 1 ) / 2 ) ) ) ) /\ ( ( y gcd ( 2 x. N ) ) = 1 -> ( ( y /L N ) x. ( N /L y ) ) = ( -u 1 ^ ( ( ( y - 1 ) / 2 ) x. ( ( N - 1 ) / 2 ) ) ) ) ) ) ) -> ( ( x /L N ) x. ( N /L x ) ) = ( -u 1 ^ ( ( ( x - 1 ) / 2 ) x. ( ( N - 1 ) / 2 ) ) ) )
193 161 simprd 
 |-  ( ( ( ph /\ ( x e. ( ZZ>= ` 2 ) /\ y e. ( ZZ>= ` 2 ) ) ) /\ ( ( x x. y ) gcd ( 2 x. N ) ) = 1 ) -> y e. ZZ )
194 193 164 gcdcomd 
 |-  ( ( ( ph /\ ( x e. ( ZZ>= ` 2 ) /\ y e. ( ZZ>= ` 2 ) ) ) /\ ( ( x x. y ) gcd ( 2 x. N ) ) = 1 ) -> ( y gcd ( 2 x. N ) ) = ( ( 2 x. N ) gcd y ) )
195 dvdsmul2 
 |-  ( ( x e. ZZ /\ y e. ZZ ) -> y || ( x x. y ) )
196 161 195 syl 
 |-  ( ( ( ph /\ ( x e. ( ZZ>= ` 2 ) /\ y e. ( ZZ>= ` 2 ) ) ) /\ ( ( x x. y ) gcd ( 2 x. N ) ) = 1 ) -> y || ( x x. y ) )
197 rpdvds 
 |-  ( ( ( ( 2 x. N ) e. ZZ /\ y e. ZZ /\ ( x x. y ) e. ZZ ) /\ ( ( ( 2 x. N ) gcd ( x x. y ) ) = 1 /\ y || ( x x. y ) ) ) -> ( ( 2 x. N ) gcd y ) = 1 )
198 164 193 163 184 196 197 syl32anc 
 |-  ( ( ( ph /\ ( x e. ( ZZ>= ` 2 ) /\ y e. ( ZZ>= ` 2 ) ) ) /\ ( ( x x. y ) gcd ( 2 x. N ) ) = 1 ) -> ( ( 2 x. N ) gcd y ) = 1 )
199 194 198 eqtrd 
 |-  ( ( ( ph /\ ( x e. ( ZZ>= ` 2 ) /\ y e. ( ZZ>= ` 2 ) ) ) /\ ( ( x x. y ) gcd ( 2 x. N ) ) = 1 ) -> ( y gcd ( 2 x. N ) ) = 1 )
200 199 adantrr 
 |-  ( ( ( ph /\ ( x e. ( ZZ>= ` 2 ) /\ y e. ( ZZ>= ` 2 ) ) ) /\ ( ( ( x x. y ) gcd ( 2 x. N ) ) = 1 /\ ( ( ( x gcd ( 2 x. N ) ) = 1 -> ( ( x /L N ) x. ( N /L x ) ) = ( -u 1 ^ ( ( ( x - 1 ) / 2 ) x. ( ( N - 1 ) / 2 ) ) ) ) /\ ( ( y gcd ( 2 x. N ) ) = 1 -> ( ( y /L N ) x. ( N /L y ) ) = ( -u 1 ^ ( ( ( y - 1 ) / 2 ) x. ( ( N - 1 ) / 2 ) ) ) ) ) ) ) -> ( y gcd ( 2 x. N ) ) = 1 )
201 simprrr 
 |-  ( ( ( ph /\ ( x e. ( ZZ>= ` 2 ) /\ y e. ( ZZ>= ` 2 ) ) ) /\ ( ( ( x x. y ) gcd ( 2 x. N ) ) = 1 /\ ( ( ( x gcd ( 2 x. N ) ) = 1 -> ( ( x /L N ) x. ( N /L x ) ) = ( -u 1 ^ ( ( ( x - 1 ) / 2 ) x. ( ( N - 1 ) / 2 ) ) ) ) /\ ( ( y gcd ( 2 x. N ) ) = 1 -> ( ( y /L N ) x. ( N /L y ) ) = ( -u 1 ^ ( ( ( y - 1 ) / 2 ) x. ( ( N - 1 ) / 2 ) ) ) ) ) ) ) -> ( ( y gcd ( 2 x. N ) ) = 1 -> ( ( y /L N ) x. ( N /L y ) ) = ( -u 1 ^ ( ( ( y - 1 ) / 2 ) x. ( ( N - 1 ) / 2 ) ) ) ) )
202 200 201 mpd 
 |-  ( ( ( ph /\ ( x e. ( ZZ>= ` 2 ) /\ y e. ( ZZ>= ` 2 ) ) ) /\ ( ( ( x x. y ) gcd ( 2 x. N ) ) = 1 /\ ( ( ( x gcd ( 2 x. N ) ) = 1 -> ( ( x /L N ) x. ( N /L x ) ) = ( -u 1 ^ ( ( ( x - 1 ) / 2 ) x. ( ( N - 1 ) / 2 ) ) ) ) /\ ( ( y gcd ( 2 x. N ) ) = 1 -> ( ( y /L N ) x. ( N /L y ) ) = ( -u 1 ^ ( ( ( y - 1 ) / 2 ) x. ( ( N - 1 ) / 2 ) ) ) ) ) ) ) -> ( ( y /L N ) x. ( N /L y ) ) = ( -u 1 ^ ( ( ( y - 1 ) / 2 ) x. ( ( N - 1 ) / 2 ) ) ) )
203 154 172 173 174 179 150 153 180 192 202 lgsquad2lem1 
 |-  ( ( ( ph /\ ( x e. ( ZZ>= ` 2 ) /\ y e. ( ZZ>= ` 2 ) ) ) /\ ( ( ( x x. y ) gcd ( 2 x. N ) ) = 1 /\ ( ( ( x gcd ( 2 x. N ) ) = 1 -> ( ( x /L N ) x. ( N /L x ) ) = ( -u 1 ^ ( ( ( x - 1 ) / 2 ) x. ( ( N - 1 ) / 2 ) ) ) ) /\ ( ( y gcd ( 2 x. N ) ) = 1 -> ( ( y /L N ) x. ( N /L y ) ) = ( -u 1 ^ ( ( ( y - 1 ) / 2 ) x. ( ( N - 1 ) / 2 ) ) ) ) ) ) ) -> ( ( ( x x. y ) /L N ) x. ( N /L ( x x. y ) ) ) = ( -u 1 ^ ( ( ( ( x x. y ) - 1 ) / 2 ) x. ( ( N - 1 ) / 2 ) ) ) )
204 203 exp32 
 |-  ( ( ph /\ ( x e. ( ZZ>= ` 2 ) /\ y e. ( ZZ>= ` 2 ) ) ) -> ( ( ( x x. y ) gcd ( 2 x. N ) ) = 1 -> ( ( ( ( x gcd ( 2 x. N ) ) = 1 -> ( ( x /L N ) x. ( N /L x ) ) = ( -u 1 ^ ( ( ( x - 1 ) / 2 ) x. ( ( N - 1 ) / 2 ) ) ) ) /\ ( ( y gcd ( 2 x. N ) ) = 1 -> ( ( y /L N ) x. ( N /L y ) ) = ( -u 1 ^ ( ( ( y - 1 ) / 2 ) x. ( ( N - 1 ) / 2 ) ) ) ) ) -> ( ( ( x x. y ) /L N ) x. ( N /L ( x x. y ) ) ) = ( -u 1 ^ ( ( ( ( x x. y ) - 1 ) / 2 ) x. ( ( N - 1 ) / 2 ) ) ) ) ) )
205 204 com23 
 |-  ( ( ph /\ ( x e. ( ZZ>= ` 2 ) /\ y e. ( ZZ>= ` 2 ) ) ) -> ( ( ( ( x gcd ( 2 x. N ) ) = 1 -> ( ( x /L N ) x. ( N /L x ) ) = ( -u 1 ^ ( ( ( x - 1 ) / 2 ) x. ( ( N - 1 ) / 2 ) ) ) ) /\ ( ( y gcd ( 2 x. N ) ) = 1 -> ( ( y /L N ) x. ( N /L y ) ) = ( -u 1 ^ ( ( ( y - 1 ) / 2 ) x. ( ( N - 1 ) / 2 ) ) ) ) ) -> ( ( ( x x. y ) gcd ( 2 x. N ) ) = 1 -> ( ( ( x x. y ) /L N ) x. ( N /L ( x x. y ) ) ) = ( -u 1 ^ ( ( ( ( x x. y ) - 1 ) / 2 ) x. ( ( N - 1 ) / 2 ) ) ) ) ) )
206 205 expcom 
 |-  ( ( x e. ( ZZ>= ` 2 ) /\ y e. ( ZZ>= ` 2 ) ) -> ( ph -> ( ( ( ( x gcd ( 2 x. N ) ) = 1 -> ( ( x /L N ) x. ( N /L x ) ) = ( -u 1 ^ ( ( ( x - 1 ) / 2 ) x. ( ( N - 1 ) / 2 ) ) ) ) /\ ( ( y gcd ( 2 x. N ) ) = 1 -> ( ( y /L N ) x. ( N /L y ) ) = ( -u 1 ^ ( ( ( y - 1 ) / 2 ) x. ( ( N - 1 ) / 2 ) ) ) ) ) -> ( ( ( x x. y ) gcd ( 2 x. N ) ) = 1 -> ( ( ( x x. y ) /L N ) x. ( N /L ( x x. y ) ) ) = ( -u 1 ^ ( ( ( ( x x. y ) - 1 ) / 2 ) x. ( ( N - 1 ) / 2 ) ) ) ) ) ) )
207 206 a2d 
 |-  ( ( x e. ( ZZ>= ` 2 ) /\ y e. ( ZZ>= ` 2 ) ) -> ( ( ph -> ( ( ( x gcd ( 2 x. N ) ) = 1 -> ( ( x /L N ) x. ( N /L x ) ) = ( -u 1 ^ ( ( ( x - 1 ) / 2 ) x. ( ( N - 1 ) / 2 ) ) ) ) /\ ( ( y gcd ( 2 x. N ) ) = 1 -> ( ( y /L N ) x. ( N /L y ) ) = ( -u 1 ^ ( ( ( y - 1 ) / 2 ) x. ( ( N - 1 ) / 2 ) ) ) ) ) ) -> ( ph -> ( ( ( x x. y ) gcd ( 2 x. N ) ) = 1 -> ( ( ( x x. y ) /L N ) x. ( N /L ( x x. y ) ) ) = ( -u 1 ^ ( ( ( ( x x. y ) - 1 ) / 2 ) x. ( ( N - 1 ) / 2 ) ) ) ) ) ) )
208 147 207 biimtrrid 
 |-  ( ( x e. ( ZZ>= ` 2 ) /\ y e. ( ZZ>= ` 2 ) ) -> ( ( ( ph -> ( ( x gcd ( 2 x. N ) ) = 1 -> ( ( x /L N ) x. ( N /L x ) ) = ( -u 1 ^ ( ( ( x - 1 ) / 2 ) x. ( ( N - 1 ) / 2 ) ) ) ) ) /\ ( ph -> ( ( y gcd ( 2 x. N ) ) = 1 -> ( ( y /L N ) x. ( N /L y ) ) = ( -u 1 ^ ( ( ( y - 1 ) / 2 ) x. ( ( N - 1 ) / 2 ) ) ) ) ) ) -> ( ph -> ( ( ( x x. y ) gcd ( 2 x. N ) ) = 1 -> ( ( ( x x. y ) /L N ) x. ( N /L ( x x. y ) ) ) = ( -u 1 ^ ( ( ( ( x x. y ) - 1 ) / 2 ) x. ( ( N - 1 ) / 2 ) ) ) ) ) ) )
209 37 49 61 73 85 118 146 208 prmind 
 |-  ( M e. NN -> ( ph -> ( ( M gcd ( 2 x. N ) ) = 1 -> ( ( M /L N ) x. ( N /L M ) ) = ( -u 1 ^ ( ( ( M - 1 ) / 2 ) x. ( ( N - 1 ) / 2 ) ) ) ) ) )
210 1 209 mpcom 
 |-  ( ph -> ( ( M gcd ( 2 x. N ) ) = 1 -> ( ( M /L N ) x. ( N /L M ) ) = ( -u 1 ^ ( ( ( M - 1 ) / 2 ) x. ( ( N - 1 ) / 2 ) ) ) ) )
211 21 210 mpd 
 |-  ( ph -> ( ( M /L N ) x. ( N /L M ) ) = ( -u 1 ^ ( ( ( M - 1 ) / 2 ) x. ( ( N - 1 ) / 2 ) ) ) )