lgsdir - Intuitionistic Logic Explorer

	Intuitionistic Logic Explorer		< Previous Next > Nearby theorems
Mirrors > Home > ILE Home > Th. List > lgsdir		GIF version

Theorem lgsdir 13695

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). (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		1cnd 7929	. . . . . . . 8 ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) → 1 ∈ ℂ)
2		0cnd 7906	. . . . . . . 8 ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) → 0 ∈ ℂ)
3		zsqcl 10539	. . . . . . . . . 10 ⊢ (𝐵 ∈ ℤ → (𝐵↑2) ∈ ℤ)
4	3	3ad2ant2 1014	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝐵↑2) ∈ ℤ)
5		1z 9231	. . . . . . . . 9 ⊢ 1 ∈ ℤ
6		zdceq 9280	. . . . . . . . 9 ⊢ (((𝐵↑2) ∈ ℤ ∧ 1 ∈ ℤ) → DECID (𝐵↑2) = 1)
7	4, 5, 6	sylancl 411	. . . . . . . 8 ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) → DECID (𝐵↑2) = 1)
8	1, 2, 7	ifcldcd 3560	. . . . . . 7 ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) → if((𝐵↑2) = 1, 1, 0) ∈ ℂ)
9	8	mulid2d 7931	. . . . . 6 ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (1 · if((𝐵↑2) = 1, 1, 0)) = if((𝐵↑2) = 1, 1, 0))
10	9	ad3antrrr 489	. . . . 5 ⊢ (((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 = 0) ∧ (𝐴↑2) = 1) → (1 · if((𝐵↑2) = 1, 1, 0)) = if((𝐵↑2) = 1, 1, 0))
11		iftrue 3530	. . . . . . 7 ⊢ ((𝐴↑2) = 1 → if((𝐴↑2) = 1, 1, 0) = 1)
12	11	adantl 275	. . . . . 6 ⊢ (((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 = 0) ∧ (𝐴↑2) = 1) → if((𝐴↑2) = 1, 1, 0) = 1)
13	12	oveq1d 5866	. . . . 5 ⊢ (((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 = 0) ∧ (𝐴↑2) = 1) → (if((𝐴↑2) = 1, 1, 0) · if((𝐵↑2) = 1, 1, 0)) = (1 · if((𝐵↑2) = 1, 1, 0)))
14		simpl1 995	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) → 𝐴 ∈ ℤ)
15	14	zcnd 9328	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) → 𝐴 ∈ ℂ)
16	15	ad2antrr 485	. . . . . . . . 9 ⊢ (((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 = 0) ∧ (𝐴↑2) = 1) → 𝐴 ∈ ℂ)
17		simpl2 996	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) → 𝐵 ∈ ℤ)
18	17	zcnd 9328	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) → 𝐵 ∈ ℂ)
19	18	ad2antrr 485	. . . . . . . . 9 ⊢ (((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 = 0) ∧ (𝐴↑2) = 1) → 𝐵 ∈ ℂ)
20	16, 19	sqmuld 10614	. . . . . . . 8 ⊢ (((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 = 0) ∧ (𝐴↑2) = 1) → ((𝐴 · 𝐵)↑2) = ((𝐴↑2) · (𝐵↑2)))
21		simpr 109	. . . . . . . . 9 ⊢ (((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 = 0) ∧ (𝐴↑2) = 1) → (𝐴↑2) = 1)
22	21	oveq1d 5866	. . . . . . . 8 ⊢ (((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 = 0) ∧ (𝐴↑2) = 1) → ((𝐴↑2) · (𝐵↑2)) = (1 · (𝐵↑2)))
23	18	sqcld 10600	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) → (𝐵↑2) ∈ ℂ)
24	23	ad2antrr 485	. . . . . . . . 9 ⊢ (((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 = 0) ∧ (𝐴↑2) = 1) → (𝐵↑2) ∈ ℂ)
25	24	mulid2d 7931	. . . . . . . 8 ⊢ (((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 = 0) ∧ (𝐴↑2) = 1) → (1 · (𝐵↑2)) = (𝐵↑2))
26	20, 22, 25	3eqtrd 2207	. . . . . . 7 ⊢ (((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 = 0) ∧ (𝐴↑2) = 1) → ((𝐴 · 𝐵)↑2) = (𝐵↑2))
27	26	eqeq1d 2179	. . . . . 6 ⊢ (((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 = 0) ∧ (𝐴↑2) = 1) → (((𝐴 · 𝐵)↑2) = 1 ↔ (𝐵↑2) = 1))
28	27	ifbid 3546	. . . . 5 ⊢ (((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 = 0) ∧ (𝐴↑2) = 1) → if(((𝐴 · 𝐵)↑2) = 1, 1, 0) = if((𝐵↑2) = 1, 1, 0))
29	10, 13, 28	3eqtr4d 2213	. . . 4 ⊢ (((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 = 0) ∧ (𝐴↑2) = 1) → (if((𝐴↑2) = 1, 1, 0) · if((𝐵↑2) = 1, 1, 0)) = if(((𝐴 · 𝐵)↑2) = 1, 1, 0))
30	8	mul02d 8304	. . . . . 6 ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (0 · if((𝐵↑2) = 1, 1, 0)) = 0)
31	30	ad3antrrr 489	. . . . 5 ⊢ (((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 = 0) ∧ ¬ (𝐴↑2) = 1) → (0 · if((𝐵↑2) = 1, 1, 0)) = 0)
32		iffalse 3533	. . . . . . 7 ⊢ (¬ (𝐴↑2) = 1 → if((𝐴↑2) = 1, 1, 0) = 0)
33	32	adantl 275	. . . . . 6 ⊢ (((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 = 0) ∧ ¬ (𝐴↑2) = 1) → if((𝐴↑2) = 1, 1, 0) = 0)
34	33	oveq1d 5866	. . . . 5 ⊢ (((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 = 0) ∧ ¬ (𝐴↑2) = 1) → (if((𝐴↑2) = 1, 1, 0) · if((𝐵↑2) = 1, 1, 0)) = (0 · if((𝐵↑2) = 1, 1, 0)))
35		dvdsmul1 11768	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → 𝐴 ∥ (𝐴 · 𝐵))
36	14, 17, 35	syl2anc 409	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) → 𝐴 ∥ (𝐴 · 𝐵))
37	14, 17	zmulcld 9333	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) → (𝐴 · 𝐵) ∈ ℤ)
38		dvdssq 11979	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ ℤ ∧ (𝐴 · 𝐵) ∈ ℤ) → (𝐴 ∥ (𝐴 · 𝐵) ↔ (𝐴↑2) ∥ ((𝐴 · 𝐵)↑2)))
39	14, 37, 38	syl2anc 409	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) → (𝐴 ∥ (𝐴 · 𝐵) ↔ (𝐴↑2) ∥ ((𝐴 · 𝐵)↑2)))
40	36, 39	mpbid 146	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) → (𝐴↑2) ∥ ((𝐴 · 𝐵)↑2))
41	40	adantr 274	. . . . . . . . 9 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 = 0) → (𝐴↑2) ∥ ((𝐴 · 𝐵)↑2))
42		breq2 3991	. . . . . . . . 9 ⊢ (((𝐴 · 𝐵)↑2) = 1 → ((𝐴↑2) ∥ ((𝐴 · 𝐵)↑2) ↔ (𝐴↑2) ∥ 1))
43	41, 42	syl5ibcom 154	. . . . . . . 8 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 = 0) → (((𝐴 · 𝐵)↑2) = 1 → (𝐴↑2) ∥ 1))
44		simprl 526	. . . . . . . . . . . . . . . 16 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) → 𝐴 ≠ 0)
45	44	neneqd 2361	. . . . . . . . . . . . . . 15 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) → ¬ 𝐴 = 0)
46		sqeq0 10532	. . . . . . . . . . . . . . . 16 ⊢ (𝐴 ∈ ℂ → ((𝐴↑2) = 0 ↔ 𝐴 = 0))
47	15, 46	syl 14	. . . . . . . . . . . . . . 15 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) → ((𝐴↑2) = 0 ↔ 𝐴 = 0))
48	45, 47	mtbird 668	. . . . . . . . . . . . . 14 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) → ¬ (𝐴↑2) = 0)
49		zsqcl2 10546	. . . . . . . . . . . . . . . 16 ⊢ (𝐴 ∈ ℤ → (𝐴↑2) ∈ ℕ₀)
50	14, 49	syl 14	. . . . . . . . . . . . . . 15 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) → (𝐴↑2) ∈ ℕ₀)
51		elnn0 9130	. . . . . . . . . . . . . . 15 ⊢ ((𝐴↑2) ∈ ℕ₀ ↔ ((𝐴↑2) ∈ ℕ ∨ (𝐴↑2) = 0))
52	50, 51	sylib 121	. . . . . . . . . . . . . 14 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) → ((𝐴↑2) ∈ ℕ ∨ (𝐴↑2) = 0))
53	48, 52	ecased 1344	. . . . . . . . . . . . 13 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) → (𝐴↑2) ∈ ℕ)
54	53	adantr 274	. . . . . . . . . . . 12 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 = 0) → (𝐴↑2) ∈ ℕ)
55	54	nnzd 9326	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 = 0) → (𝐴↑2) ∈ ℤ)
56		1nn 8882	. . . . . . . . . . 11 ⊢ 1 ∈ ℕ
57		dvdsle 11797	. . . . . . . . . . 11 ⊢ (((𝐴↑2) ∈ ℤ ∧ 1 ∈ ℕ) → ((𝐴↑2) ∥ 1 → (𝐴↑2) ≤ 1))
58	55, 56, 57	sylancl 411	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 = 0) → ((𝐴↑2) ∥ 1 → (𝐴↑2) ≤ 1))
59	54	nnge1d 8914	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 = 0) → 1 ≤ (𝐴↑2))
60	58, 59	jctird 315	. . . . . . . . 9 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 = 0) → ((𝐴↑2) ∥ 1 → ((𝐴↑2) ≤ 1 ∧ 1 ≤ (𝐴↑2))))
61	54	nnred 8884	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 = 0) → (𝐴↑2) ∈ ℝ)
62		1re 7912	. . . . . . . . . 10 ⊢ 1 ∈ ℝ
63		letri3 7993	. . . . . . . . . 10 ⊢ (((𝐴↑2) ∈ ℝ ∧ 1 ∈ ℝ) → ((𝐴↑2) = 1 ↔ ((𝐴↑2) ≤ 1 ∧ 1 ≤ (𝐴↑2))))
64	61, 62, 63	sylancl 411	. . . . . . . . 9 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 = 0) → ((𝐴↑2) = 1 ↔ ((𝐴↑2) ≤ 1 ∧ 1 ≤ (𝐴↑2))))
65	60, 64	sylibrd 168	. . . . . . . 8 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 = 0) → ((𝐴↑2) ∥ 1 → (𝐴↑2) = 1))
66	43, 65	syld 45	. . . . . . 7 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 = 0) → (((𝐴 · 𝐵)↑2) = 1 → (𝐴↑2) = 1))
67	66	con3dimp 630	. . . . . 6 ⊢ (((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 = 0) ∧ ¬ (𝐴↑2) = 1) → ¬ ((𝐴 · 𝐵)↑2) = 1)
68	67	iffalsed 3535	. . . . 5 ⊢ (((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 = 0) ∧ ¬ (𝐴↑2) = 1) → if(((𝐴 · 𝐵)↑2) = 1, 1, 0) = 0)
69	31, 34, 68	3eqtr4d 2213	. . . 4 ⊢ (((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 = 0) ∧ ¬ (𝐴↑2) = 1) → (if((𝐴↑2) = 1, 1, 0) · if((𝐵↑2) = 1, 1, 0)) = if(((𝐴 · 𝐵)↑2) = 1, 1, 0))
70		zdceq 9280	. . . . . 6 ⊢ (((𝐴↑2) ∈ ℤ ∧ 1 ∈ ℤ) → DECID (𝐴↑2) = 1)
71	55, 5, 70	sylancl 411	. . . . 5 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 = 0) → DECID (𝐴↑2) = 1)
72		exmiddc 831	. . . . 5 ⊢ (DECID (𝐴↑2) = 1 → ((𝐴↑2) = 1 ∨ ¬ (𝐴↑2) = 1))
73	71, 72	syl 14	. . . 4 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 = 0) → ((𝐴↑2) = 1 ∨ ¬ (𝐴↑2) = 1))
74	29, 69, 73	mpjaodan 793	. . 3 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 = 0) → (if((𝐴↑2) = 1, 1, 0) · if((𝐵↑2) = 1, 1, 0)) = if(((𝐴 · 𝐵)↑2) = 1, 1, 0))
75		oveq2 5859	. . . . 5 ⊢ (𝑁 = 0 → (𝐴 /_L 𝑁) = (𝐴 /_L 0))
76		lgs0 13673	. . . . . 6 ⊢ (𝐴 ∈ ℤ → (𝐴 /_L 0) = if((𝐴↑2) = 1, 1, 0))
77	14, 76	syl 14	. . . . 5 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) → (𝐴 /_L 0) = if((𝐴↑2) = 1, 1, 0))
78	75, 77	sylan9eqr 2225	. . . 4 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 = 0) → (𝐴 /_L 𝑁) = if((𝐴↑2) = 1, 1, 0))
79		oveq2 5859	. . . . 5 ⊢ (𝑁 = 0 → (𝐵 /_L 𝑁) = (𝐵 /_L 0))
80		lgs0 13673	. . . . . 6 ⊢ (𝐵 ∈ ℤ → (𝐵 /_L 0) = if((𝐵↑2) = 1, 1, 0))
81	17, 80	syl 14	. . . . 5 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) → (𝐵 /_L 0) = if((𝐵↑2) = 1, 1, 0))
82	79, 81	sylan9eqr 2225	. . . 4 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 = 0) → (𝐵 /_L 𝑁) = if((𝐵↑2) = 1, 1, 0))
83	78, 82	oveq12d 5869	. . 3 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 = 0) → ((𝐴 /_L 𝑁) · (𝐵 /_L 𝑁)) = (if((𝐴↑2) = 1, 1, 0) · if((𝐵↑2) = 1, 1, 0)))
84		oveq2 5859	. . . 4 ⊢ (𝑁 = 0 → ((𝐴 · 𝐵) /_L 𝑁) = ((𝐴 · 𝐵) /_L 0))
85		lgs0 13673	. . . . 5 ⊢ ((𝐴 · 𝐵) ∈ ℤ → ((𝐴 · 𝐵) /_L 0) = if(((𝐴 · 𝐵)↑2) = 1, 1, 0))
86	37, 85	syl 14	. . . 4 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) → ((𝐴 · 𝐵) /_L 0) = if(((𝐴 · 𝐵)↑2) = 1, 1, 0))
87	84, 86	sylan9eqr 2225	. . 3 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 = 0) → ((𝐴 · 𝐵) /_L 𝑁) = if(((𝐴 · 𝐵)↑2) = 1, 1, 0))
88	74, 83, 87	3eqtr4rd 2214	. 2 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 = 0) → ((𝐴 · 𝐵) /_L 𝑁) = ((𝐴 /_L 𝑁) · (𝐵 /_L 𝑁)))
89		lgsdilem 13687	. . . . 5 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) → if((𝑁 < 0 ∧ (𝐴 · 𝐵) < 0), -1, 1) = (if((𝑁 < 0 ∧ 𝐴 < 0), -1, 1) · if((𝑁 < 0 ∧ 𝐵 < 0), -1, 1)))
90	89	adantr 274	. . . 4 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 ≠ 0) → if((𝑁 < 0 ∧ (𝐴 · 𝐵) < 0), -1, 1) = (if((𝑁 < 0 ∧ 𝐴 < 0), -1, 1) · if((𝑁 < 0 ∧ 𝐵 < 0), -1, 1)))
91		simpl3 997	. . . . . . 7 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) → 𝑁 ∈ ℤ)
92		nnabscl 11057	. . . . . . 7 ⊢ ((𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) → (abs‘𝑁) ∈ ℕ)
93	91, 92	sylan 281	. . . . . 6 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 ≠ 0) → (abs‘𝑁) ∈ ℕ)
94		nnuz 9515	. . . . . 6 ⊢ ℕ = (ℤ_≥‘1)
95	93, 94	eleqtrdi 2263	. . . . 5 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 ≠ 0) → (abs‘𝑁) ∈ (ℤ_≥‘1))
96		simpll1 1031	. . . . . . . 8 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 ≠ 0) → 𝐴 ∈ ℤ)
97		simpll3 1033	. . . . . . . 8 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 ≠ 0) → 𝑁 ∈ ℤ)
98		simpr 109	. . . . . . . 8 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 ≠ 0) → 𝑁 ≠ 0)
99		eqid 2170	. . . . . . . . 9 ⊢ (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /_L 𝑛)↑(𝑛 pCnt 𝑁)), 1)) = (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /_L 𝑛)↑(𝑛 pCnt 𝑁)), 1))
100	99	lgsfcl3 13681	. . . . . . . 8 ⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) → (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /_L 𝑛)↑(𝑛 pCnt 𝑁)), 1)):ℕ⟶ℤ)
101	96, 97, 98, 100	syl3anc 1233	. . . . . . 7 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 ≠ 0) → (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /_L 𝑛)↑(𝑛 pCnt 𝑁)), 1)):ℕ⟶ℤ)
102		elnnuz 9516	. . . . . . . 8 ⊢ (𝑘 ∈ ℕ ↔ 𝑘 ∈ (ℤ_≥‘1))
103	102	biimpri 132	. . . . . . 7 ⊢ (𝑘 ∈ (ℤ_≥‘1) → 𝑘 ∈ ℕ)
104		ffvelrn 5627	. . . . . . 7 ⊢ (((𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /_L 𝑛)↑(𝑛 pCnt 𝑁)), 1)):ℕ⟶ℤ ∧ 𝑘 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /_L 𝑛)↑(𝑛 pCnt 𝑁)), 1))‘𝑘) ∈ ℤ)
105	101, 103, 104	syl2an 287	. . . . . 6 ⊢ (((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 ≠ 0) ∧ 𝑘 ∈ (ℤ_≥‘1)) → ((𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /_L 𝑛)↑(𝑛 pCnt 𝑁)), 1))‘𝑘) ∈ ℤ)
106	105	zcnd 9328	. . . . 5 ⊢ (((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 ≠ 0) ∧ 𝑘 ∈ (ℤ_≥‘1)) → ((𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /_L 𝑛)↑(𝑛 pCnt 𝑁)), 1))‘𝑘) ∈ ℂ)
107		simpll2 1032	. . . . . . . 8 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 ≠ 0) → 𝐵 ∈ ℤ)
108		eqid 2170	. . . . . . . . 9 ⊢ (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐵 /_L 𝑛)↑(𝑛 pCnt 𝑁)), 1)) = (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐵 /_L 𝑛)↑(𝑛 pCnt 𝑁)), 1))
109	108	lgsfcl3 13681	. . . . . . . 8 ⊢ ((𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) → (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐵 /_L 𝑛)↑(𝑛 pCnt 𝑁)), 1)):ℕ⟶ℤ)
110	107, 97, 98, 109	syl3anc 1233	. . . . . . 7 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 ≠ 0) → (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐵 /_L 𝑛)↑(𝑛 pCnt 𝑁)), 1)):ℕ⟶ℤ)
111		ffvelrn 5627	. . . . . . 7 ⊢ (((𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐵 /_L 𝑛)↑(𝑛 pCnt 𝑁)), 1)):ℕ⟶ℤ ∧ 𝑘 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐵 /_L 𝑛)↑(𝑛 pCnt 𝑁)), 1))‘𝑘) ∈ ℤ)
112	110, 103, 111	syl2an 287	. . . . . 6 ⊢ (((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 ≠ 0) ∧ 𝑘 ∈ (ℤ_≥‘1)) → ((𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐵 /_L 𝑛)↑(𝑛 pCnt 𝑁)), 1))‘𝑘) ∈ ℤ)
113	112	zcnd 9328	. . . . 5 ⊢ (((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 ≠ 0) ∧ 𝑘 ∈ (ℤ_≥‘1)) → ((𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐵 /_L 𝑛)↑(𝑛 pCnt 𝑁)), 1))‘𝑘) ∈ ℂ)
114	96	adantr 274	. . . . . . . . . . . 12 ⊢ (((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 ≠ 0) ∧ 𝑘 ∈ ℙ) → 𝐴 ∈ ℤ)
115	107	adantr 274	. . . . . . . . . . . 12 ⊢ (((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 ≠ 0) ∧ 𝑘 ∈ ℙ) → 𝐵 ∈ ℤ)
116		simpr 109	. . . . . . . . . . . 12 ⊢ (((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 ≠ 0) ∧ 𝑘 ∈ ℙ) → 𝑘 ∈ ℙ)
117		lgsdirprm 13694	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑘 ∈ ℙ) → ((𝐴 · 𝐵) /_L 𝑘) = ((𝐴 /_L 𝑘) · (𝐵 /_L 𝑘)))
118	114, 115, 116, 117	syl3anc 1233	. . . . . . . . . . 11 ⊢ (((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 ≠ 0) ∧ 𝑘 ∈ ℙ) → ((𝐴 · 𝐵) /_L 𝑘) = ((𝐴 /_L 𝑘) · (𝐵 /_L 𝑘)))
119	118	oveq1d 5866	. . . . . . . . . 10 ⊢ (((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 ≠ 0) ∧ 𝑘 ∈ ℙ) → (((𝐴 · 𝐵) /_L 𝑘)↑(𝑘 pCnt 𝑁)) = (((𝐴 /_L 𝑘) · (𝐵 /_L 𝑘))↑(𝑘 pCnt 𝑁)))
120		prmz 12058	. . . . . . . . . . . . 13 ⊢ (𝑘 ∈ ℙ → 𝑘 ∈ ℤ)
121		lgscl 13674	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ ℤ ∧ 𝑘 ∈ ℤ) → (𝐴 /_L 𝑘) ∈ ℤ)
122	96, 120, 121	syl2an 287	. . . . . . . . . . . 12 ⊢ (((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 ≠ 0) ∧ 𝑘 ∈ ℙ) → (𝐴 /_L 𝑘) ∈ ℤ)
123	122	zcnd 9328	. . . . . . . . . . 11 ⊢ (((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 ≠ 0) ∧ 𝑘 ∈ ℙ) → (𝐴 /_L 𝑘) ∈ ℂ)
124		lgscl 13674	. . . . . . . . . . . . 13 ⊢ ((𝐵 ∈ ℤ ∧ 𝑘 ∈ ℤ) → (𝐵 /_L 𝑘) ∈ ℤ)
125	107, 120, 124	syl2an 287	. . . . . . . . . . . 12 ⊢ (((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 ≠ 0) ∧ 𝑘 ∈ ℙ) → (𝐵 /_L 𝑘) ∈ ℤ)
126	125	zcnd 9328	. . . . . . . . . . 11 ⊢ (((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 ≠ 0) ∧ 𝑘 ∈ ℙ) → (𝐵 /_L 𝑘) ∈ ℂ)
127	97	adantr 274	. . . . . . . . . . . 12 ⊢ (((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 ≠ 0) ∧ 𝑘 ∈ ℙ) → 𝑁 ∈ ℤ)
128	98	adantr 274	. . . . . . . . . . . 12 ⊢ (((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 ≠ 0) ∧ 𝑘 ∈ ℙ) → 𝑁 ≠ 0)
129		pczcl 12245	. . . . . . . . . . . 12 ⊢ ((𝑘 ∈ ℙ ∧ (𝑁 ∈ ℤ ∧ 𝑁 ≠ 0)) → (𝑘 pCnt 𝑁) ∈ ℕ₀)
130	116, 127, 128, 129	syl12anc 1231	. . . . . . . . . . 11 ⊢ (((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 ≠ 0) ∧ 𝑘 ∈ ℙ) → (𝑘 pCnt 𝑁) ∈ ℕ₀)
131	123, 126, 130	mulexpd 10617	. . . . . . . . . 10 ⊢ (((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 ≠ 0) ∧ 𝑘 ∈ ℙ) → (((𝐴 /_L 𝑘) · (𝐵 /_L 𝑘))↑(𝑘 pCnt 𝑁)) = (((𝐴 /_L 𝑘)↑(𝑘 pCnt 𝑁)) · ((𝐵 /_L 𝑘)↑(𝑘 pCnt 𝑁))))
132	119, 131	eqtrd 2203	. . . . . . . . 9 ⊢ (((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 ≠ 0) ∧ 𝑘 ∈ ℙ) → (((𝐴 · 𝐵) /_L 𝑘)↑(𝑘 pCnt 𝑁)) = (((𝐴 /_L 𝑘)↑(𝑘 pCnt 𝑁)) · ((𝐵 /_L 𝑘)↑(𝑘 pCnt 𝑁))))
133		iftrue 3530	. . . . . . . . . 10 ⊢ (𝑘 ∈ ℙ → if(𝑘 ∈ ℙ, (((𝐴 · 𝐵) /_L 𝑘)↑(𝑘 pCnt 𝑁)), 1) = (((𝐴 · 𝐵) /_L 𝑘)↑(𝑘 pCnt 𝑁)))
134	133	adantl 275	. . . . . . . . 9 ⊢ (((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 ≠ 0) ∧ 𝑘 ∈ ℙ) → if(𝑘 ∈ ℙ, (((𝐴 · 𝐵) /_L 𝑘)↑(𝑘 pCnt 𝑁)), 1) = (((𝐴 · 𝐵) /_L 𝑘)↑(𝑘 pCnt 𝑁)))
135		iftrue 3530	. . . . . . . . . . 11 ⊢ (𝑘 ∈ ℙ → if(𝑘 ∈ ℙ, ((𝐴 /_L 𝑘)↑(𝑘 pCnt 𝑁)), 1) = ((𝐴 /_L 𝑘)↑(𝑘 pCnt 𝑁)))
136		iftrue 3530	. . . . . . . . . . 11 ⊢ (𝑘 ∈ ℙ → if(𝑘 ∈ ℙ, ((𝐵 /_L 𝑘)↑(𝑘 pCnt 𝑁)), 1) = ((𝐵 /_L 𝑘)↑(𝑘 pCnt 𝑁)))
137	135, 136	oveq12d 5869	. . . . . . . . . 10 ⊢ (𝑘 ∈ ℙ → (if(𝑘 ∈ ℙ, ((𝐴 /_L 𝑘)↑(𝑘 pCnt 𝑁)), 1) · if(𝑘 ∈ ℙ, ((𝐵 /_L 𝑘)↑(𝑘 pCnt 𝑁)), 1)) = (((𝐴 /_L 𝑘)↑(𝑘 pCnt 𝑁)) · ((𝐵 /_L 𝑘)↑(𝑘 pCnt 𝑁))))
138	137	adantl 275	. . . . . . . . 9 ⊢ (((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 ≠ 0) ∧ 𝑘 ∈ ℙ) → (if(𝑘 ∈ ℙ, ((𝐴 /_L 𝑘)↑(𝑘 pCnt 𝑁)), 1) · if(𝑘 ∈ ℙ, ((𝐵 /_L 𝑘)↑(𝑘 pCnt 𝑁)), 1)) = (((𝐴 /_L 𝑘)↑(𝑘 pCnt 𝑁)) · ((𝐵 /_L 𝑘)↑(𝑘 pCnt 𝑁))))
139	132, 134, 138	3eqtr4d 2213	. . . . . . . 8 ⊢ (((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 ≠ 0) ∧ 𝑘 ∈ ℙ) → if(𝑘 ∈ ℙ, (((𝐴 · 𝐵) /_L 𝑘)↑(𝑘 pCnt 𝑁)), 1) = (if(𝑘 ∈ ℙ, ((𝐴 /_L 𝑘)↑(𝑘 pCnt 𝑁)), 1) · if(𝑘 ∈ ℙ, ((𝐵 /_L 𝑘)↑(𝑘 pCnt 𝑁)), 1)))
140	139	adantlr 474	. . . . . . 7 ⊢ ((((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 ≠ 0) ∧ 𝑘 ∈ (ℤ_≥‘1)) ∧ 𝑘 ∈ ℙ) → if(𝑘 ∈ ℙ, (((𝐴 · 𝐵) /_L 𝑘)↑(𝑘 pCnt 𝑁)), 1) = (if(𝑘 ∈ ℙ, ((𝐴 /_L 𝑘)↑(𝑘 pCnt 𝑁)), 1) · if(𝑘 ∈ ℙ, ((𝐵 /_L 𝑘)↑(𝑘 pCnt 𝑁)), 1)))
141		1t1e1 9023	. . . . . . . . . 10 ⊢ (1 · 1) = 1
142	141	eqcomi 2174	. . . . . . . . 9 ⊢ 1 = (1 · 1)
143		iffalse 3533	. . . . . . . . 9 ⊢ (¬ 𝑘 ∈ ℙ → if(𝑘 ∈ ℙ, (((𝐴 · 𝐵) /_L 𝑘)↑(𝑘 pCnt 𝑁)), 1) = 1)
144		iffalse 3533	. . . . . . . . . 10 ⊢ (¬ 𝑘 ∈ ℙ → if(𝑘 ∈ ℙ, ((𝐴 /_L 𝑘)↑(𝑘 pCnt 𝑁)), 1) = 1)
145		iffalse 3533	. . . . . . . . . 10 ⊢ (¬ 𝑘 ∈ ℙ → if(𝑘 ∈ ℙ, ((𝐵 /_L 𝑘)↑(𝑘 pCnt 𝑁)), 1) = 1)
146	144, 145	oveq12d 5869	. . . . . . . . 9 ⊢ (¬ 𝑘 ∈ ℙ → (if(𝑘 ∈ ℙ, ((𝐴 /_L 𝑘)↑(𝑘 pCnt 𝑁)), 1) · if(𝑘 ∈ ℙ, ((𝐵 /_L 𝑘)↑(𝑘 pCnt 𝑁)), 1)) = (1 · 1))
147	142, 143, 146	3eqtr4a 2229	. . . . . . . 8 ⊢ (¬ 𝑘 ∈ ℙ → if(𝑘 ∈ ℙ, (((𝐴 · 𝐵) /_L 𝑘)↑(𝑘 pCnt 𝑁)), 1) = (if(𝑘 ∈ ℙ, ((𝐴 /_L 𝑘)↑(𝑘 pCnt 𝑁)), 1) · if(𝑘 ∈ ℙ, ((𝐵 /_L 𝑘)↑(𝑘 pCnt 𝑁)), 1)))
148	147	adantl 275	. . . . . . 7 ⊢ ((((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 ≠ 0) ∧ 𝑘 ∈ (ℤ_≥‘1)) ∧ ¬ 𝑘 ∈ ℙ) → if(𝑘 ∈ ℙ, (((𝐴 · 𝐵) /_L 𝑘)↑(𝑘 pCnt 𝑁)), 1) = (if(𝑘 ∈ ℙ, ((𝐴 /_L 𝑘)↑(𝑘 pCnt 𝑁)), 1) · if(𝑘 ∈ ℙ, ((𝐵 /_L 𝑘)↑(𝑘 pCnt 𝑁)), 1)))
149	103	adantl 275	. . . . . . . . 9 ⊢ (((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 ≠ 0) ∧ 𝑘 ∈ (ℤ_≥‘1)) → 𝑘 ∈ ℕ)
150		prmdc 12077	. . . . . . . . 9 ⊢ (𝑘 ∈ ℕ → DECID 𝑘 ∈ ℙ)
151	149, 150	syl 14	. . . . . . . 8 ⊢ (((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 ≠ 0) ∧ 𝑘 ∈ (ℤ_≥‘1)) → DECID 𝑘 ∈ ℙ)
152		exmiddc 831	. . . . . . . 8 ⊢ (DECID 𝑘 ∈ ℙ → (𝑘 ∈ ℙ ∨ ¬ 𝑘 ∈ ℙ))
153	151, 152	syl 14	. . . . . . 7 ⊢ (((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 ≠ 0) ∧ 𝑘 ∈ (ℤ_≥‘1)) → (𝑘 ∈ ℙ ∨ ¬ 𝑘 ∈ ℙ))
154	140, 148, 153	mpjaodan 793	. . . . . 6 ⊢ (((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 ≠ 0) ∧ 𝑘 ∈ (ℤ_≥‘1)) → if(𝑘 ∈ ℙ, (((𝐴 · 𝐵) /_L 𝑘)↑(𝑘 pCnt 𝑁)), 1) = (if(𝑘 ∈ ℙ, ((𝐴 /_L 𝑘)↑(𝑘 pCnt 𝑁)), 1) · if(𝑘 ∈ ℙ, ((𝐵 /_L 𝑘)↑(𝑘 pCnt 𝑁)), 1)))
155		eqid 2170	. . . . . . 7 ⊢ (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, (((𝐴 · 𝐵) /_L 𝑛)↑(𝑛 pCnt 𝑁)), 1)) = (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, (((𝐴 · 𝐵) /_L 𝑛)↑(𝑛 pCnt 𝑁)), 1))
156		eleq1w 2231	. . . . . . . 8 ⊢ (𝑛 = 𝑘 → (𝑛 ∈ ℙ ↔ 𝑘 ∈ ℙ))
157		oveq2 5859	. . . . . . . . 9 ⊢ (𝑛 = 𝑘 → ((𝐴 · 𝐵) /_L 𝑛) = ((𝐴 · 𝐵) /_L 𝑘))
158		oveq1 5858	. . . . . . . . 9 ⊢ (𝑛 = 𝑘 → (𝑛 pCnt 𝑁) = (𝑘 pCnt 𝑁))
159	157, 158	oveq12d 5869	. . . . . . . 8 ⊢ (𝑛 = 𝑘 → (((𝐴 · 𝐵) /_L 𝑛)↑(𝑛 pCnt 𝑁)) = (((𝐴 · 𝐵) /_L 𝑘)↑(𝑘 pCnt 𝑁)))
160	156, 159	ifbieq1d 3547	. . . . . . 7 ⊢ (𝑛 = 𝑘 → if(𝑛 ∈ ℙ, (((𝐴 · 𝐵) /_L 𝑛)↑(𝑛 pCnt 𝑁)), 1) = if(𝑘 ∈ ℙ, (((𝐴 · 𝐵) /_L 𝑘)↑(𝑘 pCnt 𝑁)), 1))
161	37	ad3antrrr 489	. . . . . . . . . 10 ⊢ ((((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 ≠ 0) ∧ 𝑘 ∈ (ℤ_≥‘1)) ∧ 𝑘 ∈ ℙ) → (𝐴 · 𝐵) ∈ ℤ)
162	120	adantl 275	. . . . . . . . . 10 ⊢ ((((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 ≠ 0) ∧ 𝑘 ∈ (ℤ_≥‘1)) ∧ 𝑘 ∈ ℙ) → 𝑘 ∈ ℤ)
163		lgscl 13674	. . . . . . . . . 10 ⊢ (((𝐴 · 𝐵) ∈ ℤ ∧ 𝑘 ∈ ℤ) → ((𝐴 · 𝐵) /_L 𝑘) ∈ ℤ)
164	161, 162, 163	syl2anc 409	. . . . . . . . 9 ⊢ ((((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 ≠ 0) ∧ 𝑘 ∈ (ℤ_≥‘1)) ∧ 𝑘 ∈ ℙ) → ((𝐴 · 𝐵) /_L 𝑘) ∈ ℤ)
165	130	adantlr 474	. . . . . . . . 9 ⊢ ((((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 ≠ 0) ∧ 𝑘 ∈ (ℤ_≥‘1)) ∧ 𝑘 ∈ ℙ) → (𝑘 pCnt 𝑁) ∈ ℕ₀)
166		zexpcl 10484	. . . . . . . . 9 ⊢ ((((𝐴 · 𝐵) /_L 𝑘) ∈ ℤ ∧ (𝑘 pCnt 𝑁) ∈ ℕ₀) → (((𝐴 · 𝐵) /_L 𝑘)↑(𝑘 pCnt 𝑁)) ∈ ℤ)
167	164, 165, 166	syl2anc 409	. . . . . . . 8 ⊢ ((((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 ≠ 0) ∧ 𝑘 ∈ (ℤ_≥‘1)) ∧ 𝑘 ∈ ℙ) → (((𝐴 · 𝐵) /_L 𝑘)↑(𝑘 pCnt 𝑁)) ∈ ℤ)
168		1zzd 9232	. . . . . . . 8 ⊢ ((((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 ≠ 0) ∧ 𝑘 ∈ (ℤ_≥‘1)) ∧ ¬ 𝑘 ∈ ℙ) → 1 ∈ ℤ)
169	167, 168, 151	ifcldadc 3554	. . . . . . 7 ⊢ (((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 ≠ 0) ∧ 𝑘 ∈ (ℤ_≥‘1)) → if(𝑘 ∈ ℙ, (((𝐴 · 𝐵) /_L 𝑘)↑(𝑘 pCnt 𝑁)), 1) ∈ ℤ)
170	155, 160, 149, 169	fvmptd3 5587	. . . . . 6 ⊢ (((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 ≠ 0) ∧ 𝑘 ∈ (ℤ_≥‘1)) → ((𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, (((𝐴 · 𝐵) /_L 𝑛)↑(𝑛 pCnt 𝑁)), 1))‘𝑘) = if(𝑘 ∈ ℙ, (((𝐴 · 𝐵) /_L 𝑘)↑(𝑘 pCnt 𝑁)), 1))
171		oveq2 5859	. . . . . . . . . 10 ⊢ (𝑛 = 𝑘 → (𝐴 /_L 𝑛) = (𝐴 /_L 𝑘))
172	171, 158	oveq12d 5869	. . . . . . . . 9 ⊢ (𝑛 = 𝑘 → ((𝐴 /_L 𝑛)↑(𝑛 pCnt 𝑁)) = ((𝐴 /_L 𝑘)↑(𝑘 pCnt 𝑁)))
173	156, 172	ifbieq1d 3547	. . . . . . . 8 ⊢ (𝑛 = 𝑘 → if(𝑛 ∈ ℙ, ((𝐴 /_L 𝑛)↑(𝑛 pCnt 𝑁)), 1) = if(𝑘 ∈ ℙ, ((𝐴 /_L 𝑘)↑(𝑘 pCnt 𝑁)), 1))
174	122	adantlr 474	. . . . . . . . . 10 ⊢ ((((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 ≠ 0) ∧ 𝑘 ∈ (ℤ_≥‘1)) ∧ 𝑘 ∈ ℙ) → (𝐴 /_L 𝑘) ∈ ℤ)
175		zexpcl 10484	. . . . . . . . . 10 ⊢ (((𝐴 /_L 𝑘) ∈ ℤ ∧ (𝑘 pCnt 𝑁) ∈ ℕ₀) → ((𝐴 /_L 𝑘)↑(𝑘 pCnt 𝑁)) ∈ ℤ)
176	174, 165, 175	syl2anc 409	. . . . . . . . 9 ⊢ ((((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 ≠ 0) ∧ 𝑘 ∈ (ℤ_≥‘1)) ∧ 𝑘 ∈ ℙ) → ((𝐴 /_L 𝑘)↑(𝑘 pCnt 𝑁)) ∈ ℤ)
177	176, 168, 151	ifcldadc 3554	. . . . . . . 8 ⊢ (((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 ≠ 0) ∧ 𝑘 ∈ (ℤ_≥‘1)) → if(𝑘 ∈ ℙ, ((𝐴 /_L 𝑘)↑(𝑘 pCnt 𝑁)), 1) ∈ ℤ)
178	99, 173, 149, 177	fvmptd3 5587	. . . . . . 7 ⊢ (((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 ≠ 0) ∧ 𝑘 ∈ (ℤ_≥‘1)) → ((𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /_L 𝑛)↑(𝑛 pCnt 𝑁)), 1))‘𝑘) = if(𝑘 ∈ ℙ, ((𝐴 /_L 𝑘)↑(𝑘 pCnt 𝑁)), 1))
179		oveq2 5859	. . . . . . . . . 10 ⊢ (𝑛 = 𝑘 → (𝐵 /_L 𝑛) = (𝐵 /_L 𝑘))
180	179, 158	oveq12d 5869	. . . . . . . . 9 ⊢ (𝑛 = 𝑘 → ((𝐵 /_L 𝑛)↑(𝑛 pCnt 𝑁)) = ((𝐵 /_L 𝑘)↑(𝑘 pCnt 𝑁)))
181	156, 180	ifbieq1d 3547	. . . . . . . 8 ⊢ (𝑛 = 𝑘 → if(𝑛 ∈ ℙ, ((𝐵 /_L 𝑛)↑(𝑛 pCnt 𝑁)), 1) = if(𝑘 ∈ ℙ, ((𝐵 /_L 𝑘)↑(𝑘 pCnt 𝑁)), 1))
182	125	adantlr 474	. . . . . . . . . 10 ⊢ ((((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 ≠ 0) ∧ 𝑘 ∈ (ℤ_≥‘1)) ∧ 𝑘 ∈ ℙ) → (𝐵 /_L 𝑘) ∈ ℤ)
183		zexpcl 10484	. . . . . . . . . 10 ⊢ (((𝐵 /_L 𝑘) ∈ ℤ ∧ (𝑘 pCnt 𝑁) ∈ ℕ₀) → ((𝐵 /_L 𝑘)↑(𝑘 pCnt 𝑁)) ∈ ℤ)
184	182, 165, 183	syl2anc 409	. . . . . . . . 9 ⊢ ((((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 ≠ 0) ∧ 𝑘 ∈ (ℤ_≥‘1)) ∧ 𝑘 ∈ ℙ) → ((𝐵 /_L 𝑘)↑(𝑘 pCnt 𝑁)) ∈ ℤ)
185	184, 168, 151	ifcldadc 3554	. . . . . . . 8 ⊢ (((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 ≠ 0) ∧ 𝑘 ∈ (ℤ_≥‘1)) → if(𝑘 ∈ ℙ, ((𝐵 /_L 𝑘)↑(𝑘 pCnt 𝑁)), 1) ∈ ℤ)
186	108, 181, 149, 185	fvmptd3 5587	. . . . . . 7 ⊢ (((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 ≠ 0) ∧ 𝑘 ∈ (ℤ_≥‘1)) → ((𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐵 /_L 𝑛)↑(𝑛 pCnt 𝑁)), 1))‘𝑘) = if(𝑘 ∈ ℙ, ((𝐵 /_L 𝑘)↑(𝑘 pCnt 𝑁)), 1))
187	178, 186	oveq12d 5869	. . . . . 6 ⊢ (((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 ≠ 0) ∧ 𝑘 ∈ (ℤ_≥‘1)) → (((𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /_L 𝑛)↑(𝑛 pCnt 𝑁)), 1))‘𝑘) · ((𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐵 /_L 𝑛)↑(𝑛 pCnt 𝑁)), 1))‘𝑘)) = (if(𝑘 ∈ ℙ, ((𝐴 /_L 𝑘)↑(𝑘 pCnt 𝑁)), 1) · if(𝑘 ∈ ℙ, ((𝐵 /_L 𝑘)↑(𝑘 pCnt 𝑁)), 1)))
188	154, 170, 187	3eqtr4d 2213	. . . . 5 ⊢ (((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 ≠ 0) ∧ 𝑘 ∈ (ℤ_≥‘1)) → ((𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, (((𝐴 · 𝐵) /_L 𝑛)↑(𝑛 pCnt 𝑁)), 1))‘𝑘) = (((𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /_L 𝑛)↑(𝑛 pCnt 𝑁)), 1))‘𝑘) · ((𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐵 /_L 𝑛)↑(𝑛 pCnt 𝑁)), 1))‘𝑘)))
189	95, 106, 113, 188	prod3fmul 11497	. . . 4 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 ≠ 0) → (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, (((𝐴 · 𝐵) /_L 𝑛)↑(𝑛 pCnt 𝑁)), 1)))‘(abs‘𝑁)) = ((seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /_L 𝑛)↑(𝑛 pCnt 𝑁)), 1)))‘(abs‘𝑁)) · (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐵 /_L 𝑛)↑(𝑛 pCnt 𝑁)), 1)))‘(abs‘𝑁))))
190	90, 189	oveq12d 5869	. . 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‘𝑁)))))
191	37	adantr 274	. . . 4 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 ≠ 0) → (𝐴 · 𝐵) ∈ ℤ)
192	155	lgsval4 13680	. . . 4 ⊢ (((𝐴 · 𝐵) ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) → ((𝐴 · 𝐵) /_L 𝑁) = (if((𝑁 < 0 ∧ (𝐴 · 𝐵) < 0), -1, 1) · (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, (((𝐴 · 𝐵) /_L 𝑛)↑(𝑛 pCnt 𝑁)), 1)))‘(abs‘𝑁))))
193	191, 97, 98, 192	syl3anc 1233	. . 3 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 ≠ 0) → ((𝐴 · 𝐵) /_L 𝑁) = (if((𝑁 < 0 ∧ (𝐴 · 𝐵) < 0), -1, 1) · (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, (((𝐴 · 𝐵) /_L 𝑛)↑(𝑛 pCnt 𝑁)), 1)))‘(abs‘𝑁))))
194	99	lgsval4 13680	. . . . . 6 ⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) → (𝐴 /_L 𝑁) = (if((𝑁 < 0 ∧ 𝐴 < 0), -1, 1) · (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /_L 𝑛)↑(𝑛 pCnt 𝑁)), 1)))‘(abs‘𝑁))))
195	96, 97, 98, 194	syl3anc 1233	. . . . 5 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 ≠ 0) → (𝐴 /_L 𝑁) = (if((𝑁 < 0 ∧ 𝐴 < 0), -1, 1) · (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /_L 𝑛)↑(𝑛 pCnt 𝑁)), 1)))‘(abs‘𝑁))))
196	108	lgsval4 13680	. . . . . 6 ⊢ ((𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) → (𝐵 /_L 𝑁) = (if((𝑁 < 0 ∧ 𝐵 < 0), -1, 1) · (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐵 /_L 𝑛)↑(𝑛 pCnt 𝑁)), 1)))‘(abs‘𝑁))))
197	107, 97, 98, 196	syl3anc 1233	. . . . 5 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 ≠ 0) → (𝐵 /_L 𝑁) = (if((𝑁 < 0 ∧ 𝐵 < 0), -1, 1) · (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐵 /_L 𝑛)↑(𝑛 pCnt 𝑁)), 1)))‘(abs‘𝑁))))
198	195, 197	oveq12d 5869	. . . 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‘𝑁)))))
199		neg1cn 8976	. . . . . . 7 ⊢ -1 ∈ ℂ
200	199	a1i 9	. . . . . 6 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 ≠ 0) → -1 ∈ ℂ)
201		1cnd 7929	. . . . . 6 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 ≠ 0) → 1 ∈ ℂ)
202		0z 9216	. . . . . . . 8 ⊢ 0 ∈ ℤ
203		zdclt 9282	. . . . . . . 8 ⊢ ((𝑁 ∈ ℤ ∧ 0 ∈ ℤ) → DECID 𝑁 < 0)
204	97, 202, 203	sylancl 411	. . . . . . 7 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 ≠ 0) → DECID 𝑁 < 0)
205		zdclt 9282	. . . . . . . 8 ⊢ ((𝐴 ∈ ℤ ∧ 0 ∈ ℤ) → DECID 𝐴 < 0)
206	96, 202, 205	sylancl 411	. . . . . . 7 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 ≠ 0) → DECID 𝐴 < 0)
207		dcan2 929	. . . . . . 7 ⊢ (DECID 𝑁 < 0 → (DECID 𝐴 < 0 → DECID (𝑁 < 0 ∧ 𝐴 < 0)))
208	204, 206, 207	sylc 62	. . . . . 6 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 ≠ 0) → DECID (𝑁 < 0 ∧ 𝐴 < 0))
209	200, 201, 208	ifcldcd 3560	. . . . 5 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 ≠ 0) → if((𝑁 < 0 ∧ 𝐴 < 0), -1, 1) ∈ ℂ)
210		1zzd 9232	. . . . . . . 8 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 ≠ 0) → 1 ∈ ℤ)
211	101	ffvelrnda 5629	. . . . . . . 8 ⊢ (((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 ≠ 0) ∧ 𝑘 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /_L 𝑛)↑(𝑛 pCnt 𝑁)), 1))‘𝑘) ∈ ℤ)
212		zmulcl 9258	. . . . . . . . 9 ⊢ ((𝑘 ∈ ℤ ∧ 𝑣 ∈ ℤ) → (𝑘 · 𝑣) ∈ ℤ)
213	212	adantl 275	. . . . . . . 8 ⊢ (((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 ≠ 0) ∧ (𝑘 ∈ ℤ ∧ 𝑣 ∈ ℤ)) → (𝑘 · 𝑣) ∈ ℤ)
214	94, 210, 211, 213	seqf 10410	. . . . . . 7 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 ≠ 0) → seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /_L 𝑛)↑(𝑛 pCnt 𝑁)), 1))):ℕ⟶ℤ)
215	214, 93	ffvelrnd 5630	. . . . . 6 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 ≠ 0) → (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /_L 𝑛)↑(𝑛 pCnt 𝑁)), 1)))‘(abs‘𝑁)) ∈ ℤ)
216	215	zcnd 9328	. . . . 5 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 ≠ 0) → (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /_L 𝑛)↑(𝑛 pCnt 𝑁)), 1)))‘(abs‘𝑁)) ∈ ℂ)
217		neg1z 9237	. . . . . . . 8 ⊢ -1 ∈ ℤ
218	217	a1i 9	. . . . . . 7 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 ≠ 0) → -1 ∈ ℤ)
219		zdclt 9282	. . . . . . . . 9 ⊢ ((𝐵 ∈ ℤ ∧ 0 ∈ ℤ) → DECID 𝐵 < 0)
220	107, 202, 219	sylancl 411	. . . . . . . 8 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 ≠ 0) → DECID 𝐵 < 0)
221		dcan2 929	. . . . . . . 8 ⊢ (DECID 𝑁 < 0 → (DECID 𝐵 < 0 → DECID (𝑁 < 0 ∧ 𝐵 < 0)))
222	204, 220, 221	sylc 62	. . . . . . 7 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 ≠ 0) → DECID (𝑁 < 0 ∧ 𝐵 < 0))
223	218, 210, 222	ifcldcd 3560	. . . . . 6 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 ≠ 0) → if((𝑁 < 0 ∧ 𝐵 < 0), -1, 1) ∈ ℤ)
224	223	zcnd 9328	. . . . 5 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 ≠ 0) → if((𝑁 < 0 ∧ 𝐵 < 0), -1, 1) ∈ ℂ)
225	110	ffvelrnda 5629	. . . . . . . 8 ⊢ (((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 ≠ 0) ∧ 𝑘 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐵 /_L 𝑛)↑(𝑛 pCnt 𝑁)), 1))‘𝑘) ∈ ℤ)
226	94, 210, 225, 213	seqf 10410	. . . . . . 7 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 ≠ 0) → seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐵 /_L 𝑛)↑(𝑛 pCnt 𝑁)), 1))):ℕ⟶ℤ)
227	226, 93	ffvelrnd 5630	. . . . . 6 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 ≠ 0) → (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐵 /_L 𝑛)↑(𝑛 pCnt 𝑁)), 1)))‘(abs‘𝑁)) ∈ ℤ)
228	227	zcnd 9328	. . . . 5 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 ≠ 0) → (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐵 /_L 𝑛)↑(𝑛 pCnt 𝑁)), 1)))‘(abs‘𝑁)) ∈ ℂ)
229	209, 216, 224, 228	mul4d 8067	. . . 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‘𝑁)))))
230	198, 229	eqtrd 2203	. . 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‘𝑁)))))
231	190, 193, 230	3eqtr4d 2213	. 2 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ 𝑁 ≠ 0) → ((𝐴 · 𝐵) /_L 𝑁) = ((𝐴 /_L 𝑁) · (𝐵 /_L 𝑁)))
232		zdceq 9280	. . . 4 ⊢ ((𝑁 ∈ ℤ ∧ 0 ∈ ℤ) → DECID 𝑁 = 0)
233	91, 202, 232	sylancl 411	. . 3 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) → DECID 𝑁 = 0)
234		dcne 2351	. . 3 ⊢ (DECID 𝑁 = 0 ↔ (𝑁 = 0 ∨ 𝑁 ≠ 0))
235	233, 234	sylib 121	. 2 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) → (𝑁 = 0 ∨ 𝑁 ≠ 0))
236	88, 231, 235	mpjaodan 793	1 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) → ((𝐴 · 𝐵) /_L 𝑁) = ((𝐴 /_L 𝑁) · (𝐵 /_L 𝑁)))

