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 𝑃 ) ) )