Metamath Proof Explorer

Theorem lgsquad3

Description: Extend lgsquad2 to integers which share a factor. (Contributed by Mario Carneiro, 19-Jun-2015)

Ref Expression
Assertion lgsquad3 ( ( ( 𝑀 ∈ ℕ ∧ ¬ 2 ∥ 𝑀 ) ∧ ( 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) ) → ( 𝑀 /L 𝑁 ) = ( ( - 1 ↑ ( ( ( 𝑀 − 1 ) / 2 ) · ( ( 𝑁 − 1 ) / 2 ) ) ) · ( 𝑁 /L 𝑀 ) ) )

Proof

Step Hyp Ref Expression
1 simplrl ⊢ ( ( ( ( 𝑀 ∈ ℕ ∧ ¬ 2 ∥ 𝑀 ) ∧ ( 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) ) ∧ ( 𝑀 gcd 𝑁 ) = 1 ) → 𝑁 ∈ ℕ )
2 nnz ⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℤ )
3 1 2 syl ⊢ ( ( ( ( 𝑀 ∈ ℕ ∧ ¬ 2 ∥ 𝑀 ) ∧ ( 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) ) ∧ ( 𝑀 gcd 𝑁 ) = 1 ) → 𝑁 ∈ ℤ )
4 nnz ⊢ ( 𝑀 ∈ ℕ → 𝑀 ∈ ℤ )
5 4 ad3antrrr ⊢ ( ( ( ( 𝑀 ∈ ℕ ∧ ¬ 2 ∥ 𝑀 ) ∧ ( 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) ) ∧ ( 𝑀 gcd 𝑁 ) = 1 ) → 𝑀 ∈ ℤ )
6 lgscl ⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ ) → ( 𝑁 /L 𝑀 ) ∈ ℤ )
7 3 5 6 syl2anc ⊢ ( ( ( ( 𝑀 ∈ ℕ ∧ ¬ 2 ∥ 𝑀 ) ∧ ( 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) ) ∧ ( 𝑀 gcd 𝑁 ) = 1 ) → ( 𝑁 /L 𝑀 ) ∈ ℤ )
8 7 zred ⊢ ( ( ( ( 𝑀 ∈ ℕ ∧ ¬ 2 ∥ 𝑀 ) ∧ ( 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) ) ∧ ( 𝑀 gcd 𝑁 ) = 1 ) → ( 𝑁 /L 𝑀 ) ∈ ℝ )
9 absresq ⊢ ( ( 𝑁 /L 𝑀 ) ∈ ℝ → ( ( abs ‘ ( 𝑁 /L 𝑀 ) ) ↑ 2 ) = ( ( 𝑁 /L 𝑀 ) ↑ 2 ) )
10 8 9 syl ⊢ ( ( ( ( 𝑀 ∈ ℕ ∧ ¬ 2 ∥ 𝑀 ) ∧ ( 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) ) ∧ ( 𝑀 gcd 𝑁 ) = 1 ) → ( ( abs ‘ ( 𝑁 /L 𝑀 ) ) ↑ 2 ) = ( ( 𝑁 /L 𝑀 ) ↑ 2 ) )
11 3 5 gcdcomd ⊢ ( ( ( ( 𝑀 ∈ ℕ ∧ ¬ 2 ∥ 𝑀 ) ∧ ( 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) ) ∧ ( 𝑀 gcd 𝑁 ) = 1 ) → ( 𝑁 gcd 𝑀 ) = ( 𝑀 gcd 𝑁 ) )
12 simpr ⊢ ( ( ( ( 𝑀 ∈ ℕ ∧ ¬ 2 ∥ 𝑀 ) ∧ ( 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) ) ∧ ( 𝑀 gcd 𝑁 ) = 1 ) → ( 𝑀 gcd 𝑁 ) = 1 )
13 11 12 eqtrd ⊢ ( ( ( ( 𝑀 ∈ ℕ ∧ ¬ 2 ∥ 𝑀 ) ∧ ( 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) ) ∧ ( 𝑀 gcd 𝑁 ) = 1 ) → ( 𝑁 gcd 𝑀 ) = 1 )
14 lgsabs1 ⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ ) → ( ( abs ‘ ( 𝑁 /L 𝑀 ) ) = 1 ↔ ( 𝑁 gcd 𝑀 ) = 1 ) )
15 3 5 14 syl2anc ⊢ ( ( ( ( 𝑀 ∈ ℕ ∧ ¬ 2 ∥ 𝑀 ) ∧ ( 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) ) ∧ ( 𝑀 gcd 𝑁 ) = 1 ) → ( ( abs ‘ ( 𝑁 /L 𝑀 ) ) = 1 ↔ ( 𝑁 gcd 𝑀 ) = 1 ) )
16 13 15 mpbird ⊢ ( ( ( ( 𝑀 ∈ ℕ ∧ ¬ 2 ∥ 𝑀 ) ∧ ( 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) ) ∧ ( 𝑀 gcd 𝑁 ) = 1 ) → ( abs ‘ ( 𝑁 /L 𝑀 ) ) = 1 )
17 16 oveq1d ⊢ ( ( ( ( 𝑀 ∈ ℕ ∧ ¬ 2 ∥ 𝑀 ) ∧ ( 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) ) ∧ ( 𝑀 gcd 𝑁 ) = 1 ) → ( ( abs ‘ ( 𝑁 /L 𝑀 ) ) ↑ 2 ) = ( 1 ↑ 2 ) )
18 sq1 ⊢ ( 1 ↑ 2 ) = 1
19 17 18 eqtrdi ⊢ ( ( ( ( 𝑀 ∈ ℕ ∧ ¬ 2 ∥ 𝑀 ) ∧ ( 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) ) ∧ ( 𝑀 gcd 𝑁 ) = 1 ) → ( ( abs ‘ ( 𝑁 /L 𝑀 ) ) ↑ 2 ) = 1 )
20 7 zcnd ⊢ ( ( ( ( 𝑀 ∈ ℕ ∧ ¬ 2 ∥ 𝑀 ) ∧ ( 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) ) ∧ ( 𝑀 gcd 𝑁 ) = 1 ) → ( 𝑁 /L 𝑀 ) ∈ ℂ )
21 20 sqvald ⊢ ( ( ( ( 𝑀 ∈ ℕ ∧ ¬ 2 ∥ 𝑀 ) ∧ ( 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) ) ∧ ( 𝑀 gcd 𝑁 ) = 1 ) → ( ( 𝑁 /L 𝑀 ) ↑ 2 ) = ( ( 𝑁 /L 𝑀 ) · ( 𝑁 /L 𝑀 ) ) )
22 10 19 21 3eqtr3d ⊢ ( ( ( ( 𝑀 ∈ ℕ ∧ ¬ 2 ∥ 𝑀 ) ∧ ( 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) ) ∧ ( 𝑀 gcd 𝑁 ) = 1 ) → 1 = ( ( 𝑁 /L 𝑀 ) · ( 𝑁 /L 𝑀 ) ) )
23 22 oveq2d ⊢ ( ( ( ( 𝑀 ∈ ℕ ∧ ¬ 2 ∥ 𝑀 ) ∧ ( 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) ) ∧ ( 𝑀 gcd 𝑁 ) = 1 ) → ( ( 𝑀 /L 𝑁 ) · 1 ) = ( ( 𝑀 /L 𝑁 ) · ( ( 𝑁 /L 𝑀 ) · ( 𝑁 /L 𝑀 ) ) ) )
24 lgscl ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑀 /L 𝑁 ) ∈ ℤ )
25 5 3 24 syl2anc ⊢ ( ( ( ( 𝑀 ∈ ℕ ∧ ¬ 2 ∥ 𝑀 ) ∧ ( 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) ) ∧ ( 𝑀 gcd 𝑁 ) = 1 ) → ( 𝑀 /L 𝑁 ) ∈ ℤ )
26 25 zcnd ⊢ ( ( ( ( 𝑀 ∈ ℕ ∧ ¬ 2 ∥ 𝑀 ) ∧ ( 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) ) ∧ ( 𝑀 gcd 𝑁 ) = 1 ) → ( 𝑀 /L 𝑁 ) ∈ ℂ )
27 26 20 20 mulassd ⊢ ( ( ( ( 𝑀 ∈ ℕ ∧ ¬ 2 ∥ 𝑀 ) ∧ ( 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) ) ∧ ( 𝑀 gcd 𝑁 ) = 1 ) → ( ( ( 𝑀 /L 𝑁 ) · ( 𝑁 /L 𝑀 ) ) · ( 𝑁 /L 𝑀 ) ) = ( ( 𝑀 /L 𝑁 ) · ( ( 𝑁 /L 𝑀 ) · ( 𝑁 /L 𝑀 ) ) ) )
28 23 27 eqtr4d ⊢ ( ( ( ( 𝑀 ∈ ℕ ∧ ¬ 2 ∥ 𝑀 ) ∧ ( 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) ) ∧ ( 𝑀 gcd 𝑁 ) = 1 ) → ( ( 𝑀 /L 𝑁 ) · 1 ) = ( ( ( 𝑀 /L 𝑁 ) · ( 𝑁 /L 𝑀 ) ) · ( 𝑁 /L 𝑀 ) ) )
29 26 mulridd ⊢ ( ( ( ( 𝑀 ∈ ℕ ∧ ¬ 2 ∥ 𝑀 ) ∧ ( 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) ) ∧ ( 𝑀 gcd 𝑁 ) = 1 ) → ( ( 𝑀 /L 𝑁 ) · 1 ) = ( 𝑀 /L 𝑁 ) )
30 simplll ⊢ ( ( ( ( 𝑀 ∈ ℕ ∧ ¬ 2 ∥ 𝑀 ) ∧ ( 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) ) ∧ ( 𝑀 gcd 𝑁 ) = 1 ) → 𝑀 ∈ ℕ )
31 simpllr ⊢ ( ( ( ( 𝑀 ∈ ℕ ∧ ¬ 2 ∥ 𝑀 ) ∧ ( 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) ) ∧ ( 𝑀 gcd 𝑁 ) = 1 ) → ¬ 2 ∥ 𝑀 )
32 simplrr ⊢ ( ( ( ( 𝑀 ∈ ℕ ∧ ¬ 2 ∥ 𝑀 ) ∧ ( 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) ) ∧ ( 𝑀 gcd 𝑁 ) = 1 ) → ¬ 2 ∥ 𝑁 )
33 30 31 1 32 12 lgsquad2 ⊢ ( ( ( ( 𝑀 ∈ ℕ ∧ ¬ 2 ∥ 𝑀 ) ∧ ( 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) ) ∧ ( 𝑀 gcd 𝑁 ) = 1 ) → ( ( 𝑀 /L 𝑁 ) · ( 𝑁 /L 𝑀 ) ) = ( - 1 ↑ ( ( ( 𝑀 − 1 ) / 2 ) · ( ( 𝑁 − 1 ) / 2 ) ) ) )
34 33 oveq1d ⊢ ( ( ( ( 𝑀 ∈ ℕ ∧ ¬ 2 ∥ 𝑀 ) ∧ ( 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) ) ∧ ( 𝑀 gcd 𝑁 ) = 1 ) → ( ( ( 𝑀 /L 𝑁 ) · ( 𝑁 /L 𝑀 ) ) · ( 𝑁 /L 𝑀 ) ) = ( ( - 1 ↑ ( ( ( 𝑀 − 1 ) / 2 ) · ( ( 𝑁 − 1 ) / 2 ) ) ) · ( 𝑁 /L 𝑀 ) ) )
35 28 29 34 3eqtr3d ⊢ ( ( ( ( 𝑀 ∈ ℕ ∧ ¬ 2 ∥ 𝑀 ) ∧ ( 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) ) ∧ ( 𝑀 gcd 𝑁 ) = 1 ) → ( 𝑀 /L 𝑁 ) = ( ( - 1 ↑ ( ( ( 𝑀 − 1 ) / 2 ) · ( ( 𝑁 − 1 ) / 2 ) ) ) · ( 𝑁 /L 𝑀 ) ) )
36 neg1cn ⊢ - 1 ∈ ℂ
37 36 a1i ⊢ ( ( ( ( 𝑀 ∈ ℕ ∧ ¬ 2 ∥ 𝑀 ) ∧ ( 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) ) ∧ ¬ ( 𝑀 gcd 𝑁 ) = 1 ) → - 1 ∈ ℂ )
38 neg1ne0 ⊢ - 1 ≠ 0
39 38 a1i ⊢ ( ( ( ( 𝑀 ∈ ℕ ∧ ¬ 2 ∥ 𝑀 ) ∧ ( 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) ) ∧ ¬ ( 𝑀 gcd 𝑁 ) = 1 ) → - 1 ≠ 0 )
40 4 ad3antrrr ⊢ ( ( ( ( 𝑀 ∈ ℕ ∧ ¬ 2 ∥ 𝑀 ) ∧ ( 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) ) ∧ ¬ ( 𝑀 gcd 𝑁 ) = 1 ) → 𝑀 ∈ ℤ )
41 simpllr ⊢ ( ( ( ( 𝑀 ∈ ℕ ∧ ¬ 2 ∥ 𝑀 ) ∧ ( 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) ) ∧ ¬ ( 𝑀 gcd 𝑁 ) = 1 ) → ¬ 2 ∥ 𝑀 )
42 1zzd ⊢ ( ( ( ( 𝑀 ∈ ℕ ∧ ¬ 2 ∥ 𝑀 ) ∧ ( 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) ) ∧ ¬ ( 𝑀 gcd 𝑁 ) = 1 ) → 1 ∈ ℤ )
43 2prm ⊢ 2 ∈ ℙ
44 nprmdvds1 ⊢ ( 2 ∈ ℙ → ¬ 2 ∥ 1 )
45 43 44 mp1i ⊢ ( ( ( ( 𝑀 ∈ ℕ ∧ ¬ 2 ∥ 𝑀 ) ∧ ( 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) ) ∧ ¬ ( 𝑀 gcd 𝑁 ) = 1 ) → ¬ 2 ∥ 1 )
46 omoe ⊢ ( ( ( 𝑀 ∈ ℤ ∧ ¬ 2 ∥ 𝑀 ) ∧ ( 1 ∈ ℤ ∧ ¬ 2 ∥ 1 ) ) → 2 ∥ ( 𝑀 − 1 ) )
47 40 41 42 45 46 syl22anc ⊢ ( ( ( ( 𝑀 ∈ ℕ ∧ ¬ 2 ∥ 𝑀 ) ∧ ( 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) ) ∧ ¬ ( 𝑀 gcd 𝑁 ) = 1 ) → 2 ∥ ( 𝑀 − 1 ) )
48 2z ⊢ 2 ∈ ℤ
49 2ne0 ⊢ 2 ≠ 0
50 peano2zm ⊢ ( 𝑀 ∈ ℤ → ( 𝑀 − 1 ) ∈ ℤ )
51 40 50 syl ⊢ ( ( ( ( 𝑀 ∈ ℕ ∧ ¬ 2 ∥ 𝑀 ) ∧ ( 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) ) ∧ ¬ ( 𝑀 gcd 𝑁 ) = 1 ) → ( 𝑀 − 1 ) ∈ ℤ )
52 dvdsval2 ⊢ ( ( 2 ∈ ℤ ∧ 2 ≠ 0 ∧ ( 𝑀 − 1 ) ∈ ℤ ) → ( 2 ∥ ( 𝑀 − 1 ) ↔ ( ( 𝑀 − 1 ) / 2 ) ∈ ℤ ) )
53 48 49 51 52 mp3an12i ⊢ ( ( ( ( 𝑀 ∈ ℕ ∧ ¬ 2 ∥ 𝑀 ) ∧ ( 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) ) ∧ ¬ ( 𝑀 gcd 𝑁 ) = 1 ) → ( 2 ∥ ( 𝑀 − 1 ) ↔ ( ( 𝑀 − 1 ) / 2 ) ∈ ℤ ) )
54 47 53 mpbid ⊢ ( ( ( ( 𝑀 ∈ ℕ ∧ ¬ 2 ∥ 𝑀 ) ∧ ( 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) ) ∧ ¬ ( 𝑀 gcd 𝑁 ) = 1 ) → ( ( 𝑀 − 1 ) / 2 ) ∈ ℤ )
55 2 adantr ⊢ ( ( 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) → 𝑁 ∈ ℤ )
56 55 ad2antlr ⊢ ( ( ( ( 𝑀 ∈ ℕ ∧ ¬ 2 ∥ 𝑀 ) ∧ ( 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) ) ∧ ¬ ( 𝑀 gcd 𝑁 ) = 1 ) → 𝑁 ∈ ℤ )
57 simplrr ⊢ ( ( ( ( 𝑀 ∈ ℕ ∧ ¬ 2 ∥ 𝑀 ) ∧ ( 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) ) ∧ ¬ ( 𝑀 gcd 𝑁 ) = 1 ) → ¬ 2 ∥ 𝑁 )
58 omoe ⊢ ( ( ( 𝑁 ∈ ℤ ∧ ¬ 2 ∥ 𝑁 ) ∧ ( 1 ∈ ℤ ∧ ¬ 2 ∥ 1 ) ) → 2 ∥ ( 𝑁 − 1 ) )
59 56 57 42 45 58 syl22anc ⊢ ( ( ( ( 𝑀 ∈ ℕ ∧ ¬ 2 ∥ 𝑀 ) ∧ ( 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) ) ∧ ¬ ( 𝑀 gcd 𝑁 ) = 1 ) → 2 ∥ ( 𝑁 − 1 ) )
60 peano2zm ⊢ ( 𝑁 ∈ ℤ → ( 𝑁 − 1 ) ∈ ℤ )
61 56 60 syl ⊢ ( ( ( ( 𝑀 ∈ ℕ ∧ ¬ 2 ∥ 𝑀 ) ∧ ( 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) ) ∧ ¬ ( 𝑀 gcd 𝑁 ) = 1 ) → ( 𝑁 − 1 ) ∈ ℤ )
62 dvdsval2 ⊢ ( ( 2 ∈ ℤ ∧ 2 ≠ 0 ∧ ( 𝑁 − 1 ) ∈ ℤ ) → ( 2 ∥ ( 𝑁 − 1 ) ↔ ( ( 𝑁 − 1 ) / 2 ) ∈ ℤ ) )
63 48 49 61 62 mp3an12i ⊢ ( ( ( ( 𝑀 ∈ ℕ ∧ ¬ 2 ∥ 𝑀 ) ∧ ( 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) ) ∧ ¬ ( 𝑀 gcd 𝑁 ) = 1 ) → ( 2 ∥ ( 𝑁 − 1 ) ↔ ( ( 𝑁 − 1 ) / 2 ) ∈ ℤ ) )
64 59 63 mpbid ⊢ ( ( ( ( 𝑀 ∈ ℕ ∧ ¬ 2 ∥ 𝑀 ) ∧ ( 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) ) ∧ ¬ ( 𝑀 gcd 𝑁 ) = 1 ) → ( ( 𝑁 − 1 ) / 2 ) ∈ ℤ )
65 54 64 zmulcld ⊢ ( ( ( ( 𝑀 ∈ ℕ ∧ ¬ 2 ∥ 𝑀 ) ∧ ( 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) ) ∧ ¬ ( 𝑀 gcd 𝑁 ) = 1 ) → ( ( ( 𝑀 − 1 ) / 2 ) · ( ( 𝑁 − 1 ) / 2 ) ) ∈ ℤ )
66 37 39 65 expclzd ⊢ ( ( ( ( 𝑀 ∈ ℕ ∧ ¬ 2 ∥ 𝑀 ) ∧ ( 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) ) ∧ ¬ ( 𝑀 gcd 𝑁 ) = 1 ) → ( - 1 ↑ ( ( ( 𝑀 − 1 ) / 2 ) · ( ( 𝑁 − 1 ) / 2 ) ) ) ∈ ℂ )
67 66 mul01d ⊢ ( ( ( ( 𝑀 ∈ ℕ ∧ ¬ 2 ∥ 𝑀 ) ∧ ( 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) ) ∧ ¬ ( 𝑀 gcd 𝑁 ) = 1 ) → ( ( - 1 ↑ ( ( ( 𝑀 − 1 ) / 2 ) · ( ( 𝑁 − 1 ) / 2 ) ) ) · 0 ) = 0 )
68 lgsne0 ⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ ) → ( ( 𝑁 /L 𝑀 ) ≠ 0 ↔ ( 𝑁 gcd 𝑀 ) = 1 ) )
69 gcdcom ⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ ) → ( 𝑁 gcd 𝑀 ) = ( 𝑀 gcd 𝑁 ) )
70 69 eqeq1d ⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ ) → ( ( 𝑁 gcd 𝑀 ) = 1 ↔ ( 𝑀 gcd 𝑁 ) = 1 ) )
71 68 70 bitrd ⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ ) → ( ( 𝑁 /L 𝑀 ) ≠ 0 ↔ ( 𝑀 gcd 𝑁 ) = 1 ) )
72 2 4 71 syl2anr ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( ( 𝑁 /L 𝑀 ) ≠ 0 ↔ ( 𝑀 gcd 𝑁 ) = 1 ) )
73 72 necon1bbid ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( ¬ ( 𝑀 gcd 𝑁 ) = 1 ↔ ( 𝑁 /L 𝑀 ) = 0 ) )
74 73 ad2ant2r ⊢ ( ( ( 𝑀 ∈ ℕ ∧ ¬ 2 ∥ 𝑀 ) ∧ ( 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) ) → ( ¬ ( 𝑀 gcd 𝑁 ) = 1 ↔ ( 𝑁 /L 𝑀 ) = 0 ) )
75 74 biimpa ⊢ ( ( ( ( 𝑀 ∈ ℕ ∧ ¬ 2 ∥ 𝑀 ) ∧ ( 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) ) ∧ ¬ ( 𝑀 gcd 𝑁 ) = 1 ) → ( 𝑁 /L 𝑀 ) = 0 )
76 75 oveq2d ⊢ ( ( ( ( 𝑀 ∈ ℕ ∧ ¬ 2 ∥ 𝑀 ) ∧ ( 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) ) ∧ ¬ ( 𝑀 gcd 𝑁 ) = 1 ) → ( ( - 1 ↑ ( ( ( 𝑀 − 1 ) / 2 ) · ( ( 𝑁 − 1 ) / 2 ) ) ) · ( 𝑁 /L 𝑀 ) ) = ( ( - 1 ↑ ( ( ( 𝑀 − 1 ) / 2 ) · ( ( 𝑁 − 1 ) / 2 ) ) ) · 0 ) )
77 lgsne0 ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( 𝑀 /L 𝑁 ) ≠ 0 ↔ ( 𝑀 gcd 𝑁 ) = 1 ) )
78 77 necon1bbid ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ¬ ( 𝑀 gcd 𝑁 ) = 1 ↔ ( 𝑀 /L 𝑁 ) = 0 ) )
79 4 2 78 syl2an ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( ¬ ( 𝑀 gcd 𝑁 ) = 1 ↔ ( 𝑀 /L 𝑁 ) = 0 ) )
80 79 ad2ant2r ⊢ ( ( ( 𝑀 ∈ ℕ ∧ ¬ 2 ∥ 𝑀 ) ∧ ( 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) ) → ( ¬ ( 𝑀 gcd 𝑁 ) = 1 ↔ ( 𝑀 /L 𝑁 ) = 0 ) )
81 80 biimpa ⊢ ( ( ( ( 𝑀 ∈ ℕ ∧ ¬ 2 ∥ 𝑀 ) ∧ ( 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) ) ∧ ¬ ( 𝑀 gcd 𝑁 ) = 1 ) → ( 𝑀 /L 𝑁 ) = 0 )
82 67 76 81 3eqtr4rd ⊢ ( ( ( ( 𝑀 ∈ ℕ ∧ ¬ 2 ∥ 𝑀 ) ∧ ( 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) ) ∧ ¬ ( 𝑀 gcd 𝑁 ) = 1 ) → ( 𝑀 /L 𝑁 ) = ( ( - 1 ↑ ( ( ( 𝑀 − 1 ) / 2 ) · ( ( 𝑁 − 1 ) / 2 ) ) ) · ( 𝑁 /L 𝑀 ) ) )
83 35 82 pm2.61dan ⊢ ( ( ( 𝑀 ∈ ℕ ∧ ¬ 2 ∥ 𝑀 ) ∧ ( 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) ) → ( 𝑀 /L 𝑁 ) = ( ( - 1 ↑ ( ( ( 𝑀 − 1 ) / 2 ) · ( ( 𝑁 − 1 ) / 2 ) ) ) · ( 𝑁 /L 𝑀 ) ) )