# 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 ${⊢}\left(\left({A}\in ℤ\wedge {M}\in ℤ\wedge {N}\in ℤ\right)\wedge \left({M}\ne 0\wedge {N}\ne 0\right)\right)\to {A}{/}_{L}{M}\cdot {N}=\left({A}{/}_{L}{M}\right)\left({A}{/}_{L}{N}\right)$

### Proof

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