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 27442

Description: Lemma for lgseisen 27445. 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 27441	. . 3 ⊢ (𝜑 → 𝑀:(1...((𝑃 − 1) / 2))⟶(1...((𝑃 − 1) / 2)))
7		oveq2 7406	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = 𝑦 → (2 · 𝑥) = (2 · 𝑦))
8	7	oveq2d 7414	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝑦 → (𝑄 · (2 · 𝑥)) = (𝑄 · (2 · 𝑦)))
9	8	oveq1d 7413	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝑦 → ((𝑄 · (2 · 𝑥)) mod 𝑃) = ((𝑄 · (2 · 𝑦)) mod 𝑃))
10		lgseisen.6	. . . . . . . . . . . . . 14 ⊢ 𝑆 = ((𝑄 · (2 · 𝑦)) mod 𝑃)
11	9, 4, 10	3eqtr4g 2824	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑦 → 𝑅 = 𝑆)
12	11	oveq2d 7414	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑦 → (-1↑𝑅) = (-1↑𝑆))
13	12, 11	oveq12d 7416	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑦 → ((-1↑𝑅) · 𝑅) = ((-1↑𝑆) · 𝑆))
14	13	oveq1d 7413	. . . . . . . . . 10 ⊢ (𝑥 = 𝑦 → (((-1↑𝑅) · 𝑅) mod 𝑃) = (((-1↑𝑆) · 𝑆) mod 𝑃))
15	14	oveq1d 7413	. . . . . . . . 9 ⊢ (𝑥 = 𝑦 → ((((-1↑𝑅) · 𝑅) mod 𝑃) / 2) = ((((-1↑𝑆) · 𝑆) mod 𝑃) / 2))
16		ovex 7431	. . . . . . . . 9 ⊢ ((((-1↑𝑆) · 𝑆) mod 𝑃) / 2) ∈ V
17	15, 5, 16	fvmpt 6977	. . . . . . . 8 ⊢ (𝑦 ∈ (1...((𝑃 − 1) / 2)) → (𝑀‘𝑦) = ((((-1↑𝑆) · 𝑆) mod 𝑃) / 2))
18	17	ad2antrl 738	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → (𝑀‘𝑦) = ((((-1↑𝑆) · 𝑆) mod 𝑃) / 2))
19		ovex 7431	. . . . . . . . 9 ⊢ ((((-1↑𝑅) · 𝑅) mod 𝑃) / 2) ∈ V
20	5	fvmpt2 6989	. . . . . . . . 9 ⊢ ((𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ ((((-1↑𝑅) · 𝑅) mod 𝑃) / 2) ∈ V) → (𝑀‘𝑥) = ((((-1↑𝑅) · 𝑅) mod 𝑃) / 2))
21	19, 20	mpan2 701	. . . . . . . 8 ⊢ (𝑥 ∈ (1...((𝑃 − 1) / 2)) → (𝑀‘𝑥) = ((((-1↑𝑅) · 𝑅) mod 𝑃) / 2))
22	21	ad2antll 739	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → (𝑀‘𝑥) = ((((-1↑𝑅) · 𝑅) mod 𝑃) / 2))
23	18, 22	eqeq12d 2780	. . . . . 6 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → ((𝑀‘𝑦) = (𝑀‘𝑥) ↔ ((((-1↑𝑆) · 𝑆) mod 𝑃) / 2) = ((((-1↑𝑅) · 𝑅) mod 𝑃) / 2)))
24	2	adantr 484	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → 𝑄 ∈ (ℙ ∖ {2}))
25	24	eldifad 3918	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → 𝑄 ∈ ℙ)
26		prmz 16711	. . . . . . . . . . . . . . . . 17 ⊢ (𝑄 ∈ ℙ → 𝑄 ∈ ℤ)
27	25, 26	syl 17	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → 𝑄 ∈ ℤ)
28		2z 12605	. . . . . . . . . . . . . . . . 17 ⊢ 2 ∈ ℤ
29		elfzelz 13531	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 ∈ (1...((𝑃 − 1) / 2)) → 𝑦 ∈ ℤ)
30	29	ad2antrl 738	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → 𝑦 ∈ ℤ)
31		zmulcl 12622	. . . . . . . . . . . . . . . . 17 ⊢ ((2 ∈ ℤ ∧ 𝑦 ∈ ℤ) → (2 · 𝑦) ∈ ℤ)
32	28, 30, 31	sylancr 596	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → (2 · 𝑦) ∈ ℤ)
33	27, 32	zmulcld 12685	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → (𝑄 · (2 · 𝑦)) ∈ ℤ)
34	1	adantr 484	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → 𝑃 ∈ (ℙ ∖ {2}))
35	34	eldifad 3918	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → 𝑃 ∈ ℙ)
36		prmnn 16710	. . . . . . . . . . . . . . . 16 ⊢ (𝑃 ∈ ℙ → 𝑃 ∈ ℕ)
37	35, 36	syl 17	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → 𝑃 ∈ ℕ)
38	33, 37	zmodcld 13904	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → ((𝑄 · (2 · 𝑦)) mod 𝑃) ∈ ℕ₀)
39	10, 38	eqeltrid 2868	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → 𝑆 ∈ ℕ₀)
40	39	nn0zd 12595	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → 𝑆 ∈ ℤ)
41		m1expcl 14101	. . . . . . . . . . . 12 ⊢ (𝑆 ∈ ℤ → (-1↑𝑆) ∈ ℤ)
42	40, 41	syl 17	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → (-1↑𝑆) ∈ ℤ)
43	42, 40	zmulcld 12685	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → ((-1↑𝑆) · 𝑆) ∈ ℤ)
44	43, 37	zmodcld 13904	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → (((-1↑𝑆) · 𝑆) mod 𝑃) ∈ ℕ₀)
45	44	nn0cnd 12546	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → (((-1↑𝑆) · 𝑆) mod 𝑃) ∈ ℂ)
46		elfzelz 13531	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 ∈ (1...((𝑃 − 1) / 2)) → 𝑥 ∈ ℤ)
47	46	ad2antll 739	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → 𝑥 ∈ ℤ)
48		zmulcl 12622	. . . . . . . . . . . . . . . . 17 ⊢ ((2 ∈ ℤ ∧ 𝑥 ∈ ℤ) → (2 · 𝑥) ∈ ℤ)
49	28, 47, 48	sylancr 596	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → (2 · 𝑥) ∈ ℤ)
50	27, 49	zmulcld 12685	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → (𝑄 · (2 · 𝑥)) ∈ ℤ)
51	50, 37	zmodcld 13904	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → ((𝑄 · (2 · 𝑥)) mod 𝑃) ∈ ℕ₀)
52	4, 51	eqeltrid 2868	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → 𝑅 ∈ ℕ₀)
53	52	nn0zd 12595	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → 𝑅 ∈ ℤ)
54		m1expcl 14101	. . . . . . . . . . . 12 ⊢ (𝑅 ∈ ℤ → (-1↑𝑅) ∈ ℤ)
55	53, 54	syl 17	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → (-1↑𝑅) ∈ ℤ)
56	55, 53	zmulcld 12685	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → ((-1↑𝑅) · 𝑅) ∈ ℤ)
57	56, 37	zmodcld 13904	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → (((-1↑𝑅) · 𝑅) mod 𝑃) ∈ ℕ₀)
58	57	nn0cnd 12546	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → (((-1↑𝑅) · 𝑅) mod 𝑃) ∈ ℂ)
59		2cnd 12298	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → 2 ∈ ℂ)
60		2ne0 12326	. . . . . . . . 9 ⊢ 2 ≠ 0
61	60	a1i 11	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → 2 ≠ 0)
62		div11 11875	. . . . . . . 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 1395	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → (((((-1↑𝑆) · 𝑆) mod 𝑃) / 2) = ((((-1↑𝑅) · 𝑅) mod 𝑃) / 2) ↔ (((-1↑𝑆) · 𝑆) mod 𝑃) = (((-1↑𝑅) · 𝑅) mod 𝑃)))
64	37	nnrpd 13037	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → 𝑃 ∈ ℝ⁺)
65		eqidd 2765	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → ((-1↑𝑆) mod 𝑃) = ((-1↑𝑆) mod 𝑃))
66	10	oveq1i 7408	. . . . . . . . . . 11 ⊢ (𝑆 mod 𝑃) = (((𝑄 · (2 · 𝑦)) mod 𝑃) mod 𝑃)
67	33	zred 12679	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → (𝑄 · (2 · 𝑦)) ∈ ℝ)
68		modabs2 13917	. . . . . . . . . . . 12 ⊢ (((𝑄 · (2 · 𝑦)) ∈ ℝ ∧ 𝑃 ∈ ℝ⁺) → (((𝑄 · (2 · 𝑦)) mod 𝑃) mod 𝑃) = ((𝑄 · (2 · 𝑦)) mod 𝑃))
69	67, 64, 68	syl2anc 593	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → (((𝑄 · (2 · 𝑦)) mod 𝑃) mod 𝑃) = ((𝑄 · (2 · 𝑦)) mod 𝑃))
70	66, 69	eqtrid 2811	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → (𝑆 mod 𝑃) = ((𝑄 · (2 · 𝑦)) mod 𝑃))
71	42, 42, 40, 33, 64, 65, 70	modmul12d 13940	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → (((-1↑𝑆) · 𝑆) mod 𝑃) = (((-1↑𝑆) · (𝑄 · (2 · 𝑦))) mod 𝑃))
72		eqidd 2765	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → ((-1↑𝑅) mod 𝑃) = ((-1↑𝑅) mod 𝑃))
73	4	oveq1i 7408	. . . . . . . . . . 11 ⊢ (𝑅 mod 𝑃) = (((𝑄 · (2 · 𝑥)) mod 𝑃) mod 𝑃)
74	50	zred 12679	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → (𝑄 · (2 · 𝑥)) ∈ ℝ)
75		modabs2 13917	. . . . . . . . . . . 12 ⊢ (((𝑄 · (2 · 𝑥)) ∈ ℝ ∧ 𝑃 ∈ ℝ⁺) → (((𝑄 · (2 · 𝑥)) mod 𝑃) mod 𝑃) = ((𝑄 · (2 · 𝑥)) mod 𝑃))
76	74, 64, 75	syl2anc 593	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → (((𝑄 · (2 · 𝑥)) mod 𝑃) mod 𝑃) = ((𝑄 · (2 · 𝑥)) mod 𝑃))
77	73, 76	eqtrid 2811	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → (𝑅 mod 𝑃) = ((𝑄 · (2 · 𝑥)) mod 𝑃))
78	55, 55, 53, 50, 64, 72, 77	modmul12d 13940	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → (((-1↑𝑅) · 𝑅) mod 𝑃) = (((-1↑𝑅) · (𝑄 · (2 · 𝑥))) mod 𝑃))
79	71, 78	eqeq12d 2780	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → ((((-1↑𝑆) · 𝑆) mod 𝑃) = (((-1↑𝑅) · 𝑅) mod 𝑃) ↔ (((-1↑𝑆) · (𝑄 · (2 · 𝑦))) mod 𝑃) = (((-1↑𝑅) · (𝑄 · (2 · 𝑥))) mod 𝑃)))
80	42, 33	zmulcld 12685	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → ((-1↑𝑆) · (𝑄 · (2 · 𝑦))) ∈ ℤ)
81	55, 50	zmulcld 12685	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → ((-1↑𝑅) · (𝑄 · (2 · 𝑥))) ∈ ℤ)
82		moddvds 16299	. . . . . . . . . 10 ⊢ ((𝑃 ∈ ℕ ∧ ((-1↑𝑆) · (𝑄 · (2 · 𝑦))) ∈ ℤ ∧ ((-1↑𝑅) · (𝑄 · (2 · 𝑥))) ∈ ℤ) → ((((-1↑𝑆) · (𝑄 · (2 · 𝑦))) mod 𝑃) = (((-1↑𝑅) · (𝑄 · (2 · 𝑥))) mod 𝑃) ↔ 𝑃 ∥ (((-1↑𝑆) · (𝑄 · (2 · 𝑦))) − ((-1↑𝑅) · (𝑄 · (2 · 𝑥))))))
83	37, 80, 81, 82	syl3anc 1392	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → ((((-1↑𝑆) · (𝑄 · (2 · 𝑦))) mod 𝑃) = (((-1↑𝑅) · (𝑄 · (2 · 𝑥))) mod 𝑃) ↔ 𝑃 ∥ (((-1↑𝑆) · (𝑄 · (2 · 𝑦))) − ((-1↑𝑅) · (𝑄 · (2 · 𝑥))))))
84	27	zcnd 12680	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → 𝑄 ∈ ℂ)
85	42, 32	zmulcld 12685	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → ((-1↑𝑆) · (2 · 𝑦)) ∈ ℤ)
86	85	zcnd 12680	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → ((-1↑𝑆) · (2 · 𝑦)) ∈ ℂ)
87	55, 49	zmulcld 12685	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → ((-1↑𝑅) · (2 · 𝑥)) ∈ ℤ)
88	87	zcnd 12680	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → ((-1↑𝑅) · (2 · 𝑥)) ∈ ℂ)
89	84, 86, 88	subdid 11645	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → (𝑄 · (((-1↑𝑆) · (2 · 𝑦)) − ((-1↑𝑅) · (2 · 𝑥)))) = ((𝑄 · ((-1↑𝑆) · (2 · 𝑦))) − (𝑄 · ((-1↑𝑅) · (2 · 𝑥)))))
90	42	zcnd 12680	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → (-1↑𝑆) ∈ ℂ)
91	32	zcnd 12680	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → (2 · 𝑦) ∈ ℂ)
92	84, 90, 91	mul12d 11394	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → (𝑄 · ((-1↑𝑆) · (2 · 𝑦))) = ((-1↑𝑆) · (𝑄 · (2 · 𝑦))))
93	55	zcnd 12680	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → (-1↑𝑅) ∈ ℂ)
94	49	zcnd 12680	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → (2 · 𝑥) ∈ ℂ)
95	84, 93, 94	mul12d 11394	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → (𝑄 · ((-1↑𝑅) · (2 · 𝑥))) = ((-1↑𝑅) · (𝑄 · (2 · 𝑥))))
96	92, 95	oveq12d 7416	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → ((𝑄 · ((-1↑𝑆) · (2 · 𝑦))) − (𝑄 · ((-1↑𝑅) · (2 · 𝑥)))) = (((-1↑𝑆) · (𝑄 · (2 · 𝑦))) − ((-1↑𝑅) · (𝑄 · (2 · 𝑥)))))
97	89, 96	eqtrd 2799	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → (𝑄 · (((-1↑𝑆) · (2 · 𝑦)) − ((-1↑𝑅) · (2 · 𝑥)))) = (((-1↑𝑆) · (𝑄 · (2 · 𝑦))) − ((-1↑𝑅) · (𝑄 · (2 · 𝑥)))))
98	97	breq2d 5114	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → (𝑃 ∥ (𝑄 · (((-1↑𝑆) · (2 · 𝑦)) − ((-1↑𝑅) · (2 · 𝑥)))) ↔ 𝑃 ∥ (((-1↑𝑆) · (𝑄 · (2 · 𝑦))) − ((-1↑𝑅) · (𝑄 · (2 · 𝑥))))))
99	3	adantr 484	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → 𝑃 ≠ 𝑄)
100		prmrp 16749	. . . . . . . . . . . . . 14 ⊢ ((𝑃 ∈ ℙ ∧ 𝑄 ∈ ℙ) → ((𝑃 gcd 𝑄) = 1 ↔ 𝑃 ≠ 𝑄))
101	35, 25, 100	syl2anc 593	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → ((𝑃 gcd 𝑄) = 1 ↔ 𝑃 ≠ 𝑄))
102	99, 101	mpbird 259	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → (𝑃 gcd 𝑄) = 1)
103		prmz 16711	. . . . . . . . . . . . . 14 ⊢ (𝑃 ∈ ℙ → 𝑃 ∈ ℤ)
104	35, 103	syl 17	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → 𝑃 ∈ ℤ)
105	85, 87	zsubcld 12684	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → (((-1↑𝑆) · (2 · 𝑦)) − ((-1↑𝑅) · (2 · 𝑥))) ∈ ℤ)
106		coprmdvds 16689	. . . . . . . . . . . . 13 ⊢ ((𝑃 ∈ ℤ ∧ 𝑄 ∈ ℤ ∧ (((-1↑𝑆) · (2 · 𝑦)) − ((-1↑𝑅) · (2 · 𝑥))) ∈ ℤ) → ((𝑃 ∥ (𝑄 · (((-1↑𝑆) · (2 · 𝑦)) − ((-1↑𝑅) · (2 · 𝑥)))) ∧ (𝑃 gcd 𝑄) = 1) → 𝑃 ∥ (((-1↑𝑆) · (2 · 𝑦)) − ((-1↑𝑅) · (2 · 𝑥)))))
107	104, 27, 105, 106	syl3anc 1392	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → ((𝑃 ∥ (𝑄 · (((-1↑𝑆) · (2 · 𝑦)) − ((-1↑𝑅) · (2 · 𝑥)))) ∧ (𝑃 gcd 𝑄) = 1) → 𝑃 ∥ (((-1↑𝑆) · (2 · 𝑦)) − ((-1↑𝑅) · (2 · 𝑥)))))
108	102, 107	mpan2d 704	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → (𝑃 ∥ (𝑄 · (((-1↑𝑆) · (2 · 𝑦)) − ((-1↑𝑅) · (2 · 𝑥)))) → 𝑃 ∥ (((-1↑𝑆) · (2 · 𝑦)) − ((-1↑𝑅) · (2 · 𝑥)))))
109		dvdsmultr2 16334	. . . . . . . . . . . 12 ⊢ ((𝑃 ∈ ℤ ∧ (-1↑𝑅) ∈ ℤ ∧ (((-1↑𝑆) · (2 · 𝑦)) − ((-1↑𝑅) · (2 · 𝑥))) ∈ ℤ) → (𝑃 ∥ (((-1↑𝑆) · (2 · 𝑦)) − ((-1↑𝑅) · (2 · 𝑥))) → 𝑃 ∥ ((-1↑𝑅) · (((-1↑𝑆) · (2 · 𝑦)) − ((-1↑𝑅) · (2 · 𝑥))))))
110	104, 55, 105, 109	syl3anc 1392	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → (𝑃 ∥ (((-1↑𝑆) · (2 · 𝑦)) − ((-1↑𝑅) · (2 · 𝑥))) → 𝑃 ∥ ((-1↑𝑅) · (((-1↑𝑆) · (2 · 𝑦)) − ((-1↑𝑅) · (2 · 𝑥))))))
111	93, 86, 88	subdid 11645	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → ((-1↑𝑅) · (((-1↑𝑆) · (2 · 𝑦)) − ((-1↑𝑅) · (2 · 𝑥)))) = (((-1↑𝑅) · ((-1↑𝑆) · (2 · 𝑦))) − ((-1↑𝑅) · ((-1↑𝑅) · (2 · 𝑥)))))
112		neg1cn 12182	. . . . . . . . . . . . . . . . . . 19 ⊢ -1 ∈ ℂ
113	112	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → -1 ∈ ℂ)
114	113, 39, 52	expaddd 14163	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → (-1↑(𝑅 + 𝑆)) = ((-1↑𝑅) · (-1↑𝑆)))
115	114	oveq1d 7413	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → ((-1↑(𝑅 + 𝑆)) · (2 · 𝑦)) = (((-1↑𝑅) · (-1↑𝑆)) · (2 · 𝑦)))
116	93, 90, 91	mulassd 11207	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → (((-1↑𝑅) · (-1↑𝑆)) · (2 · 𝑦)) = ((-1↑𝑅) · ((-1↑𝑆) · (2 · 𝑦))))
117	115, 116	eqtr2d 2800	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → ((-1↑𝑅) · ((-1↑𝑆) · (2 · 𝑦))) = ((-1↑(𝑅 + 𝑆)) · (2 · 𝑦)))
118		ax-1cn 11133	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ 1 ∈ ℂ
119		ax-1ne0 11144	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ 1 ≠ 0
120		divneg2 11917	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((1 ∈ ℂ ∧ 1 ∈ ℂ ∧ 1 ≠ 0) → -(1 / 1) = (1 / -1))
121	118, 118, 119, 120	mp3an 1484	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ -(1 / 1) = (1 / -1)
122		1div1e1 11883	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (1 / 1) = 1
123	122	negeqi 11425	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ -(1 / 1) = -1
124	121, 123	eqtr3i 2789	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (1 / -1) = -1
125	124	oveq1i 7408	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((1 / -1)↑𝑅) = (-1↑𝑅)
126		neg1ne0 12184	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ -1 ≠ 0
127	126	a1i 11	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → -1 ≠ 0)
128	113, 127, 53	exprecd 14169	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → ((1 / -1)↑𝑅) = (1 / (-1↑𝑅)))
129	125, 128	eqtr3id 2813	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → (-1↑𝑅) = (1 / (-1↑𝑅)))
130	129	oveq2d 7414	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → ((-1↑𝑅) · (-1↑𝑅)) = ((-1↑𝑅) · (1 / (-1↑𝑅))))
131	113, 127, 53	expne0d 14167	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → (-1↑𝑅) ≠ 0)
132	93, 131	recidd 11964	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → ((-1↑𝑅) · (1 / (-1↑𝑅))) = 1)
133	130, 132	eqtrd 2799	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → ((-1↑𝑅) · (-1↑𝑅)) = 1)
134	133	oveq1d 7413	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → (((-1↑𝑅) · (-1↑𝑅)) · (2 · 𝑥)) = (1 · (2 · 𝑥)))
135	93, 93, 94	mulassd 11207	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → (((-1↑𝑅) · (-1↑𝑅)) · (2 · 𝑥)) = ((-1↑𝑅) · ((-1↑𝑅) · (2 · 𝑥))))
136	94	mullidd 11202	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → (1 · (2 · 𝑥)) = (2 · 𝑥))
137	134, 135, 136	3eqtr3d 2807	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → ((-1↑𝑅) · ((-1↑𝑅) · (2 · 𝑥))) = (2 · 𝑥))
138	117, 137	oveq12d 7416	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → (((-1↑𝑅) · ((-1↑𝑆) · (2 · 𝑦))) − ((-1↑𝑅) · ((-1↑𝑅) · (2 · 𝑥)))) = (((-1↑(𝑅 + 𝑆)) · (2 · 𝑦)) − (2 · 𝑥)))
139	111, 138	eqtrd 2799	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → ((-1↑𝑅) · (((-1↑𝑆) · (2 · 𝑦)) − ((-1↑𝑅) · (2 · 𝑥)))) = (((-1↑(𝑅 + 𝑆)) · (2 · 𝑦)) − (2 · 𝑥)))
140	139	breq2d 5114	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → (𝑃 ∥ ((-1↑𝑅) · (((-1↑𝑆) · (2 · 𝑦)) − ((-1↑𝑅) · (2 · 𝑥)))) ↔ 𝑃 ∥ (((-1↑(𝑅 + 𝑆)) · (2 · 𝑦)) − (2 · 𝑥))))
141		eqcom 2771	. . . . . . . . . . . . . . . . 17 ⊢ (((-1 · (2 · 𝑦)) mod 𝑃) = ((2 · 𝑥) mod 𝑃) ↔ ((2 · 𝑥) mod 𝑃) = ((-1 · (2 · 𝑦)) mod 𝑃))
142	91	mulm1d 11641	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → (-1 · (2 · 𝑦)) = -(2 · 𝑦))
143	142	oveq1d 7413	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → ((-1 · (2 · 𝑦)) mod 𝑃) = (-(2 · 𝑦) mod 𝑃))
144	143	eqeq2d 2775	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → (((2 · 𝑥) mod 𝑃) = ((-1 · (2 · 𝑦)) mod 𝑃) ↔ ((2 · 𝑥) mod 𝑃) = (-(2 · 𝑦) mod 𝑃)))
145	141, 144	bitrid 285	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → (((-1 · (2 · 𝑦)) mod 𝑃) = ((2 · 𝑥) mod 𝑃) ↔ ((2 · 𝑥) mod 𝑃) = (-(2 · 𝑦) mod 𝑃)))
146	32	znegcld 12681	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → -(2 · 𝑦) ∈ ℤ)
147		moddvds 16299	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑃 ∈ ℕ ∧ (2 · 𝑥) ∈ ℤ ∧ -(2 · 𝑦) ∈ ℤ) → (((2 · 𝑥) mod 𝑃) = (-(2 · 𝑦) mod 𝑃) ↔ 𝑃 ∥ ((2 · 𝑥) − -(2 · 𝑦))))
148	37, 49, 146, 147	syl3anc 1392	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → (((2 · 𝑥) mod 𝑃) = (-(2 · 𝑦) mod 𝑃) ↔ 𝑃 ∥ ((2 · 𝑥) − -(2 · 𝑦))))
149		elfznn 13560	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑥 ∈ (1...((𝑃 − 1) / 2)) → 𝑥 ∈ ℕ)
150	149	ad2antll 739	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → 𝑥 ∈ ℕ)
151		elfznn 13560	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑦 ∈ (1...((𝑃 − 1) / 2)) → 𝑦 ∈ ℕ)
152	151	ad2antrl 738	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → 𝑦 ∈ ℕ)
153	150, 152	nnaddcld 12267	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → (𝑥 + 𝑦) ∈ ℕ)
154	150	nnred 12227	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → 𝑥 ∈ ℝ)
155	30	zred 12679	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → 𝑦 ∈ ℝ)
156		oddprm 16848	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → ((𝑃 − 1) / 2) ∈ ℕ)
157	34, 156	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → ((𝑃 − 1) / 2) ∈ ℕ)
158	157	nnred 12227	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → ((𝑃 − 1) / 2) ∈ ℝ)
159		elfzle2 13535	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑥 ∈ (1...((𝑃 − 1) / 2)) → 𝑥 ≤ ((𝑃 − 1) / 2))
160	159	ad2antll 739	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → 𝑥 ≤ ((𝑃 − 1) / 2))
161		elfzle2 13535	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑦 ∈ (1...((𝑃 − 1) / 2)) → 𝑦 ≤ ((𝑃 − 1) / 2))
162	161	ad2antrl 738	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → 𝑦 ≤ ((𝑃 − 1) / 2))
163	154, 155, 158, 158, 160, 162	le2addd 11808	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → (𝑥 + 𝑦) ≤ (((𝑃 − 1) / 2) + ((𝑃 − 1) / 2)))
164	37	nnred 12227	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → 𝑃 ∈ ℝ)
165		peano2rem 11500	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑃 ∈ ℝ → (𝑃 − 1) ∈ ℝ)
166	164, 165	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → (𝑃 − 1) ∈ ℝ)
167	166	recnd 11212	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → (𝑃 − 1) ∈ ℂ)
168	167	2halvesd 12469	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → (((𝑃 − 1) / 2) + ((𝑃 − 1) / 2)) = (𝑃 − 1))
169	163, 168	breqtrd 5128	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → (𝑥 + 𝑦) ≤ (𝑃 − 1))
170		peano2zm 12616	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑃 ∈ ℤ → (𝑃 − 1) ∈ ℤ)
171		fznn 13599	. . . . . . . . . . . . . . . . . . . . . . 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 723	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → (𝑥 + 𝑦) ∈ (1...(𝑃 − 1)))
174		fzm1ndvds 16358	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑃 ∈ ℕ ∧ (𝑥 + 𝑦) ∈ (1...(𝑃 − 1))) → ¬ 𝑃 ∥ (𝑥 + 𝑦))
175	37, 173, 174	syl2anc 593	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → ¬ 𝑃 ∥ (𝑥 + 𝑦))
176		eldifsni 4752	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → 𝑃 ≠ 2)
177	34, 176	syl 17	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → 𝑃 ≠ 2)
178		2prm 16728	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ 2 ∈ ℙ
179		prmrp 16749	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑃 ∈ ℙ ∧ 2 ∈ ℙ) → ((𝑃 gcd 2) = 1 ↔ 𝑃 ≠ 2))
180	35, 178, 179	sylancl 595	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → ((𝑃 gcd 2) = 1 ↔ 𝑃 ≠ 2))
181	177, 180	mpbird 259	. . . . . . . . . . . . . . . . . . . . 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 12596	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → (𝑥 + 𝑦) ∈ ℤ)
184		coprmdvds 16689	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑃 ∈ ℤ ∧ 2 ∈ ℤ ∧ (𝑥 + 𝑦) ∈ ℤ) → ((𝑃 ∥ (2 · (𝑥 + 𝑦)) ∧ (𝑃 gcd 2) = 1) → 𝑃 ∥ (𝑥 + 𝑦)))
185	104, 182, 183, 184	syl3anc 1392	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → ((𝑃 ∥ (2 · (𝑥 + 𝑦)) ∧ (𝑃 gcd 2) = 1) → 𝑃 ∥ (𝑥 + 𝑦)))
186	181, 185	mpan2d 704	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → (𝑃 ∥ (2 · (𝑥 + 𝑦)) → 𝑃 ∥ (𝑥 + 𝑦)))
187	175, 186	mtod 200	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → ¬ 𝑃 ∥ (2 · (𝑥 + 𝑦)))
188	94, 91	subnegd 11551	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → ((2 · 𝑥) − -(2 · 𝑦)) = ((2 · 𝑥) + (2 · 𝑦)))
189	47	zcnd 12680	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → 𝑥 ∈ ℂ)
190	30	zcnd 12680	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → 𝑦 ∈ ℂ)
191	59, 189, 190	adddid 11208	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → (2 · (𝑥 + 𝑦)) = ((2 · 𝑥) + (2 · 𝑦)))
192	188, 191	eqtr4d 2802	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → ((2 · 𝑥) − -(2 · 𝑦)) = (2 · (𝑥 + 𝑦)))
193	192	breq2d 5114	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → (𝑃 ∥ ((2 · 𝑥) − -(2 · 𝑦)) ↔ 𝑃 ∥ (2 · (𝑥 + 𝑦))))
194	187, 193	mtbird 327	. . . . . . . . . . . . . . . . . 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 242	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → (((2 · 𝑥) mod 𝑃) = (-(2 · 𝑦) mod 𝑃) → (2 · 𝑦) = (2 · 𝑥)))
197	145, 196	sylbid 242	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → (((-1 · (2 · 𝑦)) mod 𝑃) = ((2 · 𝑥) mod 𝑃) → (2 · 𝑦) = (2 · 𝑥)))
198		oveq1 7405	. . . . . . . . . . . . . . . . . 18 ⊢ ((-1↑(𝑅 + 𝑆)) = -1 → ((-1↑(𝑅 + 𝑆)) · (2 · 𝑦)) = (-1 · (2 · 𝑦)))
199	198	oveq1d 7413	. . . . . . . . . . . . . . . . 17 ⊢ ((-1↑(𝑅 + 𝑆)) = -1 → (((-1↑(𝑅 + 𝑆)) · (2 · 𝑦)) mod 𝑃) = ((-1 · (2 · 𝑦)) mod 𝑃))
200	199	eqeq1d 2766	. . . . . . . . . . . . . . . 16 ⊢ ((-1↑(𝑅 + 𝑆)) = -1 → ((((-1↑(𝑅 + 𝑆)) · (2 · 𝑦)) mod 𝑃) = ((2 · 𝑥) mod 𝑃) ↔ ((-1 · (2 · 𝑦)) mod 𝑃) = ((2 · 𝑥) mod 𝑃)))
201	200	imbi1d 343	. . . . . . . . . . . . . . 15 ⊢ ((-1↑(𝑅 + 𝑆)) = -1 → (((((-1↑(𝑅 + 𝑆)) · (2 · 𝑦)) mod 𝑃) = ((2 · 𝑥) mod 𝑃) → (2 · 𝑦) = (2 · 𝑥)) ↔ (((-1 · (2 · 𝑦)) mod 𝑃) = ((2 · 𝑥) mod 𝑃) → (2 · 𝑦) = (2 · 𝑥))))
202	197, 201	syl5ibrcom 249	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → ((-1↑(𝑅 + 𝑆)) = -1 → ((((-1↑(𝑅 + 𝑆)) · (2 · 𝑦)) mod 𝑃) = ((2 · 𝑥) mod 𝑃) → (2 · 𝑦) = (2 · 𝑥))))
203	91	mullidd 11202	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → (1 · (2 · 𝑦)) = (2 · 𝑦))
204	203	oveq1d 7413	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → ((1 · (2 · 𝑦)) mod 𝑃) = ((2 · 𝑦) mod 𝑃))
205	32	zred 12679	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → (2 · 𝑦) ∈ ℝ)
206		2nn 12293	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 2 ∈ ℕ
207		nnmulcl 12236	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((2 ∈ ℕ ∧ 𝑦 ∈ ℕ) → (2 · 𝑦) ∈ ℕ)
208	206, 152, 207	sylancr 596	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → (2 · 𝑦) ∈ ℕ)
209	208	nnnn0d 12544	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → (2 · 𝑦) ∈ ℕ₀)
210	209	nn0ge0d 12547	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → 0 ≤ (2 · 𝑦))
211		2re 12294	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ 2 ∈ ℝ
212	211	a1i 11	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → 2 ∈ ℝ)
213		2pos 12324	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ 0 < 2
214	213	a1i 11	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → 0 < 2)
215		lemuldiv2 12075	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑦 ∈ ℝ ∧ (𝑃 − 1) ∈ ℝ ∧ (2 ∈ ℝ ∧ 0 < 2)) → ((2 · 𝑦) ≤ (𝑃 − 1) ↔ 𝑦 ≤ ((𝑃 − 1) / 2)))
216	155, 166, 212, 214, 215	syl112anc 1395	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → ((2 · 𝑦) ≤ (𝑃 − 1) ↔ 𝑦 ≤ ((𝑃 − 1) / 2)))
217	162, 216	mpbird 259	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → (2 · 𝑦) ≤ (𝑃 − 1))
218		zltlem1 12626	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((2 · 𝑦) ∈ ℤ ∧ 𝑃 ∈ ℤ) → ((2 · 𝑦) < 𝑃 ↔ (2 · 𝑦) ≤ (𝑃 − 1)))
219	32, 104, 218	syl2anc 593	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → ((2 · 𝑦) < 𝑃 ↔ (2 · 𝑦) ≤ (𝑃 − 1)))
220	217, 219	mpbird 259	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → (2 · 𝑦) < 𝑃)
221		modid 13908	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((2 · 𝑦) ∈ ℝ ∧ 𝑃 ∈ ℝ⁺) ∧ (0 ≤ (2 · 𝑦) ∧ (2 · 𝑦) < 𝑃)) → ((2 · 𝑦) mod 𝑃) = (2 · 𝑦))
222	205, 64, 210, 220, 221	syl22anc 849	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → ((2 · 𝑦) mod 𝑃) = (2 · 𝑦))
223	204, 222	eqtrd 2799	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → ((1 · (2 · 𝑦)) mod 𝑃) = (2 · 𝑦))
224	49	zred 12679	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → (2 · 𝑥) ∈ ℝ)
225		nnmulcl 12236	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((2 ∈ ℕ ∧ 𝑥 ∈ ℕ) → (2 · 𝑥) ∈ ℕ)
226	206, 150, 225	sylancr 596	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → (2 · 𝑥) ∈ ℕ)
227	226	nnnn0d 12544	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → (2 · 𝑥) ∈ ℕ₀)
228	227	nn0ge0d 12547	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → 0 ≤ (2 · 𝑥))
229		lemuldiv2 12075	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑥 ∈ ℝ ∧ (𝑃 − 1) ∈ ℝ ∧ (2 ∈ ℝ ∧ 0 < 2)) → ((2 · 𝑥) ≤ (𝑃 − 1) ↔ 𝑥 ≤ ((𝑃 − 1) / 2)))
230	154, 166, 212, 214, 229	syl112anc 1395	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → ((2 · 𝑥) ≤ (𝑃 − 1) ↔ 𝑥 ≤ ((𝑃 − 1) / 2)))
231	160, 230	mpbird 259	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → (2 · 𝑥) ≤ (𝑃 − 1))
232		zltlem1 12626	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((2 · 𝑥) ∈ ℤ ∧ 𝑃 ∈ ℤ) → ((2 · 𝑥) < 𝑃 ↔ (2 · 𝑥) ≤ (𝑃 − 1)))
233	49, 104, 232	syl2anc 593	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → ((2 · 𝑥) < 𝑃 ↔ (2 · 𝑥) ≤ (𝑃 − 1)))
234	231, 233	mpbird 259	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → (2 · 𝑥) < 𝑃)
235		modid 13908	. . . . . . . . . . . . . . . . . 18 ⊢ ((((2 · 𝑥) ∈ ℝ ∧ 𝑃 ∈ ℝ⁺) ∧ (0 ≤ (2 · 𝑥) ∧ (2 · 𝑥) < 𝑃)) → ((2 · 𝑥) mod 𝑃) = (2 · 𝑥))
236	224, 64, 228, 234, 235	syl22anc 849	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → ((2 · 𝑥) mod 𝑃) = (2 · 𝑥))
237	223, 236	eqeq12d 2780	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → (((1 · (2 · 𝑦)) mod 𝑃) = ((2 · 𝑥) mod 𝑃) ↔ (2 · 𝑦) = (2 · 𝑥)))
238	237	biimpd 231	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → (((1 · (2 · 𝑦)) mod 𝑃) = ((2 · 𝑥) mod 𝑃) → (2 · 𝑦) = (2 · 𝑥)))
239		oveq1 7405	. . . . . . . . . . . . . . . . . 18 ⊢ ((-1↑(𝑅 + 𝑆)) = 1 → ((-1↑(𝑅 + 𝑆)) · (2 · 𝑦)) = (1 · (2 · 𝑦)))
240	239	oveq1d 7413	. . . . . . . . . . . . . . . . 17 ⊢ ((-1↑(𝑅 + 𝑆)) = 1 → (((-1↑(𝑅 + 𝑆)) · (2 · 𝑦)) mod 𝑃) = ((1 · (2 · 𝑦)) mod 𝑃))
241	240	eqeq1d 2766	. . . . . . . . . . . . . . . 16 ⊢ ((-1↑(𝑅 + 𝑆)) = 1 → ((((-1↑(𝑅 + 𝑆)) · (2 · 𝑦)) mod 𝑃) = ((2 · 𝑥) mod 𝑃) ↔ ((1 · (2 · 𝑦)) mod 𝑃) = ((2 · 𝑥) mod 𝑃)))
242	241	imbi1d 343	. . . . . . . . . . . . . . 15 ⊢ ((-1↑(𝑅 + 𝑆)) = 1 → (((((-1↑(𝑅 + 𝑆)) · (2 · 𝑦)) mod 𝑃) = ((2 · 𝑥) mod 𝑃) → (2 · 𝑦) = (2 · 𝑥)) ↔ (((1 · (2 · 𝑦)) mod 𝑃) = ((2 · 𝑥) mod 𝑃) → (2 · 𝑦) = (2 · 𝑥))))
243	238, 242	syl5ibrcom 249	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → ((-1↑(𝑅 + 𝑆)) = 1 → ((((-1↑(𝑅 + 𝑆)) · (2 · 𝑦)) mod 𝑃) = ((2 · 𝑥) mod 𝑃) → (2 · 𝑦) = (2 · 𝑥))))
244	52, 39	nn0addcld 12548	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → (𝑅 + 𝑆) ∈ ℕ₀)
245	244	nn0zd 12595	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → (𝑅 + 𝑆) ∈ ℤ)
246		m1expcl2 14100	. . . . . . . . . . . . . . 15 ⊢ ((𝑅 + 𝑆) ∈ ℤ → (-1↑(𝑅 + 𝑆)) ∈ {-1, 1})
247		elpri 4608	. . . . . . . . . . . . . . 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 871	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → ((((-1↑(𝑅 + 𝑆)) · (2 · 𝑦)) mod 𝑃) = ((2 · 𝑥) mod 𝑃) → (2 · 𝑦) = (2 · 𝑥)))
250		neg1z 12609	. . . . . . . . . . . . . . . 16 ⊢ -1 ∈ ℤ
251		zexpcl 14091	. . . . . . . . . . . . . . . 16 ⊢ ((-1 ∈ ℤ ∧ (𝑅 + 𝑆) ∈ ℕ₀) → (-1↑(𝑅 + 𝑆)) ∈ ℤ)
252	250, 244, 251	sylancr 596	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → (-1↑(𝑅 + 𝑆)) ∈ ℤ)
253	252, 32	zmulcld 12685	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → ((-1↑(𝑅 + 𝑆)) · (2 · 𝑦)) ∈ ℤ)
254		moddvds 16299	. . . . . . . . . . . . . 14 ⊢ ((𝑃 ∈ ℕ ∧ ((-1↑(𝑅 + 𝑆)) · (2 · 𝑦)) ∈ ℤ ∧ (2 · 𝑥) ∈ ℤ) → ((((-1↑(𝑅 + 𝑆)) · (2 · 𝑦)) mod 𝑃) = ((2 · 𝑥) mod 𝑃) ↔ 𝑃 ∥ (((-1↑(𝑅 + 𝑆)) · (2 · 𝑦)) − (2 · 𝑥))))
255	37, 253, 49, 254	syl3anc 1392	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → ((((-1↑(𝑅 + 𝑆)) · (2 · 𝑦)) mod 𝑃) = ((2 · 𝑥) mod 𝑃) ↔ 𝑃 ∥ (((-1↑(𝑅 + 𝑆)) · (2 · 𝑦)) − (2 · 𝑥))))
256	190, 189, 59, 61	mulcand 11822	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → ((2 · 𝑦) = (2 · 𝑥) ↔ 𝑦 = 𝑥))
257	249, 255, 256	3imtr3d 295	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → (𝑃 ∥ (((-1↑(𝑅 + 𝑆)) · (2 · 𝑦)) − (2 · 𝑥)) → 𝑦 = 𝑥))
258	140, 257	sylbid 242	. . . . . . . . . . 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 262	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → (𝑃 ∥ (((-1↑𝑆) · (𝑄 · (2 · 𝑦))) − ((-1↑𝑅) · (𝑄 · (2 · 𝑥)))) → 𝑦 = 𝑥))
261	83, 260	sylbid 242	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → ((((-1↑𝑆) · (𝑄 · (2 · 𝑦))) mod 𝑃) = (((-1↑𝑅) · (𝑄 · (2 · 𝑥))) mod 𝑃) → 𝑦 = 𝑥))
262	79, 261	sylbid 242	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → ((((-1↑𝑆) · 𝑆) mod 𝑃) = (((-1↑𝑅) · 𝑅) mod 𝑃) → 𝑦 = 𝑥))
263	63, 262	sylbid 242	. . . . . 6 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → (((((-1↑𝑆) · 𝑆) mod 𝑃) / 2) = ((((-1↑𝑅) · 𝑅) mod 𝑃) / 2) → 𝑦 = 𝑥))
264	23, 263	sylbid 242	. . . . 5 ⊢ ((𝜑 ∧ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2)))) → ((𝑀‘𝑦) = (𝑀‘𝑥) → 𝑦 = 𝑥))
265	264	ralrimivva 3207	. . . 4 ⊢ (𝜑 → ∀𝑦 ∈ (1...((𝑃 − 1) / 2))∀𝑥 ∈ (1...((𝑃 − 1) / 2))((𝑀‘𝑦) = (𝑀‘𝑥) → 𝑦 = 𝑥))
266		nfmpt1 5201	. . . . . . . . . 10 ⊢ Ⅎ𝑥(𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ ((((-1↑𝑅) · 𝑅) mod 𝑃) / 2))
267	5, 266	nfcxfr 2924	. . . . . . . . 9 ⊢ Ⅎ𝑥𝑀
268		nfcv 2926	. . . . . . . . 9 ⊢ Ⅎ𝑥𝑦
269	267, 268	nffv 6879	. . . . . . . 8 ⊢ Ⅎ𝑥(𝑀‘𝑦)
270		nfcv 2926	. . . . . . . . 9 ⊢ Ⅎ𝑥𝑧
271	267, 270	nffv 6879	. . . . . . . 8 ⊢ Ⅎ𝑥(𝑀‘𝑧)
272	269, 271	nfeq 2939	. . . . . . 7 ⊢ Ⅎ𝑥(𝑀‘𝑦) = (𝑀‘𝑧)
273		nfv 1936	. . . . . . 7 ⊢ Ⅎ𝑥 𝑦 = 𝑧
274	272, 273	nfim 1918	. . . . . 6 ⊢ Ⅎ𝑥((𝑀‘𝑦) = (𝑀‘𝑧) → 𝑦 = 𝑧)
275		nfv 1936	. . . . . 6 ⊢ Ⅎ𝑧((𝑀‘𝑦) = (𝑀‘𝑥) → 𝑦 = 𝑥)
276		fveq2 6869	. . . . . . . 8 ⊢ (𝑧 = 𝑥 → (𝑀‘𝑧) = (𝑀‘𝑥))
277	276	eqeq2d 2775	. . . . . . 7 ⊢ (𝑧 = 𝑥 → ((𝑀‘𝑦) = (𝑀‘𝑧) ↔ (𝑀‘𝑦) = (𝑀‘𝑥)))
278		equequ2 2048	. . . . . . 7 ⊢ (𝑧 = 𝑥 → (𝑦 = 𝑧 ↔ 𝑦 = 𝑥))
279	277, 278	imbi12d 346	. . . . . 6 ⊢ (𝑧 = 𝑥 → (((𝑀‘𝑦) = (𝑀‘𝑧) → 𝑦 = 𝑧) ↔ ((𝑀‘𝑦) = (𝑀‘𝑥) → 𝑦 = 𝑥)))
280	274, 275, 279	cbvralw 3306	. . . . 5 ⊢ (∀𝑧 ∈ (1...((𝑃 − 1) / 2))((𝑀‘𝑦) = (𝑀‘𝑧) → 𝑦 = 𝑧) ↔ ∀𝑥 ∈ (1...((𝑃 − 1) / 2))((𝑀‘𝑦) = (𝑀‘𝑥) → 𝑦 = 𝑥))
281	280	ralbii 3110	. . . 4 ⊢ (∀𝑦 ∈ (1...((𝑃 − 1) / 2))∀𝑧 ∈ (1...((𝑃 − 1) / 2))((𝑀‘𝑦) = (𝑀‘𝑧) → 𝑦 = 𝑧) ↔ ∀𝑦 ∈ (1...((𝑃 − 1) / 2))∀𝑥 ∈ (1...((𝑃 − 1) / 2))((𝑀‘𝑦) = (𝑀‘𝑥) → 𝑦 = 𝑥))
282	265, 281	sylibr 236	. . 3 ⊢ (𝜑 → ∀𝑦 ∈ (1...((𝑃 − 1) / 2))∀𝑧 ∈ (1...((𝑃 − 1) / 2))((𝑀‘𝑦) = (𝑀‘𝑧) → 𝑦 = 𝑧))
283		dff13 7240	. . 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 592	. 2 ⊢ (𝜑 → 𝑀:(1...((𝑃 − 1) / 2))–1-1→(1...((𝑃 − 1) / 2)))
285		ovex 7431	. . . 4 ⊢ (1...((𝑃 − 1) / 2)) ∈ V
286	285	enref 8968	. . 3 ⊢ (1...((𝑃 − 1) / 2)) ≈ (1...((𝑃 − 1) / 2))
287		fzfi 13987	. . 3 ⊢ (1...((𝑃 − 1) / 2)) ∈ Fin
288		f1finf1o 9219	. . 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 702	. 2 ⊢ (𝑀:(1...((𝑃 − 1) / 2))–1-1→(1...((𝑃 − 1) / 2)) ↔ 𝑀:(1...((𝑃 − 1) / 2))–1-1-onto→(1...((𝑃 − 1) / 2)))
290	284, 289	sylib 220	1 ⊢ (𝜑 → 𝑀:(1...((𝑃 − 1) / 2))–1-1-onto→(1...((𝑃 − 1) / 2)))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 208 ∧ wa 399 ∨ wo 858 = wceq 1562 ∈ wcel 2144 ≠ wne 2959 ∀wral 3078 Vcvv 3456 ∖ cdif 3903 {csn 4584 {cpr 4586 class class class wbr 5102 ↦ cmpt 5183 ⟶wf 6519 –1-1→wf1 6520 –1-1-onto→wf1o 6522 ‘cfv 6523 (class class class)co 7398 ≈ cen 8926 Fincfn 8929 ℂcc 11073 ℝcr 11074 0cc0 11075 1c1 11076 + caddc 11078 · cmul 11080 < clt 11218 ≤ cle 11219 − cmin 11416 -cneg 11417 / cdiv 11846 ℕcn 12212 2c2 12274 ℕ₀cn0 12483 ℤcz 12570 ℝ⁺crp 12995 ...cfz 13514 mod cmo 13881 ↑cexp 14076 ∥ cdvds 16288 gcd cgcd 16530 ℙcprime 16707

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1817 ax-4 1831 ax-5 1932 ax-6 1989 ax-7 2030 ax-8 2146 ax-9 2154 ax-10 2177 ax-11 2193 ax-12 2214 ax-ext 2736 ax-sep 5248 ax-nul 5258 ax-pow 5324 ax-pr 5392 ax-un 7720 ax-cnex 11131 ax-resscn 11132 ax-1cn 11133 ax-icn 11134 ax-addcl 11135 ax-addrcl 11136 ax-mulcl 11137 ax-mulrcl 11138 ax-mulcom 11139 ax-addass 11140 ax-mulass 11141 ax-distr 11142 ax-i2m1 11143 ax-1ne0 11144 ax-1rid 11145 ax-rnegex 11146 ax-rrecex 11147 ax-cnre 11148 ax-pre-lttri 11149 ax-pre-lttrn 11150 ax-pre-ltadd 11151 ax-pre-mulgt0 11152 ax-pre-sup 11153

This theorem depends on definitions: df-bi 209 df-an 400 df-or 859 df-3or 1100 df-3an 1101 df-tru 1565 df-fal 1575 df-ex 1802 df-nf 1806 df-sb 2093 df-mo 2568 df-eu 2598 df-clab 2743 df-cleq 2756 df-clel 2839 df-nfc 2913 df-ne 2960 df-nel 3064 df-ral 3079 df-rex 3089 df-rmo 3369 df-reu 3370 df-rab 3417 df-v 3458 df-sbc 3747 df-csb 3855 df-dif 3909 df-un 3911 df-in 3913 df-ss 3923 df-pss 3926 df-nul 4288 df-if 4483 df-pw 4559 df-sn 4585 df-pr 4587 df-op 4591 df-uni 4868 df-iun 4953 df-br 5103 df-opab 5165 df-mpt 5184 df-tr 5210 df-id 5544 df-eprel 5549 df-po 5557 df-so 5558 df-fr 5602 df-we 5604 df-xp 5655 df-rel 5656 df-cnv 5657 df-co 5658 df-dm 5659 df-rn 5660 df-res 5661 df-ima 5662 df-pred 6290 df-ord 6351 df-on 6352 df-lim 6353 df-suc 6354 df-iota 6479 df-fun 6525 df-fn 6526 df-f 6527 df-f1 6528 df-fo 6529 df-f1o 6530 df-fv 6531 df-riota 7355 df-ov 7401 df-oprab 7402 df-mpo 7403 df-om 7849 df-1st 7972 df-2nd 7973 df-frecs 8264 df-wrecs 8295 df-recs 8344 df-rdg 8383 df-1o 8439 df-2o 8440 df-er 8680 df-en 8930 df-dom 8931 df-sdom 8932 df-fin 8933 df-sup 9390 df-inf 9391 df-pnf 11220 df-mnf 11221 df-xr 11222 df-ltxr 11223 df-le 11224 df-sub 11418 df-neg 11419 df-div 11847 df-nn 12213 df-2 12282 df-3 12283 df-n0 12484 df-z 12571 df-uz 12842 df-rp 12996 df-fz 13515 df-fl 13804 df-mod 13882 df-seq 14017 df-exp 14077 df-cj 15128 df-re 15129 df-im 15130 df-sqrt 15264 df-abs 15265 df-dvds 16289 df-gcd 16531 df-prm 16708

This theorem is referenced by: lgseisenlem3 27443

W3C validator