lgsqr

Description: The Legendre symbol for odd primes is 1 iff the number is not a multiple of the prime (in which case it is 0 , see lgsne0 ) and the number is a quadratic residue mod P (it is -u 1 for nonresidues by the process of elimination from lgsabs1 ). Given our definition of the Legendre symbol, this theorem is equivalent to Euler's criterion. (Contributed by Mario Carneiro, 15-Jun-2015)

		Ref	Expression
	Assertion	lgsqr	$⊢ (A \in ℤ \land P \in (ℙ ∖ \{2\})) \to (A /_{L} P = 1 \leftrightarrow (\neg P ∥ A \land \exists x \in ℤ P ∥ (x^{2} - A)))$

Proof

Step	Hyp	Ref	Expression
1		eldifi	$⊢ P \in (ℙ ∖ \{2\}) \to P \in ℙ$
2	1	adantl	$⊢ (A \in ℤ \land P \in (ℙ ∖ \{2\})) \to P \in ℙ$
3		prmz	$⊢ P \in ℙ \to P \in ℤ$
4	2 3	syl	$⊢ (A \in ℤ \land P \in (ℙ ∖ \{2\})) \to P \in ℤ$
5		simpl	$⊢ (A \in ℤ \land P \in (ℙ ∖ \{2\})) \to A \in ℤ$
6		gcdcom	$⊢ (P \in ℤ \land A \in ℤ) \to P \gcd A = A \gcd P$
7	4 5 6	syl2anc	$⊢ (A \in ℤ \land P \in (ℙ ∖ \{2\})) \to P \gcd A = A \gcd P$
8	7	eqeq1d	$⊢ (A \in ℤ \land P \in (ℙ ∖ \{2\})) \to (P \gcd A = 1 \leftrightarrow A \gcd P = 1)$
9		coprm	$⊢ (P \in ℙ \land A \in ℤ) \to (\neg P ∥ A \leftrightarrow P \gcd A = 1)$
10	2 5 9	syl2anc	$⊢ (A \in ℤ \land P \in (ℙ ∖ \{2\})) \to (\neg P ∥ A \leftrightarrow P \gcd A = 1)$
11		lgsne0	$⊢ (A \in ℤ \land P \in ℤ) \to (A /_{L} P \neq 0 \leftrightarrow A \gcd P = 1)$
12	5 4 11	syl2anc	$⊢ (A \in ℤ \land P \in (ℙ ∖ \{2\})) \to (A /_{L} P \neq 0 \leftrightarrow A \gcd P = 1)$
13	8 10 12	3bitr4d	$⊢ (A \in ℤ \land P \in (ℙ ∖ \{2\})) \to (\neg P ∥ A \leftrightarrow A /_{L} P \neq 0)$
14	13	necon4bbid	$⊢ (A \in ℤ \land P \in (ℙ ∖ \{2\})) \to (P ∥ A \leftrightarrow A /_{L} P = 0)$
15		0ne1	$⊢ 0 \neq 1$
16		neeq1	$⊢ A /_{L} P = 0 \to (A /_{L} P \neq 1 \leftrightarrow 0 \neq 1)$
17	15 16	mpbiri	$⊢ A /_{L} P = 0 \to A /_{L} P \neq 1$
18	14 17	syl6bi	$⊢ (A \in ℤ \land P \in (ℙ ∖ \{2\})) \to (P ∥ A \to A /_{L} P \neq 1)$
19	18	necon2bd	$⊢ (A \in ℤ \land P \in (ℙ ∖ \{2\})) \to (A /_{L} P = 1 \to \neg P ∥ A)$
20		lgsqrlem5	$⊢ (A \in ℤ \land P \in (ℙ ∖ \{2\}) \land A /_{L} P = 1) \to \exists x \in ℤ P ∥ (x^{2} - A)$
21	20	3expia	$⊢ (A \in ℤ \land P \in (ℙ ∖ \{2\})) \to (A /_{L} P = 1 \to \exists x \in ℤ P ∥ (x^{2} - A))$
22	19 21	jcad	$⊢ (A \in ℤ \land P \in (ℙ ∖ \{2\})) \to (A /_{L} P = 1 \to (\neg P ∥ A \land \exists x \in ℤ P ∥ (x^{2} - A)))$
23		simprl	$⊢ (((A \in ℤ \land P \in (ℙ ∖ \{2\})) \land \neg P ∥ A) \land (x \in ℤ \land P ∥ (x^{2} - A))) \to x \in ℤ$
24	23	zred	$⊢ (((A \in ℤ \land P \in (ℙ ∖ \{2\})) \land \neg P ∥ A) \land (x \in ℤ \land P ∥ (x^{2} - A))) \to x \in ℝ$
25		absresq	$⊢ x \in ℝ \to {\|x\|}^{2} = x^{2}$
26	24 25	syl	$⊢ (((A \in ℤ \land P \in (ℙ ∖ \{2\})) \land \neg P ∥ A) \land (x \in ℤ \land P ∥ (x^{2} - A))) \to {\|x\|}^{2} = x^{2}$
27	26	oveq1d	$⊢ (((A \in ℤ \land P \in (ℙ ∖ \{2\})) \land \neg P ∥ A) \land (x \in ℤ \land P ∥ (x^{2} - A))) \to {\|x\|}^{2} /_{L} P = x^{2} /_{L} P$
28		simplr	$⊢ (((A \in ℤ \land P \in (ℙ ∖ \{2\})) \land \neg P ∥ A) \land (x \in ℤ \land P ∥ (x^{2} - A))) \to \neg P ∥ A$
29	1	ad3antlr	$⊢ (((A \in ℤ \land P \in (ℙ ∖ \{2\})) \land \neg P ∥ A) \land (x \in ℤ \land P ∥ (x^{2} - A))) \to P \in ℙ$
30	29 3	syl	$⊢ (((A \in ℤ \land P \in (ℙ ∖ \{2\})) \land \neg P ∥ A) \land (x \in ℤ \land P ∥ (x^{2} - A))) \to P \in ℤ$
31		zsqcl	$⊢ x \in ℤ \to x^{2} \in ℤ$
32	23 31	syl	$⊢ (((A \in ℤ \land P \in (ℙ ∖ \{2\})) \land \neg P ∥ A) \land (x \in ℤ \land P ∥ (x^{2} - A))) \to x^{2} \in ℤ$
33		simplll	$⊢ (((A \in ℤ \land P \in (ℙ ∖ \{2\})) \land \neg P ∥ A) \land (x \in ℤ \land P ∥ (x^{2} - A))) \to A \in ℤ$
34		simprr	$⊢ (((A \in ℤ \land P \in (ℙ ∖ \{2\})) \land \neg P ∥ A) \land (x \in ℤ \land P ∥ (x^{2} - A))) \to P ∥ (x^{2} - A)$
35		dvdssub2	$⊢ ((P \in ℤ \land x^{2} \in ℤ \land A \in ℤ) \land P ∥ (x^{2} - A)) \to (P ∥ x^{2} \leftrightarrow P ∥ A)$
36	30 32 33 34 35	syl31anc	$⊢ (((A \in ℤ \land P \in (ℙ ∖ \{2\})) \land \neg P ∥ A) \land (x \in ℤ \land P ∥ (x^{2} - A))) \to (P ∥ x^{2} \leftrightarrow P ∥ A)$
37	28 36	mtbird	$⊢ (((A \in ℤ \land P \in (ℙ ∖ \{2\})) \land \neg P ∥ A) \land (x \in ℤ \land P ∥ (x^{2} - A))) \to \neg P ∥ x^{2}$
38		2nn	$⊢ 2 \in ℕ$
39	38	a1i	$⊢ (((A \in ℤ \land P \in (ℙ ∖ \{2\})) \land \neg P ∥ A) \land (x \in ℤ \land P ∥ (x^{2} - A))) \to 2 \in ℕ$
40		prmdvdsexp	$⊢ (P \in ℙ \land x \in ℤ \land 2 \in ℕ) \to (P ∥ x^{2} \leftrightarrow P ∥ x)$
41	29 23 39 40	syl3anc	$⊢ (((A \in ℤ \land P \in (ℙ ∖ \{2\})) \land \neg P ∥ A) \land (x \in ℤ \land P ∥ (x^{2} - A))) \to (P ∥ x^{2} \leftrightarrow P ∥ x)$
42	37 41	mtbid	$⊢ (((A \in ℤ \land P \in (ℙ ∖ \{2\})) \land \neg P ∥ A) \land (x \in ℤ \land P ∥ (x^{2} - A))) \to \neg P ∥ x$
43		dvds0	$⊢ P \in ℤ \to P ∥ 0$
44	30 43	syl	$⊢ (((A \in ℤ \land P \in (ℙ ∖ \{2\})) \land \neg P ∥ A) \land (x \in ℤ \land P ∥ (x^{2} - A))) \to P ∥ 0$
45		breq2	$⊢ x = 0 \to (P ∥ x \leftrightarrow P ∥ 0)$
46	44 45	syl5ibrcom	$⊢ (((A \in ℤ \land P \in (ℙ ∖ \{2\})) \land \neg P ∥ A) \land (x \in ℤ \land P ∥ (x^{2} - A))) \to (x = 0 \to P ∥ x)$
47	46	necon3bd	$⊢ (((A \in ℤ \land P \in (ℙ ∖ \{2\})) \land \neg P ∥ A) \land (x \in ℤ \land P ∥ (x^{2} - A))) \to (\neg P ∥ x \to x \neq 0)$
48	42 47	mpd	$⊢ (((A \in ℤ \land P \in (ℙ ∖ \{2\})) \land \neg P ∥ A) \land (x \in ℤ \land P ∥ (x^{2} - A))) \to x \neq 0$
49		nnabscl	$⊢ (x \in ℤ \land x \neq 0) \to \|x\| \in ℕ$
50	23 48 49	syl2anc	$⊢ (((A \in ℤ \land P \in (ℙ ∖ \{2\})) \land \neg P ∥ A) \land (x \in ℤ \land P ∥ (x^{2} - A))) \to \|x\| \in ℕ$
51	50	nnzd	$⊢ (((A \in ℤ \land P \in (ℙ ∖ \{2\})) \land \neg P ∥ A) \land (x \in ℤ \land P ∥ (x^{2} - A))) \to \|x\| \in ℤ$
52	50	nnne0d	$⊢ (((A \in ℤ \land P \in (ℙ ∖ \{2\})) \land \neg P ∥ A) \land (x \in ℤ \land P ∥ (x^{2} - A))) \to \|x\| \neq 0$
53		gcdcom	$⊢ (\|x\| \in ℤ \land P \in ℤ) \to \|x\| \gcd P = P \gcd \|x\|$
54	51 30 53	syl2anc	$⊢ (((A \in ℤ \land P \in (ℙ ∖ \{2\})) \land \neg P ∥ A) \land (x \in ℤ \land P ∥ (x^{2} - A))) \to \|x\| \gcd P = P \gcd \|x\|$
55		dvdsabsb	$⊢ (P \in ℤ \land x \in ℤ) \to (P ∥ x \leftrightarrow P ∥ \|x\|)$
56	30 23 55	syl2anc	$⊢ (((A \in ℤ \land P \in (ℙ ∖ \{2\})) \land \neg P ∥ A) \land (x \in ℤ \land P ∥ (x^{2} - A))) \to (P ∥ x \leftrightarrow P ∥ \|x\|)$
57	42 56	mtbid	$⊢ (((A \in ℤ \land P \in (ℙ ∖ \{2\})) \land \neg P ∥ A) \land (x \in ℤ \land P ∥ (x^{2} - A))) \to \neg P ∥ \|x\|$
58		coprm	$⊢ (P \in ℙ \land \|x\| \in ℤ) \to (\neg P ∥ \|x\| \leftrightarrow P \gcd \|x\| = 1)$
59	29 51 58	syl2anc	$⊢ (((A \in ℤ \land P \in (ℙ ∖ \{2\})) \land \neg P ∥ A) \land (x \in ℤ \land P ∥ (x^{2} - A))) \to (\neg P ∥ \|x\| \leftrightarrow P \gcd \|x\| = 1)$
60	57 59	mpbid	$⊢ (((A \in ℤ \land P \in (ℙ ∖ \{2\})) \land \neg P ∥ A) \land (x \in ℤ \land P ∥ (x^{2} - A))) \to P \gcd \|x\| = 1$
61	54 60	eqtrd	$⊢ (((A \in ℤ \land P \in (ℙ ∖ \{2\})) \land \neg P ∥ A) \land (x \in ℤ \land P ∥ (x^{2} - A))) \to \|x\| \gcd P = 1$
62		lgssq	$⊢ ((\|x\| \in ℤ \land \|x\| \neq 0) \land P \in ℤ \land \|x\| \gcd P = 1) \to {\|x\|}^{2} /_{L} P = 1$
63	51 52 30 61 62	syl211anc	$⊢ (((A \in ℤ \land P \in (ℙ ∖ \{2\})) \land \neg P ∥ A) \land (x \in ℤ \land P ∥ (x^{2} - A))) \to {\|x\|}^{2} /_{L} P = 1$
64		prmnn	$⊢ P \in ℙ \to P \in ℕ$
65	29 64	syl	$⊢ (((A \in ℤ \land P \in (ℙ ∖ \{2\})) \land \neg P ∥ A) \land (x \in ℤ \land P ∥ (x^{2} - A))) \to P \in ℕ$
66		moddvds	$⊢ (P \in ℕ \land x^{2} \in ℤ \land A \in ℤ) \to (x^{2} \mod P = A \mod P \leftrightarrow P ∥ (x^{2} - A))$
67	65 32 33 66	syl3anc	$⊢ (((A \in ℤ \land P \in (ℙ ∖ \{2\})) \land \neg P ∥ A) \land (x \in ℤ \land P ∥ (x^{2} - A))) \to (x^{2} \mod P = A \mod P \leftrightarrow P ∥ (x^{2} - A))$
68	34 67	mpbird	$⊢ (((A \in ℤ \land P \in (ℙ ∖ \{2\})) \land \neg P ∥ A) \land (x \in ℤ \land P ∥ (x^{2} - A))) \to x^{2} \mod P = A \mod P$
69	68	oveq1d	$⊢ (((A \in ℤ \land P \in (ℙ ∖ \{2\})) \land \neg P ∥ A) \land (x \in ℤ \land P ∥ (x^{2} - A))) \to (x^{2} \mod P) /_{L} P = (A \mod P) /_{L} P$
70		eldifsni	$⊢ P \in (ℙ ∖ \{2\}) \to P \neq 2$
71	70	ad3antlr	$⊢ (((A \in ℤ \land P \in (ℙ ∖ \{2\})) \land \neg P ∥ A) \land (x \in ℤ \land P ∥ (x^{2} - A))) \to P \neq 2$
72	71	necomd	$⊢ (((A \in ℤ \land P \in (ℙ ∖ \{2\})) \land \neg P ∥ A) \land (x \in ℤ \land P ∥ (x^{2} - A))) \to 2 \neq P$
73		2z	$⊢ 2 \in ℤ$
74		uzid	$⊢ 2 \in ℤ \to 2 \in ℤ_{\geq 2}$
75	73 74	ax-mp	$⊢ 2 \in ℤ_{\geq 2}$
76		dvdsprm	$⊢ (2 \in ℤ_{\geq 2} \land P \in ℙ) \to (2 ∥ P \leftrightarrow 2 = P)$
77	76	necon3bbid	$⊢ (2 \in ℤ_{\geq 2} \land P \in ℙ) \to (\neg 2 ∥ P \leftrightarrow 2 \neq P)$
78	75 29 77	sylancr	$⊢ (((A \in ℤ \land P \in (ℙ ∖ \{2\})) \land \neg P ∥ A) \land (x \in ℤ \land P ∥ (x^{2} - A))) \to (\neg 2 ∥ P \leftrightarrow 2 \neq P)$
79	72 78	mpbird	$⊢ (((A \in ℤ \land P \in (ℙ ∖ \{2\})) \land \neg P ∥ A) \land (x \in ℤ \land P ∥ (x^{2} - A))) \to \neg 2 ∥ P$
80		lgsmod	$⊢ (x^{2} \in ℤ \land P \in ℕ \land \neg 2 ∥ P) \to (x^{2} \mod P) /_{L} P = x^{2} /_{L} P$
81	32 65 79 80	syl3anc	$⊢ (((A \in ℤ \land P \in (ℙ ∖ \{2\})) \land \neg P ∥ A) \land (x \in ℤ \land P ∥ (x^{2} - A))) \to (x^{2} \mod P) /_{L} P = x^{2} /_{L} P$
82		lgsmod	$⊢ (A \in ℤ \land P \in ℕ \land \neg 2 ∥ P) \to (A \mod P) /_{L} P = A /_{L} P$
83	33 65 79 82	syl3anc	$⊢ (((A \in ℤ \land P \in (ℙ ∖ \{2\})) \land \neg P ∥ A) \land (x \in ℤ \land P ∥ (x^{2} - A))) \to (A \mod P) /_{L} P = A /_{L} P$
84	69 81 83	3eqtr3d	$⊢ (((A \in ℤ \land P \in (ℙ ∖ \{2\})) \land \neg P ∥ A) \land (x \in ℤ \land P ∥ (x^{2} - A))) \to x^{2} /_{L} P = A /_{L} P$
85	27 63 84	3eqtr3rd	$⊢ (((A \in ℤ \land P \in (ℙ ∖ \{2\})) \land \neg P ∥ A) \land (x \in ℤ \land P ∥ (x^{2} - A))) \to A /_{L} P = 1$
86	85	rexlimdvaa	$⊢ ((A \in ℤ \land P \in (ℙ ∖ \{2\})) \land \neg P ∥ A) \to (\exists x \in ℤ P ∥ (x^{2} - A) \to A /_{L} P = 1)$
87	86	expimpd	$⊢ (A \in ℤ \land P \in (ℙ ∖ \{2\})) \to ((\neg P ∥ A \land \exists x \in ℤ P ∥ (x^{2} - A)) \to A /_{L} P = 1)$
88	22 87	impbid	$⊢ (A \in ℤ \land P \in (ℙ ∖ \{2\})) \to (A /_{L} P = 1 \leftrightarrow (\neg P ∥ A \land \exists x \in ℤ P ∥ (x^{2} - A)))$

Metamath Proof Explorer

Theorem lgsqr

Proof