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