Colors of variables: wff set class

Syntax hints: ¬ wn 3 → wi 4 ∧ wa 103 ↔ wb 104 ∨ wo 703 DECID wdc 829 ∧ w3a 973 = wceq 1348 ∈ wcel 2141 ≠ wne 2340 ifcif 3525 class class class wbr 3987 ↦ cmpt 4048 ⟶wf 5192 ‘cfv 5196 (class class class)co 5851 ℂcc 7765 ℝcr 7766 0cc0 7767 1c1 7768 · cmul 7772 < clt 7947 ≤ cle 7948 -cneg 8084 ℕcn 8871 2c2 8922 ℕ₀cn0 9128 ℤcz 9205 ℤ_≥cuz 9480 seqcseq 10394 ↑cexp 10468 abscabs 10954 ∥ cdvds 11742 ℙcprime 12054 pCnt cpc 12231 /_L clgs 13657

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-in1 609 ax-in2 610 ax-io 704 ax-5 1440 ax-7 1441 ax-gen 1442 ax-ie1 1486 ax-ie2 1487 ax-8 1497 ax-10 1498 ax-11 1499 ax-i12 1500 ax-bndl 1502 ax-4 1503 ax-17 1519 ax-i9 1523 ax-ial 1527 ax-i5r 1528 ax-13 2143 ax-14 2144 ax-ext 2152 ax-coll 4102 ax-sep 4105 ax-nul 4113 ax-pow 4158 ax-pr 4192 ax-un 4416 ax-setind 4519 ax-iinf 4570 ax-cnex 7858 ax-resscn 7859 ax-1cn 7860 ax-1re 7861 ax-icn 7862 ax-addcl 7863 ax-addrcl 7864 ax-mulcl 7865 ax-mulrcl 7866 ax-addcom 7867 ax-mulcom 7868 ax-addass 7869 ax-mulass 7870 ax-distr 7871 ax-i2m1 7872 ax-0lt1 7873 ax-1rid 7874 ax-0id 7875 ax-rnegex 7876 ax-precex 7877 ax-cnre 7878 ax-pre-ltirr 7879 ax-pre-ltwlin 7880 ax-pre-lttrn 7881 ax-pre-apti 7882 ax-pre-ltadd 7883 ax-pre-mulgt0 7884 ax-pre-mulext 7885 ax-arch 7886 ax-caucvg 7887

