lgsdir - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > lgsdir		Structured version Visualization version GIF version

Theorem lgsdir 27659

Description: The Legendre symbol is completely multiplicative in its left argument. Generalization of theorem 9.9(a) in [ApostolNT] p. 188 (which assumes that 𝐴 and 𝐵 are odd positive integers). Together with lgsqr 27678 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.)

**Assertion**
Ref	Expression
lgsdir	⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) → ((𝐴 · 𝐵) /_L 𝑁) = ((𝐴 /_L 𝑁) · (𝐵 /_L 𝑁)))

Proof of Theorem lgsdir Dummy variables 𝑘 𝑛 𝑥 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		ax-1cn 11258	. . . . . . 7 ⊢ 1 ∈ ℂ
2		0cn 11298	. . . . . . 7 ⊢ 0 ∈ ℂ
3	1, 2	ifcli 4530	. . . . . 6 ⊢ if((𝐵↑2) = 1, 1, 0) ∈ ℂ
4	3	mullidi 11314	. . . . 5 ⊢ (1 · if((𝐵↑2) = 1, 1, 0)) = if((𝐵↑2) = 1, 1, 0)
5		iftrue 4488	. . . . . . 7 ⊢ ((𝐴↑2) = 1 → if((𝐴↑2) = 1, 1, 0) = 1)
6	5	adantl 487	. . . . . 6 ⊢ (((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 = 0) ∧ (𝐴↑2) = 1) → if((𝐴↑2) = 1, 1, 0) = 1)
7	6	oveq1d 7435	. . . . 5 ⊢ (((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 = 0) ∧ (𝐴↑2) = 1) → (if((𝐴↑2) = 1, 1, 0) · if((𝐵↑2) = 1, 1, 0)) = (1 · if((𝐵↑2) = 1, 1, 0)))
8		simpl1 1210	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) → 𝐴 ∈ ℤ)
9	8	zcnd 12804	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) → 𝐴 ∈ ℂ)
10	9	ad2antrr 739	. . . . . . . . 9 ⊢ (((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 = 0) ∧ (𝐴↑2) = 1) → 𝐴 ∈ ℂ)
11		simpl2 1211	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) → 𝐵 ∈ ℤ)
12	11	zcnd 12804	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) → 𝐵 ∈ ℂ)
13	12	ad2antrr 739	. . . . . . . . 9 ⊢ (((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 = 0) ∧ (𝐴↑2) = 1) → 𝐵 ∈ ℂ)
14	10, 13	sqmuld 14301	. . . . . . . 8 ⊢ (((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 = 0) ∧ (𝐴↑2) = 1) → ((𝐴 · 𝐵)↑2) = ((𝐴↑2) · (𝐵↑2)))
15		simpr 490	. . . . . . . . 9 ⊢ (((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 = 0) ∧ (𝐴↑2) = 1) → (𝐴↑2) = 1)
16	15	oveq1d 7435	. . . . . . . 8 ⊢ (((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 = 0) ∧ (𝐴↑2) = 1) → ((𝐴↑2) · (𝐵↑2)) = (1 · (𝐵↑2)))
17	12	sqcld 14287	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) → (𝐵↑2) ∈ ℂ)
18	17	ad2antrr 739	. . . . . . . . 9 ⊢ (((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 = 0) ∧ (𝐴↑2) = 1) → (𝐵↑2) ∈ ℂ)
19	18	mullidd 11327	. . . . . . . 8 ⊢ (((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 = 0) ∧ (𝐴↑2) = 1) → (1 · (𝐵↑2)) = (𝐵↑2))
20	14, 16, 19	3eqtrd 2800	. . . . . . 7 ⊢ (((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 = 0) ∧ (𝐴↑2) = 1) → ((𝐴 · 𝐵)↑2) = (𝐵↑2))
21	20	eqeq1d 2763	. . . . . 6 ⊢ (((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 = 0) ∧ (𝐴↑2) = 1) → (((𝐴 · 𝐵)↑2) = 1 ↔ (𝐵↑2) = 1))
22	21	ifbid 4506	. . . . 5 ⊢ (((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 = 0) ∧ (𝐴↑2) = 1) → if(((𝐴 · 𝐵)↑2) = 1, 1, 0) = if((𝐵↑2) = 1, 1, 0))
23	4, 7, 22	3eqtr4a 2822	. . . 4 ⊢ (((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 = 0) ∧ (𝐴↑2) = 1) → (if((𝐴↑2) = 1, 1, 0) · if((𝐵↑2) = 1, 1, 0)) = if(((𝐴 · 𝐵)↑2) = 1, 1, 0))
24	3	mul02i 11499	. . . . 5 ⊢ (0 · if((𝐵↑2) = 1, 1, 0)) = 0
25		iffalse 4491	. . . . . . 7 ⊢ (¬ (𝐴↑2) = 1 → if((𝐴↑2) = 1, 1, 0) = 0)
26	25	adantl 487	. . . . . 6 ⊢ (((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 = 0) ∧ ¬ (𝐴↑2) = 1) → if((𝐴↑2) = 1, 1, 0) = 0)
27	26	oveq1d 7435	. . . . 5 ⊢ (((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 = 0) ∧ ¬ (𝐴↑2) = 1) → (if((𝐴↑2) = 1, 1, 0) · if((𝐵↑2) = 1, 1, 0)) = (0 · if((𝐵↑2) = 1, 1, 0)))
28		dvdsmul1 16447	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → 𝐴 ∥ (𝐴 · 𝐵))
29	8, 11, 28	syl2anc 596	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) → 𝐴 ∥ (𝐴 · 𝐵))
30	8, 11	zmulcld 12809	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) → (𝐴 · 𝐵) ∈ ℤ)
31		dvdssq 16742	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ ℤ ∧ (𝐴 · 𝐵) ∈ ℤ) → (𝐴 ∥ (𝐴 · 𝐵) ↔ (𝐴↑2) ∥ ((𝐴 · 𝐵)↑2)))
32	8, 30, 31	syl2anc 596	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) → (𝐴 ∥ (𝐴 · 𝐵) ↔ (𝐴↑2) ∥ ((𝐴 · 𝐵)↑2)))
33	29, 32	mpbid 235	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) → (𝐴↑2) ∥ ((𝐴 · 𝐵)↑2))
34	33	adantr 486	. . . . . . . . 9 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 = 0) → (𝐴↑2) ∥ ((𝐴 · 𝐵)↑2))
35		breq2 5107	. . . . . . . . 9 ⊢ (((𝐴 · 𝐵)↑2) = 1 → ((𝐴↑2) ∥ ((𝐴 · 𝐵)↑2) ↔ (𝐴↑2) ∥ 1))
36	34, 35	syl5ibcom 248	. . . . . . . 8 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 = 0) → (((𝐴 · 𝐵)↑2) = 1 → (𝐴↑2) ∥ 1))
37		simprl 783	. . . . . . . . . . . . . . . 16 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) → 𝐴 ≠ 0)
38	37	neneqd 2961	. . . . . . . . . . . . . . 15 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) → ¬ 𝐴 = 0)
39		sqeq0 14263	. . . . . . . . . . . . . . . 16 ⊢ (𝐴 ∈ ℂ → ((𝐴↑2) = 0 ↔ 𝐴 = 0))
40	9, 39	syl 18	. . . . . . . . . . . . . . 15 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) → ((𝐴↑2) = 0 ↔ 𝐴 = 0))
41	38, 40	mtbird 328	. . . . . . . . . . . . . 14 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) → ¬ (𝐴↑2) = 0)
42		zsqcl2 14281	. . . . . . . . . . . . . . . . 17 ⊢ (𝐴 ∈ ℤ → (𝐴↑2) ∈ ℕ₀)
43	8, 42	syl 18	. . . . . . . . . . . . . . . 16 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) → (𝐴↑2) ∈ ℕ₀)
44		elnn0 12608	. . . . . . . . . . . . . . . 16 ⊢ ((𝐴↑2) ∈ ℕ₀ ↔ ((𝐴↑2) ∈ ℕ ∨ (𝐴↑2) = 0))
45	43, 44	sylib 221	. . . . . . . . . . . . . . 15 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) → ((𝐴↑2) ∈ ℕ ∨ (𝐴↑2) = 0))
46	45	ord 878	. . . . . . . . . . . . . 14 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) → (¬ (𝐴↑2) ∈ ℕ → (𝐴↑2) = 0))
47	41, 46	mt3d 149	. . . . . . . . . . . . 13 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) → (𝐴↑2) ∈ ℕ)
48	47	adantr 486	. . . . . . . . . . . 12 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 = 0) → (𝐴↑2) ∈ ℕ)
49	48	nnzd 12719	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 = 0) → (𝐴↑2) ∈ ℤ)
50		1nn 12346	. . . . . . . . . . 11 ⊢ 1 ∈ ℕ
51		dvdsle 16480	. . . . . . . . . . 11 ⊢ (((𝐴↑2) ∈ ℤ ∧ 1 ∈ ℕ) → ((𝐴↑2) ∥ 1 → (𝐴↑2) ≤ 1))
52	49, 50, 51	sylancl 598	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 = 0) → ((𝐴↑2) ∥ 1 → (𝐴↑2) ≤ 1))
53	48	nnge1d 12386	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 = 0) → 1 ≤ (𝐴↑2))
54	52, 53	jctird 536	. . . . . . . . 9 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 = 0) → ((𝐴↑2) ∥ 1 → ((𝐴↑2) ≤ 1 ∧ 1 ≤ (𝐴↑2))))
55	48	nnred 12350	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 = 0) → (𝐴↑2) ∈ ℝ)
56		1re 11308	. . . . . . . . . 10 ⊢ 1 ∈ ℝ
57		letri3 11395	. . . . . . . . . 10 ⊢ (((𝐴↑2) ∈ ℝ ∧ 1 ∈ ℝ) → ((𝐴↑2) = 1 ↔ ((𝐴↑2) ≤ 1 ∧ 1 ≤ (𝐴↑2))))
58	55, 56, 57	sylancl 598	. . . . . . . . 9 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 = 0) → ((𝐴↑2) = 1 ↔ ((𝐴↑2) ≤ 1 ∧ 1 ≤ (𝐴↑2))))
59	54, 58	sylibrd 262	. . . . . . . 8 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 = 0) → ((𝐴↑2) ∥ 1 → (𝐴↑2) = 1))
60	36, 59	syld 48	. . . . . . 7 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 = 0) → (((𝐴 · 𝐵)↑2) = 1 → (𝐴↑2) = 1))
61	60	con3dimp 414	. . . . . 6 ⊢ (((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 = 0) ∧ ¬ (𝐴↑2) = 1) → ¬ ((𝐴 · 𝐵)↑2) = 1)
62	61	iffalsed 4493	. . . . 5 ⊢ (((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 = 0) ∧ ¬ (𝐴↑2) = 1) → if(((𝐴 · 𝐵)↑2) = 1, 1, 0) = 0)
63	24, 27, 62	3eqtr4a 2822	. . . 4 ⊢ (((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 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 825	. . 3 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 = 0) → (if((𝐴↑2) = 1, 1, 0) · if((𝐵↑2) = 1, 1, 0)) = if(((𝐴 · 𝐵)↑2) = 1, 1, 0))
65		oveq2 7428	. . . . 5 ⊢ (𝑁 = 0 → (𝐴 /_L 𝑁) = (𝐴 /_L 0))
66		lgs0 27637	. . . . . 6 ⊢ (𝐴 ∈ ℤ → (𝐴 /_L 0) = if((𝐴↑2) = 1, 1, 0))
67	8, 66	syl 18	. . . . 5 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) → (𝐴 /_L 0) = if((𝐴↑2) = 1, 1, 0))
68	65, 67	sylan9eqr 2818	. . . 4 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 = 0) → (𝐴 /_L 𝑁) = if((𝐴↑2) = 1, 1, 0))
69		oveq2 7428	. . . . 5 ⊢ (𝑁 = 0 → (𝐵 /_L 𝑁) = (𝐵 /_L 0))
70		lgs0 27637	. . . . . 6 ⊢ (𝐵 ∈ ℤ → (𝐵 /_L 0) = if((𝐵↑2) = 1, 1, 0))
71	11, 70	syl 18	. . . . 5 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) → (𝐵 /_L 0) = if((𝐵↑2) = 1, 1, 0))
72	69, 71	sylan9eqr 2818	. . . 4 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 = 0) → (𝐵 /_L 𝑁) = if((𝐵↑2) = 1, 1, 0))
73	68, 72	oveq12d 7438	. . 3 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 = 0) → ((𝐴 /_L 𝑁) · (𝐵 /_L 𝑁)) = (if((𝐴↑2) = 1, 1, 0) · if((𝐵↑2) = 1, 1, 0)))
74		oveq2 7428	. . . 4 ⊢ (𝑁 = 0 → ((𝐴 · 𝐵) /_L 𝑁) = ((𝐴 · 𝐵) /_L 0))
75		lgs0 27637	. . . . 5 ⊢ ((𝐴 · 𝐵) ∈ ℤ → ((𝐴 · 𝐵) /_L 0) = if(((𝐴 · 𝐵)↑2) = 1, 1, 0))
76	30, 75	syl 18	. . . 4 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) → ((𝐴 · 𝐵) /_L 0) = if(((𝐴 · 𝐵)↑2) = 1, 1, 0))
77	74, 76	sylan9eqr 2818	. . 3 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 = 0) → ((𝐴 · 𝐵) /_L 𝑁) = if(((𝐴 · 𝐵)↑2) = 1, 1, 0))
78	64, 73, 77	3eqtr4rd 2807	. 2 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 = 0) → ((𝐴 · 𝐵) /_L 𝑁) = ((𝐴 /_L 𝑁) · (𝐵 /_L 𝑁)))
79		lgsdilem 27651	. . . . 5 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) → if((𝑁 < 0 ∧ (𝐴 · 𝐵) < 0), -1, 1) = (if((𝑁 < 0 ∧ 𝐴 < 0), -1, 1) · if((𝑁 < 0 ∧ 𝐵 < 0), -1, 1)))
80	79	adantr 486	. . . 4 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 ≠ 0) → if((𝑁 < 0 ∧ (𝐴 · 𝐵) < 0), -1, 1) = (if((𝑁 < 0 ∧ 𝐴 < 0), -1, 1) · if((𝑁 < 0 ∧ 𝐵 < 0), -1, 1)))
81		simpl3 1212	. . . . . . 7 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) → 𝑁 ∈ ℤ)
82		nnabscl 15493	. . . . . . 7 ⊢ ((𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) → (abs‘𝑁) ∈ ℕ)
83	81, 82	sylan 592	. . . . . 6 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 ≠ 0) → (abs‘𝑁) ∈ ℕ)
84		nnuz 13004	. . . . . 6 ⊢ ℕ = (ℤ_≥‘1)
85	83, 84	eleqtrdi 2871	. . . . 5 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 ≠ 0) → (abs‘𝑁) ∈ (ℤ_≥‘1))
86		simpll1 1231	. . . . . . . 8 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 ≠ 0) → 𝐴 ∈ ℤ)
87		simpll3 1233	. . . . . . . 8 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 ≠ 0) → 𝑁 ∈ ℤ)
88		simpr 490	. . . . . . . 8 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 ≠ 0) → 𝑁 ≠ 0)
89		eqid 2761	. . . . . . . . 9 ⊢ (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /_L 𝑛)↑(𝑛 pCnt 𝑁)), 1)) = (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /_L 𝑛)↑(𝑛 pCnt 𝑁)), 1))
90	89	lgsfcl3 27645	. . . . . . . 8 ⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) → (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /_L 𝑛)↑(𝑛 pCnt 𝑁)), 1)):ℕ⟶ℤ)
91	86, 87, 88, 90	syl3anc 1398	. . . . . . 7 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 ≠ 0) → (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /_L 𝑛)↑(𝑛 pCnt 𝑁)), 1)):ℕ⟶ℤ)
92		elfznn 13687	. . . . . . 7 ⊢ (𝑘 ∈ (1...(abs‘𝑁)) → 𝑘 ∈ ℕ)
93		ffvelcdm 7081	. . . . . . 7 ⊢ (((𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /_L 𝑛)↑(𝑛 pCnt 𝑁)), 1)):ℕ⟶ℤ ∧ 𝑘 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /_L 𝑛)↑(𝑛 pCnt 𝑁)), 1))‘𝑘) ∈ ℤ)
94	91, 92, 93	syl2an 608	. . . . . 6 ⊢ (((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 ≠ 0) ∧ 𝑘 ∈ (1...(abs‘𝑁))) → ((𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /_L 𝑛)↑(𝑛 pCnt 𝑁)), 1))‘𝑘) ∈ ℤ)
95	94	zcnd 12804	. . . . 5 ⊢ (((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 ≠ 0) ∧ 𝑘 ∈ (1...(abs‘𝑁))) → ((𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /_L 𝑛)↑(𝑛 pCnt 𝑁)), 1))‘𝑘) ∈ ℂ)
96		simpll2 1232	. . . . . . . 8 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 ≠ 0) → 𝐵 ∈ ℤ)
97		eqid 2761	. . . . . . . . 9 ⊢ (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐵 /_L 𝑛)↑(𝑛 pCnt 𝑁)), 1)) = (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐵 /_L 𝑛)↑(𝑛 pCnt 𝑁)), 1))
98	97	lgsfcl3 27645	. . . . . . . 8 ⊢ ((𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) → (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐵 /_L 𝑛)↑(𝑛 pCnt 𝑁)), 1)):ℕ⟶ℤ)
99	96, 87, 88, 98	syl3anc 1398	. . . . . . 7 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 ≠ 0) → (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐵 /_L 𝑛)↑(𝑛 pCnt 𝑁)), 1)):ℕ⟶ℤ)
100		ffvelcdm 7081	. . . . . . 7 ⊢ (((𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐵 /_L 𝑛)↑(𝑛 pCnt 𝑁)), 1)):ℕ⟶ℤ ∧ 𝑘 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐵 /_L 𝑛)↑(𝑛 pCnt 𝑁)), 1))‘𝑘) ∈ ℤ)
101	99, 92, 100	syl2an 608	. . . . . 6 ⊢ (((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 ≠ 0) ∧ 𝑘 ∈ (1...(abs‘𝑁))) → ((𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐵 /_L 𝑛)↑(𝑛 pCnt 𝑁)), 1))‘𝑘) ∈ ℤ)
102	101	zcnd 12804	. . . . 5 ⊢ (((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 ≠ 0) ∧ 𝑘 ∈ (1...(abs‘𝑁))) → ((𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐵 /_L 𝑛)↑(𝑛 pCnt 𝑁)), 1))‘𝑘) ∈ ℂ)
103	86	adantr 486	. . . . . . . . . . . 12 ⊢ (((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 ≠ 0) ∧ 𝑘 ∈ ℙ) → 𝐴 ∈ ℤ)
104	96	adantr 486	. . . . . . . . . . . 12 ⊢ (((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 ≠ 0) ∧ 𝑘 ∈ ℙ) → 𝐵 ∈ ℤ)
105		simpr 490	. . . . . . . . . . . 12 ⊢ (((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 ≠ 0) ∧ 𝑘 ∈ ℙ) → 𝑘 ∈ ℙ)
106		lgsdirprm 27658	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑘 ∈ ℙ) → ((𝐴 · 𝐵) /_L 𝑘) = ((𝐴 /_L 𝑘) · (𝐵 /_L 𝑘)))
107	103, 104, 105, 106	syl3anc 1398	. . . . . . . . . . 11 ⊢ (((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 ≠ 0) ∧ 𝑘 ∈ ℙ) → ((𝐴 · 𝐵) /_L 𝑘) = ((𝐴 /_L 𝑘) · (𝐵 /_L 𝑘)))
108	107	oveq1d 7435	. . . . . . . . . 10 ⊢ (((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 ≠ 0) ∧ 𝑘 ∈ ℙ) → (((𝐴 · 𝐵) /_L 𝑘)↑(𝑘 pCnt 𝑁)) = (((𝐴 /_L 𝑘) · (𝐵 /_L 𝑘))↑(𝑘 pCnt 𝑁)))
109		prmz 16850	. . . . . . . . . . . . 13 ⊢ (𝑘 ∈ ℙ → 𝑘 ∈ ℤ)
110		lgscl 27638	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ ℤ ∧ 𝑘 ∈ ℤ) → (𝐴 /_L 𝑘) ∈ ℤ)
111	86, 109, 110	syl2an 608	. . . . . . . . . . . 12 ⊢ (((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 ≠ 0) ∧ 𝑘 ∈ ℙ) → (𝐴 /_L 𝑘) ∈ ℤ)
112	111	zcnd 12804	. . . . . . . . . . 11 ⊢ (((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 ≠ 0) ∧ 𝑘 ∈ ℙ) → (𝐴 /_L 𝑘) ∈ ℂ)
113		lgscl 27638	. . . . . . . . . . . . 13 ⊢ ((𝐵 ∈ ℤ ∧ 𝑘 ∈ ℤ) → (𝐵 /_L 𝑘) ∈ ℤ)
114	96, 109, 113	syl2an 608	. . . . . . . . . . . 12 ⊢ (((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 ≠ 0) ∧ 𝑘 ∈ ℙ) → (𝐵 /_L 𝑘) ∈ ℤ)
115	114	zcnd 12804	. . . . . . . . . . 11 ⊢ (((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 ≠ 0) ∧ 𝑘 ∈ ℙ) → (𝐵 /_L 𝑘) ∈ ℂ)
116	87	adantr 486	. . . . . . . . . . . 12 ⊢ (((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 ≠ 0) ∧ 𝑘 ∈ ℙ) → 𝑁 ∈ ℤ)
117	88	adantr 486	. . . . . . . . . . . 12 ⊢ (((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 ≠ 0) ∧ 𝑘 ∈ ℙ) → 𝑁 ≠ 0)
118		pczcl 17026	. . . . . . . . . . . 12 ⊢ ((𝑘 ∈ ℙ ∧ (𝑁 ∈ ℤ ∧ 𝑁 ≠ 0)) → (𝑘 pCnt 𝑁) ∈ ℕ₀)
119	105, 116, 117, 118	syl12anc 850	. . . . . . . . . . 11 ⊢ (((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 ≠ 0) ∧ 𝑘 ∈ ℙ) → (𝑘 pCnt 𝑁) ∈ ℕ₀)
120	112, 115, 119	mulexpd 14304	. . . . . . . . . 10 ⊢ (((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 ≠ 0) ∧ 𝑘 ∈ ℙ) → (((𝐴 /_L 𝑘) · (𝐵 /_L 𝑘))↑(𝑘 pCnt 𝑁)) = (((𝐴 /_L 𝑘)↑(𝑘 pCnt 𝑁)) · ((𝐵 /_L 𝑘)↑(𝑘 pCnt 𝑁))))
121	108, 120	eqtrd 2796	. . . . . . . . 9 ⊢ (((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 ≠ 0) ∧ 𝑘 ∈ ℙ) → (((𝐴 · 𝐵) /_L 𝑘)↑(𝑘 pCnt 𝑁)) = (((𝐴 /_L 𝑘)↑(𝑘 pCnt 𝑁)) · ((𝐵 /_L 𝑘)↑(𝑘 pCnt 𝑁))))
122		iftrue 4488	. . . . . . . . . 10 ⊢ (𝑘 ∈ ℙ → if(𝑘 ∈ ℙ, (((𝐴 · 𝐵) /_L 𝑘)↑(𝑘 pCnt 𝑁)), 1) = (((𝐴 · 𝐵) /_L 𝑘)↑(𝑘 pCnt 𝑁)))
123	122	adantl 487	. . . . . . . . 9 ⊢ (((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 ≠ 0) ∧ 𝑘 ∈ ℙ) → if(𝑘 ∈ ℙ, (((𝐴 · 𝐵) /_L 𝑘)↑(𝑘 pCnt 𝑁)), 1) = (((𝐴 · 𝐵) /_L 𝑘)↑(𝑘 pCnt 𝑁)))
124		iftrue 4488	. . . . . . . . . . 11 ⊢ (𝑘 ∈ ℙ → if(𝑘 ∈ ℙ, ((𝐴 /_L 𝑘)↑(𝑘 pCnt 𝑁)), 1) = ((𝐴 /_L 𝑘)↑(𝑘 pCnt 𝑁)))
125		iftrue 4488	. . . . . . . . . . 11 ⊢ (𝑘 ∈ ℙ → if(𝑘 ∈ ℙ, ((𝐵 /_L 𝑘)↑(𝑘 pCnt 𝑁)), 1) = ((𝐵 /_L 𝑘)↑(𝑘 pCnt 𝑁)))
126	124, 125	oveq12d 7438	. . . . . . . . . 10 ⊢ (𝑘 ∈ ℙ → (if(𝑘 ∈ ℙ, ((𝐴 /_L 𝑘)↑(𝑘 pCnt 𝑁)), 1) · if(𝑘 ∈ ℙ, ((𝐵 /_L 𝑘)↑(𝑘 pCnt 𝑁)), 1)) = (((𝐴 /_L 𝑘)↑(𝑘 pCnt 𝑁)) · ((𝐵 /_L 𝑘)↑(𝑘 pCnt 𝑁))))
127	126	adantl 487	. . . . . . . . 9 ⊢ (((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 ≠ 0) ∧ 𝑘 ∈ ℙ) → (if(𝑘 ∈ ℙ, ((𝐴 /_L 𝑘)↑(𝑘 pCnt 𝑁)), 1) · if(𝑘 ∈ ℙ, ((𝐵 /_L 𝑘)↑(𝑘 pCnt 𝑁)), 1)) = (((𝐴 /_L 𝑘)↑(𝑘 pCnt 𝑁)) · ((𝐵 /_L 𝑘)↑(𝑘 pCnt 𝑁))))
128	121, 123, 127	3eqtr4d 2806	. . . . . . . 8 ⊢ (((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 ≠ 0) ∧ 𝑘 ∈ ℙ) → if(𝑘 ∈ ℙ, (((𝐴 · 𝐵) /_L 𝑘)↑(𝑘 pCnt 𝑁)), 1) = (if(𝑘 ∈ ℙ, ((𝐴 /_L 𝑘)↑(𝑘 pCnt 𝑁)), 1) · if(𝑘 ∈ ℙ, ((𝐵 /_L 𝑘)↑(𝑘 pCnt 𝑁)), 1)))
129		1t1e1 12504	. . . . . . . . . . 11 ⊢ (1 · 1) = 1
130	129	eqcomi 2770	. . . . . . . . . 10 ⊢ 1 = (1 · 1)
131		iffalse 4491	. . . . . . . . . 10 ⊢ (¬ 𝑘 ∈ ℙ → if(𝑘 ∈ ℙ, (((𝐴 · 𝐵) /_L 𝑘)↑(𝑘 pCnt 𝑁)), 1) = 1)
132		iffalse 4491	. . . . . . . . . . 11 ⊢ (¬ 𝑘 ∈ ℙ → if(𝑘 ∈ ℙ, ((𝐴 /_L 𝑘)↑(𝑘 pCnt 𝑁)), 1) = 1)
133		iffalse 4491	. . . . . . . . . . 11 ⊢ (¬ 𝑘 ∈ ℙ → if(𝑘 ∈ ℙ, ((𝐵 /_L 𝑘)↑(𝑘 pCnt 𝑁)), 1) = 1)
134	132, 133	oveq12d 7438	. . . . . . . . . 10 ⊢ (¬ 𝑘 ∈ ℙ → (if(𝑘 ∈ ℙ, ((𝐴 /_L 𝑘)↑(𝑘 pCnt 𝑁)), 1) · if(𝑘 ∈ ℙ, ((𝐵 /_L 𝑘)↑(𝑘 pCnt 𝑁)), 1)) = (1 · 1))
135	130, 131, 134	3eqtr4a 2822	. . . . . . . . 9 ⊢ (¬ 𝑘 ∈ ℙ → if(𝑘 ∈ ℙ, (((𝐴 · 𝐵) /_L 𝑘)↑(𝑘 pCnt 𝑁)), 1) = (if(𝑘 ∈ ℙ, ((𝐴 /_L 𝑘)↑(𝑘 pCnt 𝑁)), 1) · if(𝑘 ∈ ℙ, ((𝐵 /_L 𝑘)↑(𝑘 pCnt 𝑁)), 1)))
136	135	adantl 487	. . . . . . . 8 ⊢ (((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 ≠ 0) ∧ ¬ 𝑘 ∈ ℙ) → if(𝑘 ∈ ℙ, (((𝐴 · 𝐵) /_L 𝑘)↑(𝑘 pCnt 𝑁)), 1) = (if(𝑘 ∈ ℙ, ((𝐴 /_L 𝑘)↑(𝑘 pCnt 𝑁)), 1) · if(𝑘 ∈ ℙ, ((𝐵 /_L 𝑘)↑(𝑘 pCnt 𝑁)), 1)))
137	128, 136	pm2.61dan 825	. . . . . . 7 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 ≠ 0) → if(𝑘 ∈ ℙ, (((𝐴 · 𝐵) /_L 𝑘)↑(𝑘 pCnt 𝑁)), 1) = (if(𝑘 ∈ ℙ, ((𝐴 /_L 𝑘)↑(𝑘 pCnt 𝑁)), 1) · if(𝑘 ∈ ℙ, ((𝐵 /_L 𝑘)↑(𝑘 pCnt 𝑁)), 1)))
138	137	adantr 486	. . . . . 6 ⊢ (((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 ≠ 0) ∧ 𝑘 ∈ (1...(abs‘𝑁))) → if(𝑘 ∈ ℙ, (((𝐴 · 𝐵) /_L 𝑘)↑(𝑘 pCnt 𝑁)), 1) = (if(𝑘 ∈ ℙ, ((𝐴 /_L 𝑘)↑(𝑘 pCnt 𝑁)), 1) · if(𝑘 ∈ ℙ, ((𝐵 /_L 𝑘)↑(𝑘 pCnt 𝑁)), 1)))
139	92	adantl 487	. . . . . . 7 ⊢ (((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 ≠ 0) ∧ 𝑘 ∈ (1...(abs‘𝑁))) → 𝑘 ∈ ℕ)
140		eleq1w 2844	. . . . . . . . 9 ⊢ (𝑛 = 𝑘 → (𝑛 ∈ ℙ ↔ 𝑘 ∈ ℙ))
141		oveq2 7428	. . . . . . . . . 10 ⊢ (𝑛 = 𝑘 → ((𝐴 · 𝐵) /_L 𝑛) = ((𝐴 · 𝐵) /_L 𝑘))
142		oveq1 7427	. . . . . . . . . 10 ⊢ (𝑛 = 𝑘 → (𝑛 pCnt 𝑁) = (𝑘 pCnt 𝑁))
143	141, 142	oveq12d 7438	. . . . . . . . 9 ⊢ (𝑛 = 𝑘 → (((𝐴 · 𝐵) /_L 𝑛)↑(𝑛 pCnt 𝑁)) = (((𝐴 · 𝐵) /_L 𝑘)↑(𝑘 pCnt 𝑁)))
144	140, 143	ifbieq1d 4507	. . . . . . . 8 ⊢ (𝑛 = 𝑘 → if(𝑛 ∈ ℙ, (((𝐴 · 𝐵) /_L 𝑛)↑(𝑛 pCnt 𝑁)), 1) = if(𝑘 ∈ ℙ, (((𝐴 · 𝐵) /_L 𝑘)↑(𝑘 pCnt 𝑁)), 1))
145		eqid 2761	. . . . . . . 8 ⊢ (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, (((𝐴 · 𝐵) /_L 𝑛)↑(𝑛 pCnt 𝑁)), 1)) = (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, (((𝐴 · 𝐵) /_L 𝑛)↑(𝑛 pCnt 𝑁)), 1))
146		ovex 7453	. . . . . . . . 9 ⊢ (((𝐴 · 𝐵) /_L 𝑘)↑(𝑘 pCnt 𝑁)) ∈ V
147		1ex 11303	. . . . . . . . 9 ⊢ 1 ∈ V
148	146, 147	ifex 4533	. . . . . . . 8 ⊢ if(𝑘 ∈ ℙ, (((𝐴 · 𝐵) /_L 𝑘)↑(𝑘 pCnt 𝑁)), 1) ∈ V
149	144, 145, 148	fvmpt 6993	. . . . . . 7 ⊢ (𝑘 ∈ ℕ → ((𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, (((𝐴 · 𝐵) /_L 𝑛)↑(𝑛 pCnt 𝑁)), 1))‘𝑘) = if(𝑘 ∈ ℙ, (((𝐴 · 𝐵) /_L 𝑘)↑(𝑘 pCnt 𝑁)), 1))
150	139, 149	syl 18	. . . . . 6 ⊢ (((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 ≠ 0) ∧ 𝑘 ∈ (1...(abs‘𝑁))) → ((𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, (((𝐴 · 𝐵) /_L 𝑛)↑(𝑛 pCnt 𝑁)), 1))‘𝑘) = if(𝑘 ∈ ℙ, (((𝐴 · 𝐵) /_L 𝑘)↑(𝑘 pCnt 𝑁)), 1))
151		oveq2 7428	. . . . . . . . . . 11 ⊢ (𝑛 = 𝑘 → (𝐴 /_L 𝑛) = (𝐴 /_L 𝑘))
152	151, 142	oveq12d 7438	. . . . . . . . . 10 ⊢ (𝑛 = 𝑘 → ((𝐴 /_L 𝑛)↑(𝑛 pCnt 𝑁)) = ((𝐴 /_L 𝑘)↑(𝑘 pCnt 𝑁)))
153	140, 152	ifbieq1d 4507	. . . . . . . . 9 ⊢ (𝑛 = 𝑘 → if(𝑛 ∈ ℙ, ((𝐴 /_L 𝑛)↑(𝑛 pCnt 𝑁)), 1) = if(𝑘 ∈ ℙ, ((𝐴 /_L 𝑘)↑(𝑘 pCnt 𝑁)), 1))
154		ovex 7453	. . . . . . . . . 10 ⊢ ((𝐴 /_L 𝑘)↑(𝑘 pCnt 𝑁)) ∈ V
155	154, 147	ifex 4533	. . . . . . . . 9 ⊢ if(𝑘 ∈ ℙ, ((𝐴 /_L 𝑘)↑(𝑘 pCnt 𝑁)), 1) ∈ V
156	153, 89, 155	fvmpt 6993	. . . . . . . 8 ⊢ (𝑘 ∈ ℕ → ((𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /_L 𝑛)↑(𝑛 pCnt 𝑁)), 1))‘𝑘) = if(𝑘 ∈ ℙ, ((𝐴 /_L 𝑘)↑(𝑘 pCnt 𝑁)), 1))
157	139, 156	syl 18	. . . . . . 7 ⊢ (((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 ≠ 0) ∧ 𝑘 ∈ (1...(abs‘𝑁))) → ((𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /_L 𝑛)↑(𝑛 pCnt 𝑁)), 1))‘𝑘) = if(𝑘 ∈ ℙ, ((𝐴 /_L 𝑘)↑(𝑘 pCnt 𝑁)), 1))
158		oveq2 7428	. . . . . . . . . . 11 ⊢ (𝑛 = 𝑘 → (𝐵 /_L 𝑛) = (𝐵 /_L 𝑘))
159	158, 142	oveq12d 7438	. . . . . . . . . 10 ⊢ (𝑛 = 𝑘 → ((𝐵 /_L 𝑛)↑(𝑛 pCnt 𝑁)) = ((𝐵 /_L 𝑘)↑(𝑘 pCnt 𝑁)))
160	140, 159	ifbieq1d 4507	. . . . . . . . 9 ⊢ (𝑛 = 𝑘 → if(𝑛 ∈ ℙ, ((𝐵 /_L 𝑛)↑(𝑛 pCnt 𝑁)), 1) = if(𝑘 ∈ ℙ, ((𝐵 /_L 𝑘)↑(𝑘 pCnt 𝑁)), 1))
161		ovex 7453	. . . . . . . . . 10 ⊢ ((𝐵 /_L 𝑘)↑(𝑘 pCnt 𝑁)) ∈ V
162	161, 147	ifex 4533	. . . . . . . . 9 ⊢ if(𝑘 ∈ ℙ, ((𝐵 /_L 𝑘)↑(𝑘 pCnt 𝑁)), 1) ∈ V
163	160, 97, 162	fvmpt 6993	. . . . . . . 8 ⊢ (𝑘 ∈ ℕ → ((𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐵 /_L 𝑛)↑(𝑛 pCnt 𝑁)), 1))‘𝑘) = if(𝑘 ∈ ℙ, ((𝐵 /_L 𝑘)↑(𝑘 pCnt 𝑁)), 1))
164	139, 163	syl 18	. . . . . . 7 ⊢ (((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 ≠ 0) ∧ 𝑘 ∈ (1...(abs‘𝑁))) → ((𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐵 /_L 𝑛)↑(𝑛 pCnt 𝑁)), 1))‘𝑘) = if(𝑘 ∈ ℙ, ((𝐵 /_L 𝑘)↑(𝑘 pCnt 𝑁)), 1))
165	157, 164	oveq12d 7438	. . . . . 6 ⊢ (((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 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 2806	. . . . 5 ⊢ (((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 ≠ 0) ∧ 𝑘 ∈ (1...(abs‘𝑁))) → ((𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, (((𝐴 · 𝐵) /_L 𝑛)↑(𝑛 pCnt 𝑁)), 1))‘𝑘) = (((𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /_L 𝑛)↑(𝑛 pCnt 𝑁)), 1))‘𝑘) · ((𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐵 /_L 𝑛)↑(𝑛 pCnt 𝑁)), 1))‘𝑘)))
167	85, 95, 102, 166	prodfmul 16059	. . . 4 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 ≠ 0) → (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, (((𝐴 · 𝐵) /_L 𝑛)↑(𝑛 pCnt 𝑁)), 1)))‘(abs‘𝑁)) = ((seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /_L 𝑛)↑(𝑛 pCnt 𝑁)), 1)))‘(abs‘𝑁)) · (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐵 /_L 𝑛)↑(𝑛 pCnt 𝑁)), 1)))‘(abs‘𝑁))))
168	80, 167	oveq12d 7438	. . 3 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 ≠ 0) → (if((𝑁 < 0 ∧ (𝐴 · 𝐵) < 0), -1, 1) · (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, (((𝐴 · 𝐵) /_L 𝑛)↑(𝑛 pCnt 𝑁)), 1)))‘(abs‘𝑁))) = ((if((𝑁 < 0 ∧ 𝐴 < 0), -1, 1) · if((𝑁 < 0 ∧ 𝐵 < 0), -1, 1)) · ((seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /_L 𝑛)↑(𝑛 pCnt 𝑁)), 1)))‘(abs‘𝑁)) · (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐵 /_L 𝑛)↑(𝑛 pCnt 𝑁)), 1)))‘(abs‘𝑁)))))
169	30	adantr 486	. . . 4 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 ≠ 0) → (𝐴 · 𝐵) ∈ ℤ)
170	145	lgsval4 27644	. . . 4 ⊢ (((𝐴 · 𝐵) ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) → ((𝐴 · 𝐵) /_L 𝑁) = (if((𝑁 < 0 ∧ (𝐴 · 𝐵) < 0), -1, 1) · (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, (((𝐴 · 𝐵) /_L 𝑛)↑(𝑛 pCnt 𝑁)), 1)))‘(abs‘𝑁))))
171	169, 87, 88, 170	syl3anc 1398	. . 3 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 ≠ 0) → ((𝐴 · 𝐵) /_L 𝑁) = (if((𝑁 < 0 ∧ (𝐴 · 𝐵) < 0), -1, 1) · (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, (((𝐴 · 𝐵) /_L 𝑛)↑(𝑛 pCnt 𝑁)), 1)))‘(abs‘𝑁))))
172	89	lgsval4 27644	. . . . . 6 ⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) → (𝐴 /_L 𝑁) = (if((𝑁 < 0 ∧ 𝐴 < 0), -1, 1) · (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /_L 𝑛)↑(𝑛 pCnt 𝑁)), 1)))‘(abs‘𝑁))))
173	86, 87, 88, 172	syl3anc 1398	. . . . 5 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 ≠ 0) → (𝐴 /_L 𝑁) = (if((𝑁 < 0 ∧ 𝐴 < 0), -1, 1) · (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /_L 𝑛)↑(𝑛 pCnt 𝑁)), 1)))‘(abs‘𝑁))))
174	97	lgsval4 27644	. . . . . 6 ⊢ ((𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) → (𝐵 /_L 𝑁) = (if((𝑁 < 0 ∧ 𝐵 < 0), -1, 1) · (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐵 /_L 𝑛)↑(𝑛 pCnt 𝑁)), 1)))‘(abs‘𝑁))))
175	96, 87, 88, 174	syl3anc 1398	. . . . 5 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 ≠ 0) → (𝐵 /_L 𝑁) = (if((𝑁 < 0 ∧ 𝐵 < 0), -1, 1) · (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐵 /_L 𝑛)↑(𝑛 pCnt 𝑁)), 1)))‘(abs‘𝑁))))
176	173, 175	oveq12d 7438	. . . 4 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 ≠ 0) → ((𝐴 /_L 𝑁) · (𝐵 /_L 𝑁)) = ((if((𝑁 < 0 ∧ 𝐴 < 0), -1, 1) · (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /_L 𝑛)↑(𝑛 pCnt 𝑁)), 1)))‘(abs‘𝑁))) · (if((𝑁 < 0 ∧ 𝐵 < 0), -1, 1) · (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐵 /_L 𝑛)↑(𝑛 pCnt 𝑁)), 1)))‘(abs‘𝑁)))))
177		neg1cn 12305	. . . . . . 7 ⊢ -1 ∈ ℂ
178	177, 1	ifcli 4530	. . . . . 6 ⊢ if((𝑁 < 0 ∧ 𝐴 < 0), -1, 1) ∈ ℂ
179	178	a1i 11	. . . . 5 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 ≠ 0) → if((𝑁 < 0 ∧ 𝐴 < 0), -1, 1) ∈ ℂ)
180		mulcl 11284	. . . . . . 7 ⊢ ((𝑘 ∈ ℂ ∧ 𝑥 ∈ ℂ) → (𝑘 · 𝑥) ∈ ℂ)
181	180	adantl 487	. . . . . 6 ⊢ (((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 ≠ 0) ∧ (𝑘 ∈ ℂ ∧ 𝑥 ∈ ℂ)) → (𝑘 · 𝑥) ∈ ℂ)
182	85, 95, 181	seqcl 14165	. . . . 5 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 ≠ 0) → (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /_L 𝑛)↑(𝑛 pCnt 𝑁)), 1)))‘(abs‘𝑁)) ∈ ℂ)
183	177, 1	ifcli 4530	. . . . . 6 ⊢ if((𝑁 < 0 ∧ 𝐵 < 0), -1, 1) ∈ ℂ
184	183	a1i 11	. . . . 5 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 ≠ 0) → if((𝑁 < 0 ∧ 𝐵 < 0), -1, 1) ∈ ℂ)
185	85, 102, 181	seqcl 14165	. . . . 5 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 ≠ 0) → (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐵 /_L 𝑛)↑(𝑛 pCnt 𝑁)), 1)))‘(abs‘𝑁)) ∈ ℂ)
186	179, 182, 184, 185	mul4d 11522	. . . 4 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 ≠ 0) → ((if((𝑁 < 0 ∧ 𝐴 < 0), -1, 1) · (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /_L 𝑛)↑(𝑛 pCnt 𝑁)), 1)))‘(abs‘𝑁))) · (if((𝑁 < 0 ∧ 𝐵 < 0), -1, 1) · (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐵 /_L 𝑛)↑(𝑛 pCnt 𝑁)), 1)))‘(abs‘𝑁)))) = ((if((𝑁 < 0 ∧ 𝐴 < 0), -1, 1) · if((𝑁 < 0 ∧ 𝐵 < 0), -1, 1)) · ((seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /_L 𝑛)↑(𝑛 pCnt 𝑁)), 1)))‘(abs‘𝑁)) · (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐵 /_L 𝑛)↑(𝑛 pCnt 𝑁)), 1)))‘(abs‘𝑁)))))
187	176, 186	eqtrd 2796	. . 3 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 ≠ 0) → ((𝐴 /_L 𝑁) · (𝐵 /_L 𝑁)) = ((if((𝑁 < 0 ∧ 𝐴 < 0), -1, 1) · if((𝑁 < 0 ∧ 𝐵 < 0), -1, 1)) · ((seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /_L 𝑛)↑(𝑛 pCnt 𝑁)), 1)))‘(abs‘𝑁)) · (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐵 /_L 𝑛)↑(𝑛 pCnt 𝑁)), 1)))‘(abs‘𝑁)))))
188	168, 171, 187	3eqtr4d 2806	. 2 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 ≠ 0) → ((𝐴 · 𝐵) /_L 𝑁) = ((𝐴 /_L 𝑁) · (𝐵 /_L 𝑁)))
189	78, 188	pm2.61dane 3043	1 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) → ((𝐴 · 𝐵) /_L 𝑁) = ((𝐴 /_L 𝑁) · (𝐵 /_L 𝑁)))

