Theorem 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	⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐴 ≠ 0 ∧ 𝐵 ≠ 0 ) ) → ( ( 𝐴 · 𝐵 ) /L 𝑁 ) = ( ( 𝐴 /L 𝑁 ) · ( 𝐵 /L 𝑁 ) ) )

Proof

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