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 \in ℤ \land B \in ℤ \land P \in ℙ) \to A B /_{L} P = (A /_{L} P) (B /_{L} P)$

Proof

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

Metamath Proof Explorer

Theorem lgsdirprm

Proof