lgsquad3

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

		Ref	Expression
	Assertion	lgsquad3	$⊢ ((M \in ℕ \land \neg 2 ∥ M) \land (N \in ℕ \land \neg 2 ∥ N)) \to M /_{L} N = {(- 1)}^{(\frac{M - 1}{2}) (\frac{N - 1}{2})} (N /_{L} M)$

Proof

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

Metamath Proof Explorer

Theorem lgsquad3

Proof