Metamath Proof Explorer

Theorem lgsdirprm

Description: The Legendre symbol is completely multiplicative at the primes. See theorem 9.3 in ApostolNT p. 180. (Contributed by Mario Carneiro, 4-Feb-2015) (Proof shortened by AV, 18-Mar-2022)

Ref Expression
Assertion lgsdirprm ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑃 ∈ ℙ ) → ( ( 𝐴 · 𝐵 ) /L 𝑃 ) = ( ( 𝐴 /L 𝑃 ) · ( 𝐵 /L 𝑃 ) ) )

Proof

Step Hyp Ref Expression
1 simpl1 ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑃 ∈ ℙ ) ∧ 𝑃 = 2 ) → 𝐴 ∈ ℤ )
2 simpl2 ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑃 ∈ ℙ ) ∧ 𝑃 = 2 ) → 𝐵 ∈ ℤ )
3 lgsdir2 ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → ( ( 𝐴 · 𝐵 ) /L 2 ) = ( ( 𝐴 /L 2 ) · ( 𝐵 /L 2 ) ) )
4 1 2 3 syl2anc ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑃 ∈ ℙ ) ∧ 𝑃 = 2 ) → ( ( 𝐴 · 𝐵 ) /L 2 ) = ( ( 𝐴 /L 2 ) · ( 𝐵 /L 2 ) ) )
5 simpr ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑃 ∈ ℙ ) ∧ 𝑃 = 2 ) → 𝑃 = 2 )
6 5 oveq2d ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑃 ∈ ℙ ) ∧ 𝑃 = 2 ) → ( ( 𝐴 · 𝐵 ) /L 𝑃 ) = ( ( 𝐴 · 𝐵 ) /L 2 ) )
7 5 oveq2d ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑃 ∈ ℙ ) ∧ 𝑃 = 2 ) → ( 𝐴 /L 𝑃 ) = ( 𝐴 /L 2 ) )
8 5 oveq2d ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑃 ∈ ℙ ) ∧ 𝑃 = 2 ) → ( 𝐵 /L 𝑃 ) = ( 𝐵 /L 2 ) )
9 7 8 oveq12d ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑃 ∈ ℙ ) ∧ 𝑃 = 2 ) → ( ( 𝐴 /L 𝑃 ) · ( 𝐵 /L 𝑃 ) ) = ( ( 𝐴 /L 2 ) · ( 𝐵 /L 2 ) ) )
10 4 6 9 3eqtr4d ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑃 ∈ ℙ ) ∧ 𝑃 = 2 ) → ( ( 𝐴 · 𝐵 ) /L 𝑃 ) = ( ( 𝐴 /L 𝑃 ) · ( 𝐵 /L 𝑃 ) ) )
11 simpl1 ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑃 ∈ ℙ ) ∧ 𝑃 ≠ 2 ) → 𝐴 ∈ ℤ )
12 simpl2 ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑃 ∈ ℙ ) ∧ 𝑃 ≠ 2 ) → 𝐵 ∈ ℤ )
13 11 12 zmulcld ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑃 ∈ ℙ ) ∧ 𝑃 ≠ 2 ) → ( 𝐴 · 𝐵 ) ∈ ℤ )
14 simpl3 ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑃 ∈ ℙ ) ∧ 𝑃 ≠ 2 ) → 𝑃 ∈ ℙ )
15 prmz ⊢ ( 𝑃 ∈ ℙ → 𝑃 ∈ ℤ )
16 14 15 syl ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑃 ∈ ℙ ) ∧ 𝑃 ≠ 2 ) → 𝑃 ∈ ℤ )
17 lgscl ⊢ ( ( ( 𝐴 · 𝐵 ) ∈ ℤ ∧ 𝑃 ∈ ℤ ) → ( ( 𝐴 · 𝐵 ) /L 𝑃 ) ∈ ℤ )
18 13 16 17 syl2anc ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑃 ∈ ℙ ) ∧ 𝑃 ≠ 2 ) → ( ( 𝐴 · 𝐵 ) /L 𝑃 ) ∈ ℤ )
19 18 zcnd ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑃 ∈ ℙ ) ∧ 𝑃 ≠ 2 ) → ( ( 𝐴 · 𝐵 ) /L 𝑃 ) ∈ ℂ )
20 lgscl ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑃 ∈ ℤ ) → ( 𝐴 /L 𝑃 ) ∈ ℤ )
21 11 16 20 syl2anc ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑃 ∈ ℙ ) ∧ 𝑃 ≠ 2 ) → ( 𝐴 /L 𝑃 ) ∈ ℤ )
22 lgscl ⊢ ( ( 𝐵 ∈ ℤ ∧ 𝑃 ∈ ℤ ) → ( 𝐵 /L 𝑃 ) ∈ ℤ )
23 12 16 22 syl2anc ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑃 ∈ ℙ ) ∧ 𝑃 ≠ 2 ) → ( 𝐵 /L 𝑃 ) ∈ ℤ )
24 21 23 zmulcld ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑃 ∈ ℙ ) ∧ 𝑃 ≠ 2 ) → ( ( 𝐴 /L 𝑃 ) · ( 𝐵 /L 𝑃 ) ) ∈ ℤ )
25 24 zcnd ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑃 ∈ ℙ ) ∧ 𝑃 ≠ 2 ) → ( ( 𝐴 /L 𝑃 ) · ( 𝐵 /L 𝑃 ) ) ∈ ℂ )
26 19 25 subcld ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑃 ∈ ℙ ) ∧ 𝑃 ≠ 2 ) → ( ( ( 𝐴 · 𝐵 ) /L 𝑃 ) − ( ( 𝐴 /L 𝑃 ) · ( 𝐵 /L 𝑃 ) ) ) ∈ ℂ )
27 26 abscld ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑃 ∈ ℙ ) ∧ 𝑃 ≠ 2 ) → ( abs ‘ ( ( ( 𝐴 · 𝐵 ) /L 𝑃 ) − ( ( 𝐴 /L 𝑃 ) · ( 𝐵 /L 𝑃 ) ) ) ) ∈ ℝ )
28 prmnn ⊢ ( 𝑃 ∈ ℙ → 𝑃 ∈ ℕ )
29 14 28 syl ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑃 ∈ ℙ ) ∧ 𝑃 ≠ 2 ) → 𝑃 ∈ ℕ )
30 29 nnrpd ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑃 ∈ ℙ ) ∧ 𝑃 ≠ 2 ) → 𝑃 ∈ ℝ+ )
31 26 absge0d ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑃 ∈ ℙ ) ∧ 𝑃 ≠ 2 ) → 0 ≤ ( abs ‘ ( ( ( 𝐴 · 𝐵 ) /L 𝑃 ) − ( ( 𝐴 /L 𝑃 ) · ( 𝐵 /L 𝑃 ) ) ) ) )
32 2re ⊢ 2 ∈ ℝ
33 32 a1i ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑃 ∈ ℙ ) ∧ 𝑃 ≠ 2 ) → 2 ∈ ℝ )
34 29 nnred ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑃 ∈ ℙ ) ∧ 𝑃 ≠ 2 ) → 𝑃 ∈ ℝ )
35 19 abscld ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑃 ∈ ℙ ) ∧ 𝑃 ≠ 2 ) → ( abs ‘ ( ( 𝐴 · 𝐵 ) /L 𝑃 ) ) ∈ ℝ )
36 25 abscld ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑃 ∈ ℙ ) ∧ 𝑃 ≠ 2 ) → ( abs ‘ ( ( 𝐴 /L 𝑃 ) · ( 𝐵 /L 𝑃 ) ) ) ∈ ℝ )
37 35 36 readdcld ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑃 ∈ ℙ ) ∧ 𝑃 ≠ 2 ) → ( ( abs ‘ ( ( 𝐴 · 𝐵 ) /L 𝑃 ) ) + ( abs ‘ ( ( 𝐴 /L 𝑃 ) · ( 𝐵 /L 𝑃 ) ) ) ) ∈ ℝ )
38 19 25 abs2dif2d ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑃 ∈ ℙ ) ∧ 𝑃 ≠ 2 ) → ( abs ‘ ( ( ( 𝐴 · 𝐵 ) /L 𝑃 ) − ( ( 𝐴 /L 𝑃 ) · ( 𝐵 /L 𝑃 ) ) ) ) ≤ ( ( abs ‘ ( ( 𝐴 · 𝐵 ) /L 𝑃 ) ) + ( abs ‘ ( ( 𝐴 /L 𝑃 ) · ( 𝐵 /L 𝑃 ) ) ) ) )
39 1red ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑃 ∈ ℙ ) ∧ 𝑃 ≠ 2 ) → 1 ∈ ℝ )
40 lgsle1 ⊢ ( ( ( 𝐴 · 𝐵 ) ∈ ℤ ∧ 𝑃 ∈ ℤ ) → ( abs ‘ ( ( 𝐴 · 𝐵 ) /L 𝑃 ) ) ≤ 1 )
41 13 16 40 syl2anc ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑃 ∈ ℙ ) ∧ 𝑃 ≠ 2 ) → ( abs ‘ ( ( 𝐴 · 𝐵 ) /L 𝑃 ) ) ≤ 1 )
42 eqid ⊢ { 𝑥 ∈ ℤ ∣ ( abs ‘ 𝑥 ) ≤ 1 } = { 𝑥 ∈ ℤ ∣ ( abs ‘ 𝑥 ) ≤ 1 }
43 42 lgscl2 ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑃 ∈ ℤ ) → ( 𝐴 /L 𝑃 ) ∈ { 𝑥 ∈ ℤ ∣ ( abs ‘ 𝑥 ) ≤ 1 } )
44 11 16 43 syl2anc ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑃 ∈ ℙ ) ∧ 𝑃 ≠ 2 ) → ( 𝐴 /L 𝑃 ) ∈ { 𝑥 ∈ ℤ ∣ ( abs ‘ 𝑥 ) ≤ 1 } )
45 42 lgscl2 ⊢ ( ( 𝐵 ∈ ℤ ∧ 𝑃 ∈ ℤ ) → ( 𝐵 /L 𝑃 ) ∈ { 𝑥 ∈ ℤ ∣ ( abs ‘ 𝑥 ) ≤ 1 } )
46 12 16 45 syl2anc ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑃 ∈ ℙ ) ∧ 𝑃 ≠ 2 ) → ( 𝐵 /L 𝑃 ) ∈ { 𝑥 ∈ ℤ ∣ ( abs ‘ 𝑥 ) ≤ 1 } )
47 42 lgslem3 ⊢ ( ( ( 𝐴 /L 𝑃 ) ∈ { 𝑥 ∈ ℤ ∣ ( abs ‘ 𝑥 ) ≤ 1 } ∧ ( 𝐵 /L 𝑃 ) ∈ { 𝑥 ∈ ℤ ∣ ( abs ‘ 𝑥 ) ≤ 1 } ) → ( ( 𝐴 /L 𝑃 ) · ( 𝐵 /L 𝑃 ) ) ∈ { 𝑥 ∈ ℤ ∣ ( abs ‘ 𝑥 ) ≤ 1 } )
48 44 46 47 syl2anc ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑃 ∈ ℙ ) ∧ 𝑃 ≠ 2 ) → ( ( 𝐴 /L 𝑃 ) · ( 𝐵 /L 𝑃 ) ) ∈ { 𝑥 ∈ ℤ ∣ ( abs ‘ 𝑥 ) ≤ 1 } )
49 fveq2 ⊢ ( 𝑥 = ( ( 𝐴 /L 𝑃 ) · ( 𝐵 /L 𝑃 ) ) → ( abs ‘ 𝑥 ) = ( abs ‘ ( ( 𝐴 /L 𝑃 ) · ( 𝐵 /L 𝑃 ) ) ) )
50 49 breq1d ⊢ ( 𝑥 = ( ( 𝐴 /L 𝑃 ) · ( 𝐵 /L 𝑃 ) ) → ( ( abs ‘ 𝑥 ) ≤ 1 ↔ ( abs ‘ ( ( 𝐴 /L 𝑃 ) · ( 𝐵 /L 𝑃 ) ) ) ≤ 1 ) )
51 50 elrab ⊢ ( ( ( 𝐴 /L 𝑃 ) · ( 𝐵 /L 𝑃 ) ) ∈ { 𝑥 ∈ ℤ ∣ ( abs ‘ 𝑥 ) ≤ 1 } ↔ ( ( ( 𝐴 /L 𝑃 ) · ( 𝐵 /L 𝑃 ) ) ∈ ℤ ∧ ( abs ‘ ( ( 𝐴 /L 𝑃 ) · ( 𝐵 /L 𝑃 ) ) ) ≤ 1 ) )
52 51 simprbi ⊢ ( ( ( 𝐴 /L 𝑃 ) · ( 𝐵 /L 𝑃 ) ) ∈ { 𝑥 ∈ ℤ ∣ ( abs ‘ 𝑥 ) ≤ 1 } → ( abs ‘ ( ( 𝐴 /L 𝑃 ) · ( 𝐵 /L 𝑃 ) ) ) ≤ 1 )
53 48 52 syl ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑃 ∈ ℙ ) ∧ 𝑃 ≠ 2 ) → ( abs ‘ ( ( 𝐴 /L 𝑃 ) · ( 𝐵 /L 𝑃 ) ) ) ≤ 1 )
54 35 36 39 39 41 53 le2addd ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑃 ∈ ℙ ) ∧ 𝑃 ≠ 2 ) → ( ( abs ‘ ( ( 𝐴 · 𝐵 ) /L 𝑃 ) ) + ( abs ‘ ( ( 𝐴 /L 𝑃 ) · ( 𝐵 /L 𝑃 ) ) ) ) ≤ ( 1 + 1 ) )
55 df-2 ⊢ 2 = ( 1 + 1 )
56 54 55 breqtrrdi ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑃 ∈ ℙ ) ∧ 𝑃 ≠ 2 ) → ( ( abs ‘ ( ( 𝐴 · 𝐵 ) /L 𝑃 ) ) + ( abs ‘ ( ( 𝐴 /L 𝑃 ) · ( 𝐵 /L 𝑃 ) ) ) ) ≤ 2 )
57 27 37 33 38 56 letrd ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑃 ∈ ℙ ) ∧ 𝑃 ≠ 2 ) → ( abs ‘ ( ( ( 𝐴 · 𝐵 ) /L 𝑃 ) − ( ( 𝐴 /L 𝑃 ) · ( 𝐵 /L 𝑃 ) ) ) ) ≤ 2 )
58 prmuz2 ⊢ ( 𝑃 ∈ ℙ → 𝑃 ∈ ( ℤ≥ ‘ 2 ) )
59 eluzle ⊢ ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) → 2 ≤ 𝑃 )
60 14 58 59 3syl ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑃 ∈ ℙ ) ∧ 𝑃 ≠ 2 ) → 2 ≤ 𝑃 )
61 simpr ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑃 ∈ ℙ ) ∧ 𝑃 ≠ 2 ) → 𝑃 ≠ 2 )
62 ltlen ⊢ ( ( 2 ∈ ℝ ∧ 𝑃 ∈ ℝ ) → ( 2 < 𝑃 ↔ ( 2 ≤ 𝑃 ∧ 𝑃 ≠ 2 ) ) )
63 32 34 62 sylancr ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑃 ∈ ℙ ) ∧ 𝑃 ≠ 2 ) → ( 2 < 𝑃 ↔ ( 2 ≤ 𝑃 ∧ 𝑃 ≠ 2 ) ) )
64 60 61 63 mpbir2and ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑃 ∈ ℙ ) ∧ 𝑃 ≠ 2 ) → 2 < 𝑃 )
65 27 33 34 57 64 lelttrd ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑃 ∈ ℙ ) ∧ 𝑃 ≠ 2 ) → ( abs ‘ ( ( ( 𝐴 · 𝐵 ) /L 𝑃 ) − ( ( 𝐴 /L 𝑃 ) · ( 𝐵 /L 𝑃 ) ) ) ) < 𝑃 )
66 modid ⊢ ( ( ( ( abs ‘ ( ( ( 𝐴 · 𝐵 ) /L 𝑃 ) − ( ( 𝐴 /L 𝑃 ) · ( 𝐵 /L 𝑃 ) ) ) ) ∈ ℝ ∧ 𝑃 ∈ ℝ+ ) ∧ ( 0 ≤ ( abs ‘ ( ( ( 𝐴 · 𝐵 ) /L 𝑃 ) − ( ( 𝐴 /L 𝑃 ) · ( 𝐵 /L 𝑃 ) ) ) ) ∧ ( abs ‘ ( ( ( 𝐴 · 𝐵 ) /L 𝑃 ) − ( ( 𝐴 /L 𝑃 ) · ( 𝐵 /L 𝑃 ) ) ) ) < 𝑃 ) ) → ( ( abs ‘ ( ( ( 𝐴 · 𝐵 ) /L 𝑃 ) − ( ( 𝐴 /L 𝑃 ) · ( 𝐵 /L 𝑃 ) ) ) ) mod 𝑃 ) = ( abs ‘ ( ( ( 𝐴 · 𝐵 ) /L 𝑃 ) − ( ( 𝐴 /L 𝑃 ) · ( 𝐵 /L 𝑃 ) ) ) ) )
67 27 30 31 65 66 syl22anc ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑃 ∈ ℙ ) ∧ 𝑃 ≠ 2 ) → ( ( abs ‘ ( ( ( 𝐴 · 𝐵 ) /L 𝑃 ) − ( ( 𝐴 /L 𝑃 ) · ( 𝐵 /L 𝑃 ) ) ) ) mod 𝑃 ) = ( abs ‘ ( ( ( 𝐴 · 𝐵 ) /L 𝑃 ) − ( ( 𝐴 /L 𝑃 ) · ( 𝐵 /L 𝑃 ) ) ) ) )
68 11 zcnd ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑃 ∈ ℙ ) ∧ 𝑃 ≠ 2 ) → 𝐴 ∈ ℂ )
69 12 zcnd ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑃 ∈ ℙ ) ∧ 𝑃 ≠ 2 ) → 𝐵 ∈ ℂ )
70 eldifsn ⊢ ( 𝑃 ∈ ( ℙ ∖ { 2 } ) ↔ ( 𝑃 ∈ ℙ ∧ 𝑃 ≠ 2 ) )
71 14 61 70 sylanbrc ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑃 ∈ ℙ ) ∧ 𝑃 ≠ 2 ) → 𝑃 ∈ ( ℙ ∖ { 2 } ) )
72 oddprm ⊢ ( 𝑃 ∈ ( ℙ ∖ { 2 } ) → ( ( 𝑃 − 1 ) / 2 ) ∈ ℕ )
73 71 72 syl ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑃 ∈ ℙ ) ∧ 𝑃 ≠ 2 ) → ( ( 𝑃 − 1 ) / 2 ) ∈ ℕ )
74 73 nnnn0d ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑃 ∈ ℙ ) ∧ 𝑃 ≠ 2 ) → ( ( 𝑃 − 1 ) / 2 ) ∈ ℕ0 )
75 68 69 74 mulexpd ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑃 ∈ ℙ ) ∧ 𝑃 ≠ 2 ) → ( ( 𝐴 · 𝐵 ) ↑ ( ( 𝑃 − 1 ) / 2 ) ) = ( ( 𝐴 ↑ ( ( 𝑃 − 1 ) / 2 ) ) · ( 𝐵 ↑ ( ( 𝑃 − 1 ) / 2 ) ) ) )
76 zexpcl ⊢ ( ( 𝐴 ∈ ℤ ∧ ( ( 𝑃 − 1 ) / 2 ) ∈ ℕ0 ) → ( 𝐴 ↑ ( ( 𝑃 − 1 ) / 2 ) ) ∈ ℤ )
77 11 74 76 syl2anc ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑃 ∈ ℙ ) ∧ 𝑃 ≠ 2 ) → ( 𝐴 ↑ ( ( 𝑃 − 1 ) / 2 ) ) ∈ ℤ )
78 77 zcnd ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑃 ∈ ℙ ) ∧ 𝑃 ≠ 2 ) → ( 𝐴 ↑ ( ( 𝑃 − 1 ) / 2 ) ) ∈ ℂ )
79 zexpcl ⊢ ( ( 𝐵 ∈ ℤ ∧ ( ( 𝑃 − 1 ) / 2 ) ∈ ℕ0 ) → ( 𝐵 ↑ ( ( 𝑃 − 1 ) / 2 ) ) ∈ ℤ )
80 12 74 79 syl2anc ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑃 ∈ ℙ ) ∧ 𝑃 ≠ 2 ) → ( 𝐵 ↑ ( ( 𝑃 − 1 ) / 2 ) ) ∈ ℤ )
81 80 zcnd ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑃 ∈ ℙ ) ∧ 𝑃 ≠ 2 ) → ( 𝐵 ↑ ( ( 𝑃 − 1 ) / 2 ) ) ∈ ℂ )
82 78 81 mulcomd ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑃 ∈ ℙ ) ∧ 𝑃 ≠ 2 ) → ( ( 𝐴 ↑ ( ( 𝑃 − 1 ) / 2 ) ) · ( 𝐵 ↑ ( ( 𝑃 − 1 ) / 2 ) ) ) = ( ( 𝐵 ↑ ( ( 𝑃 − 1 ) / 2 ) ) · ( 𝐴 ↑ ( ( 𝑃 − 1 ) / 2 ) ) ) )
83 75 82 eqtrd ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑃 ∈ ℙ ) ∧ 𝑃 ≠ 2 ) → ( ( 𝐴 · 𝐵 ) ↑ ( ( 𝑃 − 1 ) / 2 ) ) = ( ( 𝐵 ↑ ( ( 𝑃 − 1 ) / 2 ) ) · ( 𝐴 ↑ ( ( 𝑃 − 1 ) / 2 ) ) ) )
84 83 oveq1d ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑃 ∈ ℙ ) ∧ 𝑃 ≠ 2 ) → ( ( ( 𝐴 · 𝐵 ) ↑ ( ( 𝑃 − 1 ) / 2 ) ) mod 𝑃 ) = ( ( ( 𝐵 ↑ ( ( 𝑃 − 1 ) / 2 ) ) · ( 𝐴 ↑ ( ( 𝑃 − 1 ) / 2 ) ) ) mod 𝑃 ) )
85 lgsvalmod ⊢ ( ( ( 𝐴 · 𝐵 ) ∈ ℤ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ) → ( ( ( 𝐴 · 𝐵 ) /L 𝑃 ) mod 𝑃 ) = ( ( ( 𝐴 · 𝐵 ) ↑ ( ( 𝑃 − 1 ) / 2 ) ) mod 𝑃 ) )
86 13 71 85 syl2anc ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑃 ∈ ℙ ) ∧ 𝑃 ≠ 2 ) → ( ( ( 𝐴 · 𝐵 ) /L 𝑃 ) mod 𝑃 ) = ( ( ( 𝐴 · 𝐵 ) ↑ ( ( 𝑃 − 1 ) / 2 ) ) mod 𝑃 ) )
87 21 zred ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑃 ∈ ℙ ) ∧ 𝑃 ≠ 2 ) → ( 𝐴 /L 𝑃 ) ∈ ℝ )
88 77 zred ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑃 ∈ ℙ ) ∧ 𝑃 ≠ 2 ) → ( 𝐴 ↑ ( ( 𝑃 − 1 ) / 2 ) ) ∈ ℝ )
89 lgsvalmod ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ) → ( ( 𝐴 /L 𝑃 ) mod 𝑃 ) = ( ( 𝐴 ↑ ( ( 𝑃 − 1 ) / 2 ) ) mod 𝑃 ) )
90 11 71 89 syl2anc ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑃 ∈ ℙ ) ∧ 𝑃 ≠ 2 ) → ( ( 𝐴 /L 𝑃 ) mod 𝑃 ) = ( ( 𝐴 ↑ ( ( 𝑃 − 1 ) / 2 ) ) mod 𝑃 ) )
91 modmul1 ⊢ ( ( ( ( 𝐴 /L 𝑃 ) ∈ ℝ ∧ ( 𝐴 ↑ ( ( 𝑃 − 1 ) / 2 ) ) ∈ ℝ ) ∧ ( ( 𝐵 /L 𝑃 ) ∈ ℤ ∧ 𝑃 ∈ ℝ+ ) ∧ ( ( 𝐴 /L 𝑃 ) mod 𝑃 ) = ( ( 𝐴 ↑ ( ( 𝑃 − 1 ) / 2 ) ) mod 𝑃 ) ) → ( ( ( 𝐴 /L 𝑃 ) · ( 𝐵 /L 𝑃 ) ) mod 𝑃 ) = ( ( ( 𝐴 ↑ ( ( 𝑃 − 1 ) / 2 ) ) · ( 𝐵 /L 𝑃 ) ) mod 𝑃 ) )
92 87 88 23 30 90 91 syl221anc ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑃 ∈ ℙ ) ∧ 𝑃 ≠ 2 ) → ( ( ( 𝐴 /L 𝑃 ) · ( 𝐵 /L 𝑃 ) ) mod 𝑃 ) = ( ( ( 𝐴 ↑ ( ( 𝑃 − 1 ) / 2 ) ) · ( 𝐵 /L 𝑃 ) ) mod 𝑃 ) )
93 23 zcnd ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑃 ∈ ℙ ) ∧ 𝑃 ≠ 2 ) → ( 𝐵 /L 𝑃 ) ∈ ℂ )
94 78 93 mulcomd ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑃 ∈ ℙ ) ∧ 𝑃 ≠ 2 ) → ( ( 𝐴 ↑ ( ( 𝑃 − 1 ) / 2 ) ) · ( 𝐵 /L 𝑃 ) ) = ( ( 𝐵 /L 𝑃 ) · ( 𝐴 ↑ ( ( 𝑃 − 1 ) / 2 ) ) ) )
95 94 oveq1d ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑃 ∈ ℙ ) ∧ 𝑃 ≠ 2 ) → ( ( ( 𝐴 ↑ ( ( 𝑃 − 1 ) / 2 ) ) · ( 𝐵 /L 𝑃 ) ) mod 𝑃 ) = ( ( ( 𝐵 /L 𝑃 ) · ( 𝐴 ↑ ( ( 𝑃 − 1 ) / 2 ) ) ) mod 𝑃 ) )
96 23 zred ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑃 ∈ ℙ ) ∧ 𝑃 ≠ 2 ) → ( 𝐵 /L 𝑃 ) ∈ ℝ )
97 80 zred ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑃 ∈ ℙ ) ∧ 𝑃 ≠ 2 ) → ( 𝐵 ↑ ( ( 𝑃 − 1 ) / 2 ) ) ∈ ℝ )
98 lgsvalmod ⊢ ( ( 𝐵 ∈ ℤ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ) → ( ( 𝐵 /L 𝑃 ) mod 𝑃 ) = ( ( 𝐵 ↑ ( ( 𝑃 − 1 ) / 2 ) ) mod 𝑃 ) )
99 12 71 98 syl2anc ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑃 ∈ ℙ ) ∧ 𝑃 ≠ 2 ) → ( ( 𝐵 /L 𝑃 ) mod 𝑃 ) = ( ( 𝐵 ↑ ( ( 𝑃 − 1 ) / 2 ) ) mod 𝑃 ) )
100 modmul1 ⊢ ( ( ( ( 𝐵 /L 𝑃 ) ∈ ℝ ∧ ( 𝐵 ↑ ( ( 𝑃 − 1 ) / 2 ) ) ∈ ℝ ) ∧ ( ( 𝐴 ↑ ( ( 𝑃 − 1 ) / 2 ) ) ∈ ℤ ∧ 𝑃 ∈ ℝ+ ) ∧ ( ( 𝐵 /L 𝑃 ) mod 𝑃 ) = ( ( 𝐵 ↑ ( ( 𝑃 − 1 ) / 2 ) ) mod 𝑃 ) ) → ( ( ( 𝐵 /L 𝑃 ) · ( 𝐴 ↑ ( ( 𝑃 − 1 ) / 2 ) ) ) mod 𝑃 ) = ( ( ( 𝐵 ↑ ( ( 𝑃 − 1 ) / 2 ) ) · ( 𝐴 ↑ ( ( 𝑃 − 1 ) / 2 ) ) ) mod 𝑃 ) )
101 96 97 77 30 99 100 syl221anc ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑃 ∈ ℙ ) ∧ 𝑃 ≠ 2 ) → ( ( ( 𝐵 /L 𝑃 ) · ( 𝐴 ↑ ( ( 𝑃 − 1 ) / 2 ) ) ) mod 𝑃 ) = ( ( ( 𝐵 ↑ ( ( 𝑃 − 1 ) / 2 ) ) · ( 𝐴 ↑ ( ( 𝑃 − 1 ) / 2 ) ) ) mod 𝑃 ) )
102 92 95 101 3eqtrd ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑃 ∈ ℙ ) ∧ 𝑃 ≠ 2 ) → ( ( ( 𝐴 /L 𝑃 ) · ( 𝐵 /L 𝑃 ) ) mod 𝑃 ) = ( ( ( 𝐵 ↑ ( ( 𝑃 − 1 ) / 2 ) ) · ( 𝐴 ↑ ( ( 𝑃 − 1 ) / 2 ) ) ) mod 𝑃 ) )
103 84 86 102 3eqtr4d ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑃 ∈ ℙ ) ∧ 𝑃 ≠ 2 ) → ( ( ( 𝐴 · 𝐵 ) /L 𝑃 ) mod 𝑃 ) = ( ( ( 𝐴 /L 𝑃 ) · ( 𝐵 /L 𝑃 ) ) mod 𝑃 ) )
104 moddvds ⊢ ( ( 𝑃 ∈ ℕ ∧ ( ( 𝐴 · 𝐵 ) /L 𝑃 ) ∈ ℤ ∧ ( ( 𝐴 /L 𝑃 ) · ( 𝐵 /L 𝑃 ) ) ∈ ℤ ) → ( ( ( ( 𝐴 · 𝐵 ) /L 𝑃 ) mod 𝑃 ) = ( ( ( 𝐴 /L 𝑃 ) · ( 𝐵 /L 𝑃 ) ) mod 𝑃 ) ↔ 𝑃 ∥ ( ( ( 𝐴 · 𝐵 ) /L 𝑃 ) − ( ( 𝐴 /L 𝑃 ) · ( 𝐵 /L 𝑃 ) ) ) ) )
105 29 18 24 104 syl3anc ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑃 ∈ ℙ ) ∧ 𝑃 ≠ 2 ) → ( ( ( ( 𝐴 · 𝐵 ) /L 𝑃 ) mod 𝑃 ) = ( ( ( 𝐴 /L 𝑃 ) · ( 𝐵 /L 𝑃 ) ) mod 𝑃 ) ↔ 𝑃 ∥ ( ( ( 𝐴 · 𝐵 ) /L 𝑃 ) − ( ( 𝐴 /L 𝑃 ) · ( 𝐵 /L 𝑃 ) ) ) ) )
106 103 105 mpbid ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑃 ∈ ℙ ) ∧ 𝑃 ≠ 2 ) → 𝑃 ∥ ( ( ( 𝐴 · 𝐵 ) /L 𝑃 ) − ( ( 𝐴 /L 𝑃 ) · ( 𝐵 /L 𝑃 ) ) ) )
107 18 24 zsubcld ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑃 ∈ ℙ ) ∧ 𝑃 ≠ 2 ) → ( ( ( 𝐴 · 𝐵 ) /L 𝑃 ) − ( ( 𝐴 /L 𝑃 ) · ( 𝐵 /L 𝑃 ) ) ) ∈ ℤ )
108 dvdsabsb ⊢ ( ( 𝑃 ∈ ℤ ∧ ( ( ( 𝐴 · 𝐵 ) /L 𝑃 ) − ( ( 𝐴 /L 𝑃 ) · ( 𝐵 /L 𝑃 ) ) ) ∈ ℤ ) → ( 𝑃 ∥ ( ( ( 𝐴 · 𝐵 ) /L 𝑃 ) − ( ( 𝐴 /L 𝑃 ) · ( 𝐵 /L 𝑃 ) ) ) ↔ 𝑃 ∥ ( abs ‘ ( ( ( 𝐴 · 𝐵 ) /L 𝑃 ) − ( ( 𝐴 /L 𝑃 ) · ( 𝐵 /L 𝑃 ) ) ) ) ) )
109 16 107 108 syl2anc ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑃 ∈ ℙ ) ∧ 𝑃 ≠ 2 ) → ( 𝑃 ∥ ( ( ( 𝐴 · 𝐵 ) /L 𝑃 ) − ( ( 𝐴 /L 𝑃 ) · ( 𝐵 /L 𝑃 ) ) ) ↔ 𝑃 ∥ ( abs ‘ ( ( ( 𝐴 · 𝐵 ) /L 𝑃 ) − ( ( 𝐴 /L 𝑃 ) · ( 𝐵 /L 𝑃 ) ) ) ) ) )
110 106 109 mpbid ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑃 ∈ ℙ ) ∧ 𝑃 ≠ 2 ) → 𝑃 ∥ ( abs ‘ ( ( ( 𝐴 · 𝐵 ) /L 𝑃 ) − ( ( 𝐴 /L 𝑃 ) · ( 𝐵 /L 𝑃 ) ) ) ) )
111 dvdsmod0 ⊢ ( ( 𝑃 ∈ ℕ ∧ 𝑃 ∥ ( abs ‘ ( ( ( 𝐴 · 𝐵 ) /L 𝑃 ) − ( ( 𝐴 /L 𝑃 ) · ( 𝐵 /L 𝑃 ) ) ) ) ) → ( ( abs ‘ ( ( ( 𝐴 · 𝐵 ) /L 𝑃 ) − ( ( 𝐴 /L 𝑃 ) · ( 𝐵 /L 𝑃 ) ) ) ) mod 𝑃 ) = 0 )
112 29 110 111 syl2anc ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑃 ∈ ℙ ) ∧ 𝑃 ≠ 2 ) → ( ( abs ‘ ( ( ( 𝐴 · 𝐵 ) /L 𝑃 ) − ( ( 𝐴 /L 𝑃 ) · ( 𝐵 /L 𝑃 ) ) ) ) mod 𝑃 ) = 0 )
113 67 112 eqtr3d ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑃 ∈ ℙ ) ∧ 𝑃 ≠ 2 ) → ( abs ‘ ( ( ( 𝐴 · 𝐵 ) /L 𝑃 ) − ( ( 𝐴 /L 𝑃 ) · ( 𝐵 /L 𝑃 ) ) ) ) = 0 )
114 26 113 abs00d ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑃 ∈ ℙ ) ∧ 𝑃 ≠ 2 ) → ( ( ( 𝐴 · 𝐵 ) /L 𝑃 ) − ( ( 𝐴 /L 𝑃 ) · ( 𝐵 /L 𝑃 ) ) ) = 0 )
115 19 25 114 subeq0d ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑃 ∈ ℙ ) ∧ 𝑃 ≠ 2 ) → ( ( 𝐴 · 𝐵 ) /L 𝑃 ) = ( ( 𝐴 /L 𝑃 ) · ( 𝐵 /L 𝑃 ) ) )
116 10 115 pm2.61dane ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑃 ∈ ℙ ) → ( ( 𝐴 · 𝐵 ) /L 𝑃 ) = ( ( 𝐴 /L 𝑃 ) · ( 𝐵 /L 𝑃 ) ) )