Theorem lgsquad3 25526

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

Assertion

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

Proof of Theorem lgsquad3

Step	Hyp	Ref	Expression
1		simplrl 797	. . . . . . . . . 10 ⊢ ((((𝑀 ∈ ℕ ∧ ¬ 2 ∥ 𝑀) ∧ (𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁)) ∧ (𝑀 gcd 𝑁) = 1) → 𝑁 ∈ ℕ)
2		nnz 11728	. . . . . . . . . 10 ⊢ (𝑁 ∈ ℕ → 𝑁 ∈ ℤ)
3	1, 2	syl 17	. . . . . . . . 9 ⊢ ((((𝑀 ∈ ℕ ∧ ¬ 2 ∥ 𝑀) ∧ (𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁)) ∧ (𝑀 gcd 𝑁) = 1) → 𝑁 ∈ ℤ)
4		nnz 11728	. . . . . . . . . 10 ⊢ (𝑀 ∈ ℕ → 𝑀 ∈ ℤ)
5	4	ad3antrrr 723	. . . . . . . . 9 ⊢ ((((𝑀 ∈ ℕ ∧ ¬ 2 ∥ 𝑀) ∧ (𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁)) ∧ (𝑀 gcd 𝑁) = 1) → 𝑀 ∈ ℤ)
6		lgscl 25450	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ) → (𝑁 /L 𝑀) ∈ ℤ)
7	3, 5, 6	syl2anc 581	. . . . . . . 8 ⊢ ((((𝑀 ∈ ℕ ∧ ¬ 2 ∥ 𝑀) ∧ (𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁)) ∧ (𝑀 gcd 𝑁) = 1) → (𝑁 /L 𝑀) ∈ ℤ)
8	7	zred 11811	. . . . . . 7 ⊢ ((((𝑀 ∈ ℕ ∧ ¬ 2 ∥ 𝑀) ∧ (𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁)) ∧ (𝑀 gcd 𝑁) = 1) → (𝑁 /L 𝑀) ∈ ℝ)
9		absresq 14420	. . . . . . 7 ⊢ ((𝑁 /L 𝑀) ∈ ℝ → ((abs‘(𝑁 /L 𝑀))↑2) = ((𝑁 /L 𝑀)↑2))
10	8, 9	syl 17	. . . . . 6 ⊢ ((((𝑀 ∈ ℕ ∧ ¬ 2 ∥ 𝑀) ∧ (𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁)) ∧ (𝑀 gcd 𝑁) = 1) → ((abs‘(𝑁 /L 𝑀))↑2) = ((𝑁 /L 𝑀)↑2))
11		gcdcom 15609	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ) → (𝑁 gcd 𝑀) = (𝑀 gcd 𝑁))
12	3, 5, 11	syl2anc 581	. . . . . . . . . 10 ⊢ ((((𝑀 ∈ ℕ ∧ ¬ 2 ∥ 𝑀) ∧ (𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁)) ∧ (𝑀 gcd 𝑁) = 1) → (𝑁 gcd 𝑀) = (𝑀 gcd 𝑁))
13		simpr 479	. . . . . . . . . 10 ⊢ ((((𝑀 ∈ ℕ ∧ ¬ 2 ∥ 𝑀) ∧ (𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁)) ∧ (𝑀 gcd 𝑁) = 1) → (𝑀 gcd 𝑁) = 1)
14	12, 13	eqtrd 2862	. . . . . . . . 9 ⊢ ((((𝑀 ∈ ℕ ∧ ¬ 2 ∥ 𝑀) ∧ (𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁)) ∧ (𝑀 gcd 𝑁) = 1) → (𝑁 gcd 𝑀) = 1)
15		lgsabs1 25475	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ) → ((abs‘(𝑁 /L 𝑀)) = 1 ↔ (𝑁 gcd 𝑀) = 1))
16	3, 5, 15	syl2anc 581	. . . . . . . . 9 ⊢ ((((𝑀 ∈ ℕ ∧ ¬ 2 ∥ 𝑀) ∧ (𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁)) ∧ (𝑀 gcd 𝑁) = 1) → ((abs‘(𝑁 /L 𝑀)) = 1 ↔ (𝑁 gcd 𝑀) = 1))
17	14, 16	mpbird 249	. . . . . . . 8 ⊢ ((((𝑀 ∈ ℕ ∧ ¬ 2 ∥ 𝑀) ∧ (𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁)) ∧ (𝑀 gcd 𝑁) = 1) → (abs‘(𝑁 /L 𝑀)) = 1)
18	17	oveq1d 6921	. . . . . . 7 ⊢ ((((𝑀 ∈ ℕ ∧ ¬ 2 ∥ 𝑀) ∧ (𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁)) ∧ (𝑀 gcd 𝑁) = 1) → ((abs‘(𝑁 /L 𝑀))↑2) = (1↑2))
19		sq1 13253	. . . . . . 7 ⊢ (1↑2) = 1
20	18, 19	syl6eq 2878	. . . . . 6 ⊢ ((((𝑀 ∈ ℕ ∧ ¬ 2 ∥ 𝑀) ∧ (𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁)) ∧ (𝑀 gcd 𝑁) = 1) → ((abs‘(𝑁 /L 𝑀))↑2) = 1)
21	7	zcnd 11812	. . . . . . 7 ⊢ ((((𝑀 ∈ ℕ ∧ ¬ 2 ∥ 𝑀) ∧ (𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁)) ∧ (𝑀 gcd 𝑁) = 1) → (𝑁 /L 𝑀) ∈ ℂ)
22	21	sqvald 13300	. . . . . 6 ⊢ ((((𝑀 ∈ ℕ ∧ ¬ 2 ∥ 𝑀) ∧ (𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁)) ∧ (𝑀 gcd 𝑁) = 1) → ((𝑁 /L 𝑀)↑2) = ((𝑁 /L 𝑀) · (𝑁 /L 𝑀)))
23	10, 20, 22	3eqtr3d 2870	. . . . 5 ⊢ ((((𝑀 ∈ ℕ ∧ ¬ 2 ∥ 𝑀) ∧ (𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁)) ∧ (𝑀 gcd 𝑁) = 1) → 1 = ((𝑁 /L 𝑀) · (𝑁 /L 𝑀)))
24	23	oveq2d 6922	. . . 4 ⊢ ((((𝑀 ∈ ℕ ∧ ¬ 2 ∥ 𝑀) ∧ (𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁)) ∧ (𝑀 gcd 𝑁) = 1) → ((𝑀 /L 𝑁) · 1) = ((𝑀 /L 𝑁) · ((𝑁 /L 𝑀) · (𝑁 /L 𝑀))))
25		lgscl 25450	. . . . . . 7 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 /L 𝑁) ∈ ℤ)
26	5, 3, 25	syl2anc 581	. . . . . 6 ⊢ ((((𝑀 ∈ ℕ ∧ ¬ 2 ∥ 𝑀) ∧ (𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁)) ∧ (𝑀 gcd 𝑁) = 1) → (𝑀 /L 𝑁) ∈ ℤ)
27	26	zcnd 11812	. . . . 5 ⊢ ((((𝑀 ∈ ℕ ∧ ¬ 2 ∥ 𝑀) ∧ (𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁)) ∧ (𝑀 gcd 𝑁) = 1) → (𝑀 /L 𝑁) ∈ ℂ)
28	27, 21, 21	mulassd 10381	. . . 4 ⊢ ((((𝑀 ∈ ℕ ∧ ¬ 2 ∥ 𝑀) ∧ (𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁)) ∧ (𝑀 gcd 𝑁) = 1) → (((𝑀 /L 𝑁) · (𝑁 /L 𝑀)) · (𝑁 /L 𝑀)) = ((𝑀 /L 𝑁) · ((𝑁 /L 𝑀) · (𝑁 /L 𝑀))))
29	24, 28	eqtr4d 2865	. . 3 ⊢ ((((𝑀 ∈ ℕ ∧ ¬ 2 ∥ 𝑀) ∧ (𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁)) ∧ (𝑀 gcd 𝑁) = 1) → ((𝑀 /L 𝑁) · 1) = (((𝑀 /L 𝑁) · (𝑁 /L 𝑀)) · (𝑁 /L 𝑀)))
30	27	mulid1d 10375	. . 3 ⊢ ((((𝑀 ∈ ℕ ∧ ¬ 2 ∥ 𝑀) ∧ (𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁)) ∧ (𝑀 gcd 𝑁) = 1) → ((𝑀 /L 𝑁) · 1) = (𝑀 /L 𝑁))
31		simplll 793	. . . . 5 ⊢ ((((𝑀 ∈ ℕ ∧ ¬ 2 ∥ 𝑀) ∧ (𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁)) ∧ (𝑀 gcd 𝑁) = 1) → 𝑀 ∈ ℕ)
32		simpllr 795	. . . . 5 ⊢ ((((𝑀 ∈ ℕ ∧ ¬ 2 ∥ 𝑀) ∧ (𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁)) ∧ (𝑀 gcd 𝑁) = 1) → ¬ 2 ∥ 𝑀)
33		simplrr 798	. . . . 5 ⊢ ((((𝑀 ∈ ℕ ∧ ¬ 2 ∥ 𝑀) ∧ (𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁)) ∧ (𝑀 gcd 𝑁) = 1) → ¬ 2 ∥ 𝑁)
34	31, 32, 1, 33, 13	lgsquad2 25525	. . . 4 ⊢ ((((𝑀 ∈ ℕ ∧ ¬ 2 ∥ 𝑀) ∧ (𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁)) ∧ (𝑀 gcd 𝑁) = 1) → ((𝑀 /L 𝑁) · (𝑁 /L 𝑀)) = (-1↑(((𝑀 − 1) / 2) · ((𝑁 − 1) / 2))))
35	34	oveq1d 6921	. . 3 ⊢ ((((𝑀 ∈ ℕ ∧ ¬ 2 ∥ 𝑀) ∧ (𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁)) ∧ (𝑀 gcd 𝑁) = 1) → (((𝑀 /L 𝑁) · (𝑁 /L 𝑀)) · (𝑁 /L 𝑀)) = ((-1↑(((𝑀 − 1) / 2) · ((𝑁 − 1) / 2))) · (𝑁 /L 𝑀)))
36	29, 30, 35	3eqtr3d 2870	. 2 ⊢ ((((𝑀 ∈ ℕ ∧ ¬ 2 ∥ 𝑀) ∧ (𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁)) ∧ (𝑀 gcd 𝑁) = 1) → (𝑀 /L 𝑁) = ((-1↑(((𝑀 − 1) / 2) · ((𝑁 − 1) / 2))) · (𝑁 /L 𝑀)))
37		neg1cn 11473	. . . . . 6 ⊢ -1 ∈ ℂ
38	37	a1i 11	. . . . 5 ⊢ ((((𝑀 ∈ ℕ ∧ ¬ 2 ∥ 𝑀) ∧ (𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁)) ∧ ¬ (𝑀 gcd 𝑁) = 1) → -1 ∈ ℂ)
39		neg1ne0 11475	. . . . . 6 ⊢ -1 ≠ 0
40	39	a1i 11	. . . . 5 ⊢ ((((𝑀 ∈ ℕ ∧ ¬ 2 ∥ 𝑀) ∧ (𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁)) ∧ ¬ (𝑀 gcd 𝑁) = 1) → -1 ≠ 0)
41	4	ad3antrrr 723	. . . . . . . 8 ⊢ ((((𝑀 ∈ ℕ ∧ ¬ 2 ∥ 𝑀) ∧ (𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁)) ∧ ¬ (𝑀 gcd 𝑁) = 1) → 𝑀 ∈ ℤ)
42		simpllr 795	. . . . . . . 8 ⊢ ((((𝑀 ∈ ℕ ∧ ¬ 2 ∥ 𝑀) ∧ (𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁)) ∧ ¬ (𝑀 gcd 𝑁) = 1) → ¬ 2 ∥ 𝑀)
43		1zzd 11737	. . . . . . . 8 ⊢ ((((𝑀 ∈ ℕ ∧ ¬ 2 ∥ 𝑀) ∧ (𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁)) ∧ ¬ (𝑀 gcd 𝑁) = 1) → 1 ∈ ℤ)
44		2prm 15778	. . . . . . . . 9 ⊢ 2 ∈ ℙ
45		nprmdvds1 15790	. . . . . . . . 9 ⊢ (2 ∈ ℙ → ¬ 2 ∥ 1)
46	44, 45	mp1i 13	. . . . . . . 8 ⊢ ((((𝑀 ∈ ℕ ∧ ¬ 2 ∥ 𝑀) ∧ (𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁)) ∧ ¬ (𝑀 gcd 𝑁) = 1) → ¬ 2 ∥ 1)
47		omoe 15463	. . . . . . . 8 ⊢ (((𝑀 ∈ ℤ ∧ ¬ 2 ∥ 𝑀) ∧ (1 ∈ ℤ ∧ ¬ 2 ∥ 1)) → 2 ∥ (𝑀 − 1))
48	41, 42, 43, 46, 47	syl22anc 874	. . . . . . 7 ⊢ ((((𝑀 ∈ ℕ ∧ ¬ 2 ∥ 𝑀) ∧ (𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁)) ∧ ¬ (𝑀 gcd 𝑁) = 1) → 2 ∥ (𝑀 − 1))
49		2z 11738	. . . . . . . . 9 ⊢ 2 ∈ ℤ
50	49	a1i 11	. . . . . . . 8 ⊢ ((((𝑀 ∈ ℕ ∧ ¬ 2 ∥ 𝑀) ∧ (𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁)) ∧ ¬ (𝑀 gcd 𝑁) = 1) → 2 ∈ ℤ)
51		2ne0 11463	. . . . . . . . 9 ⊢ 2 ≠ 0
52	51	a1i 11	. . . . . . . 8 ⊢ ((((𝑀 ∈ ℕ ∧ ¬ 2 ∥ 𝑀) ∧ (𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁)) ∧ ¬ (𝑀 gcd 𝑁) = 1) → 2 ≠ 0)
53		peano2zm 11749	. . . . . . . . 9 ⊢ (𝑀 ∈ ℤ → (𝑀 − 1) ∈ ℤ)
54	41, 53	syl 17	. . . . . . . 8 ⊢ ((((𝑀 ∈ ℕ ∧ ¬ 2 ∥ 𝑀) ∧ (𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁)) ∧ ¬ (𝑀 gcd 𝑁) = 1) → (𝑀 − 1) ∈ ℤ)
55		dvdsval2 15361	. . . . . . . 8 ⊢ ((2 ∈ ℤ ∧ 2 ≠ 0 ∧ (𝑀 − 1) ∈ ℤ) → (2 ∥ (𝑀 − 1) ↔ ((𝑀 − 1) / 2) ∈ ℤ))
56	50, 52, 54, 55	syl3anc 1496	. . . . . . 7 ⊢ ((((𝑀 ∈ ℕ ∧ ¬ 2 ∥ 𝑀) ∧ (𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁)) ∧ ¬ (𝑀 gcd 𝑁) = 1) → (2 ∥ (𝑀 − 1) ↔ ((𝑀 − 1) / 2) ∈ ℤ))
57	48, 56	mpbid 224	. . . . . 6 ⊢ ((((𝑀 ∈ ℕ ∧ ¬ 2 ∥ 𝑀) ∧ (𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁)) ∧ ¬ (𝑀 gcd 𝑁) = 1) → ((𝑀 − 1) / 2) ∈ ℤ)
58	2	adantr 474	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁) → 𝑁 ∈ ℤ)
59	58	ad2antlr 720	. . . . . . . 8 ⊢ ((((𝑀 ∈ ℕ ∧ ¬ 2 ∥ 𝑀) ∧ (𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁)) ∧ ¬ (𝑀 gcd 𝑁) = 1) → 𝑁 ∈ ℤ)
60		simplrr 798	. . . . . . . 8 ⊢ ((((𝑀 ∈ ℕ ∧ ¬ 2 ∥ 𝑀) ∧ (𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁)) ∧ ¬ (𝑀 gcd 𝑁) = 1) → ¬ 2 ∥ 𝑁)
61		omoe 15463	. . . . . . . 8 ⊢ (((𝑁 ∈ ℤ ∧ ¬ 2 ∥ 𝑁) ∧ (1 ∈ ℤ ∧ ¬ 2 ∥ 1)) → 2 ∥ (𝑁 − 1))
62	59, 60, 43, 46, 61	syl22anc 874	. . . . . . 7 ⊢ ((((𝑀 ∈ ℕ ∧ ¬ 2 ∥ 𝑀) ∧ (𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁)) ∧ ¬ (𝑀 gcd 𝑁) = 1) → 2 ∥ (𝑁 − 1))
63		peano2zm 11749	. . . . . . . . 9 ⊢ (𝑁 ∈ ℤ → (𝑁 − 1) ∈ ℤ)
64	59, 63	syl 17	. . . . . . . 8 ⊢ ((((𝑀 ∈ ℕ ∧ ¬ 2 ∥ 𝑀) ∧ (𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁)) ∧ ¬ (𝑀 gcd 𝑁) = 1) → (𝑁 − 1) ∈ ℤ)
65		dvdsval2 15361	. . . . . . . 8 ⊢ ((2 ∈ ℤ ∧ 2 ≠ 0 ∧ (𝑁 − 1) ∈ ℤ) → (2 ∥ (𝑁 − 1) ↔ ((𝑁 − 1) / 2) ∈ ℤ))
66	50, 52, 64, 65	syl3anc 1496	. . . . . . 7 ⊢ ((((𝑀 ∈ ℕ ∧ ¬ 2 ∥ 𝑀) ∧ (𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁)) ∧ ¬ (𝑀 gcd 𝑁) = 1) → (2 ∥ (𝑁 − 1) ↔ ((𝑁 − 1) / 2) ∈ ℤ))
67	62, 66	mpbid 224	. . . . . 6 ⊢ ((((𝑀 ∈ ℕ ∧ ¬ 2 ∥ 𝑀) ∧ (𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁)) ∧ ¬ (𝑀 gcd 𝑁) = 1) → ((𝑁 − 1) / 2) ∈ ℤ)
68	57, 67	zmulcld 11817	. . . . 5 ⊢ ((((𝑀 ∈ ℕ ∧ ¬ 2 ∥ 𝑀) ∧ (𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁)) ∧ ¬ (𝑀 gcd 𝑁) = 1) → (((𝑀 − 1) / 2) · ((𝑁 − 1) / 2)) ∈ ℤ)
69	38, 40, 68	expclzd 13308	. . . 4 ⊢ ((((𝑀 ∈ ℕ ∧ ¬ 2 ∥ 𝑀) ∧ (𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁)) ∧ ¬ (𝑀 gcd 𝑁) = 1) → (-1↑(((𝑀 − 1) / 2) · ((𝑁 − 1) / 2))) ∈ ℂ)
70	69	mul01d 10555	. . 3 ⊢ ((((𝑀 ∈ ℕ ∧ ¬ 2 ∥ 𝑀) ∧ (𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁)) ∧ ¬ (𝑀 gcd 𝑁) = 1) → ((-1↑(((𝑀 − 1) / 2) · ((𝑁 − 1) / 2))) · 0) = 0)
71		lgsne0 25474	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ) → ((𝑁 /L 𝑀) ≠ 0 ↔ (𝑁 gcd 𝑀) = 1))
72	11	eqeq1d 2828	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ) → ((𝑁 gcd 𝑀) = 1 ↔ (𝑀 gcd 𝑁) = 1))
73	71, 72	bitrd 271	. . . . . . . 8 ⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ) → ((𝑁 /L 𝑀) ≠ 0 ↔ (𝑀 gcd 𝑁) = 1))
74	2, 4, 73	syl2anr 592	. . . . . . 7 ⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → ((𝑁 /L 𝑀) ≠ 0 ↔ (𝑀 gcd 𝑁) = 1))
75	74	necon1bbid 3039	. . . . . 6 ⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (¬ (𝑀 gcd 𝑁) = 1 ↔ (𝑁 /L 𝑀) = 0))
76	75	ad2ant2r 755	. . . . 5 ⊢ (((𝑀 ∈ ℕ ∧ ¬ 2 ∥ 𝑀) ∧ (𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁)) → (¬ (𝑀 gcd 𝑁) = 1 ↔ (𝑁 /L 𝑀) = 0))
77	76	biimpa 470	. . . 4 ⊢ ((((𝑀 ∈ ℕ ∧ ¬ 2 ∥ 𝑀) ∧ (𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁)) ∧ ¬ (𝑀 gcd 𝑁) = 1) → (𝑁 /L 𝑀) = 0)
78	77	oveq2d 6922	. . 3 ⊢ ((((𝑀 ∈ ℕ ∧ ¬ 2 ∥ 𝑀) ∧ (𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁)) ∧ ¬ (𝑀 gcd 𝑁) = 1) → ((-1↑(((𝑀 − 1) / 2) · ((𝑁 − 1) / 2))) · (𝑁 /L 𝑀)) = ((-1↑(((𝑀 − 1) / 2) · ((𝑁 − 1) / 2))) · 0))
79		lgsne0 25474	. . . . . . 7 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝑀 /L 𝑁) ≠ 0 ↔ (𝑀 gcd 𝑁) = 1))
80	79	necon1bbid 3039	. . . . . 6 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (¬ (𝑀 gcd 𝑁) = 1 ↔ (𝑀 /L 𝑁) = 0))
81	4, 2, 80	syl2an 591	. . . . 5 ⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (¬ (𝑀 gcd 𝑁) = 1 ↔ (𝑀 /L 𝑁) = 0))
82	81	ad2ant2r 755	. . . 4 ⊢ (((𝑀 ∈ ℕ ∧ ¬ 2 ∥ 𝑀) ∧ (𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁)) → (¬ (𝑀 gcd 𝑁) = 1 ↔ (𝑀 /L 𝑁) = 0))
83	82	biimpa 470	. . 3 ⊢ ((((𝑀 ∈ ℕ ∧ ¬ 2 ∥ 𝑀) ∧ (𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁)) ∧ ¬ (𝑀 gcd 𝑁) = 1) → (𝑀 /L 𝑁) = 0)
84	70, 78, 83	3eqtr4rd 2873	. 2 ⊢ ((((𝑀 ∈ ℕ ∧ ¬ 2 ∥ 𝑀) ∧ (𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁)) ∧ ¬ (𝑀 gcd 𝑁) = 1) → (𝑀 /L 𝑁) = ((-1↑(((𝑀 − 1) / 2) · ((𝑁 − 1) / 2))) · (𝑁 /L 𝑀)))
85	36, 84	pm2.61dan 849	1 ⊢ (((𝑀 ∈ ℕ ∧ ¬ 2 ∥ 𝑀) ∧ (𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁)) → (𝑀 /L 𝑁) = ((-1↑(((𝑀 − 1) / 2) · ((𝑁 − 1) / 2))) · (𝑁 /L 𝑀)))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 198   ∧ wa 386   = wceq 1658   ∈ wcel 2166   ≠ wne 3000   class class class wbr 4874  ‘cfv 6124  (class class class)co 6906  ℂcc 10251  ℝcr 10252  0cc0 10253  1c1 10254   · cmul 10258   − cmin 10586  -cneg 10587   / cdiv 11010  ℕcn 11351  2c2 11407  ℤcz 11705  ↑cexp 13155  abscabs 14352   ∥ cdvds 15358   gcd cgcd 15590  ℙcprime 15758   /_L clgs 25433

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1896  ax-4 1910  ax-5 2011  ax-6 2077  ax-7 2114  ax-8 2168  ax-9 2175  ax-10 2194  ax-11 2209  ax-12 2222  ax-13 2391  ax-ext 2804  ax-rep 4995  ax-sep 5006  ax-nul 5014  ax-pow 5066  ax-pr 5128  ax-un 7210  ax-inf2 8816  ax-cnex 10309  ax-resscn 10310  ax-1cn 10311  ax-icn 10312  ax-addcl 10313  ax-addrcl 10314  ax-mulcl 10315  ax-mulrcl 10316  ax-mulcom 10317  ax-addass 10318  ax-mulass 10319  ax-distr 10320  ax-i2m1 10321  ax-1ne0 10322  ax-1rid 10323  ax-rnegex 10324  ax-rrecex 10325  ax-cnre 10326  ax-pre-lttri 10327  ax-pre-lttrn 10328  ax-pre-ltadd 10329  ax-pre-mulgt0 10330  ax-pre-sup 10331  ax-addf 10332  ax-mulf 10333

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 881  df-3or 1114  df-3an 1115  df-tru 1662  df-fal 1672  df-ex 1881  df-nf 1885  df-sb 2070  df-mo 2606  df-eu 2641  df-clab 2813  df-cleq 2819  df-clel 2822  df-nfc 2959  df-ne 3001  df-nel 3104  df-ral 3123  df-rex 3124  df-reu 3125  df-rmo 3126  df-rab 3127  df-v 3417  df-sbc 3664  df-csb 3759  df-dif 3802  df-un 3804  df-in 3806  df-ss 3813  df-pss 3815  df-nul 4146  df-if 4308  df-pw 4381  df-sn 4399  df-pr 4401  df-tp 4403  df-op 4405  df-uni 4660  df-int 4699  df-iun 4743  df-disj 4843  df-br 4875  df-opab 4937  df-mpt 4954  df-tr 4977  df-id 5251  df-eprel 5256  df-po 5264  df-so 5265  df-fr 5302  df-se 5303  df-we 5304  df-xp 5349  df-rel 5350  df-cnv 5351  df-co 5352  df-dm 5353  df-rn 5354  df-res 5355  df-ima 5356  df-pred 5921  df-ord 5967  df-on 5968  df-lim 5969  df-suc 5970  df-iota 6087  df-fun 6126  df-fn 6127  df-f 6128  df-f1 6129  df-fo 6130  df-f1o 6131  df-fv 6132  df-isom 6133  df-riota 6867  df-ov 6909  df-oprab 6910  df-mpt2 6911  df-of 7158  df-om 7328  df-1st 7429  df-2nd 7430  df-supp 7561  df-tpos 7618  df-wrecs 7673  df-recs 7735  df-rdg 7773  df-1o 7827  df-2o 7828  df-oadd 7831  df-er 8010  df-ec 8012  df-qs 8016  df-map 8125  df-en 8224  df-dom 8225  df-sdom 8226  df-fin 8227  df-fsupp 8546  df-sup 8618  df-inf 8619  df-oi 8685  df-card 9079  df-cda 9306  df-pnf 10394  df-mnf 10395  df-xr 10396  df-ltxr 10397  df-le 10398  df-sub 10588  df-neg 10589  df-div 11011  df-nn 11352  df-2 11415  df-3 11416  df-4 11417  df-5 11418  df-6 11419  df-7 11420  df-8 11421  df-9 11422  df-n0 11620  df-xnn0 11692  df-z 11706  df-dec 11823  df-uz 11970  df-q 12073  df-rp 12114  df-fz 12621  df-fzo 12762  df-fl 12889  df-mod 12965  df-seq 13097  df-exp 13156  df-hash 13412  df-cj 14217  df-re 14218  df-im 14219  df-sqrt 14353  df-abs 14354  df-clim 14597  df-sum 14795  df-dvds 15359  df-gcd 15591  df-prm 15759  df-phi 15843  df-pc 15914  df-struct 16225  df-ndx 16226  df-slot 16227  df-base 16229  df-sets 16230  df-ress 16231  df-plusg 16319  df-mulr 16320  df-starv 16321  df-sca 16322  df-vsca 16323  df-ip 16324  df-tset 16325  df-ple 16326  df-ds 16328  df-unif 16329  df-0g 16456  df-gsum 16457  df-imas 16522  df-qus 16523  df-mgm 17596  df-sgrp 17638  df-mnd 17649  df-mhm 17689  df-submnd 17690  df-grp 17780  df-minusg 17781  df-sbg 17782  df-mulg 17896  df-subg 17943  df-nsg 17944  df-eqg 17945  df-ghm 18010  df-cntz 18101  df-cmn 18549  df-abl 18550  df-mgp 18845  df-ur 18857  df-ring 18904  df-cring 18905  df-oppr 18978  df-dvdsr 18996  df-unit 18997  df-invr 19027  df-dvr 19038  df-rnghom 19072  df-drng 19106  df-field 19107  df-subrg 19135  df-lmod 19222  df-lss 19290  df-lsp 19332  df-sra 19534  df-rgmod 19535  df-lidl 19536  df-rsp 19537  df-2idl 19594  df-nzr 19620  df-rlreg 19645  df-domn 19646  df-idom 19647  df-cnfld 20108  df-zring 20180  df-zrh 20213  df-zn 20216  df-lgs 25434

This theorem is referenced by: (None)