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 𝑀 ) ) )