lgsdi - Intuitionistic Logic Explorer

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

Theorem lgsdi 14891

Description: The Legendre symbol is completely multiplicative in its right argument. Generalization of theorem 9.9(b) in [ApostolNT] p. 188 (which assumes that 𝑀 and 𝑁 are odd positive integers). (Contributed by Mario Carneiro, 5-Feb-2015.)

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

Proof of Theorem lgsdi Dummy variables 𝑘 𝑛 𝑣 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		3anrot 985	. . . . 5 ⊢ ((𝐴 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ↔ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐴 ∈ ℤ))
2		lgsdilem 14881	. . . . 5 ⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐴 ∈ ℤ) ∧ (𝑀 ≠ 0 ∧ 𝑁 ≠ 0)) → if((𝐴 < 0 ∧ (𝑀 · 𝑁) < 0), -1, 1) = (if((𝐴 < 0 ∧ 𝑀 < 0), -1, 1) · if((𝐴 < 0 ∧ 𝑁 < 0), -1, 1)))
3	1, 2	sylanb 284	. . . 4 ⊢ (((𝐴 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑀 ≠ 0 ∧ 𝑁 ≠ 0)) → if((𝐴 < 0 ∧ (𝑀 · 𝑁) < 0), -1, 1) = (if((𝐴 < 0 ∧ 𝑀 < 0), -1, 1) · if((𝐴 < 0 ∧ 𝑁 < 0), -1, 1)))
4		ancom 266	. . . . 5 ⊢ (((𝑀 · 𝑁) < 0 ∧ 𝐴 < 0) ↔ (𝐴 < 0 ∧ (𝑀 · 𝑁) < 0))
5		ifbi 3569	. . . . 5 ⊢ ((((𝑀 · 𝑁) < 0 ∧ 𝐴 < 0) ↔ (𝐴 < 0 ∧ (𝑀 · 𝑁) < 0)) → if(((𝑀 · 𝑁) < 0 ∧ 𝐴 < 0), -1, 1) = if((𝐴 < 0 ∧ (𝑀 · 𝑁) < 0), -1, 1))
6	4, 5	ax-mp 5	. . . 4 ⊢ if(((𝑀 · 𝑁) < 0 ∧ 𝐴 < 0), -1, 1) = if((𝐴 < 0 ∧ (𝑀 · 𝑁) < 0), -1, 1)
7		ancom 266	. . . . . 6 ⊢ ((𝑀 < 0 ∧ 𝐴 < 0) ↔ (𝐴 < 0 ∧ 𝑀 < 0))
8		ifbi 3569	. . . . . 6 ⊢ (((𝑀 < 0 ∧ 𝐴 < 0) ↔ (𝐴 < 0 ∧ 𝑀 < 0)) → if((𝑀 < 0 ∧ 𝐴 < 0), -1, 1) = if((𝐴 < 0 ∧ 𝑀 < 0), -1, 1))
9	7, 8	ax-mp 5	. . . . 5 ⊢ if((𝑀 < 0 ∧ 𝐴 < 0), -1, 1) = if((𝐴 < 0 ∧ 𝑀 < 0), -1, 1)
10		ancom 266	. . . . . 6 ⊢ ((𝑁 < 0 ∧ 𝐴 < 0) ↔ (𝐴 < 0 ∧ 𝑁 < 0))
11		ifbi 3569	. . . . . 6 ⊢ (((𝑁 < 0 ∧ 𝐴 < 0) ↔ (𝐴 < 0 ∧ 𝑁 < 0)) → if((𝑁 < 0 ∧ 𝐴 < 0), -1, 1) = if((𝐴 < 0 ∧ 𝑁 < 0), -1, 1))
12	10, 11	ax-mp 5	. . . . 5 ⊢ if((𝑁 < 0 ∧ 𝐴 < 0), -1, 1) = if((𝐴 < 0 ∧ 𝑁 < 0), -1, 1)
13	9, 12	oveq12i 5907	. . . 4 ⊢ (if((𝑀 < 0 ∧ 𝐴 < 0), -1, 1) · if((𝑁 < 0 ∧ 𝐴 < 0), -1, 1)) = (if((𝐴 < 0 ∧ 𝑀 < 0), -1, 1) · if((𝐴 < 0 ∧ 𝑁 < 0), -1, 1))
14	3, 6, 13	3eqtr4g 2247	. . 3 ⊢ (((𝐴 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑀 ≠ 0 ∧ 𝑁 ≠ 0)) → if(((𝑀 · 𝑁) < 0 ∧ 𝐴 < 0), -1, 1) = (if((𝑀 < 0 ∧ 𝐴 < 0), -1, 1) · if((𝑁 < 0 ∧ 𝐴 < 0), -1, 1)))
15		simpl2 1003	. . . . . . . 8 ⊢ (((𝐴 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑀 ≠ 0 ∧ 𝑁 ≠ 0)) → 𝑀 ∈ ℤ)
16		simpl3 1004	. . . . . . . 8 ⊢ (((𝐴 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑀 ≠ 0 ∧ 𝑁 ≠ 0)) → 𝑁 ∈ ℤ)
17	15, 16	zmulcld 9410	. . . . . . 7 ⊢ (((𝐴 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑀 ≠ 0 ∧ 𝑁 ≠ 0)) → (𝑀 · 𝑁) ∈ ℤ)
18	15	zcnd 9405	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑀 ≠ 0 ∧ 𝑁 ≠ 0)) → 𝑀 ∈ ℂ)
19	16	zcnd 9405	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑀 ≠ 0 ∧ 𝑁 ≠ 0)) → 𝑁 ∈ ℂ)
20		simprl 529	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑀 ≠ 0 ∧ 𝑁 ≠ 0)) → 𝑀 ≠ 0)
21		0z 9293	. . . . . . . . . . 11 ⊢ 0 ∈ ℤ
22		zapne 9356	. . . . . . . . . . 11 ⊢ ((𝑀 ∈ ℤ ∧ 0 ∈ ℤ) → (𝑀 # 0 ↔ 𝑀 ≠ 0))
23	15, 21, 22	sylancl 413	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑀 ≠ 0 ∧ 𝑁 ≠ 0)) → (𝑀 # 0 ↔ 𝑀 ≠ 0))
24	20, 23	mpbird 167	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑀 ≠ 0 ∧ 𝑁 ≠ 0)) → 𝑀 # 0)
25		simprr 531	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑀 ≠ 0 ∧ 𝑁 ≠ 0)) → 𝑁 ≠ 0)
26		zapne 9356	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ ℤ ∧ 0 ∈ ℤ) → (𝑁 # 0 ↔ 𝑁 ≠ 0))
27	16, 21, 26	sylancl 413	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑀 ≠ 0 ∧ 𝑁 ≠ 0)) → (𝑁 # 0 ↔ 𝑁 ≠ 0))
28	25, 27	mpbird 167	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑀 ≠ 0 ∧ 𝑁 ≠ 0)) → 𝑁 # 0)
29	18, 19, 24, 28	mulap0d 8644	. . . . . . . 8 ⊢ (((𝐴 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑀 ≠ 0 ∧ 𝑁 ≠ 0)) → (𝑀 · 𝑁) # 0)
30		zapne 9356	. . . . . . . . 9 ⊢ (((𝑀 · 𝑁) ∈ ℤ ∧ 0 ∈ ℤ) → ((𝑀 · 𝑁) # 0 ↔ (𝑀 · 𝑁) ≠ 0))
31	17, 21, 30	sylancl 413	. . . . . . . 8 ⊢ (((𝐴 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑀 ≠ 0 ∧ 𝑁 ≠ 0)) → ((𝑀 · 𝑁) # 0 ↔ (𝑀 · 𝑁) ≠ 0))
32	29, 31	mpbid 147	. . . . . . 7 ⊢ (((𝐴 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑀 ≠ 0 ∧ 𝑁 ≠ 0)) → (𝑀 · 𝑁) ≠ 0)
33		nnabscl 11140	. . . . . . 7 ⊢ (((𝑀 · 𝑁) ∈ ℤ ∧ (𝑀 · 𝑁) ≠ 0) → (abs‘(𝑀 · 𝑁)) ∈ ℕ)
34	17, 32, 33	syl2anc 411	. . . . . 6 ⊢ (((𝐴 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑀 ≠ 0 ∧ 𝑁 ≠ 0)) → (abs‘(𝑀 · 𝑁)) ∈ ℕ)
35		nnuz 9592	. . . . . 6 ⊢ ℕ = (ℤ_≥‘1)
36	34, 35	eleqtrdi 2282	. . . . 5 ⊢ (((𝐴 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑀 ≠ 0 ∧ 𝑁 ≠ 0)) → (abs‘(𝑀 · 𝑁)) ∈ (ℤ_≥‘1))
37		simpl1 1002	. . . . . . . 8 ⊢ (((𝐴 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑀 ≠ 0 ∧ 𝑁 ≠ 0)) → 𝐴 ∈ ℤ)
38		eqid 2189	. . . . . . . . 9 ⊢ (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /_L 𝑛)↑(𝑛 pCnt 𝑀)), 1)) = (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /_L 𝑛)↑(𝑛 pCnt 𝑀)), 1))
39	38	lgsfcl3 14875	. . . . . . . 8 ⊢ ((𝐴 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑀 ≠ 0) → (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /_L 𝑛)↑(𝑛 pCnt 𝑀)), 1)):ℕ⟶ℤ)
40	37, 15, 20, 39	syl3anc 1249	. . . . . . 7 ⊢ (((𝐴 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑀 ≠ 0 ∧ 𝑁 ≠ 0)) → (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /_L 𝑛)↑(𝑛 pCnt 𝑀)), 1)):ℕ⟶ℤ)
41		elnnuz 9593	. . . . . . . 8 ⊢ (𝑘 ∈ ℕ ↔ 𝑘 ∈ (ℤ_≥‘1))
42	41	biimpri 133	. . . . . . 7 ⊢ (𝑘 ∈ (ℤ_≥‘1) → 𝑘 ∈ ℕ)
43		ffvelcdm 5669	. . . . . . 7 ⊢ (((𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /_L 𝑛)↑(𝑛 pCnt 𝑀)), 1)):ℕ⟶ℤ ∧ 𝑘 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /_L 𝑛)↑(𝑛 pCnt 𝑀)), 1))‘𝑘) ∈ ℤ)
44	40, 42, 43	syl2an 289	. . . . . 6 ⊢ ((((𝐴 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑀 ≠ 0 ∧ 𝑁 ≠ 0)) ∧ 𝑘 ∈ (ℤ_≥‘1)) → ((𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /_L 𝑛)↑(𝑛 pCnt 𝑀)), 1))‘𝑘) ∈ ℤ)
45	44	zcnd 9405	. . . . 5 ⊢ ((((𝐴 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑀 ≠ 0 ∧ 𝑁 ≠ 0)) ∧ 𝑘 ∈ (ℤ_≥‘1)) → ((𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /_L 𝑛)↑(𝑛 pCnt 𝑀)), 1))‘𝑘) ∈ ℂ)
46		eqid 2189	. . . . . . . . 9 ⊢ (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /_L 𝑛)↑(𝑛 pCnt 𝑁)), 1)) = (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /_L 𝑛)↑(𝑛 pCnt 𝑁)), 1))
47	46	lgsfcl3 14875	. . . . . . . 8 ⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) → (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /_L 𝑛)↑(𝑛 pCnt 𝑁)), 1)):ℕ⟶ℤ)
48	37, 16, 25, 47	syl3anc 1249	. . . . . . 7 ⊢ (((𝐴 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑀 ≠ 0 ∧ 𝑁 ≠ 0)) → (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /_L 𝑛)↑(𝑛 pCnt 𝑁)), 1)):ℕ⟶ℤ)
49		ffvelcdm 5669	. . . . . . 7 ⊢ (((𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /_L 𝑛)↑(𝑛 pCnt 𝑁)), 1)):ℕ⟶ℤ ∧ 𝑘 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /_L 𝑛)↑(𝑛 pCnt 𝑁)), 1))‘𝑘) ∈ ℤ)
50	48, 42, 49	syl2an 289	. . . . . 6 ⊢ ((((𝐴 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑀 ≠ 0 ∧ 𝑁 ≠ 0)) ∧ 𝑘 ∈ (ℤ_≥‘1)) → ((𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /_L 𝑛)↑(𝑛 pCnt 𝑁)), 1))‘𝑘) ∈ ℤ)
51	50	zcnd 9405	. . . . 5 ⊢ ((((𝐴 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑀 ≠ 0 ∧ 𝑁 ≠ 0)) ∧ 𝑘 ∈ (ℤ_≥‘1)) → ((𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /_L 𝑛)↑(𝑛 pCnt 𝑁)), 1))‘𝑘) ∈ ℂ)
52		simpr 110	. . . . . . . . . . 11 ⊢ (((((𝐴 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑀 ≠ 0 ∧ 𝑁 ≠ 0)) ∧ 𝑘 ∈ (ℤ_≥‘1)) ∧ 𝑘 ∈ ℙ) → 𝑘 ∈ ℙ)
53	15	ad2antrr 488	. . . . . . . . . . 11 ⊢ (((((𝐴 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑀 ≠ 0 ∧ 𝑁 ≠ 0)) ∧ 𝑘 ∈ (ℤ_≥‘1)) ∧ 𝑘 ∈ ℙ) → 𝑀 ∈ ℤ)
54	20	ad2antrr 488	. . . . . . . . . . 11 ⊢ (((((𝐴 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑀 ≠ 0 ∧ 𝑁 ≠ 0)) ∧ 𝑘 ∈ (ℤ_≥‘1)) ∧ 𝑘 ∈ ℙ) → 𝑀 ≠ 0)
55	16	ad2antrr 488	. . . . . . . . . . 11 ⊢ (((((𝐴 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑀 ≠ 0 ∧ 𝑁 ≠ 0)) ∧ 𝑘 ∈ (ℤ_≥‘1)) ∧ 𝑘 ∈ ℙ) → 𝑁 ∈ ℤ)
56	25	ad2antrr 488	. . . . . . . . . . 11 ⊢ (((((𝐴 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑀 ≠ 0 ∧ 𝑁 ≠ 0)) ∧ 𝑘 ∈ (ℤ_≥‘1)) ∧ 𝑘 ∈ ℙ) → 𝑁 ≠ 0)
57		pcmul 12332	. . . . . . . . . . 11 ⊢ ((𝑘 ∈ ℙ ∧ (𝑀 ∈ ℤ ∧ 𝑀 ≠ 0) ∧ (𝑁 ∈ ℤ ∧ 𝑁 ≠ 0)) → (𝑘 pCnt (𝑀 · 𝑁)) = ((𝑘 pCnt 𝑀) + (𝑘 pCnt 𝑁)))
58	52, 53, 54, 55, 56, 57	syl122anc 1258	. . . . . . . . . 10 ⊢ (((((𝐴 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑀 ≠ 0 ∧ 𝑁 ≠ 0)) ∧ 𝑘 ∈ (ℤ_≥‘1)) ∧ 𝑘 ∈ ℙ) → (𝑘 pCnt (𝑀 · 𝑁)) = ((𝑘 pCnt 𝑀) + (𝑘 pCnt 𝑁)))
59	58	oveq2d 5911	. . . . . . . . 9 ⊢ (((((𝐴 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑀 ≠ 0 ∧ 𝑁 ≠ 0)) ∧ 𝑘 ∈ (ℤ_≥‘1)) ∧ 𝑘 ∈ ℙ) → ((𝐴 /_L 𝑘)↑(𝑘 pCnt (𝑀 · 𝑁))) = ((𝐴 /_L 𝑘)↑((𝑘 pCnt 𝑀) + (𝑘 pCnt 𝑁))))
60	37	ad2antrr 488	. . . . . . . . . . . 12 ⊢ (((((𝐴 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑀 ≠ 0 ∧ 𝑁 ≠ 0)) ∧ 𝑘 ∈ (ℤ_≥‘1)) ∧ 𝑘 ∈ ℙ) → 𝐴 ∈ ℤ)
61		prmz 12142	. . . . . . . . . . . . 13 ⊢ (𝑘 ∈ ℙ → 𝑘 ∈ ℤ)
62	61	adantl 277	. . . . . . . . . . . 12 ⊢ (((((𝐴 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑀 ≠ 0 ∧ 𝑁 ≠ 0)) ∧ 𝑘 ∈ (ℤ_≥‘1)) ∧ 𝑘 ∈ ℙ) → 𝑘 ∈ ℤ)
63		lgscl 14868	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ ℤ ∧ 𝑘 ∈ ℤ) → (𝐴 /_L 𝑘) ∈ ℤ)
64	60, 62, 63	syl2anc 411	. . . . . . . . . . 11 ⊢ (((((𝐴 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑀 ≠ 0 ∧ 𝑁 ≠ 0)) ∧ 𝑘 ∈ (ℤ_≥‘1)) ∧ 𝑘 ∈ ℙ) → (𝐴 /_L 𝑘) ∈ ℤ)
65	64	zcnd 9405	. . . . . . . . . 10 ⊢ (((((𝐴 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑀 ≠ 0 ∧ 𝑁 ≠ 0)) ∧ 𝑘 ∈ (ℤ_≥‘1)) ∧ 𝑘 ∈ ℙ) → (𝐴 /_L 𝑘) ∈ ℂ)
66		pczcl 12329	. . . . . . . . . . 11 ⊢ ((𝑘 ∈ ℙ ∧ (𝑁 ∈ ℤ ∧ 𝑁 ≠ 0)) → (𝑘 pCnt 𝑁) ∈ ℕ₀)
67	52, 55, 56, 66	syl12anc 1247	. . . . . . . . . 10 ⊢ (((((𝐴 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑀 ≠ 0 ∧ 𝑁 ≠ 0)) ∧ 𝑘 ∈ (ℤ_≥‘1)) ∧ 𝑘 ∈ ℙ) → (𝑘 pCnt 𝑁) ∈ ℕ₀)
68		pczcl 12329	. . . . . . . . . . 11 ⊢ ((𝑘 ∈ ℙ ∧ (𝑀 ∈ ℤ ∧ 𝑀 ≠ 0)) → (𝑘 pCnt 𝑀) ∈ ℕ₀)
69	52, 53, 54, 68	syl12anc 1247	. . . . . . . . . 10 ⊢ (((((𝐴 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑀 ≠ 0 ∧ 𝑁 ≠ 0)) ∧ 𝑘 ∈ (ℤ_≥‘1)) ∧ 𝑘 ∈ ℙ) → (𝑘 pCnt 𝑀) ∈ ℕ₀)
70	65, 67, 69	expaddd 10686	. . . . . . . . 9 ⊢ (((((𝐴 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑀 ≠ 0 ∧ 𝑁 ≠ 0)) ∧ 𝑘 ∈ (ℤ_≥‘1)) ∧ 𝑘 ∈ ℙ) → ((𝐴 /_L 𝑘)↑((𝑘 pCnt 𝑀) + (𝑘 pCnt 𝑁))) = (((𝐴 /_L 𝑘)↑(𝑘 pCnt 𝑀)) · ((𝐴 /_L 𝑘)↑(𝑘 pCnt 𝑁))))
71	59, 70	eqtrd 2222	. . . . . . . 8 ⊢ (((((𝐴 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑀 ≠ 0 ∧ 𝑁 ≠ 0)) ∧ 𝑘 ∈ (ℤ_≥‘1)) ∧ 𝑘 ∈ ℙ) → ((𝐴 /_L 𝑘)↑(𝑘 pCnt (𝑀 · 𝑁))) = (((𝐴 /_L 𝑘)↑(𝑘 pCnt 𝑀)) · ((𝐴 /_L 𝑘)↑(𝑘 pCnt 𝑁))))
72		iftrue 3554	. . . . . . . . 9 ⊢ (𝑘 ∈ ℙ → if(𝑘 ∈ ℙ, ((𝐴 /_L 𝑘)↑(𝑘 pCnt (𝑀 · 𝑁))), 1) = ((𝐴 /_L 𝑘)↑(𝑘 pCnt (𝑀 · 𝑁))))
73	72	adantl 277	. . . . . . . 8 ⊢ (((((𝐴 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑀 ≠ 0 ∧ 𝑁 ≠ 0)) ∧ 𝑘 ∈ (ℤ_≥‘1)) ∧ 𝑘 ∈ ℙ) → if(𝑘 ∈ ℙ, ((𝐴 /_L 𝑘)↑(𝑘 pCnt (𝑀 · 𝑁))), 1) = ((𝐴 /_L 𝑘)↑(𝑘 pCnt (𝑀 · 𝑁))))
74		iftrue 3554	. . . . . . . . . 10 ⊢ (𝑘 ∈ ℙ → if(𝑘 ∈ ℙ, ((𝐴 /_L 𝑘)↑(𝑘 pCnt 𝑀)), 1) = ((𝐴 /_L 𝑘)↑(𝑘 pCnt 𝑀)))
75		iftrue 3554	. . . . . . . . . 10 ⊢ (𝑘 ∈ ℙ → if(𝑘 ∈ ℙ, ((𝐴 /_L 𝑘)↑(𝑘 pCnt 𝑁)), 1) = ((𝐴 /_L 𝑘)↑(𝑘 pCnt 𝑁)))
76	74, 75	oveq12d 5913	. . . . . . . . 9 ⊢ (𝑘 ∈ ℙ → (if(𝑘 ∈ ℙ, ((𝐴 /_L 𝑘)↑(𝑘 pCnt 𝑀)), 1) · if(𝑘 ∈ ℙ, ((𝐴 /_L 𝑘)↑(𝑘 pCnt 𝑁)), 1)) = (((𝐴 /_L 𝑘)↑(𝑘 pCnt 𝑀)) · ((𝐴 /_L 𝑘)↑(𝑘 pCnt 𝑁))))
77	76	adantl 277	. . . . . . . 8 ⊢ (((((𝐴 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑀 ≠ 0 ∧ 𝑁 ≠ 0)) ∧ 𝑘 ∈ (ℤ_≥‘1)) ∧ 𝑘 ∈ ℙ) → (if(𝑘 ∈ ℙ, ((𝐴 /_L 𝑘)↑(𝑘 pCnt 𝑀)), 1) · if(𝑘 ∈ ℙ, ((𝐴 /_L 𝑘)↑(𝑘 pCnt 𝑁)), 1)) = (((𝐴 /_L 𝑘)↑(𝑘 pCnt 𝑀)) · ((𝐴 /_L 𝑘)↑(𝑘 pCnt 𝑁))))
78	71, 73, 77	3eqtr4rd 2233	. . . . . . 7 ⊢ (((((𝐴 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑀 ≠ 0 ∧ 𝑁 ≠ 0)) ∧ 𝑘 ∈ (ℤ_≥‘1)) ∧ 𝑘 ∈ ℙ) → (if(𝑘 ∈ ℙ, ((𝐴 /_L 𝑘)↑(𝑘 pCnt 𝑀)), 1) · if(𝑘 ∈ ℙ, ((𝐴 /_L 𝑘)↑(𝑘 pCnt 𝑁)), 1)) = if(𝑘 ∈ ℙ, ((𝐴 /_L 𝑘)↑(𝑘 pCnt (𝑀 · 𝑁))), 1))
79		1t1e1 9100	. . . . . . . . 9 ⊢ (1 · 1) = 1
80		iffalse 3557	. . . . . . . . . 10 ⊢ (¬ 𝑘 ∈ ℙ → if(𝑘 ∈ ℙ, ((𝐴 /_L 𝑘)↑(𝑘 pCnt 𝑀)), 1) = 1)
81		iffalse 3557	. . . . . . . . . 10 ⊢ (¬ 𝑘 ∈ ℙ → if(𝑘 ∈ ℙ, ((𝐴 /_L 𝑘)↑(𝑘 pCnt 𝑁)), 1) = 1)
82	80, 81	oveq12d 5913	. . . . . . . . 9 ⊢ (¬ 𝑘 ∈ ℙ → (if(𝑘 ∈ ℙ, ((𝐴 /_L 𝑘)↑(𝑘 pCnt 𝑀)), 1) · if(𝑘 ∈ ℙ, ((𝐴 /_L 𝑘)↑(𝑘 pCnt 𝑁)), 1)) = (1 · 1))
83		iffalse 3557	. . . . . . . . 9 ⊢ (¬ 𝑘 ∈ ℙ → if(𝑘 ∈ ℙ, ((𝐴 /_L 𝑘)↑(𝑘 pCnt (𝑀 · 𝑁))), 1) = 1)
84	79, 82, 83	3eqtr4a 2248	. . . . . . . 8 ⊢ (¬ 𝑘 ∈ ℙ → (if(𝑘 ∈ ℙ, ((𝐴 /_L 𝑘)↑(𝑘 pCnt 𝑀)), 1) · if(𝑘 ∈ ℙ, ((𝐴 /_L 𝑘)↑(𝑘 pCnt 𝑁)), 1)) = if(𝑘 ∈ ℙ, ((𝐴 /_L 𝑘)↑(𝑘 pCnt (𝑀 · 𝑁))), 1))
85	84	adantl 277	. . . . . . 7 ⊢ (((((𝐴 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑀 ≠ 0 ∧ 𝑁 ≠ 0)) ∧ 𝑘 ∈ (ℤ_≥‘1)) ∧ ¬ 𝑘 ∈ ℙ) → (if(𝑘 ∈ ℙ, ((𝐴 /_L 𝑘)↑(𝑘 pCnt 𝑀)), 1) · if(𝑘 ∈ ℙ, ((𝐴 /_L 𝑘)↑(𝑘 pCnt 𝑁)), 1)) = if(𝑘 ∈ ℙ, ((𝐴 /_L 𝑘)↑(𝑘 pCnt (𝑀 · 𝑁))), 1))
86		prmdc 12161	. . . . . . . . . 10 ⊢ (𝑘 ∈ ℕ → DECID 𝑘 ∈ ℙ)
87		exmiddc 837	. . . . . . . . . 10 ⊢ (DECID 𝑘 ∈ ℙ → (𝑘 ∈ ℙ ∨ ¬ 𝑘 ∈ ℙ))
88	86, 87	syl 14	. . . . . . . . 9 ⊢ (𝑘 ∈ ℕ → (𝑘 ∈ ℙ ∨ ¬ 𝑘 ∈ ℙ))
89	42, 88	syl 14	. . . . . . . 8 ⊢ (𝑘 ∈ (ℤ_≥‘1) → (𝑘 ∈ ℙ ∨ ¬ 𝑘 ∈ ℙ))
90	89	adantl 277	. . . . . . 7 ⊢ ((((𝐴 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑀 ≠ 0 ∧ 𝑁 ≠ 0)) ∧ 𝑘 ∈ (ℤ_≥‘1)) → (𝑘 ∈ ℙ ∨ ¬ 𝑘 ∈ ℙ))
91	78, 85, 90	mpjaodan 799	. . . . . 6 ⊢ ((((𝐴 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑀 ≠ 0 ∧ 𝑁 ≠ 0)) ∧ 𝑘 ∈ (ℤ_≥‘1)) → (if(𝑘 ∈ ℙ, ((𝐴 /_L 𝑘)↑(𝑘 pCnt 𝑀)), 1) · if(𝑘 ∈ ℙ, ((𝐴 /_L 𝑘)↑(𝑘 pCnt 𝑁)), 1)) = if(𝑘 ∈ ℙ, ((𝐴 /_L 𝑘)↑(𝑘 pCnt (𝑀 · 𝑁))), 1))
92		eleq1w 2250	. . . . . . . . 9 ⊢ (𝑛 = 𝑘 → (𝑛 ∈ ℙ ↔ 𝑘 ∈ ℙ))
93		oveq2 5903	. . . . . . . . . 10 ⊢ (𝑛 = 𝑘 → (𝐴 /_L 𝑛) = (𝐴 /_L 𝑘))
94		oveq1 5902	. . . . . . . . . 10 ⊢ (𝑛 = 𝑘 → (𝑛 pCnt 𝑀) = (𝑘 pCnt 𝑀))
95	93, 94	oveq12d 5913	. . . . . . . . 9 ⊢ (𝑛 = 𝑘 → ((𝐴 /_L 𝑛)↑(𝑛 pCnt 𝑀)) = ((𝐴 /_L 𝑘)↑(𝑘 pCnt 𝑀)))
96	92, 95	ifbieq1d 3571	. . . . . . . 8 ⊢ (𝑛 = 𝑘 → if(𝑛 ∈ ℙ, ((𝐴 /_L 𝑛)↑(𝑛 pCnt 𝑀)), 1) = if(𝑘 ∈ ℙ, ((𝐴 /_L 𝑘)↑(𝑘 pCnt 𝑀)), 1))
97	42	adantl 277	. . . . . . . 8 ⊢ ((((𝐴 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑀 ≠ 0 ∧ 𝑁 ≠ 0)) ∧ 𝑘 ∈ (ℤ_≥‘1)) → 𝑘 ∈ ℕ)
98		zexpcl 10565	. . . . . . . . . 10 ⊢ (((𝐴 /_L 𝑘) ∈ ℤ ∧ (𝑘 pCnt 𝑀) ∈ ℕ₀) → ((𝐴 /_L 𝑘)↑(𝑘 pCnt 𝑀)) ∈ ℤ)
99	64, 69, 98	syl2anc 411	. . . . . . . . 9 ⊢ (((((𝐴 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑀 ≠ 0 ∧ 𝑁 ≠ 0)) ∧ 𝑘 ∈ (ℤ_≥‘1)) ∧ 𝑘 ∈ ℙ) → ((𝐴 /_L 𝑘)↑(𝑘 pCnt 𝑀)) ∈ ℤ)
100		1zzd 9309	. . . . . . . . 9 ⊢ (((((𝐴 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑀 ≠ 0 ∧ 𝑁 ≠ 0)) ∧ 𝑘 ∈ (ℤ_≥‘1)) ∧ ¬ 𝑘 ∈ ℙ) → 1 ∈ ℤ)
101	97, 86	syl 14	. . . . . . . . 9 ⊢ ((((𝐴 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑀 ≠ 0 ∧ 𝑁 ≠ 0)) ∧ 𝑘 ∈ (ℤ_≥‘1)) → DECID 𝑘 ∈ ℙ)
102	99, 100, 101	ifcldadc 3578	. . . . . . . 8 ⊢ ((((𝐴 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑀 ≠ 0 ∧ 𝑁 ≠ 0)) ∧ 𝑘 ∈ (ℤ_≥‘1)) → if(𝑘 ∈ ℙ, ((𝐴 /_L 𝑘)↑(𝑘 pCnt 𝑀)), 1) ∈ ℤ)
103	38, 96, 97, 102	fvmptd3 5629	. . . . . . 7 ⊢ ((((𝐴 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑀 ≠ 0 ∧ 𝑁 ≠ 0)) ∧ 𝑘 ∈ (ℤ_≥‘1)) → ((𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /_L 𝑛)↑(𝑛 pCnt 𝑀)), 1))‘𝑘) = if(𝑘 ∈ ℙ, ((𝐴 /_L 𝑘)↑(𝑘 pCnt 𝑀)), 1))
104		oveq1 5902	. . . . . . . . . 10 ⊢ (𝑛 = 𝑘 → (𝑛 pCnt 𝑁) = (𝑘 pCnt 𝑁))
105	93, 104	oveq12d 5913	. . . . . . . . 9 ⊢ (𝑛 = 𝑘 → ((𝐴 /_L 𝑛)↑(𝑛 pCnt 𝑁)) = ((𝐴 /_L 𝑘)↑(𝑘 pCnt 𝑁)))
106	92, 105	ifbieq1d 3571	. . . . . . . 8 ⊢ (𝑛 = 𝑘 → if(𝑛 ∈ ℙ, ((𝐴 /_L 𝑛)↑(𝑛 pCnt 𝑁)), 1) = if(𝑘 ∈ ℙ, ((𝐴 /_L 𝑘)↑(𝑘 pCnt 𝑁)), 1))
107		zexpcl 10565	. . . . . . . . . 10 ⊢ (((𝐴 /_L 𝑘) ∈ ℤ ∧ (𝑘 pCnt 𝑁) ∈ ℕ₀) → ((𝐴 /_L 𝑘)↑(𝑘 pCnt 𝑁)) ∈ ℤ)
108	64, 67, 107	syl2anc 411	. . . . . . . . 9 ⊢ (((((𝐴 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑀 ≠ 0 ∧ 𝑁 ≠ 0)) ∧ 𝑘 ∈ (ℤ_≥‘1)) ∧ 𝑘 ∈ ℙ) → ((𝐴 /_L 𝑘)↑(𝑘 pCnt 𝑁)) ∈ ℤ)
109	108, 100, 101	ifcldadc 3578	. . . . . . . 8 ⊢ ((((𝐴 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑀 ≠ 0 ∧ 𝑁 ≠ 0)) ∧ 𝑘 ∈ (ℤ_≥‘1)) → if(𝑘 ∈ ℙ, ((𝐴 /_L 𝑘)↑(𝑘 pCnt 𝑁)), 1) ∈ ℤ)
110	46, 106, 97, 109	fvmptd3 5629	. . . . . . 7 ⊢ ((((𝐴 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑀 ≠ 0 ∧ 𝑁 ≠ 0)) ∧ 𝑘 ∈ (ℤ_≥‘1)) → ((𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /_L 𝑛)↑(𝑛 pCnt 𝑁)), 1))‘𝑘) = if(𝑘 ∈ ℙ, ((𝐴 /_L 𝑘)↑(𝑘 pCnt 𝑁)), 1))
111	103, 110	oveq12d 5913	. . . . . 6 ⊢ ((((𝐴 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑀 ≠ 0 ∧ 𝑁 ≠ 0)) ∧ 𝑘 ∈ (ℤ_≥‘1)) → (((𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /_L 𝑛)↑(𝑛 pCnt 𝑀)), 1))‘𝑘) · ((𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /_L 𝑛)↑(𝑛 pCnt 𝑁)), 1))‘𝑘)) = (if(𝑘 ∈ ℙ, ((𝐴 /_L 𝑘)↑(𝑘 pCnt 𝑀)), 1) · if(𝑘 ∈ ℙ, ((𝐴 /_L 𝑘)↑(𝑘 pCnt 𝑁)), 1)))
112		eqid 2189	. . . . . . 7 ⊢ (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /_L 𝑛)↑(𝑛 pCnt (𝑀 · 𝑁))), 1)) = (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /_L 𝑛)↑(𝑛 pCnt (𝑀 · 𝑁))), 1))
113		oveq1 5902	. . . . . . . . 9 ⊢ (𝑛 = 𝑘 → (𝑛 pCnt (𝑀 · 𝑁)) = (𝑘 pCnt (𝑀 · 𝑁)))
114	93, 113	oveq12d 5913	. . . . . . . 8 ⊢ (𝑛 = 𝑘 → ((𝐴 /_L 𝑛)↑(𝑛 pCnt (𝑀 · 𝑁))) = ((𝐴 /_L 𝑘)↑(𝑘 pCnt (𝑀 · 𝑁))))
115	92, 114	ifbieq1d 3571	. . . . . . 7 ⊢ (𝑛 = 𝑘 → if(𝑛 ∈ ℙ, ((𝐴 /_L 𝑛)↑(𝑛 pCnt (𝑀 · 𝑁))), 1) = if(𝑘 ∈ ℙ, ((𝐴 /_L 𝑘)↑(𝑘 pCnt (𝑀 · 𝑁))), 1))
116	17	ad2antrr 488	. . . . . . . . . 10 ⊢ (((((𝐴 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑀 ≠ 0 ∧ 𝑁 ≠ 0)) ∧ 𝑘 ∈ (ℤ_≥‘1)) ∧ 𝑘 ∈ ℙ) → (𝑀 · 𝑁) ∈ ℤ)
117	32	ad2antrr 488	. . . . . . . . . 10 ⊢ (((((𝐴 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑀 ≠ 0 ∧ 𝑁 ≠ 0)) ∧ 𝑘 ∈ (ℤ_≥‘1)) ∧ 𝑘 ∈ ℙ) → (𝑀 · 𝑁) ≠ 0)
118		pczcl 12329	. . . . . . . . . 10 ⊢ ((𝑘 ∈ ℙ ∧ ((𝑀 · 𝑁) ∈ ℤ ∧ (𝑀 · 𝑁) ≠ 0)) → (𝑘 pCnt (𝑀 · 𝑁)) ∈ ℕ₀)
119	52, 116, 117, 118	syl12anc 1247	. . . . . . . . 9 ⊢ (((((𝐴 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑀 ≠ 0 ∧ 𝑁 ≠ 0)) ∧ 𝑘 ∈ (ℤ_≥‘1)) ∧ 𝑘 ∈ ℙ) → (𝑘 pCnt (𝑀 · 𝑁)) ∈ ℕ₀)
120		zexpcl 10565	. . . . . . . . 9 ⊢ (((𝐴 /_L 𝑘) ∈ ℤ ∧ (𝑘 pCnt (𝑀 · 𝑁)) ∈ ℕ₀) → ((𝐴 /_L 𝑘)↑(𝑘 pCnt (𝑀 · 𝑁))) ∈ ℤ)
121	64, 119, 120	syl2anc 411	. . . . . . . 8 ⊢ (((((𝐴 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑀 ≠ 0 ∧ 𝑁 ≠ 0)) ∧ 𝑘 ∈ (ℤ_≥‘1)) ∧ 𝑘 ∈ ℙ) → ((𝐴 /_L 𝑘)↑(𝑘 pCnt (𝑀 · 𝑁))) ∈ ℤ)
122	121, 100, 101	ifcldadc 3578	. . . . . . 7 ⊢ ((((𝐴 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑀 ≠ 0 ∧ 𝑁 ≠ 0)) ∧ 𝑘 ∈ (ℤ_≥‘1)) → if(𝑘 ∈ ℙ, ((𝐴 /_L 𝑘)↑(𝑘 pCnt (𝑀 · 𝑁))), 1) ∈ ℤ)
123	112, 115, 97, 122	fvmptd3 5629	. . . . . 6 ⊢ ((((𝐴 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑀 ≠ 0 ∧ 𝑁 ≠ 0)) ∧ 𝑘 ∈ (ℤ_≥‘1)) → ((𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /_L 𝑛)↑(𝑛 pCnt (𝑀 · 𝑁))), 1))‘𝑘) = if(𝑘 ∈ ℙ, ((𝐴 /_L 𝑘)↑(𝑘 pCnt (𝑀 · 𝑁))), 1))
124	91, 111, 123	3eqtr4rd 2233	. . . . 5 ⊢ ((((𝐴 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑀 ≠ 0 ∧ 𝑁 ≠ 0)) ∧ 𝑘 ∈ (ℤ_≥‘1)) → ((𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /_L 𝑛)↑(𝑛 pCnt (𝑀 · 𝑁))), 1))‘𝑘) = (((𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /_L 𝑛)↑(𝑛 pCnt 𝑀)), 1))‘𝑘) · ((𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /_L 𝑛)↑(𝑛 pCnt 𝑁)), 1))‘𝑘)))
125	36, 45, 51, 124	prod3fmul 11580	. . . 4 ⊢ (((𝐴 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑀 ≠ 0 ∧ 𝑁 ≠ 0)) → (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /_L 𝑛)↑(𝑛 pCnt (𝑀 · 𝑁))), 1)))‘(abs‘(𝑀 · 𝑁))) = ((seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /_L 𝑛)↑(𝑛 pCnt 𝑀)), 1)))‘(abs‘(𝑀 · 𝑁))) · (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /_L 𝑛)↑(𝑛 pCnt 𝑁)), 1)))‘(abs‘(𝑀 · 𝑁)))))
126	37, 15, 16, 20, 25, 38	lgsdilem2 14890	. . . . 5 ⊢ (((𝐴 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑀 ≠ 0 ∧ 𝑁 ≠ 0)) → (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /_L 𝑛)↑(𝑛 pCnt 𝑀)), 1)))‘(abs‘𝑀)) = (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /_L 𝑛)↑(𝑛 pCnt 𝑀)), 1)))‘(abs‘(𝑀 · 𝑁))))
127	37, 16, 15, 25, 20, 46	lgsdilem2 14890	. . . . . 6 ⊢ (((𝐴 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑀 ≠ 0 ∧ 𝑁 ≠ 0)) → (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /_L 𝑛)↑(𝑛 pCnt 𝑁)), 1)))‘(abs‘𝑁)) = (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /_L 𝑛)↑(𝑛 pCnt 𝑁)), 1)))‘(abs‘(𝑁 · 𝑀))))
128	18, 19	mulcomd 8008	. . . . . . . 8 ⊢ (((𝐴 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑀 ≠ 0 ∧ 𝑁 ≠ 0)) → (𝑀 · 𝑁) = (𝑁 · 𝑀))
129	128	fveq2d 5538	. . . . . . 7 ⊢ (((𝐴 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑀 ≠ 0 ∧ 𝑁 ≠ 0)) → (abs‘(𝑀 · 𝑁)) = (abs‘(𝑁 · 𝑀)))
130	129	fveq2d 5538	. . . . . 6 ⊢ (((𝐴 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑀 ≠ 0 ∧ 𝑁 ≠ 0)) → (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /_L 𝑛)↑(𝑛 pCnt 𝑁)), 1)))‘(abs‘(𝑀 · 𝑁))) = (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /_L 𝑛)↑(𝑛 pCnt 𝑁)), 1)))‘(abs‘(𝑁 · 𝑀))))
131	127, 130	eqtr4d 2225	. . . . 5 ⊢ (((𝐴 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑀 ≠ 0 ∧ 𝑁 ≠ 0)) → (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /_L 𝑛)↑(𝑛 pCnt 𝑁)), 1)))‘(abs‘𝑁)) = (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /_L 𝑛)↑(𝑛 pCnt 𝑁)), 1)))‘(abs‘(𝑀 · 𝑁))))
132	126, 131	oveq12d 5913	. . . 4 ⊢ (((𝐴 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑀 ≠ 0 ∧ 𝑁 ≠ 0)) → ((seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /_L 𝑛)↑(𝑛 pCnt 𝑀)), 1)))‘(abs‘𝑀)) · (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /_L 𝑛)↑(𝑛 pCnt 𝑁)), 1)))‘(abs‘𝑁))) = ((seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /_L 𝑛)↑(𝑛 pCnt 𝑀)), 1)))‘(abs‘(𝑀 · 𝑁))) · (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /_L 𝑛)↑(𝑛 pCnt 𝑁)), 1)))‘(abs‘(𝑀 · 𝑁)))))
133	125, 132	eqtr4d 2225	. . 3 ⊢ (((𝐴 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑀 ≠ 0 ∧ 𝑁 ≠ 0)) → (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /_L 𝑛)↑(𝑛 pCnt (𝑀 · 𝑁))), 1)))‘(abs‘(𝑀 · 𝑁))) = ((seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /_L 𝑛)↑(𝑛 pCnt 𝑀)), 1)))‘(abs‘𝑀)) · (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /_L 𝑛)↑(𝑛 pCnt 𝑁)), 1)))‘(abs‘𝑁))))
134	14, 133	oveq12d 5913	. 2 ⊢ (((𝐴 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑀 ≠ 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‘𝑁)))))
135	112	lgsval4 14874	. . 3 ⊢ ((𝐴 ∈ ℤ ∧ (𝑀 · 𝑁) ∈ ℤ ∧ (𝑀 · 𝑁) ≠ 0) → (𝐴 /_L (𝑀 · 𝑁)) = (if(((𝑀 · 𝑁) < 0 ∧ 𝐴 < 0), -1, 1) · (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /_L 𝑛)↑(𝑛 pCnt (𝑀 · 𝑁))), 1)))‘(abs‘(𝑀 · 𝑁)))))
136	37, 17, 32, 135	syl3anc 1249	. 2 ⊢ (((𝐴 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑀 ≠ 0 ∧ 𝑁 ≠ 0)) → (𝐴 /_L (𝑀 · 𝑁)) = (if(((𝑀 · 𝑁) < 0 ∧ 𝐴 < 0), -1, 1) · (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /_L 𝑛)↑(𝑛 pCnt (𝑀 · 𝑁))), 1)))‘(abs‘(𝑀 · 𝑁)))))
137	38	lgsval4 14874	. . . . 5 ⊢ ((𝐴 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑀 ≠ 0) → (𝐴 /_L 𝑀) = (if((𝑀 < 0 ∧ 𝐴 < 0), -1, 1) · (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /_L 𝑛)↑(𝑛 pCnt 𝑀)), 1)))‘(abs‘𝑀))))
138	37, 15, 20, 137	syl3anc 1249	. . . 4 ⊢ (((𝐴 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑀 ≠ 0 ∧ 𝑁 ≠ 0)) → (𝐴 /_L 𝑀) = (if((𝑀 < 0 ∧ 𝐴 < 0), -1, 1) · (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /_L 𝑛)↑(𝑛 pCnt 𝑀)), 1)))‘(abs‘𝑀))))
139	46	lgsval4 14874	. . . . 5 ⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) → (𝐴 /_L 𝑁) = (if((𝑁 < 0 ∧ 𝐴 < 0), -1, 1) · (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /_L 𝑛)↑(𝑛 pCnt 𝑁)), 1)))‘(abs‘𝑁))))
140	37, 16, 25, 139	syl3anc 1249	. . . 4 ⊢ (((𝐴 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑀 ≠ 0 ∧ 𝑁 ≠ 0)) → (𝐴 /_L 𝑁) = (if((𝑁 < 0 ∧ 𝐴 < 0), -1, 1) · (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /_L 𝑛)↑(𝑛 pCnt 𝑁)), 1)))‘(abs‘𝑁))))
141	138, 140	oveq12d 5913	. . 3 ⊢ (((𝐴 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑀 ≠ 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‘𝑁)))))
142		neg1z 9314	. . . . . . 7 ⊢ -1 ∈ ℤ
143	142	a1i 9	. . . . . 6 ⊢ (((𝐴 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑀 ≠ 0 ∧ 𝑁 ≠ 0)) → -1 ∈ ℤ)
144		1zzd 9309	. . . . . 6 ⊢ (((𝐴 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑀 ≠ 0 ∧ 𝑁 ≠ 0)) → 1 ∈ ℤ)
145		zdclt 9359	. . . . . . . 8 ⊢ ((𝑀 ∈ ℤ ∧ 0 ∈ ℤ) → DECID 𝑀 < 0)
146	15, 21, 145	sylancl 413	. . . . . . 7 ⊢ (((𝐴 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑀 ≠ 0 ∧ 𝑁 ≠ 0)) → DECID 𝑀 < 0)
147		zdclt 9359	. . . . . . . 8 ⊢ ((𝐴 ∈ ℤ ∧ 0 ∈ ℤ) → DECID 𝐴 < 0)
148	37, 21, 147	sylancl 413	. . . . . . 7 ⊢ (((𝐴 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑀 ≠ 0 ∧ 𝑁 ≠ 0)) → DECID 𝐴 < 0)
149		dcan2 936	. . . . . . 7 ⊢ (DECID 𝑀 < 0 → (DECID 𝐴 < 0 → DECID (𝑀 < 0 ∧ 𝐴 < 0)))
150	146, 148, 149	sylc 62	. . . . . 6 ⊢ (((𝐴 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑀 ≠ 0 ∧ 𝑁 ≠ 0)) → DECID (𝑀 < 0 ∧ 𝐴 < 0))
151	143, 144, 150	ifcldcd 3585	. . . . 5 ⊢ (((𝐴 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑀 ≠ 0 ∧ 𝑁 ≠ 0)) → if((𝑀 < 0 ∧ 𝐴 < 0), -1, 1) ∈ ℤ)
152	151	zcnd 9405	. . . 4 ⊢ (((𝐴 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑀 ≠ 0 ∧ 𝑁 ≠ 0)) → if((𝑀 < 0 ∧ 𝐴 < 0), -1, 1) ∈ ℂ)
153	40	ffvelcdmda 5671	. . . . . . 7 ⊢ ((((𝐴 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑀 ≠ 0 ∧ 𝑁 ≠ 0)) ∧ 𝑘 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /_L 𝑛)↑(𝑛 pCnt 𝑀)), 1))‘𝑘) ∈ ℤ)
154		zmulcl 9335	. . . . . . . 8 ⊢ ((𝑘 ∈ ℤ ∧ 𝑣 ∈ ℤ) → (𝑘 · 𝑣) ∈ ℤ)
155	154	adantl 277	. . . . . . 7 ⊢ ((((𝐴 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑀 ≠ 0 ∧ 𝑁 ≠ 0)) ∧ (𝑘 ∈ ℤ ∧ 𝑣 ∈ ℤ)) → (𝑘 · 𝑣) ∈ ℤ)
156	35, 144, 153, 155	seqf 10491	. . . . . 6 ⊢ (((𝐴 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑀 ≠ 0 ∧ 𝑁 ≠ 0)) → seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /_L 𝑛)↑(𝑛 pCnt 𝑀)), 1))):ℕ⟶ℤ)
157		nnabscl 11140	. . . . . . 7 ⊢ ((𝑀 ∈ ℤ ∧ 𝑀 ≠ 0) → (abs‘𝑀) ∈ ℕ)
158	15, 20, 157	syl2anc 411	. . . . . 6 ⊢ (((𝐴 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑀 ≠ 0 ∧ 𝑁 ≠ 0)) → (abs‘𝑀) ∈ ℕ)
159	156, 158	ffvelcdmd 5672	. . . . 5 ⊢ (((𝐴 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑀 ≠ 0 ∧ 𝑁 ≠ 0)) → (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /_L 𝑛)↑(𝑛 pCnt 𝑀)), 1)))‘(abs‘𝑀)) ∈ ℤ)
160	159	zcnd 9405	. . . 4 ⊢ (((𝐴 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑀 ≠ 0 ∧ 𝑁 ≠ 0)) → (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /_L 𝑛)↑(𝑛 pCnt 𝑀)), 1)))‘(abs‘𝑀)) ∈ ℂ)
161		zdclt 9359	. . . . . . . 8 ⊢ ((𝑁 ∈ ℤ ∧ 0 ∈ ℤ) → DECID 𝑁 < 0)
162	16, 21, 161	sylancl 413	. . . . . . 7 ⊢ (((𝐴 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑀 ≠ 0 ∧ 𝑁 ≠ 0)) → DECID 𝑁 < 0)
163		dcan2 936	. . . . . . 7 ⊢ (DECID 𝑁 < 0 → (DECID 𝐴 < 0 → DECID (𝑁 < 0 ∧ 𝐴 < 0)))
164	162, 148, 163	sylc 62	. . . . . 6 ⊢ (((𝐴 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑀 ≠ 0 ∧ 𝑁 ≠ 0)) → DECID (𝑁 < 0 ∧ 𝐴 < 0))
165	143, 144, 164	ifcldcd 3585	. . . . 5 ⊢ (((𝐴 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑀 ≠ 0 ∧ 𝑁 ≠ 0)) → if((𝑁 < 0 ∧ 𝐴 < 0), -1, 1) ∈ ℤ)
166	165	zcnd 9405	. . . 4 ⊢ (((𝐴 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑀 ≠ 0 ∧ 𝑁 ≠ 0)) → if((𝑁 < 0 ∧ 𝐴 < 0), -1, 1) ∈ ℂ)
167	48	ffvelcdmda 5671	. . . . . . 7 ⊢ ((((𝐴 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑀 ≠ 0 ∧ 𝑁 ≠ 0)) ∧ 𝑘 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /_L 𝑛)↑(𝑛 pCnt 𝑁)), 1))‘𝑘) ∈ ℤ)
168	35, 144, 167, 155	seqf 10491	. . . . . 6 ⊢ (((𝐴 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑀 ≠ 0 ∧ 𝑁 ≠ 0)) → seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /_L 𝑛)↑(𝑛 pCnt 𝑁)), 1))):ℕ⟶ℤ)
169		nnabscl 11140	. . . . . . 7 ⊢ ((𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) → (abs‘𝑁) ∈ ℕ)
170	16, 25, 169	syl2anc 411	. . . . . 6 ⊢ (((𝐴 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑀 ≠ 0 ∧ 𝑁 ≠ 0)) → (abs‘𝑁) ∈ ℕ)
171	168, 170	ffvelcdmd 5672	. . . . 5 ⊢ (((𝐴 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑀 ≠ 0 ∧ 𝑁 ≠ 0)) → (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /_L 𝑛)↑(𝑛 pCnt 𝑁)), 1)))‘(abs‘𝑁)) ∈ ℤ)
172	171	zcnd 9405	. . . 4 ⊢ (((𝐴 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑀 ≠ 0 ∧ 𝑁 ≠ 0)) → (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /_L 𝑛)↑(𝑛 pCnt 𝑁)), 1)))‘(abs‘𝑁)) ∈ ℂ)
173	152, 160, 166, 172	mul4d 8141	. . 3 ⊢ (((𝐴 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑀 ≠ 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‘𝑁)))))
174	141, 173	eqtrd 2222	. 2 ⊢ (((𝐴 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑀 ≠ 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‘𝑁)))))
175	134, 136, 174	3eqtr4d 2232	1 ⊢ (((𝐴 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑀 ≠ 0 ∧ 𝑁 ≠ 0)) → (𝐴 /_L (𝑀 · 𝑁)) = ((𝐴 /_L 𝑀) · (𝐴 /_L 𝑁)))