Colors of variables: wff setvar class

This proof depends on syntax axioms: ¬ wn 3 → wi 4 ↔ wb 209 ∧ wa 401 ∨ wo 861 ∧ w3a 1103 = wceq 1570 ∈ wcel 2145 ≠ wne 2956 ifcif 4482 class class class wbr 5103 ↦ cmpt 5186 ⟶wf 6534 ‘cfv 6538 (class class class)co 7420 ℂcc 11198 ℝcr 11199 0cc0 11200 1c1 11201 · cmul 11205 < clt 11343 ≤ cle 11344 -cneg 11542 ℕcn 12335 2c2 12397 ℕ₀cn0 12606 ℤcz 12693 ℤ_≥cuz 12965 ...cfz 13639 seqcseq 14144 ↑cexp 14204 abscabs 15401 ∥ cdvds 16422 ℙcprime 16846 pCnt cpc 17014 /_L clgs 27621

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1943 ax-6 2000 ax-7 2041 ax-8 2147 ax-9 2155 ax-10 2178 ax-11 2194 ax-12 2213 ax-ext 2733 ax-rep 5232 ax-sep 5249 ax-nul 5260 ax-pow 5327 ax-pr 5391 ax-un 7751 ax-cnex 11256 ax-resscn 11257 ax-1cn 11258 ax-icn 11259 ax-addcl 11260 ax-addrcl 11261 ax-mulcl 11262 ax-mulrcl 11263 ax-mulcom 11264 ax-addass 11265 ax-mulass 11266 ax-distr 11267 ax-i2m1 11268 ax-1ne0 11269 ax-1rid 11270 ax-rnegex 11271 ax-rrecex 11272 ax-cnre 11273 ax-pre-lttri 11274 ax-pre-lttrn 11275 ax-pre-ltadd 11276 ax-pre-mulgt0 11277 ax-pre-sup 11278

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1813 df-nf 1817 df-sb 2100 df-mo 2565 df-eu 2595 df-clab 2740 df-cleq 2753 df-clel 2836 df-nfc 2910 df-ne 2957 df-nel 3063 df-ral 3078 df-rex 3088 df-rmo 3366 df-reu 3367 df-rab 3414 df-v 3453 df-sbc 3740 df-csb 3848 df-dif 3902 df-un 3904 df-in 3906 df-ss 3916 df-pss 3919 df-nul 4280 df-if 4483 df-pw 4559 df-sn 4585 df-pr 4587 df-op 4591 df-uni 4868 df-int 4908 df-iun 4953 df-br 5104 df-opab 5168 df-mpt 5187 df-tr 5213 df-id 5546 df-eprel 5551 df-po 5559 df-so 5560 df-fr 5604 df-we 5606 df-xp 5657 df-rel 5658 df-cnv 5659 df-co 5660 df-dm 5661 df-rn 5662 df-res 5663 df-ima 5664 df-pred 6304 df-ord 6365 df-on 6366 df-lim 6367 df-suc 6368 df-iota 6494 df-fun 6540 df-fn 6541 df-f 6542 df-f1 6543 df-fo 6544 df-f1o 6545 df-fv 6546 df-riota 7377 df-ov 7423 df-oprab 7424 df-mpo 7425 df-om 7878 df-1st 8001 df-2nd 8002 df-frecs 8299 df-wrecs 8330 df-recs 8379 df-rdg 8418 df-1o 8476 df-2o 8477 df-oadd 8480 df-er 8717 df-en 8974 df-dom 8975 df-sdom 8976 df-fin 8977 df-sup 9434 df-inf 9435 df-dju 9982 df-card 10020 df-pnf 11345 df-mnf 11346 df-xr 11347 df-ltxr 11348 df-le 11349 df-sub 11543 df-neg 11544 df-div 11974 df-nn 12336 df-2 12405 df-3 12406 df-4 12407 df-5 12408 df-6 12409 df-7 12410 df-8 12411 df-9 12412 df-n0 12607 df-xnn0 12680 df-z 12694 df-uz 12966 df-q 13076 df-rp 13121 df-fz 13640 df-fzo 13789 df-fl 13932 df-mod 14010 df-seq 14145 df-exp 14205 df-hash 14475 df-cj 15266 df-re 15267 df-im 15268 df-sqrt 15402 df-abs 15403 df-dvds 16423 df-gcd 16665 df-prm 16847 df-phi 16943 df-pc 17015 df-lgs 27622

This theorem is used by: lgssq 27664 lgsmulsqcoprm 27670 lgsdirnn0 27671 lgsquad2lem1 27711

W3C validator