Metamath Proof Explorer

Theorem lgsdir

Description: The Legendre symbol is completely multiplicative in its left argument. Generalization of theorem 9.9(a) in ApostolNT p. 188 (which assumes that A and B are odd positive integers). Together with lgsqr this implies that the product of two quadratic residues or nonresidues is a residue, and the product of a residue and a nonresidue is a nonresidue. (Contributed by Mario Carneiro, 4-Feb-2015)

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

Proof

Step Hyp Ref Expression
1 ax-1cn ⊢ 1 ∈ ℂ
2 0cn ⊢ 0 ∈ ℂ
3 1 2 ifcli ⊢ if ( ( 𝐵 ↑ 2 ) = 1 , 1 , 0 ) ∈ ℂ
4 3 mulid2i ⊢ ( 1 · if ( ( 𝐵 ↑ 2 ) = 1 , 1 , 0 ) ) = if ( ( 𝐵 ↑ 2 ) = 1 , 1 , 0 )
5 iftrue ⊢ ( ( 𝐴 ↑ 2 ) = 1 → if ( ( 𝐴 ↑ 2 ) = 1 , 1 , 0 ) = 1 )
6 5 adantl ⊢ ( ( ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐴 ≠ 0 ∧ 𝐵 ≠ 0 ) ) ∧ 𝑁 = 0 ) ∧ ( 𝐴 ↑ 2 ) = 1 ) → if ( ( 𝐴 ↑ 2 ) = 1 , 1 , 0 ) = 1 )
7 6 oveq1d ⊢ ( ( ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐴 ≠ 0 ∧ 𝐵 ≠ 0 ) ) ∧ 𝑁 = 0 ) ∧ ( 𝐴 ↑ 2 ) = 1 ) → ( if ( ( 𝐴 ↑ 2 ) = 1 , 1 , 0 ) · if ( ( 𝐵 ↑ 2 ) = 1 , 1 , 0 ) ) = ( 1 · if ( ( 𝐵 ↑ 2 ) = 1 , 1 , 0 ) ) )
8 simpl1 ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐴 ≠ 0 ∧ 𝐵 ≠ 0 ) ) → 𝐴 ∈ ℤ )
9 8 zcnd ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐴 ≠ 0 ∧ 𝐵 ≠ 0 ) ) → 𝐴 ∈ ℂ )
10 9 ad2antrr ⊢ ( ( ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐴 ≠ 0 ∧ 𝐵 ≠ 0 ) ) ∧ 𝑁 = 0 ) ∧ ( 𝐴 ↑ 2 ) = 1 ) → 𝐴 ∈ ℂ )
11 simpl2 ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐴 ≠ 0 ∧ 𝐵 ≠ 0 ) ) → 𝐵 ∈ ℤ )
12 11 zcnd ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐴 ≠ 0 ∧ 𝐵 ≠ 0 ) ) → 𝐵 ∈ ℂ )
13 12 ad2antrr ⊢ ( ( ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐴 ≠ 0 ∧ 𝐵 ≠ 0 ) ) ∧ 𝑁 = 0 ) ∧ ( 𝐴 ↑ 2 ) = 1 ) → 𝐵 ∈ ℂ )
14 10 13 sqmuld ⊢ ( ( ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐴 ≠ 0 ∧ 𝐵 ≠ 0 ) ) ∧ 𝑁 = 0 ) ∧ ( 𝐴 ↑ 2 ) = 1 ) → ( ( 𝐴 · 𝐵 ) ↑ 2 ) = ( ( 𝐴 ↑ 2 ) · ( 𝐵 ↑ 2 ) ) )
15 simpr ⊢ ( ( ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐴 ≠ 0 ∧ 𝐵 ≠ 0 ) ) ∧ 𝑁 = 0 ) ∧ ( 𝐴 ↑ 2 ) = 1 ) → ( 𝐴 ↑ 2 ) = 1 )
16 15 oveq1d ⊢ ( ( ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐴 ≠ 0 ∧ 𝐵 ≠ 0 ) ) ∧ 𝑁 = 0 ) ∧ ( 𝐴 ↑ 2 ) = 1 ) → ( ( 𝐴 ↑ 2 ) · ( 𝐵 ↑ 2 ) ) = ( 1 · ( 𝐵 ↑ 2 ) ) )
17 12 sqcld ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐴 ≠ 0 ∧ 𝐵 ≠ 0 ) ) → ( 𝐵 ↑ 2 ) ∈ ℂ )
18 17 ad2antrr ⊢ ( ( ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐴 ≠ 0 ∧ 𝐵 ≠ 0 ) ) ∧ 𝑁 = 0 ) ∧ ( 𝐴 ↑ 2 ) = 1 ) → ( 𝐵 ↑ 2 ) ∈ ℂ )
19 18 mulid2d ⊢ ( ( ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐴 ≠ 0 ∧ 𝐵 ≠ 0 ) ) ∧ 𝑁 = 0 ) ∧ ( 𝐴 ↑ 2 ) = 1 ) → ( 1 · ( 𝐵 ↑ 2 ) ) = ( 𝐵 ↑ 2 ) )
20 14 16 19 3eqtrd ⊢ ( ( ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐴 ≠ 0 ∧ 𝐵 ≠ 0 ) ) ∧ 𝑁 = 0 ) ∧ ( 𝐴 ↑ 2 ) = 1 ) → ( ( 𝐴 · 𝐵 ) ↑ 2 ) = ( 𝐵 ↑ 2 ) )
21 20 eqeq1d ⊢ ( ( ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐴 ≠ 0 ∧ 𝐵 ≠ 0 ) ) ∧ 𝑁 = 0 ) ∧ ( 𝐴 ↑ 2 ) = 1 ) → ( ( ( 𝐴 · 𝐵 ) ↑ 2 ) = 1 ↔ ( 𝐵 ↑ 2 ) = 1 ) )
22 21 ifbid ⊢ ( ( ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐴 ≠ 0 ∧ 𝐵 ≠ 0 ) ) ∧ 𝑁 = 0 ) ∧ ( 𝐴 ↑ 2 ) = 1 ) → if ( ( ( 𝐴 · 𝐵 ) ↑ 2 ) = 1 , 1 , 0 ) = if ( ( 𝐵 ↑ 2 ) = 1 , 1 , 0 ) )
23 4 7 22 3eqtr4a ⊢ ( ( ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐴 ≠ 0 ∧ 𝐵 ≠ 0 ) ) ∧ 𝑁 = 0 ) ∧ ( 𝐴 ↑ 2 ) = 1 ) → ( if ( ( 𝐴 ↑ 2 ) = 1 , 1 , 0 ) · if ( ( 𝐵 ↑ 2 ) = 1 , 1 , 0 ) ) = if ( ( ( 𝐴 · 𝐵 ) ↑ 2 ) = 1 , 1 , 0 ) )
24 3 mul02i ⊢ ( 0 · if ( ( 𝐵 ↑ 2 ) = 1 , 1 , 0 ) ) = 0
25 iffalse ⊢ ( ¬ ( 𝐴 ↑ 2 ) = 1 → if ( ( 𝐴 ↑ 2 ) = 1 , 1 , 0 ) = 0 )
26 25 adantl ⊢ ( ( ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐴 ≠ 0 ∧ 𝐵 ≠ 0 ) ) ∧ 𝑁 = 0 ) ∧ ¬ ( 𝐴 ↑ 2 ) = 1 ) → if ( ( 𝐴 ↑ 2 ) = 1 , 1 , 0 ) = 0 )
27 26 oveq1d ⊢ ( ( ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐴 ≠ 0 ∧ 𝐵 ≠ 0 ) ) ∧ 𝑁 = 0 ) ∧ ¬ ( 𝐴 ↑ 2 ) = 1 ) → ( if ( ( 𝐴 ↑ 2 ) = 1 , 1 , 0 ) · if ( ( 𝐵 ↑ 2 ) = 1 , 1 , 0 ) ) = ( 0 · if ( ( 𝐵 ↑ 2 ) = 1 , 1 , 0 ) ) )
28 dvdsmul1 ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → 𝐴 ∥ ( 𝐴 · 𝐵 ) )
29 8 11 28 syl2anc ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐴 ≠ 0 ∧ 𝐵 ≠ 0 ) ) → 𝐴 ∥ ( 𝐴 · 𝐵 ) )
30 8 11 zmulcld ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐴 ≠ 0 ∧ 𝐵 ≠ 0 ) ) → ( 𝐴 · 𝐵 ) ∈ ℤ )
31 dvdssq ⊢ ( ( 𝐴 ∈ ℤ ∧ ( 𝐴 · 𝐵 ) ∈ ℤ ) → ( 𝐴 ∥ ( 𝐴 · 𝐵 ) ↔ ( 𝐴 ↑ 2 ) ∥ ( ( 𝐴 · 𝐵 ) ↑ 2 ) ) )
32 8 30 31 syl2anc ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐴 ≠ 0 ∧ 𝐵 ≠ 0 ) ) → ( 𝐴 ∥ ( 𝐴 · 𝐵 ) ↔ ( 𝐴 ↑ 2 ) ∥ ( ( 𝐴 · 𝐵 ) ↑ 2 ) ) )
33 29 32 mpbid ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐴 ≠ 0 ∧ 𝐵 ≠ 0 ) ) → ( 𝐴 ↑ 2 ) ∥ ( ( 𝐴 · 𝐵 ) ↑ 2 ) )
34 33 adantr ⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐴 ≠ 0 ∧ 𝐵 ≠ 0 ) ) ∧ 𝑁 = 0 ) → ( 𝐴 ↑ 2 ) ∥ ( ( 𝐴 · 𝐵 ) ↑ 2 ) )
35 breq2 ⊢ ( ( ( 𝐴 · 𝐵 ) ↑ 2 ) = 1 → ( ( 𝐴 ↑ 2 ) ∥ ( ( 𝐴 · 𝐵 ) ↑ 2 ) ↔ ( 𝐴 ↑ 2 ) ∥ 1 ) )
36 34 35 syl5ibcom ⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐴 ≠ 0 ∧ 𝐵 ≠ 0 ) ) ∧ 𝑁 = 0 ) → ( ( ( 𝐴 · 𝐵 ) ↑ 2 ) = 1 → ( 𝐴 ↑ 2 ) ∥ 1 ) )
37 simprl ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐴 ≠ 0 ∧ 𝐵 ≠ 0 ) ) → 𝐴 ≠ 0 )
38 37 neneqd ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐴 ≠ 0 ∧ 𝐵 ≠ 0 ) ) → ¬ 𝐴 = 0 )
39 sqeq0 ⊢ ( 𝐴 ∈ ℂ → ( ( 𝐴 ↑ 2 ) = 0 ↔ 𝐴 = 0 ) )
40 9 39 syl ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐴 ≠ 0 ∧ 𝐵 ≠ 0 ) ) → ( ( 𝐴 ↑ 2 ) = 0 ↔ 𝐴 = 0 ) )
41 38 40 mtbird ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐴 ≠ 0 ∧ 𝐵 ≠ 0 ) ) → ¬ ( 𝐴 ↑ 2 ) = 0 )
42 zsqcl2 ⊢ ( 𝐴 ∈ ℤ → ( 𝐴 ↑ 2 ) ∈ ℕ0 )
43 8 42 syl ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐴 ≠ 0 ∧ 𝐵 ≠ 0 ) ) → ( 𝐴 ↑ 2 ) ∈ ℕ0 )
44 elnn0 ⊢ ( ( 𝐴 ↑ 2 ) ∈ ℕ0 ↔ ( ( 𝐴 ↑ 2 ) ∈ ℕ ∨ ( 𝐴 ↑ 2 ) = 0 ) )
45 43 44 sylib ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐴 ≠ 0 ∧ 𝐵 ≠ 0 ) ) → ( ( 𝐴 ↑ 2 ) ∈ ℕ ∨ ( 𝐴 ↑ 2 ) = 0 ) )
46 45 ord ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐴 ≠ 0 ∧ 𝐵 ≠ 0 ) ) → ( ¬ ( 𝐴 ↑ 2 ) ∈ ℕ → ( 𝐴 ↑ 2 ) = 0 ) )
47 41 46 mt3d ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐴 ≠ 0 ∧ 𝐵 ≠ 0 ) ) → ( 𝐴 ↑ 2 ) ∈ ℕ )
48 47 adantr ⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐴 ≠ 0 ∧ 𝐵 ≠ 0 ) ) ∧ 𝑁 = 0 ) → ( 𝐴 ↑ 2 ) ∈ ℕ )
49 48 nnzd ⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐴 ≠ 0 ∧ 𝐵 ≠ 0 ) ) ∧ 𝑁 = 0 ) → ( 𝐴 ↑ 2 ) ∈ ℤ )
50 1nn ⊢ 1 ∈ ℕ
51 dvdsle ⊢ ( ( ( 𝐴 ↑ 2 ) ∈ ℤ ∧ 1 ∈ ℕ ) → ( ( 𝐴 ↑ 2 ) ∥ 1 → ( 𝐴 ↑ 2 ) ≤ 1 ) )
52 49 50 51 sylancl ⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐴 ≠ 0 ∧ 𝐵 ≠ 0 ) ) ∧ 𝑁 = 0 ) → ( ( 𝐴 ↑ 2 ) ∥ 1 → ( 𝐴 ↑ 2 ) ≤ 1 ) )
53 48 nnge1d ⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐴 ≠ 0 ∧ 𝐵 ≠ 0 ) ) ∧ 𝑁 = 0 ) → 1 ≤ ( 𝐴 ↑ 2 ) )
54 52 53 jctird ⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐴 ≠ 0 ∧ 𝐵 ≠ 0 ) ) ∧ 𝑁 = 0 ) → ( ( 𝐴 ↑ 2 ) ∥ 1 → ( ( 𝐴 ↑ 2 ) ≤ 1 ∧ 1 ≤ ( 𝐴 ↑ 2 ) ) ) )
55 48 nnred ⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐴 ≠ 0 ∧ 𝐵 ≠ 0 ) ) ∧ 𝑁 = 0 ) → ( 𝐴 ↑ 2 ) ∈ ℝ )
56 1re ⊢ 1 ∈ ℝ
57 letri3 ⊢ ( ( ( 𝐴 ↑ 2 ) ∈ ℝ ∧ 1 ∈ ℝ ) → ( ( 𝐴 ↑ 2 ) = 1 ↔ ( ( 𝐴 ↑ 2 ) ≤ 1 ∧ 1 ≤ ( 𝐴 ↑ 2 ) ) ) )
58 55 56 57 sylancl ⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐴 ≠ 0 ∧ 𝐵 ≠ 0 ) ) ∧ 𝑁 = 0 ) → ( ( 𝐴 ↑ 2 ) = 1 ↔ ( ( 𝐴 ↑ 2 ) ≤ 1 ∧ 1 ≤ ( 𝐴 ↑ 2 ) ) ) )
59 54 58 sylibrd ⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐴 ≠ 0 ∧ 𝐵 ≠ 0 ) ) ∧ 𝑁 = 0 ) → ( ( 𝐴 ↑ 2 ) ∥ 1 → ( 𝐴 ↑ 2 ) = 1 ) )
60 36 59 syld ⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐴 ≠ 0 ∧ 𝐵 ≠ 0 ) ) ∧ 𝑁 = 0 ) → ( ( ( 𝐴 · 𝐵 ) ↑ 2 ) = 1 → ( 𝐴 ↑ 2 ) = 1 ) )
61 60 con3dimp ⊢ ( ( ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐴 ≠ 0 ∧ 𝐵 ≠ 0 ) ) ∧ 𝑁 = 0 ) ∧ ¬ ( 𝐴 ↑ 2 ) = 1 ) → ¬ ( ( 𝐴 · 𝐵 ) ↑ 2 ) = 1 )
62 61 iffalsed ⊢ ( ( ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐴 ≠ 0 ∧ 𝐵 ≠ 0 ) ) ∧ 𝑁 = 0 ) ∧ ¬ ( 𝐴 ↑ 2 ) = 1 ) → if ( ( ( 𝐴 · 𝐵 ) ↑ 2 ) = 1 , 1 , 0 ) = 0 )
63 24 27 62 3eqtr4a ⊢ ( ( ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐴 ≠ 0 ∧ 𝐵 ≠ 0 ) ) ∧ 𝑁 = 0 ) ∧ ¬ ( 𝐴 ↑ 2 ) = 1 ) → ( if ( ( 𝐴 ↑ 2 ) = 1 , 1 , 0 ) · if ( ( 𝐵 ↑ 2 ) = 1 , 1 , 0 ) ) = if ( ( ( 𝐴 · 𝐵 ) ↑ 2 ) = 1 , 1 , 0 ) )
64 23 63 pm2.61dan ⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐴 ≠ 0 ∧ 𝐵 ≠ 0 ) ) ∧ 𝑁 = 0 ) → ( if ( ( 𝐴 ↑ 2 ) = 1 , 1 , 0 ) · if ( ( 𝐵 ↑ 2 ) = 1 , 1 , 0 ) ) = if ( ( ( 𝐴 · 𝐵 ) ↑ 2 ) = 1 , 1 , 0 ) )
65 oveq2 ⊢ ( 𝑁 = 0 → ( 𝐴 /L 𝑁 ) = ( 𝐴 /L 0 ) )
66 lgs0 ⊢ ( 𝐴 ∈ ℤ → ( 𝐴 /L 0 ) = if ( ( 𝐴 ↑ 2 ) = 1 , 1 , 0 ) )
67 8 66 syl ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐴 ≠ 0 ∧ 𝐵 ≠ 0 ) ) → ( 𝐴 /L 0 ) = if ( ( 𝐴 ↑ 2 ) = 1 , 1 , 0 ) )
68 65 67 sylan9eqr ⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐴 ≠ 0 ∧ 𝐵 ≠ 0 ) ) ∧ 𝑁 = 0 ) → ( 𝐴 /L 𝑁 ) = if ( ( 𝐴 ↑ 2 ) = 1 , 1 , 0 ) )
69 oveq2 ⊢ ( 𝑁 = 0 → ( 𝐵 /L 𝑁 ) = ( 𝐵 /L 0 ) )
70 lgs0 ⊢ ( 𝐵 ∈ ℤ → ( 𝐵 /L 0 ) = if ( ( 𝐵 ↑ 2 ) = 1 , 1 , 0 ) )
71 11 70 syl ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐴 ≠ 0 ∧ 𝐵 ≠ 0 ) ) → ( 𝐵 /L 0 ) = if ( ( 𝐵 ↑ 2 ) = 1 , 1 , 0 ) )
72 69 71 sylan9eqr ⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐴 ≠ 0 ∧ 𝐵 ≠ 0 ) ) ∧ 𝑁 = 0 ) → ( 𝐵 /L 𝑁 ) = if ( ( 𝐵 ↑ 2 ) = 1 , 1 , 0 ) )
73 68 72 oveq12d ⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐴 ≠ 0 ∧ 𝐵 ≠ 0 ) ) ∧ 𝑁 = 0 ) → ( ( 𝐴 /L 𝑁 ) · ( 𝐵 /L 𝑁 ) ) = ( if ( ( 𝐴 ↑ 2 ) = 1 , 1 , 0 ) · if ( ( 𝐵 ↑ 2 ) = 1 , 1 , 0 ) ) )
74 oveq2 ⊢ ( 𝑁 = 0 → ( ( 𝐴 · 𝐵 ) /L 𝑁 ) = ( ( 𝐴 · 𝐵 ) /L 0 ) )
75 lgs0 ⊢ ( ( 𝐴 · 𝐵 ) ∈ ℤ → ( ( 𝐴 · 𝐵 ) /L 0 ) = if ( ( ( 𝐴 · 𝐵 ) ↑ 2 ) = 1 , 1 , 0 ) )
76 30 75 syl ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐴 ≠ 0 ∧ 𝐵 ≠ 0 ) ) → ( ( 𝐴 · 𝐵 ) /L 0 ) = if ( ( ( 𝐴 · 𝐵 ) ↑ 2 ) = 1 , 1 , 0 ) )
77 74 76 sylan9eqr ⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐴 ≠ 0 ∧ 𝐵 ≠ 0 ) ) ∧ 𝑁 = 0 ) → ( ( 𝐴 · 𝐵 ) /L 𝑁 ) = if ( ( ( 𝐴 · 𝐵 ) ↑ 2 ) = 1 , 1 , 0 ) )
78 64 73 77 3eqtr4rd ⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐴 ≠ 0 ∧ 𝐵 ≠ 0 ) ) ∧ 𝑁 = 0 ) → ( ( 𝐴 · 𝐵 ) /L 𝑁 ) = ( ( 𝐴 /L 𝑁 ) · ( 𝐵 /L 𝑁 ) ) )
79 lgsdilem ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐴 ≠ 0 ∧ 𝐵 ≠ 0 ) ) → if ( ( 𝑁 < 0 ∧ ( 𝐴 · 𝐵 ) < 0 ) , - 1 , 1 ) = ( if ( ( 𝑁 < 0 ∧ 𝐴 < 0 ) , - 1 , 1 ) · if ( ( 𝑁 < 0 ∧ 𝐵 < 0 ) , - 1 , 1 ) ) )
80 79 adantr ⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐴 ≠ 0 ∧ 𝐵 ≠ 0 ) ) ∧ 𝑁 ≠ 0 ) → if ( ( 𝑁 < 0 ∧ ( 𝐴 · 𝐵 ) < 0 ) , - 1 , 1 ) = ( if ( ( 𝑁 < 0 ∧ 𝐴 < 0 ) , - 1 , 1 ) · if ( ( 𝑁 < 0 ∧ 𝐵 < 0 ) , - 1 , 1 ) ) )
81 simpl3 ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐴 ≠ 0 ∧ 𝐵 ≠ 0 ) ) → 𝑁 ∈ ℤ )
82 nnabscl ⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) → ( abs ‘ 𝑁 ) ∈ ℕ )
83 81 82 sylan ⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐴 ≠ 0 ∧ 𝐵 ≠ 0 ) ) ∧ 𝑁 ≠ 0 ) → ( abs ‘ 𝑁 ) ∈ ℕ )
84 nnuz ⊢ ℕ = ( ℤ≥ ‘ 1 )
85 83 84 eleqtrdi ⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐴 ≠ 0 ∧ 𝐵 ≠ 0 ) ) ∧ 𝑁 ≠ 0 ) → ( abs ‘ 𝑁 ) ∈ ( ℤ≥ ‘ 1 ) )
86 simpll1 ⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐴 ≠ 0 ∧ 𝐵 ≠ 0 ) ) ∧ 𝑁 ≠ 0 ) → 𝐴 ∈ ℤ )
87 simpll3 ⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐴 ≠ 0 ∧ 𝐵 ≠ 0 ) ) ∧ 𝑁 ≠ 0 ) → 𝑁 ∈ ℤ )
88 simpr ⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐴 ≠ 0 ∧ 𝐵 ≠ 0 ) ) ∧ 𝑁 ≠ 0 ) → 𝑁 ≠ 0 )
89 eqid ⊢ ( 𝑛 ∈ ℕ ↦ if ( 𝑛 ∈ ℙ , ( ( 𝐴 /L 𝑛 ) ↑ ( 𝑛 pCnt 𝑁 ) ) , 1 ) ) = ( 𝑛 ∈ ℕ ↦ if ( 𝑛 ∈ ℙ , ( ( 𝐴 /L 𝑛 ) ↑ ( 𝑛 pCnt 𝑁 ) ) , 1 ) )
90 89 lgsfcl3 ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) → ( 𝑛 ∈ ℕ ↦ if ( 𝑛 ∈ ℙ , ( ( 𝐴 /L 𝑛 ) ↑ ( 𝑛 pCnt 𝑁 ) ) , 1 ) ) : ℕ ⟶ ℤ )
91 86 87 88 90 syl3anc ⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐴 ≠ 0 ∧ 𝐵 ≠ 0 ) ) ∧ 𝑁 ≠ 0 ) → ( 𝑛 ∈ ℕ ↦ if ( 𝑛 ∈ ℙ , ( ( 𝐴 /L 𝑛 ) ↑ ( 𝑛 pCnt 𝑁 ) ) , 1 ) ) : ℕ ⟶ ℤ )
92 elfznn ⊢ ( 𝑘 ∈ ( 1 ... ( abs ‘ 𝑁 ) ) → 𝑘 ∈ ℕ )
93 ffvelrn ⊢ ( ( ( 𝑛 ∈ ℕ ↦ if ( 𝑛 ∈ ℙ , ( ( 𝐴 /L 𝑛 ) ↑ ( 𝑛 pCnt 𝑁 ) ) , 1 ) ) : ℕ ⟶ ℤ ∧ 𝑘 ∈ ℕ ) → ( ( 𝑛 ∈ ℕ ↦ if ( 𝑛 ∈ ℙ , ( ( 𝐴 /L 𝑛 ) ↑ ( 𝑛 pCnt 𝑁 ) ) , 1 ) ) ‘ 𝑘 ) ∈ ℤ )
94 91 92 93 syl2an ⊢ ( ( ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐴 ≠ 0 ∧ 𝐵 ≠ 0 ) ) ∧ 𝑁 ≠ 0 ) ∧ 𝑘 ∈ ( 1 ... ( abs ‘ 𝑁 ) ) ) → ( ( 𝑛 ∈ ℕ ↦ if ( 𝑛 ∈ ℙ , ( ( 𝐴 /L 𝑛 ) ↑ ( 𝑛 pCnt 𝑁 ) ) , 1 ) ) ‘ 𝑘 ) ∈ ℤ )
95 94 zcnd ⊢ ( ( ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐴 ≠ 0 ∧ 𝐵 ≠ 0 ) ) ∧ 𝑁 ≠ 0 ) ∧ 𝑘 ∈ ( 1 ... ( abs ‘ 𝑁 ) ) ) → ( ( 𝑛 ∈ ℕ ↦ if ( 𝑛 ∈ ℙ , ( ( 𝐴 /L 𝑛 ) ↑ ( 𝑛 pCnt 𝑁 ) ) , 1 ) ) ‘ 𝑘 ) ∈ ℂ )
96 simpll2 ⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐴 ≠ 0 ∧ 𝐵 ≠ 0 ) ) ∧ 𝑁 ≠ 0 ) → 𝐵 ∈ ℤ )
97 eqid ⊢ ( 𝑛 ∈ ℕ ↦ if ( 𝑛 ∈ ℙ , ( ( 𝐵 /L 𝑛 ) ↑ ( 𝑛 pCnt 𝑁 ) ) , 1 ) ) = ( 𝑛 ∈ ℕ ↦ if ( 𝑛 ∈ ℙ , ( ( 𝐵 /L 𝑛 ) ↑ ( 𝑛 pCnt 𝑁 ) ) , 1 ) )
98 97 lgsfcl3 ⊢ ( ( 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) → ( 𝑛 ∈ ℕ ↦ if ( 𝑛 ∈ ℙ , ( ( 𝐵 /L 𝑛 ) ↑ ( 𝑛 pCnt 𝑁 ) ) , 1 ) ) : ℕ ⟶ ℤ )
99 96 87 88 98 syl3anc ⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐴 ≠ 0 ∧ 𝐵 ≠ 0 ) ) ∧ 𝑁 ≠ 0 ) → ( 𝑛 ∈ ℕ ↦ if ( 𝑛 ∈ ℙ , ( ( 𝐵 /L 𝑛 ) ↑ ( 𝑛 pCnt 𝑁 ) ) , 1 ) ) : ℕ ⟶ ℤ )
100 ffvelrn ⊢ ( ( ( 𝑛 ∈ ℕ ↦ if ( 𝑛 ∈ ℙ , ( ( 𝐵 /L 𝑛 ) ↑ ( 𝑛 pCnt 𝑁 ) ) , 1 ) ) : ℕ ⟶ ℤ ∧ 𝑘 ∈ ℕ ) → ( ( 𝑛 ∈ ℕ ↦ if ( 𝑛 ∈ ℙ , ( ( 𝐵 /L 𝑛 ) ↑ ( 𝑛 pCnt 𝑁 ) ) , 1 ) ) ‘ 𝑘 ) ∈ ℤ )
101 99 92 100 syl2an ⊢ ( ( ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐴 ≠ 0 ∧ 𝐵 ≠ 0 ) ) ∧ 𝑁 ≠ 0 ) ∧ 𝑘 ∈ ( 1 ... ( abs ‘ 𝑁 ) ) ) → ( ( 𝑛 ∈ ℕ ↦ if ( 𝑛 ∈ ℙ , ( ( 𝐵 /L 𝑛 ) ↑ ( 𝑛 pCnt 𝑁 ) ) , 1 ) ) ‘ 𝑘 ) ∈ ℤ )
102 101 zcnd ⊢ ( ( ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐴 ≠ 0 ∧ 𝐵 ≠ 0 ) ) ∧ 𝑁 ≠ 0 ) ∧ 𝑘 ∈ ( 1 ... ( abs ‘ 𝑁 ) ) ) → ( ( 𝑛 ∈ ℕ ↦ if ( 𝑛 ∈ ℙ , ( ( 𝐵 /L 𝑛 ) ↑ ( 𝑛 pCnt 𝑁 ) ) , 1 ) ) ‘ 𝑘 ) ∈ ℂ )
103 86 adantr ⊢ ( ( ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐴 ≠ 0 ∧ 𝐵 ≠ 0 ) ) ∧ 𝑁 ≠ 0 ) ∧ 𝑘 ∈ ℙ ) → 𝐴 ∈ ℤ )
104 96 adantr ⊢ ( ( ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐴 ≠ 0 ∧ 𝐵 ≠ 0 ) ) ∧ 𝑁 ≠ 0 ) ∧ 𝑘 ∈ ℙ ) → 𝐵 ∈ ℤ )
105 simpr ⊢ ( ( ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐴 ≠ 0 ∧ 𝐵 ≠ 0 ) ) ∧ 𝑁 ≠ 0 ) ∧ 𝑘 ∈ ℙ ) → 𝑘 ∈ ℙ )
106 lgsdirprm ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑘 ∈ ℙ ) → ( ( 𝐴 · 𝐵 ) /L 𝑘 ) = ( ( 𝐴 /L 𝑘 ) · ( 𝐵 /L 𝑘 ) ) )
107 103 104 105 106 syl3anc ⊢ ( ( ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐴 ≠ 0 ∧ 𝐵 ≠ 0 ) ) ∧ 𝑁 ≠ 0 ) ∧ 𝑘 ∈ ℙ ) → ( ( 𝐴 · 𝐵 ) /L 𝑘 ) = ( ( 𝐴 /L 𝑘 ) · ( 𝐵 /L 𝑘 ) ) )
108 107 oveq1d ⊢ ( ( ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐴 ≠ 0 ∧ 𝐵 ≠ 0 ) ) ∧ 𝑁 ≠ 0 ) ∧ 𝑘 ∈ ℙ ) → ( ( ( 𝐴 · 𝐵 ) /L 𝑘 ) ↑ ( 𝑘 pCnt 𝑁 ) ) = ( ( ( 𝐴 /L 𝑘 ) · ( 𝐵 /L 𝑘 ) ) ↑ ( 𝑘 pCnt 𝑁 ) ) )
109 prmz ⊢ ( 𝑘 ∈ ℙ → 𝑘 ∈ ℤ )
110 lgscl ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑘 ∈ ℤ ) → ( 𝐴 /L 𝑘 ) ∈ ℤ )
111 86 109 110 syl2an ⊢ ( ( ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐴 ≠ 0 ∧ 𝐵 ≠ 0 ) ) ∧ 𝑁 ≠ 0 ) ∧ 𝑘 ∈ ℙ ) → ( 𝐴 /L 𝑘 ) ∈ ℤ )
112 111 zcnd ⊢ ( ( ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐴 ≠ 0 ∧ 𝐵 ≠ 0 ) ) ∧ 𝑁 ≠ 0 ) ∧ 𝑘 ∈ ℙ ) → ( 𝐴 /L 𝑘 ) ∈ ℂ )
113 lgscl ⊢ ( ( 𝐵 ∈ ℤ ∧ 𝑘 ∈ ℤ ) → ( 𝐵 /L 𝑘 ) ∈ ℤ )
114 96 109 113 syl2an ⊢ ( ( ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐴 ≠ 0 ∧ 𝐵 ≠ 0 ) ) ∧ 𝑁 ≠ 0 ) ∧ 𝑘 ∈ ℙ ) → ( 𝐵 /L 𝑘 ) ∈ ℤ )
115 114 zcnd ⊢ ( ( ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐴 ≠ 0 ∧ 𝐵 ≠ 0 ) ) ∧ 𝑁 ≠ 0 ) ∧ 𝑘 ∈ ℙ ) → ( 𝐵 /L 𝑘 ) ∈ ℂ )
116 87 adantr ⊢ ( ( ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐴 ≠ 0 ∧ 𝐵 ≠ 0 ) ) ∧ 𝑁 ≠ 0 ) ∧ 𝑘 ∈ ℙ ) → 𝑁 ∈ ℤ )
117 88 adantr ⊢ ( ( ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐴 ≠ 0 ∧ 𝐵 ≠ 0 ) ) ∧ 𝑁 ≠ 0 ) ∧ 𝑘 ∈ ℙ ) → 𝑁 ≠ 0 )
118 pczcl ⊢ ( ( 𝑘 ∈ ℙ ∧ ( 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) ) → ( 𝑘 pCnt 𝑁 ) ∈ ℕ0 )
119 105 116 117 118 syl12anc ⊢ ( ( ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐴 ≠ 0 ∧ 𝐵 ≠ 0 ) ) ∧ 𝑁 ≠ 0 ) ∧ 𝑘 ∈ ℙ ) → ( 𝑘 pCnt 𝑁 ) ∈ ℕ0 )
120 112 115 119 mulexpd ⊢ ( ( ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐴 ≠ 0 ∧ 𝐵 ≠ 0 ) ) ∧ 𝑁 ≠ 0 ) ∧ 𝑘 ∈ ℙ ) → ( ( ( 𝐴 /L 𝑘 ) · ( 𝐵 /L 𝑘 ) ) ↑ ( 𝑘 pCnt 𝑁 ) ) = ( ( ( 𝐴 /L 𝑘 ) ↑ ( 𝑘 pCnt 𝑁 ) ) · ( ( 𝐵 /L 𝑘 ) ↑ ( 𝑘 pCnt 𝑁 ) ) ) )
121 108 120 eqtrd ⊢ ( ( ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐴 ≠ 0 ∧ 𝐵 ≠ 0 ) ) ∧ 𝑁 ≠ 0 ) ∧ 𝑘 ∈ ℙ ) → ( ( ( 𝐴 · 𝐵 ) /L 𝑘 ) ↑ ( 𝑘 pCnt 𝑁 ) ) = ( ( ( 𝐴 /L 𝑘 ) ↑ ( 𝑘 pCnt 𝑁 ) ) · ( ( 𝐵 /L 𝑘 ) ↑ ( 𝑘 pCnt 𝑁 ) ) ) )
122 iftrue ⊢ ( 𝑘 ∈ ℙ → if ( 𝑘 ∈ ℙ , ( ( ( 𝐴 · 𝐵 ) /L 𝑘 ) ↑ ( 𝑘 pCnt 𝑁 ) ) , 1 ) = ( ( ( 𝐴 · 𝐵 ) /L 𝑘 ) ↑ ( 𝑘 pCnt 𝑁 ) ) )
123 122 adantl ⊢ ( ( ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐴 ≠ 0 ∧ 𝐵 ≠ 0 ) ) ∧ 𝑁 ≠ 0 ) ∧ 𝑘 ∈ ℙ ) → if ( 𝑘 ∈ ℙ , ( ( ( 𝐴 · 𝐵 ) /L 𝑘 ) ↑ ( 𝑘 pCnt 𝑁 ) ) , 1 ) = ( ( ( 𝐴 · 𝐵 ) /L 𝑘 ) ↑ ( 𝑘 pCnt 𝑁 ) ) )
124 iftrue ⊢ ( 𝑘 ∈ ℙ → if ( 𝑘 ∈ ℙ , ( ( 𝐴 /L 𝑘 ) ↑ ( 𝑘 pCnt 𝑁 ) ) , 1 ) = ( ( 𝐴 /L 𝑘 ) ↑ ( 𝑘 pCnt 𝑁 ) ) )
125 iftrue ⊢ ( 𝑘 ∈ ℙ → if ( 𝑘 ∈ ℙ , ( ( 𝐵 /L 𝑘 ) ↑ ( 𝑘 pCnt 𝑁 ) ) , 1 ) = ( ( 𝐵 /L 𝑘 ) ↑ ( 𝑘 pCnt 𝑁 ) ) )
126 124 125 oveq12d ⊢ ( 𝑘 ∈ ℙ → ( if ( 𝑘 ∈ ℙ , ( ( 𝐴 /L 𝑘 ) ↑ ( 𝑘 pCnt 𝑁 ) ) , 1 ) · if ( 𝑘 ∈ ℙ , ( ( 𝐵 /L 𝑘 ) ↑ ( 𝑘 pCnt 𝑁 ) ) , 1 ) ) = ( ( ( 𝐴 /L 𝑘 ) ↑ ( 𝑘 pCnt 𝑁 ) ) · ( ( 𝐵 /L 𝑘 ) ↑ ( 𝑘 pCnt 𝑁 ) ) ) )
127 126 adantl ⊢ ( ( ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐴 ≠ 0 ∧ 𝐵 ≠ 0 ) ) ∧ 𝑁 ≠ 0 ) ∧ 𝑘 ∈ ℙ ) → ( if ( 𝑘 ∈ ℙ , ( ( 𝐴 /L 𝑘 ) ↑ ( 𝑘 pCnt 𝑁 ) ) , 1 ) · if ( 𝑘 ∈ ℙ , ( ( 𝐵 /L 𝑘 ) ↑ ( 𝑘 pCnt 𝑁 ) ) , 1 ) ) = ( ( ( 𝐴 /L 𝑘 ) ↑ ( 𝑘 pCnt 𝑁 ) ) · ( ( 𝐵 /L 𝑘 ) ↑ ( 𝑘 pCnt 𝑁 ) ) ) )
128 121 123 127 3eqtr4d ⊢ ( ( ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐴 ≠ 0 ∧ 𝐵 ≠ 0 ) ) ∧ 𝑁 ≠ 0 ) ∧ 𝑘 ∈ ℙ ) → if ( 𝑘 ∈ ℙ , ( ( ( 𝐴 · 𝐵 ) /L 𝑘 ) ↑ ( 𝑘 pCnt 𝑁 ) ) , 1 ) = ( if ( 𝑘 ∈ ℙ , ( ( 𝐴 /L 𝑘 ) ↑ ( 𝑘 pCnt 𝑁 ) ) , 1 ) · if ( 𝑘 ∈ ℙ , ( ( 𝐵 /L 𝑘 ) ↑ ( 𝑘 pCnt 𝑁 ) ) , 1 ) ) )
129 1t1e1 ⊢ ( 1 · 1 ) = 1
130 129 eqcomi ⊢ 1 = ( 1 · 1 )
131 iffalse ⊢ ( ¬ 𝑘 ∈ ℙ → if ( 𝑘 ∈ ℙ , ( ( ( 𝐴 · 𝐵 ) /L 𝑘 ) ↑ ( 𝑘 pCnt 𝑁 ) ) , 1 ) = 1 )
132 iffalse ⊢ ( ¬ 𝑘 ∈ ℙ → if ( 𝑘 ∈ ℙ , ( ( 𝐴 /L 𝑘 ) ↑ ( 𝑘 pCnt 𝑁 ) ) , 1 ) = 1 )
133 iffalse ⊢ ( ¬ 𝑘 ∈ ℙ → if ( 𝑘 ∈ ℙ , ( ( 𝐵 /L 𝑘 ) ↑ ( 𝑘 pCnt 𝑁 ) ) , 1 ) = 1 )
134 132 133 oveq12d ⊢ ( ¬ 𝑘 ∈ ℙ → ( if ( 𝑘 ∈ ℙ , ( ( 𝐴 /L 𝑘 ) ↑ ( 𝑘 pCnt 𝑁 ) ) , 1 ) · if ( 𝑘 ∈ ℙ , ( ( 𝐵 /L 𝑘 ) ↑ ( 𝑘 pCnt 𝑁 ) ) , 1 ) ) = ( 1 · 1 ) )
135 130 131 134 3eqtr4a ⊢ ( ¬ 𝑘 ∈ ℙ → if ( 𝑘 ∈ ℙ , ( ( ( 𝐴 · 𝐵 ) /L 𝑘 ) ↑ ( 𝑘 pCnt 𝑁 ) ) , 1 ) = ( if ( 𝑘 ∈ ℙ , ( ( 𝐴 /L 𝑘 ) ↑ ( 𝑘 pCnt 𝑁 ) ) , 1 ) · if ( 𝑘 ∈ ℙ , ( ( 𝐵 /L 𝑘 ) ↑ ( 𝑘 pCnt 𝑁 ) ) , 1 ) ) )
136 135 adantl ⊢ ( ( ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐴 ≠ 0 ∧ 𝐵 ≠ 0 ) ) ∧ 𝑁 ≠ 0 ) ∧ ¬ 𝑘 ∈ ℙ ) → if ( 𝑘 ∈ ℙ , ( ( ( 𝐴 · 𝐵 ) /L 𝑘 ) ↑ ( 𝑘 pCnt 𝑁 ) ) , 1 ) = ( if ( 𝑘 ∈ ℙ , ( ( 𝐴 /L 𝑘 ) ↑ ( 𝑘 pCnt 𝑁 ) ) , 1 ) · if ( 𝑘 ∈ ℙ , ( ( 𝐵 /L 𝑘 ) ↑ ( 𝑘 pCnt 𝑁 ) ) , 1 ) ) )
137 128 136 pm2.61dan ⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐴 ≠ 0 ∧ 𝐵 ≠ 0 ) ) ∧ 𝑁 ≠ 0 ) → if ( 𝑘 ∈ ℙ , ( ( ( 𝐴 · 𝐵 ) /L 𝑘 ) ↑ ( 𝑘 pCnt 𝑁 ) ) , 1 ) = ( if ( 𝑘 ∈ ℙ , ( ( 𝐴 /L 𝑘 ) ↑ ( 𝑘 pCnt 𝑁 ) ) , 1 ) · if ( 𝑘 ∈ ℙ , ( ( 𝐵 /L 𝑘 ) ↑ ( 𝑘 pCnt 𝑁 ) ) , 1 ) ) )
138 137 adantr ⊢ ( ( ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐴 ≠ 0 ∧ 𝐵 ≠ 0 ) ) ∧ 𝑁 ≠ 0 ) ∧ 𝑘 ∈ ( 1 ... ( abs ‘ 𝑁 ) ) ) → if ( 𝑘 ∈ ℙ , ( ( ( 𝐴 · 𝐵 ) /L 𝑘 ) ↑ ( 𝑘 pCnt 𝑁 ) ) , 1 ) = ( if ( 𝑘 ∈ ℙ , ( ( 𝐴 /L 𝑘 ) ↑ ( 𝑘 pCnt 𝑁 ) ) , 1 ) · if ( 𝑘 ∈ ℙ , ( ( 𝐵 /L 𝑘 ) ↑ ( 𝑘 pCnt 𝑁 ) ) , 1 ) ) )
139 92 adantl ⊢ ( ( ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐴 ≠ 0 ∧ 𝐵 ≠ 0 ) ) ∧ 𝑁 ≠ 0 ) ∧ 𝑘 ∈ ( 1 ... ( abs ‘ 𝑁 ) ) ) → 𝑘 ∈ ℕ )
140 eleq1w ⊢ ( 𝑛 = 𝑘 → ( 𝑛 ∈ ℙ ↔ 𝑘 ∈ ℙ ) )
141 oveq2 ⊢ ( 𝑛 = 𝑘 → ( ( 𝐴 · 𝐵 ) /L 𝑛 ) = ( ( 𝐴 · 𝐵 ) /L 𝑘 ) )
142 oveq1 ⊢ ( 𝑛 = 𝑘 → ( 𝑛 pCnt 𝑁 ) = ( 𝑘 pCnt 𝑁 ) )
143 141 142 oveq12d ⊢ ( 𝑛 = 𝑘 → ( ( ( 𝐴 · 𝐵 ) /L 𝑛 ) ↑ ( 𝑛 pCnt 𝑁 ) ) = ( ( ( 𝐴 · 𝐵 ) /L 𝑘 ) ↑ ( 𝑘 pCnt 𝑁 ) ) )
144 140 143 ifbieq1d ⊢ ( 𝑛 = 𝑘 → if ( 𝑛 ∈ ℙ , ( ( ( 𝐴 · 𝐵 ) /L 𝑛 ) ↑ ( 𝑛 pCnt 𝑁 ) ) , 1 ) = if ( 𝑘 ∈ ℙ , ( ( ( 𝐴 · 𝐵 ) /L 𝑘 ) ↑ ( 𝑘 pCnt 𝑁 ) ) , 1 ) )
145 eqid ⊢ ( 𝑛 ∈ ℕ ↦ if ( 𝑛 ∈ ℙ , ( ( ( 𝐴 · 𝐵 ) /L 𝑛 ) ↑ ( 𝑛 pCnt 𝑁 ) ) , 1 ) ) = ( 𝑛 ∈ ℕ ↦ if ( 𝑛 ∈ ℙ , ( ( ( 𝐴 · 𝐵 ) /L 𝑛 ) ↑ ( 𝑛 pCnt 𝑁 ) ) , 1 ) )
146 ovex ⊢ ( ( ( 𝐴 · 𝐵 ) /L 𝑘 ) ↑ ( 𝑘 pCnt 𝑁 ) ) ∈ V
147 1ex ⊢ 1 ∈ V
148 146 147 ifex ⊢ if ( 𝑘 ∈ ℙ , ( ( ( 𝐴 · 𝐵 ) /L 𝑘 ) ↑ ( 𝑘 pCnt 𝑁 ) ) , 1 ) ∈ V
149 144 145 148 fvmpt ⊢ ( 𝑘 ∈ ℕ → ( ( 𝑛 ∈ ℕ ↦ if ( 𝑛 ∈ ℙ , ( ( ( 𝐴 · 𝐵 ) /L 𝑛 ) ↑ ( 𝑛 pCnt 𝑁 ) ) , 1 ) ) ‘ 𝑘 ) = if ( 𝑘 ∈ ℙ , ( ( ( 𝐴 · 𝐵 ) /L 𝑘 ) ↑ ( 𝑘 pCnt 𝑁 ) ) , 1 ) )
150 139 149 syl ⊢ ( ( ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐴 ≠ 0 ∧ 𝐵 ≠ 0 ) ) ∧ 𝑁 ≠ 0 ) ∧ 𝑘 ∈ ( 1 ... ( abs ‘ 𝑁 ) ) ) → ( ( 𝑛 ∈ ℕ ↦ if ( 𝑛 ∈ ℙ , ( ( ( 𝐴 · 𝐵 ) /L 𝑛 ) ↑ ( 𝑛 pCnt 𝑁 ) ) , 1 ) ) ‘ 𝑘 ) = if ( 𝑘 ∈ ℙ , ( ( ( 𝐴 · 𝐵 ) /L 𝑘 ) ↑ ( 𝑘 pCnt 𝑁 ) ) , 1 ) )
151 oveq2 ⊢ ( 𝑛 = 𝑘 → ( 𝐴 /L 𝑛 ) = ( 𝐴 /L 𝑘 ) )
152 151 142 oveq12d ⊢ ( 𝑛 = 𝑘 → ( ( 𝐴 /L 𝑛 ) ↑ ( 𝑛 pCnt 𝑁 ) ) = ( ( 𝐴 /L 𝑘 ) ↑ ( 𝑘 pCnt 𝑁 ) ) )
153 140 152 ifbieq1d ⊢ ( 𝑛 = 𝑘 → if ( 𝑛 ∈ ℙ , ( ( 𝐴 /L 𝑛 ) ↑ ( 𝑛 pCnt 𝑁 ) ) , 1 ) = if ( 𝑘 ∈ ℙ , ( ( 𝐴 /L 𝑘 ) ↑ ( 𝑘 pCnt 𝑁 ) ) , 1 ) )
154 ovex ⊢ ( ( 𝐴 /L 𝑘 ) ↑ ( 𝑘 pCnt 𝑁 ) ) ∈ V
155 154 147 ifex ⊢ if ( 𝑘 ∈ ℙ , ( ( 𝐴 /L 𝑘 ) ↑ ( 𝑘 pCnt 𝑁 ) ) , 1 ) ∈ V
156 153 89 155 fvmpt ⊢ ( 𝑘 ∈ ℕ → ( ( 𝑛 ∈ ℕ ↦ if ( 𝑛 ∈ ℙ , ( ( 𝐴 /L 𝑛 ) ↑ ( 𝑛 pCnt 𝑁 ) ) , 1 ) ) ‘ 𝑘 ) = if ( 𝑘 ∈ ℙ , ( ( 𝐴 /L 𝑘 ) ↑ ( 𝑘 pCnt 𝑁 ) ) , 1 ) )
157 139 156 syl ⊢ ( ( ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐴 ≠ 0 ∧ 𝐵 ≠ 0 ) ) ∧ 𝑁 ≠ 0 ) ∧ 𝑘 ∈ ( 1 ... ( abs ‘ 𝑁 ) ) ) → ( ( 𝑛 ∈ ℕ ↦ if ( 𝑛 ∈ ℙ , ( ( 𝐴 /L 𝑛 ) ↑ ( 𝑛 pCnt 𝑁 ) ) , 1 ) ) ‘ 𝑘 ) = if ( 𝑘 ∈ ℙ , ( ( 𝐴 /L 𝑘 ) ↑ ( 𝑘 pCnt 𝑁 ) ) , 1 ) )
158 oveq2 ⊢ ( 𝑛 = 𝑘 → ( 𝐵 /L 𝑛 ) = ( 𝐵 /L 𝑘 ) )
159 158 142 oveq12d ⊢ ( 𝑛 = 𝑘 → ( ( 𝐵 /L 𝑛 ) ↑ ( 𝑛 pCnt 𝑁 ) ) = ( ( 𝐵 /L 𝑘 ) ↑ ( 𝑘 pCnt 𝑁 ) ) )
160 140 159 ifbieq1d ⊢ ( 𝑛 = 𝑘 → if ( 𝑛 ∈ ℙ , ( ( 𝐵 /L 𝑛 ) ↑ ( 𝑛 pCnt 𝑁 ) ) , 1 ) = if ( 𝑘 ∈ ℙ , ( ( 𝐵 /L 𝑘 ) ↑ ( 𝑘 pCnt 𝑁 ) ) , 1 ) )
161 ovex ⊢ ( ( 𝐵 /L 𝑘 ) ↑ ( 𝑘 pCnt 𝑁 ) ) ∈ V
162 161 147 ifex ⊢ if ( 𝑘 ∈ ℙ , ( ( 𝐵 /L 𝑘 ) ↑ ( 𝑘 pCnt 𝑁 ) ) , 1 ) ∈ V
163 160 97 162 fvmpt ⊢ ( 𝑘 ∈ ℕ → ( ( 𝑛 ∈ ℕ ↦ if ( 𝑛 ∈ ℙ , ( ( 𝐵 /L 𝑛 ) ↑ ( 𝑛 pCnt 𝑁 ) ) , 1 ) ) ‘ 𝑘 ) = if ( 𝑘 ∈ ℙ , ( ( 𝐵 /L 𝑘 ) ↑ ( 𝑘 pCnt 𝑁 ) ) , 1 ) )
164 139 163 syl ⊢ ( ( ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐴 ≠ 0 ∧ 𝐵 ≠ 0 ) ) ∧ 𝑁 ≠ 0 ) ∧ 𝑘 ∈ ( 1 ... ( abs ‘ 𝑁 ) ) ) → ( ( 𝑛 ∈ ℕ ↦ if ( 𝑛 ∈ ℙ , ( ( 𝐵 /L 𝑛 ) ↑ ( 𝑛 pCnt 𝑁 ) ) , 1 ) ) ‘ 𝑘 ) = if ( 𝑘 ∈ ℙ , ( ( 𝐵 /L 𝑘 ) ↑ ( 𝑘 pCnt 𝑁 ) ) , 1 ) )
165 157 164 oveq12d ⊢ ( ( ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐴 ≠ 0 ∧ 𝐵 ≠ 0 ) ) ∧ 𝑁 ≠ 0 ) ∧ 𝑘 ∈ ( 1 ... ( abs ‘ 𝑁 ) ) ) → ( ( ( 𝑛 ∈ ℕ ↦ if ( 𝑛 ∈ ℙ , ( ( 𝐴 /L 𝑛 ) ↑ ( 𝑛 pCnt 𝑁 ) ) , 1 ) ) ‘ 𝑘 ) · ( ( 𝑛 ∈ ℕ ↦ if ( 𝑛 ∈ ℙ , ( ( 𝐵 /L 𝑛 ) ↑ ( 𝑛 pCnt 𝑁 ) ) , 1 ) ) ‘ 𝑘 ) ) = ( if ( 𝑘 ∈ ℙ , ( ( 𝐴 /L 𝑘 ) ↑ ( 𝑘 pCnt 𝑁 ) ) , 1 ) · if ( 𝑘 ∈ ℙ , ( ( 𝐵 /L 𝑘 ) ↑ ( 𝑘 pCnt 𝑁 ) ) , 1 ) ) )
166 138 150 165 3eqtr4d ⊢ ( ( ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐴 ≠ 0 ∧ 𝐵 ≠ 0 ) ) ∧ 𝑁 ≠ 0 ) ∧ 𝑘 ∈ ( 1 ... ( abs ‘ 𝑁 ) ) ) → ( ( 𝑛 ∈ ℕ ↦ if ( 𝑛 ∈ ℙ , ( ( ( 𝐴 · 𝐵 ) /L 𝑛 ) ↑ ( 𝑛 pCnt 𝑁 ) ) , 1 ) ) ‘ 𝑘 ) = ( ( ( 𝑛 ∈ ℕ ↦ if ( 𝑛 ∈ ℙ , ( ( 𝐴 /L 𝑛 ) ↑ ( 𝑛 pCnt 𝑁 ) ) , 1 ) ) ‘ 𝑘 ) · ( ( 𝑛 ∈ ℕ ↦ if ( 𝑛 ∈ ℙ , ( ( 𝐵 /L 𝑛 ) ↑ ( 𝑛 pCnt 𝑁 ) ) , 1 ) ) ‘ 𝑘 ) ) )
167 85 95 102 166 prodfmul ⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐴 ≠ 0 ∧ 𝐵 ≠ 0 ) ) ∧ 𝑁 ≠ 0 ) → ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ if ( 𝑛 ∈ ℙ , ( ( ( 𝐴 · 𝐵 ) /L 𝑛 ) ↑ ( 𝑛 pCnt 𝑁 ) ) , 1 ) ) ) ‘ ( abs ‘ 𝑁 ) ) = ( ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ if ( 𝑛 ∈ ℙ , ( ( 𝐴 /L 𝑛 ) ↑ ( 𝑛 pCnt 𝑁 ) ) , 1 ) ) ) ‘ ( abs ‘ 𝑁 ) ) · ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ if ( 𝑛 ∈ ℙ , ( ( 𝐵 /L 𝑛 ) ↑ ( 𝑛 pCnt 𝑁 ) ) , 1 ) ) ) ‘ ( abs ‘ 𝑁 ) ) ) )
168 80 167 oveq12d ⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐴 ≠ 0 ∧ 𝐵 ≠ 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 ‘ 𝑁 ) ) ) ) )
169 30 adantr ⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐴 ≠ 0 ∧ 𝐵 ≠ 0 ) ) ∧ 𝑁 ≠ 0 ) → ( 𝐴 · 𝐵 ) ∈ ℤ )
170 145 lgsval4 ⊢ ( ( ( 𝐴 · 𝐵 ) ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) → ( ( 𝐴 · 𝐵 ) /L 𝑁 ) = ( if ( ( 𝑁 < 0 ∧ ( 𝐴 · 𝐵 ) < 0 ) , - 1 , 1 ) · ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ if ( 𝑛 ∈ ℙ , ( ( ( 𝐴 · 𝐵 ) /L 𝑛 ) ↑ ( 𝑛 pCnt 𝑁 ) ) , 1 ) ) ) ‘ ( abs ‘ 𝑁 ) ) ) )
171 169 87 88 170 syl3anc ⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐴 ≠ 0 ∧ 𝐵 ≠ 0 ) ) ∧ 𝑁 ≠ 0 ) → ( ( 𝐴 · 𝐵 ) /L 𝑁 ) = ( if ( ( 𝑁 < 0 ∧ ( 𝐴 · 𝐵 ) < 0 ) , - 1 , 1 ) · ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ if ( 𝑛 ∈ ℙ , ( ( ( 𝐴 · 𝐵 ) /L 𝑛 ) ↑ ( 𝑛 pCnt 𝑁 ) ) , 1 ) ) ) ‘ ( abs ‘ 𝑁 ) ) ) )
172 89 lgsval4 ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) → ( 𝐴 /L 𝑁 ) = ( if ( ( 𝑁 < 0 ∧ 𝐴 < 0 ) , - 1 , 1 ) · ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ if ( 𝑛 ∈ ℙ , ( ( 𝐴 /L 𝑛 ) ↑ ( 𝑛 pCnt 𝑁 ) ) , 1 ) ) ) ‘ ( abs ‘ 𝑁 ) ) ) )
173 86 87 88 172 syl3anc ⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐴 ≠ 0 ∧ 𝐵 ≠ 0 ) ) ∧ 𝑁 ≠ 0 ) → ( 𝐴 /L 𝑁 ) = ( if ( ( 𝑁 < 0 ∧ 𝐴 < 0 ) , - 1 , 1 ) · ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ if ( 𝑛 ∈ ℙ , ( ( 𝐴 /L 𝑛 ) ↑ ( 𝑛 pCnt 𝑁 ) ) , 1 ) ) ) ‘ ( abs ‘ 𝑁 ) ) ) )
174 97 lgsval4 ⊢ ( ( 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) → ( 𝐵 /L 𝑁 ) = ( if ( ( 𝑁 < 0 ∧ 𝐵 < 0 ) , - 1 , 1 ) · ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ if ( 𝑛 ∈ ℙ , ( ( 𝐵 /L 𝑛 ) ↑ ( 𝑛 pCnt 𝑁 ) ) , 1 ) ) ) ‘ ( abs ‘ 𝑁 ) ) ) )
175 96 87 88 174 syl3anc ⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐴 ≠ 0 ∧ 𝐵 ≠ 0 ) ) ∧ 𝑁 ≠ 0 ) → ( 𝐵 /L 𝑁 ) = ( if ( ( 𝑁 < 0 ∧ 𝐵 < 0 ) , - 1 , 1 ) · ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ if ( 𝑛 ∈ ℙ , ( ( 𝐵 /L 𝑛 ) ↑ ( 𝑛 pCnt 𝑁 ) ) , 1 ) ) ) ‘ ( abs ‘ 𝑁 ) ) ) )
176 173 175 oveq12d ⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐴 ≠ 0 ∧ 𝐵 ≠ 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 ‘ 𝑁 ) ) ) ) )
177 neg1cn ⊢ - 1 ∈ ℂ
178 177 1 ifcli ⊢ if ( ( 𝑁 < 0 ∧ 𝐴 < 0 ) , - 1 , 1 ) ∈ ℂ
179 178 a1i ⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐴 ≠ 0 ∧ 𝐵 ≠ 0 ) ) ∧ 𝑁 ≠ 0 ) → if ( ( 𝑁 < 0 ∧ 𝐴 < 0 ) , - 1 , 1 ) ∈ ℂ )
180 mulcl ⊢ ( ( 𝑘 ∈ ℂ ∧ 𝑥 ∈ ℂ ) → ( 𝑘 · 𝑥 ) ∈ ℂ )
181 180 adantl ⊢ ( ( ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐴 ≠ 0 ∧ 𝐵 ≠ 0 ) ) ∧ 𝑁 ≠ 0 ) ∧ ( 𝑘 ∈ ℂ ∧ 𝑥 ∈ ℂ ) ) → ( 𝑘 · 𝑥 ) ∈ ℂ )
182 85 95 181 seqcl ⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐴 ≠ 0 ∧ 𝐵 ≠ 0 ) ) ∧ 𝑁 ≠ 0 ) → ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ if ( 𝑛 ∈ ℙ , ( ( 𝐴 /L 𝑛 ) ↑ ( 𝑛 pCnt 𝑁 ) ) , 1 ) ) ) ‘ ( abs ‘ 𝑁 ) ) ∈ ℂ )
183 177 1 ifcli ⊢ if ( ( 𝑁 < 0 ∧ 𝐵 < 0 ) , - 1 , 1 ) ∈ ℂ
184 183 a1i ⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐴 ≠ 0 ∧ 𝐵 ≠ 0 ) ) ∧ 𝑁 ≠ 0 ) → if ( ( 𝑁 < 0 ∧ 𝐵 < 0 ) , - 1 , 1 ) ∈ ℂ )
185 85 102 181 seqcl ⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐴 ≠ 0 ∧ 𝐵 ≠ 0 ) ) ∧ 𝑁 ≠ 0 ) → ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ if ( 𝑛 ∈ ℙ , ( ( 𝐵 /L 𝑛 ) ↑ ( 𝑛 pCnt 𝑁 ) ) , 1 ) ) ) ‘ ( abs ‘ 𝑁 ) ) ∈ ℂ )
186 179 182 184 185 mul4d ⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐴 ≠ 0 ∧ 𝐵 ≠ 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 ‘ 𝑁 ) ) ) ) )
187 176 186 eqtrd ⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐴 ≠ 0 ∧ 𝐵 ≠ 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 ‘ 𝑁 ) ) ) ) )
188 168 171 187 3eqtr4d ⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐴 ≠ 0 ∧ 𝐵 ≠ 0 ) ) ∧ 𝑁 ≠ 0 ) → ( ( 𝐴 · 𝐵 ) /L 𝑁 ) = ( ( 𝐴 /L 𝑁 ) · ( 𝐵 /L 𝑁 ) ) )
189 78 188 pm2.61dane ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐴 ≠ 0 ∧ 𝐵 ≠ 0 ) ) → ( ( 𝐴 · 𝐵 ) /L 𝑁 ) = ( ( 𝐴 /L 𝑁 ) · ( 𝐵 /L 𝑁 ) ) )