lgsdi

Description: The Legendre symbol is completely multiplicative in its right argument. Generalization of theorem 9.9(b) in ApostolNT p. 188 (which assumes that M and N are odd positive integers). (Contributed by Mario Carneiro, 5-Feb-2015)

		Ref	Expression
	Assertion	lgsdi	$⊢ ((A \in ℤ \land M \in ℤ \land N \in ℤ) \land (M \neq 0 \land N \neq 0)) \to A /_{L} M \cdot N = (A /_{L} M) (A /_{L} N)$

Proof

Step	Hyp	Ref	Expression
1		3anrot	$⊢ (A \in ℤ \land M \in ℤ \land N \in ℤ) \leftrightarrow (M \in ℤ \land N \in ℤ \land A \in ℤ)$
2		lgsdilem	$⊢ ((M \in ℤ \land N \in ℤ \land A \in ℤ) \land (M \neq 0 \land N \neq 0)) \to if ((A < 0 \land M \cdot N < 0), - 1, 1) = if ((A < 0 \land M < 0), - 1, 1) if ((A < 0 \land N < 0), - 1, 1)$
3	1 2	sylanb	$⊢ ((A \in ℤ \land M \in ℤ \land N \in ℤ) \land (M \neq 0 \land N \neq 0)) \to if ((A < 0 \land M \cdot N < 0), - 1, 1) = if ((A < 0 \land M < 0), - 1, 1) if ((A < 0 \land N < 0), - 1, 1)$
4		ancom	$⊢ (M \cdot N < 0 \land A < 0) \leftrightarrow (A < 0 \land M \cdot N < 0)$
5		ifbi	$⊢ ((M \cdot N < 0 \land A < 0) \leftrightarrow (A < 0 \land M \cdot N < 0)) \to if ((M \cdot N < 0 \land A < 0), - 1, 1) = if ((A < 0 \land M \cdot N < 0), - 1, 1)$
6	4 5	ax-mp	$⊢ if ((M \cdot N < 0 \land A < 0), - 1, 1) = if ((A < 0 \land M \cdot N < 0), - 1, 1)$
7		ancom	$⊢ (M < 0 \land A < 0) \leftrightarrow (A < 0 \land M < 0)$
8		ifbi	$⊢ ((M < 0 \land A < 0) \leftrightarrow (A < 0 \land M < 0)) \to if ((M < 0 \land A < 0), - 1, 1) = if ((A < 0 \land M < 0), - 1, 1)$
9	7 8	ax-mp	$⊢ if ((M < 0 \land A < 0), - 1, 1) = if ((A < 0 \land M < 0), - 1, 1)$
10		ancom	$⊢ (N < 0 \land A < 0) \leftrightarrow (A < 0 \land N < 0)$
11		ifbi	$⊢ ((N < 0 \land A < 0) \leftrightarrow (A < 0 \land N < 0)) \to if ((N < 0 \land A < 0), - 1, 1) = if ((A < 0 \land N < 0), - 1, 1)$
12	10 11	ax-mp	$⊢ if ((N < 0 \land A < 0), - 1, 1) = if ((A < 0 \land N < 0), - 1, 1)$
13	9 12	oveq12i	$⊢ if ((M < 0 \land A < 0), - 1, 1) if ((N < 0 \land A < 0), - 1, 1) = if ((A < 0 \land M < 0), - 1, 1) if ((A < 0 \land N < 0), - 1, 1)$
14	3 6 13	3eqtr4g	$⊢ ((A \in ℤ \land M \in ℤ \land N \in ℤ) \land (M \neq 0 \land N \neq 0)) \to if ((M \cdot N < 0 \land A < 0), - 1, 1) = if ((M < 0 \land A < 0), - 1, 1) if ((N < 0 \land A < 0), - 1, 1)$
15		simpl2	$⊢ ((A \in ℤ \land M \in ℤ \land N \in ℤ) \land (M \neq 0 \land N \neq 0)) \to M \in ℤ$
16		simpl3	$⊢ ((A \in ℤ \land M \in ℤ \land N \in ℤ) \land (M \neq 0 \land N \neq 0)) \to N \in ℤ$
17	15 16	zmulcld	$⊢ ((A \in ℤ \land M \in ℤ \land N \in ℤ) \land (M \neq 0 \land N \neq 0)) \to M \cdot N \in ℤ$
18	15	zcnd	$⊢ ((A \in ℤ \land M \in ℤ \land N \in ℤ) \land (M \neq 0 \land N \neq 0)) \to M \in ℂ$
19	16	zcnd	$⊢ ((A \in ℤ \land M \in ℤ \land N \in ℤ) \land (M \neq 0 \land N \neq 0)) \to N \in ℂ$
20		simprl	$⊢ ((A \in ℤ \land M \in ℤ \land N \in ℤ) \land (M \neq 0 \land N \neq 0)) \to M \neq 0$
21		simprr	$⊢ ((A \in ℤ \land M \in ℤ \land N \in ℤ) \land (M \neq 0 \land N \neq 0)) \to N \neq 0$
22	18 19 20 21	mulne0d	$⊢ ((A \in ℤ \land M \in ℤ \land N \in ℤ) \land (M \neq 0 \land N \neq 0)) \to M \cdot N \neq 0$
23		nnabscl	$⊢ (M \cdot N \in ℤ \land M \cdot N \neq 0) \to \|M \cdot N\| \in ℕ$
24	17 22 23	syl2anc	$⊢ ((A \in ℤ \land M \in ℤ \land N \in ℤ) \land (M \neq 0 \land N \neq 0)) \to \|M \cdot N\| \in ℕ$
25		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
26	24 25	eleqtrdi	$⊢ ((A \in ℤ \land M \in ℤ \land N \in ℤ) \land (M \neq 0 \land N \neq 0)) \to \|M \cdot N\| \in ℤ_{\geq 1}$
27		simpl1	$⊢ ((A \in ℤ \land M \in ℤ \land N \in ℤ) \land (M \neq 0 \land N \neq 0)) \to A \in ℤ$
28		eqid	$⊢ (n \in ℕ ⟼ if (n \in ℙ, {(A /_{L} n)}^{n pCnt M}, 1)) = (n \in ℕ ⟼ if (n \in ℙ, {(A /_{L} n)}^{n pCnt M}, 1))$
29	28	lgsfcl3	$⊢ (A \in ℤ \land M \in ℤ \land M \neq 0) \to (n \in ℕ ⟼ if (n \in ℙ, {(A /_{L} n)}^{n pCnt M}, 1)) : ℕ ⟶ ℤ$
30	27 15 20 29	syl3anc	$⊢ ((A \in ℤ \land M \in ℤ \land N \in ℤ) \land (M \neq 0 \land N \neq 0)) \to (n \in ℕ ⟼ if (n \in ℙ, {(A /_{L} n)}^{n pCnt M}, 1)) : ℕ ⟶ ℤ$
31		elfznn	$⊢ k \in (1 \dots \|M \cdot N\|) \to k \in ℕ$
32		ffvelrn	$⊢ ((n \in ℕ ⟼ if (n \in ℙ, {(A /_{L} n)}^{n pCnt M}, 1)) : ℕ ⟶ ℤ \land k \in ℕ) \to (n \in ℕ ⟼ if (n \in ℙ, {(A /_{L} n)}^{n pCnt M}, 1)) (k) \in ℤ$
33	30 31 32	syl2an	$⊢ (((A \in ℤ \land M \in ℤ \land N \in ℤ) \land (M \neq 0 \land N \neq 0)) \land k \in (1 \dots \|M \cdot N\|)) \to (n \in ℕ ⟼ if (n \in ℙ, {(A /_{L} n)}^{n pCnt M}, 1)) (k) \in ℤ$
34	33	zcnd	$⊢ (((A \in ℤ \land M \in ℤ \land N \in ℤ) \land (M \neq 0 \land N \neq 0)) \land k \in (1 \dots \|M \cdot N\|)) \to (n \in ℕ ⟼ if (n \in ℙ, {(A /_{L} n)}^{n pCnt M}, 1)) (k) \in ℂ$
35		eqid	$⊢ (n \in ℕ ⟼ if (n \in ℙ, {(A /_{L} n)}^{n pCnt N}, 1)) = (n \in ℕ ⟼ if (n \in ℙ, {(A /_{L} n)}^{n pCnt N}, 1))$
36	35	lgsfcl3	$⊢ (A \in ℤ \land N \in ℤ \land N \neq 0) \to (n \in ℕ ⟼ if (n \in ℙ, {(A /_{L} n)}^{n pCnt N}, 1)) : ℕ ⟶ ℤ$
37	27 16 21 36	syl3anc	$⊢ ((A \in ℤ \land M \in ℤ \land N \in ℤ) \land (M \neq 0 \land N \neq 0)) \to (n \in ℕ ⟼ if (n \in ℙ, {(A /_{L} n)}^{n pCnt N}, 1)) : ℕ ⟶ ℤ$
38		ffvelrn	$⊢ ((n \in ℕ ⟼ if (n \in ℙ, {(A /_{L} n)}^{n pCnt N}, 1)) : ℕ ⟶ ℤ \land k \in ℕ) \to (n \in ℕ ⟼ if (n \in ℙ, {(A /_{L} n)}^{n pCnt N}, 1)) (k) \in ℤ$
39	37 31 38	syl2an	$⊢ (((A \in ℤ \land M \in ℤ \land N \in ℤ) \land (M \neq 0 \land N \neq 0)) \land k \in (1 \dots \|M \cdot N\|)) \to (n \in ℕ ⟼ if (n \in ℙ, {(A /_{L} n)}^{n pCnt N}, 1)) (k) \in ℤ$
40	39	zcnd	$⊢ (((A \in ℤ \land M \in ℤ \land N \in ℤ) \land (M \neq 0 \land N \neq 0)) \land k \in (1 \dots \|M \cdot N\|)) \to (n \in ℕ ⟼ if (n \in ℙ, {(A /_{L} n)}^{n pCnt N}, 1)) (k) \in ℂ$
41		simpr	$⊢ ((((A \in ℤ \land M \in ℤ \land N \in ℤ) \land (M \neq 0 \land N \neq 0)) \land k \in (1 \dots \|M \cdot N\|)) \land k \in ℙ) \to k \in ℙ$
42	15	ad2antrr	$⊢ ((((A \in ℤ \land M \in ℤ \land N \in ℤ) \land (M \neq 0 \land N \neq 0)) \land k \in (1 \dots \|M \cdot N\|)) \land k \in ℙ) \to M \in ℤ$
43	20	ad2antrr	$⊢ ((((A \in ℤ \land M \in ℤ \land N \in ℤ) \land (M \neq 0 \land N \neq 0)) \land k \in (1 \dots \|M \cdot N\|)) \land k \in ℙ) \to M \neq 0$
44	16	ad2antrr	$⊢ ((((A \in ℤ \land M \in ℤ \land N \in ℤ) \land (M \neq 0 \land N \neq 0)) \land k \in (1 \dots \|M \cdot N\|)) \land k \in ℙ) \to N \in ℤ$
45	21	ad2antrr	$⊢ ((((A \in ℤ \land M \in ℤ \land N \in ℤ) \land (M \neq 0 \land N \neq 0)) \land k \in (1 \dots \|M \cdot N\|)) \land k \in ℙ) \to N \neq 0$
46		pcmul	$⊢ (k \in ℙ \land (M \in ℤ \land M \neq 0) \land (N \in ℤ \land N \neq 0)) \to k pCnt M \cdot N = (k pCnt M) + (k pCnt N)$
47	41 42 43 44 45 46	syl122anc	$⊢ ((((A \in ℤ \land M \in ℤ \land N \in ℤ) \land (M \neq 0 \land N \neq 0)) \land k \in (1 \dots \|M \cdot N\|)) \land k \in ℙ) \to k pCnt M \cdot N = (k pCnt M) + (k pCnt N)$
48	47	oveq2d	$⊢ ((((A \in ℤ \land M \in ℤ \land N \in ℤ) \land (M \neq 0 \land N \neq 0)) \land k \in (1 \dots \|M \cdot N\|)) \land k \in ℙ) \to {(A /_{L} k)}^{k pCnt M \cdot N} = {(A /_{L} k)}^{(k pCnt M) + (k pCnt N)}$
49	27	ad2antrr	$⊢ ((((A \in ℤ \land M \in ℤ \land N \in ℤ) \land (M \neq 0 \land N \neq 0)) \land k \in (1 \dots \|M \cdot N\|)) \land k \in ℙ) \to A \in ℤ$
50		prmz	$⊢ k \in ℙ \to k \in ℤ$
51	50	adantl	$⊢ ((((A \in ℤ \land M \in ℤ \land N \in ℤ) \land (M \neq 0 \land N \neq 0)) \land k \in (1 \dots \|M \cdot N\|)) \land k \in ℙ) \to k \in ℤ$
52		lgscl	$⊢ (A \in ℤ \land k \in ℤ) \to A /_{L} k \in ℤ$
53	49 51 52	syl2anc	$⊢ ((((A \in ℤ \land M \in ℤ \land N \in ℤ) \land (M \neq 0 \land N \neq 0)) \land k \in (1 \dots \|M \cdot N\|)) \land k \in ℙ) \to A /_{L} k \in ℤ$
54	53	zcnd	$⊢ ((((A \in ℤ \land M \in ℤ \land N \in ℤ) \land (M \neq 0 \land N \neq 0)) \land k \in (1 \dots \|M \cdot N\|)) \land k \in ℙ) \to A /_{L} k \in ℂ$
55		pczcl	$⊢ (k \in ℙ \land (N \in ℤ \land N \neq 0)) \to k pCnt N \in ℕ_{0}$
56	41 44 45 55	syl12anc	$⊢ ((((A \in ℤ \land M \in ℤ \land N \in ℤ) \land (M \neq 0 \land N \neq 0)) \land k \in (1 \dots \|M \cdot N\|)) \land k \in ℙ) \to k pCnt N \in ℕ_{0}$
57		pczcl	$⊢ (k \in ℙ \land (M \in ℤ \land M \neq 0)) \to k pCnt M \in ℕ_{0}$
58	41 42 43 57	syl12anc	$⊢ ((((A \in ℤ \land M \in ℤ \land N \in ℤ) \land (M \neq 0 \land N \neq 0)) \land k \in (1 \dots \|M \cdot N\|)) \land k \in ℙ) \to k pCnt M \in ℕ_{0}$
59	54 56 58	expaddd	$⊢ ((((A \in ℤ \land M \in ℤ \land N \in ℤ) \land (M \neq 0 \land N \neq 0)) \land k \in (1 \dots \|M \cdot N\|)) \land k \in ℙ) \to {(A /_{L} k)}^{(k pCnt M) + (k pCnt N)} = {(A /_{L} k)}^{k pCnt M} {(A /_{L} k)}^{k pCnt N}$
60	48 59	eqtrd	$⊢ ((((A \in ℤ \land M \in ℤ \land N \in ℤ) \land (M \neq 0 \land N \neq 0)) \land k \in (1 \dots \|M \cdot N\|)) \land k \in ℙ) \to {(A /_{L} k)}^{k pCnt M \cdot N} = {(A /_{L} k)}^{k pCnt M} {(A /_{L} k)}^{k pCnt N}$
61		iftrue	$⊢ k \in ℙ \to if (k \in ℙ, {(A /_{L} k)}^{k pCnt M \cdot N}, 1) = {(A /_{L} k)}^{k pCnt M \cdot N}$
62	61	adantl	$⊢ ((((A \in ℤ \land M \in ℤ \land N \in ℤ) \land (M \neq 0 \land N \neq 0)) \land k \in (1 \dots \|M \cdot N\|)) \land k \in ℙ) \to if (k \in ℙ, {(A /_{L} k)}^{k pCnt M \cdot N}, 1) = {(A /_{L} k)}^{k pCnt M \cdot N}$
63		iftrue	$⊢ k \in ℙ \to if (k \in ℙ, {(A /_{L} k)}^{k pCnt M}, 1) = {(A /_{L} k)}^{k pCnt M}$
64		iftrue	$⊢ k \in ℙ \to if (k \in ℙ, {(A /_{L} k)}^{k pCnt N}, 1) = {(A /_{L} k)}^{k pCnt N}$
65	63 64	oveq12d	$⊢ k \in ℙ \to if (k \in ℙ, {(A /_{L} k)}^{k pCnt M}, 1) if (k \in ℙ, {(A /_{L} k)}^{k pCnt N}, 1) = {(A /_{L} k)}^{k pCnt M} {(A /_{L} k)}^{k pCnt N}$
66	65	adantl	$⊢ ((((A \in ℤ \land M \in ℤ \land N \in ℤ) \land (M \neq 0 \land N \neq 0)) \land k \in (1 \dots \|M \cdot N\|)) \land k \in ℙ) \to if (k \in ℙ, {(A /_{L} k)}^{k pCnt M}, 1) if (k \in ℙ, {(A /_{L} k)}^{k pCnt N}, 1) = {(A /_{L} k)}^{k pCnt M} {(A /_{L} k)}^{k pCnt N}$
67	60 62 66	3eqtr4rd	$⊢ ((((A \in ℤ \land M \in ℤ \land N \in ℤ) \land (M \neq 0 \land N \neq 0)) \land k \in (1 \dots \|M \cdot N\|)) \land k \in ℙ) \to if (k \in ℙ, {(A /_{L} k)}^{k pCnt M}, 1) if (k \in ℙ, {(A /_{L} k)}^{k pCnt N}, 1) = if (k \in ℙ, {(A /_{L} k)}^{k pCnt M \cdot N}, 1)$
68		1t1e1	$⊢ 1 \cdot 1 = 1$
69		iffalse	$⊢ \neg k \in ℙ \to if (k \in ℙ, {(A /_{L} k)}^{k pCnt M}, 1) = 1$
70		iffalse	$⊢ \neg k \in ℙ \to if (k \in ℙ, {(A /_{L} k)}^{k pCnt N}, 1) = 1$
71	69 70	oveq12d	$⊢ \neg k \in ℙ \to if (k \in ℙ, {(A /_{L} k)}^{k pCnt M}, 1) if (k \in ℙ, {(A /_{L} k)}^{k pCnt N}, 1) = 1 \cdot 1$
72		iffalse	$⊢ \neg k \in ℙ \to if (k \in ℙ, {(A /_{L} k)}^{k pCnt M \cdot N}, 1) = 1$
73	68 71 72	3eqtr4a	$⊢ \neg k \in ℙ \to if (k \in ℙ, {(A /_{L} k)}^{k pCnt M}, 1) if (k \in ℙ, {(A /_{L} k)}^{k pCnt N}, 1) = if (k \in ℙ, {(A /_{L} k)}^{k pCnt M \cdot N}, 1)$
74	73	adantl	$⊢ ((((A \in ℤ \land M \in ℤ \land N \in ℤ) \land (M \neq 0 \land N \neq 0)) \land k \in (1 \dots \|M \cdot N\|)) \land \neg k \in ℙ) \to if (k \in ℙ, {(A /_{L} k)}^{k pCnt M}, 1) if (k \in ℙ, {(A /_{L} k)}^{k pCnt N}, 1) = if (k \in ℙ, {(A /_{L} k)}^{k pCnt M \cdot N}, 1)$
75	67 74	pm2.61dan	$⊢ (((A \in ℤ \land M \in ℤ \land N \in ℤ) \land (M \neq 0 \land N \neq 0)) \land k \in (1 \dots \|M \cdot N\|)) \to if (k \in ℙ, {(A /_{L} k)}^{k pCnt M}, 1) if (k \in ℙ, {(A /_{L} k)}^{k pCnt N}, 1) = if (k \in ℙ, {(A /_{L} k)}^{k pCnt M \cdot N}, 1)$
76	31	adantl	$⊢ (((A \in ℤ \land M \in ℤ \land N \in ℤ) \land (M \neq 0 \land N \neq 0)) \land k \in (1 \dots \|M \cdot N\|)) \to k \in ℕ$
77		eleq1w	$⊢ n = k \to (n \in ℙ \leftrightarrow k \in ℙ)$
78		oveq2	$⊢ n = k \to A /_{L} n = A /_{L} k$
79		oveq1	$⊢ n = k \to n pCnt M = k pCnt M$
80	78 79	oveq12d	$⊢ n = k \to {(A /_{L} n)}^{n pCnt M} = {(A /_{L} k)}^{k pCnt M}$
81	77 80	ifbieq1d	$⊢ n = k \to if (n \in ℙ, {(A /_{L} n)}^{n pCnt M}, 1) = if (k \in ℙ, {(A /_{L} k)}^{k pCnt M}, 1)$
82		ovex	$⊢ {(A /_{L} k)}^{k pCnt M} \in V$
83		1ex	$⊢ 1 \in V$
84	82 83	ifex	$⊢ if (k \in ℙ, {(A /_{L} k)}^{k pCnt M}, 1) \in V$
85	81 28 84	fvmpt	$⊢ k \in ℕ \to (n \in ℕ ⟼ if (n \in ℙ, {(A /_{L} n)}^{n pCnt M}, 1)) (k) = if (k \in ℙ, {(A /_{L} k)}^{k pCnt M}, 1)$
86		oveq1	$⊢ n = k \to n pCnt N = k pCnt N$
87	78 86	oveq12d	$⊢ n = k \to {(A /_{L} n)}^{n pCnt N} = {(A /_{L} k)}^{k pCnt N}$
88	77 87	ifbieq1d	$⊢ n = k \to if (n \in ℙ, {(A /_{L} n)}^{n pCnt N}, 1) = if (k \in ℙ, {(A /_{L} k)}^{k pCnt N}, 1)$
89		ovex	$⊢ {(A /_{L} k)}^{k pCnt N} \in V$
90	89 83	ifex	$⊢ if (k \in ℙ, {(A /_{L} k)}^{k pCnt N}, 1) \in V$
91	88 35 90	fvmpt	$⊢ k \in ℕ \to (n \in ℕ ⟼ if (n \in ℙ, {(A /_{L} n)}^{n pCnt N}, 1)) (k) = if (k \in ℙ, {(A /_{L} k)}^{k pCnt N}, 1)$
92	85 91	oveq12d	$⊢ k \in ℕ \to (n \in ℕ ⟼ if (n \in ℙ, {(A /_{L} n)}^{n pCnt M}, 1)) (k) (n \in ℕ ⟼ if (n \in ℙ, {(A /_{L} n)}^{n pCnt N}, 1)) (k) = if (k \in ℙ, {(A /_{L} k)}^{k pCnt M}, 1) if (k \in ℙ, {(A /_{L} k)}^{k pCnt N}, 1)$
93	76 92	syl	$⊢ (((A \in ℤ \land M \in ℤ \land N \in ℤ) \land (M \neq 0 \land N \neq 0)) \land k \in (1 \dots \|M \cdot N\|)) \to (n \in ℕ ⟼ if (n \in ℙ, {(A /_{L} n)}^{n pCnt M}, 1)) (k) (n \in ℕ ⟼ if (n \in ℙ, {(A /_{L} n)}^{n pCnt N}, 1)) (k) = if (k \in ℙ, {(A /_{L} k)}^{k pCnt M}, 1) if (k \in ℙ, {(A /_{L} k)}^{k pCnt N}, 1)$
94		oveq1	$⊢ n = k \to n pCnt M \cdot N = k pCnt M \cdot N$
95	78 94	oveq12d	$⊢ n = k \to {(A /_{L} n)}^{n pCnt M \cdot N} = {(A /_{L} k)}^{k pCnt M \cdot N}$
96	77 95	ifbieq1d	$⊢ n = k \to if (n \in ℙ, {(A /_{L} n)}^{n pCnt M \cdot N}, 1) = if (k \in ℙ, {(A /_{L} k)}^{k pCnt M \cdot N}, 1)$
97		eqid	$⊢ (n \in ℕ ⟼ if (n \in ℙ, {(A /_{L} n)}^{n pCnt M \cdot N}, 1)) = (n \in ℕ ⟼ if (n \in ℙ, {(A /_{L} n)}^{n pCnt M \cdot N}, 1))$
98		ovex	$⊢ {(A /_{L} k)}^{k pCnt M \cdot N} \in V$
99	98 83	ifex	$⊢ if (k \in ℙ, {(A /_{L} k)}^{k pCnt M \cdot N}, 1) \in V$
100	96 97 99	fvmpt	$⊢ k \in ℕ \to (n \in ℕ ⟼ if (n \in ℙ, {(A /_{L} n)}^{n pCnt M \cdot N}, 1)) (k) = if (k \in ℙ, {(A /_{L} k)}^{k pCnt M \cdot N}, 1)$
101	76 100	syl	$⊢ (((A \in ℤ \land M \in ℤ \land N \in ℤ) \land (M \neq 0 \land N \neq 0)) \land k \in (1 \dots \|M \cdot N\|)) \to (n \in ℕ ⟼ if (n \in ℙ, {(A /_{L} n)}^{n pCnt M \cdot N}, 1)) (k) = if (k \in ℙ, {(A /_{L} k)}^{k pCnt M \cdot N}, 1)$
102	75 93 101	3eqtr4rd	$⊢ (((A \in ℤ \land M \in ℤ \land N \in ℤ) \land (M \neq 0 \land N \neq 0)) \land k \in (1 \dots \|M \cdot N\|)) \to (n \in ℕ ⟼ if (n \in ℙ, {(A /_{L} n)}^{n pCnt M \cdot N}, 1)) (k) = (n \in ℕ ⟼ if (n \in ℙ, {(A /_{L} n)}^{n pCnt M}, 1)) (k) (n \in ℕ ⟼ if (n \in ℙ, {(A /_{L} n)}^{n pCnt N}, 1)) (k)$
103	26 34 40 102	prodfmul	$⊢ ((A \in ℤ \land M \in ℤ \land N \in ℤ) \land (M \neq 0 \land N \neq 0)) \to seq 1 (\times (n \in ℕ ⟼ if (n \in ℙ, {(A /_{L} n)}^{n pCnt M \cdot N}, 1))) (\|M \cdot N\|) = seq 1 (\times (n \in ℕ ⟼ if (n \in ℙ, {(A /_{L} n)}^{n pCnt M}, 1))) (\|M \cdot N\|) seq 1 (\times (n \in ℕ ⟼ if (n \in ℙ, {(A /_{L} n)}^{n pCnt N}, 1))) (\|M \cdot N\|)$
104	27 15 16 20 21 28	lgsdilem2	$⊢ ((A \in ℤ \land M \in ℤ \land N \in ℤ) \land (M \neq 0 \land N \neq 0)) \to seq 1 (\times (n \in ℕ ⟼ if (n \in ℙ, {(A /_{L} n)}^{n pCnt M}, 1))) (\|M\|) = seq 1 (\times (n \in ℕ ⟼ if (n \in ℙ, {(A /_{L} n)}^{n pCnt M}, 1))) (\|M \cdot N\|)$
105	27 16 15 21 20 35	lgsdilem2	$⊢ ((A \in ℤ \land M \in ℤ \land N \in ℤ) \land (M \neq 0 \land N \neq 0)) \to seq 1 (\times (n \in ℕ ⟼ if (n \in ℙ, {(A /_{L} n)}^{n pCnt N}, 1))) (\|N\|) = seq 1 (\times (n \in ℕ ⟼ if (n \in ℙ, {(A /_{L} n)}^{n pCnt N}, 1))) (\|N \cdot M\|)$
106	18 19	mulcomd	$⊢ ((A \in ℤ \land M \in ℤ \land N \in ℤ) \land (M \neq 0 \land N \neq 0)) \to M \cdot N = N \cdot M$
107	106	fveq2d	$⊢ ((A \in ℤ \land M \in ℤ \land N \in ℤ) \land (M \neq 0 \land N \neq 0)) \to \|M \cdot N\| = \|N \cdot M\|$
108	107	fveq2d	$⊢ ((A \in ℤ \land M \in ℤ \land N \in ℤ) \land (M \neq 0 \land N \neq 0)) \to seq 1 (\times (n \in ℕ ⟼ if (n \in ℙ, {(A /_{L} n)}^{n pCnt N}, 1))) (\|M \cdot N\|) = seq 1 (\times (n \in ℕ ⟼ if (n \in ℙ, {(A /_{L} n)}^{n pCnt N}, 1))) (\|N \cdot M\|)$
109	105 108	eqtr4d	$⊢ ((A \in ℤ \land M \in ℤ \land N \in ℤ) \land (M \neq 0 \land N \neq 0)) \to seq 1 (\times (n \in ℕ ⟼ if (n \in ℙ, {(A /_{L} n)}^{n pCnt N}, 1))) (\|N\|) = seq 1 (\times (n \in ℕ ⟼ if (n \in ℙ, {(A /_{L} n)}^{n pCnt N}, 1))) (\|M \cdot N\|)$
110	104 109	oveq12d	$⊢ ((A \in ℤ \land M \in ℤ \land N \in ℤ) \land (M \neq 0 \land N \neq 0)) \to seq 1 (\times (n \in ℕ ⟼ if (n \in ℙ, {(A /_{L} n)}^{n pCnt M}, 1))) (\|M\|) seq 1 (\times (n \in ℕ ⟼ if (n \in ℙ, {(A /_{L} n)}^{n pCnt N}, 1))) (\|N\|) = seq 1 (\times (n \in ℕ ⟼ if (n \in ℙ, {(A /_{L} n)}^{n pCnt M}, 1))) (\|M \cdot N\|) seq 1 (\times (n \in ℕ ⟼ if (n \in ℙ, {(A /_{L} n)}^{n pCnt N}, 1))) (\|M \cdot N\|)$
111	103 110	eqtr4d	$⊢ ((A \in ℤ \land M \in ℤ \land N \in ℤ) \land (M \neq 0 \land N \neq 0)) \to seq 1 (\times (n \in ℕ ⟼ if (n \in ℙ, {(A /_{L} n)}^{n pCnt M \cdot N}, 1))) (\|M \cdot N\|) = seq 1 (\times (n \in ℕ ⟼ if (n \in ℙ, {(A /_{L} n)}^{n pCnt M}, 1))) (\|M\|) seq 1 (\times (n \in ℕ ⟼ if (n \in ℙ, {(A /_{L} n)}^{n pCnt N}, 1))) (\|N\|)$
112	14 111	oveq12d	$⊢ ((A \in ℤ \land M \in ℤ \land N \in ℤ) \land (M \neq 0 \land N \neq 0)) \to if ((M \cdot N < 0 \land A < 0), - 1, 1) seq 1 (\times (n \in ℕ ⟼ if (n \in ℙ, {(A /_{L} n)}^{n pCnt M \cdot N}, 1))) (\|M \cdot N\|) = if ((M < 0 \land A < 0), - 1, 1) if ((N < 0 \land A < 0), - 1, 1) seq 1 (\times (n \in ℕ ⟼ if (n \in ℙ, {(A /_{L} n)}^{n pCnt M}, 1))) (\|M\|) seq 1 (\times (n \in ℕ ⟼ if (n \in ℙ, {(A /_{L} n)}^{n pCnt N}, 1))) (\|N\|)$
113	97	lgsval4	$⊢ (A \in ℤ \land M \cdot N \in ℤ \land M \cdot N \neq 0) \to A /_{L} M \cdot N = if ((M \cdot N < 0 \land A < 0), - 1, 1) seq 1 (\times (n \in ℕ ⟼ if (n \in ℙ, {(A /_{L} n)}^{n pCnt M \cdot N}, 1))) (\|M \cdot N\|)$
114	27 17 22 113	syl3anc	$⊢ ((A \in ℤ \land M \in ℤ \land N \in ℤ) \land (M \neq 0 \land N \neq 0)) \to A /_{L} M \cdot N = if ((M \cdot N < 0 \land A < 0), - 1, 1) seq 1 (\times (n \in ℕ ⟼ if (n \in ℙ, {(A /_{L} n)}^{n pCnt M \cdot N}, 1))) (\|M \cdot N\|)$
115	28	lgsval4	$⊢ (A \in ℤ \land M \in ℤ \land M \neq 0) \to A /_{L} M = if ((M < 0 \land A < 0), - 1, 1) seq 1 (\times (n \in ℕ ⟼ if (n \in ℙ, {(A /_{L} n)}^{n pCnt M}, 1))) (\|M\|)$
116	27 15 20 115	syl3anc	$⊢ ((A \in ℤ \land M \in ℤ \land N \in ℤ) \land (M \neq 0 \land N \neq 0)) \to A /_{L} M = if ((M < 0 \land A < 0), - 1, 1) seq 1 (\times (n \in ℕ ⟼ if (n \in ℙ, {(A /_{L} n)}^{n pCnt M}, 1))) (\|M\|)$
117	35	lgsval4	$⊢ (A \in ℤ \land N \in ℤ \land N \neq 0) \to A /_{L} N = if ((N < 0 \land A < 0), - 1, 1) seq 1 (\times (n \in ℕ ⟼ if (n \in ℙ, {(A /_{L} n)}^{n pCnt N}, 1))) (\|N\|)$
118	27 16 21 117	syl3anc	$⊢ ((A \in ℤ \land M \in ℤ \land N \in ℤ) \land (M \neq 0 \land N \neq 0)) \to A /_{L} N = if ((N < 0 \land A < 0), - 1, 1) seq 1 (\times (n \in ℕ ⟼ if (n \in ℙ, {(A /_{L} n)}^{n pCnt N}, 1))) (\|N\|)$
119	116 118	oveq12d	$⊢ ((A \in ℤ \land M \in ℤ \land N \in ℤ) \land (M \neq 0 \land N \neq 0)) \to (A /_{L} M) (A /_{L} N) = if ((M < 0 \land A < 0), - 1, 1) seq 1 (\times (n \in ℕ ⟼ if (n \in ℙ, {(A /_{L} n)}^{n pCnt M}, 1))) (\|M\|) if ((N < 0 \land A < 0), - 1, 1) seq 1 (\times (n \in ℕ ⟼ if (n \in ℙ, {(A /_{L} n)}^{n pCnt N}, 1))) (\|N\|)$
120		neg1cn	$⊢ - 1 \in ℂ$
121		ax-1cn	$⊢ 1 \in ℂ$
122	120 121	ifcli	$⊢ if ((M < 0 \land A < 0), - 1, 1) \in ℂ$
123	122	a1i	$⊢ ((A \in ℤ \land M \in ℤ \land N \in ℤ) \land (M \neq 0 \land N \neq 0)) \to if ((M < 0 \land A < 0), - 1, 1) \in ℂ$
124		nnabscl	$⊢ (M \in ℤ \land M \neq 0) \to \|M\| \in ℕ$
125	15 20 124	syl2anc	$⊢ ((A \in ℤ \land M \in ℤ \land N \in ℤ) \land (M \neq 0 \land N \neq 0)) \to \|M\| \in ℕ$
126	125 25	eleqtrdi	$⊢ ((A \in ℤ \land M \in ℤ \land N \in ℤ) \land (M \neq 0 \land N \neq 0)) \to \|M\| \in ℤ_{\geq 1}$
127		elfznn	$⊢ k \in (1 \dots \|M\|) \to k \in ℕ$
128	30 127 32	syl2an	$⊢ (((A \in ℤ \land M \in ℤ \land N \in ℤ) \land (M \neq 0 \land N \neq 0)) \land k \in (1 \dots \|M\|)) \to (n \in ℕ ⟼ if (n \in ℙ, {(A /_{L} n)}^{n pCnt M}, 1)) (k) \in ℤ$
129	128	zcnd	$⊢ (((A \in ℤ \land M \in ℤ \land N \in ℤ) \land (M \neq 0 \land N \neq 0)) \land k \in (1 \dots \|M\|)) \to (n \in ℕ ⟼ if (n \in ℙ, {(A /_{L} n)}^{n pCnt M}, 1)) (k) \in ℂ$
130		mulcl	$⊢ (k \in ℂ \land x \in ℂ) \to k x \in ℂ$
131	130	adantl	$⊢ (((A \in ℤ \land M \in ℤ \land N \in ℤ) \land (M \neq 0 \land N \neq 0)) \land (k \in ℂ \land x \in ℂ)) \to k x \in ℂ$
132	126 129 131	seqcl	$⊢ ((A \in ℤ \land M \in ℤ \land N \in ℤ) \land (M \neq 0 \land N \neq 0)) \to seq 1 (\times (n \in ℕ ⟼ if (n \in ℙ, {(A /_{L} n)}^{n pCnt M}, 1))) (\|M\|) \in ℂ$
133	120 121	ifcli	$⊢ if ((N < 0 \land A < 0), - 1, 1) \in ℂ$
134	133	a1i	$⊢ ((A \in ℤ \land M \in ℤ \land N \in ℤ) \land (M \neq 0 \land N \neq 0)) \to if ((N < 0 \land A < 0), - 1, 1) \in ℂ$
135		nnabscl	$⊢ (N \in ℤ \land N \neq 0) \to \|N\| \in ℕ$
136	16 21 135	syl2anc	$⊢ ((A \in ℤ \land M \in ℤ \land N \in ℤ) \land (M \neq 0 \land N \neq 0)) \to \|N\| \in ℕ$
137	136 25	eleqtrdi	$⊢ ((A \in ℤ \land M \in ℤ \land N \in ℤ) \land (M \neq 0 \land N \neq 0)) \to \|N\| \in ℤ_{\geq 1}$
138		elfznn	$⊢ k \in (1 \dots \|N\|) \to k \in ℕ$
139	37 138 38	syl2an	$⊢ (((A \in ℤ \land M \in ℤ \land N \in ℤ) \land (M \neq 0 \land N \neq 0)) \land k \in (1 \dots \|N\|)) \to (n \in ℕ ⟼ if (n \in ℙ, {(A /_{L} n)}^{n pCnt N}, 1)) (k) \in ℤ$
140	139	zcnd	$⊢ (((A \in ℤ \land M \in ℤ \land N \in ℤ) \land (M \neq 0 \land N \neq 0)) \land k \in (1 \dots \|N\|)) \to (n \in ℕ ⟼ if (n \in ℙ, {(A /_{L} n)}^{n pCnt N}, 1)) (k) \in ℂ$
141	137 140 131	seqcl	$⊢ ((A \in ℤ \land M \in ℤ \land N \in ℤ) \land (M \neq 0 \land N \neq 0)) \to seq 1 (\times (n \in ℕ ⟼ if (n \in ℙ, {(A /_{L} n)}^{n pCnt N}, 1))) (\|N\|) \in ℂ$
142	123 132 134 141	mul4d	$⊢ ((A \in ℤ \land M \in ℤ \land N \in ℤ) \land (M \neq 0 \land N \neq 0)) \to if ((M < 0 \land A < 0), - 1, 1) seq 1 (\times (n \in ℕ ⟼ if (n \in ℙ, {(A /_{L} n)}^{n pCnt M}, 1))) (\|M\|) if ((N < 0 \land A < 0), - 1, 1) seq 1 (\times (n \in ℕ ⟼ if (n \in ℙ, {(A /_{L} n)}^{n pCnt N}, 1))) (\|N\|) = if ((M < 0 \land A < 0), - 1, 1) if ((N < 0 \land A < 0), - 1, 1) seq 1 (\times (n \in ℕ ⟼ if (n \in ℙ, {(A /_{L} n)}^{n pCnt M}, 1))) (\|M\|) seq 1 (\times (n \in ℕ ⟼ if (n \in ℙ, {(A /_{L} n)}^{n pCnt N}, 1))) (\|N\|)$
143	119 142	eqtrd	$⊢ ((A \in ℤ \land M \in ℤ \land N \in ℤ) \land (M \neq 0 \land N \neq 0)) \to (A /_{L} M) (A /_{L} N) = if ((M < 0 \land A < 0), - 1, 1) if ((N < 0 \land A < 0), - 1, 1) seq 1 (\times (n \in ℕ ⟼ if (n \in ℙ, {(A /_{L} n)}^{n pCnt M}, 1))) (\|M\|) seq 1 (\times (n \in ℕ ⟼ if (n \in ℙ, {(A /_{L} n)}^{n pCnt N}, 1))) (\|N\|)$
144	112 114 143	3eqtr4d	$⊢ ((A \in ℤ \land M \in ℤ \land N \in ℤ) \land (M \neq 0 \land N \neq 0)) \to A /_{L} M \cdot N = (A /_{L} M) (A /_{L} N)$

Metamath Proof Explorer

Theorem lgsdi

Proof