Metamath Proof Explorer

Theorem lgsdi

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

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

Proof

Step Hyp Ref Expression
1 3anrot ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ↔ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐴 ∈ ℤ ) )
2 lgsdilem ⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐴 ∈ ℤ ) ∧ ( 𝑀 ≠ 0 ∧ 𝑁 ≠ 0 ) ) → if ( ( 𝐴 < 0 ∧ ( 𝑀 · 𝑁 ) < 0 ) , - 1 , 1 ) = ( if ( ( 𝐴 < 0 ∧ 𝑀 < 0 ) , - 1 , 1 ) · if ( ( 𝐴 < 0 ∧ 𝑁 < 0 ) , - 1 , 1 ) ) )
3 1 2 sylanb ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑀 ≠ 0 ∧ 𝑁 ≠ 0 ) ) → if ( ( 𝐴 < 0 ∧ ( 𝑀 · 𝑁 ) < 0 ) , - 1 , 1 ) = ( if ( ( 𝐴 < 0 ∧ 𝑀 < 0 ) , - 1 , 1 ) · if ( ( 𝐴 < 0 ∧ 𝑁 < 0 ) , - 1 , 1 ) ) )
4 ancom ⊢ ( ( ( 𝑀 · 𝑁 ) < 0 ∧ 𝐴 < 0 ) ↔ ( 𝐴 < 0 ∧ ( 𝑀 · 𝑁 ) < 0 ) )
5 ifbi ⊢ ( ( ( ( 𝑀 · 𝑁 ) < 0 ∧ 𝐴 < 0 ) ↔ ( 𝐴 < 0 ∧ ( 𝑀 · 𝑁 ) < 0 ) ) → if ( ( ( 𝑀 · 𝑁 ) < 0 ∧ 𝐴 < 0 ) , - 1 , 1 ) = if ( ( 𝐴 < 0 ∧ ( 𝑀 · 𝑁 ) < 0 ) , - 1 , 1 ) )
6 4 5 ax-mp ⊢ if ( ( ( 𝑀 · 𝑁 ) < 0 ∧ 𝐴 < 0 ) , - 1 , 1 ) = if ( ( 𝐴 < 0 ∧ ( 𝑀 · 𝑁 ) < 0 ) , - 1 , 1 )
7 ancom ⊢ ( ( 𝑀 < 0 ∧ 𝐴 < 0 ) ↔ ( 𝐴 < 0 ∧ 𝑀 < 0 ) )
8 ifbi ⊢ ( ( ( 𝑀 < 0 ∧ 𝐴 < 0 ) ↔ ( 𝐴 < 0 ∧ 𝑀 < 0 ) ) → if ( ( 𝑀 < 0 ∧ 𝐴 < 0 ) , - 1 , 1 ) = if ( ( 𝐴 < 0 ∧ 𝑀 < 0 ) , - 1 , 1 ) )
9 7 8 ax-mp ⊢ if ( ( 𝑀 < 0 ∧ 𝐴 < 0 ) , - 1 , 1 ) = if ( ( 𝐴 < 0 ∧ 𝑀 < 0 ) , - 1 , 1 )
10 ancom ⊢ ( ( 𝑁 < 0 ∧ 𝐴 < 0 ) ↔ ( 𝐴 < 0 ∧ 𝑁 < 0 ) )
11 ifbi ⊢ ( ( ( 𝑁 < 0 ∧ 𝐴 < 0 ) ↔ ( 𝐴 < 0 ∧ 𝑁 < 0 ) ) → if ( ( 𝑁 < 0 ∧ 𝐴 < 0 ) , - 1 , 1 ) = if ( ( 𝐴 < 0 ∧ 𝑁 < 0 ) , - 1 , 1 ) )
12 10 11 ax-mp ⊢ if ( ( 𝑁 < 0 ∧ 𝐴 < 0 ) , - 1 , 1 ) = if ( ( 𝐴 < 0 ∧ 𝑁 < 0 ) , - 1 , 1 )
13 9 12 oveq12i ⊢ ( 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 ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑀 ≠ 0 ∧ 𝑁 ≠ 0 ) ) → if ( ( ( 𝑀 · 𝑁 ) < 0 ∧ 𝐴 < 0 ) , - 1 , 1 ) = ( if ( ( 𝑀 < 0 ∧ 𝐴 < 0 ) , - 1 , 1 ) · if ( ( 𝑁 < 0 ∧ 𝐴 < 0 ) , - 1 , 1 ) ) )
15 simpl2 ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑀 ≠ 0 ∧ 𝑁 ≠ 0 ) ) → 𝑀 ∈ ℤ )
16 simpl3 ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑀 ≠ 0 ∧ 𝑁 ≠ 0 ) ) → 𝑁 ∈ ℤ )
17 15 16 zmulcld ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑀 ≠ 0 ∧ 𝑁 ≠ 0 ) ) → ( 𝑀 · 𝑁 ) ∈ ℤ )
18 15 zcnd ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑀 ≠ 0 ∧ 𝑁 ≠ 0 ) ) → 𝑀 ∈ ℂ )
19 16 zcnd ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑀 ≠ 0 ∧ 𝑁 ≠ 0 ) ) → 𝑁 ∈ ℂ )
20 simprl ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑀 ≠ 0 ∧ 𝑁 ≠ 0 ) ) → 𝑀 ≠ 0 )
21 simprr ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑀 ≠ 0 ∧ 𝑁 ≠ 0 ) ) → 𝑁 ≠ 0 )
22 18 19 20 21 mulne0d ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑀 ≠ 0 ∧ 𝑁 ≠ 0 ) ) → ( 𝑀 · 𝑁 ) ≠ 0 )
23 nnabscl ⊢ ( ( ( 𝑀 · 𝑁 ) ∈ ℤ ∧ ( 𝑀 · 𝑁 ) ≠ 0 ) → ( abs ‘ ( 𝑀 · 𝑁 ) ) ∈ ℕ )
24 17 22 23 syl2anc ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑀 ≠ 0 ∧ 𝑁 ≠ 0 ) ) → ( abs ‘ ( 𝑀 · 𝑁 ) ) ∈ ℕ )
25 nnuz ⊢ ℕ = ( ℤ≥ ‘ 1 )
26 24 25 eleqtrdi ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑀 ≠ 0 ∧ 𝑁 ≠ 0 ) ) → ( abs ‘ ( 𝑀 · 𝑁 ) ) ∈ ( ℤ≥ ‘ 1 ) )
27 simpl1 ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑀 ≠ 0 ∧ 𝑁 ≠ 0 ) ) → 𝐴 ∈ ℤ )
28 eqid ⊢ ( 𝑛 ∈ ℕ ↦ if ( 𝑛 ∈ ℙ , ( ( 𝐴 /L 𝑛 ) ↑ ( 𝑛 pCnt 𝑀 ) ) , 1 ) ) = ( 𝑛 ∈ ℕ ↦ if ( 𝑛 ∈ ℙ , ( ( 𝐴 /L 𝑛 ) ↑ ( 𝑛 pCnt 𝑀 ) ) , 1 ) )
29 28 lgsfcl3 ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑀 ≠ 0 ) → ( 𝑛 ∈ ℕ ↦ if ( 𝑛 ∈ ℙ , ( ( 𝐴 /L 𝑛 ) ↑ ( 𝑛 pCnt 𝑀 ) ) , 1 ) ) : ℕ ⟶ ℤ )
30 27 15 20 29 syl3anc ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑀 ≠ 0 ∧ 𝑁 ≠ 0 ) ) → ( 𝑛 ∈ ℕ ↦ if ( 𝑛 ∈ ℙ , ( ( 𝐴 /L 𝑛 ) ↑ ( 𝑛 pCnt 𝑀 ) ) , 1 ) ) : ℕ ⟶ ℤ )
31 elfznn ⊢ ( 𝑘 ∈ ( 1 ... ( abs ‘ ( 𝑀 · 𝑁 ) ) ) → 𝑘 ∈ ℕ )
32 ffvelcdm ⊢ ( ( ( 𝑛 ∈ ℕ ↦ if ( 𝑛 ∈ ℙ , ( ( 𝐴 /L 𝑛 ) ↑ ( 𝑛 pCnt 𝑀 ) ) , 1 ) ) : ℕ ⟶ ℤ ∧ 𝑘 ∈ ℕ ) → ( ( 𝑛 ∈ ℕ ↦ if ( 𝑛 ∈ ℙ , ( ( 𝐴 /L 𝑛 ) ↑ ( 𝑛 pCnt 𝑀 ) ) , 1 ) ) ‘ 𝑘 ) ∈ ℤ )
33 30 31 32 syl2an ⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑀 ≠ 0 ∧ 𝑁 ≠ 0 ) ) ∧ 𝑘 ∈ ( 1 ... ( abs ‘ ( 𝑀 · 𝑁 ) ) ) ) → ( ( 𝑛 ∈ ℕ ↦ if ( 𝑛 ∈ ℙ , ( ( 𝐴 /L 𝑛 ) ↑ ( 𝑛 pCnt 𝑀 ) ) , 1 ) ) ‘ 𝑘 ) ∈ ℤ )
34 33 zcnd ⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑀 ≠ 0 ∧ 𝑁 ≠ 0 ) ) ∧ 𝑘 ∈ ( 1 ... ( abs ‘ ( 𝑀 · 𝑁 ) ) ) ) → ( ( 𝑛 ∈ ℕ ↦ if ( 𝑛 ∈ ℙ , ( ( 𝐴 /L 𝑛 ) ↑ ( 𝑛 pCnt 𝑀 ) ) , 1 ) ) ‘ 𝑘 ) ∈ ℂ )
35 eqid ⊢ ( 𝑛 ∈ ℕ ↦ if ( 𝑛 ∈ ℙ , ( ( 𝐴 /L 𝑛 ) ↑ ( 𝑛 pCnt 𝑁 ) ) , 1 ) ) = ( 𝑛 ∈ ℕ ↦ if ( 𝑛 ∈ ℙ , ( ( 𝐴 /L 𝑛 ) ↑ ( 𝑛 pCnt 𝑁 ) ) , 1 ) )
36 35 lgsfcl3 ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) → ( 𝑛 ∈ ℕ ↦ if ( 𝑛 ∈ ℙ , ( ( 𝐴 /L 𝑛 ) ↑ ( 𝑛 pCnt 𝑁 ) ) , 1 ) ) : ℕ ⟶ ℤ )
37 27 16 21 36 syl3anc ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑀 ≠ 0 ∧ 𝑁 ≠ 0 ) ) → ( 𝑛 ∈ ℕ ↦ if ( 𝑛 ∈ ℙ , ( ( 𝐴 /L 𝑛 ) ↑ ( 𝑛 pCnt 𝑁 ) ) , 1 ) ) : ℕ ⟶ ℤ )
38 ffvelcdm ⊢ ( ( ( 𝑛 ∈ ℕ ↦ if ( 𝑛 ∈ ℙ , ( ( 𝐴 /L 𝑛 ) ↑ ( 𝑛 pCnt 𝑁 ) ) , 1 ) ) : ℕ ⟶ ℤ ∧ 𝑘 ∈ ℕ ) → ( ( 𝑛 ∈ ℕ ↦ if ( 𝑛 ∈ ℙ , ( ( 𝐴 /L 𝑛 ) ↑ ( 𝑛 pCnt 𝑁 ) ) , 1 ) ) ‘ 𝑘 ) ∈ ℤ )
39 37 31 38 syl2an ⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑀 ≠ 0 ∧ 𝑁 ≠ 0 ) ) ∧ 𝑘 ∈ ( 1 ... ( abs ‘ ( 𝑀 · 𝑁 ) ) ) ) → ( ( 𝑛 ∈ ℕ ↦ if ( 𝑛 ∈ ℙ , ( ( 𝐴 /L 𝑛 ) ↑ ( 𝑛 pCnt 𝑁 ) ) , 1 ) ) ‘ 𝑘 ) ∈ ℤ )
40 39 zcnd ⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑀 ≠ 0 ∧ 𝑁 ≠ 0 ) ) ∧ 𝑘 ∈ ( 1 ... ( abs ‘ ( 𝑀 · 𝑁 ) ) ) ) → ( ( 𝑛 ∈ ℕ ↦ if ( 𝑛 ∈ ℙ , ( ( 𝐴 /L 𝑛 ) ↑ ( 𝑛 pCnt 𝑁 ) ) , 1 ) ) ‘ 𝑘 ) ∈ ℂ )
41 simpr ⊢ ( ( ( ( ( 𝐴 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑀 ≠ 0 ∧ 𝑁 ≠ 0 ) ) ∧ 𝑘 ∈ ( 1 ... ( abs ‘ ( 𝑀 · 𝑁 ) ) ) ) ∧ 𝑘 ∈ ℙ ) → 𝑘 ∈ ℙ )
42 15 ad2antrr ⊢ ( ( ( ( ( 𝐴 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑀 ≠ 0 ∧ 𝑁 ≠ 0 ) ) ∧ 𝑘 ∈ ( 1 ... ( abs ‘ ( 𝑀 · 𝑁 ) ) ) ) ∧ 𝑘 ∈ ℙ ) → 𝑀 ∈ ℤ )
43 20 ad2antrr ⊢ ( ( ( ( ( 𝐴 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑀 ≠ 0 ∧ 𝑁 ≠ 0 ) ) ∧ 𝑘 ∈ ( 1 ... ( abs ‘ ( 𝑀 · 𝑁 ) ) ) ) ∧ 𝑘 ∈ ℙ ) → 𝑀 ≠ 0 )
44 16 ad2antrr ⊢ ( ( ( ( ( 𝐴 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑀 ≠ 0 ∧ 𝑁 ≠ 0 ) ) ∧ 𝑘 ∈ ( 1 ... ( abs ‘ ( 𝑀 · 𝑁 ) ) ) ) ∧ 𝑘 ∈ ℙ ) → 𝑁 ∈ ℤ )
45 21 ad2antrr ⊢ ( ( ( ( ( 𝐴 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑀 ≠ 0 ∧ 𝑁 ≠ 0 ) ) ∧ 𝑘 ∈ ( 1 ... ( abs ‘ ( 𝑀 · 𝑁 ) ) ) ) ∧ 𝑘 ∈ ℙ ) → 𝑁 ≠ 0 )
46 pcmul ⊢ ( ( 𝑘 ∈ ℙ ∧ ( 𝑀 ∈ ℤ ∧ 𝑀 ≠ 0 ) ∧ ( 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) ) → ( 𝑘 pCnt ( 𝑀 · 𝑁 ) ) = ( ( 𝑘 pCnt 𝑀 ) + ( 𝑘 pCnt 𝑁 ) ) )
47 41 42 43 44 45 46 syl122anc ⊢ ( ( ( ( ( 𝐴 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑀 ≠ 0 ∧ 𝑁 ≠ 0 ) ) ∧ 𝑘 ∈ ( 1 ... ( abs ‘ ( 𝑀 · 𝑁 ) ) ) ) ∧ 𝑘 ∈ ℙ ) → ( 𝑘 pCnt ( 𝑀 · 𝑁 ) ) = ( ( 𝑘 pCnt 𝑀 ) + ( 𝑘 pCnt 𝑁 ) ) )
48 47 oveq2d ⊢ ( ( ( ( ( 𝐴 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑀 ≠ 0 ∧ 𝑁 ≠ 0 ) ) ∧ 𝑘 ∈ ( 1 ... ( abs ‘ ( 𝑀 · 𝑁 ) ) ) ) ∧ 𝑘 ∈ ℙ ) → ( ( 𝐴 /L 𝑘 ) ↑ ( 𝑘 pCnt ( 𝑀 · 𝑁 ) ) ) = ( ( 𝐴 /L 𝑘 ) ↑ ( ( 𝑘 pCnt 𝑀 ) + ( 𝑘 pCnt 𝑁 ) ) ) )
49 27 ad2antrr ⊢ ( ( ( ( ( 𝐴 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑀 ≠ 0 ∧ 𝑁 ≠ 0 ) ) ∧ 𝑘 ∈ ( 1 ... ( abs ‘ ( 𝑀 · 𝑁 ) ) ) ) ∧ 𝑘 ∈ ℙ ) → 𝐴 ∈ ℤ )
50 prmz ⊢ ( 𝑘 ∈ ℙ → 𝑘 ∈ ℤ )
51 50 adantl ⊢ ( ( ( ( ( 𝐴 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑀 ≠ 0 ∧ 𝑁 ≠ 0 ) ) ∧ 𝑘 ∈ ( 1 ... ( abs ‘ ( 𝑀 · 𝑁 ) ) ) ) ∧ 𝑘 ∈ ℙ ) → 𝑘 ∈ ℤ )
52 lgscl ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑘 ∈ ℤ ) → ( 𝐴 /L 𝑘 ) ∈ ℤ )
53 49 51 52 syl2anc ⊢ ( ( ( ( ( 𝐴 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑀 ≠ 0 ∧ 𝑁 ≠ 0 ) ) ∧ 𝑘 ∈ ( 1 ... ( abs ‘ ( 𝑀 · 𝑁 ) ) ) ) ∧ 𝑘 ∈ ℙ ) → ( 𝐴 /L 𝑘 ) ∈ ℤ )
54 53 zcnd ⊢ ( ( ( ( ( 𝐴 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑀 ≠ 0 ∧ 𝑁 ≠ 0 ) ) ∧ 𝑘 ∈ ( 1 ... ( abs ‘ ( 𝑀 · 𝑁 ) ) ) ) ∧ 𝑘 ∈ ℙ ) → ( 𝐴 /L 𝑘 ) ∈ ℂ )
55 pczcl ⊢ ( ( 𝑘 ∈ ℙ ∧ ( 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) ) → ( 𝑘 pCnt 𝑁 ) ∈ ℕ0 )
56 41 44 45 55 syl12anc ⊢ ( ( ( ( ( 𝐴 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑀 ≠ 0 ∧ 𝑁 ≠ 0 ) ) ∧ 𝑘 ∈ ( 1 ... ( abs ‘ ( 𝑀 · 𝑁 ) ) ) ) ∧ 𝑘 ∈ ℙ ) → ( 𝑘 pCnt 𝑁 ) ∈ ℕ0 )
57 pczcl ⊢ ( ( 𝑘 ∈ ℙ ∧ ( 𝑀 ∈ ℤ ∧ 𝑀 ≠ 0 ) ) → ( 𝑘 pCnt 𝑀 ) ∈ ℕ0 )
58 41 42 43 57 syl12anc ⊢ ( ( ( ( ( 𝐴 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑀 ≠ 0 ∧ 𝑁 ≠ 0 ) ) ∧ 𝑘 ∈ ( 1 ... ( abs ‘ ( 𝑀 · 𝑁 ) ) ) ) ∧ 𝑘 ∈ ℙ ) → ( 𝑘 pCnt 𝑀 ) ∈ ℕ0 )
59 54 56 58 expaddd ⊢ ( ( ( ( ( 𝐴 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑀 ≠ 0 ∧ 𝑁 ≠ 0 ) ) ∧ 𝑘 ∈ ( 1 ... ( abs ‘ ( 𝑀 · 𝑁 ) ) ) ) ∧ 𝑘 ∈ ℙ ) → ( ( 𝐴 /L 𝑘 ) ↑ ( ( 𝑘 pCnt 𝑀 ) + ( 𝑘 pCnt 𝑁 ) ) ) = ( ( ( 𝐴 /L 𝑘 ) ↑ ( 𝑘 pCnt 𝑀 ) ) · ( ( 𝐴 /L 𝑘 ) ↑ ( 𝑘 pCnt 𝑁 ) ) ) )
60 48 59 eqtrd ⊢ ( ( ( ( ( 𝐴 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑀 ≠ 0 ∧ 𝑁 ≠ 0 ) ) ∧ 𝑘 ∈ ( 1 ... ( abs ‘ ( 𝑀 · 𝑁 ) ) ) ) ∧ 𝑘 ∈ ℙ ) → ( ( 𝐴 /L 𝑘 ) ↑ ( 𝑘 pCnt ( 𝑀 · 𝑁 ) ) ) = ( ( ( 𝐴 /L 𝑘 ) ↑ ( 𝑘 pCnt 𝑀 ) ) · ( ( 𝐴 /L 𝑘 ) ↑ ( 𝑘 pCnt 𝑁 ) ) ) )
61 iftrue ⊢ ( 𝑘 ∈ ℙ → if ( 𝑘 ∈ ℙ , ( ( 𝐴 /L 𝑘 ) ↑ ( 𝑘 pCnt ( 𝑀 · 𝑁 ) ) ) , 1 ) = ( ( 𝐴 /L 𝑘 ) ↑ ( 𝑘 pCnt ( 𝑀 · 𝑁 ) ) ) )
62 61 adantl ⊢ ( ( ( ( ( 𝐴 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑀 ≠ 0 ∧ 𝑁 ≠ 0 ) ) ∧ 𝑘 ∈ ( 1 ... ( abs ‘ ( 𝑀 · 𝑁 ) ) ) ) ∧ 𝑘 ∈ ℙ ) → if ( 𝑘 ∈ ℙ , ( ( 𝐴 /L 𝑘 ) ↑ ( 𝑘 pCnt ( 𝑀 · 𝑁 ) ) ) , 1 ) = ( ( 𝐴 /L 𝑘 ) ↑ ( 𝑘 pCnt ( 𝑀 · 𝑁 ) ) ) )
63 iftrue ⊢ ( 𝑘 ∈ ℙ → if ( 𝑘 ∈ ℙ , ( ( 𝐴 /L 𝑘 ) ↑ ( 𝑘 pCnt 𝑀 ) ) , 1 ) = ( ( 𝐴 /L 𝑘 ) ↑ ( 𝑘 pCnt 𝑀 ) ) )
64 iftrue ⊢ ( 𝑘 ∈ ℙ → if ( 𝑘 ∈ ℙ , ( ( 𝐴 /L 𝑘 ) ↑ ( 𝑘 pCnt 𝑁 ) ) , 1 ) = ( ( 𝐴 /L 𝑘 ) ↑ ( 𝑘 pCnt 𝑁 ) ) )
65 63 64 oveq12d ⊢ ( 𝑘 ∈ ℙ → ( if ( 𝑘 ∈ ℙ , ( ( 𝐴 /L 𝑘 ) ↑ ( 𝑘 pCnt 𝑀 ) ) , 1 ) · if ( 𝑘 ∈ ℙ , ( ( 𝐴 /L 𝑘 ) ↑ ( 𝑘 pCnt 𝑁 ) ) , 1 ) ) = ( ( ( 𝐴 /L 𝑘 ) ↑ ( 𝑘 pCnt 𝑀 ) ) · ( ( 𝐴 /L 𝑘 ) ↑ ( 𝑘 pCnt 𝑁 ) ) ) )
66 65 adantl ⊢ ( ( ( ( ( 𝐴 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑀 ≠ 0 ∧ 𝑁 ≠ 0 ) ) ∧ 𝑘 ∈ ( 1 ... ( abs ‘ ( 𝑀 · 𝑁 ) ) ) ) ∧ 𝑘 ∈ ℙ ) → ( if ( 𝑘 ∈ ℙ , ( ( 𝐴 /L 𝑘 ) ↑ ( 𝑘 pCnt 𝑀 ) ) , 1 ) · if ( 𝑘 ∈ ℙ , ( ( 𝐴 /L 𝑘 ) ↑ ( 𝑘 pCnt 𝑁 ) ) , 1 ) ) = ( ( ( 𝐴 /L 𝑘 ) ↑ ( 𝑘 pCnt 𝑀 ) ) · ( ( 𝐴 /L 𝑘 ) ↑ ( 𝑘 pCnt 𝑁 ) ) ) )
67 60 62 66 3eqtr4rd ⊢ ( ( ( ( ( 𝐴 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑀 ≠ 0 ∧ 𝑁 ≠ 0 ) ) ∧ 𝑘 ∈ ( 1 ... ( abs ‘ ( 𝑀 · 𝑁 ) ) ) ) ∧ 𝑘 ∈ ℙ ) → ( if ( 𝑘 ∈ ℙ , ( ( 𝐴 /L 𝑘 ) ↑ ( 𝑘 pCnt 𝑀 ) ) , 1 ) · if ( 𝑘 ∈ ℙ , ( ( 𝐴 /L 𝑘 ) ↑ ( 𝑘 pCnt 𝑁 ) ) , 1 ) ) = if ( 𝑘 ∈ ℙ , ( ( 𝐴 /L 𝑘 ) ↑ ( 𝑘 pCnt ( 𝑀 · 𝑁 ) ) ) , 1 ) )
68 1t1e1 ⊢ ( 1 · 1 ) = 1
69 iffalse ⊢ ( ¬ 𝑘 ∈ ℙ → if ( 𝑘 ∈ ℙ , ( ( 𝐴 /L 𝑘 ) ↑ ( 𝑘 pCnt 𝑀 ) ) , 1 ) = 1 )
70 iffalse ⊢ ( ¬ 𝑘 ∈ ℙ → if ( 𝑘 ∈ ℙ , ( ( 𝐴 /L 𝑘 ) ↑ ( 𝑘 pCnt 𝑁 ) ) , 1 ) = 1 )
71 69 70 oveq12d ⊢ ( ¬ 𝑘 ∈ ℙ → ( if ( 𝑘 ∈ ℙ , ( ( 𝐴 /L 𝑘 ) ↑ ( 𝑘 pCnt 𝑀 ) ) , 1 ) · if ( 𝑘 ∈ ℙ , ( ( 𝐴 /L 𝑘 ) ↑ ( 𝑘 pCnt 𝑁 ) ) , 1 ) ) = ( 1 · 1 ) )
72 iffalse ⊢ ( ¬ 𝑘 ∈ ℙ → if ( 𝑘 ∈ ℙ , ( ( 𝐴 /L 𝑘 ) ↑ ( 𝑘 pCnt ( 𝑀 · 𝑁 ) ) ) , 1 ) = 1 )
73 68 71 72 3eqtr4a ⊢ ( ¬ 𝑘 ∈ ℙ → ( if ( 𝑘 ∈ ℙ , ( ( 𝐴 /L 𝑘 ) ↑ ( 𝑘 pCnt 𝑀 ) ) , 1 ) · if ( 𝑘 ∈ ℙ , ( ( 𝐴 /L 𝑘 ) ↑ ( 𝑘 pCnt 𝑁 ) ) , 1 ) ) = if ( 𝑘 ∈ ℙ , ( ( 𝐴 /L 𝑘 ) ↑ ( 𝑘 pCnt ( 𝑀 · 𝑁 ) ) ) , 1 ) )
74 73 adantl ⊢ ( ( ( ( ( 𝐴 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑀 ≠ 0 ∧ 𝑁 ≠ 0 ) ) ∧ 𝑘 ∈ ( 1 ... ( abs ‘ ( 𝑀 · 𝑁 ) ) ) ) ∧ ¬ 𝑘 ∈ ℙ ) → ( if ( 𝑘 ∈ ℙ , ( ( 𝐴 /L 𝑘 ) ↑ ( 𝑘 pCnt 𝑀 ) ) , 1 ) · if ( 𝑘 ∈ ℙ , ( ( 𝐴 /L 𝑘 ) ↑ ( 𝑘 pCnt 𝑁 ) ) , 1 ) ) = if ( 𝑘 ∈ ℙ , ( ( 𝐴 /L 𝑘 ) ↑ ( 𝑘 pCnt ( 𝑀 · 𝑁 ) ) ) , 1 ) )
75 67 74 pm2.61dan ⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑀 ≠ 0 ∧ 𝑁 ≠ 0 ) ) ∧ 𝑘 ∈ ( 1 ... ( abs ‘ ( 𝑀 · 𝑁 ) ) ) ) → ( if ( 𝑘 ∈ ℙ , ( ( 𝐴 /L 𝑘 ) ↑ ( 𝑘 pCnt 𝑀 ) ) , 1 ) · if ( 𝑘 ∈ ℙ , ( ( 𝐴 /L 𝑘 ) ↑ ( 𝑘 pCnt 𝑁 ) ) , 1 ) ) = if ( 𝑘 ∈ ℙ , ( ( 𝐴 /L 𝑘 ) ↑ ( 𝑘 pCnt ( 𝑀 · 𝑁 ) ) ) , 1 ) )
76 31 adantl ⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑀 ≠ 0 ∧ 𝑁 ≠ 0 ) ) ∧ 𝑘 ∈ ( 1 ... ( abs ‘ ( 𝑀 · 𝑁 ) ) ) ) → 𝑘 ∈ ℕ )
77 eleq1w ⊢ ( 𝑛 = 𝑘 → ( 𝑛 ∈ ℙ ↔ 𝑘 ∈ ℙ ) )
78 oveq2 ⊢ ( 𝑛 = 𝑘 → ( 𝐴 /L 𝑛 ) = ( 𝐴 /L 𝑘 ) )
79 oveq1 ⊢ ( 𝑛 = 𝑘 → ( 𝑛 pCnt 𝑀 ) = ( 𝑘 pCnt 𝑀 ) )
80 78 79 oveq12d ⊢ ( 𝑛 = 𝑘 → ( ( 𝐴 /L 𝑛 ) ↑ ( 𝑛 pCnt 𝑀 ) ) = ( ( 𝐴 /L 𝑘 ) ↑ ( 𝑘 pCnt 𝑀 ) ) )
81 77 80 ifbieq1d ⊢ ( 𝑛 = 𝑘 → if ( 𝑛 ∈ ℙ , ( ( 𝐴 /L 𝑛 ) ↑ ( 𝑛 pCnt 𝑀 ) ) , 1 ) = if ( 𝑘 ∈ ℙ , ( ( 𝐴 /L 𝑘 ) ↑ ( 𝑘 pCnt 𝑀 ) ) , 1 ) )
82 ovex ⊢ ( ( 𝐴 /L 𝑘 ) ↑ ( 𝑘 pCnt 𝑀 ) ) ∈ V
83 1ex ⊢ 1 ∈ V
84 82 83 ifex ⊢ if ( 𝑘 ∈ ℙ , ( ( 𝐴 /L 𝑘 ) ↑ ( 𝑘 pCnt 𝑀 ) ) , 1 ) ∈ V
85 81 28 84 fvmpt ⊢ ( 𝑘 ∈ ℕ → ( ( 𝑛 ∈ ℕ ↦ if ( 𝑛 ∈ ℙ , ( ( 𝐴 /L 𝑛 ) ↑ ( 𝑛 pCnt 𝑀 ) ) , 1 ) ) ‘ 𝑘 ) = if ( 𝑘 ∈ ℙ , ( ( 𝐴 /L 𝑘 ) ↑ ( 𝑘 pCnt 𝑀 ) ) , 1 ) )
86 oveq1 ⊢ ( 𝑛 = 𝑘 → ( 𝑛 pCnt 𝑁 ) = ( 𝑘 pCnt 𝑁 ) )
87 78 86 oveq12d ⊢ ( 𝑛 = 𝑘 → ( ( 𝐴 /L 𝑛 ) ↑ ( 𝑛 pCnt 𝑁 ) ) = ( ( 𝐴 /L 𝑘 ) ↑ ( 𝑘 pCnt 𝑁 ) ) )
88 77 87 ifbieq1d ⊢ ( 𝑛 = 𝑘 → if ( 𝑛 ∈ ℙ , ( ( 𝐴 /L 𝑛 ) ↑ ( 𝑛 pCnt 𝑁 ) ) , 1 ) = if ( 𝑘 ∈ ℙ , ( ( 𝐴 /L 𝑘 ) ↑ ( 𝑘 pCnt 𝑁 ) ) , 1 ) )
89 ovex ⊢ ( ( 𝐴 /L 𝑘 ) ↑ ( 𝑘 pCnt 𝑁 ) ) ∈ V
90 89 83 ifex ⊢ if ( 𝑘 ∈ ℙ , ( ( 𝐴 /L 𝑘 ) ↑ ( 𝑘 pCnt 𝑁 ) ) , 1 ) ∈ V
91 88 35 90 fvmpt ⊢ ( 𝑘 ∈ ℕ → ( ( 𝑛 ∈ ℕ ↦ if ( 𝑛 ∈ ℙ , ( ( 𝐴 /L 𝑛 ) ↑ ( 𝑛 pCnt 𝑁 ) ) , 1 ) ) ‘ 𝑘 ) = if ( 𝑘 ∈ ℙ , ( ( 𝐴 /L 𝑘 ) ↑ ( 𝑘 pCnt 𝑁 ) ) , 1 ) )
92 85 91 oveq12d ⊢ ( 𝑘 ∈ ℕ → ( ( ( 𝑛 ∈ ℕ ↦ if ( 𝑛 ∈ ℙ , ( ( 𝐴 /L 𝑛 ) ↑ ( 𝑛 pCnt 𝑀 ) ) , 1 ) ) ‘ 𝑘 ) · ( ( 𝑛 ∈ ℕ ↦ if ( 𝑛 ∈ ℙ , ( ( 𝐴 /L 𝑛 ) ↑ ( 𝑛 pCnt 𝑁 ) ) , 1 ) ) ‘ 𝑘 ) ) = ( if ( 𝑘 ∈ ℙ , ( ( 𝐴 /L 𝑘 ) ↑ ( 𝑘 pCnt 𝑀 ) ) , 1 ) · if ( 𝑘 ∈ ℙ , ( ( 𝐴 /L 𝑘 ) ↑ ( 𝑘 pCnt 𝑁 ) ) , 1 ) ) )
93 76 92 syl ⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑀 ≠ 0 ∧ 𝑁 ≠ 0 ) ) ∧ 𝑘 ∈ ( 1 ... ( abs ‘ ( 𝑀 · 𝑁 ) ) ) ) → ( ( ( 𝑛 ∈ ℕ ↦ if ( 𝑛 ∈ ℙ , ( ( 𝐴 /L 𝑛 ) ↑ ( 𝑛 pCnt 𝑀 ) ) , 1 ) ) ‘ 𝑘 ) · ( ( 𝑛 ∈ ℕ ↦ if ( 𝑛 ∈ ℙ , ( ( 𝐴 /L 𝑛 ) ↑ ( 𝑛 pCnt 𝑁 ) ) , 1 ) ) ‘ 𝑘 ) ) = ( if ( 𝑘 ∈ ℙ , ( ( 𝐴 /L 𝑘 ) ↑ ( 𝑘 pCnt 𝑀 ) ) , 1 ) · if ( 𝑘 ∈ ℙ , ( ( 𝐴 /L 𝑘 ) ↑ ( 𝑘 pCnt 𝑁 ) ) , 1 ) ) )
94 oveq1 ⊢ ( 𝑛 = 𝑘 → ( 𝑛 pCnt ( 𝑀 · 𝑁 ) ) = ( 𝑘 pCnt ( 𝑀 · 𝑁 ) ) )
95 78 94 oveq12d ⊢ ( 𝑛 = 𝑘 → ( ( 𝐴 /L 𝑛 ) ↑ ( 𝑛 pCnt ( 𝑀 · 𝑁 ) ) ) = ( ( 𝐴 /L 𝑘 ) ↑ ( 𝑘 pCnt ( 𝑀 · 𝑁 ) ) ) )
96 77 95 ifbieq1d ⊢ ( 𝑛 = 𝑘 → if ( 𝑛 ∈ ℙ , ( ( 𝐴 /L 𝑛 ) ↑ ( 𝑛 pCnt ( 𝑀 · 𝑁 ) ) ) , 1 ) = if ( 𝑘 ∈ ℙ , ( ( 𝐴 /L 𝑘 ) ↑ ( 𝑘 pCnt ( 𝑀 · 𝑁 ) ) ) , 1 ) )
97 eqid ⊢ ( 𝑛 ∈ ℕ ↦ if ( 𝑛 ∈ ℙ , ( ( 𝐴 /L 𝑛 ) ↑ ( 𝑛 pCnt ( 𝑀 · 𝑁 ) ) ) , 1 ) ) = ( 𝑛 ∈ ℕ ↦ if ( 𝑛 ∈ ℙ , ( ( 𝐴 /L 𝑛 ) ↑ ( 𝑛 pCnt ( 𝑀 · 𝑁 ) ) ) , 1 ) )
98 ovex ⊢ ( ( 𝐴 /L 𝑘 ) ↑ ( 𝑘 pCnt ( 𝑀 · 𝑁 ) ) ) ∈ V
99 98 83 ifex ⊢ if ( 𝑘 ∈ ℙ , ( ( 𝐴 /L 𝑘 ) ↑ ( 𝑘 pCnt ( 𝑀 · 𝑁 ) ) ) , 1 ) ∈ V
100 96 97 99 fvmpt ⊢ ( 𝑘 ∈ ℕ → ( ( 𝑛 ∈ ℕ ↦ if ( 𝑛 ∈ ℙ , ( ( 𝐴 /L 𝑛 ) ↑ ( 𝑛 pCnt ( 𝑀 · 𝑁 ) ) ) , 1 ) ) ‘ 𝑘 ) = if ( 𝑘 ∈ ℙ , ( ( 𝐴 /L 𝑘 ) ↑ ( 𝑘 pCnt ( 𝑀 · 𝑁 ) ) ) , 1 ) )
101 76 100 syl ⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑀 ≠ 0 ∧ 𝑁 ≠ 0 ) ) ∧ 𝑘 ∈ ( 1 ... ( abs ‘ ( 𝑀 · 𝑁 ) ) ) ) → ( ( 𝑛 ∈ ℕ ↦ if ( 𝑛 ∈ ℙ , ( ( 𝐴 /L 𝑛 ) ↑ ( 𝑛 pCnt ( 𝑀 · 𝑁 ) ) ) , 1 ) ) ‘ 𝑘 ) = if ( 𝑘 ∈ ℙ , ( ( 𝐴 /L 𝑘 ) ↑ ( 𝑘 pCnt ( 𝑀 · 𝑁 ) ) ) , 1 ) )
102 75 93 101 3eqtr4rd ⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑀 ≠ 0 ∧ 𝑁 ≠ 0 ) ) ∧ 𝑘 ∈ ( 1 ... ( abs ‘ ( 𝑀 · 𝑁 ) ) ) ) → ( ( 𝑛 ∈ ℕ ↦ if ( 𝑛 ∈ ℙ , ( ( 𝐴 /L 𝑛 ) ↑ ( 𝑛 pCnt ( 𝑀 · 𝑁 ) ) ) , 1 ) ) ‘ 𝑘 ) = ( ( ( 𝑛 ∈ ℕ ↦ if ( 𝑛 ∈ ℙ , ( ( 𝐴 /L 𝑛 ) ↑ ( 𝑛 pCnt 𝑀 ) ) , 1 ) ) ‘ 𝑘 ) · ( ( 𝑛 ∈ ℕ ↦ if ( 𝑛 ∈ ℙ , ( ( 𝐴 /L 𝑛 ) ↑ ( 𝑛 pCnt 𝑁 ) ) , 1 ) ) ‘ 𝑘 ) ) )
103 26 34 40 102 prodfmul ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑀 ≠ 0 ∧ 𝑁 ≠ 0 ) ) → ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ if ( 𝑛 ∈ ℙ , ( ( 𝐴 /L 𝑛 ) ↑ ( 𝑛 pCnt ( 𝑀 · 𝑁 ) ) ) , 1 ) ) ) ‘ ( abs ‘ ( 𝑀 · 𝑁 ) ) ) = ( ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ if ( 𝑛 ∈ ℙ , ( ( 𝐴 /L 𝑛 ) ↑ ( 𝑛 pCnt 𝑀 ) ) , 1 ) ) ) ‘ ( abs ‘ ( 𝑀 · 𝑁 ) ) ) · ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ if ( 𝑛 ∈ ℙ , ( ( 𝐴 /L 𝑛 ) ↑ ( 𝑛 pCnt 𝑁 ) ) , 1 ) ) ) ‘ ( abs ‘ ( 𝑀 · 𝑁 ) ) ) ) )
104 27 15 16 20 21 28 lgsdilem2 ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑀 ≠ 0 ∧ 𝑁 ≠ 0 ) ) → ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ if ( 𝑛 ∈ ℙ , ( ( 𝐴 /L 𝑛 ) ↑ ( 𝑛 pCnt 𝑀 ) ) , 1 ) ) ) ‘ ( abs ‘ 𝑀 ) ) = ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ if ( 𝑛 ∈ ℙ , ( ( 𝐴 /L 𝑛 ) ↑ ( 𝑛 pCnt 𝑀 ) ) , 1 ) ) ) ‘ ( abs ‘ ( 𝑀 · 𝑁 ) ) ) )
105 27 16 15 21 20 35 lgsdilem2 ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑀 ≠ 0 ∧ 𝑁 ≠ 0 ) ) → ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ if ( 𝑛 ∈ ℙ , ( ( 𝐴 /L 𝑛 ) ↑ ( 𝑛 pCnt 𝑁 ) ) , 1 ) ) ) ‘ ( abs ‘ 𝑁 ) ) = ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ if ( 𝑛 ∈ ℙ , ( ( 𝐴 /L 𝑛 ) ↑ ( 𝑛 pCnt 𝑁 ) ) , 1 ) ) ) ‘ ( abs ‘ ( 𝑁 · 𝑀 ) ) ) )
106 18 19 mulcomd ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑀 ≠ 0 ∧ 𝑁 ≠ 0 ) ) → ( 𝑀 · 𝑁 ) = ( 𝑁 · 𝑀 ) )
107 106 fveq2d ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑀 ≠ 0 ∧ 𝑁 ≠ 0 ) ) → ( abs ‘ ( 𝑀 · 𝑁 ) ) = ( abs ‘ ( 𝑁 · 𝑀 ) ) )
108 107 fveq2d ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑀 ≠ 0 ∧ 𝑁 ≠ 0 ) ) → ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ if ( 𝑛 ∈ ℙ , ( ( 𝐴 /L 𝑛 ) ↑ ( 𝑛 pCnt 𝑁 ) ) , 1 ) ) ) ‘ ( abs ‘ ( 𝑀 · 𝑁 ) ) ) = ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ if ( 𝑛 ∈ ℙ , ( ( 𝐴 /L 𝑛 ) ↑ ( 𝑛 pCnt 𝑁 ) ) , 1 ) ) ) ‘ ( abs ‘ ( 𝑁 · 𝑀 ) ) ) )
109 105 108 eqtr4d ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑀 ≠ 0 ∧ 𝑁 ≠ 0 ) ) → ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ if ( 𝑛 ∈ ℙ , ( ( 𝐴 /L 𝑛 ) ↑ ( 𝑛 pCnt 𝑁 ) ) , 1 ) ) ) ‘ ( abs ‘ 𝑁 ) ) = ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ if ( 𝑛 ∈ ℙ , ( ( 𝐴 /L 𝑛 ) ↑ ( 𝑛 pCnt 𝑁 ) ) , 1 ) ) ) ‘ ( abs ‘ ( 𝑀 · 𝑁 ) ) ) )
110 104 109 oveq12d ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑀 ≠ 0 ∧ 𝑁 ≠ 0 ) ) → ( ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ if ( 𝑛 ∈ ℙ , ( ( 𝐴 /L 𝑛 ) ↑ ( 𝑛 pCnt 𝑀 ) ) , 1 ) ) ) ‘ ( abs ‘ 𝑀 ) ) · ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ if ( 𝑛 ∈ ℙ , ( ( 𝐴 /L 𝑛 ) ↑ ( 𝑛 pCnt 𝑁 ) ) , 1 ) ) ) ‘ ( abs ‘ 𝑁 ) ) ) = ( ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ if ( 𝑛 ∈ ℙ , ( ( 𝐴 /L 𝑛 ) ↑ ( 𝑛 pCnt 𝑀 ) ) , 1 ) ) ) ‘ ( abs ‘ ( 𝑀 · 𝑁 ) ) ) · ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ if ( 𝑛 ∈ ℙ , ( ( 𝐴 /L 𝑛 ) ↑ ( 𝑛 pCnt 𝑁 ) ) , 1 ) ) ) ‘ ( abs ‘ ( 𝑀 · 𝑁 ) ) ) ) )
111 103 110 eqtr4d ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑀 ≠ 0 ∧ 𝑁 ≠ 0 ) ) → ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ if ( 𝑛 ∈ ℙ , ( ( 𝐴 /L 𝑛 ) ↑ ( 𝑛 pCnt ( 𝑀 · 𝑁 ) ) ) , 1 ) ) ) ‘ ( abs ‘ ( 𝑀 · 𝑁 ) ) ) = ( ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ if ( 𝑛 ∈ ℙ , ( ( 𝐴 /L 𝑛 ) ↑ ( 𝑛 pCnt 𝑀 ) ) , 1 ) ) ) ‘ ( abs ‘ 𝑀 ) ) · ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ if ( 𝑛 ∈ ℙ , ( ( 𝐴 /L 𝑛 ) ↑ ( 𝑛 pCnt 𝑁 ) ) , 1 ) ) ) ‘ ( abs ‘ 𝑁 ) ) ) )
112 14 111 oveq12d ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑀 ≠ 0 ∧ 𝑁 ≠ 0 ) ) → ( if ( ( ( 𝑀 · 𝑁 ) < 0 ∧ 𝐴 < 0 ) , - 1 , 1 ) · ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ if ( 𝑛 ∈ ℙ , ( ( 𝐴 /L 𝑛 ) ↑ ( 𝑛 pCnt ( 𝑀 · 𝑁 ) ) ) , 1 ) ) ) ‘ ( abs ‘ ( 𝑀 · 𝑁 ) ) ) ) = ( ( if ( ( 𝑀 < 0 ∧ 𝐴 < 0 ) , - 1 , 1 ) · if ( ( 𝑁 < 0 ∧ 𝐴 < 0 ) , - 1 , 1 ) ) · ( ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ if ( 𝑛 ∈ ℙ , ( ( 𝐴 /L 𝑛 ) ↑ ( 𝑛 pCnt 𝑀 ) ) , 1 ) ) ) ‘ ( abs ‘ 𝑀 ) ) · ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ if ( 𝑛 ∈ ℙ , ( ( 𝐴 /L 𝑛 ) ↑ ( 𝑛 pCnt 𝑁 ) ) , 1 ) ) ) ‘ ( abs ‘ 𝑁 ) ) ) ) )
113 97 lgsval4 ⊢ ( ( 𝐴 ∈ ℤ ∧ ( 𝑀 · 𝑁 ) ∈ ℤ ∧ ( 𝑀 · 𝑁 ) ≠ 0 ) → ( 𝐴 /L ( 𝑀 · 𝑁 ) ) = ( if ( ( ( 𝑀 · 𝑁 ) < 0 ∧ 𝐴 < 0 ) , - 1 , 1 ) · ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ if ( 𝑛 ∈ ℙ , ( ( 𝐴 /L 𝑛 ) ↑ ( 𝑛 pCnt ( 𝑀 · 𝑁 ) ) ) , 1 ) ) ) ‘ ( abs ‘ ( 𝑀 · 𝑁 ) ) ) ) )
114 27 17 22 113 syl3anc ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑀 ≠ 0 ∧ 𝑁 ≠ 0 ) ) → ( 𝐴 /L ( 𝑀 · 𝑁 ) ) = ( if ( ( ( 𝑀 · 𝑁 ) < 0 ∧ 𝐴 < 0 ) , - 1 , 1 ) · ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ if ( 𝑛 ∈ ℙ , ( ( 𝐴 /L 𝑛 ) ↑ ( 𝑛 pCnt ( 𝑀 · 𝑁 ) ) ) , 1 ) ) ) ‘ ( abs ‘ ( 𝑀 · 𝑁 ) ) ) ) )
115 28 lgsval4 ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑀 ≠ 0 ) → ( 𝐴 /L 𝑀 ) = ( if ( ( 𝑀 < 0 ∧ 𝐴 < 0 ) , - 1 , 1 ) · ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ if ( 𝑛 ∈ ℙ , ( ( 𝐴 /L 𝑛 ) ↑ ( 𝑛 pCnt 𝑀 ) ) , 1 ) ) ) ‘ ( abs ‘ 𝑀 ) ) ) )
116 27 15 20 115 syl3anc ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑀 ≠ 0 ∧ 𝑁 ≠ 0 ) ) → ( 𝐴 /L 𝑀 ) = ( if ( ( 𝑀 < 0 ∧ 𝐴 < 0 ) , - 1 , 1 ) · ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ if ( 𝑛 ∈ ℙ , ( ( 𝐴 /L 𝑛 ) ↑ ( 𝑛 pCnt 𝑀 ) ) , 1 ) ) ) ‘ ( abs ‘ 𝑀 ) ) ) )
117 35 lgsval4 ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) → ( 𝐴 /L 𝑁 ) = ( if ( ( 𝑁 < 0 ∧ 𝐴 < 0 ) , - 1 , 1 ) · ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ if ( 𝑛 ∈ ℙ , ( ( 𝐴 /L 𝑛 ) ↑ ( 𝑛 pCnt 𝑁 ) ) , 1 ) ) ) ‘ ( abs ‘ 𝑁 ) ) ) )
118 27 16 21 117 syl3anc ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑀 ≠ 0 ∧ 𝑁 ≠ 0 ) ) → ( 𝐴 /L 𝑁 ) = ( if ( ( 𝑁 < 0 ∧ 𝐴 < 0 ) , - 1 , 1 ) · ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ if ( 𝑛 ∈ ℙ , ( ( 𝐴 /L 𝑛 ) ↑ ( 𝑛 pCnt 𝑁 ) ) , 1 ) ) ) ‘ ( abs ‘ 𝑁 ) ) ) )
119 116 118 oveq12d ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑀 ≠ 0 ∧ 𝑁 ≠ 0 ) ) → ( ( 𝐴 /L 𝑀 ) · ( 𝐴 /L 𝑁 ) ) = ( ( if ( ( 𝑀 < 0 ∧ 𝐴 < 0 ) , - 1 , 1 ) · ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ if ( 𝑛 ∈ ℙ , ( ( 𝐴 /L 𝑛 ) ↑ ( 𝑛 pCnt 𝑀 ) ) , 1 ) ) ) ‘ ( abs ‘ 𝑀 ) ) ) · ( if ( ( 𝑁 < 0 ∧ 𝐴 < 0 ) , - 1 , 1 ) · ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ if ( 𝑛 ∈ ℙ , ( ( 𝐴 /L 𝑛 ) ↑ ( 𝑛 pCnt 𝑁 ) ) , 1 ) ) ) ‘ ( abs ‘ 𝑁 ) ) ) ) )
120 neg1cn ⊢ - 1 ∈ ℂ
121 ax-1cn ⊢ 1 ∈ ℂ
122 120 121 ifcli ⊢ if ( ( 𝑀 < 0 ∧ 𝐴 < 0 ) , - 1 , 1 ) ∈ ℂ
123 122 a1i ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑀 ≠ 0 ∧ 𝑁 ≠ 0 ) ) → if ( ( 𝑀 < 0 ∧ 𝐴 < 0 ) , - 1 , 1 ) ∈ ℂ )
124 nnabscl ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑀 ≠ 0 ) → ( abs ‘ 𝑀 ) ∈ ℕ )
125 15 20 124 syl2anc ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑀 ≠ 0 ∧ 𝑁 ≠ 0 ) ) → ( abs ‘ 𝑀 ) ∈ ℕ )
126 125 25 eleqtrdi ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑀 ≠ 0 ∧ 𝑁 ≠ 0 ) ) → ( abs ‘ 𝑀 ) ∈ ( ℤ≥ ‘ 1 ) )
127 elfznn ⊢ ( 𝑘 ∈ ( 1 ... ( abs ‘ 𝑀 ) ) → 𝑘 ∈ ℕ )
128 30 127 32 syl2an ⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑀 ≠ 0 ∧ 𝑁 ≠ 0 ) ) ∧ 𝑘 ∈ ( 1 ... ( abs ‘ 𝑀 ) ) ) → ( ( 𝑛 ∈ ℕ ↦ if ( 𝑛 ∈ ℙ , ( ( 𝐴 /L 𝑛 ) ↑ ( 𝑛 pCnt 𝑀 ) ) , 1 ) ) ‘ 𝑘 ) ∈ ℤ )
129 128 zcnd ⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑀 ≠ 0 ∧ 𝑁 ≠ 0 ) ) ∧ 𝑘 ∈ ( 1 ... ( abs ‘ 𝑀 ) ) ) → ( ( 𝑛 ∈ ℕ ↦ if ( 𝑛 ∈ ℙ , ( ( 𝐴 /L 𝑛 ) ↑ ( 𝑛 pCnt 𝑀 ) ) , 1 ) ) ‘ 𝑘 ) ∈ ℂ )
130 mulcl ⊢ ( ( 𝑘 ∈ ℂ ∧ 𝑥 ∈ ℂ ) → ( 𝑘 · 𝑥 ) ∈ ℂ )
131 130 adantl ⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑀 ≠ 0 ∧ 𝑁 ≠ 0 ) ) ∧ ( 𝑘 ∈ ℂ ∧ 𝑥 ∈ ℂ ) ) → ( 𝑘 · 𝑥 ) ∈ ℂ )
132 126 129 131 seqcl ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑀 ≠ 0 ∧ 𝑁 ≠ 0 ) ) → ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ if ( 𝑛 ∈ ℙ , ( ( 𝐴 /L 𝑛 ) ↑ ( 𝑛 pCnt 𝑀 ) ) , 1 ) ) ) ‘ ( abs ‘ 𝑀 ) ) ∈ ℂ )
133 120 121 ifcli ⊢ if ( ( 𝑁 < 0 ∧ 𝐴 < 0 ) , - 1 , 1 ) ∈ ℂ
134 133 a1i ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑀 ≠ 0 ∧ 𝑁 ≠ 0 ) ) → if ( ( 𝑁 < 0 ∧ 𝐴 < 0 ) , - 1 , 1 ) ∈ ℂ )
135 nnabscl ⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) → ( abs ‘ 𝑁 ) ∈ ℕ )
136 16 21 135 syl2anc ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑀 ≠ 0 ∧ 𝑁 ≠ 0 ) ) → ( abs ‘ 𝑁 ) ∈ ℕ )
137 136 25 eleqtrdi ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑀 ≠ 0 ∧ 𝑁 ≠ 0 ) ) → ( abs ‘ 𝑁 ) ∈ ( ℤ≥ ‘ 1 ) )
138 elfznn ⊢ ( 𝑘 ∈ ( 1 ... ( abs ‘ 𝑁 ) ) → 𝑘 ∈ ℕ )
139 37 138 38 syl2an ⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑀 ≠ 0 ∧ 𝑁 ≠ 0 ) ) ∧ 𝑘 ∈ ( 1 ... ( abs ‘ 𝑁 ) ) ) → ( ( 𝑛 ∈ ℕ ↦ if ( 𝑛 ∈ ℙ , ( ( 𝐴 /L 𝑛 ) ↑ ( 𝑛 pCnt 𝑁 ) ) , 1 ) ) ‘ 𝑘 ) ∈ ℤ )
140 139 zcnd ⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑀 ≠ 0 ∧ 𝑁 ≠ 0 ) ) ∧ 𝑘 ∈ ( 1 ... ( abs ‘ 𝑁 ) ) ) → ( ( 𝑛 ∈ ℕ ↦ if ( 𝑛 ∈ ℙ , ( ( 𝐴 /L 𝑛 ) ↑ ( 𝑛 pCnt 𝑁 ) ) , 1 ) ) ‘ 𝑘 ) ∈ ℂ )
141 137 140 131 seqcl ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑀 ≠ 0 ∧ 𝑁 ≠ 0 ) ) → ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ if ( 𝑛 ∈ ℙ , ( ( 𝐴 /L 𝑛 ) ↑ ( 𝑛 pCnt 𝑁 ) ) , 1 ) ) ) ‘ ( abs ‘ 𝑁 ) ) ∈ ℂ )
142 123 132 134 141 mul4d ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑀 ≠ 0 ∧ 𝑁 ≠ 0 ) ) → ( ( if ( ( 𝑀 < 0 ∧ 𝐴 < 0 ) , - 1 , 1 ) · ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ if ( 𝑛 ∈ ℙ , ( ( 𝐴 /L 𝑛 ) ↑ ( 𝑛 pCnt 𝑀 ) ) , 1 ) ) ) ‘ ( abs ‘ 𝑀 ) ) ) · ( if ( ( 𝑁 < 0 ∧ 𝐴 < 0 ) , - 1 , 1 ) · ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ if ( 𝑛 ∈ ℙ , ( ( 𝐴 /L 𝑛 ) ↑ ( 𝑛 pCnt 𝑁 ) ) , 1 ) ) ) ‘ ( abs ‘ 𝑁 ) ) ) ) = ( ( if ( ( 𝑀 < 0 ∧ 𝐴 < 0 ) , - 1 , 1 ) · if ( ( 𝑁 < 0 ∧ 𝐴 < 0 ) , - 1 , 1 ) ) · ( ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ if ( 𝑛 ∈ ℙ , ( ( 𝐴 /L 𝑛 ) ↑ ( 𝑛 pCnt 𝑀 ) ) , 1 ) ) ) ‘ ( abs ‘ 𝑀 ) ) · ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ if ( 𝑛 ∈ ℙ , ( ( 𝐴 /L 𝑛 ) ↑ ( 𝑛 pCnt 𝑁 ) ) , 1 ) ) ) ‘ ( abs ‘ 𝑁 ) ) ) ) )
143 119 142 eqtrd ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑀 ≠ 0 ∧ 𝑁 ≠ 0 ) ) → ( ( 𝐴 /L 𝑀 ) · ( 𝐴 /L 𝑁 ) ) = ( ( if ( ( 𝑀 < 0 ∧ 𝐴 < 0 ) , - 1 , 1 ) · if ( ( 𝑁 < 0 ∧ 𝐴 < 0 ) , - 1 , 1 ) ) · ( ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ if ( 𝑛 ∈ ℙ , ( ( 𝐴 /L 𝑛 ) ↑ ( 𝑛 pCnt 𝑀 ) ) , 1 ) ) ) ‘ ( abs ‘ 𝑀 ) ) · ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ if ( 𝑛 ∈ ℙ , ( ( 𝐴 /L 𝑛 ) ↑ ( 𝑛 pCnt 𝑁 ) ) , 1 ) ) ) ‘ ( abs ‘ 𝑁 ) ) ) ) )
144 112 114 143 3eqtr4d ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑀 ≠ 0 ∧ 𝑁 ≠ 0 ) ) → ( 𝐴 /L ( 𝑀 · 𝑁 ) ) = ( ( 𝐴 /L 𝑀 ) · ( 𝐴 /L 𝑁 ) ) )