This theorem depends on definitions: df-bi 116 df-stab 826 df-dc 830 df-3or 974 df-3an 975 df-tru 1351 df-fal 1354 df-xor 1371 df-nf 1454 df-sb 1756 df-eu 2022 df-mo 2023 df-clab 2157 df-cleq 2163 df-clel 2166 df-nfc 2301 df-ne 2341 df-nel 2436 df-ral 2453 df-rex 2454 df-reu 2455 df-rmo 2456 df-rab 2457 df-v 2732 df-sbc 2956 df-csb 3050 df-dif 3123 df-un 3125 df-in 3127 df-ss 3134 df-nul 3415 df-if 3526 df-pw 3566 df-sn 3587 df-pr 3588 df-op 3590 df-uni 3795 df-int 3830 df-iun 3873 df-br 3988 df-opab 4049 df-mpt 4050 df-tr 4086 df-id 4276 df-po 4279 df-iso 4280 df-iord 4349 df-on 4351 df-ilim 4352 df-suc 4354 df-iom 4573 df-xp 4615 df-rel 4616 df-cnv 4617 df-co 4618 df-dm 4619 df-rn 4620 df-res 4621 df-ima 4622 df-iota 5158 df-fun 5198 df-fn 5199 df-f 5200 df-f1 5201 df-fo 5202 df-f1o 5203 df-fv 5204 df-isom 5205 df-riota 5807 df-ov 5854 df-oprab 5855 df-mpo 5856 df-1st 6117 df-2nd 6118 df-recs 6282 df-irdg 6347 df-frec 6368 df-1o 6393 df-2o 6394 df-oadd 6397 df-er 6511 df-en 6717 df-dom 6718 df-fin 6719 df-sup 6959 df-inf 6960 df-pnf 7949 df-mnf 7950 df-xr 7951 df-ltxr 7952 df-le 7953 df-sub 8085 df-neg 8086 df-reap 8487 df-ap 8494 df-div 8583 df-inn 8872 df-2 8930 df-3 8931 df-4 8932 df-5 8933 df-6 8934 df-7 8935 df-8 8936 df-9 8937 df-n0 9129 df-z 9206 df-uz 9481 df-q 9572 df-rp 9604 df-fz 9959 df-fzo 10092 df-fl 10219 df-mod 10272 df-seqfrec 10395 df-exp 10469 df-ihash 10703 df-cj 10799 df-re 10800 df-im 10801 df-rsqrt 10955 df-abs 10956 df-clim 11235 df-proddc 11507 df-dvds 11743 df-gcd 11891 df-prm 12055 df-phi 12158 df-pc 12232 df-lgs 13658

This theorem is referenced by: lgssq 13700 lgsmulsqcoprm 13706 lgsdirnn0 13707

W3C validator