Theorem lgsqr 27568

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 27552) and the number is a quadratic residue mod 𝑃 (it is -1 for nonresidues by the process of elimination from lgsabs1 27553). Given our definition of the Legendre symbol, this theorem is equivalent to Euler's criterion. (Contributed by Mario Carneiro, 15-Jun-2015.)

Assertion

Ref	Expression
lgsqr	⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})) → ((𝐴 /L 𝑃) = 1 ↔ (¬ 𝑃 ∥ 𝐴 ∧ ∃𝑥 ∈ ℤ 𝑃 ∥ ((𝑥↑2) − 𝐴))))

Distinct variable groups:   𝑥,𝐴   𝑥,𝑃

Proof of Theorem lgsqr

Step	Hyp	Ref	Expression
1		eldifi 4085	. . . . . . . . . . 11 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → 𝑃 ∈ ℙ)
2	1	adantl 487	. . . . . . . . . 10 ⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})) → 𝑃 ∈ ℙ)
3		prmz 16757	. . . . . . . . . 10 ⊢ (𝑃 ∈ ℙ → 𝑃 ∈ ℤ)
4	2, 3	syl 18	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})) → 𝑃 ∈ ℤ)
5		simpl 488	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})) → 𝐴 ∈ ℤ)
6	4, 5	gcdcomd 16596	. . . . . . . 8 ⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})) → (𝑃 gcd 𝐴) = (𝐴 gcd 𝑃))
7	6	eqeq1d 2767	. . . . . . 7 ⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})) → ((𝑃 gcd 𝐴) = 1 ↔ (𝐴 gcd 𝑃) = 1))
8		coprm 16794	. . . . . . . 8 ⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ) → (¬ 𝑃 ∥ 𝐴 ↔ (𝑃 gcd 𝐴) = 1))
9	2, 5, 8	syl2anc 596	. . . . . . 7 ⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})) → (¬ 𝑃 ∥ 𝐴 ↔ (𝑃 gcd 𝐴) = 1))
10		lgsne0 27552	. . . . . . . 8 ⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ ℤ) → ((𝐴 /L 𝑃) ≠ 0 ↔ (𝐴 gcd 𝑃) = 1))
11	5, 4, 10	syl2anc 596	. . . . . . 7 ⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})) → ((𝐴 /L 𝑃) ≠ 0 ↔ (𝐴 gcd 𝑃) = 1))
12	7, 9, 11	3bitr4d 314	. . . . . 6 ⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})) → (¬ 𝑃 ∥ 𝐴 ↔ (𝐴 /L 𝑃) ≠ 0))
13	12	necon4bbid 3001	. . . . 5 ⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})) → (𝑃 ∥ 𝐴 ↔ (𝐴 /L 𝑃) = 0))
14		0ne1 12329	. . . . . 6 ⊢ 0 ≠ 1
15		neeq1 3022	. . . . . 6 ⊢ ((𝐴 /L 𝑃) = 0 → ((𝐴 /L 𝑃) ≠ 1 ↔ 0 ≠ 1))
16	14, 15	mpbiri 261	. . . . 5 ⊢ ((𝐴 /L 𝑃) = 0 → (𝐴 /L 𝑃) ≠ 1)
17	13, 16	biimtrdi 256	. . . 4 ⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})) → (𝑃 ∥ 𝐴 → (𝐴 /L 𝑃) ≠ 1))
18	17	necon2bd 2976	. . 3 ⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})) → ((𝐴 /L 𝑃) = 1 → ¬ 𝑃 ∥ 𝐴))
19		lgsqrlem5 27567	. . . 4 ⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2}) ∧ (𝐴 /L 𝑃) = 1) → ∃𝑥 ∈ ℤ 𝑃 ∥ ((𝑥↑2) − 𝐴))
20	19	3expia 1139	. . 3 ⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})) → ((𝐴 /L 𝑃) = 1 → ∃𝑥 ∈ ℤ 𝑃 ∥ ((𝑥↑2) − 𝐴)))
21	18, 20	jcad 522	. 2 ⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})) → ((𝐴 /L 𝑃) = 1 → (¬ 𝑃 ∥ 𝐴 ∧ ∃𝑥 ∈ ℤ 𝑃 ∥ ((𝑥↑2) − 𝐴))))
22		simprl 783	. . . . . . . 8 ⊢ ((((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})) ∧ ¬ 𝑃 ∥ 𝐴) ∧ (𝑥 ∈ ℤ ∧ 𝑃 ∥ ((𝑥↑2) − 𝐴))) → 𝑥 ∈ ℤ)
23	22	zred 12718	. . . . . . 7 ⊢ ((((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})) ∧ ¬ 𝑃 ∥ 𝐴) ∧ (𝑥 ∈ ℤ ∧ 𝑃 ∥ ((𝑥↑2) − 𝐴))) → 𝑥 ∈ ℝ)
24		absresq 15379	. . . . . . 7 ⊢ (𝑥 ∈ ℝ → ((abs‘𝑥)↑2) = (𝑥↑2))
25	23, 24	syl 18	. . . . . 6 ⊢ ((((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})) ∧ ¬ 𝑃 ∥ 𝐴) ∧ (𝑥 ∈ ℤ ∧ 𝑃 ∥ ((𝑥↑2) − 𝐴))) → ((abs‘𝑥)↑2) = (𝑥↑2))
26	25	oveq1d 7434	. . . . 5 ⊢ ((((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})) ∧ ¬ 𝑃 ∥ 𝐴) ∧ (𝑥 ∈ ℤ ∧ 𝑃 ∥ ((𝑥↑2) − 𝐴))) → (((abs‘𝑥)↑2) /L 𝑃) = ((𝑥↑2) /L 𝑃))
27		simplr 781	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})) ∧ ¬ 𝑃 ∥ 𝐴) ∧ (𝑥 ∈ ℤ ∧ 𝑃 ∥ ((𝑥↑2) − 𝐴))) → ¬ 𝑃 ∥ 𝐴)
28	1	ad3antlr 744	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})) ∧ ¬ 𝑃 ∥ 𝐴) ∧ (𝑥 ∈ ℤ ∧ 𝑃 ∥ ((𝑥↑2) − 𝐴))) → 𝑃 ∈ ℙ)
29	28, 3	syl 18	. . . . . . . . . . . 12 ⊢ ((((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})) ∧ ¬ 𝑃 ∥ 𝐴) ∧ (𝑥 ∈ ℤ ∧ 𝑃 ∥ ((𝑥↑2) − 𝐴))) → 𝑃 ∈ ℤ)
30		zsqcl 14185	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ ℤ → (𝑥↑2) ∈ ℤ)
31	22, 30	syl 18	. . . . . . . . . . . 12 ⊢ ((((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})) ∧ ¬ 𝑃 ∥ 𝐴) ∧ (𝑥 ∈ ℤ ∧ 𝑃 ∥ ((𝑥↑2) − 𝐴))) → (𝑥↑2) ∈ ℤ)
32		simplll 787	. . . . . . . . . . . 12 ⊢ ((((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})) ∧ ¬ 𝑃 ∥ 𝐴) ∧ (𝑥 ∈ ℤ ∧ 𝑃 ∥ ((𝑥↑2) − 𝐴))) → 𝐴 ∈ ℤ)
33		simprr 785	. . . . . . . . . . . 12 ⊢ ((((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})) ∧ ¬ 𝑃 ∥ 𝐴) ∧ (𝑥 ∈ ℤ ∧ 𝑃 ∥ ((𝑥↑2) − 𝐴))) → 𝑃 ∥ ((𝑥↑2) − 𝐴))
34		dvdssub2 16383	. . . . . . . . . . . 12 ⊢ (((𝑃 ∈ ℤ ∧ (𝑥↑2) ∈ ℤ ∧ 𝐴 ∈ ℤ) ∧ 𝑃 ∥ ((𝑥↑2) − 𝐴)) → (𝑃 ∥ (𝑥↑2) ↔ 𝑃 ∥ 𝐴))
35	29, 31, 32, 33, 34	syl31anc 1400	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})) ∧ ¬ 𝑃 ∥ 𝐴) ∧ (𝑥 ∈ ℤ ∧ 𝑃 ∥ ((𝑥↑2) − 𝐴))) → (𝑃 ∥ (𝑥↑2) ↔ 𝑃 ∥ 𝐴))
36	27, 35	mtbird 328	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})) ∧ ¬ 𝑃 ∥ 𝐴) ∧ (𝑥 ∈ ℤ ∧ 𝑃 ∥ ((𝑥↑2) − 𝐴))) → ¬ 𝑃 ∥ (𝑥↑2))
37		2nn 12331	. . . . . . . . . . . 12 ⊢ 2 ∈ ℕ
38	37	a1i 11	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})) ∧ ¬ 𝑃 ∥ 𝐴) ∧ (𝑥 ∈ ℤ ∧ 𝑃 ∥ ((𝑥↑2) − 𝐴))) → 2 ∈ ℕ)
39		prmdvdsexp 16798	. . . . . . . . . . 11 ⊢ ((𝑃 ∈ ℙ ∧ 𝑥 ∈ ℤ ∧ 2 ∈ ℕ) → (𝑃 ∥ (𝑥↑2) ↔ 𝑃 ∥ 𝑥))
40	28, 22, 38, 39	syl3anc 1398	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})) ∧ ¬ 𝑃 ∥ 𝐴) ∧ (𝑥 ∈ ℤ ∧ 𝑃 ∥ ((𝑥↑2) − 𝐴))) → (𝑃 ∥ (𝑥↑2) ↔ 𝑃 ∥ 𝑥))
41	36, 40	mtbid 327	. . . . . . . . 9 ⊢ ((((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})) ∧ ¬ 𝑃 ∥ 𝐴) ∧ (𝑥 ∈ ℤ ∧ 𝑃 ∥ ((𝑥↑2) − 𝐴))) → ¬ 𝑃 ∥ 𝑥)
42		dvds0 16353	. . . . . . . . . . . 12 ⊢ (𝑃 ∈ ℤ → 𝑃 ∥ 0)
43	29, 42	syl 18	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})) ∧ ¬ 𝑃 ∥ 𝐴) ∧ (𝑥 ∈ ℤ ∧ 𝑃 ∥ ((𝑥↑2) − 𝐴))) → 𝑃 ∥ 0)
44		breq2 5115	. . . . . . . . . . 11 ⊢ (𝑥 = 0 → (𝑃 ∥ 𝑥 ↔ 𝑃 ∥ 0))
45	43, 44	syl5ibrcom 250	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})) ∧ ¬ 𝑃 ∥ 𝐴) ∧ (𝑥 ∈ ℤ ∧ 𝑃 ∥ ((𝑥↑2) − 𝐴))) → (𝑥 = 0 → 𝑃 ∥ 𝑥))
46	45	necon3bd 2974	. . . . . . . . 9 ⊢ ((((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})) ∧ ¬ 𝑃 ∥ 𝐴) ∧ (𝑥 ∈ ℤ ∧ 𝑃 ∥ ((𝑥↑2) − 𝐴))) → (¬ 𝑃 ∥ 𝑥 → 𝑥 ≠ 0))
47	41, 46	mpd 16	. . . . . . . 8 ⊢ ((((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})) ∧ ¬ 𝑃 ∥ 𝐴) ∧ (𝑥 ∈ ℤ ∧ 𝑃 ∥ ((𝑥↑2) − 𝐴))) → 𝑥 ≠ 0)
48		nnabscl 15403	. . . . . . . 8 ⊢ ((𝑥 ∈ ℤ ∧ 𝑥 ≠ 0) → (abs‘𝑥) ∈ ℕ)
49	22, 47, 48	syl2anc 596	. . . . . . 7 ⊢ ((((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})) ∧ ¬ 𝑃 ∥ 𝐴) ∧ (𝑥 ∈ ℤ ∧ 𝑃 ∥ ((𝑥↑2) − 𝐴))) → (abs‘𝑥) ∈ ℕ)
50	49	nnzd 12634	. . . . . 6 ⊢ ((((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})) ∧ ¬ 𝑃 ∥ 𝐴) ∧ (𝑥 ∈ ℤ ∧ 𝑃 ∥ ((𝑥↑2) − 𝐴))) → (abs‘𝑥) ∈ ℤ)
51	49	nnne0d 12303	. . . . . 6 ⊢ ((((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})) ∧ ¬ 𝑃 ∥ 𝐴) ∧ (𝑥 ∈ ℤ ∧ 𝑃 ∥ ((𝑥↑2) − 𝐴))) → (abs‘𝑥) ≠ 0)
52	50, 29	gcdcomd 16596	. . . . . . 7 ⊢ ((((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})) ∧ ¬ 𝑃 ∥ 𝐴) ∧ (𝑥 ∈ ℤ ∧ 𝑃 ∥ ((𝑥↑2) − 𝐴))) → ((abs‘𝑥) gcd 𝑃) = (𝑃 gcd (abs‘𝑥)))
53		dvdsabsb 16357	. . . . . . . . . 10 ⊢ ((𝑃 ∈ ℤ ∧ 𝑥 ∈ ℤ) → (𝑃 ∥ 𝑥 ↔ 𝑃 ∥ (abs‘𝑥)))
54	29, 22, 53	syl2anc 596	. . . . . . . . 9 ⊢ ((((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})) ∧ ¬ 𝑃 ∥ 𝐴) ∧ (𝑥 ∈ ℤ ∧ 𝑃 ∥ ((𝑥↑2) − 𝐴))) → (𝑃 ∥ 𝑥 ↔ 𝑃 ∥ (abs‘𝑥)))
55	41, 54	mtbid 327	. . . . . . . 8 ⊢ ((((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})) ∧ ¬ 𝑃 ∥ 𝐴) ∧ (𝑥 ∈ ℤ ∧ 𝑃 ∥ ((𝑥↑2) − 𝐴))) → ¬ 𝑃 ∥ (abs‘𝑥))
56		coprm 16794	. . . . . . . . 9 ⊢ ((𝑃 ∈ ℙ ∧ (abs‘𝑥) ∈ ℤ) → (¬ 𝑃 ∥ (abs‘𝑥) ↔ (𝑃 gcd (abs‘𝑥)) = 1))
57	28, 50, 56	syl2anc 596	. . . . . . . 8 ⊢ ((((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})) ∧ ¬ 𝑃 ∥ 𝐴) ∧ (𝑥 ∈ ℤ ∧ 𝑃 ∥ ((𝑥↑2) − 𝐴))) → (¬ 𝑃 ∥ (abs‘𝑥) ↔ (𝑃 gcd (abs‘𝑥)) = 1))
58	55, 57	mpbid 235	. . . . . . 7 ⊢ ((((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})) ∧ ¬ 𝑃 ∥ 𝐴) ∧ (𝑥 ∈ ℤ ∧ 𝑃 ∥ ((𝑥↑2) − 𝐴))) → (𝑃 gcd (abs‘𝑥)) = 1)
59	52, 58	eqtrd 2800	. . . . . 6 ⊢ ((((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})) ∧ ¬ 𝑃 ∥ 𝐴) ∧ (𝑥 ∈ ℤ ∧ 𝑃 ∥ ((𝑥↑2) − 𝐴))) → ((abs‘𝑥) gcd 𝑃) = 1)
60		lgssq 27554	. . . . . 6 ⊢ ((((abs‘𝑥) ∈ ℤ ∧ (abs‘𝑥) ≠ 0) ∧ 𝑃 ∈ ℤ ∧ ((abs‘𝑥) gcd 𝑃) = 1) → (((abs‘𝑥)↑2) /L 𝑃) = 1)
61	50, 51, 29, 59, 60	syl211anc 1403	. . . . 5 ⊢ ((((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})) ∧ ¬ 𝑃 ∥ 𝐴) ∧ (𝑥 ∈ ℤ ∧ 𝑃 ∥ ((𝑥↑2) − 𝐴))) → (((abs‘𝑥)↑2) /L 𝑃) = 1)
62		prmnn 16756	. . . . . . . . . 10 ⊢ (𝑃 ∈ ℙ → 𝑃 ∈ ℕ)
63	28, 62	syl 18	. . . . . . . . 9 ⊢ ((((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})) ∧ ¬ 𝑃 ∥ 𝐴) ∧ (𝑥 ∈ ℤ ∧ 𝑃 ∥ ((𝑥↑2) − 𝐴))) → 𝑃 ∈ ℕ)
64		moddvds 16345	. . . . . . . . 9 ⊢ ((𝑃 ∈ ℕ ∧ (𝑥↑2) ∈ ℤ ∧ 𝐴 ∈ ℤ) → (((𝑥↑2) mod 𝑃) = (𝐴 mod 𝑃) ↔ 𝑃 ∥ ((𝑥↑2) − 𝐴)))
65	63, 31, 32, 64	syl3anc 1398	. . . . . . . 8 ⊢ ((((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})) ∧ ¬ 𝑃 ∥ 𝐴) ∧ (𝑥 ∈ ℤ ∧ 𝑃 ∥ ((𝑥↑2) − 𝐴))) → (((𝑥↑2) mod 𝑃) = (𝐴 mod 𝑃) ↔ 𝑃 ∥ ((𝑥↑2) − 𝐴)))
66	33, 65	mpbird 260	. . . . . . 7 ⊢ ((((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})) ∧ ¬ 𝑃 ∥ 𝐴) ∧ (𝑥 ∈ ℤ ∧ 𝑃 ∥ ((𝑥↑2) − 𝐴))) → ((𝑥↑2) mod 𝑃) = (𝐴 mod 𝑃))
67	66	oveq1d 7434	. . . . . 6 ⊢ ((((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})) ∧ ¬ 𝑃 ∥ 𝐴) ∧ (𝑥 ∈ ℤ ∧ 𝑃 ∥ ((𝑥↑2) − 𝐴))) → (((𝑥↑2) mod 𝑃) /L 𝑃) = ((𝐴 mod 𝑃) /L 𝑃))
68		eldifsni 4760	. . . . . . . . . 10 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → 𝑃 ≠ 2)
69	68	ad3antlr 744	. . . . . . . . 9 ⊢ ((((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})) ∧ ¬ 𝑃 ∥ 𝐴) ∧ (𝑥 ∈ ℤ ∧ 𝑃 ∥ ((𝑥↑2) − 𝐴))) → 𝑃 ≠ 2)
70	69	necomd 3015	. . . . . . . 8 ⊢ ((((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})) ∧ ¬ 𝑃 ∥ 𝐴) ∧ (𝑥 ∈ ℤ ∧ 𝑃 ∥ ((𝑥↑2) − 𝐴))) → 2 ≠ 𝑃)
71		2z 12643	. . . . . . . . . 10 ⊢ 2 ∈ ℤ
72		uzid 12895	. . . . . . . . . 10 ⊢ (2 ∈ ℤ → 2 ∈ (ℤ≥‘2))
73	71, 72	ax-mp 5	. . . . . . . . 9 ⊢ 2 ∈ (ℤ≥‘2)
74		dvdsprm 16786	. . . . . . . . . 10 ⊢ ((2 ∈ (ℤ≥‘2) ∧ 𝑃 ∈ ℙ) → (2 ∥ 𝑃 ↔ 2 = 𝑃))
75	74	necon3bbid 2997	. . . . . . . . 9 ⊢ ((2 ∈ (ℤ≥‘2) ∧ 𝑃 ∈ ℙ) → (¬ 2 ∥ 𝑃 ↔ 2 ≠ 𝑃))
76	73, 28, 75	sylancr 599	. . . . . . . 8 ⊢ ((((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})) ∧ ¬ 𝑃 ∥ 𝐴) ∧ (𝑥 ∈ ℤ ∧ 𝑃 ∥ ((𝑥↑2) − 𝐴))) → (¬ 2 ∥ 𝑃 ↔ 2 ≠ 𝑃))
77	70, 76	mpbird 260	. . . . . . 7 ⊢ ((((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})) ∧ ¬ 𝑃 ∥ 𝐴) ∧ (𝑥 ∈ ℤ ∧ 𝑃 ∥ ((𝑥↑2) − 𝐴))) → ¬ 2 ∥ 𝑃)
78		lgsmod 27540	. . . . . . 7 ⊢ (((𝑥↑2) ∈ ℤ ∧ 𝑃 ∈ ℕ ∧ ¬ 2 ∥ 𝑃) → (((𝑥↑2) mod 𝑃) /L 𝑃) = ((𝑥↑2) /L 𝑃))
79	31, 63, 77, 78	syl3anc 1398	. . . . . 6 ⊢ ((((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})) ∧ ¬ 𝑃 ∥ 𝐴) ∧ (𝑥 ∈ ℤ ∧ 𝑃 ∥ ((𝑥↑2) − 𝐴))) → (((𝑥↑2) mod 𝑃) /L 𝑃) = ((𝑥↑2) /L 𝑃))
80		lgsmod 27540	. . . . . . 7 ⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ ℕ ∧ ¬ 2 ∥ 𝑃) → ((𝐴 mod 𝑃) /L 𝑃) = (𝐴 /L 𝑃))
81	32, 63, 77, 80	syl3anc 1398	. . . . . 6 ⊢ ((((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})) ∧ ¬ 𝑃 ∥ 𝐴) ∧ (𝑥 ∈ ℤ ∧ 𝑃 ∥ ((𝑥↑2) − 𝐴))) → ((𝐴 mod 𝑃) /L 𝑃) = (𝐴 /L 𝑃))
82	67, 79, 81	3eqtr3d 2808	. . . . 5 ⊢ ((((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})) ∧ ¬ 𝑃 ∥ 𝐴) ∧ (𝑥 ∈ ℤ ∧ 𝑃 ∥ ((𝑥↑2) − 𝐴))) → ((𝑥↑2) /L 𝑃) = (𝐴 /L 𝑃))
83	26, 61, 82	3eqtr3rd 2809	. . . 4 ⊢ ((((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})) ∧ ¬ 𝑃 ∥ 𝐴) ∧ (𝑥 ∈ ℤ ∧ 𝑃 ∥ ((𝑥↑2) − 𝐴))) → (𝐴 /L 𝑃) = 1)
84	83	rexlimdvaa 3169	. . 3 ⊢ (((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})) ∧ ¬ 𝑃 ∥ 𝐴) → (∃𝑥 ∈ ℤ 𝑃 ∥ ((𝑥↑2) − 𝐴) → (𝐴 /L 𝑃) = 1))
85	84	expimpd 459	. 2 ⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})) → ((¬ 𝑃 ∥ 𝐴 ∧ ∃𝑥 ∈ ℤ 𝑃 ∥ ((𝑥↑2) − 𝐴)) → (𝐴 /L 𝑃) = 1))
86	21, 85	impbid 215	1 ⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})) → ((𝐴 /L 𝑃) = 1 ↔ (¬ 𝑃 ∥ 𝐴 ∧ ∃𝑥 ∈ ℤ 𝑃 ∥ ((𝑥↑2) − 𝐴))))

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 401   = wceq 1570   ∈ wcel 2146   ≠ wne 2960  ∃wrex 3091   ∖ cdif 3903  {csn 4591   class class class wbr 5111  ‘cfv 6540  (class class class)co 7419  ℝcr 11116  0cc0 11117  1c1 11118   − cmin 11458  ℕcn 12250  2c2 12312  ℤcz 12608  ℤ_≥cuz 12880   mod cmo 13922  ↑cexp 14117  abscabs 15311   ∥ cdvds 16334   gcd cgcd 16576  ℙcprime 16753   /_L clgs 27511

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-10 2179  ax-11 2195  ax-12 2216  ax-ext 2737  ax-rep 5240  ax-sep 5259  ax-nul 5271  ax-pow 5338  ax-pr 5406  ax-un 7742  ax-cnex 11173  ax-resscn 11174  ax-1cn 11175  ax-icn 11176  ax-addcl 11177  ax-addrcl 11178  ax-mulcl 11179  ax-mulrcl 11180  ax-mulcom 11181  ax-addass 11182  ax-mulass 11183  ax-distr 11184  ax-i2m1 11185  ax-1ne0 11186  ax-1rid 11187  ax-rnegex 11188  ax-rrecex 11189  ax-cnre 11190  ax-pre-lttri 11191  ax-pre-lttrn 11192  ax-pre-ltadd 11193  ax-pre-mulgt0 11194  ax-pre-sup 11195  ax-addf 11196  ax-mulf 11197

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2569  df-eu 2599  df-clab 2744  df-cleq 2757  df-clel 2840  df-nfc 2914  df-ne 2961  df-nel 3067  df-ral 3082  df-rex 3092  df-rmo 3371  df-reu 3372  df-rab 3419  df-v 3459  df-sbc 3747  df-csb 3855  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-pss 3926  df-nul 4287  df-if 4490  df-pw 4566  df-sn 4592  df-pr 4594  df-tp 4596  df-op 4598  df-uni 4875  df-int 4915  df-iun 4960  df-iin 4961  df-br 5112  df-opab 5176  df-mpt 5195  df-tr 5221  df-id 5558  df-eprel 5563  df-po 5571  df-so 5572  df-fr 5616  df-se 5617  df-we 5618  df-xp 5669  df-rel 5670  df-cnv 5671  df-co 5672  df-dm 5673  df-rn 5674  df-res 5675  df-ima 5676  df-pred 6306  df-ord 6367  df-on 6368  df-lim 6369  df-suc 6370  df-iota 6496  df-fun 6542  df-fn 6543  df-f 6544  df-f1 6545  df-fo 6546  df-f1o 6547  df-fv 6548  df-isom 6549  df-riota 7376  df-ov 7422  df-oprab 7423  df-mpo 7424  df-of 7684  df-ofr 7685  df-om 7869  df-1st 7992  df-2nd 7993  df-supp 8163  df-tpos 8228  df-frecs 8284  df-wrecs 8315  df-recs 8364  df-rdg 8403  df-1o 8459  df-2o 8460  df-oadd 8463  df-er 8700  df-ec 8702  df-qs 8706  df-map 8832  df-pm 8833  df-ixp 8902  df-en 8950  df-dom 8951  df-sdom 8952  df-fin 8953  df-fsupp 9329  df-sup 9409  df-inf 9410  df-oi 9479  df-dju 9903  df-card 9941  df-pnf 11262  df-mnf 11263  df-xr 11264  df-ltxr 11265  df-le 11266  df-sub 11460  df-neg 11461  df-div 11889  df-nn 12251  df-2 12320  df-3 12321  df-4 12322  df-5 12323  df-6 12324  df-7 12325  df-8 12326  df-9 12327  df-n0 12522  df-xnn0 12595  df-z 12609  df-dec 12730  df-uz 12881  df-q 12991  df-rp 13035  df-fz 13554  df-fzo 13702  df-fl 13845  df-mod 13923  df-seq 14058  df-exp 14118  df-hash 14387  df-cj 15176  df-re 15177  df-im 15178  df-sqrt 15312  df-abs 15313  df-dvds 16335  df-gcd 16577  df-prm 16754  df-phi 16849  df-pc 16921  df-struct 17231  df-sets 17248  df-slot 17266  df-ndx 17278  df-base 17294  df-ress 17315  df-plusg 17347  df-mulr 17348  df-starv 17349  df-sca 17350  df-vsca 17351  df-ip 17352  df-tset 17353  df-ple 17354  df-ds 17356  df-unif 17357  df-hom 17358  df-cco 17359  df-0g 17518  df-gsum 17519  df-prds 17524  df-pws 17526  df-imas 17586  df-qus 17587  df-mre 17662  df-mrc 17663  df-acs 17665  df-mgm 18722  df-sgrp 18811  df-mnd 18827  df-mhm 18880  df-submnd 18881  df-grp 19049  df-minusg 19050  df-sbg 19051  df-mulg 19180  df-subg 19235  df-nsg 19236  df-eqg 19237  df-ghm 19330  df-cntz 19433  df-cmn 19898  df-abl 19899  df-mgp 20263  df-rng 20277  df-ur 20310  df-srg 20315  df-ring 20363  df-cring 20364  df-oppr 20467  df-dvdsr 20487  df-unit 20488  df-invr 20518  df-dvr 20531  df-rhm 20602  df-nzr 20662  df-subrng 20697  df-subrg 20721  df-rlreg 20845  df-domn 20846  df-idom 20847  df-drng 20881  df-field 20882  df-lmod 21035  df-lss 21105  df-lsp 21145  df-sra 21346  df-rgmod 21347  df-lidl 21384  df-rsp 21385  df-2idl 21441  df-cnfld 21575  df-zring 21649  df-zrh 21705  df-zn 21708  df-assa 22055  df-asp 22056  df-ascl 22057  df-psr 22111  df-mvr 22112  df-mpl 22113  df-opsr 22115  df-evls 22277  df-evl 22278  df-psr1 22392  df-vr1 22393  df-ply1 22394  df-coe1 22395  df-evl1 22528  df-mdeg 26265  df-deg1 26266  df-mon1 26341  df-uc1p 26342  df-q1p 26343  df-r1p 26344  df-lgs 27512

This theorem is used by:  lgsqrmod  27569  2sqlem11  27646  2sqblem  27648