lgseisenlem2 - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > lgseisenlem2		Structured version Visualization version GIF version

Theorem lgseisenlem2 27421

Description: Lemma for lgseisen 27424. 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 27420	. . 3 ⊢ (𝜑 → 𝑀:(1...((𝑃 − 1) / 2))⟶(1...((𝑃 − 1) / 2)))
7		oveq2 7440	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = 𝑦 → (2 · 𝑥) = (2 · 𝑦))
8	7	oveq2d 7448	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝑦 → (𝑄 · (2 · 𝑥)) = (𝑄 · (2 · 𝑦)))
9	8	oveq1d 7447	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝑦 → ((𝑄 · (2 · 𝑥)) mod 𝑃) = ((𝑄 · (2 · 𝑦)) mod 𝑃))
10		lgseisen.6	. . . . . . . . . . . . . 14 ⊢ 𝑆 = ((𝑄 · (2 · 𝑦)) mod 𝑃)
11	9, 4, 10	3eqtr4g 2801	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑦 → 𝑅 = 𝑆)
12	11	oveq2d 7448	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑦 → (-1↑𝑅) = (-1↑𝑆))
13	12, 11	oveq12d 7450	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑦 → ((-1↑𝑅) · 𝑅) = ((-1↑𝑆) · 𝑆))
14	13	oveq1d 7447	. . . . . . . . . 10 ⊢ (𝑥 = 𝑦 → (((-1↑𝑅) · 𝑅) mod 𝑃) = (((-1↑𝑆) · 𝑆) mod 𝑃))
15	14	oveq1d 7447	. . . . . . . . 9 ⊢ (𝑥 = 𝑦 → ((((-1↑𝑅) · 𝑅) mod 𝑃) / 2) = ((((-1↑𝑆) · 𝑆) mod 𝑃) / 2))
16		ovex 7465	. . . . . . . . 9 ⊢ ((((-1↑𝑆) · 𝑆) mod 𝑃) / 2) ∈ V
17	15, 5, 16	fvmpt 7015	. . . . . . . 8 ⊢ (𝑦 ∈ (1...((𝑃 − 1) / 2)) → (𝑀‘𝑦) = ((((-1↑𝑆) · 𝑆) mod 𝑃) / 2))
18	17	ad2antrl 728	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → (𝑀‘𝑦) = ((((-1↑𝑆) · 𝑆) mod 𝑃) / 2))
19		ovex 7465	. . . . . . . . 9 ⊢ ((((-1↑𝑅) · 𝑅) mod 𝑃) / 2) ∈ V
20	5	fvmpt2 7026	. . . . . . . . 9 ⊢ ((𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ ((((-1↑𝑅) · 𝑅) mod 𝑃) / 2) ∈ V) → (𝑀‘𝑥) = ((((-1↑𝑅) · 𝑅) mod 𝑃) / 2))
21	19, 20	mpan2 691	. . . . . . . 8 ⊢ (𝑥 ∈ (1...((𝑃 − 1) / 2)) → (𝑀‘𝑥) = ((((-1↑𝑅) · 𝑅) mod 𝑃) / 2))
22	21	ad2antll 729	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → (𝑀‘𝑥) = ((((-1↑𝑅) · 𝑅) mod 𝑃) / 2))
23	18, 22	eqeq12d 2752	. . . . . 6 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → ((𝑀‘𝑦) = (𝑀‘𝑥) ↔ ((((-1↑𝑆) · 𝑆) mod 𝑃) / 2) = ((((-1↑𝑅) · 𝑅) mod 𝑃) / 2)))
24	2	adantr 480	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → 𝑄 ∈ (ℙ ∖ {2}))
25	24	eldifad 3962	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → 𝑄 ∈ ℙ)
26		prmz 16713	. . . . . . . . . . . . . . . . 17 ⊢ (𝑄 ∈ ℙ → 𝑄 ∈ ℤ)
27	25, 26	syl 17	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → 𝑄 ∈ ℤ)
28		2z 12651	. . . . . . . . . . . . . . . . 17 ⊢ 2 ∈ ℤ
29		elfzelz 13565	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 ∈ (1...((𝑃 − 1) / 2)) → 𝑦 ∈ ℤ)
30	29	ad2antrl 728	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → 𝑦 ∈ ℤ)
31		zmulcl 12668	. . . . . . . . . . . . . . . . 17 ⊢ ((2 ∈ ℤ ∧ 𝑦 ∈ ℤ) → (2 · 𝑦) ∈ ℤ)
32	28, 30, 31	sylancr 587	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → (2 · 𝑦) ∈ ℤ)
33	27, 32	zmulcld 12730	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → (𝑄 · (2 · 𝑦)) ∈ ℤ)
34	1	adantr 480	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → 𝑃 ∈ (ℙ ∖ {2}))
35	34	eldifad 3962	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → 𝑃 ∈ ℙ)
36		prmnn 16712	. . . . . . . . . . . . . . . 16 ⊢ (𝑃 ∈ ℙ → 𝑃 ∈ ℕ)
37	35, 36	syl 17	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → 𝑃 ∈ ℕ)
38	33, 37	zmodcld 13933	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → ((𝑄 · (2 · 𝑦)) mod 𝑃) ∈ ℕ₀)
39	10, 38	eqeltrid 2844	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → 𝑆 ∈ ℕ₀)
40	39	nn0zd 12641	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → 𝑆 ∈ ℤ)
41		m1expcl 14128	. . . . . . . . . . . 12 ⊢ (𝑆 ∈ ℤ → (-1↑𝑆) ∈ ℤ)
42	40, 41	syl 17	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → (-1↑𝑆) ∈ ℤ)
43	42, 40	zmulcld 12730	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → ((-1↑𝑆) · 𝑆) ∈ ℤ)
44	43, 37	zmodcld 13933	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → (((-1↑𝑆) · 𝑆) mod 𝑃) ∈ ℕ₀)
45	44	nn0cnd 12591	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → (((-1↑𝑆) · 𝑆) mod 𝑃) ∈ ℂ)
46		elfzelz 13565	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 ∈ (1...((𝑃 − 1) / 2)) → 𝑥 ∈ ℤ)
47	46	ad2antll 729	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → 𝑥 ∈ ℤ)
48		zmulcl 12668	. . . . . . . . . . . . . . . . 17 ⊢ ((2 ∈ ℤ ∧ 𝑥 ∈ ℤ) → (2 · 𝑥) ∈ ℤ)
49	28, 47, 48	sylancr 587	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → (2 · 𝑥) ∈ ℤ)
50	27, 49	zmulcld 12730	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → (𝑄 · (2 · 𝑥)) ∈ ℤ)
51	50, 37	zmodcld 13933	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → ((𝑄 · (2 · 𝑥)) mod 𝑃) ∈ ℕ₀)
52	4, 51	eqeltrid 2844	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → 𝑅 ∈ ℕ₀)
53	52	nn0zd 12641	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → 𝑅 ∈ ℤ)
54		m1expcl 14128	. . . . . . . . . . . 12 ⊢ (𝑅 ∈ ℤ → (-1↑𝑅) ∈ ℤ)
55	53, 54	syl 17	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → (-1↑𝑅) ∈ ℤ)
56	55, 53	zmulcld 12730	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → ((-1↑𝑅) · 𝑅) ∈ ℤ)
57	56, 37	zmodcld 13933	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → (((-1↑𝑅) · 𝑅) mod 𝑃) ∈ ℕ₀)
58	57	nn0cnd 12591	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → (((-1↑𝑅) · 𝑅) mod 𝑃) ∈ ℂ)
59		2cnd 12345	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → 2 ∈ ℂ)
60		2ne0 12371	. . . . . . . . 9 ⊢ 2 ≠ 0
61	60	a1i 11	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → 2 ≠ 0)
62		div11 11951	. . . . . . . 8 ⊢ (((((-1↑𝑆) · 𝑆) mod 𝑃) ∈ ℂ ∧ (((-1↑𝑅) · 𝑅) mod 𝑃) ∈ ℂ ∧ (2 ∈ ℂ ∧ 2 ≠ 0)) → (((((-1↑𝑆) · 𝑆) mod 𝑃) / 2) = ((((-1↑𝑅) · 𝑅) mod 𝑃) / 2) ↔ (((-1↑𝑆) · 𝑆) mod 𝑃) = (((-1↑𝑅) · 𝑅) mod 𝑃)))
63	45, 58, 59, 61, 62	syl112anc 1375	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → (((((-1↑𝑆) · 𝑆) mod 𝑃) / 2) = ((((-1↑𝑅) · 𝑅) mod 𝑃) / 2) ↔ (((-1↑𝑆) · 𝑆) mod 𝑃) = (((-1↑𝑅) · 𝑅) mod 𝑃)))
64	37	nnrpd 13076	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → 𝑃 ∈ ℝ⁺)
65		eqidd 2737	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → ((-1↑𝑆) mod 𝑃) = ((-1↑𝑆) mod 𝑃))
66	10	oveq1i 7442	. . . . . . . . . . 11 ⊢ (𝑆 mod 𝑃) = (((𝑄 · (2 · 𝑦)) mod 𝑃) mod 𝑃)
67	33	zred 12724	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → (𝑄 · (2 · 𝑦)) ∈ ℝ)
68		modabs2 13946	. . . . . . . . . . . 12 ⊢ (((𝑄 · (2 · 𝑦)) ∈ ℝ ∧ 𝑃 ∈ ℝ⁺) → (((𝑄 · (2 · 𝑦)) mod 𝑃) mod 𝑃) = ((𝑄 · (2 · 𝑦)) mod 𝑃))
69	67, 64, 68	syl2anc 584	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → (((𝑄 · (2 · 𝑦)) mod 𝑃) mod 𝑃) = ((𝑄 · (2 · 𝑦)) mod 𝑃))
70	66, 69	eqtrid 2788	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → (𝑆 mod 𝑃) = ((𝑄 · (2 · 𝑦)) mod 𝑃))
71	42, 42, 40, 33, 64, 65, 70	modmul12d 13967	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → (((-1↑𝑆) · 𝑆) mod 𝑃) = (((-1↑𝑆) · (𝑄 · (2 · 𝑦))) mod 𝑃))
72		eqidd 2737	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → ((-1↑𝑅) mod 𝑃) = ((-1↑𝑅) mod 𝑃))
73	4	oveq1i 7442	. . . . . . . . . . 11 ⊢ (𝑅 mod 𝑃) = (((𝑄 · (2 · 𝑥)) mod 𝑃) mod 𝑃)
74	50	zred 12724	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → (𝑄 · (2 · 𝑥)) ∈ ℝ)
75		modabs2 13946	. . . . . . . . . . . 12 ⊢ (((𝑄 · (2 · 𝑥)) ∈ ℝ ∧ 𝑃 ∈ ℝ⁺) → (((𝑄 · (2 · 𝑥)) mod 𝑃) mod 𝑃) = ((𝑄 · (2 · 𝑥)) mod 𝑃))
76	74, 64, 75	syl2anc 584	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → (((𝑄 · (2 · 𝑥)) mod 𝑃) mod 𝑃) = ((𝑄 · (2 · 𝑥)) mod 𝑃))
77	73, 76	eqtrid 2788	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → (𝑅 mod 𝑃) = ((𝑄 · (2 · 𝑥)) mod 𝑃))
78	55, 55, 53, 50, 64, 72, 77	modmul12d 13967	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → (((-1↑𝑅) · 𝑅) mod 𝑃) = (((-1↑𝑅) · (𝑄 · (2 · 𝑥))) mod 𝑃))
79	71, 78	eqeq12d 2752	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → ((((-1↑𝑆) · 𝑆) mod 𝑃) = (((-1↑𝑅) · 𝑅) mod 𝑃) ↔ (((-1↑𝑆) · (𝑄 · (2 · 𝑦))) mod 𝑃) = (((-1↑𝑅) · (𝑄 · (2 · 𝑥))) mod 𝑃)))
80	42, 33	zmulcld 12730	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → ((-1↑𝑆) · (𝑄 · (2 · 𝑦))) ∈ ℤ)
81	55, 50	zmulcld 12730	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → ((-1↑𝑅) · (𝑄 · (2 · 𝑥))) ∈ ℤ)
82		moddvds 16302	. . . . . . . . . 10 ⊢ ((𝑃 ∈ ℕ ∧ ((-1↑𝑆) · (𝑄 · (2 · 𝑦))) ∈ ℤ ∧ ((-1↑𝑅) · (𝑄 · (2 · 𝑥))) ∈ ℤ) → ((((-1↑𝑆) · (𝑄 · (2 · 𝑦))) mod 𝑃) = (((-1↑𝑅) · (𝑄 · (2 · 𝑥))) mod 𝑃) ↔ 𝑃 ∥ (((-1↑𝑆) · (𝑄 · (2 · 𝑦))) − ((-1↑𝑅) · (𝑄 · (2 · 𝑥))))))
83	37, 80, 81, 82	syl3anc 1372	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → ((((-1↑𝑆) · (𝑄 · (2 · 𝑦))) mod 𝑃) = (((-1↑𝑅) · (𝑄 · (2 · 𝑥))) mod 𝑃) ↔ 𝑃 ∥ (((-1↑𝑆) · (𝑄 · (2 · 𝑦))) − ((-1↑𝑅) · (𝑄 · (2 · 𝑥))))))
84	27	zcnd 12725	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → 𝑄 ∈ ℂ)
85	42, 32	zmulcld 12730	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → ((-1↑𝑆) · (2 · 𝑦)) ∈ ℤ)
86	85	zcnd 12725	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → ((-1↑𝑆) · (2 · 𝑦)) ∈ ℂ)
87	55, 49	zmulcld 12730	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → ((-1↑𝑅) · (2 · 𝑥)) ∈ ℤ)
88	87	zcnd 12725	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → ((-1↑𝑅) · (2 · 𝑥)) ∈ ℂ)
89	84, 86, 88	subdid 11720	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → (𝑄 · (((-1↑𝑆) · (2 · 𝑦)) − ((-1↑𝑅) · (2 · 𝑥)))) = ((𝑄 · ((-1↑𝑆) · (2 · 𝑦))) − (𝑄 · ((-1↑𝑅) · (2 · 𝑥)))))
90	42	zcnd 12725	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → (-1↑𝑆) ∈ ℂ)
91	32	zcnd 12725	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → (2 · 𝑦) ∈ ℂ)
92	84, 90, 91	mul12d 11471	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → (𝑄 · ((-1↑𝑆) · (2 · 𝑦))) = ((-1↑𝑆) · (𝑄 · (2 · 𝑦))))
93	55	zcnd 12725	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → (-1↑𝑅) ∈ ℂ)
94	49	zcnd 12725	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → (2 · 𝑥) ∈ ℂ)
95	84, 93, 94	mul12d 11471	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → (𝑄 · ((-1↑𝑅) · (2 · 𝑥))) = ((-1↑𝑅) · (𝑄 · (2 · 𝑥))))
96	92, 95	oveq12d 7450	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → ((𝑄 · ((-1↑𝑆) · (2 · 𝑦))) − (𝑄 · ((-1↑𝑅) · (2 · 𝑥)))) = (((-1↑𝑆) · (𝑄 · (2 · 𝑦))) − ((-1↑𝑅) · (𝑄 · (2 · 𝑥)))))
97	89, 96	eqtrd 2776	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → (𝑄 · (((-1↑𝑆) · (2 · 𝑦)) − ((-1↑𝑅) · (2 · 𝑥)))) = (((-1↑𝑆) · (𝑄 · (2 · 𝑦))) − ((-1↑𝑅) · (𝑄 · (2 · 𝑥)))))
98	97	breq2d 5154	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → (𝑃 ∥ (𝑄 · (((-1↑𝑆) · (2 · 𝑦)) − ((-1↑𝑅) · (2 · 𝑥)))) ↔ 𝑃 ∥ (((-1↑𝑆) · (𝑄 · (2 · 𝑦))) − ((-1↑𝑅) · (𝑄 · (2 · 𝑥))))))
99	3	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → 𝑃 ≠ 𝑄)
100		prmrp 16750	. . . . . . . . . . . . . 14 ⊢ ((𝑃 ∈ ℙ ∧ 𝑄 ∈ ℙ) → ((𝑃 gcd 𝑄) = 1 ↔ 𝑃 ≠ 𝑄))
101	35, 25, 100	syl2anc 584	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → ((𝑃 gcd 𝑄) = 1 ↔ 𝑃 ≠ 𝑄))
102	99, 101	mpbird 257	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → (𝑃 gcd 𝑄) = 1)
103		prmz 16713	. . . . . . . . . . . . . 14 ⊢ (𝑃 ∈ ℙ → 𝑃 ∈ ℤ)
104	35, 103	syl 17	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → 𝑃 ∈ ℤ)
105	85, 87	zsubcld 12729	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → (((-1↑𝑆) · (2 · 𝑦)) − ((-1↑𝑅) · (2 · 𝑥))) ∈ ℤ)
106		coprmdvds 16691	. . . . . . . . . . . . 13 ⊢ ((𝑃 ∈ ℤ ∧ 𝑄 ∈ ℤ ∧ (((-1↑𝑆) · (2 · 𝑦)) − ((-1↑𝑅) · (2 · 𝑥))) ∈ ℤ) → ((𝑃 ∥ (𝑄 · (((-1↑𝑆) · (2 · 𝑦)) − ((-1↑𝑅) · (2 · 𝑥)))) ∧ (𝑃 gcd 𝑄) = 1) → 𝑃 ∥ (((-1↑𝑆) · (2 · 𝑦)) − ((-1↑𝑅) · (2 · 𝑥)))))
107	104, 27, 105, 106	syl3anc 1372	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → ((𝑃 ∥ (𝑄 · (((-1↑𝑆) · (2 · 𝑦)) − ((-1↑𝑅) · (2 · 𝑥)))) ∧ (𝑃 gcd 𝑄) = 1) → 𝑃 ∥ (((-1↑𝑆) · (2 · 𝑦)) − ((-1↑𝑅) · (2 · 𝑥)))))
108	102, 107	mpan2d 694	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → (𝑃 ∥ (𝑄 · (((-1↑𝑆) · (2 · 𝑦)) − ((-1↑𝑅) · (2 · 𝑥)))) → 𝑃 ∥ (((-1↑𝑆) · (2 · 𝑦)) − ((-1↑𝑅) · (2 · 𝑥)))))
109		dvdsmultr2 16336	. . . . . . . . . . . 12 ⊢ ((𝑃 ∈ ℤ ∧ (-1↑𝑅) ∈ ℤ ∧ (((-1↑𝑆) · (2 · 𝑦)) − ((-1↑𝑅) · (2 · 𝑥))) ∈ ℤ) → (𝑃 ∥ (((-1↑𝑆) · (2 · 𝑦)) − ((-1↑𝑅) · (2 · 𝑥))) → 𝑃 ∥ ((-1↑𝑅) · (((-1↑𝑆) · (2 · 𝑦)) − ((-1↑𝑅) · (2 · 𝑥))))))
110	104, 55, 105, 109	syl3anc 1372	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → (𝑃 ∥ (((-1↑𝑆) · (2 · 𝑦)) − ((-1↑𝑅) · (2 · 𝑥))) → 𝑃 ∥ ((-1↑𝑅) · (((-1↑𝑆) · (2 · 𝑦)) − ((-1↑𝑅) · (2 · 𝑥))))))
111	93, 86, 88	subdid 11720	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → ((-1↑𝑅) · (((-1↑𝑆) · (2 · 𝑦)) − ((-1↑𝑅) · (2 · 𝑥)))) = (((-1↑𝑅) · ((-1↑𝑆) · (2 · 𝑦))) − ((-1↑𝑅) · ((-1↑𝑅) · (2 · 𝑥)))))
112		neg1cn 12381	. . . . . . . . . . . . . . . . . . 19 ⊢ -1 ∈ ℂ
113	112	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → -1 ∈ ℂ)
114	113, 39, 52	expaddd 14189	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → (-1↑(𝑅 + 𝑆)) = ((-1↑𝑅) · (-1↑𝑆)))
115	114	oveq1d 7447	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → ((-1↑(𝑅 + 𝑆)) · (2 · 𝑦)) = (((-1↑𝑅) · (-1↑𝑆)) · (2 · 𝑦)))
116	93, 90, 91	mulassd 11285	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → (((-1↑𝑅) · (-1↑𝑆)) · (2 · 𝑦)) = ((-1↑𝑅) · ((-1↑𝑆) · (2 · 𝑦))))
117	115, 116	eqtr2d 2777	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → ((-1↑𝑅) · ((-1↑𝑆) · (2 · 𝑦))) = ((-1↑(𝑅 + 𝑆)) · (2 · 𝑦)))
118		ax-1cn 11214	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ 1 ∈ ℂ
119		ax-1ne0 11225	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ 1 ≠ 0
120		divneg2 11992	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((1 ∈ ℂ ∧ 1 ∈ ℂ ∧ 1 ≠ 0) → -(1 / 1) = (1 / -1))
121	118, 118, 119, 120	mp3an 1462	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ -(1 / 1) = (1 / -1)
122		1div1e1 11959	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (1 / 1) = 1
123	122	negeqi 11502	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ -(1 / 1) = -1
124	121, 123	eqtr3i 2766	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (1 / -1) = -1
125	124	oveq1i 7442	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((1 / -1)↑𝑅) = (-1↑𝑅)
126		neg1ne0 12383	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ -1 ≠ 0
127	126	a1i 11	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → -1 ≠ 0)
128	113, 127, 53	exprecd 14195	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → ((1 / -1)↑𝑅) = (1 / (-1↑𝑅)))
129	125, 128	eqtr3id 2790	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → (-1↑𝑅) = (1 / (-1↑𝑅)))
130	129	oveq2d 7448	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → ((-1↑𝑅) · (-1↑𝑅)) = ((-1↑𝑅) · (1 / (-1↑𝑅))))
131	113, 127, 53	expne0d 14193	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → (-1↑𝑅) ≠ 0)
132	93, 131	recidd 12039	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → ((-1↑𝑅) · (1 / (-1↑𝑅))) = 1)
133	130, 132	eqtrd 2776	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → ((-1↑𝑅) · (-1↑𝑅)) = 1)
134	133	oveq1d 7447	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → (((-1↑𝑅) · (-1↑𝑅)) · (2 · 𝑥)) = (1 · (2 · 𝑥)))
135	93, 93, 94	mulassd 11285	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → (((-1↑𝑅) · (-1↑𝑅)) · (2 · 𝑥)) = ((-1↑𝑅) · ((-1↑𝑅) · (2 · 𝑥))))
136	94	mullidd 11280	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → (1 · (2 · 𝑥)) = (2 · 𝑥))
137	134, 135, 136	3eqtr3d 2784	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → ((-1↑𝑅) · ((-1↑𝑅) · (2 · 𝑥))) = (2 · 𝑥))
138	117, 137	oveq12d 7450	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → (((-1↑𝑅) · ((-1↑𝑆) · (2 · 𝑦))) − ((-1↑𝑅) · ((-1↑𝑅) · (2 · 𝑥)))) = (((-1↑(𝑅 + 𝑆)) · (2 · 𝑦)) − (2 · 𝑥)))
139	111, 138	eqtrd 2776	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → ((-1↑𝑅) · (((-1↑𝑆) · (2 · 𝑦)) − ((-1↑𝑅) · (2 · 𝑥)))) = (((-1↑(𝑅 + 𝑆)) · (2 · 𝑦)) − (2 · 𝑥)))
140	139	breq2d 5154	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → (𝑃 ∥ ((-1↑𝑅) · (((-1↑𝑆) · (2 · 𝑦)) − ((-1↑𝑅) · (2 · 𝑥)))) ↔ 𝑃 ∥ (((-1↑(𝑅 + 𝑆)) · (2 · 𝑦)) − (2 · 𝑥))))
141		eqcom 2743	. . . . . . . . . . . . . . . . 17 ⊢ (((-1 · (2 · 𝑦)) mod 𝑃) = ((2 · 𝑥) mod 𝑃) ↔ ((2 · 𝑥) mod 𝑃) = ((-1 · (2 · 𝑦)) mod 𝑃))
142	91	mulm1d 11716	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → (-1 · (2 · 𝑦)) = -(2 · 𝑦))
143	142	oveq1d 7447	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → ((-1 · (2 · 𝑦)) mod 𝑃) = (-(2 · 𝑦) mod 𝑃))
144	143	eqeq2d 2747	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → (((2 · 𝑥) mod 𝑃) = ((-1 · (2 · 𝑦)) mod 𝑃) ↔ ((2 · 𝑥) mod 𝑃) = (-(2 · 𝑦) mod 𝑃)))
145	141, 144	bitrid 283	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → (((-1 · (2 · 𝑦)) mod 𝑃) = ((2 · 𝑥) mod 𝑃) ↔ ((2 · 𝑥) mod 𝑃) = (-(2 · 𝑦) mod 𝑃)))
146	32	znegcld 12726	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → -(2 · 𝑦) ∈ ℤ)
147		moddvds 16302	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑃 ∈ ℕ ∧ (2 · 𝑥) ∈ ℤ ∧ -(2 · 𝑦) ∈ ℤ) → (((2 · 𝑥) mod 𝑃) = (-(2 · 𝑦) mod 𝑃) ↔ 𝑃 ∥ ((2 · 𝑥) − -(2 · 𝑦))))
148	37, 49, 146, 147	syl3anc 1372	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → (((2 · 𝑥) mod 𝑃) = (-(2 · 𝑦) mod 𝑃) ↔ 𝑃 ∥ ((2 · 𝑥) − -(2 · 𝑦))))
149		elfznn 13594	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑥 ∈ (1...((𝑃 − 1) / 2)) → 𝑥 ∈ ℕ)
150	149	ad2antll 729	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → 𝑥 ∈ ℕ)
151		elfznn 13594	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑦 ∈ (1...((𝑃 − 1) / 2)) → 𝑦 ∈ ℕ)
152	151	ad2antrl 728	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → 𝑦 ∈ ℕ)
153	150, 152	nnaddcld 12319	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → (𝑥 + 𝑦) ∈ ℕ)
154	150	nnred 12282	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → 𝑥 ∈ ℝ)
155	30	zred 12724	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → 𝑦 ∈ ℝ)
156		oddprm 16849	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → ((𝑃 − 1) / 2) ∈ ℕ)
157	34, 156	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → ((𝑃 − 1) / 2) ∈ ℕ)
158	157	nnred 12282	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → ((𝑃 − 1) / 2) ∈ ℝ)
159		elfzle2 13569	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑥 ∈ (1...((𝑃 − 1) / 2)) → 𝑥 ≤ ((𝑃 − 1) / 2))
160	159	ad2antll 729	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → 𝑥 ≤ ((𝑃 − 1) / 2))
161		elfzle2 13569	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑦 ∈ (1...((𝑃 − 1) / 2)) → 𝑦 ≤ ((𝑃 − 1) / 2))
162	161	ad2antrl 728	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → 𝑦 ≤ ((𝑃 − 1) / 2))
163	154, 155, 158, 158, 160, 162	le2addd 11883	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → (𝑥 + 𝑦) ≤ (((𝑃 − 1) / 2) + ((𝑃 − 1) / 2)))
164	37	nnred 12282	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → 𝑃 ∈ ℝ)
165		peano2rem 11577	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑃 ∈ ℝ → (𝑃 − 1) ∈ ℝ)
166	164, 165	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → (𝑃 − 1) ∈ ℝ)
167	166	recnd 11290	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → (𝑃 − 1) ∈ ℂ)
168	167	2halvesd 12514	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → (((𝑃 − 1) / 2) + ((𝑃 − 1) / 2)) = (𝑃 − 1))
169	163, 168	breqtrd 5168	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → (𝑥 + 𝑦) ≤ (𝑃 − 1))
170		peano2zm 12662	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑃 ∈ ℤ → (𝑃 − 1) ∈ ℤ)
171		fznn 13633	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑃 − 1) ∈ ℤ → ((𝑥 + 𝑦) ∈ (1...(𝑃 − 1)) ↔ ((𝑥 + 𝑦) ∈ ℕ ∧ (𝑥 + 𝑦) ≤ (𝑃 − 1))))
172	104, 170, 171	3syl 18	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → ((𝑥 + 𝑦) ∈ (1...(𝑃 − 1)) ↔ ((𝑥 + 𝑦) ∈ ℕ ∧ (𝑥 + 𝑦) ≤ (𝑃 − 1))))
173	153, 169, 172	mpbir2and 713	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → (𝑥 + 𝑦) ∈ (1...(𝑃 − 1)))
174		fzm1ndvds 16360	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑃 ∈ ℕ ∧ (𝑥 + 𝑦) ∈ (1...(𝑃 − 1))) → ¬ 𝑃 ∥ (𝑥 + 𝑦))
175	37, 173, 174	syl2anc 584	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → ¬ 𝑃 ∥ (𝑥 + 𝑦))
176		eldifsni 4789	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → 𝑃 ≠ 2)
177	34, 176	syl 17	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → 𝑃 ≠ 2)
178		2prm 16730	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ 2 ∈ ℙ
179		prmrp 16750	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑃 ∈ ℙ ∧ 2 ∈ ℙ) → ((𝑃 gcd 2) = 1 ↔ 𝑃 ≠ 2))
180	35, 178, 179	sylancl 586	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → ((𝑃 gcd 2) = 1 ↔ 𝑃 ≠ 2))
181	177, 180	mpbird 257	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → (𝑃 gcd 2) = 1)
182	28	a1i 11	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → 2 ∈ ℤ)
183	153	nnzd 12642	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → (𝑥 + 𝑦) ∈ ℤ)
184		coprmdvds 16691	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑃 ∈ ℤ ∧ 2 ∈ ℤ ∧ (𝑥 + 𝑦) ∈ ℤ) → ((𝑃 ∥ (2 · (𝑥 + 𝑦)) ∧ (𝑃 gcd 2) = 1) → 𝑃 ∥ (𝑥 + 𝑦)))
185	104, 182, 183, 184	syl3anc 1372	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → ((𝑃 ∥ (2 · (𝑥 + 𝑦)) ∧ (𝑃 gcd 2) = 1) → 𝑃 ∥ (𝑥 + 𝑦)))
186	181, 185	mpan2d 694	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → (𝑃 ∥ (2 · (𝑥 + 𝑦)) → 𝑃 ∥ (𝑥 + 𝑦)))
187	175, 186	mtod 198	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → ¬ 𝑃 ∥ (2 · (𝑥 + 𝑦)))
188	94, 91	subnegd 11628	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → ((2 · 𝑥) − -(2 · 𝑦)) = ((2 · 𝑥) + (2 · 𝑦)))
189	47	zcnd 12725	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → 𝑥 ∈ ℂ)
190	30	zcnd 12725	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → 𝑦 ∈ ℂ)
191	59, 189, 190	adddid 11286	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → (2 · (𝑥 + 𝑦)) = ((2 · 𝑥) + (2 · 𝑦)))
192	188, 191	eqtr4d 2779	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → ((2 · 𝑥) − -(2 · 𝑦)) = (2 · (𝑥 + 𝑦)))
193	192	breq2d 5154	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → (𝑃 ∥ ((2 · 𝑥) − -(2 · 𝑦)) ↔ 𝑃 ∥ (2 · (𝑥 + 𝑦))))
194	187, 193	mtbird 325	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → ¬ 𝑃 ∥ ((2 · 𝑥) − -(2 · 𝑦)))
195	194	pm2.21d 121	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → (𝑃 ∥ ((2 · 𝑥) − -(2 · 𝑦)) → (2 · 𝑦) = (2 · 𝑥)))
196	148, 195	sylbid 240	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → (((2 · 𝑥) mod 𝑃) = (-(2 · 𝑦) mod 𝑃) → (2 · 𝑦) = (2 · 𝑥)))
197	145, 196	sylbid 240	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → (((-1 · (2 · 𝑦)) mod 𝑃) = ((2 · 𝑥) mod 𝑃) → (2 · 𝑦) = (2 · 𝑥)))
198		oveq1 7439	. . . . . . . . . . . . . . . . . 18 ⊢ ((-1↑(𝑅 + 𝑆)) = -1 → ((-1↑(𝑅 + 𝑆)) · (2 · 𝑦)) = (-1 · (2 · 𝑦)))
199	198	oveq1d 7447	. . . . . . . . . . . . . . . . 17 ⊢ ((-1↑(𝑅 + 𝑆)) = -1 → (((-1↑(𝑅 + 𝑆)) · (2 · 𝑦)) mod 𝑃) = ((-1 · (2 · 𝑦)) mod 𝑃))
200	199	eqeq1d 2738	. . . . . . . . . . . . . . . 16 ⊢ ((-1↑(𝑅 + 𝑆)) = -1 → ((((-1↑(𝑅 + 𝑆)) · (2 · 𝑦)) mod 𝑃) = ((2 · 𝑥) mod 𝑃) ↔ ((-1 · (2 · 𝑦)) mod 𝑃) = ((2 · 𝑥) mod 𝑃)))
201	200	imbi1d 341	. . . . . . . . . . . . . . 15 ⊢ ((-1↑(𝑅 + 𝑆)) = -1 → (((((-1↑(𝑅 + 𝑆)) · (2 · 𝑦)) mod 𝑃) = ((2 · 𝑥) mod 𝑃) → (2 · 𝑦) = (2 · 𝑥)) ↔ (((-1 · (2 · 𝑦)) mod 𝑃) = ((2 · 𝑥) mod 𝑃) → (2 · 𝑦) = (2 · 𝑥))))
202	197, 201	syl5ibrcom 247	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → ((-1↑(𝑅 + 𝑆)) = -1 → ((((-1↑(𝑅 + 𝑆)) · (2 · 𝑦)) mod 𝑃) = ((2 · 𝑥) mod 𝑃) → (2 · 𝑦) = (2 · 𝑥))))
203	91	mullidd 11280	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → (1 · (2 · 𝑦)) = (2 · 𝑦))
204	203	oveq1d 7447	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → ((1 · (2 · 𝑦)) mod 𝑃) = ((2 · 𝑦) mod 𝑃))
205	32	zred 12724	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → (2 · 𝑦) ∈ ℝ)
206		2nn 12340	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 2 ∈ ℕ
207		nnmulcl 12291	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((2 ∈ ℕ ∧ 𝑦 ∈ ℕ) → (2 · 𝑦) ∈ ℕ)
208	206, 152, 207	sylancr 587	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → (2 · 𝑦) ∈ ℕ)
209	208	nnnn0d 12589	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → (2 · 𝑦) ∈ ℕ₀)
210	209	nn0ge0d 12592	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → 0 ≤ (2 · 𝑦))
211		2re 12341	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ 2 ∈ ℝ
212	211	a1i 11	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → 2 ∈ ℝ)
213		2pos 12370	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ 0 < 2
214	213	a1i 11	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → 0 < 2)
215		lemuldiv2 12150	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑦 ∈ ℝ ∧ (𝑃 − 1) ∈ ℝ ∧ (2 ∈ ℝ ∧ 0 < 2)) → ((2 · 𝑦) ≤ (𝑃 − 1) ↔ 𝑦 ≤ ((𝑃 − 1) / 2)))
216	155, 166, 212, 214, 215	syl112anc 1375	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → ((2 · 𝑦) ≤ (𝑃 − 1) ↔ 𝑦 ≤ ((𝑃 − 1) / 2)))
217	162, 216	mpbird 257	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → (2 · 𝑦) ≤ (𝑃 − 1))
218		zltlem1 12672	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((2 · 𝑦) ∈ ℤ ∧ 𝑃 ∈ ℤ) → ((2 · 𝑦) < 𝑃 ↔ (2 · 𝑦) ≤ (𝑃 − 1)))
219	32, 104, 218	syl2anc 584	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → ((2 · 𝑦) < 𝑃 ↔ (2 · 𝑦) ≤ (𝑃 − 1)))
220	217, 219	mpbird 257	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → (2 · 𝑦) < 𝑃)
221		modid 13937	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((2 · 𝑦) ∈ ℝ ∧ 𝑃 ∈ ℝ⁺) ∧ (0 ≤ (2 · 𝑦) ∧ (2 · 𝑦) < 𝑃)) → ((2 · 𝑦) mod 𝑃) = (2 · 𝑦))
222	205, 64, 210, 220, 221	syl22anc 838	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → ((2 · 𝑦) mod 𝑃) = (2 · 𝑦))
223	204, 222	eqtrd 2776	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → ((1 · (2 · 𝑦)) mod 𝑃) = (2 · 𝑦))
224	49	zred 12724	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → (2 · 𝑥) ∈ ℝ)
225		nnmulcl 12291	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((2 ∈ ℕ ∧ 𝑥 ∈ ℕ) → (2 · 𝑥) ∈ ℕ)
226	206, 150, 225	sylancr 587	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → (2 · 𝑥) ∈ ℕ)
227	226	nnnn0d 12589	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → (2 · 𝑥) ∈ ℕ₀)
228	227	nn0ge0d 12592	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → 0 ≤ (2 · 𝑥))
229		lemuldiv2 12150	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑥 ∈ ℝ ∧ (𝑃 − 1) ∈ ℝ ∧ (2 ∈ ℝ ∧ 0 < 2)) → ((2 · 𝑥) ≤ (𝑃 − 1) ↔ 𝑥 ≤ ((𝑃 − 1) / 2)))
230	154, 166, 212, 214, 229	syl112anc 1375	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → ((2 · 𝑥) ≤ (𝑃 − 1) ↔ 𝑥 ≤ ((𝑃 − 1) / 2)))
231	160, 230	mpbird 257	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → (2 · 𝑥) ≤ (𝑃 − 1))
232		zltlem1 12672	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((2 · 𝑥) ∈ ℤ ∧ 𝑃 ∈ ℤ) → ((2 · 𝑥) < 𝑃 ↔ (2 · 𝑥) ≤ (𝑃 − 1)))
233	49, 104, 232	syl2anc 584	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → ((2 · 𝑥) < 𝑃 ↔ (2 · 𝑥) ≤ (𝑃 − 1)))
234	231, 233	mpbird 257	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → (2 · 𝑥) < 𝑃)
235		modid 13937	. . . . . . . . . . . . . . . . . 18 ⊢ ((((2 · 𝑥) ∈ ℝ ∧ 𝑃 ∈ ℝ⁺) ∧ (0 ≤ (2 · 𝑥) ∧ (2 · 𝑥) < 𝑃)) → ((2 · 𝑥) mod 𝑃) = (2 · 𝑥))
236	224, 64, 228, 234, 235	syl22anc 838	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → ((2 · 𝑥) mod 𝑃) = (2 · 𝑥))
237	223, 236	eqeq12d 2752	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → (((1 · (2 · 𝑦)) mod 𝑃) = ((2 · 𝑥) mod 𝑃) ↔ (2 · 𝑦) = (2 · 𝑥)))
238	237	biimpd 229	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → (((1 · (2 · 𝑦)) mod 𝑃) = ((2 · 𝑥) mod 𝑃) → (2 · 𝑦) = (2 · 𝑥)))
239		oveq1 7439	. . . . . . . . . . . . . . . . . 18 ⊢ ((-1↑(𝑅 + 𝑆)) = 1 → ((-1↑(𝑅 + 𝑆)) · (2 · 𝑦)) = (1 · (2 · 𝑦)))
240	239	oveq1d 7447	. . . . . . . . . . . . . . . . 17 ⊢ ((-1↑(𝑅 + 𝑆)) = 1 → (((-1↑(𝑅 + 𝑆)) · (2 · 𝑦)) mod 𝑃) = ((1 · (2 · 𝑦)) mod 𝑃))
241	240	eqeq1d 2738	. . . . . . . . . . . . . . . 16 ⊢ ((-1↑(𝑅 + 𝑆)) = 1 → ((((-1↑(𝑅 + 𝑆)) · (2 · 𝑦)) mod 𝑃) = ((2 · 𝑥) mod 𝑃) ↔ ((1 · (2 · 𝑦)) mod 𝑃) = ((2 · 𝑥) mod 𝑃)))
242	241	imbi1d 341	. . . . . . . . . . . . . . 15 ⊢ ((-1↑(𝑅 + 𝑆)) = 1 → (((((-1↑(𝑅 + 𝑆)) · (2 · 𝑦)) mod 𝑃) = ((2 · 𝑥) mod 𝑃) → (2 · 𝑦) = (2 · 𝑥)) ↔ (((1 · (2 · 𝑦)) mod 𝑃) = ((2 · 𝑥) mod 𝑃) → (2 · 𝑦) = (2 · 𝑥))))
243	238, 242	syl5ibrcom 247	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → ((-1↑(𝑅 + 𝑆)) = 1 → ((((-1↑(𝑅 + 𝑆)) · (2 · 𝑦)) mod 𝑃) = ((2 · 𝑥) mod 𝑃) → (2 · 𝑦) = (2 · 𝑥))))
244	52, 39	nn0addcld 12593	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → (𝑅 + 𝑆) ∈ ℕ₀)
245	244	nn0zd 12641	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → (𝑅 + 𝑆) ∈ ℤ)
246		m1expcl2 14127	. . . . . . . . . . . . . . 15 ⊢ ((𝑅 + 𝑆) ∈ ℤ → (-1↑(𝑅 + 𝑆)) ∈ {-1, 1})
247		elpri 4648	. . . . . . . . . . . . . . 15 ⊢ ((-1↑(𝑅 + 𝑆)) ∈ {-1, 1} → ((-1↑(𝑅 + 𝑆)) = -1 ∨ (-1↑(𝑅 + 𝑆)) = 1))
248	245, 246, 247	3syl 18	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → ((-1↑(𝑅 + 𝑆)) = -1 ∨ (-1↑(𝑅 + 𝑆)) = 1))
249	202, 243, 248	mpjaod 860	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → ((((-1↑(𝑅 + 𝑆)) · (2 · 𝑦)) mod 𝑃) = ((2 · 𝑥) mod 𝑃) → (2 · 𝑦) = (2 · 𝑥)))
250		neg1z 12655	. . . . . . . . . . . . . . . 16 ⊢ -1 ∈ ℤ
251		zexpcl 14118	. . . . . . . . . . . . . . . 16 ⊢ ((-1 ∈ ℤ ∧ (𝑅 + 𝑆) ∈ ℕ₀) → (-1↑(𝑅 + 𝑆)) ∈ ℤ)
252	250, 244, 251	sylancr 587	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → (-1↑(𝑅 + 𝑆)) ∈ ℤ)
253	252, 32	zmulcld 12730	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → ((-1↑(𝑅 + 𝑆)) · (2 · 𝑦)) ∈ ℤ)
254		moddvds 16302	. . . . . . . . . . . . . 14 ⊢ ((𝑃 ∈ ℕ ∧ ((-1↑(𝑅 + 𝑆)) · (2 · 𝑦)) ∈ ℤ ∧ (2 · 𝑥) ∈ ℤ) → ((((-1↑(𝑅 + 𝑆)) · (2 · 𝑦)) mod 𝑃) = ((2 · 𝑥) mod 𝑃) ↔ 𝑃 ∥ (((-1↑(𝑅 + 𝑆)) · (2 · 𝑦)) − (2 · 𝑥))))
255	37, 253, 49, 254	syl3anc 1372	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → ((((-1↑(𝑅 + 𝑆)) · (2 · 𝑦)) mod 𝑃) = ((2 · 𝑥) mod 𝑃) ↔ 𝑃 ∥ (((-1↑(𝑅 + 𝑆)) · (2 · 𝑦)) − (2 · 𝑥))))
256	190, 189, 59, 61	mulcand 11897	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → ((2 · 𝑦) = (2 · 𝑥) ↔ 𝑦 = 𝑥))
257	249, 255, 256	3imtr3d 293	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → (𝑃 ∥ (((-1↑(𝑅 + 𝑆)) · (2 · 𝑦)) − (2 · 𝑥)) → 𝑦 = 𝑥))
258	140, 257	sylbid 240	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → (𝑃 ∥ ((-1↑𝑅) · (((-1↑𝑆) · (2 · 𝑦)) − ((-1↑𝑅) · (2 · 𝑥)))) → 𝑦 = 𝑥))
259	108, 110, 258	3syld 60	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → (𝑃 ∥ (𝑄 · (((-1↑𝑆) · (2 · 𝑦)) − ((-1↑𝑅) · (2 · 𝑥)))) → 𝑦 = 𝑥))
260	98, 259	sylbird 260	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → (𝑃 ∥ (((-1↑𝑆) · (𝑄 · (2 · 𝑦))) − ((-1↑𝑅) · (𝑄 · (2 · 𝑥)))) → 𝑦 = 𝑥))
261	83, 260	sylbid 240	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → ((((-1↑𝑆) · (𝑄 · (2 · 𝑦))) mod 𝑃) = (((-1↑𝑅) · (𝑄 · (2 · 𝑥))) mod 𝑃) → 𝑦 = 𝑥))
262	79, 261	sylbid 240	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → ((((-1↑𝑆) · 𝑆) mod 𝑃) = (((-1↑𝑅) · 𝑅) mod 𝑃) → 𝑦 = 𝑥))
263	63, 262	sylbid 240	. . . . . 6 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → (((((-1↑𝑆) · 𝑆) mod 𝑃) / 2) = ((((-1↑𝑅) · 𝑅) mod 𝑃) / 2) → 𝑦 = 𝑥))
264	23, 263	sylbid 240	. . . . 5 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → ((𝑀‘𝑦) = (𝑀‘𝑥) → 𝑦 = 𝑥))
265	264	ralrimivva 3201	. . . 4 ⊢ (𝜑 → ∀𝑦 ∈ (1...((𝑃 − 1) / 2))∀𝑥 ∈ (1...((𝑃 − 1) / 2))((𝑀‘𝑦) = (𝑀‘𝑥) → 𝑦 = 𝑥))
266		nfmpt1 5249	. . . . . . . . . 10 ⊢ Ⅎ𝑥(𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ ((((-1↑𝑅) · 𝑅) mod 𝑃) / 2))
267	5, 266	nfcxfr 2902	. . . . . . . . 9 ⊢ Ⅎ𝑥𝑀
268		nfcv 2904	. . . . . . . . 9 ⊢ Ⅎ𝑥𝑦
269	267, 268	nffv 6915	. . . . . . . 8 ⊢ Ⅎ𝑥(𝑀‘𝑦)
270		nfcv 2904	. . . . . . . . 9 ⊢ Ⅎ𝑥𝑧
271	267, 270	nffv 6915	. . . . . . . 8 ⊢ Ⅎ𝑥(𝑀‘𝑧)
272	269, 271	nfeq 2918	. . . . . . 7 ⊢ Ⅎ𝑥(𝑀‘𝑦) = (𝑀‘𝑧)
273		nfv 1913	. . . . . . 7 ⊢ Ⅎ𝑥 𝑦 = 𝑧
274	272, 273	nfim 1895	. . . . . 6 ⊢ Ⅎ𝑥((𝑀‘𝑦) = (𝑀‘𝑧) → 𝑦 = 𝑧)
275		nfv 1913	. . . . . 6 ⊢ Ⅎ𝑧((𝑀‘𝑦) = (𝑀‘𝑥) → 𝑦 = 𝑥)
276		fveq2 6905	. . . . . . . 8 ⊢ (𝑧 = 𝑥 → (𝑀‘𝑧) = (𝑀‘𝑥))
277	276	eqeq2d 2747	. . . . . . 7 ⊢ (𝑧 = 𝑥 → ((𝑀‘𝑦) = (𝑀‘𝑧) ↔ (𝑀‘𝑦) = (𝑀‘𝑥)))
278		equequ2 2024	. . . . . . 7 ⊢ (𝑧 = 𝑥 → (𝑦 = 𝑧 ↔ 𝑦 = 𝑥))
279	277, 278	imbi12d 344	. . . . . 6 ⊢ (𝑧 = 𝑥 → (((𝑀‘𝑦) = (𝑀‘𝑧) → 𝑦 = 𝑧) ↔ ((𝑀‘𝑦) = (𝑀‘𝑥) → 𝑦 = 𝑥)))
280	274, 275, 279	cbvralw 3305	. . . . 5 ⊢ (∀𝑧 ∈ (1...((𝑃 − 1) / 2))((𝑀‘𝑦) = (𝑀‘𝑧) → 𝑦 = 𝑧) ↔ ∀𝑥 ∈ (1...((𝑃 − 1) / 2))((𝑀‘𝑦) = (𝑀‘𝑥) → 𝑦 = 𝑥))
281	280	ralbii 3092	. . . 4 ⊢ (∀𝑦 ∈ (1...((𝑃 − 1) / 2))∀𝑧 ∈ (1...((𝑃 − 1) / 2))((𝑀‘𝑦) = (𝑀‘𝑧) → 𝑦 = 𝑧) ↔ ∀𝑦 ∈ (1...((𝑃 − 1) / 2))∀𝑥 ∈ (1...((𝑃 − 1) / 2))((𝑀‘𝑦) = (𝑀‘𝑥) → 𝑦 = 𝑥))
282	265, 281	sylibr 234	. . 3 ⊢ (𝜑 → ∀𝑦 ∈ (1...((𝑃 − 1) / 2))∀𝑧 ∈ (1...((𝑃 − 1) / 2))((𝑀‘𝑦) = (𝑀‘𝑧) → 𝑦 = 𝑧))
283		dff13 7276	. . 3 ⊢ (𝑀:(1...((𝑃 − 1) / 2))–1-1→(1...((𝑃 − 1) / 2)) ↔ (𝑀:(1...((𝑃 − 1) / 2))⟶(1...((𝑃 − 1) / 2)) ∧ ∀𝑦 ∈ (1...((𝑃 − 1) / 2))∀𝑧 ∈ (1...((𝑃 − 1) / 2))((𝑀‘𝑦) = (𝑀‘𝑧) → 𝑦 = 𝑧)))
284	6, 282, 283	sylanbrc 583	. 2 ⊢ (𝜑 → 𝑀:(1...((𝑃 − 1) / 2))–1-1→(1...((𝑃 − 1) / 2)))
285		ovex 7465	. . . 4 ⊢ (1...((𝑃 − 1) / 2)) ∈ V
286	285	enref 9026	. . 3 ⊢ (1...((𝑃 − 1) / 2)) ≈ (1...((𝑃 − 1) / 2))
287		fzfi 14014	. . 3 ⊢ (1...((𝑃 − 1) / 2)) ∈ Fin
288		f1finf1o 9306	. . 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))))
289	286, 287, 288	mp2an 692	. 2 ⊢ (𝑀:(1...((𝑃 − 1) / 2))–1-1→(1...((𝑃 − 1) / 2)) ↔ 𝑀:(1...((𝑃 − 1) / 2))–1-1-onto→(1...((𝑃 − 1) / 2)))
290	284, 289	sylib 218	1 ⊢ (𝜑 → 𝑀:(1...((𝑃 − 1) / 2))–1-1-onto→(1...((𝑃 − 1) / 2)))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 206 ∧ wa 395 ∨ wo 847 = wceq 1539 ∈ wcel 2107 ≠ wne 2939 ∀wral 3060 Vcvv 3479 ∖ cdif 3947 {csn 4625 {cpr 4627 class class class wbr 5142 ↦ cmpt 5224 ⟶wf 6556 –1-1→wf1 6557 –1-1-onto→wf1o 6559 ‘cfv 6560 (class class class)co 7432 ≈ cen 8983 Fincfn 8986 ℂcc 11154 ℝcr 11155 0cc0 11156 1c1 11157 + caddc 11159 · cmul 11161 < clt 11296 ≤ cle 11297 − cmin 11493 -cneg 11494 / cdiv 11921 ℕcn 12267 2c2 12322 ℕ₀cn0 12528 ℤcz 12615 ℝ⁺crp 13035 ...cfz 13548 mod cmo 13910 ↑cexp 14103 ∥ cdvds 16291 gcd cgcd 16532 ℙcprime 16709

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1794 ax-4 1808 ax-5 1909 ax-6 1966 ax-7 2006 ax-8 2109 ax-9 2117 ax-10 2140 ax-11 2156 ax-12 2176 ax-ext 2707 ax-sep 5295 ax-nul 5305 ax-pow 5364 ax-pr 5431 ax-un 7756 ax-cnex 11212 ax-resscn 11213 ax-1cn 11214 ax-icn 11215 ax-addcl 11216 ax-addrcl 11217 ax-mulcl 11218 ax-mulrcl 11219 ax-mulcom 11220 ax-addass 11221 ax-mulass 11222 ax-distr 11223 ax-i2m1 11224 ax-1ne0 11225 ax-1rid 11226 ax-rnegex 11227 ax-rrecex 11228 ax-cnre 11229 ax-pre-lttri 11230 ax-pre-lttrn 11231 ax-pre-ltadd 11232 ax-pre-mulgt0 11233 ax-pre-sup 11234

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1542 df-fal 1552 df-ex 1779 df-nf 1783 df-sb 2064 df-mo 2539 df-eu 2568 df-clab 2714 df-cleq 2728 df-clel 2815 df-nfc 2891 df-ne 2940 df-nel 3046 df-ral 3061 df-rex 3070 df-rmo 3379 df-reu 3380 df-rab 3436 df-v 3481 df-sbc 3788 df-csb 3899 df-dif 3953 df-un 3955 df-in 3957 df-ss 3967 df-pss 3970 df-nul 4333 df-if 4525 df-pw 4601 df-sn 4626 df-pr 4628 df-op 4632 df-uni 4907 df-iun 4992 df-br 5143 df-opab 5205 df-mpt 5225 df-tr 5259 df-id 5577 df-eprel 5583 df-po 5591 df-so 5592 df-fr 5636 df-we 5638 df-xp 5690 df-rel 5691 df-cnv 5692 df-co 5693 df-dm 5694 df-rn 5695 df-res 5696 df-ima 5697 df-pred 6320 df-ord 6386 df-on 6387 df-lim 6388 df-suc 6389 df-iota 6513 df-fun 6562 df-fn 6563 df-f 6564 df-f1 6565 df-fo 6566 df-f1o 6567 df-fv 6568 df-riota 7389 df-ov 7435 df-oprab 7436 df-mpo 7437 df-om 7889 df-1st 8015 df-2nd 8016 df-frecs 8307 df-wrecs 8338 df-recs 8412 df-rdg 8451 df-1o 8507 df-2o 8508 df-er 8746 df-en 8987 df-dom 8988 df-sdom 8989 df-fin 8990 df-sup 9483 df-inf 9484 df-pnf 11298 df-mnf 11299 df-xr 11300 df-ltxr 11301 df-le 11302 df-sub 11495 df-neg 11496 df-div 11922 df-nn 12268 df-2 12330 df-3 12331 df-n0 12529 df-z 12616 df-uz 12880 df-rp 13036 df-fz 13549 df-fl 13833 df-mod 13911 df-seq 14044 df-exp 14104 df-cj 15139 df-re 15140 df-im 15141 df-sqrt 15275 df-abs 15276 df-dvds 16292 df-gcd 16533 df-prm 16710

This theorem is referenced by: lgseisenlem3 27422

W3C validator