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 27285

Description: Lemma for lgseisen 27288. 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 27284	. . 3 ⊢ (𝜑 → 𝑀:(1...((𝑃 − 1) / 2))⟶(1...((𝑃 − 1) / 2)))
7		oveq2 7357	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = 𝑦 → (2 · 𝑥) = (2 · 𝑦))
8	7	oveq2d 7365	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝑦 → (𝑄 · (2 · 𝑥)) = (𝑄 · (2 · 𝑦)))
9	8	oveq1d 7364	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝑦 → ((𝑄 · (2 · 𝑥)) mod 𝑃) = ((𝑄 · (2 · 𝑦)) mod 𝑃))
10		lgseisen.6	. . . . . . . . . . . . . 14 ⊢ 𝑆 = ((𝑄 · (2 · 𝑦)) mod 𝑃)
11	9, 4, 10	3eqtr4g 2789	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑦 → 𝑅 = 𝑆)
12	11	oveq2d 7365	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑦 → (-1↑𝑅) = (-1↑𝑆))
13	12, 11	oveq12d 7367	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑦 → ((-1↑𝑅) · 𝑅) = ((-1↑𝑆) · 𝑆))
14	13	oveq1d 7364	. . . . . . . . . 10 ⊢ (𝑥 = 𝑦 → (((-1↑𝑅) · 𝑅) mod 𝑃) = (((-1↑𝑆) · 𝑆) mod 𝑃))
15	14	oveq1d 7364	. . . . . . . . 9 ⊢ (𝑥 = 𝑦 → ((((-1↑𝑅) · 𝑅) mod 𝑃) / 2) = ((((-1↑𝑆) · 𝑆) mod 𝑃) / 2))
16		ovex 7382	. . . . . . . . 9 ⊢ ((((-1↑𝑆) · 𝑆) mod 𝑃) / 2) ∈ V
17	15, 5, 16	fvmpt 6930	. . . . . . . 8 ⊢ (𝑦 ∈ (1...((𝑃 − 1) / 2)) → (𝑀‘𝑦) = ((((-1↑𝑆) · 𝑆) mod 𝑃) / 2))
18	17	ad2antrl 728	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → (𝑀‘𝑦) = ((((-1↑𝑆) · 𝑆) mod 𝑃) / 2))
19		ovex 7382	. . . . . . . . 9 ⊢ ((((-1↑𝑅) · 𝑅) mod 𝑃) / 2) ∈ V
20	5	fvmpt2 6941	. . . . . . . . 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 2745	. . . . . 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 3915	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → 𝑄 ∈ ℙ)
26		prmz 16586	. . . . . . . . . . . . . . . . 17 ⊢ (𝑄 ∈ ℙ → 𝑄 ∈ ℤ)
27	25, 26	syl 17	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → 𝑄 ∈ ℤ)
28		2z 12507	. . . . . . . . . . . . . . . . 17 ⊢ 2 ∈ ℤ
29		elfzelz 13427	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 ∈ (1...((𝑃 − 1) / 2)) → 𝑦 ∈ ℤ)
30	29	ad2antrl 728	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → 𝑦 ∈ ℤ)
31		zmulcl 12524	. . . . . . . . . . . . . . . . 17 ⊢ ((2 ∈ ℤ ∧ 𝑦 ∈ ℤ) → (2 · 𝑦) ∈ ℤ)
32	28, 30, 31	sylancr 587	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → (2 · 𝑦) ∈ ℤ)
33	27, 32	zmulcld 12586	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → (𝑄 · (2 · 𝑦)) ∈ ℤ)
34	1	adantr 480	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → 𝑃 ∈ (ℙ ∖ {2}))
35	34	eldifad 3915	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → 𝑃 ∈ ℙ)
36		prmnn 16585	. . . . . . . . . . . . . . . 16 ⊢ (𝑃 ∈ ℙ → 𝑃 ∈ ℕ)
37	35, 36	syl 17	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → 𝑃 ∈ ℕ)
38	33, 37	zmodcld 13796	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → ((𝑄 · (2 · 𝑦)) mod 𝑃) ∈ ℕ₀)
39	10, 38	eqeltrid 2832	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → 𝑆 ∈ ℕ₀)
40	39	nn0zd 12497	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → 𝑆 ∈ ℤ)
41		m1expcl 13993	. . . . . . . . . . . 12 ⊢ (𝑆 ∈ ℤ → (-1↑𝑆) ∈ ℤ)
42	40, 41	syl 17	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → (-1↑𝑆) ∈ ℤ)
43	42, 40	zmulcld 12586	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → ((-1↑𝑆) · 𝑆) ∈ ℤ)
44	43, 37	zmodcld 13796	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → (((-1↑𝑆) · 𝑆) mod 𝑃) ∈ ℕ₀)
45	44	nn0cnd 12447	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → (((-1↑𝑆) · 𝑆) mod 𝑃) ∈ ℂ)
46		elfzelz 13427	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 ∈ (1...((𝑃 − 1) / 2)) → 𝑥 ∈ ℤ)
47	46	ad2antll 729	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → 𝑥 ∈ ℤ)
48		zmulcl 12524	. . . . . . . . . . . . . . . . 17 ⊢ ((2 ∈ ℤ ∧ 𝑥 ∈ ℤ) → (2 · 𝑥) ∈ ℤ)
49	28, 47, 48	sylancr 587	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → (2 · 𝑥) ∈ ℤ)
50	27, 49	zmulcld 12586	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → (𝑄 · (2 · 𝑥)) ∈ ℤ)
51	50, 37	zmodcld 13796	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → ((𝑄 · (2 · 𝑥)) mod 𝑃) ∈ ℕ₀)
52	4, 51	eqeltrid 2832	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → 𝑅 ∈ ℕ₀)
53	52	nn0zd 12497	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → 𝑅 ∈ ℤ)
54		m1expcl 13993	. . . . . . . . . . . 12 ⊢ (𝑅 ∈ ℤ → (-1↑𝑅) ∈ ℤ)
55	53, 54	syl 17	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → (-1↑𝑅) ∈ ℤ)
56	55, 53	zmulcld 12586	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → ((-1↑𝑅) · 𝑅) ∈ ℤ)
57	56, 37	zmodcld 13796	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → (((-1↑𝑅) · 𝑅) mod 𝑃) ∈ ℕ₀)
58	57	nn0cnd 12447	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → (((-1↑𝑅) · 𝑅) mod 𝑃) ∈ ℂ)
59		2cnd 12206	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → 2 ∈ ℂ)
60		2ne0 12232	. . . . . . . . 9 ⊢ 2 ≠ 0
61	60	a1i 11	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → 2 ≠ 0)
62		div11 11807	. . . . . . . 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 1376	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → (((((-1↑𝑆) · 𝑆) mod 𝑃) / 2) = ((((-1↑𝑅) · 𝑅) mod 𝑃) / 2) ↔ (((-1↑𝑆) · 𝑆) mod 𝑃) = (((-1↑𝑅) · 𝑅) mod 𝑃)))
64	37	nnrpd 12935	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → 𝑃 ∈ ℝ⁺)
65		eqidd 2730	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → ((-1↑𝑆) mod 𝑃) = ((-1↑𝑆) mod 𝑃))
66	10	oveq1i 7359	. . . . . . . . . . 11 ⊢ (𝑆 mod 𝑃) = (((𝑄 · (2 · 𝑦)) mod 𝑃) mod 𝑃)
67	33	zred 12580	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → (𝑄 · (2 · 𝑦)) ∈ ℝ)
68		modabs2 13809	. . . . . . . . . . . 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 2776	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → (𝑆 mod 𝑃) = ((𝑄 · (2 · 𝑦)) mod 𝑃))
71	42, 42, 40, 33, 64, 65, 70	modmul12d 13832	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → (((-1↑𝑆) · 𝑆) mod 𝑃) = (((-1↑𝑆) · (𝑄 · (2 · 𝑦))) mod 𝑃))
72		eqidd 2730	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → ((-1↑𝑅) mod 𝑃) = ((-1↑𝑅) mod 𝑃))
73	4	oveq1i 7359	. . . . . . . . . . 11 ⊢ (𝑅 mod 𝑃) = (((𝑄 · (2 · 𝑥)) mod 𝑃) mod 𝑃)
74	50	zred 12580	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → (𝑄 · (2 · 𝑥)) ∈ ℝ)
75		modabs2 13809	. . . . . . . . . . . 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 2776	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → (𝑅 mod 𝑃) = ((𝑄 · (2 · 𝑥)) mod 𝑃))
78	55, 55, 53, 50, 64, 72, 77	modmul12d 13832	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → (((-1↑𝑅) · 𝑅) mod 𝑃) = (((-1↑𝑅) · (𝑄 · (2 · 𝑥))) mod 𝑃))
79	71, 78	eqeq12d 2745	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → ((((-1↑𝑆) · 𝑆) mod 𝑃) = (((-1↑𝑅) · 𝑅) mod 𝑃) ↔ (((-1↑𝑆) · (𝑄 · (2 · 𝑦))) mod 𝑃) = (((-1↑𝑅) · (𝑄 · (2 · 𝑥))) mod 𝑃)))
80	42, 33	zmulcld 12586	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → ((-1↑𝑆) · (𝑄 · (2 · 𝑦))) ∈ ℤ)
81	55, 50	zmulcld 12586	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → ((-1↑𝑅) · (𝑄 · (2 · 𝑥))) ∈ ℤ)
82		moddvds 16174	. . . . . . . . . 10 ⊢ ((𝑃 ∈ ℕ ∧ ((-1↑𝑆) · (𝑄 · (2 · 𝑦))) ∈ ℤ ∧ ((-1↑𝑅) · (𝑄 · (2 · 𝑥))) ∈ ℤ) → ((((-1↑𝑆) · (𝑄 · (2 · 𝑦))) mod 𝑃) = (((-1↑𝑅) · (𝑄 · (2 · 𝑥))) mod 𝑃) ↔ 𝑃 ∥ (((-1↑𝑆) · (𝑄 · (2 · 𝑦))) − ((-1↑𝑅) · (𝑄 · (2 · 𝑥))))))
83	37, 80, 81, 82	syl3anc 1373	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → ((((-1↑𝑆) · (𝑄 · (2 · 𝑦))) mod 𝑃) = (((-1↑𝑅) · (𝑄 · (2 · 𝑥))) mod 𝑃) ↔ 𝑃 ∥ (((-1↑𝑆) · (𝑄 · (2 · 𝑦))) − ((-1↑𝑅) · (𝑄 · (2 · 𝑥))))))
84	27	zcnd 12581	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → 𝑄 ∈ ℂ)
85	42, 32	zmulcld 12586	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → ((-1↑𝑆) · (2 · 𝑦)) ∈ ℤ)
86	85	zcnd 12581	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → ((-1↑𝑆) · (2 · 𝑦)) ∈ ℂ)
87	55, 49	zmulcld 12586	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → ((-1↑𝑅) · (2 · 𝑥)) ∈ ℤ)
88	87	zcnd 12581	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → ((-1↑𝑅) · (2 · 𝑥)) ∈ ℂ)
89	84, 86, 88	subdid 11576	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → (𝑄 · (((-1↑𝑆) · (2 · 𝑦)) − ((-1↑𝑅) · (2 · 𝑥)))) = ((𝑄 · ((-1↑𝑆) · (2 · 𝑦))) − (𝑄 · ((-1↑𝑅) · (2 · 𝑥)))))
90	42	zcnd 12581	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → (-1↑𝑆) ∈ ℂ)
91	32	zcnd 12581	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → (2 · 𝑦) ∈ ℂ)
92	84, 90, 91	mul12d 11325	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → (𝑄 · ((-1↑𝑆) · (2 · 𝑦))) = ((-1↑𝑆) · (𝑄 · (2 · 𝑦))))
93	55	zcnd 12581	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → (-1↑𝑅) ∈ ℂ)
94	49	zcnd 12581	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → (2 · 𝑥) ∈ ℂ)
95	84, 93, 94	mul12d 11325	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → (𝑄 · ((-1↑𝑅) · (2 · 𝑥))) = ((-1↑𝑅) · (𝑄 · (2 · 𝑥))))
96	92, 95	oveq12d 7367	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → ((𝑄 · ((-1↑𝑆) · (2 · 𝑦))) − (𝑄 · ((-1↑𝑅) · (2 · 𝑥)))) = (((-1↑𝑆) · (𝑄 · (2 · 𝑦))) − ((-1↑𝑅) · (𝑄 · (2 · 𝑥)))))
97	89, 96	eqtrd 2764	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → (𝑄 · (((-1↑𝑆) · (2 · 𝑦)) − ((-1↑𝑅) · (2 · 𝑥)))) = (((-1↑𝑆) · (𝑄 · (2 · 𝑦))) − ((-1↑𝑅) · (𝑄 · (2 · 𝑥)))))
98	97	breq2d 5104	. . . . . . . . . 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 16623	. . . . . . . . . . . . . 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 16586	. . . . . . . . . . . . . 14 ⊢ (𝑃 ∈ ℙ → 𝑃 ∈ ℤ)
104	35, 103	syl 17	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → 𝑃 ∈ ℤ)
105	85, 87	zsubcld 12585	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → (((-1↑𝑆) · (2 · 𝑦)) − ((-1↑𝑅) · (2 · 𝑥))) ∈ ℤ)
106		coprmdvds 16564	. . . . . . . . . . . . 13 ⊢ ((𝑃 ∈ ℤ ∧ 𝑄 ∈ ℤ ∧ (((-1↑𝑆) · (2 · 𝑦)) − ((-1↑𝑅) · (2 · 𝑥))) ∈ ℤ) → ((𝑃 ∥ (𝑄 · (((-1↑𝑆) · (2 · 𝑦)) − ((-1↑𝑅) · (2 · 𝑥)))) ∧ (𝑃 gcd 𝑄) = 1) → 𝑃 ∥ (((-1↑𝑆) · (2 · 𝑦)) − ((-1↑𝑅) · (2 · 𝑥)))))
107	104, 27, 105, 106	syl3anc 1373	. . . . . . . . . . . 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 16209	. . . . . . . . . . . 12 ⊢ ((𝑃 ∈ ℤ ∧ (-1↑𝑅) ∈ ℤ ∧ (((-1↑𝑆) · (2 · 𝑦)) − ((-1↑𝑅) · (2 · 𝑥))) ∈ ℤ) → (𝑃 ∥ (((-1↑𝑆) · (2 · 𝑦)) − ((-1↑𝑅) · (2 · 𝑥))) → 𝑃 ∥ ((-1↑𝑅) · (((-1↑𝑆) · (2 · 𝑦)) − ((-1↑𝑅) · (2 · 𝑥))))))
110	104, 55, 105, 109	syl3anc 1373	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → (𝑃 ∥ (((-1↑𝑆) · (2 · 𝑦)) − ((-1↑𝑅) · (2 · 𝑥))) → 𝑃 ∥ ((-1↑𝑅) · (((-1↑𝑆) · (2 · 𝑦)) − ((-1↑𝑅) · (2 · 𝑥))))))
111	93, 86, 88	subdid 11576	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → ((-1↑𝑅) · (((-1↑𝑆) · (2 · 𝑦)) − ((-1↑𝑅) · (2 · 𝑥)))) = (((-1↑𝑅) · ((-1↑𝑆) · (2 · 𝑦))) − ((-1↑𝑅) · ((-1↑𝑅) · (2 · 𝑥)))))
112		neg1cn 12113	. . . . . . . . . . . . . . . . . . 19 ⊢ -1 ∈ ℂ
113	112	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → -1 ∈ ℂ)
114	113, 39, 52	expaddd 14055	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → (-1↑(𝑅 + 𝑆)) = ((-1↑𝑅) · (-1↑𝑆)))
115	114	oveq1d 7364	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → ((-1↑(𝑅 + 𝑆)) · (2 · 𝑦)) = (((-1↑𝑅) · (-1↑𝑆)) · (2 · 𝑦)))
116	93, 90, 91	mulassd 11138	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → (((-1↑𝑅) · (-1↑𝑆)) · (2 · 𝑦)) = ((-1↑𝑅) · ((-1↑𝑆) · (2 · 𝑦))))
117	115, 116	eqtr2d 2765	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → ((-1↑𝑅) · ((-1↑𝑆) · (2 · 𝑦))) = ((-1↑(𝑅 + 𝑆)) · (2 · 𝑦)))
118		ax-1cn 11067	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ 1 ∈ ℂ
119		ax-1ne0 11078	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ 1 ≠ 0
120		divneg2 11848	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((1 ∈ ℂ ∧ 1 ∈ ℂ ∧ 1 ≠ 0) → -(1 / 1) = (1 / -1))
121	118, 118, 119, 120	mp3an 1463	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ -(1 / 1) = (1 / -1)
122		1div1e1 11815	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (1 / 1) = 1
123	122	negeqi 11356	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ -(1 / 1) = -1
124	121, 123	eqtr3i 2754	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (1 / -1) = -1
125	124	oveq1i 7359	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((1 / -1)↑𝑅) = (-1↑𝑅)
126		neg1ne0 12115	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ -1 ≠ 0
127	126	a1i 11	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → -1 ≠ 0)
128	113, 127, 53	exprecd 14061	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → ((1 / -1)↑𝑅) = (1 / (-1↑𝑅)))
129	125, 128	eqtr3id 2778	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → (-1↑𝑅) = (1 / (-1↑𝑅)))
130	129	oveq2d 7365	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → ((-1↑𝑅) · (-1↑𝑅)) = ((-1↑𝑅) · (1 / (-1↑𝑅))))
131	113, 127, 53	expne0d 14059	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → (-1↑𝑅) ≠ 0)
132	93, 131	recidd 11895	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → ((-1↑𝑅) · (1 / (-1↑𝑅))) = 1)
133	130, 132	eqtrd 2764	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → ((-1↑𝑅) · (-1↑𝑅)) = 1)
134	133	oveq1d 7364	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → (((-1↑𝑅) · (-1↑𝑅)) · (2 · 𝑥)) = (1 · (2 · 𝑥)))
135	93, 93, 94	mulassd 11138	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → (((-1↑𝑅) · (-1↑𝑅)) · (2 · 𝑥)) = ((-1↑𝑅) · ((-1↑𝑅) · (2 · 𝑥))))
136	94	mullidd 11133	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → (1 · (2 · 𝑥)) = (2 · 𝑥))
137	134, 135, 136	3eqtr3d 2772	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → ((-1↑𝑅) · ((-1↑𝑅) · (2 · 𝑥))) = (2 · 𝑥))
138	117, 137	oveq12d 7367	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → (((-1↑𝑅) · ((-1↑𝑆) · (2 · 𝑦))) − ((-1↑𝑅) · ((-1↑𝑅) · (2 · 𝑥)))) = (((-1↑(𝑅 + 𝑆)) · (2 · 𝑦)) − (2 · 𝑥)))
139	111, 138	eqtrd 2764	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → ((-1↑𝑅) · (((-1↑𝑆) · (2 · 𝑦)) − ((-1↑𝑅) · (2 · 𝑥)))) = (((-1↑(𝑅 + 𝑆)) · (2 · 𝑦)) − (2 · 𝑥)))
140	139	breq2d 5104	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → (𝑃 ∥ ((-1↑𝑅) · (((-1↑𝑆) · (2 · 𝑦)) − ((-1↑𝑅) · (2 · 𝑥)))) ↔ 𝑃 ∥ (((-1↑(𝑅 + 𝑆)) · (2 · 𝑦)) − (2 · 𝑥))))
141		eqcom 2736	. . . . . . . . . . . . . . . . 17 ⊢ (((-1 · (2 · 𝑦)) mod 𝑃) = ((2 · 𝑥) mod 𝑃) ↔ ((2 · 𝑥) mod 𝑃) = ((-1 · (2 · 𝑦)) mod 𝑃))
142	91	mulm1d 11572	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → (-1 · (2 · 𝑦)) = -(2 · 𝑦))
143	142	oveq1d 7364	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → ((-1 · (2 · 𝑦)) mod 𝑃) = (-(2 · 𝑦) mod 𝑃))
144	143	eqeq2d 2740	. . . . . . . . . . . . . . . . 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 12582	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → -(2 · 𝑦) ∈ ℤ)
147		moddvds 16174	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑃 ∈ ℕ ∧ (2 · 𝑥) ∈ ℤ ∧ -(2 · 𝑦) ∈ ℤ) → (((2 · 𝑥) mod 𝑃) = (-(2 · 𝑦) mod 𝑃) ↔ 𝑃 ∥ ((2 · 𝑥) − -(2 · 𝑦))))
148	37, 49, 146, 147	syl3anc 1373	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → (((2 · 𝑥) mod 𝑃) = (-(2 · 𝑦) mod 𝑃) ↔ 𝑃 ∥ ((2 · 𝑥) − -(2 · 𝑦))))
149		elfznn 13456	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑥 ∈ (1...((𝑃 − 1) / 2)) → 𝑥 ∈ ℕ)
150	149	ad2antll 729	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → 𝑥 ∈ ℕ)
151		elfznn 13456	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑦 ∈ (1...((𝑃 − 1) / 2)) → 𝑦 ∈ ℕ)
152	151	ad2antrl 728	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → 𝑦 ∈ ℕ)
153	150, 152	nnaddcld 12180	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → (𝑥 + 𝑦) ∈ ℕ)
154	150	nnred 12143	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → 𝑥 ∈ ℝ)
155	30	zred 12580	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → 𝑦 ∈ ℝ)
156		oddprm 16722	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → ((𝑃 − 1) / 2) ∈ ℕ)
157	34, 156	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → ((𝑃 − 1) / 2) ∈ ℕ)
158	157	nnred 12143	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → ((𝑃 − 1) / 2) ∈ ℝ)
159		elfzle2 13431	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑥 ∈ (1...((𝑃 − 1) / 2)) → 𝑥 ≤ ((𝑃 − 1) / 2))
160	159	ad2antll 729	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → 𝑥 ≤ ((𝑃 − 1) / 2))
161		elfzle2 13431	. . . . . . . . . . . . . . . . . . . . . . . . 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 11739	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → (𝑥 + 𝑦) ≤ (((𝑃 − 1) / 2) + ((𝑃 − 1) / 2)))
164	37	nnred 12143	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → 𝑃 ∈ ℝ)
165		peano2rem 11431	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑃 ∈ ℝ → (𝑃 − 1) ∈ ℝ)
166	164, 165	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → (𝑃 − 1) ∈ ℝ)
167	166	recnd 11143	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → (𝑃 − 1) ∈ ℂ)
168	167	2halvesd 12370	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → (((𝑃 − 1) / 2) + ((𝑃 − 1) / 2)) = (𝑃 − 1))
169	163, 168	breqtrd 5118	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → (𝑥 + 𝑦) ≤ (𝑃 − 1))
170		peano2zm 12518	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑃 ∈ ℤ → (𝑃 − 1) ∈ ℤ)
171		fznn 13495	. . . . . . . . . . . . . . . . . . . . . . 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 16233	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑃 ∈ ℕ ∧ (𝑥 + 𝑦) ∈ (1...(𝑃 − 1))) → ¬ 𝑃 ∥ (𝑥 + 𝑦))
175	37, 173, 174	syl2anc 584	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → ¬ 𝑃 ∥ (𝑥 + 𝑦))
176		eldifsni 4741	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → 𝑃 ≠ 2)
177	34, 176	syl 17	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → 𝑃 ≠ 2)
178		2prm 16603	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ 2 ∈ ℙ
179		prmrp 16623	. . . . . . . . . . . . . . . . . . . . . . 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 12498	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → (𝑥 + 𝑦) ∈ ℤ)
184		coprmdvds 16564	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑃 ∈ ℤ ∧ 2 ∈ ℤ ∧ (𝑥 + 𝑦) ∈ ℤ) → ((𝑃 ∥ (2 · (𝑥 + 𝑦)) ∧ (𝑃 gcd 2) = 1) → 𝑃 ∥ (𝑥 + 𝑦)))
185	104, 182, 183, 184	syl3anc 1373	. . . . . . . . . . . . . . . . . . . . 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 11482	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → ((2 · 𝑥) − -(2 · 𝑦)) = ((2 · 𝑥) + (2 · 𝑦)))
189	47	zcnd 12581	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → 𝑥 ∈ ℂ)
190	30	zcnd 12581	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → 𝑦 ∈ ℂ)
191	59, 189, 190	adddid 11139	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → (2 · (𝑥 + 𝑦)) = ((2 · 𝑥) + (2 · 𝑦)))
192	188, 191	eqtr4d 2767	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → ((2 · 𝑥) − -(2 · 𝑦)) = (2 · (𝑥 + 𝑦)))
193	192	breq2d 5104	. . . . . . . . . . . . . . . . . . 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 7356	. . . . . . . . . . . . . . . . . 18 ⊢ ((-1↑(𝑅 + 𝑆)) = -1 → ((-1↑(𝑅 + 𝑆)) · (2 · 𝑦)) = (-1 · (2 · 𝑦)))
199	198	oveq1d 7364	. . . . . . . . . . . . . . . . 17 ⊢ ((-1↑(𝑅 + 𝑆)) = -1 → (((-1↑(𝑅 + 𝑆)) · (2 · 𝑦)) mod 𝑃) = ((-1 · (2 · 𝑦)) mod 𝑃))
200	199	eqeq1d 2731	. . . . . . . . . . . . . . . 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 11133	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → (1 · (2 · 𝑦)) = (2 · 𝑦))
204	203	oveq1d 7364	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → ((1 · (2 · 𝑦)) mod 𝑃) = ((2 · 𝑦) mod 𝑃))
205	32	zred 12580	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → (2 · 𝑦) ∈ ℝ)
206		2nn 12201	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 2 ∈ ℕ
207		nnmulcl 12152	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((2 ∈ ℕ ∧ 𝑦 ∈ ℕ) → (2 · 𝑦) ∈ ℕ)
208	206, 152, 207	sylancr 587	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → (2 · 𝑦) ∈ ℕ)
209	208	nnnn0d 12445	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → (2 · 𝑦) ∈ ℕ₀)
210	209	nn0ge0d 12448	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → 0 ≤ (2 · 𝑦))
211		2re 12202	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ 2 ∈ ℝ
212	211	a1i 11	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → 2 ∈ ℝ)
213		2pos 12231	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ 0 < 2
214	213	a1i 11	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → 0 < 2)
215		lemuldiv2 12006	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑦 ∈ ℝ ∧ (𝑃 − 1) ∈ ℝ ∧ (2 ∈ ℝ ∧ 0 < 2)) → ((2 · 𝑦) ≤ (𝑃 − 1) ↔ 𝑦 ≤ ((𝑃 − 1) / 2)))
216	155, 166, 212, 214, 215	syl112anc 1376	. . . . . . . . . . . . . . . . . . . . 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 12528	. . . . . . . . . . . . . . . . . . . . 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 13800	. . . . . . . . . . . . . . . . . . 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 2764	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → ((1 · (2 · 𝑦)) mod 𝑃) = (2 · 𝑦))
224	49	zred 12580	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → (2 · 𝑥) ∈ ℝ)
225		nnmulcl 12152	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((2 ∈ ℕ ∧ 𝑥 ∈ ℕ) → (2 · 𝑥) ∈ ℕ)
226	206, 150, 225	sylancr 587	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → (2 · 𝑥) ∈ ℕ)
227	226	nnnn0d 12445	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → (2 · 𝑥) ∈ ℕ₀)
228	227	nn0ge0d 12448	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → 0 ≤ (2 · 𝑥))
229		lemuldiv2 12006	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑥 ∈ ℝ ∧ (𝑃 − 1) ∈ ℝ ∧ (2 ∈ ℝ ∧ 0 < 2)) → ((2 · 𝑥) ≤ (𝑃 − 1) ↔ 𝑥 ≤ ((𝑃 − 1) / 2)))
230	154, 166, 212, 214, 229	syl112anc 1376	. . . . . . . . . . . . . . . . . . . 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 12528	. . . . . . . . . . . . . . . . . . . 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 13800	. . . . . . . . . . . . . . . . . 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 2745	. . . . . . . . . . . . . . . 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 7356	. . . . . . . . . . . . . . . . . 18 ⊢ ((-1↑(𝑅 + 𝑆)) = 1 → ((-1↑(𝑅 + 𝑆)) · (2 · 𝑦)) = (1 · (2 · 𝑦)))
240	239	oveq1d 7364	. . . . . . . . . . . . . . . . 17 ⊢ ((-1↑(𝑅 + 𝑆)) = 1 → (((-1↑(𝑅 + 𝑆)) · (2 · 𝑦)) mod 𝑃) = ((1 · (2 · 𝑦)) mod 𝑃))
241	240	eqeq1d 2731	. . . . . . . . . . . . . . . 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 12449	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → (𝑅 + 𝑆) ∈ ℕ₀)
245	244	nn0zd 12497	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → (𝑅 + 𝑆) ∈ ℤ)
246		m1expcl2 13992	. . . . . . . . . . . . . . 15 ⊢ ((𝑅 + 𝑆) ∈ ℤ → (-1↑(𝑅 + 𝑆)) ∈ {-1, 1})
247		elpri 4601	. . . . . . . . . . . . . . 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 12511	. . . . . . . . . . . . . . . 16 ⊢ -1 ∈ ℤ
251		zexpcl 13983	. . . . . . . . . . . . . . . 16 ⊢ ((-1 ∈ ℤ ∧ (𝑅 + 𝑆) ∈ ℕ₀) → (-1↑(𝑅 + 𝑆)) ∈ ℤ)
252	250, 244, 251	sylancr 587	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → (-1↑(𝑅 + 𝑆)) ∈ ℤ)
253	252, 32	zmulcld 12586	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → ((-1↑(𝑅 + 𝑆)) · (2 · 𝑦)) ∈ ℤ)
254		moddvds 16174	. . . . . . . . . . . . . 14 ⊢ ((𝑃 ∈ ℕ ∧ ((-1↑(𝑅 + 𝑆)) · (2 · 𝑦)) ∈ ℤ ∧ (2 · 𝑥) ∈ ℤ) → ((((-1↑(𝑅 + 𝑆)) · (2 · 𝑦)) mod 𝑃) = ((2 · 𝑥) mod 𝑃) ↔ 𝑃 ∥ (((-1↑(𝑅 + 𝑆)) · (2 · 𝑦)) − (2 · 𝑥))))
255	37, 253, 49, 254	syl3anc 1373	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → ((((-1↑(𝑅 + 𝑆)) · (2 · 𝑦)) mod 𝑃) = ((2 · 𝑥) mod 𝑃) ↔ 𝑃 ∥ (((-1↑(𝑅 + 𝑆)) · (2 · 𝑦)) − (2 · 𝑥))))
256	190, 189, 59, 61	mulcand 11753	. . . . . . . . . . . . 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 3172	. . . 4 ⊢ (𝜑 → ∀𝑦 ∈ (1...((𝑃 − 1) / 2))∀𝑥 ∈ (1...((𝑃 − 1) / 2))((𝑀‘𝑦) = (𝑀‘𝑥) → 𝑦 = 𝑥))
266		nfmpt1 5191	. . . . . . . . . 10 ⊢ Ⅎ𝑥(𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ ((((-1↑𝑅) · 𝑅) mod 𝑃) / 2))
267	5, 266	nfcxfr 2889	. . . . . . . . 9 ⊢ Ⅎ𝑥𝑀
268		nfcv 2891	. . . . . . . . 9 ⊢ Ⅎ𝑥𝑦
269	267, 268	nffv 6832	. . . . . . . 8 ⊢ Ⅎ𝑥(𝑀‘𝑦)
270		nfcv 2891	. . . . . . . . 9 ⊢ Ⅎ𝑥𝑧
271	267, 270	nffv 6832	. . . . . . . 8 ⊢ Ⅎ𝑥(𝑀‘𝑧)
272	269, 271	nfeq 2905	. . . . . . 7 ⊢ Ⅎ𝑥(𝑀‘𝑦) = (𝑀‘𝑧)
273		nfv 1914	. . . . . . 7 ⊢ Ⅎ𝑥 𝑦 = 𝑧
274	272, 273	nfim 1896	. . . . . 6 ⊢ Ⅎ𝑥((𝑀‘𝑦) = (𝑀‘𝑧) → 𝑦 = 𝑧)
275		nfv 1914	. . . . . 6 ⊢ Ⅎ𝑧((𝑀‘𝑦) = (𝑀‘𝑥) → 𝑦 = 𝑥)
276		fveq2 6822	. . . . . . . 8 ⊢ (𝑧 = 𝑥 → (𝑀‘𝑧) = (𝑀‘𝑥))
277	276	eqeq2d 2740	. . . . . . 7 ⊢ (𝑧 = 𝑥 → ((𝑀‘𝑦) = (𝑀‘𝑧) ↔ (𝑀‘𝑦) = (𝑀‘𝑥)))
278		equequ2 2026	. . . . . . 7 ⊢ (𝑧 = 𝑥 → (𝑦 = 𝑧 ↔ 𝑦 = 𝑥))
279	277, 278	imbi12d 344	. . . . . 6 ⊢ (𝑧 = 𝑥 → (((𝑀‘𝑦) = (𝑀‘𝑧) → 𝑦 = 𝑧) ↔ ((𝑀‘𝑦) = (𝑀‘𝑥) → 𝑦 = 𝑥)))
280	274, 275, 279	cbvralw 3271	. . . . 5 ⊢ (∀𝑧 ∈ (1...((𝑃 − 1) / 2))((𝑀‘𝑦) = (𝑀‘𝑧) → 𝑦 = 𝑧) ↔ ∀𝑥 ∈ (1...((𝑃 − 1) / 2))((𝑀‘𝑦) = (𝑀‘𝑥) → 𝑦 = 𝑥))
281	280	ralbii 3075	. . . 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 7191	. . 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 7382	. . . 4 ⊢ (1...((𝑃 − 1) / 2)) ∈ V
286	285	enref 8910	. . 3 ⊢ (1...((𝑃 − 1) / 2)) ≈ (1...((𝑃 − 1) / 2))
287		fzfi 13879	. . 3 ⊢ (1...((𝑃 − 1) / 2)) ∈ Fin
288		f1finf1o 9162	. . 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 1540 ∈ wcel 2109 ≠ wne 2925 ∀wral 3044 Vcvv 3436 ∖ cdif 3900 {csn 4577 {cpr 4579 class class class wbr 5092 ↦ cmpt 5173 ⟶wf 6478 –1-1→wf1 6479 –1-1-onto→wf1o 6481 ‘cfv 6482 (class class class)co 7349 ≈ cen 8869 Fincfn 8872 ℂcc 11007 ℝcr 11008 0cc0 11009 1c1 11010 + caddc 11012 · cmul 11014 < clt 11149 ≤ cle 11150 − cmin 11347 -cneg 11348 / cdiv 11777 ℕcn 12128 2c2 12183 ℕ₀cn0 12384 ℤcz 12471 ℝ⁺crp 12893 ...cfz 13410 mod cmo 13773 ↑cexp 13968 ∥ cdvds 16163 gcd cgcd 16405 ℙcprime 16582

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2008 ax-8 2111 ax-9 2119 ax-10 2142 ax-11 2158 ax-12 2178 ax-ext 2701 ax-sep 5235 ax-nul 5245 ax-pow 5304 ax-pr 5371 ax-un 7671 ax-cnex 11065 ax-resscn 11066 ax-1cn 11067 ax-icn 11068 ax-addcl 11069 ax-addrcl 11070 ax-mulcl 11071 ax-mulrcl 11072 ax-mulcom 11073 ax-addass 11074 ax-mulass 11075 ax-distr 11076 ax-i2m1 11077 ax-1ne0 11078 ax-1rid 11079 ax-rnegex 11080 ax-rrecex 11081 ax-cnre 11082 ax-pre-lttri 11083 ax-pre-lttrn 11084 ax-pre-ltadd 11085 ax-pre-mulgt0 11086 ax-pre-sup 11087

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2066 df-mo 2533 df-eu 2562 df-clab 2708 df-cleq 2721 df-clel 2803 df-nfc 2878 df-ne 2926 df-nel 3030 df-ral 3045 df-rex 3054 df-rmo 3343 df-reu 3344 df-rab 3395 df-v 3438 df-sbc 3743 df-csb 3852 df-dif 3906 df-un 3908 df-in 3910 df-ss 3920 df-pss 3923 df-nul 4285 df-if 4477 df-pw 4553 df-sn 4578 df-pr 4580 df-op 4584 df-uni 4859 df-iun 4943 df-br 5093 df-opab 5155 df-mpt 5174 df-tr 5200 df-id 5514 df-eprel 5519 df-po 5527 df-so 5528 df-fr 5572 df-we 5574 df-xp 5625 df-rel 5626 df-cnv 5627 df-co 5628 df-dm 5629 df-rn 5630 df-res 5631 df-ima 5632 df-pred 6249 df-ord 6310 df-on 6311 df-lim 6312 df-suc 6313 df-iota 6438 df-fun 6484 df-fn 6485 df-f 6486 df-f1 6487 df-fo 6488 df-f1o 6489 df-fv 6490 df-riota 7306 df-ov 7352 df-oprab 7353 df-mpo 7354 df-om 7800 df-1st 7924 df-2nd 7925 df-frecs 8214 df-wrecs 8245 df-recs 8294 df-rdg 8332 df-1o 8388 df-2o 8389 df-er 8625 df-en 8873 df-dom 8874 df-sdom 8875 df-fin 8876 df-sup 9332 df-inf 9333 df-pnf 11151 df-mnf 11152 df-xr 11153 df-ltxr 11154 df-le 11155 df-sub 11349 df-neg 11350 df-div 11778 df-nn 12129 df-2 12191 df-3 12192 df-n0 12385 df-z 12472 df-uz 12736 df-rp 12894 df-fz 13411 df-fl 13696 df-mod 13774 df-seq 13909 df-exp 13969 df-cj 15006 df-re 15007 df-im 15008 df-sqrt 15142 df-abs 15143 df-dvds 16164 df-gcd 16406 df-prm 16583

This theorem is referenced by: lgseisenlem3 27286

W3C validator