Metamath Proof Explorer


Theorem lgsquad2lem2

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

Ref Expression
Hypotheses lgsquad2.1 ( 𝜑𝑀 ∈ ℕ )
lgsquad2.2 ( 𝜑 → ¬ 2 ∥ 𝑀 )
lgsquad2.3 ( 𝜑𝑁 ∈ ℕ )
lgsquad2.4 ( 𝜑 → ¬ 2 ∥ 𝑁 )
lgsquad2.5 ( 𝜑 → ( 𝑀 gcd 𝑁 ) = 1 )
lgsquad2lem2.f ( ( 𝜑 ∧ ( 𝑚 ∈ ( ℙ ∖ { 2 } ) ∧ ( 𝑚 gcd 𝑁 ) = 1 ) ) → ( ( 𝑚 /L 𝑁 ) · ( 𝑁 /L 𝑚 ) ) = ( - 1 ↑ ( ( ( 𝑚 − 1 ) / 2 ) · ( ( 𝑁 − 1 ) / 2 ) ) ) )
lgsquad2lem2.s ( 𝜓 ↔ ∀ 𝑥 ∈ ( 1 ... 𝑘 ) ( ( 𝑥 gcd ( 2 · 𝑁 ) ) = 1 → ( ( 𝑥 /L 𝑁 ) · ( 𝑁 /L 𝑥 ) ) = ( - 1 ↑ ( ( ( 𝑥 − 1 ) / 2 ) · ( ( 𝑁 − 1 ) / 2 ) ) ) ) )
Assertion lgsquad2lem2 ( 𝜑 → ( ( 𝑀 /L 𝑁 ) · ( 𝑁 /L 𝑀 ) ) = ( - 1 ↑ ( ( ( 𝑀 − 1 ) / 2 ) · ( ( 𝑁 − 1 ) / 2 ) ) ) )

Proof

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