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 biimtrrid ⊢ ( ( 𝑥 ∈ ( ℤ≥ ‘ 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 ) ) ) )