lgsqrmodndvds

Description: If the Legendre symbol of an integer A for an odd prime is 1 , then the number is a quadratic residue mod P with a solution x of the congruence ( x ^ 2 ) == A (mod P ) which is not divisible by the prime. (Contributed by AV, 20-Aug-2021) (Proof shortened by AV, 18-Mar-2022)

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

Proof

Step	Hyp	Ref	Expression
1		lgsqrmod	$⊢ (A \in ℤ \land P \in (ℙ ∖ \{2\})) \to (A /_{L} P = 1 \to \exists x \in ℤ x^{2} \mod P = A \mod P)$
2	1	imp	$⊢ ((A \in ℤ \land P \in (ℙ ∖ \{2\})) \land A /_{L} P = 1) \to \exists x \in ℤ x^{2} \mod P = A \mod P$
3		eldifi	$⊢ P \in (ℙ ∖ \{2\}) \to P \in ℙ$
4		prmnn	$⊢ P \in ℙ \to P \in ℕ$
5	3 4	syl	$⊢ P \in (ℙ ∖ \{2\}) \to P \in ℕ$
6	5	ad3antlr	$⊢ (((A \in ℤ \land P \in (ℙ ∖ \{2\})) \land A /_{L} P = 1) \land x \in ℤ) \to P \in ℕ$
7		zsqcl	$⊢ x \in ℤ \to x^{2} \in ℤ$
8	7	adantl	$⊢ (((A \in ℤ \land P \in (ℙ ∖ \{2\})) \land A /_{L} P = 1) \land x \in ℤ) \to x^{2} \in ℤ$
9		simplll	$⊢ (((A \in ℤ \land P \in (ℙ ∖ \{2\})) \land A /_{L} P = 1) \land x \in ℤ) \to A \in ℤ$
10		moddvds	$⊢ (P \in ℕ \land x^{2} \in ℤ \land A \in ℤ) \to (x^{2} \mod P = A \mod P \leftrightarrow P ∥ (x^{2} - A))$
11	6 8 9 10	syl3anc	$⊢ (((A \in ℤ \land P \in (ℙ ∖ \{2\})) \land A /_{L} P = 1) \land x \in ℤ) \to (x^{2} \mod P = A \mod P \leftrightarrow P ∥ (x^{2} - A))$
12	5	nnzd	$⊢ P \in (ℙ ∖ \{2\}) \to P \in ℤ$
13	12	ad3antlr	$⊢ (((A \in ℤ \land P \in (ℙ ∖ \{2\})) \land A /_{L} P = 1) \land x \in ℤ) \to P \in ℤ$
14	13 8 9	3jca	$⊢ (((A \in ℤ \land P \in (ℙ ∖ \{2\})) \land A /_{L} P = 1) \land x \in ℤ) \to (P \in ℤ \land x^{2} \in ℤ \land A \in ℤ)$
15	14	adantl	$⊢ (P ∥ x \land (((A \in ℤ \land P \in (ℙ ∖ \{2\})) \land A /_{L} P = 1) \land x \in ℤ)) \to (P \in ℤ \land x^{2} \in ℤ \land A \in ℤ)$
16		dvdssub2	$⊢ ((P \in ℤ \land x^{2} \in ℤ \land A \in ℤ) \land P ∥ (x^{2} - A)) \to (P ∥ x^{2} \leftrightarrow P ∥ A)$
17	15 16	sylan	$⊢ ((P ∥ x \land (((A \in ℤ \land P \in (ℙ ∖ \{2\})) \land A /_{L} P = 1) \land x \in ℤ)) \land P ∥ (x^{2} - A)) \to (P ∥ x^{2} \leftrightarrow P ∥ A)$
18	17	ex	$⊢ (P ∥ x \land (((A \in ℤ \land P \in (ℙ ∖ \{2\})) \land A /_{L} P = 1) \land x \in ℤ)) \to (P ∥ (x^{2} - A) \to (P ∥ x^{2} \leftrightarrow P ∥ A))$
19		bicom	$⊢ (P ∥ x^{2} \leftrightarrow P ∥ A) \leftrightarrow (P ∥ A \leftrightarrow P ∥ x^{2})$
20	3	ad3antlr	$⊢ (((A \in ℤ \land P \in (ℙ ∖ \{2\})) \land A /_{L} P = 1) \land x \in ℤ) \to P \in ℙ$
21		simpr	$⊢ (((A \in ℤ \land P \in (ℙ ∖ \{2\})) \land A /_{L} P = 1) \land x \in ℤ) \to x \in ℤ$
22		2nn	$⊢ 2 \in ℕ$
23	22	a1i	$⊢ (((A \in ℤ \land P \in (ℙ ∖ \{2\})) \land A /_{L} P = 1) \land x \in ℤ) \to 2 \in ℕ$
24		prmdvdsexp	$⊢ (P \in ℙ \land x \in ℤ \land 2 \in ℕ) \to (P ∥ x^{2} \leftrightarrow P ∥ x)$
25	20 21 23 24	syl3anc	$⊢ (((A \in ℤ \land P \in (ℙ ∖ \{2\})) \land A /_{L} P = 1) \land x \in ℤ) \to (P ∥ x^{2} \leftrightarrow P ∥ x)$
26	25	biimparc	$⊢ (P ∥ x \land (((A \in ℤ \land P \in (ℙ ∖ \{2\})) \land A /_{L} P = 1) \land x \in ℤ)) \to P ∥ x^{2}$
27		bianir	$⊢ (P ∥ x^{2} \land (P ∥ A \leftrightarrow P ∥ x^{2})) \to P ∥ A$
28	5	ad2antlr	$⊢ ((A \in ℤ \land P \in (ℙ ∖ \{2\})) \land A /_{L} P = 1) \to P \in ℕ$
29		dvdsmod0	$⊢ (P \in ℕ \land P ∥ A) \to A \mod P = 0$
30	29	ex	$⊢ P \in ℕ \to (P ∥ A \to A \mod P = 0)$
31	28 30	syl	$⊢ ((A \in ℤ \land P \in (ℙ ∖ \{2\})) \land A /_{L} P = 1) \to (P ∥ A \to A \mod P = 0)$
32		lgsprme0	$⊢ (A \in ℤ \land P \in ℙ) \to (A /_{L} P = 0 \leftrightarrow A \mod P = 0)$
33	3 32	sylan2	$⊢ (A \in ℤ \land P \in (ℙ ∖ \{2\})) \to (A /_{L} P = 0 \leftrightarrow A \mod P = 0)$
34		eqeq1	$⊢ A /_{L} P = 0 \to (A /_{L} P = 1 \leftrightarrow 0 = 1)$
35		0ne1	$⊢ 0 \neq 1$
36		eqneqall	$⊢ 0 = 1 \to (0 \neq 1 \to \neg P ∥ x)$
37	35 36	mpi	$⊢ 0 = 1 \to \neg P ∥ x$
38	34 37	biimtrdi	$⊢ A /_{L} P = 0 \to (A /_{L} P = 1 \to \neg P ∥ x)$
39	33 38	biimtrrdi	$⊢ (A \in ℤ \land P \in (ℙ ∖ \{2\})) \to (A \mod P = 0 \to (A /_{L} P = 1 \to \neg P ∥ x))$
40	39	com23	$⊢ (A \in ℤ \land P \in (ℙ ∖ \{2\})) \to (A /_{L} P = 1 \to (A \mod P = 0 \to \neg P ∥ x))$
41	40	imp	$⊢ ((A \in ℤ \land P \in (ℙ ∖ \{2\})) \land A /_{L} P = 1) \to (A \mod P = 0 \to \neg P ∥ x)$
42	31 41	syld	$⊢ ((A \in ℤ \land P \in (ℙ ∖ \{2\})) \land A /_{L} P = 1) \to (P ∥ A \to \neg P ∥ x)$
43	42	ad2antrl	$⊢ (P ∥ x \land (((A \in ℤ \land P \in (ℙ ∖ \{2\})) \land A /_{L} P = 1) \land x \in ℤ)) \to (P ∥ A \to \neg P ∥ x)$
44	27 43	syl5com	$⊢ (P ∥ x^{2} \land (P ∥ A \leftrightarrow P ∥ x^{2})) \to ((P ∥ x \land (((A \in ℤ \land P \in (ℙ ∖ \{2\})) \land A /_{L} P = 1) \land x \in ℤ)) \to \neg P ∥ x)$
45	44	ex	$⊢ P ∥ x^{2} \to ((P ∥ A \leftrightarrow P ∥ x^{2}) \to ((P ∥ x \land (((A \in ℤ \land P \in (ℙ ∖ \{2\})) \land A /_{L} P = 1) \land x \in ℤ)) \to \neg P ∥ x))$
46	45	com23	$⊢ P ∥ x^{2} \to ((P ∥ x \land (((A \in ℤ \land P \in (ℙ ∖ \{2\})) \land A /_{L} P = 1) \land x \in ℤ)) \to ((P ∥ A \leftrightarrow P ∥ x^{2}) \to \neg P ∥ x))$
47	26 46	mpcom	$⊢ (P ∥ x \land (((A \in ℤ \land P \in (ℙ ∖ \{2\})) \land A /_{L} P = 1) \land x \in ℤ)) \to ((P ∥ A \leftrightarrow P ∥ x^{2}) \to \neg P ∥ x)$
48	19 47	biimtrid	$⊢ (P ∥ x \land (((A \in ℤ \land P \in (ℙ ∖ \{2\})) \land A /_{L} P = 1) \land x \in ℤ)) \to ((P ∥ x^{2} \leftrightarrow P ∥ A) \to \neg P ∥ x)$
49	18 48	syld	$⊢ (P ∥ x \land (((A \in ℤ \land P \in (ℙ ∖ \{2\})) \land A /_{L} P = 1) \land x \in ℤ)) \to (P ∥ (x^{2} - A) \to \neg P ∥ x)$
50	49	ex	$⊢ P ∥ x \to ((((A \in ℤ \land P \in (ℙ ∖ \{2\})) \land A /_{L} P = 1) \land x \in ℤ) \to (P ∥ (x^{2} - A) \to \neg P ∥ x))$
51		2a1	$⊢ \neg P ∥ x \to ((((A \in ℤ \land P \in (ℙ ∖ \{2\})) \land A /_{L} P = 1) \land x \in ℤ) \to (P ∥ (x^{2} - A) \to \neg P ∥ x))$
52	50 51	pm2.61i	$⊢ (((A \in ℤ \land P \in (ℙ ∖ \{2\})) \land A /_{L} P = 1) \land x \in ℤ) \to (P ∥ (x^{2} - A) \to \neg P ∥ x)$
53	11 52	sylbid	$⊢ (((A \in ℤ \land P \in (ℙ ∖ \{2\})) \land A /_{L} P = 1) \land x \in ℤ) \to (x^{2} \mod P = A \mod P \to \neg P ∥ x)$
54	53	ancld	$⊢ (((A \in ℤ \land P \in (ℙ ∖ \{2\})) \land A /_{L} P = 1) \land x \in ℤ) \to (x^{2} \mod P = A \mod P \to (x^{2} \mod P = A \mod P \land \neg P ∥ x))$
55	54	reximdva	$⊢ ((A \in ℤ \land P \in (ℙ ∖ \{2\})) \land A /_{L} P = 1) \to (\exists x \in ℤ x^{2} \mod P = A \mod P \to \exists x \in ℤ (x^{2} \mod P = A \mod P \land \neg P ∥ x))$
56	2 55	mpd	$⊢ ((A \in ℤ \land P \in (ℙ ∖ \{2\})) \land A /_{L} P = 1) \to \exists x \in ℤ (x^{2} \mod P = A \mod P \land \neg P ∥ x)$
57	56	ex	$⊢ (A \in ℤ \land P \in (ℙ ∖ \{2\})) \to (A /_{L} P = 1 \to \exists x \in ℤ (x^{2} \mod P = A \mod P \land \neg P ∥ x))$

Metamath Proof Explorer

Theorem lgsqrmodndvds

Proof