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 
|- ( ( A e. ZZ /\ B e. ZZ /\ P e. Prime ) -> ( ( A x. B ) /L P ) = ( ( A /L P ) x. ( B /L P ) ) )

Proof

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