Colors of variables: wff set class

Syntax hints: ¬ wn 3 → wi 4 ∧ wa 104 ↔ wb 105 ∨ wo 709 DECID wdc 835 ∧ w3a 980 = wceq 1364 ∈ wcel 2160 ≠ wne 2360 ifcif 3549 class class class wbr 4018 ↦ cmpt 4079 ⟶wf 5231 ‘cfv 5235 (class class class)co 5895 0cc0 7840 1c1 7841 + caddc 7843 · cmul 7845 < clt 8021 -cneg 8158 # cap 8567 ℕcn 8948 ℕ₀cn0 9205 ℤcz 9282 ℤ_≥cuz 9557 seqcseq 10475 ↑cexp 10549 abscabs 11037 ℙcprime 12138 pCnt cpc 12315 /_L clgs 14851

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-in1 615 ax-in2 616 ax-io 710 ax-5 1458 ax-7 1459 ax-gen 1460 ax-ie1 1504 ax-ie2 1505 ax-8 1515 ax-10 1516 ax-11 1517 ax-i12 1518 ax-bndl 1520 ax-4 1521 ax-17 1537 ax-i9 1541 ax-ial 1545 ax-i5r 1546 ax-13 2162 ax-14 2163 ax-ext 2171 ax-coll 4133 ax-sep 4136 ax-nul 4144 ax-pow 4192 ax-pr 4227 ax-un 4451 ax-setind 4554 ax-iinf 4605 ax-cnex 7931 ax-resscn 7932 ax-1cn 7933 ax-1re 7934 ax-icn 7935 ax-addcl 7936 ax-addrcl 7937 ax-mulcl 7938 ax-mulrcl 7939 ax-addcom 7940 ax-mulcom 7941 ax-addass 7942 ax-mulass 7943 ax-distr 7944 ax-i2m1 7945 ax-0lt1 7946 ax-1rid 7947 ax-0id 7948 ax-rnegex 7949 ax-precex 7950 ax-cnre 7951 ax-pre-ltirr 7952 ax-pre-ltwlin 7953 ax-pre-lttrn 7954 ax-pre-apti 7955 ax-pre-ltadd 7956 ax-pre-mulgt0 7957 ax-pre-mulext 7958 ax-arch 7959 ax-caucvg 7960

