Theorem lgseisenlem2 15663

Description: Lemma for lgseisen 15666. The function 𝑀 is an injection (and hence a bijection by the pigeonhole principle). (Contributed by Mario Carneiro, 17-Jun-2015.)

Hypotheses

Ref	Expression
lgseisen.1	⊢ (𝜑 → 𝑃 ∈ (ℙ ∖ {2}))
lgseisen.2	⊢ (𝜑 → 𝑄 ∈ (ℙ ∖ {2}))
lgseisen.3	⊢ (𝜑 → 𝑃 ≠ 𝑄)
lgseisen.4	⊢ 𝑅 = ((𝑄 · (2 · 𝑥)) mod 𝑃)
lgseisen.5	⊢ 𝑀 = (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ ((((-1↑𝑅) · 𝑅) mod 𝑃) / 2))
lgseisen.6	⊢ 𝑆 = ((𝑄 · (2 · 𝑦)) mod 𝑃)

Assertion

Ref	Expression
lgseisenlem2	⊢ (𝜑 → 𝑀:(1...((𝑃 − 1) / 2))–1-1-onto→(1...((𝑃 − 1) / 2)))

Distinct variable groups:   𝑥,𝑦,𝑃   𝜑,𝑥,𝑦   𝑦,𝑀   𝑥,𝑄,𝑦   𝑥,𝑆

Allowed substitution hints:   𝑅(𝑥,𝑦)   𝑆(𝑦)   𝑀(𝑥)

Proof of Theorem lgseisenlem2

