lgsdir

Description: The Legendre symbol is completely multiplicative in its left argument. Generalization of theorem 9.9(a) in ApostolNT p. 188 (which assumes that A and B are odd positive integers). Together with lgsqr this implies that the product of two quadratic residues or nonresidues is a residue, and the product of a residue and a nonresidue is a nonresidue. (Contributed by Mario Carneiro, 4-Feb-2015)

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

Proof

Step	Hyp	Ref	Expression
1		ax-1cn	$⊢ 1 \in ℂ$
2		0cn	$⊢ 0 \in ℂ$
3	1 2	ifcli	$⊢ if (B^{2} = 1, 1, 0) \in ℂ$
4	3	mullidi	$⊢ 1 if (B^{2} = 1, 1, 0) = if (B^{2} = 1, 1, 0)$
5		iftrue	$⊢ A^{2} = 1 \to if (A^{2} = 1, 1, 0) = 1$
6	5	adantl	$⊢ ((((A \in ℤ \land B \in ℤ \land N \in ℤ) \land (A \neq 0 \land B \neq 0)) \land N = 0) \land A^{2} = 1) \to if (A^{2} = 1, 1, 0) = 1$
7	6	oveq1d	$⊢ ((((A \in ℤ \land B \in ℤ \land N \in ℤ) \land (A \neq 0 \land B \neq 0)) \land N = 0) \land A^{2} = 1) \to if (A^{2} = 1, 1, 0) if (B^{2} = 1, 1, 0) = 1 if (B^{2} = 1, 1, 0)$
8		simpl1	$⊢ ((A \in ℤ \land B \in ℤ \land N \in ℤ) \land (A \neq 0 \land B \neq 0)) \to A \in ℤ$
9	8	zcnd	$⊢ ((A \in ℤ \land B \in ℤ \land N \in ℤ) \land (A \neq 0 \land B \neq 0)) \to A \in ℂ$
10	9	ad2antrr	$⊢ ((((A \in ℤ \land B \in ℤ \land N \in ℤ) \land (A \neq 0 \land B \neq 0)) \land N = 0) \land A^{2} = 1) \to A \in ℂ$
11		simpl2	$⊢ ((A \in ℤ \land B \in ℤ \land N \in ℤ) \land (A \neq 0 \land B \neq 0)) \to B \in ℤ$
12	11	zcnd	$⊢ ((A \in ℤ \land B \in ℤ \land N \in ℤ) \land (A \neq 0 \land B \neq 0)) \to B \in ℂ$
13	12	ad2antrr	$⊢ ((((A \in ℤ \land B \in ℤ \land N \in ℤ) \land (A \neq 0 \land B \neq 0)) \land N = 0) \land A^{2} = 1) \to B \in ℂ$
14	10 13	sqmuld	$⊢ ((((A \in ℤ \land B \in ℤ \land N \in ℤ) \land (A \neq 0 \land B \neq 0)) \land N = 0) \land A^{2} = 1) \to {A B}^{2} = A^{2} B^{2}$
15		simpr	$⊢ ((((A \in ℤ \land B \in ℤ \land N \in ℤ) \land (A \neq 0 \land B \neq 0)) \land N = 0) \land A^{2} = 1) \to A^{2} = 1$
16	15	oveq1d	$⊢ ((((A \in ℤ \land B \in ℤ \land N \in ℤ) \land (A \neq 0 \land B \neq 0)) \land N = 0) \land A^{2} = 1) \to A^{2} B^{2} = 1 B^{2}$
17	12	sqcld	$⊢ ((A \in ℤ \land B \in ℤ \land N \in ℤ) \land (A \neq 0 \land B \neq 0)) \to B^{2} \in ℂ$
18	17	ad2antrr	$⊢ ((((A \in ℤ \land B \in ℤ \land N \in ℤ) \land (A \neq 0 \land B \neq 0)) \land N = 0) \land A^{2} = 1) \to B^{2} \in ℂ$
19	18	mullidd	$⊢ ((((A \in ℤ \land B \in ℤ \land N \in ℤ) \land (A \neq 0 \land B \neq 0)) \land N = 0) \land A^{2} = 1) \to 1 B^{2} = B^{2}$
20	14 16 19	3eqtrd	$⊢ ((((A \in ℤ \land B \in ℤ \land N \in ℤ) \land (A \neq 0 \land B \neq 0)) \land N = 0) \land A^{2} = 1) \to {A B}^{2} = B^{2}$
21	20	eqeq1d	$⊢ ((((A \in ℤ \land B \in ℤ \land N \in ℤ) \land (A \neq 0 \land B \neq 0)) \land N = 0) \land A^{2} = 1) \to ({A B}^{2} = 1 \leftrightarrow B^{2} = 1)$
22	21	ifbid	$⊢ ((((A \in ℤ \land B \in ℤ \land N \in ℤ) \land (A \neq 0 \land B \neq 0)) \land N = 0) \land A^{2} = 1) \to if ({A B}^{2} = 1, 1, 0) = if (B^{2} = 1, 1, 0)$
23	4 7 22	3eqtr4a	$⊢ ((((A \in ℤ \land B \in ℤ \land N \in ℤ) \land (A \neq 0 \land B \neq 0)) \land N = 0) \land A^{2} = 1) \to if (A^{2} = 1, 1, 0) if (B^{2} = 1, 1, 0) = if ({A B}^{2} = 1, 1, 0)$
24	3	mul02i	$⊢ 0 \cdot if (B^{2} = 1, 1, 0) = 0$
25		iffalse	$⊢ \neg A^{2} = 1 \to if (A^{2} = 1, 1, 0) = 0$
26	25	adantl	$⊢ ((((A \in ℤ \land B \in ℤ \land N \in ℤ) \land (A \neq 0 \land B \neq 0)) \land N = 0) \land \neg A^{2} = 1) \to if (A^{2} = 1, 1, 0) = 0$
27	26	oveq1d	$⊢ ((((A \in ℤ \land B \in ℤ \land N \in ℤ) \land (A \neq 0 \land B \neq 0)) \land N = 0) \land \neg A^{2} = 1) \to if (A^{2} = 1, 1, 0) if (B^{2} = 1, 1, 0) = 0 \cdot if (B^{2} = 1, 1, 0)$
28		dvdsmul1	$⊢ (A \in ℤ \land B \in ℤ) \to A ∥ A B$
29	8 11 28	syl2anc	$⊢ ((A \in ℤ \land B \in ℤ \land N \in ℤ) \land (A \neq 0 \land B \neq 0)) \to A ∥ A B$
30	8 11	zmulcld	$⊢ ((A \in ℤ \land B \in ℤ \land N \in ℤ) \land (A \neq 0 \land B \neq 0)) \to A B \in ℤ$
31		dvdssq	$⊢ (A \in ℤ \land A B \in ℤ) \to (A ∥ A B \leftrightarrow A^{2} ∥ {A B}^{2})$
32	8 30 31	syl2anc	$⊢ ((A \in ℤ \land B \in ℤ \land N \in ℤ) \land (A \neq 0 \land B \neq 0)) \to (A ∥ A B \leftrightarrow A^{2} ∥ {A B}^{2})$
33	29 32	mpbid	$⊢ ((A \in ℤ \land B \in ℤ \land N \in ℤ) \land (A \neq 0 \land B \neq 0)) \to A^{2} ∥ {A B}^{2}$
34	33	adantr	$⊢ (((A \in ℤ \land B \in ℤ \land N \in ℤ) \land (A \neq 0 \land B \neq 0)) \land N = 0) \to A^{2} ∥ {A B}^{2}$
35		breq2	$⊢ {A B}^{2} = 1 \to (A^{2} ∥ {A B}^{2} \leftrightarrow A^{2} ∥ 1)$
36	34 35	syl5ibcom	$⊢ (((A \in ℤ \land B \in ℤ \land N \in ℤ) \land (A \neq 0 \land B \neq 0)) \land N = 0) \to ({A B}^{2} = 1 \to A^{2} ∥ 1)$
37		simprl	$⊢ ((A \in ℤ \land B \in ℤ \land N \in ℤ) \land (A \neq 0 \land B \neq 0)) \to A \neq 0$
38	37	neneqd	$⊢ ((A \in ℤ \land B \in ℤ \land N \in ℤ) \land (A \neq 0 \land B \neq 0)) \to \neg A = 0$
39		sqeq0	$⊢ A \in ℂ \to (A^{2} = 0 \leftrightarrow A = 0)$
40	9 39	syl	$⊢ ((A \in ℤ \land B \in ℤ \land N \in ℤ) \land (A \neq 0 \land B \neq 0)) \to (A^{2} = 0 \leftrightarrow A = 0)$
41	38 40	mtbird	$⊢ ((A \in ℤ \land B \in ℤ \land N \in ℤ) \land (A \neq 0 \land B \neq 0)) \to \neg A^{2} = 0$
42		zsqcl2	$⊢ A \in ℤ \to A^{2} \in ℕ_{0}$
43	8 42	syl	$⊢ ((A \in ℤ \land B \in ℤ \land N \in ℤ) \land (A \neq 0 \land B \neq 0)) \to A^{2} \in ℕ_{0}$
44		elnn0	$⊢ A^{2} \in ℕ_{0} \leftrightarrow (A^{2} \in ℕ \lor A^{2} = 0)$
45	43 44	sylib	$⊢ ((A \in ℤ \land B \in ℤ \land N \in ℤ) \land (A \neq 0 \land B \neq 0)) \to (A^{2} \in ℕ \lor A^{2} = 0)$
46	45	ord	$⊢ ((A \in ℤ \land B \in ℤ \land N \in ℤ) \land (A \neq 0 \land B \neq 0)) \to (\neg A^{2} \in ℕ \to A^{2} = 0)$
47	41 46	mt3d	$⊢ ((A \in ℤ \land B \in ℤ \land N \in ℤ) \land (A \neq 0 \land B \neq 0)) \to A^{2} \in ℕ$
48	47	adantr	$⊢ (((A \in ℤ \land B \in ℤ \land N \in ℤ) \land (A \neq 0 \land B \neq 0)) \land N = 0) \to A^{2} \in ℕ$
49	48	nnzd	$⊢ (((A \in ℤ \land B \in ℤ \land N \in ℤ) \land (A \neq 0 \land B \neq 0)) \land N = 0) \to A^{2} \in ℤ$
50		1nn	$⊢ 1 \in ℕ$
51		dvdsle	$⊢ (A^{2} \in ℤ \land 1 \in ℕ) \to (A^{2} ∥ 1 \to A^{2} \leq 1)$
52	49 50 51	sylancl	$⊢ (((A \in ℤ \land B \in ℤ \land N \in ℤ) \land (A \neq 0 \land B \neq 0)) \land N = 0) \to (A^{2} ∥ 1 \to A^{2} \leq 1)$
53	48	nnge1d	$⊢ (((A \in ℤ \land B \in ℤ \land N \in ℤ) \land (A \neq 0 \land B \neq 0)) \land N = 0) \to 1 \leq A^{2}$
54	52 53	jctird	$⊢ (((A \in ℤ \land B \in ℤ \land N \in ℤ) \land (A \neq 0 \land B \neq 0)) \land N = 0) \to (A^{2} ∥ 1 \to (A^{2} \leq 1 \land 1 \leq A^{2}))$
55	48	nnred	$⊢ (((A \in ℤ \land B \in ℤ \land N \in ℤ) \land (A \neq 0 \land B \neq 0)) \land N = 0) \to A^{2} \in ℝ$
56		1re	$⊢ 1 \in ℝ$
57		letri3	$⊢ (A^{2} \in ℝ \land 1 \in ℝ) \to (A^{2} = 1 \leftrightarrow (A^{2} \leq 1 \land 1 \leq A^{2}))$
58	55 56 57	sylancl	$⊢ (((A \in ℤ \land B \in ℤ \land N \in ℤ) \land (A \neq 0 \land B \neq 0)) \land N = 0) \to (A^{2} = 1 \leftrightarrow (A^{2} \leq 1 \land 1 \leq A^{2}))$
59	54 58	sylibrd	$⊢ (((A \in ℤ \land B \in ℤ \land N \in ℤ) \land (A \neq 0 \land B \neq 0)) \land N = 0) \to (A^{2} ∥ 1 \to A^{2} = 1)$
60	36 59	syld	$⊢ (((A \in ℤ \land B \in ℤ \land N \in ℤ) \land (A \neq 0 \land B \neq 0)) \land N = 0) \to ({A B}^{2} = 1 \to A^{2} = 1)$
61	60	con3dimp	$⊢ ((((A \in ℤ \land B \in ℤ \land N \in ℤ) \land (A \neq 0 \land B \neq 0)) \land N = 0) \land \neg A^{2} = 1) \to \neg {A B}^{2} = 1$
62	61	iffalsed	$⊢ ((((A \in ℤ \land B \in ℤ \land N \in ℤ) \land (A \neq 0 \land B \neq 0)) \land N = 0) \land \neg A^{2} = 1) \to if ({A B}^{2} = 1, 1, 0) = 0$
63	24 27 62	3eqtr4a	$⊢ ((((A \in ℤ \land B \in ℤ \land N \in ℤ) \land (A \neq 0 \land B \neq 0)) \land N = 0) \land \neg A^{2} = 1) \to if (A^{2} = 1, 1, 0) if (B^{2} = 1, 1, 0) = if ({A B}^{2} = 1, 1, 0)$
64	23 63	pm2.61dan	$⊢ (((A \in ℤ \land B \in ℤ \land N \in ℤ) \land (A \neq 0 \land B \neq 0)) \land N = 0) \to if (A^{2} = 1, 1, 0) if (B^{2} = 1, 1, 0) = if ({A B}^{2} = 1, 1, 0)$
65		oveq2	$⊢ N = 0 \to A /_{L} N = A /_{L} 0$
66		lgs0	$⊢ A \in ℤ \to A /_{L} 0 = if (A^{2} = 1, 1, 0)$
67	8 66	syl	$⊢ ((A \in ℤ \land B \in ℤ \land N \in ℤ) \land (A \neq 0 \land B \neq 0)) \to A /_{L} 0 = if (A^{2} = 1, 1, 0)$
68	65 67	sylan9eqr	$⊢ (((A \in ℤ \land B \in ℤ \land N \in ℤ) \land (A \neq 0 \land B \neq 0)) \land N = 0) \to A /_{L} N = if (A^{2} = 1, 1, 0)$
69		oveq2	$⊢ N = 0 \to B /_{L} N = B /_{L} 0$
70		lgs0	$⊢ B \in ℤ \to B /_{L} 0 = if (B^{2} = 1, 1, 0)$
71	11 70	syl	$⊢ ((A \in ℤ \land B \in ℤ \land N \in ℤ) \land (A \neq 0 \land B \neq 0)) \to B /_{L} 0 = if (B^{2} = 1, 1, 0)$
72	69 71	sylan9eqr	$⊢ (((A \in ℤ \land B \in ℤ \land N \in ℤ) \land (A \neq 0 \land B \neq 0)) \land N = 0) \to B /_{L} N = if (B^{2} = 1, 1, 0)$
73	68 72	oveq12d	$⊢ (((A \in ℤ \land B \in ℤ \land N \in ℤ) \land (A \neq 0 \land B \neq 0)) \land N = 0) \to (A /_{L} N) (B /_{L} N) = if (A^{2} = 1, 1, 0) if (B^{2} = 1, 1, 0)$
74		oveq2	$⊢ N = 0 \to A B /_{L} N = A B /_{L} 0$
75		lgs0	$⊢ A B \in ℤ \to A B /_{L} 0 = if ({A B}^{2} = 1, 1, 0)$
76	30 75	syl	$⊢ ((A \in ℤ \land B \in ℤ \land N \in ℤ) \land (A \neq 0 \land B \neq 0)) \to A B /_{L} 0 = if ({A B}^{2} = 1, 1, 0)$
77	74 76	sylan9eqr	$⊢ (((A \in ℤ \land B \in ℤ \land N \in ℤ) \land (A \neq 0 \land B \neq 0)) \land N = 0) \to A B /_{L} N = if ({A B}^{2} = 1, 1, 0)$
78	64 73 77	3eqtr4rd	$⊢ (((A \in ℤ \land B \in ℤ \land N \in ℤ) \land (A \neq 0 \land B \neq 0)) \land N = 0) \to A B /_{L} N = (A /_{L} N) (B /_{L} N)$
79		lgsdilem	$⊢ ((A \in ℤ \land B \in ℤ \land N \in ℤ) \land (A \neq 0 \land B \neq 0)) \to if ((N < 0 \land A B < 0), - 1, 1) = if ((N < 0 \land A < 0), - 1, 1) if ((N < 0 \land B < 0), - 1, 1)$
80	79	adantr	$⊢ (((A \in ℤ \land B \in ℤ \land N \in ℤ) \land (A \neq 0 \land B \neq 0)) \land N \neq 0) \to if ((N < 0 \land A B < 0), - 1, 1) = if ((N < 0 \land A < 0), - 1, 1) if ((N < 0 \land B < 0), - 1, 1)$
81		simpl3	$⊢ ((A \in ℤ \land B \in ℤ \land N \in ℤ) \land (A \neq 0 \land B \neq 0)) \to N \in ℤ$
82		nnabscl	$⊢ (N \in ℤ \land N \neq 0) \to \|N\| \in ℕ$
83	81 82	sylan	$⊢ (((A \in ℤ \land B \in ℤ \land N \in ℤ) \land (A \neq 0 \land B \neq 0)) \land N \neq 0) \to \|N\| \in ℕ$
84		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
85	83 84	eleqtrdi	$⊢ (((A \in ℤ \land B \in ℤ \land N \in ℤ) \land (A \neq 0 \land B \neq 0)) \land N \neq 0) \to \|N\| \in ℤ_{\geq 1}$
86		simpll1	$⊢ (((A \in ℤ \land B \in ℤ \land N \in ℤ) \land (A \neq 0 \land B \neq 0)) \land N \neq 0) \to A \in ℤ$
87		simpll3	$⊢ (((A \in ℤ \land B \in ℤ \land N \in ℤ) \land (A \neq 0 \land B \neq 0)) \land N \neq 0) \to N \in ℤ$
88		simpr	$⊢ (((A \in ℤ \land B \in ℤ \land N \in ℤ) \land (A \neq 0 \land B \neq 0)) \land N \neq 0) \to N \neq 0$
89		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))$
90	89	lgsfcl3	$⊢ (A \in ℤ \land N \in ℤ \land N \neq 0) \to (n \in ℕ ⟼ if (n \in ℙ, {(A /_{L} n)}^{n pCnt N}, 1)) : ℕ ⟶ ℤ$
91	86 87 88 90	syl3anc	$⊢ (((A \in ℤ \land B \in ℤ \land N \in ℤ) \land (A \neq 0 \land B \neq 0)) \land N \neq 0) \to (n \in ℕ ⟼ if (n \in ℙ, {(A /_{L} n)}^{n pCnt N}, 1)) : ℕ ⟶ ℤ$
92		elfznn	$⊢ k \in (1 \dots \|N\|) \to k \in ℕ$
93		ffvelcdm	$⊢ ((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 ℤ$
94	91 92 93	syl2an	$⊢ ((((A \in ℤ \land B \in ℤ \land N \in ℤ) \land (A \neq 0 \land B \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 ℤ$
95	94	zcnd	$⊢ ((((A \in ℤ \land B \in ℤ \land N \in ℤ) \land (A \neq 0 \land B \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 ℂ$
96		simpll2	$⊢ (((A \in ℤ \land B \in ℤ \land N \in ℤ) \land (A \neq 0 \land B \neq 0)) \land N \neq 0) \to B \in ℤ$
97		eqid	$⊢ (n \in ℕ ⟼ if (n \in ℙ, {(B /_{L} n)}^{n pCnt N}, 1)) = (n \in ℕ ⟼ if (n \in ℙ, {(B /_{L} n)}^{n pCnt N}, 1))$
98	97	lgsfcl3	$⊢ (B \in ℤ \land N \in ℤ \land N \neq 0) \to (n \in ℕ ⟼ if (n \in ℙ, {(B /_{L} n)}^{n pCnt N}, 1)) : ℕ ⟶ ℤ$
99	96 87 88 98	syl3anc	$⊢ (((A \in ℤ \land B \in ℤ \land N \in ℤ) \land (A \neq 0 \land B \neq 0)) \land N \neq 0) \to (n \in ℕ ⟼ if (n \in ℙ, {(B /_{L} n)}^{n pCnt N}, 1)) : ℕ ⟶ ℤ$
100		ffvelcdm	$⊢ ((n \in ℕ ⟼ if (n \in ℙ, {(B /_{L} n)}^{n pCnt N}, 1)) : ℕ ⟶ ℤ \land k \in ℕ) \to (n \in ℕ ⟼ if (n \in ℙ, {(B /_{L} n)}^{n pCnt N}, 1)) (k) \in ℤ$
101	99 92 100	syl2an	$⊢ ((((A \in ℤ \land B \in ℤ \land N \in ℤ) \land (A \neq 0 \land B \neq 0)) \land N \neq 0) \land k \in (1 \dots \|N\|)) \to (n \in ℕ ⟼ if (n \in ℙ, {(B /_{L} n)}^{n pCnt N}, 1)) (k) \in ℤ$
102	101	zcnd	$⊢ ((((A \in ℤ \land B \in ℤ \land N \in ℤ) \land (A \neq 0 \land B \neq 0)) \land N \neq 0) \land k \in (1 \dots \|N\|)) \to (n \in ℕ ⟼ if (n \in ℙ, {(B /_{L} n)}^{n pCnt N}, 1)) (k) \in ℂ$
103	86	adantr	$⊢ ((((A \in ℤ \land B \in ℤ \land N \in ℤ) \land (A \neq 0 \land B \neq 0)) \land N \neq 0) \land k \in ℙ) \to A \in ℤ$
104	96	adantr	$⊢ ((((A \in ℤ \land B \in ℤ \land N \in ℤ) \land (A \neq 0 \land B \neq 0)) \land N \neq 0) \land k \in ℙ) \to B \in ℤ$
105		simpr	$⊢ ((((A \in ℤ \land B \in ℤ \land N \in ℤ) \land (A \neq 0 \land B \neq 0)) \land N \neq 0) \land k \in ℙ) \to k \in ℙ$
106		lgsdirprm	$⊢ (A \in ℤ \land B \in ℤ \land k \in ℙ) \to A B /_{L} k = (A /_{L} k) (B /_{L} k)$
107	103 104 105 106	syl3anc	$⊢ ((((A \in ℤ \land B \in ℤ \land N \in ℤ) \land (A \neq 0 \land B \neq 0)) \land N \neq 0) \land k \in ℙ) \to A B /_{L} k = (A /_{L} k) (B /_{L} k)$
108	107	oveq1d	$⊢ ((((A \in ℤ \land B \in ℤ \land N \in ℤ) \land (A \neq 0 \land B \neq 0)) \land N \neq 0) \land k \in ℙ) \to {(A B /_{L} k)}^{k pCnt N} = {(A /_{L} k) (B /_{L} k)}^{k pCnt N}$
109		prmz	$⊢ k \in ℙ \to k \in ℤ$
110		lgscl	$⊢ (A \in ℤ \land k \in ℤ) \to A /_{L} k \in ℤ$
111	86 109 110	syl2an	$⊢ ((((A \in ℤ \land B \in ℤ \land N \in ℤ) \land (A \neq 0 \land B \neq 0)) \land N \neq 0) \land k \in ℙ) \to A /_{L} k \in ℤ$
112	111	zcnd	$⊢ ((((A \in ℤ \land B \in ℤ \land N \in ℤ) \land (A \neq 0 \land B \neq 0)) \land N \neq 0) \land k \in ℙ) \to A /_{L} k \in ℂ$
113		lgscl	$⊢ (B \in ℤ \land k \in ℤ) \to B /_{L} k \in ℤ$
114	96 109 113	syl2an	$⊢ ((((A \in ℤ \land B \in ℤ \land N \in ℤ) \land (A \neq 0 \land B \neq 0)) \land N \neq 0) \land k \in ℙ) \to B /_{L} k \in ℤ$
115	114	zcnd	$⊢ ((((A \in ℤ \land B \in ℤ \land N \in ℤ) \land (A \neq 0 \land B \neq 0)) \land N \neq 0) \land k \in ℙ) \to B /_{L} k \in ℂ$
116	87	adantr	$⊢ ((((A \in ℤ \land B \in ℤ \land N \in ℤ) \land (A \neq 0 \land B \neq 0)) \land N \neq 0) \land k \in ℙ) \to N \in ℤ$
117	88	adantr	$⊢ ((((A \in ℤ \land B \in ℤ \land N \in ℤ) \land (A \neq 0 \land B \neq 0)) \land N \neq 0) \land k \in ℙ) \to N \neq 0$
118		pczcl	$⊢ (k \in ℙ \land (N \in ℤ \land N \neq 0)) \to k pCnt N \in ℕ_{0}$
119	105 116 117 118	syl12anc	$⊢ ((((A \in ℤ \land B \in ℤ \land N \in ℤ) \land (A \neq 0 \land B \neq 0)) \land N \neq 0) \land k \in ℙ) \to k pCnt N \in ℕ_{0}$
120	112 115 119	mulexpd	$⊢ ((((A \in ℤ \land B \in ℤ \land N \in ℤ) \land (A \neq 0 \land B \neq 0)) \land N \neq 0) \land k \in ℙ) \to {(A /_{L} k) (B /_{L} k)}^{k pCnt N} = {(A /_{L} k)}^{k pCnt N} {(B /_{L} k)}^{k pCnt N}$
121	108 120	eqtrd	$⊢ ((((A \in ℤ \land B \in ℤ \land N \in ℤ) \land (A \neq 0 \land B \neq 0)) \land N \neq 0) \land k \in ℙ) \to {(A B /_{L} k)}^{k pCnt N} = {(A /_{L} k)}^{k pCnt N} {(B /_{L} k)}^{k pCnt N}$
122		iftrue	$⊢ k \in ℙ \to if (k \in ℙ, {(A B /_{L} k)}^{k pCnt N}, 1) = {(A B /_{L} k)}^{k pCnt N}$
123	122	adantl	$⊢ ((((A \in ℤ \land B \in ℤ \land N \in ℤ) \land (A \neq 0 \land B \neq 0)) \land N \neq 0) \land k \in ℙ) \to if (k \in ℙ, {(A B /_{L} k)}^{k pCnt N}, 1) = {(A B /_{L} k)}^{k pCnt N}$
124		iftrue	$⊢ k \in ℙ \to if (k \in ℙ, {(A /_{L} k)}^{k pCnt N}, 1) = {(A /_{L} k)}^{k pCnt N}$
125		iftrue	$⊢ k \in ℙ \to if (k \in ℙ, {(B /_{L} k)}^{k pCnt N}, 1) = {(B /_{L} k)}^{k pCnt N}$
126	124 125	oveq12d	$⊢ k \in ℙ \to if (k \in ℙ, {(A /_{L} k)}^{k pCnt N}, 1) if (k \in ℙ, {(B /_{L} k)}^{k pCnt N}, 1) = {(A /_{L} k)}^{k pCnt N} {(B /_{L} k)}^{k pCnt N}$
127	126	adantl	$⊢ ((((A \in ℤ \land B \in ℤ \land N \in ℤ) \land (A \neq 0 \land B \neq 0)) \land N \neq 0) \land k \in ℙ) \to if (k \in ℙ, {(A /_{L} k)}^{k pCnt N}, 1) if (k \in ℙ, {(B /_{L} k)}^{k pCnt N}, 1) = {(A /_{L} k)}^{k pCnt N} {(B /_{L} k)}^{k pCnt N}$
128	121 123 127	3eqtr4d	$⊢ ((((A \in ℤ \land B \in ℤ \land N \in ℤ) \land (A \neq 0 \land B \neq 0)) \land N \neq 0) \land k \in ℙ) \to if (k \in ℙ, {(A B /_{L} k)}^{k pCnt N}, 1) = if (k \in ℙ, {(A /_{L} k)}^{k pCnt N}, 1) if (k \in ℙ, {(B /_{L} k)}^{k pCnt N}, 1)$
129		1t1e1	$⊢ 1 \cdot 1 = 1$
130	129	eqcomi	$⊢ 1 = 1 \cdot 1$
131		iffalse	$⊢ \neg k \in ℙ \to if (k \in ℙ, {(A B /_{L} k)}^{k pCnt N}, 1) = 1$
132		iffalse	$⊢ \neg k \in ℙ \to if (k \in ℙ, {(A /_{L} k)}^{k pCnt N}, 1) = 1$
133		iffalse	$⊢ \neg k \in ℙ \to if (k \in ℙ, {(B /_{L} k)}^{k pCnt N}, 1) = 1$
134	132 133	oveq12d	$⊢ \neg k \in ℙ \to if (k \in ℙ, {(A /_{L} k)}^{k pCnt N}, 1) if (k \in ℙ, {(B /_{L} k)}^{k pCnt N}, 1) = 1 \cdot 1$
135	130 131 134	3eqtr4a	$⊢ \neg k \in ℙ \to if (k \in ℙ, {(A B /_{L} k)}^{k pCnt N}, 1) = if (k \in ℙ, {(A /_{L} k)}^{k pCnt N}, 1) if (k \in ℙ, {(B /_{L} k)}^{k pCnt N}, 1)$
136	135	adantl	$⊢ ((((A \in ℤ \land B \in ℤ \land N \in ℤ) \land (A \neq 0 \land B \neq 0)) \land N \neq 0) \land \neg k \in ℙ) \to if (k \in ℙ, {(A B /_{L} k)}^{k pCnt N}, 1) = if (k \in ℙ, {(A /_{L} k)}^{k pCnt N}, 1) if (k \in ℙ, {(B /_{L} k)}^{k pCnt N}, 1)$
137	128 136	pm2.61dan	$⊢ (((A \in ℤ \land B \in ℤ \land N \in ℤ) \land (A \neq 0 \land B \neq 0)) \land N \neq 0) \to if (k \in ℙ, {(A B /_{L} k)}^{k pCnt N}, 1) = if (k \in ℙ, {(A /_{L} k)}^{k pCnt N}, 1) if (k \in ℙ, {(B /_{L} k)}^{k pCnt N}, 1)$
138	137	adantr	$⊢ ((((A \in ℤ \land B \in ℤ \land N \in ℤ) \land (A \neq 0 \land B \neq 0)) \land N \neq 0) \land k \in (1 \dots \|N\|)) \to if (k \in ℙ, {(A B /_{L} k)}^{k pCnt N}, 1) = if (k \in ℙ, {(A /_{L} k)}^{k pCnt N}, 1) if (k \in ℙ, {(B /_{L} k)}^{k pCnt N}, 1)$
139	92	adantl	$⊢ ((((A \in ℤ \land B \in ℤ \land N \in ℤ) \land (A \neq 0 \land B \neq 0)) \land N \neq 0) \land k \in (1 \dots \|N\|)) \to k \in ℕ$
140		eleq1w	$⊢ n = k \to (n \in ℙ \leftrightarrow k \in ℙ)$
141		oveq2	$⊢ n = k \to A B /_{L} n = A B /_{L} k$
142		oveq1	$⊢ n = k \to n pCnt N = k pCnt N$
143	141 142	oveq12d	$⊢ n = k \to {(A B /_{L} n)}^{n pCnt N} = {(A B /_{L} k)}^{k pCnt N}$
144	140 143	ifbieq1d	$⊢ n = k \to if (n \in ℙ, {(A B /_{L} n)}^{n pCnt N}, 1) = if (k \in ℙ, {(A B /_{L} k)}^{k pCnt N}, 1)$
145		eqid	$⊢ (n \in ℕ ⟼ if (n \in ℙ, {(A B /_{L} n)}^{n pCnt N}, 1)) = (n \in ℕ ⟼ if (n \in ℙ, {(A B /_{L} n)}^{n pCnt N}, 1))$
146		ovex	$⊢ {(A B /_{L} k)}^{k pCnt N} \in V$
147		1ex	$⊢ 1 \in V$
148	146 147	ifex	$⊢ if (k \in ℙ, {(A B /_{L} k)}^{k pCnt N}, 1) \in V$
149	144 145 148	fvmpt	$⊢ k \in ℕ \to (n \in ℕ ⟼ if (n \in ℙ, {(A B /_{L} n)}^{n pCnt N}, 1)) (k) = if (k \in ℙ, {(A B /_{L} k)}^{k pCnt N}, 1)$
150	139 149	syl	$⊢ ((((A \in ℤ \land B \in ℤ \land N \in ℤ) \land (A \neq 0 \land B \neq 0)) \land N \neq 0) \land k \in (1 \dots \|N\|)) \to (n \in ℕ ⟼ if (n \in ℙ, {(A B /_{L} n)}^{n pCnt N}, 1)) (k) = if (k \in ℙ, {(A B /_{L} k)}^{k pCnt N}, 1)$
151		oveq2	$⊢ n = k \to A /_{L} n = A /_{L} k$
152	151 142	oveq12d	$⊢ n = k \to {(A /_{L} n)}^{n pCnt N} = {(A /_{L} k)}^{k pCnt N}$
153	140 152	ifbieq1d	$⊢ n = k \to if (n \in ℙ, {(A /_{L} n)}^{n pCnt N}, 1) = if (k \in ℙ, {(A /_{L} k)}^{k pCnt N}, 1)$
154		ovex	$⊢ {(A /_{L} k)}^{k pCnt N} \in V$
155	154 147	ifex	$⊢ if (k \in ℙ, {(A /_{L} k)}^{k pCnt N}, 1) \in V$
156	153 89 155	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)$
157	139 156	syl	$⊢ ((((A \in ℤ \land B \in ℤ \land N \in ℤ) \land (A \neq 0 \land B \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) = if (k \in ℙ, {(A /_{L} k)}^{k pCnt N}, 1)$
158		oveq2	$⊢ n = k \to B /_{L} n = B /_{L} k$
159	158 142	oveq12d	$⊢ n = k \to {(B /_{L} n)}^{n pCnt N} = {(B /_{L} k)}^{k pCnt N}$
160	140 159	ifbieq1d	$⊢ n = k \to if (n \in ℙ, {(B /_{L} n)}^{n pCnt N}, 1) = if (k \in ℙ, {(B /_{L} k)}^{k pCnt N}, 1)$
161		ovex	$⊢ {(B /_{L} k)}^{k pCnt N} \in V$
162	161 147	ifex	$⊢ if (k \in ℙ, {(B /_{L} k)}^{k pCnt N}, 1) \in V$
163	160 97 162	fvmpt	$⊢ k \in ℕ \to (n \in ℕ ⟼ if (n \in ℙ, {(B /_{L} n)}^{n pCnt N}, 1)) (k) = if (k \in ℙ, {(B /_{L} k)}^{k pCnt N}, 1)$
164	139 163	syl	$⊢ ((((A \in ℤ \land B \in ℤ \land N \in ℤ) \land (A \neq 0 \land B \neq 0)) \land N \neq 0) \land k \in (1 \dots \|N\|)) \to (n \in ℕ ⟼ if (n \in ℙ, {(B /_{L} n)}^{n pCnt N}, 1)) (k) = if (k \in ℙ, {(B /_{L} k)}^{k pCnt N}, 1)$
165	157 164	oveq12d	$⊢ ((((A \in ℤ \land B \in ℤ \land N \in ℤ) \land (A \neq 0 \land B \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) (n \in ℕ ⟼ if (n \in ℙ, {(B /_{L} n)}^{n pCnt N}, 1)) (k) = if (k \in ℙ, {(A /_{L} k)}^{k pCnt N}, 1) if (k \in ℙ, {(B /_{L} k)}^{k pCnt N}, 1)$
166	138 150 165	3eqtr4d	$⊢ ((((A \in ℤ \land B \in ℤ \land N \in ℤ) \land (A \neq 0 \land B \neq 0)) \land N \neq 0) \land k \in (1 \dots \|N\|)) \to (n \in ℕ ⟼ if (n \in ℙ, {(A B /_{L} n)}^{n pCnt N}, 1)) (k) = (n \in ℕ ⟼ if (n \in ℙ, {(A /_{L} n)}^{n pCnt N}, 1)) (k) (n \in ℕ ⟼ if (n \in ℙ, {(B /_{L} n)}^{n pCnt N}, 1)) (k)$
167	85 95 102 166	prodfmul	$⊢ (((A \in ℤ \land B \in ℤ \land N \in ℤ) \land (A \neq 0 \land B \neq 0)) \land N \neq 0) \to seq 1 (\times (n \in ℕ ⟼ if (n \in ℙ, {(A B /_{L} n)}^{n pCnt N}, 1))) (\|N\|) = seq 1 (\times (n \in ℕ ⟼ if (n \in ℙ, {(A /_{L} n)}^{n pCnt N}, 1))) (\|N\|) seq 1 (\times (n \in ℕ ⟼ if (n \in ℙ, {(B /_{L} n)}^{n pCnt N}, 1))) (\|N\|)$
168	80 167	oveq12d	$⊢ (((A \in ℤ \land B \in ℤ \land N \in ℤ) \land (A \neq 0 \land B \neq 0)) \land N \neq 0) \to if ((N < 0 \land A B < 0), - 1, 1) seq 1 (\times (n \in ℕ ⟼ if (n \in ℙ, {(A B /_{L} n)}^{n pCnt N}, 1))) (\|N\|) = if ((N < 0 \land A < 0), - 1, 1) if ((N < 0 \land B < 0), - 1, 1) seq 1 (\times (n \in ℕ ⟼ if (n \in ℙ, {(A /_{L} n)}^{n pCnt N}, 1))) (\|N\|) seq 1 (\times (n \in ℕ ⟼ if (n \in ℙ, {(B /_{L} n)}^{n pCnt N}, 1))) (\|N\|)$
169	30	adantr	$⊢ (((A \in ℤ \land B \in ℤ \land N \in ℤ) \land (A \neq 0 \land B \neq 0)) \land N \neq 0) \to A B \in ℤ$
170	145	lgsval4	$⊢ (A B \in ℤ \land N \in ℤ \land N \neq 0) \to A B /_{L} N = if ((N < 0 \land A B < 0), - 1, 1) seq 1 (\times (n \in ℕ ⟼ if (n \in ℙ, {(A B /_{L} n)}^{n pCnt N}, 1))) (\|N\|)$
171	169 87 88 170	syl3anc	$⊢ (((A \in ℤ \land B \in ℤ \land N \in ℤ) \land (A \neq 0 \land B \neq 0)) \land N \neq 0) \to A B /_{L} N = if ((N < 0 \land A B < 0), - 1, 1) seq 1 (\times (n \in ℕ ⟼ if (n \in ℙ, {(A B /_{L} n)}^{n pCnt N}, 1))) (\|N\|)$
172	89	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\|)$
173	86 87 88 172	syl3anc	$⊢ (((A \in ℤ \land B \in ℤ \land N \in ℤ) \land (A \neq 0 \land B \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\|)$
174	97	lgsval4	$⊢ (B \in ℤ \land N \in ℤ \land N \neq 0) \to B /_{L} N = if ((N < 0 \land B < 0), - 1, 1) seq 1 (\times (n \in ℕ ⟼ if (n \in ℙ, {(B /_{L} n)}^{n pCnt N}, 1))) (\|N\|)$
175	96 87 88 174	syl3anc	$⊢ (((A \in ℤ \land B \in ℤ \land N \in ℤ) \land (A \neq 0 \land B \neq 0)) \land N \neq 0) \to B /_{L} N = if ((N < 0 \land B < 0), - 1, 1) seq 1 (\times (n \in ℕ ⟼ if (n \in ℙ, {(B /_{L} n)}^{n pCnt N}, 1))) (\|N\|)$
176	173 175	oveq12d	$⊢ (((A \in ℤ \land B \in ℤ \land N \in ℤ) \land (A \neq 0 \land B \neq 0)) \land N \neq 0) \to (A /_{L} N) (B /_{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\|) if ((N < 0 \land B < 0), - 1, 1) seq 1 (\times (n \in ℕ ⟼ if (n \in ℙ, {(B /_{L} n)}^{n pCnt N}, 1))) (\|N\|)$
177		neg1cn	$⊢ - 1 \in ℂ$
178	177 1	ifcli	$⊢ if ((N < 0 \land A < 0), - 1, 1) \in ℂ$
179	178	a1i	$⊢ (((A \in ℤ \land B \in ℤ \land N \in ℤ) \land (A \neq 0 \land B \neq 0)) \land N \neq 0) \to if ((N < 0 \land A < 0), - 1, 1) \in ℂ$
180		mulcl	$⊢ (k \in ℂ \land x \in ℂ) \to k x \in ℂ$
181	180	adantl	$⊢ ((((A \in ℤ \land B \in ℤ \land N \in ℤ) \land (A \neq 0 \land B \neq 0)) \land N \neq 0) \land (k \in ℂ \land x \in ℂ)) \to k x \in ℂ$
182	85 95 181	seqcl	$⊢ (((A \in ℤ \land B \in ℤ \land N \in ℤ) \land (A \neq 0 \land B \neq 0)) \land N \neq 0) \to seq 1 (\times (n \in ℕ ⟼ if (n \in ℙ, {(A /_{L} n)}^{n pCnt N}, 1))) (\|N\|) \in ℂ$
183	177 1	ifcli	$⊢ if ((N < 0 \land B < 0), - 1, 1) \in ℂ$
184	183	a1i	$⊢ (((A \in ℤ \land B \in ℤ \land N \in ℤ) \land (A \neq 0 \land B \neq 0)) \land N \neq 0) \to if ((N < 0 \land B < 0), - 1, 1) \in ℂ$
185	85 102 181	seqcl	$⊢ (((A \in ℤ \land B \in ℤ \land N \in ℤ) \land (A \neq 0 \land B \neq 0)) \land N \neq 0) \to seq 1 (\times (n \in ℕ ⟼ if (n \in ℙ, {(B /_{L} n)}^{n pCnt N}, 1))) (\|N\|) \in ℂ$
186	179 182 184 185	mul4d	$⊢ (((A \in ℤ \land B \in ℤ \land N \in ℤ) \land (A \neq 0 \land B \neq 0)) \land N \neq 0) \to 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 ((N < 0 \land B < 0), - 1, 1) seq 1 (\times (n \in ℕ ⟼ if (n \in ℙ, {(B /_{L} n)}^{n pCnt N}, 1))) (\|N\|) = if ((N < 0 \land A < 0), - 1, 1) if ((N < 0 \land B < 0), - 1, 1) seq 1 (\times (n \in ℕ ⟼ if (n \in ℙ, {(A /_{L} n)}^{n pCnt N}, 1))) (\|N\|) seq 1 (\times (n \in ℕ ⟼ if (n \in ℙ, {(B /_{L} n)}^{n pCnt N}, 1))) (\|N\|)$
187	176 186	eqtrd	$⊢ (((A \in ℤ \land B \in ℤ \land N \in ℤ) \land (A \neq 0 \land B \neq 0)) \land N \neq 0) \to (A /_{L} N) (B /_{L} N) = if ((N < 0 \land A < 0), - 1, 1) if ((N < 0 \land B < 0), - 1, 1) seq 1 (\times (n \in ℕ ⟼ if (n \in ℙ, {(A /_{L} n)}^{n pCnt N}, 1))) (\|N\|) seq 1 (\times (n \in ℕ ⟼ if (n \in ℙ, {(B /_{L} n)}^{n pCnt N}, 1))) (\|N\|)$
188	168 171 187	3eqtr4d	$⊢ (((A \in ℤ \land B \in ℤ \land N \in ℤ) \land (A \neq 0 \land B \neq 0)) \land N \neq 0) \to A B /_{L} N = (A /_{L} N) (B /_{L} N)$
189	78 188	pm2.61dane	$⊢ ((A \in ℤ \land B \in ℤ \land N \in ℤ) \land (A \neq 0 \land B \neq 0)) \to A B /_{L} N = (A /_{L} N) (B /_{L} N)$

Metamath Proof Explorer

Theorem lgsdir

Proof