This theorem depends on definitions: df-bi 117 df-stab 832 df-dc 836 df-3or 981 df-3an 982 df-tru 1367 df-fal 1370 df-xor 1387 df-nf 1472 df-sb 1774 df-eu 2041 df-mo 2042 df-clab 2176 df-cleq 2182 df-clel 2185 df-nfc 2321 df-ne 2361 df-nel 2456 df-ral 2473 df-rex 2474 df-reu 2475 df-rmo 2476 df-rab 2477 df-v 2754 df-sbc 2978 df-csb 3073 df-dif 3146 df-un 3148 df-in 3150 df-ss 3157 df-nul 3438 df-if 3550 df-pw 3592 df-sn 3613 df-pr 3614 df-op 3616 df-uni 3825 df-int 3860 df-iun 3903 df-br 4019 df-opab 4080 df-mpt 4081 df-tr 4117 df-id 4311 df-po 4314 df-iso 4315 df-iord 4384 df-on 4386 df-ilim 4387 df-suc 4389 df-iom 4608 df-xp 4650 df-rel 4651 df-cnv 4652 df-co 4653 df-dm 4654 df-rn 4655 df-res 4656 df-ima 4657 df-iota 5196 df-fun 5237 df-fn 5238 df-f 5239 df-f1 5240 df-fo 5241 df-f1o 5242 df-fv 5243 df-isom 5244 df-riota 5851 df-ov 5898 df-oprab 5899 df-mpo 5900 df-1st 6164 df-2nd 6165 df-recs 6329 df-irdg 6394 df-frec 6415 df-1o 6440 df-2o 6441 df-oadd 6444 df-er 6558 df-en 6766 df-dom 6767 df-fin 6768 df-sup 7012 df-inf 7013 df-pnf 8023 df-mnf 8024 df-xr 8025 df-ltxr 8026 df-le 8027 df-sub 8159 df-neg 8160 df-reap 8561 df-ap 8568 df-div 8659 df-inn 8949 df-2 9007 df-3 9008 df-4 9009 df-5 9010 df-6 9011 df-7 9012 df-8 9013 df-n0 9206 df-z 9283 df-uz 9558 df-q 9649 df-rp 9683 df-fz 10038 df-fzo 10172 df-fl 10300 df-mod 10353 df-seqfrec 10476 df-exp 10550 df-ihash 10787 df-cj 10882 df-re 10883 df-im 10884 df-rsqrt 11038 df-abs 11039 df-clim 11318 df-proddc 11590 df-dvds 11826 df-gcd 11975 df-prm 12139 df-phi 12242 df-pc 12316 df-lgs 14852

This theorem is referenced by: lgssq2 14895 lgsdinn0 14902

W3C validator