Dummy variable 𝑧 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		lgseisen.1	. . . 4 ⊢ (𝜑 → 𝑃 ∈ (ℙ ∖ {2}))
2		lgseisen.2	. . . 4 ⊢ (𝜑 → 𝑄 ∈ (ℙ ∖ {2}))
3		lgseisen.3	. . . 4 ⊢ (𝜑 → 𝑃 ≠ 𝑄)
4		lgseisen.4	. . . 4 ⊢ 𝑅 = ((𝑄 · (2 · 𝑥)) mod 𝑃)
5		lgseisen.5	. . . 4 ⊢ 𝑀 = (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ ((((-1↑𝑅) · 𝑅) mod 𝑃) / 2))
6	1, 2, 3, 4, 5	lgseisenlem1 15662	. . 3 ⊢ (𝜑 → 𝑀:(1...((𝑃 − 1) / 2))⟶(1...((𝑃 − 1) / 2)))
7		oveq2 5975	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝑦 → (2 · 𝑥) = (2 · 𝑦))
8	7	oveq2d 5983	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝑦 → (𝑄 · (2 · 𝑥)) = (𝑄 · (2 · 𝑦)))
9	8	oveq1d 5982	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑦 → ((𝑄 · (2 · 𝑥)) mod 𝑃) = ((𝑄 · (2 · 𝑦)) mod 𝑃))
10		lgseisen.6	. . . . . . . . . . . . 13 ⊢ 𝑆 = ((𝑄 · (2 · 𝑦)) mod 𝑃)
11	9, 4, 10	3eqtr4g 2265	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑦 → 𝑅 = 𝑆)
12	11	oveq2d 5983	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑦 → (-1↑𝑅) = (-1↑𝑆))
13	12, 11	oveq12d 5985	. . . . . . . . . 10 ⊢ (𝑥 = 𝑦 → ((-1↑𝑅) · 𝑅) = ((-1↑𝑆) · 𝑆))
14	13	oveq1d 5982	. . . . . . . . 9 ⊢ (𝑥 = 𝑦 → (((-1↑𝑅) · 𝑅) mod 𝑃) = (((-1↑𝑆) · 𝑆) mod 𝑃))
15	14	oveq1d 5982	. . . . . . . 8 ⊢ (𝑥 = 𝑦 → ((((-1↑𝑅) · 𝑅) mod 𝑃) / 2) = ((((-1↑𝑆) · 𝑆) mod 𝑃) / 2))
16		simprl 529	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → 𝑦 ∈ (1...((𝑃 − 1) / 2)))
17		neg1z 9439	. . . . . . . . . . . . 13 ⊢ -1 ∈ ℤ
18	2	eldifad 3185	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝑄 ∈ ℙ)
19		prmnn 12547	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑄 ∈ ℙ → 𝑄 ∈ ℕ)
20	18, 19	syl 14	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝑄 ∈ ℕ)
21	20	adantr 276	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → 𝑄 ∈ ℕ)
22		2nn 9233	. . . . . . . . . . . . . . . . . . 19 ⊢ 2 ∈ ℕ
23	22	a1i 9	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → 2 ∈ ℕ)
24		elfznn 10211	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 ∈ (1...((𝑃 − 1) / 2)) → 𝑦 ∈ ℕ)
25	24	ad2antrl 490	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → 𝑦 ∈ ℕ)
26	23, 25	nnmulcld 9120	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → (2 · 𝑦) ∈ ℕ)
27	21, 26	nnmulcld 9120	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → (𝑄 · (2 · 𝑦)) ∈ ℕ)
28	27	nnzd 9529	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → (𝑄 · (2 · 𝑦)) ∈ ℤ)
29	1	eldifad 3185	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝑃 ∈ ℙ)
30		prmnn 12547	. . . . . . . . . . . . . . . . 17 ⊢ (𝑃 ∈ ℙ → 𝑃 ∈ ℕ)
31	29, 30	syl 14	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑃 ∈ ℕ)
32	31	adantr 276	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → 𝑃 ∈ ℕ)
33	28, 32	zmodcld 10527	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → ((𝑄 · (2 · 𝑦)) mod 𝑃) ∈ ℕ0)
34	10, 33	eqeltrid 2294	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → 𝑆 ∈ ℕ0)
35		zexpcl 10736	. . . . . . . . . . . . 13 ⊢ ((-1 ∈ ℤ ∧ 𝑆 ∈ ℕ0) → (-1↑𝑆) ∈ ℤ)
36	17, 34, 35	sylancr 414	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → (-1↑𝑆) ∈ ℤ)
37	34	nn0zd 9528	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → 𝑆 ∈ ℤ)
38	36, 37	zmulcld 9536	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → ((-1↑𝑆) · 𝑆) ∈ ℤ)
39	38, 32	zmodcld 10527	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → (((-1↑𝑆) · 𝑆) mod 𝑃) ∈ ℕ0)
40	39	nn0zd 9528	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → (((-1↑𝑆) · 𝑆) mod 𝑃) ∈ ℤ)
41		znq 9780	. . . . . . . . 9 ⊢ (((((-1↑𝑆) · 𝑆) mod 𝑃) ∈ ℤ ∧ 2 ∈ ℕ) → ((((-1↑𝑆) · 𝑆) mod 𝑃) / 2) ∈ ℚ)
42	40, 22, 41	sylancl 413	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → ((((-1↑𝑆) · 𝑆) mod 𝑃) / 2) ∈ ℚ)
43	5, 15, 16, 42	fvmptd3 5696	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → (𝑀‘𝑦) = ((((-1↑𝑆) · 𝑆) mod 𝑃) / 2))
44		simprr 531	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → 𝑥 ∈ (1...((𝑃 − 1) / 2)))
45		elfznn 10211	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 ∈ (1...((𝑃 − 1) / 2)) → 𝑥 ∈ ℕ)
46	45	ad2antll 491	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → 𝑥 ∈ ℕ)
47	23, 46	nnmulcld 9120	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → (2 · 𝑥) ∈ ℕ)
48	21, 47	nnmulcld 9120	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → (𝑄 · (2 · 𝑥)) ∈ ℕ)
49	48	nnzd 9529	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → (𝑄 · (2 · 𝑥)) ∈ ℤ)
50	49, 32	zmodcld 10527	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → ((𝑄 · (2 · 𝑥)) mod 𝑃) ∈ ℕ0)
51	4, 50	eqeltrid 2294	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → 𝑅 ∈ ℕ0)
52		zexpcl 10736	. . . . . . . . . . . . . 14 ⊢ ((-1 ∈ ℤ ∧ 𝑅 ∈ ℕ0) → (-1↑𝑅) ∈ ℤ)
53	17, 51, 52	sylancr 414	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → (-1↑𝑅) ∈ ℤ)
54	51	nn0zd 9528	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → 𝑅 ∈ ℤ)
55	53, 54	zmulcld 9536	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → ((-1↑𝑅) · 𝑅) ∈ ℤ)
56	55, 32	zmodcld 10527	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → (((-1↑𝑅) · 𝑅) mod 𝑃) ∈ ℕ0)
57	56	nn0zd 9528	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → (((-1↑𝑅) · 𝑅) mod 𝑃) ∈ ℤ)
58		znq 9780	. . . . . . . . . 10 ⊢ (((((-1↑𝑅) · 𝑅) mod 𝑃) ∈ ℤ ∧ 2 ∈ ℕ) → ((((-1↑𝑅) · 𝑅) mod 𝑃) / 2) ∈ ℚ)
59	57, 22, 58	sylancl 413	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → ((((-1↑𝑅) · 𝑅) mod 𝑃) / 2) ∈ ℚ)
60	59	elexd 2790	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → ((((-1↑𝑅) · 𝑅) mod 𝑃) / 2) ∈ V)
61	5	fvmpt2 5686	. . . . . . . 8 ⊢ ((𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ ((((-1↑𝑅) · 𝑅) mod 𝑃) / 2) ∈ V) → (𝑀‘𝑥) = ((((-1↑𝑅) · 𝑅) mod 𝑃) / 2))
62	44, 60, 61	syl2anc 411	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → (𝑀‘𝑥) = ((((-1↑𝑅) · 𝑅) mod 𝑃) / 2))
63	43, 62	eqeq12d 2222	. . . . . 6 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → ((𝑀‘𝑦) = (𝑀‘𝑥) ↔ ((((-1↑𝑆) · 𝑆) mod 𝑃) / 2) = ((((-1↑𝑅) · 𝑅) mod 𝑃) / 2)))
64	2	adantr 276	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → 𝑄 ∈ (ℙ ∖ {2}))
65	64	eldifad 3185	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → 𝑄 ∈ ℙ)
66		prmz 12548	. . . . . . . . . . . . . . . . 17 ⊢ (𝑄 ∈ ℙ → 𝑄 ∈ ℤ)
67	65, 66	syl 14	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → 𝑄 ∈ ℤ)
68		2z 9435	. . . . . . . . . . . . . . . . 17 ⊢ 2 ∈ ℤ
69		elfzelz 10182	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 ∈ (1...((𝑃 − 1) / 2)) → 𝑦 ∈ ℤ)
70	69	ad2antrl 490	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → 𝑦 ∈ ℤ)
71		zmulcl 9461	. . . . . . . . . . . . . . . . 17 ⊢ ((2 ∈ ℤ ∧ 𝑦 ∈ ℤ) → (2 · 𝑦) ∈ ℤ)
72	68, 70, 71	sylancr 414	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → (2 · 𝑦) ∈ ℤ)
73	67, 72	zmulcld 9536	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → (𝑄 · (2 · 𝑦)) ∈ ℤ)
74	1	adantr 276	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → 𝑃 ∈ (ℙ ∖ {2}))
75	74	eldifad 3185	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → 𝑃 ∈ ℙ)
76	75, 30	syl 14	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → 𝑃 ∈ ℕ)
77	73, 76	zmodcld 10527	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → ((𝑄 · (2 · 𝑦)) mod 𝑃) ∈ ℕ0)
78	10, 77	eqeltrid 2294	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → 𝑆 ∈ ℕ0)
79	78	nn0zd 9528	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → 𝑆 ∈ ℤ)
80		m1expcl 10744	. . . . . . . . . . . 12 ⊢ (𝑆 ∈ ℤ → (-1↑𝑆) ∈ ℤ)
81	79, 80	syl 14	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → (-1↑𝑆) ∈ ℤ)
82	81, 79	zmulcld 9536	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → ((-1↑𝑆) · 𝑆) ∈ ℤ)
83	82, 76	zmodcld 10527	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → (((-1↑𝑆) · 𝑆) mod 𝑃) ∈ ℕ0)
84	83	nn0cnd 9385	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → (((-1↑𝑆) · 𝑆) mod 𝑃) ∈ ℂ)
85		elfzelz 10182	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 ∈ (1...((𝑃 − 1) / 2)) → 𝑥 ∈ ℤ)
86	85	ad2antll 491	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → 𝑥 ∈ ℤ)
87		zmulcl 9461	. . . . . . . . . . . . . . . . 17 ⊢ ((2 ∈ ℤ ∧ 𝑥 ∈ ℤ) → (2 · 𝑥) ∈ ℤ)
88	68, 86, 87	sylancr 414	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → (2 · 𝑥) ∈ ℤ)
89	67, 88	zmulcld 9536	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → (𝑄 · (2 · 𝑥)) ∈ ℤ)
90	89, 76	zmodcld 10527	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → ((𝑄 · (2 · 𝑥)) mod 𝑃) ∈ ℕ0)
91	4, 90	eqeltrid 2294	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → 𝑅 ∈ ℕ0)
92	91	nn0zd 9528	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → 𝑅 ∈ ℤ)
93		m1expcl 10744	. . . . . . . . . . . 12 ⊢ (𝑅 ∈ ℤ → (-1↑𝑅) ∈ ℤ)
94	92, 93	syl 14	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → (-1↑𝑅) ∈ ℤ)
95	94, 92	zmulcld 9536	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → ((-1↑𝑅) · 𝑅) ∈ ℤ)
96	95, 76	zmodcld 10527	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → (((-1↑𝑅) · 𝑅) mod 𝑃) ∈ ℕ0)
97	96	nn0cnd 9385	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → (((-1↑𝑅) · 𝑅) mod 𝑃) ∈ ℂ)
98		2cnd 9144	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → 2 ∈ ℂ)
99	23	nnap0d 9117	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → 2 # 0)
100		div11ap 8808	. . . . . . . 8 ⊢ (((((-1↑𝑆) · 𝑆) mod 𝑃) ∈ ℂ ∧ (((-1↑𝑅) · 𝑅) mod 𝑃) ∈ ℂ ∧ (2 ∈ ℂ ∧ 2 # 0)) → (((((-1↑𝑆) · 𝑆) mod 𝑃) / 2) = ((((-1↑𝑅) · 𝑅) mod 𝑃) / 2) ↔ (((-1↑𝑆) · 𝑆) mod 𝑃) = (((-1↑𝑅) · 𝑅) mod 𝑃)))
101	84, 97, 98, 99, 100	syl112anc 1254	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → (((((-1↑𝑆) · 𝑆) mod 𝑃) / 2) = ((((-1↑𝑅) · 𝑅) mod 𝑃) / 2) ↔ (((-1↑𝑆) · 𝑆) mod 𝑃) = (((-1↑𝑅) · 𝑅) mod 𝑃)))
102		nnq 9789	. . . . . . . . . . 11 ⊢ (𝑃 ∈ ℕ → 𝑃 ∈ ℚ)
103	32, 102	syl 14	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → 𝑃 ∈ ℚ)
104	32	nngt0d 9115	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → 0 < 𝑃)
105		eqidd 2208	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → ((-1↑𝑆) mod 𝑃) = ((-1↑𝑆) mod 𝑃))
106	10	oveq1i 5977	. . . . . . . . . . 11 ⊢ (𝑆 mod 𝑃) = (((𝑄 · (2 · 𝑦)) mod 𝑃) mod 𝑃)
107		nnq 9789	. . . . . . . . . . . . 13 ⊢ ((𝑄 · (2 · 𝑦)) ∈ ℕ → (𝑄 · (2 · 𝑦)) ∈ ℚ)
108	27, 107	syl 14	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → (𝑄 · (2 · 𝑦)) ∈ ℚ)
109	31, 102	syl 14	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑃 ∈ ℚ)
110	109	adantr 276	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → 𝑃 ∈ ℚ)
111		modqabs2 10540	. . . . . . . . . . . 12 ⊢ (((𝑄 · (2 · 𝑦)) ∈ ℚ ∧ 𝑃 ∈ ℚ ∧ 0 < 𝑃) → (((𝑄 · (2 · 𝑦)) mod 𝑃) mod 𝑃) = ((𝑄 · (2 · 𝑦)) mod 𝑃))
112	108, 110, 104, 111	syl3anc 1250	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → (((𝑄 · (2 · 𝑦)) mod 𝑃) mod 𝑃) = ((𝑄 · (2 · 𝑦)) mod 𝑃))
113	106, 112	eqtrid 2252	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → (𝑆 mod 𝑃) = ((𝑄 · (2 · 𝑦)) mod 𝑃))
114	36, 36, 37, 28, 103, 104, 105, 113	modqmul12d 10560	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → (((-1↑𝑆) · 𝑆) mod 𝑃) = (((-1↑𝑆) · (𝑄 · (2 · 𝑦))) mod 𝑃))
115		eqidd 2208	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → ((-1↑𝑅) mod 𝑃) = ((-1↑𝑅) mod 𝑃))
116	4	oveq1i 5977	. . . . . . . . . . 11 ⊢ (𝑅 mod 𝑃) = (((𝑄 · (2 · 𝑥)) mod 𝑃) mod 𝑃)
117		nnq 9789	. . . . . . . . . . . . 13 ⊢ ((𝑄 · (2 · 𝑥)) ∈ ℕ → (𝑄 · (2 · 𝑥)) ∈ ℚ)
118	48, 117	syl 14	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → (𝑄 · (2 · 𝑥)) ∈ ℚ)
119		modqabs2 10540	. . . . . . . . . . . 12 ⊢ (((𝑄 · (2 · 𝑥)) ∈ ℚ ∧ 𝑃 ∈ ℚ ∧ 0 < 𝑃) → (((𝑄 · (2 · 𝑥)) mod 𝑃) mod 𝑃) = ((𝑄 · (2 · 𝑥)) mod 𝑃))
120	118, 110, 104, 119	syl3anc 1250	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → (((𝑄 · (2 · 𝑥)) mod 𝑃) mod 𝑃) = ((𝑄 · (2 · 𝑥)) mod 𝑃))
121	116, 120	eqtrid 2252	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → (𝑅 mod 𝑃) = ((𝑄 · (2 · 𝑥)) mod 𝑃))
122	53, 53, 54, 49, 110, 104, 115, 121	modqmul12d 10560	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → (((-1↑𝑅) · 𝑅) mod 𝑃) = (((-1↑𝑅) · (𝑄 · (2 · 𝑥))) mod 𝑃))
123	114, 122	eqeq12d 2222	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → ((((-1↑𝑆) · 𝑆) mod 𝑃) = (((-1↑𝑅) · 𝑅) mod 𝑃) ↔ (((-1↑𝑆) · (𝑄 · (2 · 𝑦))) mod 𝑃) = (((-1↑𝑅) · (𝑄 · (2 · 𝑥))) mod 𝑃)))
124	81, 73	zmulcld 9536	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → ((-1↑𝑆) · (𝑄 · (2 · 𝑦))) ∈ ℤ)
125	94, 89	zmulcld 9536	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → ((-1↑𝑅) · (𝑄 · (2 · 𝑥))) ∈ ℤ)
126		moddvds 12225	. . . . . . . . . 10 ⊢ ((𝑃 ∈ ℕ ∧ ((-1↑𝑆) · (𝑄 · (2 · 𝑦))) ∈ ℤ ∧ ((-1↑𝑅) · (𝑄 · (2 · 𝑥))) ∈ ℤ) → ((((-1↑𝑆) · (𝑄 · (2 · 𝑦))) mod 𝑃) = (((-1↑𝑅) · (𝑄 · (2 · 𝑥))) mod 𝑃) ↔ 𝑃 ∥ (((-1↑𝑆) · (𝑄 · (2 · 𝑦))) − ((-1↑𝑅) · (𝑄 · (2 · 𝑥))))))
127	76, 124, 125, 126	syl3anc 1250	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → ((((-1↑𝑆) · (𝑄 · (2 · 𝑦))) mod 𝑃) = (((-1↑𝑅) · (𝑄 · (2 · 𝑥))) mod 𝑃) ↔ 𝑃 ∥ (((-1↑𝑆) · (𝑄 · (2 · 𝑦))) − ((-1↑𝑅) · (𝑄 · (2 · 𝑥))))))
128	67	zcnd 9531	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → 𝑄 ∈ ℂ)
129	81, 72	zmulcld 9536	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → ((-1↑𝑆) · (2 · 𝑦)) ∈ ℤ)
130	129	zcnd 9531	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → ((-1↑𝑆) · (2 · 𝑦)) ∈ ℂ)
131	94, 88	zmulcld 9536	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → ((-1↑𝑅) · (2 · 𝑥)) ∈ ℤ)
132	131	zcnd 9531	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → ((-1↑𝑅) · (2 · 𝑥)) ∈ ℂ)
133	128, 130, 132	subdid 8521	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → (𝑄 · (((-1↑𝑆) · (2 · 𝑦)) − ((-1↑𝑅) · (2 · 𝑥)))) = ((𝑄 · ((-1↑𝑆) · (2 · 𝑦))) − (𝑄 · ((-1↑𝑅) · (2 · 𝑥)))))
134	81	zcnd 9531	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → (-1↑𝑆) ∈ ℂ)
135	72	zcnd 9531	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → (2 · 𝑦) ∈ ℂ)
136	128, 134, 135	mul12d 8259	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → (𝑄 · ((-1↑𝑆) · (2 · 𝑦))) = ((-1↑𝑆) · (𝑄 · (2 · 𝑦))))
137	94	zcnd 9531	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → (-1↑𝑅) ∈ ℂ)
138	88	zcnd 9531	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → (2 · 𝑥) ∈ ℂ)
139	128, 137, 138	mul12d 8259	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → (𝑄 · ((-1↑𝑅) · (2 · 𝑥))) = ((-1↑𝑅) · (𝑄 · (2 · 𝑥))))
140	136, 139	oveq12d 5985	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → ((𝑄 · ((-1↑𝑆) · (2 · 𝑦))) − (𝑄 · ((-1↑𝑅) · (2 · 𝑥)))) = (((-1↑𝑆) · (𝑄 · (2 · 𝑦))) − ((-1↑𝑅) · (𝑄 · (2 · 𝑥)))))
141	133, 140	eqtrd 2240	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → (𝑄 · (((-1↑𝑆) · (2 · 𝑦)) − ((-1↑𝑅) · (2 · 𝑥)))) = (((-1↑𝑆) · (𝑄 · (2 · 𝑦))) − ((-1↑𝑅) · (𝑄 · (2 · 𝑥)))))
142	141	breq2d 4071	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → (𝑃 ∥ (𝑄 · (((-1↑𝑆) · (2 · 𝑦)) − ((-1↑𝑅) · (2 · 𝑥)))) ↔ 𝑃 ∥ (((-1↑𝑆) · (𝑄 · (2 · 𝑦))) − ((-1↑𝑅) · (𝑄 · (2 · 𝑥))))))
143	3	adantr 276	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → 𝑃 ≠ 𝑄)
144		prmrp 12582	. . . . . . . . . . . . . 14 ⊢ ((𝑃 ∈ ℙ ∧ 𝑄 ∈ ℙ) → ((𝑃 gcd 𝑄) = 1 ↔ 𝑃 ≠ 𝑄))
145	75, 65, 144	syl2anc 411	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → ((𝑃 gcd 𝑄) = 1 ↔ 𝑃 ≠ 𝑄))
146	143, 145	mpbird 167	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → (𝑃 gcd 𝑄) = 1)
147		prmz 12548	. . . . . . . . . . . . . 14 ⊢ (𝑃 ∈ ℙ → 𝑃 ∈ ℤ)
148	75, 147	syl 14	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → 𝑃 ∈ ℤ)
149	129, 131	zsubcld 9535	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → (((-1↑𝑆) · (2 · 𝑦)) − ((-1↑𝑅) · (2 · 𝑥))) ∈ ℤ)
150		coprmdvds 12529	. . . . . . . . . . . . 13 ⊢ ((𝑃 ∈ ℤ ∧ 𝑄 ∈ ℤ ∧ (((-1↑𝑆) · (2 · 𝑦)) − ((-1↑𝑅) · (2 · 𝑥))) ∈ ℤ) → ((𝑃 ∥ (𝑄 · (((-1↑𝑆) · (2 · 𝑦)) − ((-1↑𝑅) · (2 · 𝑥)))) ∧ (𝑃 gcd 𝑄) = 1) → 𝑃 ∥ (((-1↑𝑆) · (2 · 𝑦)) − ((-1↑𝑅) · (2 · 𝑥)))))
151	148, 67, 149, 150	syl3anc 1250	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → ((𝑃 ∥ (𝑄 · (((-1↑𝑆) · (2 · 𝑦)) − ((-1↑𝑅) · (2 · 𝑥)))) ∧ (𝑃 gcd 𝑄) = 1) → 𝑃 ∥ (((-1↑𝑆) · (2 · 𝑦)) − ((-1↑𝑅) · (2 · 𝑥)))))
152	146, 151	mpan2d 428	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → (𝑃 ∥ (𝑄 · (((-1↑𝑆) · (2 · 𝑦)) − ((-1↑𝑅) · (2 · 𝑥)))) → 𝑃 ∥ (((-1↑𝑆) · (2 · 𝑦)) − ((-1↑𝑅) · (2 · 𝑥)))))
153		dvdsmultr2 12259	. . . . . . . . . . . 12 ⊢ ((𝑃 ∈ ℤ ∧ (-1↑𝑅) ∈ ℤ ∧ (((-1↑𝑆) · (2 · 𝑦)) − ((-1↑𝑅) · (2 · 𝑥))) ∈ ℤ) → (𝑃 ∥ (((-1↑𝑆) · (2 · 𝑦)) − ((-1↑𝑅) · (2 · 𝑥))) → 𝑃 ∥ ((-1↑𝑅) · (((-1↑𝑆) · (2 · 𝑦)) − ((-1↑𝑅) · (2 · 𝑥))))))
154	148, 94, 149, 153	syl3anc 1250	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → (𝑃 ∥ (((-1↑𝑆) · (2 · 𝑦)) − ((-1↑𝑅) · (2 · 𝑥))) → 𝑃 ∥ ((-1↑𝑅) · (((-1↑𝑆) · (2 · 𝑦)) − ((-1↑𝑅) · (2 · 𝑥))))))
155	137, 130, 132	subdid 8521	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → ((-1↑𝑅) · (((-1↑𝑆) · (2 · 𝑦)) − ((-1↑𝑅) · (2 · 𝑥)))) = (((-1↑𝑅) · ((-1↑𝑆) · (2 · 𝑦))) − ((-1↑𝑅) · ((-1↑𝑅) · (2 · 𝑥)))))
156		neg1cn 9176	. . . . . . . . . . . . . . . . . . 19 ⊢ -1 ∈ ℂ
157	156	a1i 9	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → -1 ∈ ℂ)
158	157, 78, 91	expaddd 10857	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → (-1↑(𝑅 + 𝑆)) = ((-1↑𝑅) · (-1↑𝑆)))
159	158	oveq1d 5982	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → ((-1↑(𝑅 + 𝑆)) · (2 · 𝑦)) = (((-1↑𝑅) · (-1↑𝑆)) · (2 · 𝑦)))
160	137, 134, 135	mulassd 8131	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → (((-1↑𝑅) · (-1↑𝑆)) · (2 · 𝑦)) = ((-1↑𝑅) · ((-1↑𝑆) · (2 · 𝑦))))
161	159, 160	eqtr2d 2241	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → ((-1↑𝑅) · ((-1↑𝑆) · (2 · 𝑦))) = ((-1↑(𝑅 + 𝑆)) · (2 · 𝑦)))
162		ax-1cn 8053	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ 1 ∈ ℂ
163		1ap0 8698	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ 1 # 0
164		divneg2ap 8844	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((1 ∈ ℂ ∧ 1 ∈ ℂ ∧ 1 # 0) → -(1 / 1) = (1 / -1))
165	162, 162, 163, 164	mp3an 1350	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ -(1 / 1) = (1 / -1)
166		1div1e1 8812	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (1 / 1) = 1
167	166	negeqi 8301	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ -(1 / 1) = -1
168	165, 167	eqtr3i 2230	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (1 / -1) = -1
169	168	oveq1i 5977	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((1 / -1)↑𝑅) = (-1↑𝑅)
170		neg1ap0 9180	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ -1 # 0
171	170	a1i 9	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → -1 # 0)
172	157, 171, 54	exprecapd 10863	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → ((1 / -1)↑𝑅) = (1 / (-1↑𝑅)))
173	169, 172	eqtr3id 2254	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → (-1↑𝑅) = (1 / (-1↑𝑅)))
174	173	oveq2d 5983	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → ((-1↑𝑅) · (-1↑𝑅)) = ((-1↑𝑅) · (1 / (-1↑𝑅))))
175	157, 171, 54	expap0d 10861	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → (-1↑𝑅) # 0)
176	137, 175	recidapd 8891	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → ((-1↑𝑅) · (1 / (-1↑𝑅))) = 1)
177	174, 176	eqtrd 2240	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → ((-1↑𝑅) · (-1↑𝑅)) = 1)
178	177	oveq1d 5982	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → (((-1↑𝑅) · (-1↑𝑅)) · (2 · 𝑥)) = (1 · (2 · 𝑥)))
179	137, 137, 138	mulassd 8131	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → (((-1↑𝑅) · (-1↑𝑅)) · (2 · 𝑥)) = ((-1↑𝑅) · ((-1↑𝑅) · (2 · 𝑥))))
180	138	mullidd 8125	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → (1 · (2 · 𝑥)) = (2 · 𝑥))
181	178, 179, 180	3eqtr3d 2248	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → ((-1↑𝑅) · ((-1↑𝑅) · (2 · 𝑥))) = (2 · 𝑥))
182	161, 181	oveq12d 5985	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → (((-1↑𝑅) · ((-1↑𝑆) · (2 · 𝑦))) − ((-1↑𝑅) · ((-1↑𝑅) · (2 · 𝑥)))) = (((-1↑(𝑅 + 𝑆)) · (2 · 𝑦)) − (2 · 𝑥)))
183	155, 182	eqtrd 2240	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → ((-1↑𝑅) · (((-1↑𝑆) · (2 · 𝑦)) − ((-1↑𝑅) · (2 · 𝑥)))) = (((-1↑(𝑅 + 𝑆)) · (2 · 𝑦)) − (2 · 𝑥)))
184	183	breq2d 4071	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → (𝑃 ∥ ((-1↑𝑅) · (((-1↑𝑆) · (2 · 𝑦)) − ((-1↑𝑅) · (2 · 𝑥)))) ↔ 𝑃 ∥ (((-1↑(𝑅 + 𝑆)) · (2 · 𝑦)) − (2 · 𝑥))))
185		eqcom 2209	. . . . . . . . . . . . . . . . 17 ⊢ (((-1 · (2 · 𝑦)) mod 𝑃) = ((2 · 𝑥) mod 𝑃) ↔ ((2 · 𝑥) mod 𝑃) = ((-1 · (2 · 𝑦)) mod 𝑃))
186	135	mulm1d 8517	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → (-1 · (2 · 𝑦)) = -(2 · 𝑦))
187	186	oveq1d 5982	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → ((-1 · (2 · 𝑦)) mod 𝑃) = (-(2 · 𝑦) mod 𝑃))
188	187	eqeq2d 2219	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → (((2 · 𝑥) mod 𝑃) = ((-1 · (2 · 𝑦)) mod 𝑃) ↔ ((2 · 𝑥) mod 𝑃) = (-(2 · 𝑦) mod 𝑃)))
189	185, 188	bitrid 192	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → (((-1 · (2 · 𝑦)) mod 𝑃) = ((2 · 𝑥) mod 𝑃) ↔ ((2 · 𝑥) mod 𝑃) = (-(2 · 𝑦) mod 𝑃)))
190	72	znegcld 9532	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → -(2 · 𝑦) ∈ ℤ)
191		moddvds 12225	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑃 ∈ ℕ ∧ (2 · 𝑥) ∈ ℤ ∧ -(2 · 𝑦) ∈ ℤ) → (((2 · 𝑥) mod 𝑃) = (-(2 · 𝑦) mod 𝑃) ↔ 𝑃 ∥ ((2 · 𝑥) − -(2 · 𝑦))))
192	76, 88, 190, 191	syl3anc 1250	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → (((2 · 𝑥) mod 𝑃) = (-(2 · 𝑦) mod 𝑃) ↔ 𝑃 ∥ ((2 · 𝑥) − -(2 · 𝑦))))
193	46, 25	nnaddcld 9119	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → (𝑥 + 𝑦) ∈ ℕ)
194	46	nnred 9084	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → 𝑥 ∈ ℝ)
195	70	zred 9530	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → 𝑦 ∈ ℝ)
196		oddprm 12697	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → ((𝑃 − 1) / 2) ∈ ℕ)
197	74, 196	syl 14	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → ((𝑃 − 1) / 2) ∈ ℕ)
198	197	nnred 9084	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → ((𝑃 − 1) / 2) ∈ ℝ)
199		elfzle2 10185	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑥 ∈ (1...((𝑃 − 1) / 2)) → 𝑥 ≤ ((𝑃 − 1) / 2))
200	199	ad2antll 491	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → 𝑥 ≤ ((𝑃 − 1) / 2))
201		elfzle2 10185	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑦 ∈ (1...((𝑃 − 1) / 2)) → 𝑦 ≤ ((𝑃 − 1) / 2))
202	201	ad2antrl 490	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → 𝑦 ≤ ((𝑃 − 1) / 2))
203	194, 195, 198, 198, 200, 202	le2addd 8671	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → (𝑥 + 𝑦) ≤ (((𝑃 − 1) / 2) + ((𝑃 − 1) / 2)))
204	76	nnred 9084	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → 𝑃 ∈ ℝ)
205		peano2rem 8374	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑃 ∈ ℝ → (𝑃 − 1) ∈ ℝ)
206	204, 205	syl 14	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → (𝑃 − 1) ∈ ℝ)
207	206	recnd 8136	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → (𝑃 − 1) ∈ ℂ)
208	207	2halvesd 9318	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → (((𝑃 − 1) / 2) + ((𝑃 − 1) / 2)) = (𝑃 − 1))
209	203, 208	breqtrd 4085	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → (𝑥 + 𝑦) ≤ (𝑃 − 1))
210		peano2zm 9445	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑃 ∈ ℤ → (𝑃 − 1) ∈ ℤ)
211		fznn 10246	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑃 − 1) ∈ ℤ → ((𝑥 + 𝑦) ∈ (1...(𝑃 − 1)) ↔ ((𝑥 + 𝑦) ∈ ℕ ∧ (𝑥 + 𝑦) ≤ (𝑃 − 1))))
212	148, 210, 211	3syl 17	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → ((𝑥 + 𝑦) ∈ (1...(𝑃 − 1)) ↔ ((𝑥 + 𝑦) ∈ ℕ ∧ (𝑥 + 𝑦) ≤ (𝑃 − 1))))
213	193, 209, 212	mpbir2and 947	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → (𝑥 + 𝑦) ∈ (1...(𝑃 − 1)))
214		fzm1ndvds 12282	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑃 ∈ ℕ ∧ (𝑥 + 𝑦) ∈ (1...(𝑃 − 1))) → ¬ 𝑃 ∥ (𝑥 + 𝑦))
215	76, 213, 214	syl2anc 411	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → ¬ 𝑃 ∥ (𝑥 + 𝑦))
216		eldifsni 3773	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → 𝑃 ≠ 2)
217	74, 216	syl 14	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → 𝑃 ≠ 2)
218		2prm 12564	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ 2 ∈ ℙ
219		prmrp 12582	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑃 ∈ ℙ ∧ 2 ∈ ℙ) → ((𝑃 gcd 2) = 1 ↔ 𝑃 ≠ 2))
220	75, 218, 219	sylancl 413	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → ((𝑃 gcd 2) = 1 ↔ 𝑃 ≠ 2))
221	217, 220	mpbird 167	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → (𝑃 gcd 2) = 1)
222	68	a1i 9	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → 2 ∈ ℤ)
223	193	nnzd 9529	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → (𝑥 + 𝑦) ∈ ℤ)
224		coprmdvds 12529	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑃 ∈ ℤ ∧ 2 ∈ ℤ ∧ (𝑥 + 𝑦) ∈ ℤ) → ((𝑃 ∥ (2 · (𝑥 + 𝑦)) ∧ (𝑃 gcd 2) = 1) → 𝑃 ∥ (𝑥 + 𝑦)))
225	148, 222, 223, 224	syl3anc 1250	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → ((𝑃 ∥ (2 · (𝑥 + 𝑦)) ∧ (𝑃 gcd 2) = 1) → 𝑃 ∥ (𝑥 + 𝑦)))
226	221, 225	mpan2d 428	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → (𝑃 ∥ (2 · (𝑥 + 𝑦)) → 𝑃 ∥ (𝑥 + 𝑦)))
227	215, 226	mtod 665	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → ¬ 𝑃 ∥ (2 · (𝑥 + 𝑦)))
228	138, 135	subnegd 8425	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → ((2 · 𝑥) − -(2 · 𝑦)) = ((2 · 𝑥) + (2 · 𝑦)))
229	86	zcnd 9531	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → 𝑥 ∈ ℂ)
230	70	zcnd 9531	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → 𝑦 ∈ ℂ)
231	98, 229, 230	adddid 8132	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → (2 · (𝑥 + 𝑦)) = ((2 · 𝑥) + (2 · 𝑦)))
232	228, 231	eqtr4d 2243	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → ((2 · 𝑥) − -(2 · 𝑦)) = (2 · (𝑥 + 𝑦)))
233	232	breq2d 4071	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → (𝑃 ∥ ((2 · 𝑥) − -(2 · 𝑦)) ↔ 𝑃 ∥ (2 · (𝑥 + 𝑦))))
234	227, 233	mtbird 675	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → ¬ 𝑃 ∥ ((2 · 𝑥) − -(2 · 𝑦)))
235	234	pm2.21d 620	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → (𝑃 ∥ ((2 · 𝑥) − -(2 · 𝑦)) → (2 · 𝑦) = (2 · 𝑥)))
236	192, 235	sylbid 150	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → (((2 · 𝑥) mod 𝑃) = (-(2 · 𝑦) mod 𝑃) → (2 · 𝑦) = (2 · 𝑥)))
237	189, 236	sylbid 150	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → (((-1 · (2 · 𝑦)) mod 𝑃) = ((2 · 𝑥) mod 𝑃) → (2 · 𝑦) = (2 · 𝑥)))
238		oveq1 5974	. . . . . . . . . . . . . . . . . 18 ⊢ ((-1↑(𝑅 + 𝑆)) = -1 → ((-1↑(𝑅 + 𝑆)) · (2 · 𝑦)) = (-1 · (2 · 𝑦)))
239	238	oveq1d 5982	. . . . . . . . . . . . . . . . 17 ⊢ ((-1↑(𝑅 + 𝑆)) = -1 → (((-1↑(𝑅 + 𝑆)) · (2 · 𝑦)) mod 𝑃) = ((-1 · (2 · 𝑦)) mod 𝑃))
240	239	eqeq1d 2216	. . . . . . . . . . . . . . . 16 ⊢ ((-1↑(𝑅 + 𝑆)) = -1 → ((((-1↑(𝑅 + 𝑆)) · (2 · 𝑦)) mod 𝑃) = ((2 · 𝑥) mod 𝑃) ↔ ((-1 · (2 · 𝑦)) mod 𝑃) = ((2 · 𝑥) mod 𝑃)))
241	240	imbi1d 231	. . . . . . . . . . . . . . 15 ⊢ ((-1↑(𝑅 + 𝑆)) = -1 → (((((-1↑(𝑅 + 𝑆)) · (2 · 𝑦)) mod 𝑃) = ((2 · 𝑥) mod 𝑃) → (2 · 𝑦) = (2 · 𝑥)) ↔ (((-1 · (2 · 𝑦)) mod 𝑃) = ((2 · 𝑥) mod 𝑃) → (2 · 𝑦) = (2 · 𝑥))))
242	237, 241	syl5ibrcom 157	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → ((-1↑(𝑅 + 𝑆)) = -1 → ((((-1↑(𝑅 + 𝑆)) · (2 · 𝑦)) mod 𝑃) = ((2 · 𝑥) mod 𝑃) → (2 · 𝑦) = (2 · 𝑥))))
243	135	mullidd 8125	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → (1 · (2 · 𝑦)) = (2 · 𝑦))
244	243	oveq1d 5982	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → ((1 · (2 · 𝑦)) mod 𝑃) = ((2 · 𝑦) mod 𝑃))
245		nnq 9789	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((2 · 𝑦) ∈ ℕ → (2 · 𝑦) ∈ ℚ)
246	26, 245	syl 14	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → (2 · 𝑦) ∈ ℚ)
247		nnmulcl 9092	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((2 ∈ ℕ ∧ 𝑦 ∈ ℕ) → (2 · 𝑦) ∈ ℕ)
248	22, 25, 247	sylancr 414	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → (2 · 𝑦) ∈ ℕ)
249	248	nnnn0d 9383	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → (2 · 𝑦) ∈ ℕ0)
250	249	nn0ge0d 9386	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → 0 ≤ (2 · 𝑦))
251		2re 9141	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ 2 ∈ ℝ
252	251	a1i 9	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → 2 ∈ ℝ)
253		2pos 9162	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ 0 < 2
254	253	a1i 9	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → 0 < 2)
255		lemuldiv2 8990	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑦 ∈ ℝ ∧ (𝑃 − 1) ∈ ℝ ∧ (2 ∈ ℝ ∧ 0 < 2)) → ((2 · 𝑦) ≤ (𝑃 − 1) ↔ 𝑦 ≤ ((𝑃 − 1) / 2)))
256	195, 206, 252, 254, 255	syl112anc 1254	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → ((2 · 𝑦) ≤ (𝑃 − 1) ↔ 𝑦 ≤ ((𝑃 − 1) / 2)))
257	202, 256	mpbird 167	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → (2 · 𝑦) ≤ (𝑃 − 1))
258		zltlem1 9465	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((2 · 𝑦) ∈ ℤ ∧ 𝑃 ∈ ℤ) → ((2 · 𝑦) < 𝑃 ↔ (2 · 𝑦) ≤ (𝑃 − 1)))
259	72, 148, 258	syl2anc 411	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → ((2 · 𝑦) < 𝑃 ↔ (2 · 𝑦) ≤ (𝑃 − 1)))
260	257, 259	mpbird 167	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → (2 · 𝑦) < 𝑃)
261		modqid 10531	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((2 · 𝑦) ∈ ℚ ∧ 𝑃 ∈ ℚ) ∧ (0 ≤ (2 · 𝑦) ∧ (2 · 𝑦) < 𝑃)) → ((2 · 𝑦) mod 𝑃) = (2 · 𝑦))
262	246, 110, 250, 260, 261	syl22anc 1251	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → ((2 · 𝑦) mod 𝑃) = (2 · 𝑦))
263	244, 262	eqtrd 2240	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → ((1 · (2 · 𝑦)) mod 𝑃) = (2 · 𝑦))
264		nnq 9789	. . . . . . . . . . . . . . . . . . 19 ⊢ ((2 · 𝑥) ∈ ℕ → (2 · 𝑥) ∈ ℚ)
265	47, 264	syl 14	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → (2 · 𝑥) ∈ ℚ)
266		nnmulcl 9092	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((2 ∈ ℕ ∧ 𝑥 ∈ ℕ) → (2 · 𝑥) ∈ ℕ)
267	22, 46, 266	sylancr 414	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → (2 · 𝑥) ∈ ℕ)
268	267	nnnn0d 9383	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → (2 · 𝑥) ∈ ℕ0)
269	268	nn0ge0d 9386	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → 0 ≤ (2 · 𝑥))
270		lemuldiv2 8990	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑥 ∈ ℝ ∧ (𝑃 − 1) ∈ ℝ ∧ (2 ∈ ℝ ∧ 0 < 2)) → ((2 · 𝑥) ≤ (𝑃 − 1) ↔ 𝑥 ≤ ((𝑃 − 1) / 2)))
271	194, 206, 252, 254, 270	syl112anc 1254	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → ((2 · 𝑥) ≤ (𝑃 − 1) ↔ 𝑥 ≤ ((𝑃 − 1) / 2)))
272	200, 271	mpbird 167	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → (2 · 𝑥) ≤ (𝑃 − 1))
273		zltlem1 9465	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((2 · 𝑥) ∈ ℤ ∧ 𝑃 ∈ ℤ) → ((2 · 𝑥) < 𝑃 ↔ (2 · 𝑥) ≤ (𝑃 − 1)))
274	88, 148, 273	syl2anc 411	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → ((2 · 𝑥) < 𝑃 ↔ (2 · 𝑥) ≤ (𝑃 − 1)))
275	272, 274	mpbird 167	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → (2 · 𝑥) < 𝑃)
276		modqid 10531	. . . . . . . . . . . . . . . . . 18 ⊢ ((((2 · 𝑥) ∈ ℚ ∧ 𝑃 ∈ ℚ) ∧ (0 ≤ (2 · 𝑥) ∧ (2 · 𝑥) < 𝑃)) → ((2 · 𝑥) mod 𝑃) = (2 · 𝑥))
277	265, 110, 269, 275, 276	syl22anc 1251	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → ((2 · 𝑥) mod 𝑃) = (2 · 𝑥))
278	263, 277	eqeq12d 2222	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → (((1 · (2 · 𝑦)) mod 𝑃) = ((2 · 𝑥) mod 𝑃) ↔ (2 · 𝑦) = (2 · 𝑥)))
279	278	biimpd 144	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → (((1 · (2 · 𝑦)) mod 𝑃) = ((2 · 𝑥) mod 𝑃) → (2 · 𝑦) = (2 · 𝑥)))
280		oveq1 5974	. . . . . . . . . . . . . . . . . 18 ⊢ ((-1↑(𝑅 + 𝑆)) = 1 → ((-1↑(𝑅 + 𝑆)) · (2 · 𝑦)) = (1 · (2 · 𝑦)))
281	280	oveq1d 5982	. . . . . . . . . . . . . . . . 17 ⊢ ((-1↑(𝑅 + 𝑆)) = 1 → (((-1↑(𝑅 + 𝑆)) · (2 · 𝑦)) mod 𝑃) = ((1 · (2 · 𝑦)) mod 𝑃))
282	281	eqeq1d 2216	. . . . . . . . . . . . . . . 16 ⊢ ((-1↑(𝑅 + 𝑆)) = 1 → ((((-1↑(𝑅 + 𝑆)) · (2 · 𝑦)) mod 𝑃) = ((2 · 𝑥) mod 𝑃) ↔ ((1 · (2 · 𝑦)) mod 𝑃) = ((2 · 𝑥) mod 𝑃)))
283	282	imbi1d 231	. . . . . . . . . . . . . . 15 ⊢ ((-1↑(𝑅 + 𝑆)) = 1 → (((((-1↑(𝑅 + 𝑆)) · (2 · 𝑦)) mod 𝑃) = ((2 · 𝑥) mod 𝑃) → (2 · 𝑦) = (2 · 𝑥)) ↔ (((1 · (2 · 𝑦)) mod 𝑃) = ((2 · 𝑥) mod 𝑃) → (2 · 𝑦) = (2 · 𝑥))))
284	279, 283	syl5ibrcom 157	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → ((-1↑(𝑅 + 𝑆)) = 1 → ((((-1↑(𝑅 + 𝑆)) · (2 · 𝑦)) mod 𝑃) = ((2 · 𝑥) mod 𝑃) → (2 · 𝑦) = (2 · 𝑥))))
285	91, 78	nn0addcld 9387	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → (𝑅 + 𝑆) ∈ ℕ0)
286	285	nn0zd 9528	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → (𝑅 + 𝑆) ∈ ℤ)
287		m1expcl2 10743	. . . . . . . . . . . . . . 15 ⊢ ((𝑅 + 𝑆) ∈ ℤ → (-1↑(𝑅 + 𝑆)) ∈ {-1, 1})
288		elpri 3666	. . . . . . . . . . . . . . 15 ⊢ ((-1↑(𝑅 + 𝑆)) ∈ {-1, 1} → ((-1↑(𝑅 + 𝑆)) = -1 ∨ (-1↑(𝑅 + 𝑆)) = 1))
289	286, 287, 288	3syl 17	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → ((-1↑(𝑅 + 𝑆)) = -1 ∨ (-1↑(𝑅 + 𝑆)) = 1))
290	242, 284, 289	mpjaod 720	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → ((((-1↑(𝑅 + 𝑆)) · (2 · 𝑦)) mod 𝑃) = ((2 · 𝑥) mod 𝑃) → (2 · 𝑦) = (2 · 𝑥)))
291		zexpcl 10736	. . . . . . . . . . . . . . . 16 ⊢ ((-1 ∈ ℤ ∧ (𝑅 + 𝑆) ∈ ℕ0) → (-1↑(𝑅 + 𝑆)) ∈ ℤ)
292	17, 285, 291	sylancr 414	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → (-1↑(𝑅 + 𝑆)) ∈ ℤ)
293	292, 72	zmulcld 9536	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → ((-1↑(𝑅 + 𝑆)) · (2 · 𝑦)) ∈ ℤ)
294		moddvds 12225	. . . . . . . . . . . . . 14 ⊢ ((𝑃 ∈ ℕ ∧ ((-1↑(𝑅 + 𝑆)) · (2 · 𝑦)) ∈ ℤ ∧ (2 · 𝑥) ∈ ℤ) → ((((-1↑(𝑅 + 𝑆)) · (2 · 𝑦)) mod 𝑃) = ((2 · 𝑥) mod 𝑃) ↔ 𝑃 ∥ (((-1↑(𝑅 + 𝑆)) · (2 · 𝑦)) − (2 · 𝑥))))
295	76, 293, 88, 294	syl3anc 1250	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → ((((-1↑(𝑅 + 𝑆)) · (2 · 𝑦)) mod 𝑃) = ((2 · 𝑥) mod 𝑃) ↔ 𝑃 ∥ (((-1↑(𝑅 + 𝑆)) · (2 · 𝑦)) − (2 · 𝑥))))
296	230, 229, 98, 99	mulcanapd 8769	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → ((2 · 𝑦) = (2 · 𝑥) ↔ 𝑦 = 𝑥))
297	290, 295, 296	3imtr3d 202	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → (𝑃 ∥ (((-1↑(𝑅 + 𝑆)) · (2 · 𝑦)) − (2 · 𝑥)) → 𝑦 = 𝑥))
298	184, 297	sylbid 150	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → (𝑃 ∥ ((-1↑𝑅) · (((-1↑𝑆) · (2 · 𝑦)) − ((-1↑𝑅) · (2 · 𝑥)))) → 𝑦 = 𝑥))
299	152, 154, 298	3syld 57	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → (𝑃 ∥ (𝑄 · (((-1↑𝑆) · (2 · 𝑦)) − ((-1↑𝑅) · (2 · 𝑥)))) → 𝑦 = 𝑥))
300	142, 299	sylbird 170	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → (𝑃 ∥ (((-1↑𝑆) · (𝑄 · (2 · 𝑦))) − ((-1↑𝑅) · (𝑄 · (2 · 𝑥)))) → 𝑦 = 𝑥))
301	127, 300	sylbid 150	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → ((((-1↑𝑆) · (𝑄 · (2 · 𝑦))) mod 𝑃) = (((-1↑𝑅) · (𝑄 · (2 · 𝑥))) mod 𝑃) → 𝑦 = 𝑥))
302	123, 301	sylbid 150	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → ((((-1↑𝑆) · 𝑆) mod 𝑃) = (((-1↑𝑅) · 𝑅) mod 𝑃) → 𝑦 = 𝑥))
303	101, 302	sylbid 150	. . . . . 6 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → (((((-1↑𝑆) · 𝑆) mod 𝑃) / 2) = ((((-1↑𝑅) · 𝑅) mod 𝑃) / 2) → 𝑦 = 𝑥))
304	63, 303	sylbid 150	. . . . 5 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → ((𝑀‘𝑦) = (𝑀‘𝑥) → 𝑦 = 𝑥))
305	304	ralrimivva 2590	. . . 4 ⊢ (𝜑 → ∀𝑦 ∈ (1...((𝑃 − 1) / 2))∀𝑥 ∈ (1...((𝑃 − 1) / 2))((𝑀‘𝑦) = (𝑀‘𝑥) → 𝑦 = 𝑥))
306		nfmpt1 4153	. . . . . . . . . 10 ⊢ Ⅎ𝑥(𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ ((((-1↑𝑅) · 𝑅) mod 𝑃) / 2))
307	5, 306	nfcxfr 2347	. . . . . . . . 9 ⊢ Ⅎ𝑥𝑀
308		nfcv 2350	. . . . . . . . 9 ⊢ Ⅎ𝑥𝑦
309	307, 308	nffv 5609	. . . . . . . 8 ⊢ Ⅎ𝑥(𝑀‘𝑦)
310		nfcv 2350	. . . . . . . . 9 ⊢ Ⅎ𝑥𝑧
311	307, 310	nffv 5609	. . . . . . . 8 ⊢ Ⅎ𝑥(𝑀‘𝑧)
312	309, 311	nfeq 2358	. . . . . . 7 ⊢ Ⅎ𝑥(𝑀‘𝑦) = (𝑀‘𝑧)
313		nfv 1552	. . . . . . 7 ⊢ Ⅎ𝑥 𝑦 = 𝑧
314	312, 313	nfim 1596	. . . . . 6 ⊢ Ⅎ𝑥((𝑀‘𝑦) = (𝑀‘𝑧) → 𝑦 = 𝑧)
315		nfv 1552	. . . . . 6 ⊢ Ⅎ𝑧((𝑀‘𝑦) = (𝑀‘𝑥) → 𝑦 = 𝑥)
316		fveq2 5599	. . . . . . . 8 ⊢ (𝑧 = 𝑥 → (𝑀‘𝑧) = (𝑀‘𝑥))
317	316	eqeq2d 2219	. . . . . . 7 ⊢ (𝑧 = 𝑥 → ((𝑀‘𝑦) = (𝑀‘𝑧) ↔ (𝑀‘𝑦) = (𝑀‘𝑥)))
318		equequ2 1737	. . . . . . 7 ⊢ (𝑧 = 𝑥 → (𝑦 = 𝑧 ↔ 𝑦 = 𝑥))
319	317, 318	imbi12d 234	. . . . . 6 ⊢ (𝑧 = 𝑥 → (((𝑀‘𝑦) = (𝑀‘𝑧) → 𝑦 = 𝑧) ↔ ((𝑀‘𝑦) = (𝑀‘𝑥) → 𝑦 = 𝑥)))
320	314, 315, 319	cbvralw 2735	. . . . 5 ⊢ (∀𝑧 ∈ (1...((𝑃 − 1) / 2))((𝑀‘𝑦) = (𝑀‘𝑧) → 𝑦 = 𝑧) ↔ ∀𝑥 ∈ (1...((𝑃 − 1) / 2))((𝑀‘𝑦) = (𝑀‘𝑥) → 𝑦 = 𝑥))
321	320	ralbii 2514	. . . 4 ⊢ (∀𝑦 ∈ (1...((𝑃 − 1) / 2))∀𝑧 ∈ (1...((𝑃 − 1) / 2))((𝑀‘𝑦) = (𝑀‘𝑧) → 𝑦 = 𝑧) ↔ ∀𝑦 ∈ (1...((𝑃 − 1) / 2))∀𝑥 ∈ (1...((𝑃 − 1) / 2))((𝑀‘𝑦) = (𝑀‘𝑥) → 𝑦 = 𝑥))
322	305, 321	sylibr 134	. . 3 ⊢ (𝜑 → ∀𝑦 ∈ (1...((𝑃 − 1) / 2))∀𝑧 ∈ (1...((𝑃 − 1) / 2))((𝑀‘𝑦) = (𝑀‘𝑧) → 𝑦 = 𝑧))
323		dff13 5860	. . 3 ⊢ (𝑀:(1...((𝑃 − 1) / 2))–1-1→(1...((𝑃 − 1) / 2)) ↔ (𝑀:(1...((𝑃 − 1) / 2))⟶(1...((𝑃 − 1) / 2)) ∧ ∀𝑦 ∈ (1...((𝑃 − 1) / 2))∀𝑧 ∈ (1...((𝑃 − 1) / 2))((𝑀‘𝑦) = (𝑀‘𝑧) → 𝑦 = 𝑧)))
324	6, 322, 323	sylanbrc 417	. 2 ⊢ (𝜑 → 𝑀:(1...((𝑃 − 1) / 2))–1-1→(1...((𝑃 − 1) / 2)))
325		1zzd 9434	. . . . 5 ⊢ (𝜑 → 1 ∈ ℤ)
326	1, 196	syl 14	. . . . . 6 ⊢ (𝜑 → ((𝑃 − 1) / 2) ∈ ℕ)
327	326	nnzd 9529	. . . . 5 ⊢ (𝜑 → ((𝑃 − 1) / 2) ∈ ℤ)
328	325, 327	fzfigd 10613	. . . 4 ⊢ (𝜑 → (1...((𝑃 − 1) / 2)) ∈ Fin)
329		enrefg 6878	. . . 4 ⊢ ((1...((𝑃 − 1) / 2)) ∈ Fin → (1...((𝑃 − 1) / 2)) ≈ (1...((𝑃 − 1) / 2)))
330	328, 329	syl 14	. . 3 ⊢ (𝜑 → (1...((𝑃 − 1) / 2)) ≈ (1...((𝑃 − 1) / 2)))
331		f1finf1o 7075	. . 3 ⊢ (((1...((𝑃 − 1) / 2)) ≈ (1...((𝑃 − 1) / 2)) ∧ (1...((𝑃 − 1) / 2)) ∈ Fin) → (𝑀:(1...((𝑃 − 1) / 2))–1-1→(1...((𝑃 − 1) / 2)) ↔ 𝑀:(1...((𝑃 − 1) / 2))–1-1-onto→(1...((𝑃 − 1) / 2))))
332	330, 328, 331	syl2anc 411	. 2 ⊢ (𝜑 → (𝑀:(1...((𝑃 − 1) / 2))–1-1→(1...((𝑃 − 1) / 2)) ↔ 𝑀:(1...((𝑃 − 1) / 2))–1-1-onto→(1...((𝑃 − 1) / 2))))
333	324, 332	mpbid 147	1 ⊢ (𝜑 → 𝑀:(1...((𝑃 − 1) / 2))–1-1-onto→(1...((𝑃 − 1) / 2)))

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 104   ↔ wb 105   ∨ wo 710   = wceq 1373   ∈ wcel 2178   ≠ wne 2378  ∀wral 2486  Vcvv 2776   ∖ cdif 3171  {csn 3643  {cpr 3644   class class class wbr 4059   ↦ cmpt 4121  ⟶wf 5286  –1-1→wf1 5287  –1-1-onto→wf1o 5289  ‘cfv 5290  (class class class)co 5967   ≈ cen 6848  Fincfn 6850  ℂcc 7958  ℝcr 7959  0cc0 7960  1c1 7961   + caddc 7963   · cmul 7965   < clt 8142   ≤ cle 8143   − cmin 8278  -cneg 8279   # cap 8689   / cdiv 8780  ℕcn 9071  2c2 9122  ℕ₀cn0 9330  ℤcz 9407  ℚcq 9775  ...cfz 10165   mod cmo 10504  ↑cexp 10720   ∥ cdvds 12213   gcd cgcd 12389  ℙcprime 12544

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 615  ax-in2 616  ax-io 711  ax-5 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-10 1529  ax-11 1530  ax-i12 1531  ax-bndl 1533  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-i5r 1559  ax-13 2180  ax-14 2181  ax-ext 2189  ax-coll 4175  ax-sep 4178  ax-nul 4186  ax-pow 4234  ax-pr 4269  ax-un 4498  ax-setind 4603  ax-iinf 4654  ax-cnex 8051  ax-resscn 8052  ax-1cn 8053  ax-1re 8054  ax-icn 8055  ax-addcl 8056  ax-addrcl 8057  ax-mulcl 8058  ax-mulrcl 8059  ax-addcom 8060  ax-mulcom 8061  ax-addass 8062  ax-mulass 8063  ax-distr 8064  ax-i2m1 8065  ax-0lt1 8066  ax-1rid 8067  ax-0id 8068  ax-rnegex 8069  ax-precex 8070  ax-cnre 8071  ax-pre-ltirr 8072  ax-pre-ltwlin 8073  ax-pre-lttrn 8074  ax-pre-apti 8075  ax-pre-ltadd 8076  ax-pre-mulgt0 8077  ax-pre-mulext 8078  ax-arch 8079  ax-caucvg 8080

This theorem depends on definitions:  df-bi 117  df-stab 833  df-dc 837  df-3or 982  df-3an 983  df-tru 1376  df-fal 1379  df-xor 1396  df-nf 1485  df-sb 1787  df-eu 2058  df-mo 2059  df-clab 2194  df-cleq 2200  df-clel 2203  df-nfc 2339  df-ne 2379  df-nel 2474  df-ral 2491  df-rex 2492  df-reu 2493  df-rmo 2494  df-rab 2495  df-v 2778  df-sbc 3006  df-csb 3102  df-dif 3176  df-un 3178  df-in 3180  df-ss 3187  df-nul 3469  df-if 3580  df-pw 3628  df-sn 3649  df-pr 3650  df-op 3652  df-uni 3865  df-int 3900  df-iun 3943  df-br 4060  df-opab 4122  df-mpt 4123  df-tr 4159  df-id 4358  df-po 4361  df-iso 4362  df-iord 4431  df-on 4433  df-ilim 4434  df-suc 4436  df-iom 4657  df-xp 4699  df-rel 4700  df-cnv 4701  df-co 4702  df-dm 4703  df-rn 4704  df-res 4705  df-ima 4706  df-iota 5251  df-fun 5292  df-fn 5293  df-f 5294  df-f1 5295  df-fo 5296  df-f1o 5297  df-fv 5298  df-riota 5922  df-ov 5970  df-oprab 5971  df-mpo 5972  df-1st 6249  df-2nd 6250  df-recs 6414  df-frec 6500  df-1o 6525  df-2o 6526  df-er 6643  df-en 6851  df-fin 6853  df-sup 7112  df-pnf 8144  df-mnf 8145  df-xr 8146  df-ltxr 8147  df-le 8148  df-sub 8280  df-neg 8281  df-reap 8683  df-ap 8690  df-div 8781  df-inn 9072  df-2 9130  df-3 9131  df-4 9132  df-n0 9331  df-z 9408  df-uz 9684  df-q 9776  df-rp 9811  df-fz 10166  df-fzo 10300  df-fl 10450  df-mod 10505  df-seqfrec 10630  df-exp 10721  df-cj 11268  df-re 11269  df-im 11270  df-rsqrt 11424  df-abs 11425  df-dvds 12214  df-gcd 12390  df-prm 12545

This theorem is referenced by:  lgseisenlem3  15664