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 27241

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 27260 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 11067	. . . . . . 7 ⊢ 1 ∈ ℂ
2		0cn 11107	. . . . . . 7 ⊢ 0 ∈ ℂ
3	1, 2	ifcli 4524	. . . . . 6 ⊢ if((𝐵↑2) = 1, 1, 0) ∈ ℂ
4	3	mullidi 11120	. . . . 5 ⊢ (1 · if((𝐵↑2) = 1, 1, 0)) = if((𝐵↑2) = 1, 1, 0)
5		iftrue 4482	. . . . . . 7 ⊢ ((𝐴↑2) = 1 → if((𝐴↑2) = 1, 1, 0) = 1)
6	5	adantl 481	. . . . . 6 ⊢ (((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 = 0) ∧ (𝐴↑2) = 1) → if((𝐴↑2) = 1, 1, 0) = 1)
7	6	oveq1d 7364	. . . . 5 ⊢ (((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 = 0) ∧ (𝐴↑2) = 1) → (if((𝐴↑2) = 1, 1, 0) · if((𝐵↑2) = 1, 1, 0)) = (1 · if((𝐵↑2) = 1, 1, 0)))
8		simpl1 1192	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) → 𝐴 ∈ ℤ)
9	8	zcnd 12581	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) → 𝐴 ∈ ℂ)
10	9	ad2antrr 726	. . . . . . . . 9 ⊢ (((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 = 0) ∧ (𝐴↑2) = 1) → 𝐴 ∈ ℂ)
11		simpl2 1193	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) → 𝐵 ∈ ℤ)
12	11	zcnd 12581	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) → 𝐵 ∈ ℂ)
13	12	ad2antrr 726	. . . . . . . . 9 ⊢ (((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 = 0) ∧ (𝐴↑2) = 1) → 𝐵 ∈ ℂ)
14	10, 13	sqmuld 14065	. . . . . . . 8 ⊢ (((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 = 0) ∧ (𝐴↑2) = 1) → ((𝐴 · 𝐵)↑2) = ((𝐴↑2) · (𝐵↑2)))
15		simpr 484	. . . . . . . . 9 ⊢ (((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 = 0) ∧ (𝐴↑2) = 1) → (𝐴↑2) = 1)
16	15	oveq1d 7364	. . . . . . . 8 ⊢ (((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 = 0) ∧ (𝐴↑2) = 1) → ((𝐴↑2) · (𝐵↑2)) = (1 · (𝐵↑2)))
17	12	sqcld 14051	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) → (𝐵↑2) ∈ ℂ)
18	17	ad2antrr 726	. . . . . . . . 9 ⊢ (((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 = 0) ∧ (𝐴↑2) = 1) → (𝐵↑2) ∈ ℂ)
19	18	mullidd 11133	. . . . . . . 8 ⊢ (((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 = 0) ∧ (𝐴↑2) = 1) → (1 · (𝐵↑2)) = (𝐵↑2))
20	14, 16, 19	3eqtrd 2768	. . . . . . 7 ⊢ (((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 = 0) ∧ (𝐴↑2) = 1) → ((𝐴 · 𝐵)↑2) = (𝐵↑2))
21	20	eqeq1d 2731	. . . . . 6 ⊢ (((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 = 0) ∧ (𝐴↑2) = 1) → (((𝐴 · 𝐵)↑2) = 1 ↔ (𝐵↑2) = 1))
22	21	ifbid 4500	. . . . 5 ⊢ (((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 = 0) ∧ (𝐴↑2) = 1) → if(((𝐴 · 𝐵)↑2) = 1, 1, 0) = if((𝐵↑2) = 1, 1, 0))
23	4, 7, 22	3eqtr4a 2790	. . . 4 ⊢ (((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 = 0) ∧ (𝐴↑2) = 1) → (if((𝐴↑2) = 1, 1, 0) · if((𝐵↑2) = 1, 1, 0)) = if(((𝐴 · 𝐵)↑2) = 1, 1, 0))
24	3	mul02i 11305	. . . . 5 ⊢ (0 · if((𝐵↑2) = 1, 1, 0)) = 0
25		iffalse 4485	. . . . . . 7 ⊢ (¬ (𝐴↑2) = 1 → if((𝐴↑2) = 1, 1, 0) = 0)
26	25	adantl 481	. . . . . 6 ⊢ (((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 = 0) ∧ ¬ (𝐴↑2) = 1) → if((𝐴↑2) = 1, 1, 0) = 0)
27	26	oveq1d 7364	. . . . 5 ⊢ (((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 = 0) ∧ ¬ (𝐴↑2) = 1) → (if((𝐴↑2) = 1, 1, 0) · if((𝐵↑2) = 1, 1, 0)) = (0 · if((𝐵↑2) = 1, 1, 0)))
28		dvdsmul1 16188	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → 𝐴 ∥ (𝐴 · 𝐵))
29	8, 11, 28	syl2anc 584	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) → 𝐴 ∥ (𝐴 · 𝐵))
30	8, 11	zmulcld 12586	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) → (𝐴 · 𝐵) ∈ ℤ)
31		dvdssq 16478	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ ℤ ∧ (𝐴 · 𝐵) ∈ ℤ) → (𝐴 ∥ (𝐴 · 𝐵) ↔ (𝐴↑2) ∥ ((𝐴 · 𝐵)↑2)))
32	8, 30, 31	syl2anc 584	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) → (𝐴 ∥ (𝐴 · 𝐵) ↔ (𝐴↑2) ∥ ((𝐴 · 𝐵)↑2)))
33	29, 32	mpbid 232	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) → (𝐴↑2) ∥ ((𝐴 · 𝐵)↑2))
34	33	adantr 480	. . . . . . . . 9 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 = 0) → (𝐴↑2) ∥ ((𝐴 · 𝐵)↑2))
35		breq2 5096	. . . . . . . . 9 ⊢ (((𝐴 · 𝐵)↑2) = 1 → ((𝐴↑2) ∥ ((𝐴 · 𝐵)↑2) ↔ (𝐴↑2) ∥ 1))
36	34, 35	syl5ibcom 245	. . . . . . . 8 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 = 0) → (((𝐴 · 𝐵)↑2) = 1 → (𝐴↑2) ∥ 1))
37		simprl 770	. . . . . . . . . . . . . . . 16 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) → 𝐴 ≠ 0)
38	37	neneqd 2930	. . . . . . . . . . . . . . 15 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) → ¬ 𝐴 = 0)
39		sqeq0 14027	. . . . . . . . . . . . . . . 16 ⊢ (𝐴 ∈ ℂ → ((𝐴↑2) = 0 ↔ 𝐴 = 0))
40	9, 39	syl 17	. . . . . . . . . . . . . . 15 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) → ((𝐴↑2) = 0 ↔ 𝐴 = 0))
41	38, 40	mtbird 325	. . . . . . . . . . . . . 14 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) → ¬ (𝐴↑2) = 0)
42		zsqcl2 14045	. . . . . . . . . . . . . . . . 17 ⊢ (𝐴 ∈ ℤ → (𝐴↑2) ∈ ℕ₀)
43	8, 42	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) → (𝐴↑2) ∈ ℕ₀)
44		elnn0 12386	. . . . . . . . . . . . . . . 16 ⊢ ((𝐴↑2) ∈ ℕ₀ ↔ ((𝐴↑2) ∈ ℕ ∨ (𝐴↑2) = 0))
45	43, 44	sylib 218	. . . . . . . . . . . . . . 15 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) → ((𝐴↑2) ∈ ℕ ∨ (𝐴↑2) = 0))
46	45	ord 864	. . . . . . . . . . . . . 14 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) → (¬ (𝐴↑2) ∈ ℕ → (𝐴↑2) = 0))
47	41, 46	mt3d 148	. . . . . . . . . . . . 13 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) → (𝐴↑2) ∈ ℕ)
48	47	adantr 480	. . . . . . . . . . . 12 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 = 0) → (𝐴↑2) ∈ ℕ)
49	48	nnzd 12498	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 = 0) → (𝐴↑2) ∈ ℤ)
50		1nn 12139	. . . . . . . . . . 11 ⊢ 1 ∈ ℕ
51		dvdsle 16221	. . . . . . . . . . 11 ⊢ (((𝐴↑2) ∈ ℤ ∧ 1 ∈ ℕ) → ((𝐴↑2) ∥ 1 → (𝐴↑2) ≤ 1))
52	49, 50, 51	sylancl 586	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 = 0) → ((𝐴↑2) ∥ 1 → (𝐴↑2) ≤ 1))
53	48	nnge1d 12176	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 = 0) → 1 ≤ (𝐴↑2))
54	52, 53	jctird 526	. . . . . . . . 9 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 = 0) → ((𝐴↑2) ∥ 1 → ((𝐴↑2) ≤ 1 ∧ 1 ≤ (𝐴↑2))))
55	48	nnred 12143	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 = 0) → (𝐴↑2) ∈ ℝ)
56		1re 11115	. . . . . . . . . 10 ⊢ 1 ∈ ℝ
57		letri3 11201	. . . . . . . . . 10 ⊢ (((𝐴↑2) ∈ ℝ ∧ 1 ∈ ℝ) → ((𝐴↑2) = 1 ↔ ((𝐴↑2) ≤ 1 ∧ 1 ≤ (𝐴↑2))))
58	55, 56, 57	sylancl 586	. . . . . . . . 9 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 = 0) → ((𝐴↑2) = 1 ↔ ((𝐴↑2) ≤ 1 ∧ 1 ≤ (𝐴↑2))))
59	54, 58	sylibrd 259	. . . . . . . 8 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 = 0) → ((𝐴↑2) ∥ 1 → (𝐴↑2) = 1))
60	36, 59	syld 47	. . . . . . 7 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 = 0) → (((𝐴 · 𝐵)↑2) = 1 → (𝐴↑2) = 1))
61	60	con3dimp 408	. . . . . 6 ⊢ (((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 = 0) ∧ ¬ (𝐴↑2) = 1) → ¬ ((𝐴 · 𝐵)↑2) = 1)
62	61	iffalsed 4487	. . . . 5 ⊢ (((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 = 0) ∧ ¬ (𝐴↑2) = 1) → if(((𝐴 · 𝐵)↑2) = 1, 1, 0) = 0)
63	24, 27, 62	3eqtr4a 2790	. . . 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 812	. . 3 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 = 0) → (if((𝐴↑2) = 1, 1, 0) · if((𝐵↑2) = 1, 1, 0)) = if(((𝐴 · 𝐵)↑2) = 1, 1, 0))
65		oveq2 7357	. . . . 5 ⊢ (𝑁 = 0 → (𝐴 /_L 𝑁) = (𝐴 /_L 0))
66		lgs0 27219	. . . . . 6 ⊢ (𝐴 ∈ ℤ → (𝐴 /_L 0) = if((𝐴↑2) = 1, 1, 0))
67	8, 66	syl 17	. . . . 5 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) → (𝐴 /_L 0) = if((𝐴↑2) = 1, 1, 0))
68	65, 67	sylan9eqr 2786	. . . 4 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 = 0) → (𝐴 /_L 𝑁) = if((𝐴↑2) = 1, 1, 0))
69		oveq2 7357	. . . . 5 ⊢ (𝑁 = 0 → (𝐵 /_L 𝑁) = (𝐵 /_L 0))
70		lgs0 27219	. . . . . 6 ⊢ (𝐵 ∈ ℤ → (𝐵 /_L 0) = if((𝐵↑2) = 1, 1, 0))
71	11, 70	syl 17	. . . . 5 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) → (𝐵 /_L 0) = if((𝐵↑2) = 1, 1, 0))
72	69, 71	sylan9eqr 2786	. . . 4 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 = 0) → (𝐵 /_L 𝑁) = if((𝐵↑2) = 1, 1, 0))
73	68, 72	oveq12d 7367	. . 3 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 = 0) → ((𝐴 /_L 𝑁) · (𝐵 /_L 𝑁)) = (if((𝐴↑2) = 1, 1, 0) · if((𝐵↑2) = 1, 1, 0)))
74		oveq2 7357	. . . 4 ⊢ (𝑁 = 0 → ((𝐴 · 𝐵) /_L 𝑁) = ((𝐴 · 𝐵) /_L 0))
75		lgs0 27219	. . . . 5 ⊢ ((𝐴 · 𝐵) ∈ ℤ → ((𝐴 · 𝐵) /_L 0) = if(((𝐴 · 𝐵)↑2) = 1, 1, 0))
76	30, 75	syl 17	. . . 4 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) → ((𝐴 · 𝐵) /_L 0) = if(((𝐴 · 𝐵)↑2) = 1, 1, 0))
77	74, 76	sylan9eqr 2786	. . 3 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 = 0) → ((𝐴 · 𝐵) /_L 𝑁) = if(((𝐴 · 𝐵)↑2) = 1, 1, 0))
78	64, 73, 77	3eqtr4rd 2775	. 2 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 = 0) → ((𝐴 · 𝐵) /_L 𝑁) = ((𝐴 /_L 𝑁) · (𝐵 /_L 𝑁)))
79		lgsdilem 27233	. . . . 5 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) → if((𝑁 < 0 ∧ (𝐴 · 𝐵) < 0), -1, 1) = (if((𝑁 < 0 ∧ 𝐴 < 0), -1, 1) · if((𝑁 < 0 ∧ 𝐵 < 0), -1, 1)))
80	79	adantr 480	. . . 4 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 ≠ 0) → if((𝑁 < 0 ∧ (𝐴 · 𝐵) < 0), -1, 1) = (if((𝑁 < 0 ∧ 𝐴 < 0), -1, 1) · if((𝑁 < 0 ∧ 𝐵 < 0), -1, 1)))
81		simpl3 1194	. . . . . . 7 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) → 𝑁 ∈ ℤ)
82		nnabscl 15233	. . . . . . 7 ⊢ ((𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) → (abs‘𝑁) ∈ ℕ)
83	81, 82	sylan 580	. . . . . 6 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 ≠ 0) → (abs‘𝑁) ∈ ℕ)
84		nnuz 12778	. . . . . 6 ⊢ ℕ = (ℤ_≥‘1)
85	83, 84	eleqtrdi 2838	. . . . 5 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 ≠ 0) → (abs‘𝑁) ∈ (ℤ_≥‘1))
86		simpll1 1213	. . . . . . . 8 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 ≠ 0) → 𝐴 ∈ ℤ)
87		simpll3 1215	. . . . . . . 8 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 ≠ 0) → 𝑁 ∈ ℤ)
88		simpr 484	. . . . . . . 8 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 ≠ 0) → 𝑁 ≠ 0)
89		eqid 2729	. . . . . . . . 9 ⊢ (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /_L 𝑛)↑(𝑛 pCnt 𝑁)), 1)) = (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /_L 𝑛)↑(𝑛 pCnt 𝑁)), 1))
90	89	lgsfcl3 27227	. . . . . . . 8 ⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) → (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /_L 𝑛)↑(𝑛 pCnt 𝑁)), 1)):ℕ⟶ℤ)
91	86, 87, 88, 90	syl3anc 1373	. . . . . . 7 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 ≠ 0) → (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /_L 𝑛)↑(𝑛 pCnt 𝑁)), 1)):ℕ⟶ℤ)
92		elfznn 13456	. . . . . . 7 ⊢ (𝑘 ∈ (1...(abs‘𝑁)) → 𝑘 ∈ ℕ)
93		ffvelcdm 7015	. . . . . . 7 ⊢ (((𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /_L 𝑛)↑(𝑛 pCnt 𝑁)), 1)):ℕ⟶ℤ ∧ 𝑘 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /_L 𝑛)↑(𝑛 pCnt 𝑁)), 1))‘𝑘) ∈ ℤ)
94	91, 92, 93	syl2an 596	. . . . . 6 ⊢ (((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 ≠ 0) ∧ 𝑘 ∈ (1...(abs‘𝑁))) → ((𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /_L 𝑛)↑(𝑛 pCnt 𝑁)), 1))‘𝑘) ∈ ℤ)
95	94	zcnd 12581	. . . . 5 ⊢ (((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 ≠ 0) ∧ 𝑘 ∈ (1...(abs‘𝑁))) → ((𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /_L 𝑛)↑(𝑛 pCnt 𝑁)), 1))‘𝑘) ∈ ℂ)
96		simpll2 1214	. . . . . . . 8 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 ≠ 0) → 𝐵 ∈ ℤ)
97		eqid 2729	. . . . . . . . 9 ⊢ (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐵 /_L 𝑛)↑(𝑛 pCnt 𝑁)), 1)) = (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐵 /_L 𝑛)↑(𝑛 pCnt 𝑁)), 1))
98	97	lgsfcl3 27227	. . . . . . . 8 ⊢ ((𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) → (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐵 /_L 𝑛)↑(𝑛 pCnt 𝑁)), 1)):ℕ⟶ℤ)
99	96, 87, 88, 98	syl3anc 1373	. . . . . . 7 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 ≠ 0) → (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐵 /_L 𝑛)↑(𝑛 pCnt 𝑁)), 1)):ℕ⟶ℤ)
100		ffvelcdm 7015	. . . . . . 7 ⊢ (((𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐵 /_L 𝑛)↑(𝑛 pCnt 𝑁)), 1)):ℕ⟶ℤ ∧ 𝑘 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐵 /_L 𝑛)↑(𝑛 pCnt 𝑁)), 1))‘𝑘) ∈ ℤ)
101	99, 92, 100	syl2an 596	. . . . . 6 ⊢ (((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 ≠ 0) ∧ 𝑘 ∈ (1...(abs‘𝑁))) → ((𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐵 /_L 𝑛)↑(𝑛 pCnt 𝑁)), 1))‘𝑘) ∈ ℤ)
102	101	zcnd 12581	. . . . 5 ⊢ (((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 ≠ 0) ∧ 𝑘 ∈ (1...(abs‘𝑁))) → ((𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐵 /_L 𝑛)↑(𝑛 pCnt 𝑁)), 1))‘𝑘) ∈ ℂ)
103	86	adantr 480	. . . . . . . . . . . 12 ⊢ (((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 ≠ 0) ∧ 𝑘 ∈ ℙ) → 𝐴 ∈ ℤ)
104	96	adantr 480	. . . . . . . . . . . 12 ⊢ (((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 ≠ 0) ∧ 𝑘 ∈ ℙ) → 𝐵 ∈ ℤ)
105		simpr 484	. . . . . . . . . . . 12 ⊢ (((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 ≠ 0) ∧ 𝑘 ∈ ℙ) → 𝑘 ∈ ℙ)
106		lgsdirprm 27240	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑘 ∈ ℙ) → ((𝐴 · 𝐵) /_L 𝑘) = ((𝐴 /_L 𝑘) · (𝐵 /_L 𝑘)))
107	103, 104, 105, 106	syl3anc 1373	. . . . . . . . . . 11 ⊢ (((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 ≠ 0) ∧ 𝑘 ∈ ℙ) → ((𝐴 · 𝐵) /_L 𝑘) = ((𝐴 /_L 𝑘) · (𝐵 /_L 𝑘)))
108	107	oveq1d 7364	. . . . . . . . . 10 ⊢ (((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 ≠ 0) ∧ 𝑘 ∈ ℙ) → (((𝐴 · 𝐵) /_L 𝑘)↑(𝑘 pCnt 𝑁)) = (((𝐴 /_L 𝑘) · (𝐵 /_L 𝑘))↑(𝑘 pCnt 𝑁)))
109		prmz 16586	. . . . . . . . . . . . 13 ⊢ (𝑘 ∈ ℙ → 𝑘 ∈ ℤ)
110		lgscl 27220	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ ℤ ∧ 𝑘 ∈ ℤ) → (𝐴 /_L 𝑘) ∈ ℤ)
111	86, 109, 110	syl2an 596	. . . . . . . . . . . 12 ⊢ (((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 ≠ 0) ∧ 𝑘 ∈ ℙ) → (𝐴 /_L 𝑘) ∈ ℤ)
112	111	zcnd 12581	. . . . . . . . . . 11 ⊢ (((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 ≠ 0) ∧ 𝑘 ∈ ℙ) → (𝐴 /_L 𝑘) ∈ ℂ)
113		lgscl 27220	. . . . . . . . . . . . 13 ⊢ ((𝐵 ∈ ℤ ∧ 𝑘 ∈ ℤ) → (𝐵 /_L 𝑘) ∈ ℤ)
114	96, 109, 113	syl2an 596	. . . . . . . . . . . 12 ⊢ (((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 ≠ 0) ∧ 𝑘 ∈ ℙ) → (𝐵 /_L 𝑘) ∈ ℤ)
115	114	zcnd 12581	. . . . . . . . . . 11 ⊢ (((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 ≠ 0) ∧ 𝑘 ∈ ℙ) → (𝐵 /_L 𝑘) ∈ ℂ)
116	87	adantr 480	. . . . . . . . . . . 12 ⊢ (((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 ≠ 0) ∧ 𝑘 ∈ ℙ) → 𝑁 ∈ ℤ)
117	88	adantr 480	. . . . . . . . . . . 12 ⊢ (((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 ≠ 0) ∧ 𝑘 ∈ ℙ) → 𝑁 ≠ 0)
118		pczcl 16760	. . . . . . . . . . . 12 ⊢ ((𝑘 ∈ ℙ ∧ (𝑁 ∈ ℤ ∧ 𝑁 ≠ 0)) → (𝑘 pCnt 𝑁) ∈ ℕ₀)
119	105, 116, 117, 118	syl12anc 836	. . . . . . . . . . 11 ⊢ (((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 ≠ 0) ∧ 𝑘 ∈ ℙ) → (𝑘 pCnt 𝑁) ∈ ℕ₀)
120	112, 115, 119	mulexpd 14068	. . . . . . . . . 10 ⊢ (((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 ≠ 0) ∧ 𝑘 ∈ ℙ) → (((𝐴 /_L 𝑘) · (𝐵 /_L 𝑘))↑(𝑘 pCnt 𝑁)) = (((𝐴 /_L 𝑘)↑(𝑘 pCnt 𝑁)) · ((𝐵 /_L 𝑘)↑(𝑘 pCnt 𝑁))))
121	108, 120	eqtrd 2764	. . . . . . . . 9 ⊢ (((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 ≠ 0) ∧ 𝑘 ∈ ℙ) → (((𝐴 · 𝐵) /_L 𝑘)↑(𝑘 pCnt 𝑁)) = (((𝐴 /_L 𝑘)↑(𝑘 pCnt 𝑁)) · ((𝐵 /_L 𝑘)↑(𝑘 pCnt 𝑁))))
122		iftrue 4482	. . . . . . . . . 10 ⊢ (𝑘 ∈ ℙ → if(𝑘 ∈ ℙ, (((𝐴 · 𝐵) /_L 𝑘)↑(𝑘 pCnt 𝑁)), 1) = (((𝐴 · 𝐵) /_L 𝑘)↑(𝑘 pCnt 𝑁)))
123	122	adantl 481	. . . . . . . . 9 ⊢ (((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 ≠ 0) ∧ 𝑘 ∈ ℙ) → if(𝑘 ∈ ℙ, (((𝐴 · 𝐵) /_L 𝑘)↑(𝑘 pCnt 𝑁)), 1) = (((𝐴 · 𝐵) /_L 𝑘)↑(𝑘 pCnt 𝑁)))
124		iftrue 4482	. . . . . . . . . . 11 ⊢ (𝑘 ∈ ℙ → if(𝑘 ∈ ℙ, ((𝐴 /_L 𝑘)↑(𝑘 pCnt 𝑁)), 1) = ((𝐴 /_L 𝑘)↑(𝑘 pCnt 𝑁)))
125		iftrue 4482	. . . . . . . . . . 11 ⊢ (𝑘 ∈ ℙ → if(𝑘 ∈ ℙ, ((𝐵 /_L 𝑘)↑(𝑘 pCnt 𝑁)), 1) = ((𝐵 /_L 𝑘)↑(𝑘 pCnt 𝑁)))
126	124, 125	oveq12d 7367	. . . . . . . . . 10 ⊢ (𝑘 ∈ ℙ → (if(𝑘 ∈ ℙ, ((𝐴 /_L 𝑘)↑(𝑘 pCnt 𝑁)), 1) · if(𝑘 ∈ ℙ, ((𝐵 /_L 𝑘)↑(𝑘 pCnt 𝑁)), 1)) = (((𝐴 /_L 𝑘)↑(𝑘 pCnt 𝑁)) · ((𝐵 /_L 𝑘)↑(𝑘 pCnt 𝑁))))
127	126	adantl 481	. . . . . . . . 9 ⊢ (((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 ≠ 0) ∧ 𝑘 ∈ ℙ) → (if(𝑘 ∈ ℙ, ((𝐴 /_L 𝑘)↑(𝑘 pCnt 𝑁)), 1) · if(𝑘 ∈ ℙ, ((𝐵 /_L 𝑘)↑(𝑘 pCnt 𝑁)), 1)) = (((𝐴 /_L 𝑘)↑(𝑘 pCnt 𝑁)) · ((𝐵 /_L 𝑘)↑(𝑘 pCnt 𝑁))))
128	121, 123, 127	3eqtr4d 2774	. . . . . . . 8 ⊢ (((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 ≠ 0) ∧ 𝑘 ∈ ℙ) → if(𝑘 ∈ ℙ, (((𝐴 · 𝐵) /_L 𝑘)↑(𝑘 pCnt 𝑁)), 1) = (if(𝑘 ∈ ℙ, ((𝐴 /_L 𝑘)↑(𝑘 pCnt 𝑁)), 1) · if(𝑘 ∈ ℙ, ((𝐵 /_L 𝑘)↑(𝑘 pCnt 𝑁)), 1)))
129		1t1e1 12285	. . . . . . . . . . 11 ⊢ (1 · 1) = 1
130	129	eqcomi 2738	. . . . . . . . . 10 ⊢ 1 = (1 · 1)
131		iffalse 4485	. . . . . . . . . 10 ⊢ (¬ 𝑘 ∈ ℙ → if(𝑘 ∈ ℙ, (((𝐴 · 𝐵) /_L 𝑘)↑(𝑘 pCnt 𝑁)), 1) = 1)
132		iffalse 4485	. . . . . . . . . . 11 ⊢ (¬ 𝑘 ∈ ℙ → if(𝑘 ∈ ℙ, ((𝐴 /_L 𝑘)↑(𝑘 pCnt 𝑁)), 1) = 1)
133		iffalse 4485	. . . . . . . . . . 11 ⊢ (¬ 𝑘 ∈ ℙ → if(𝑘 ∈ ℙ, ((𝐵 /_L 𝑘)↑(𝑘 pCnt 𝑁)), 1) = 1)
134	132, 133	oveq12d 7367	. . . . . . . . . 10 ⊢ (¬ 𝑘 ∈ ℙ → (if(𝑘 ∈ ℙ, ((𝐴 /_L 𝑘)↑(𝑘 pCnt 𝑁)), 1) · if(𝑘 ∈ ℙ, ((𝐵 /_L 𝑘)↑(𝑘 pCnt 𝑁)), 1)) = (1 · 1))
135	130, 131, 134	3eqtr4a 2790	. . . . . . . . 9 ⊢ (¬ 𝑘 ∈ ℙ → if(𝑘 ∈ ℙ, (((𝐴 · 𝐵) /_L 𝑘)↑(𝑘 pCnt 𝑁)), 1) = (if(𝑘 ∈ ℙ, ((𝐴 /_L 𝑘)↑(𝑘 pCnt 𝑁)), 1) · if(𝑘 ∈ ℙ, ((𝐵 /_L 𝑘)↑(𝑘 pCnt 𝑁)), 1)))
136	135	adantl 481	. . . . . . . 8 ⊢ (((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 ≠ 0) ∧ ¬ 𝑘 ∈ ℙ) → if(𝑘 ∈ ℙ, (((𝐴 · 𝐵) /_L 𝑘)↑(𝑘 pCnt 𝑁)), 1) = (if(𝑘 ∈ ℙ, ((𝐴 /_L 𝑘)↑(𝑘 pCnt 𝑁)), 1) · if(𝑘 ∈ ℙ, ((𝐵 /_L 𝑘)↑(𝑘 pCnt 𝑁)), 1)))
137	128, 136	pm2.61dan 812	. . . . . . 7 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 ≠ 0) → if(𝑘 ∈ ℙ, (((𝐴 · 𝐵) /_L 𝑘)↑(𝑘 pCnt 𝑁)), 1) = (if(𝑘 ∈ ℙ, ((𝐴 /_L 𝑘)↑(𝑘 pCnt 𝑁)), 1) · if(𝑘 ∈ ℙ, ((𝐵 /_L 𝑘)↑(𝑘 pCnt 𝑁)), 1)))
138	137	adantr 480	. . . . . 6 ⊢ (((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 ≠ 0) ∧ 𝑘 ∈ (1...(abs‘𝑁))) → if(𝑘 ∈ ℙ, (((𝐴 · 𝐵) /_L 𝑘)↑(𝑘 pCnt 𝑁)), 1) = (if(𝑘 ∈ ℙ, ((𝐴 /_L 𝑘)↑(𝑘 pCnt 𝑁)), 1) · if(𝑘 ∈ ℙ, ((𝐵 /_L 𝑘)↑(𝑘 pCnt 𝑁)), 1)))
139	92	adantl 481	. . . . . . 7 ⊢ (((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 ≠ 0) ∧ 𝑘 ∈ (1...(abs‘𝑁))) → 𝑘 ∈ ℕ)
140		eleq1w 2811	. . . . . . . . 9 ⊢ (𝑛 = 𝑘 → (𝑛 ∈ ℙ ↔ 𝑘 ∈ ℙ))
141		oveq2 7357	. . . . . . . . . 10 ⊢ (𝑛 = 𝑘 → ((𝐴 · 𝐵) /_L 𝑛) = ((𝐴 · 𝐵) /_L 𝑘))
142		oveq1 7356	. . . . . . . . . 10 ⊢ (𝑛 = 𝑘 → (𝑛 pCnt 𝑁) = (𝑘 pCnt 𝑁))
143	141, 142	oveq12d 7367	. . . . . . . . 9 ⊢ (𝑛 = 𝑘 → (((𝐴 · 𝐵) /_L 𝑛)↑(𝑛 pCnt 𝑁)) = (((𝐴 · 𝐵) /_L 𝑘)↑(𝑘 pCnt 𝑁)))
144	140, 143	ifbieq1d 4501	. . . . . . . 8 ⊢ (𝑛 = 𝑘 → if(𝑛 ∈ ℙ, (((𝐴 · 𝐵) /_L 𝑛)↑(𝑛 pCnt 𝑁)), 1) = if(𝑘 ∈ ℙ, (((𝐴 · 𝐵) /_L 𝑘)↑(𝑘 pCnt 𝑁)), 1))
145		eqid 2729	. . . . . . . 8 ⊢ (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, (((𝐴 · 𝐵) /_L 𝑛)↑(𝑛 pCnt 𝑁)), 1)) = (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, (((𝐴 · 𝐵) /_L 𝑛)↑(𝑛 pCnt 𝑁)), 1))
146		ovex 7382	. . . . . . . . 9 ⊢ (((𝐴 · 𝐵) /_L 𝑘)↑(𝑘 pCnt 𝑁)) ∈ V
147		1ex 11111	. . . . . . . . 9 ⊢ 1 ∈ V
148	146, 147	ifex 4527	. . . . . . . 8 ⊢ if(𝑘 ∈ ℙ, (((𝐴 · 𝐵) /_L 𝑘)↑(𝑘 pCnt 𝑁)), 1) ∈ V
149	144, 145, 148	fvmpt 6930	. . . . . . 7 ⊢ (𝑘 ∈ ℕ → ((𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, (((𝐴 · 𝐵) /_L 𝑛)↑(𝑛 pCnt 𝑁)), 1))‘𝑘) = if(𝑘 ∈ ℙ, (((𝐴 · 𝐵) /_L 𝑘)↑(𝑘 pCnt 𝑁)), 1))
150	139, 149	syl 17	. . . . . 6 ⊢ (((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 ≠ 0) ∧ 𝑘 ∈ (1...(abs‘𝑁))) → ((𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, (((𝐴 · 𝐵) /_L 𝑛)↑(𝑛 pCnt 𝑁)), 1))‘𝑘) = if(𝑘 ∈ ℙ, (((𝐴 · 𝐵) /_L 𝑘)↑(𝑘 pCnt 𝑁)), 1))
151		oveq2 7357	. . . . . . . . . . 11 ⊢ (𝑛 = 𝑘 → (𝐴 /_L 𝑛) = (𝐴 /_L 𝑘))
152	151, 142	oveq12d 7367	. . . . . . . . . 10 ⊢ (𝑛 = 𝑘 → ((𝐴 /_L 𝑛)↑(𝑛 pCnt 𝑁)) = ((𝐴 /_L 𝑘)↑(𝑘 pCnt 𝑁)))
153	140, 152	ifbieq1d 4501	. . . . . . . . 9 ⊢ (𝑛 = 𝑘 → if(𝑛 ∈ ℙ, ((𝐴 /_L 𝑛)↑(𝑛 pCnt 𝑁)), 1) = if(𝑘 ∈ ℙ, ((𝐴 /_L 𝑘)↑(𝑘 pCnt 𝑁)), 1))
154		ovex 7382	. . . . . . . . . 10 ⊢ ((𝐴 /_L 𝑘)↑(𝑘 pCnt 𝑁)) ∈ V
155	154, 147	ifex 4527	. . . . . . . . 9 ⊢ if(𝑘 ∈ ℙ, ((𝐴 /_L 𝑘)↑(𝑘 pCnt 𝑁)), 1) ∈ V
156	153, 89, 155	fvmpt 6930	. . . . . . . 8 ⊢ (𝑘 ∈ ℕ → ((𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /_L 𝑛)↑(𝑛 pCnt 𝑁)), 1))‘𝑘) = if(𝑘 ∈ ℙ, ((𝐴 /_L 𝑘)↑(𝑘 pCnt 𝑁)), 1))
157	139, 156	syl 17	. . . . . . 7 ⊢ (((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 ≠ 0) ∧ 𝑘 ∈ (1...(abs‘𝑁))) → ((𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /_L 𝑛)↑(𝑛 pCnt 𝑁)), 1))‘𝑘) = if(𝑘 ∈ ℙ, ((𝐴 /_L 𝑘)↑(𝑘 pCnt 𝑁)), 1))
158		oveq2 7357	. . . . . . . . . . 11 ⊢ (𝑛 = 𝑘 → (𝐵 /_L 𝑛) = (𝐵 /_L 𝑘))
159	158, 142	oveq12d 7367	. . . . . . . . . 10 ⊢ (𝑛 = 𝑘 → ((𝐵 /_L 𝑛)↑(𝑛 pCnt 𝑁)) = ((𝐵 /_L 𝑘)↑(𝑘 pCnt 𝑁)))
160	140, 159	ifbieq1d 4501	. . . . . . . . 9 ⊢ (𝑛 = 𝑘 → if(𝑛 ∈ ℙ, ((𝐵 /_L 𝑛)↑(𝑛 pCnt 𝑁)), 1) = if(𝑘 ∈ ℙ, ((𝐵 /_L 𝑘)↑(𝑘 pCnt 𝑁)), 1))
161		ovex 7382	. . . . . . . . . 10 ⊢ ((𝐵 /_L 𝑘)↑(𝑘 pCnt 𝑁)) ∈ V
162	161, 147	ifex 4527	. . . . . . . . 9 ⊢ if(𝑘 ∈ ℙ, ((𝐵 /_L 𝑘)↑(𝑘 pCnt 𝑁)), 1) ∈ V
163	160, 97, 162	fvmpt 6930	. . . . . . . 8 ⊢ (𝑘 ∈ ℕ → ((𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐵 /_L 𝑛)↑(𝑛 pCnt 𝑁)), 1))‘𝑘) = if(𝑘 ∈ ℙ, ((𝐵 /_L 𝑘)↑(𝑘 pCnt 𝑁)), 1))
164	139, 163	syl 17	. . . . . . 7 ⊢ (((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 ≠ 0) ∧ 𝑘 ∈ (1...(abs‘𝑁))) → ((𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐵 /_L 𝑛)↑(𝑛 pCnt 𝑁)), 1))‘𝑘) = if(𝑘 ∈ ℙ, ((𝐵 /_L 𝑘)↑(𝑘 pCnt 𝑁)), 1))
165	157, 164	oveq12d 7367	. . . . . 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 2774	. . . . 5 ⊢ (((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 ≠ 0) ∧ 𝑘 ∈ (1...(abs‘𝑁))) → ((𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, (((𝐴 · 𝐵) /_L 𝑛)↑(𝑛 pCnt 𝑁)), 1))‘𝑘) = (((𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /_L 𝑛)↑(𝑛 pCnt 𝑁)), 1))‘𝑘) · ((𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐵 /_L 𝑛)↑(𝑛 pCnt 𝑁)), 1))‘𝑘)))
167	85, 95, 102, 166	prodfmul 15797	. . . 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 7367	. . 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 480	. . . 4 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 ≠ 0) → (𝐴 · 𝐵) ∈ ℤ)
170	145	lgsval4 27226	. . . 4 ⊢ (((𝐴 · 𝐵) ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) → ((𝐴 · 𝐵) /_L 𝑁) = (if((𝑁 < 0 ∧ (𝐴 · 𝐵) < 0), -1, 1) · (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, (((𝐴 · 𝐵) /_L 𝑛)↑(𝑛 pCnt 𝑁)), 1)))‘(abs‘𝑁))))
171	169, 87, 88, 170	syl3anc 1373	. . 3 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 ≠ 0) → ((𝐴 · 𝐵) /_L 𝑁) = (if((𝑁 < 0 ∧ (𝐴 · 𝐵) < 0), -1, 1) · (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, (((𝐴 · 𝐵) /_L 𝑛)↑(𝑛 pCnt 𝑁)), 1)))‘(abs‘𝑁))))
172	89	lgsval4 27226	. . . . . 6 ⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) → (𝐴 /_L 𝑁) = (if((𝑁 < 0 ∧ 𝐴 < 0), -1, 1) · (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /_L 𝑛)↑(𝑛 pCnt 𝑁)), 1)))‘(abs‘𝑁))))
173	86, 87, 88, 172	syl3anc 1373	. . . . 5 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 ≠ 0) → (𝐴 /_L 𝑁) = (if((𝑁 < 0 ∧ 𝐴 < 0), -1, 1) · (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /_L 𝑛)↑(𝑛 pCnt 𝑁)), 1)))‘(abs‘𝑁))))
174	97	lgsval4 27226	. . . . . 6 ⊢ ((𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) → (𝐵 /_L 𝑁) = (if((𝑁 < 0 ∧ 𝐵 < 0), -1, 1) · (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐵 /_L 𝑛)↑(𝑛 pCnt 𝑁)), 1)))‘(abs‘𝑁))))
175	96, 87, 88, 174	syl3anc 1373	. . . . 5 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 ≠ 0) → (𝐵 /_L 𝑁) = (if((𝑁 < 0 ∧ 𝐵 < 0), -1, 1) · (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐵 /_L 𝑛)↑(𝑛 pCnt 𝑁)), 1)))‘(abs‘𝑁))))
176	173, 175	oveq12d 7367	. . . 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 12113	. . . . . . 7 ⊢ -1 ∈ ℂ
178	177, 1	ifcli 4524	. . . . . 6 ⊢ if((𝑁 < 0 ∧ 𝐴 < 0), -1, 1) ∈ ℂ
179	178	a1i 11	. . . . 5 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 ≠ 0) → if((𝑁 < 0 ∧ 𝐴 < 0), -1, 1) ∈ ℂ)
180		mulcl 11093	. . . . . . 7 ⊢ ((𝑘 ∈ ℂ ∧ 𝑥 ∈ ℂ) → (𝑘 · 𝑥) ∈ ℂ)
181	180	adantl 481	. . . . . 6 ⊢ (((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 ≠ 0) ∧ (𝑘 ∈ ℂ ∧ 𝑥 ∈ ℂ)) → (𝑘 · 𝑥) ∈ ℂ)
182	85, 95, 181	seqcl 13929	. . . . 5 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 ≠ 0) → (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /_L 𝑛)↑(𝑛 pCnt 𝑁)), 1)))‘(abs‘𝑁)) ∈ ℂ)
183	177, 1	ifcli 4524	. . . . . 6 ⊢ if((𝑁 < 0 ∧ 𝐵 < 0), -1, 1) ∈ ℂ
184	183	a1i 11	. . . . 5 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 ≠ 0) → if((𝑁 < 0 ∧ 𝐵 < 0), -1, 1) ∈ ℂ)
185	85, 102, 181	seqcl 13929	. . . . 5 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 ≠ 0) → (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐵 /_L 𝑛)↑(𝑛 pCnt 𝑁)), 1)))‘(abs‘𝑁)) ∈ ℂ)
186	179, 182, 184, 185	mul4d 11328	. . . 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 2764	. . 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 2774	. 2 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 ≠ 0) → ((𝐴 · 𝐵) /_L 𝑁) = ((𝐴 /_L 𝑁) · (𝐵 /_L 𝑁)))
189	78, 188	pm2.61dane 3012	1 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) → ((𝐴 · 𝐵) /_L 𝑁) = ((𝐴 /_L 𝑁) · (𝐵 /_L 𝑁)))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 206 ∧ wa 395 ∨ wo 847 ∧ w3a 1086 = wceq 1540 ∈ wcel 2109 ≠ wne 2925 ifcif 4476 class class class wbr 5092 ↦ cmpt 5173 ⟶wf 6478 ‘cfv 6482 (class class class)co 7349 ℂcc 11007 ℝcr 11008 0cc0 11009 1c1 11010 · cmul 11014 < clt 11149 ≤ cle 11150 -cneg 11348 ℕcn 12128 2c2 12183 ℕ₀cn0 12384 ℤcz 12471 ℤ_≥cuz 12735 ...cfz 13410 seqcseq 13908 ↑cexp 13968 abscabs 15141 ∥ cdvds 16163 ℙcprime 16582 pCnt cpc 16748 /_L clgs 27203

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2008 ax-8 2111 ax-9 2119 ax-10 2142 ax-11 2158 ax-12 2178 ax-ext 2701 ax-rep 5218 ax-sep 5235 ax-nul 5245 ax-pow 5304 ax-pr 5371 ax-un 7671 ax-cnex 11065 ax-resscn 11066 ax-1cn 11067 ax-icn 11068 ax-addcl 11069 ax-addrcl 11070 ax-mulcl 11071 ax-mulrcl 11072 ax-mulcom 11073 ax-addass 11074 ax-mulass 11075 ax-distr 11076 ax-i2m1 11077 ax-1ne0 11078 ax-1rid 11079 ax-rnegex 11080 ax-rrecex 11081 ax-cnre 11082 ax-pre-lttri 11083 ax-pre-lttrn 11084 ax-pre-ltadd 11085 ax-pre-mulgt0 11086 ax-pre-sup 11087

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2066 df-mo 2533 df-eu 2562 df-clab 2708 df-cleq 2721 df-clel 2803 df-nfc 2878 df-ne 2926 df-nel 3030 df-ral 3045 df-rex 3054 df-rmo 3343 df-reu 3344 df-rab 3395 df-v 3438 df-sbc 3743 df-csb 3852 df-dif 3906 df-un 3908 df-in 3910 df-ss 3920 df-pss 3923 df-nul 4285 df-if 4477 df-pw 4553 df-sn 4578 df-pr 4580 df-op 4584 df-uni 4859 df-int 4897 df-iun 4943 df-br 5093 df-opab 5155 df-mpt 5174 df-tr 5200 df-id 5514 df-eprel 5519 df-po 5527 df-so 5528 df-fr 5572 df-we 5574 df-xp 5625 df-rel 5626 df-cnv 5627 df-co 5628 df-dm 5629 df-rn 5630 df-res 5631 df-ima 5632 df-pred 6249 df-ord 6310 df-on 6311 df-lim 6312 df-suc 6313 df-iota 6438 df-fun 6484 df-fn 6485 df-f 6486 df-f1 6487 df-fo 6488 df-f1o 6489 df-fv 6490 df-riota 7306 df-ov 7352 df-oprab 7353 df-mpo 7354 df-om 7800 df-1st 7924 df-2nd 7925 df-frecs 8214 df-wrecs 8245 df-recs 8294 df-rdg 8332 df-1o 8388 df-2o 8389 df-oadd 8392 df-er 8625 df-en 8873 df-dom 8874 df-sdom 8875 df-fin 8876 df-sup 9332 df-inf 9333 df-dju 9797 df-card 9835 df-pnf 11151 df-mnf 11152 df-xr 11153 df-ltxr 11154 df-le 11155 df-sub 11349 df-neg 11350 df-div 11778 df-nn 12129 df-2 12191 df-3 12192 df-4 12193 df-5 12194 df-6 12195 df-7 12196 df-8 12197 df-9 12198 df-n0 12385 df-xnn0 12458 df-z 12472 df-uz 12736 df-q 12850 df-rp 12894 df-fz 13411 df-fzo 13558 df-fl 13696 df-mod 13774 df-seq 13909 df-exp 13969 df-hash 14238 df-cj 15006 df-re 15007 df-im 15008 df-sqrt 15142 df-abs 15143 df-dvds 16164 df-gcd 16406 df-prm 16583 df-phi 16677 df-pc 16749 df-lgs 27204

This theorem is referenced by: lgssq 27246 lgsmulsqcoprm 27252 lgsdirnn0 27253 lgsquad2lem1 27293

W3C validator