lgseisenlem1 - Intuitionistic Logic Explorer

	Intuitionistic Logic Explorer		< Previous Next > Nearby theorems
Mirrors > Home > ILE Home > Th. List > lgseisenlem1		GIF version

Theorem lgseisenlem1 15798

Description: Lemma for lgseisen 15802. If 𝑅(𝑢) = (𝑄 · 𝑢) mod 𝑃 and 𝑀(𝑢) = (-1↑𝑅(𝑢)) · 𝑅(𝑢), then for any even 1 ≤ 𝑢 ≤ 𝑃 − 1, 𝑀(𝑢) is also an even integer 1 ≤ 𝑀(𝑢) ≤ 𝑃 − 1. To simplify these statements, we divide all the even numbers by 2, so that it becomes the statement that 𝑀(𝑥 / 2) = (-1↑𝑅(𝑥 / 2)) · 𝑅(𝑥 / 2) / 2 is an integer between 1 and (𝑃 − 1) / 2. (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))

**Assertion**
Ref	Expression
lgseisenlem1	⊢ (𝜑 → 𝑀:(1...((𝑃 − 1) / 2))⟶(1...((𝑃 − 1) / 2)))

Distinct variable groups: 𝑥,𝑃 𝜑,𝑥 𝑥,𝑄 Allowed substitution hints: 𝑅(𝑥) 𝑀(𝑥)

**Proof of Theorem lgseisenlem1**
Step	Hyp	Ref	Expression
1		1zzd 9505	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → 1 ∈ ℤ)
2		lgseisen.1	. . . . . 6 ⊢ (𝜑 → 𝑃 ∈ (ℙ ∖ {2}))
3	2	adantr 276	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑃 ∈ (ℙ ∖ {2}))
4		oddprm 12831	. . . . 5 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → ((𝑃 − 1) / 2) ∈ ℕ)
5	3, 4	syl 14	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → ((𝑃 − 1) / 2) ∈ ℕ)
6	5	nnzd 9600	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → ((𝑃 − 1) / 2) ∈ ℤ)
7		neg1cn 9247	. . . . . . . . . . . . 13 ⊢ -1 ∈ ℂ
8	7	a1i 9	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) ∧ (𝑅 / 2) ∈ ℤ) → -1 ∈ ℂ)
9		neg1ap0 9251	. . . . . . . . . . . . 13 ⊢ -1 # 0
10	9	a1i 9	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) ∧ (𝑅 / 2) ∈ ℤ) → -1 # 0)
11		2z 9506	. . . . . . . . . . . . 13 ⊢ 2 ∈ ℤ
12	11	a1i 9	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) ∧ (𝑅 / 2) ∈ ℤ) → 2 ∈ ℤ)
13		simpr 110	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) ∧ (𝑅 / 2) ∈ ℤ) → (𝑅 / 2) ∈ ℤ)
14		expmulzap 10846	. . . . . . . . . . . 12 ⊢ (((-1 ∈ ℂ ∧ -1 # 0) ∧ (2 ∈ ℤ ∧ (𝑅 / 2) ∈ ℤ)) → (-1↑(2 · (𝑅 / 2))) = ((-1↑2)↑(𝑅 / 2)))
15	8, 10, 12, 13, 14	syl22anc 1274	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) ∧ (𝑅 / 2) ∈ ℤ) → (-1↑(2 · (𝑅 / 2))) = ((-1↑2)↑(𝑅 / 2)))
16		lgseisen.4	. . . . . . . . . . . . . . . . . 18 ⊢ 𝑅 = ((𝑄 · (2 · 𝑥)) mod 𝑃)
17		lgseisen.2	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → 𝑄 ∈ (ℙ ∖ {2}))
18	17	adantr 276	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑄 ∈ (ℙ ∖ {2}))
19	18	eldifad 3211	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑄 ∈ ℙ)
20		prmz 12682	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑄 ∈ ℙ → 𝑄 ∈ ℤ)
21	19, 20	syl 14	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑄 ∈ ℤ)
22		elfzelz 10259	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑥 ∈ (1...((𝑃 − 1) / 2)) → 𝑥 ∈ ℤ)
23	22	adantl 277	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑥 ∈ ℤ)
24		zmulcl 9532	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((2 ∈ ℤ ∧ 𝑥 ∈ ℤ) → (2 · 𝑥) ∈ ℤ)
25	11, 23, 24	sylancr 414	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (2 · 𝑥) ∈ ℤ)
26	21, 25	zmulcld 9607	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (𝑄 · (2 · 𝑥)) ∈ ℤ)
27	3	eldifad 3211	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑃 ∈ ℙ)
28		prmnn 12681	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑃 ∈ ℙ → 𝑃 ∈ ℕ)
29	27, 28	syl 14	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑃 ∈ ℕ)
30		zmodfz 10607	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑄 · (2 · 𝑥)) ∈ ℤ ∧ 𝑃 ∈ ℕ) → ((𝑄 · (2 · 𝑥)) mod 𝑃) ∈ (0...(𝑃 − 1)))
31	26, 29, 30	syl2anc 411	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → ((𝑄 · (2 · 𝑥)) mod 𝑃) ∈ (0...(𝑃 − 1)))
32	16, 31	eqeltrid 2318	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑅 ∈ (0...(𝑃 − 1)))
33		elfznn0 10348	. . . . . . . . . . . . . . . . 17 ⊢ (𝑅 ∈ (0...(𝑃 − 1)) → 𝑅 ∈ ℕ₀)
34	32, 33	syl 14	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑅 ∈ ℕ₀)
35	34	nn0zd 9599	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑅 ∈ ℤ)
36	35	zcnd 9602	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑅 ∈ ℂ)
37	36	adantr 276	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) ∧ (𝑅 / 2) ∈ ℤ) → 𝑅 ∈ ℂ)
38		2cnd 9215	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) ∧ (𝑅 / 2) ∈ ℤ) → 2 ∈ ℂ)
39		2ap0 9235	. . . . . . . . . . . . . 14 ⊢ 2 # 0
40	39	a1i 9	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) ∧ (𝑅 / 2) ∈ ℤ) → 2 # 0)
41	37, 38, 40	divcanap2d 8971	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) ∧ (𝑅 / 2) ∈ ℤ) → (2 · (𝑅 / 2)) = 𝑅)
42	41	oveq2d 6033	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) ∧ (𝑅 / 2) ∈ ℤ) → (-1↑(2 · (𝑅 / 2))) = (-1↑𝑅))
43		neg1sqe1 10895	. . . . . . . . . . . . 13 ⊢ (-1↑2) = 1
44	43	oveq1i 6027	. . . . . . . . . . . 12 ⊢ ((-1↑2)↑(𝑅 / 2)) = (1↑(𝑅 / 2))
45		1exp 10829	. . . . . . . . . . . . 13 ⊢ ((𝑅 / 2) ∈ ℤ → (1↑(𝑅 / 2)) = 1)
46	45	adantl 277	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) ∧ (𝑅 / 2) ∈ ℤ) → (1↑(𝑅 / 2)) = 1)
47	44, 46	eqtrid 2276	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) ∧ (𝑅 / 2) ∈ ℤ) → ((-1↑2)↑(𝑅 / 2)) = 1)
48	15, 42, 47	3eqtr3d 2272	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) ∧ (𝑅 / 2) ∈ ℤ) → (-1↑𝑅) = 1)
49	48	oveq1d 6032	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) ∧ (𝑅 / 2) ∈ ℤ) → ((-1↑𝑅) · 𝑅) = (1 · 𝑅))
50	37	mullidd 8196	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) ∧ (𝑅 / 2) ∈ ℤ) → (1 · 𝑅) = 𝑅)
51	49, 50	eqtrd 2264	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) ∧ (𝑅 / 2) ∈ ℤ) → ((-1↑𝑅) · 𝑅) = 𝑅)
52	51	oveq1d 6032	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) ∧ (𝑅 / 2) ∈ ℤ) → (((-1↑𝑅) · 𝑅) mod 𝑃) = (𝑅 mod 𝑃))
53		zq 9859	. . . . . . . . . 10 ⊢ (𝑅 ∈ ℤ → 𝑅 ∈ ℚ)
54	35, 53	syl 14	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑅 ∈ ℚ)
55		nnq 9866	. . . . . . . . . 10 ⊢ (𝑃 ∈ ℕ → 𝑃 ∈ ℚ)
56	29, 55	syl 14	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑃 ∈ ℚ)
57	34	nn0ge0d 9457	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → 0 ≤ 𝑅)
58		zq 9859	. . . . . . . . . . . 12 ⊢ ((𝑄 · (2 · 𝑥)) ∈ ℤ → (𝑄 · (2 · 𝑥)) ∈ ℚ)
59	26, 58	syl 14	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (𝑄 · (2 · 𝑥)) ∈ ℚ)
60	29	nngt0d 9186	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → 0 < 𝑃)
61		modqlt 10594	. . . . . . . . . . 11 ⊢ (((𝑄 · (2 · 𝑥)) ∈ ℚ ∧ 𝑃 ∈ ℚ ∧ 0 < 𝑃) → ((𝑄 · (2 · 𝑥)) mod 𝑃) < 𝑃)
62	59, 56, 60, 61	syl3anc 1273	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → ((𝑄 · (2 · 𝑥)) mod 𝑃) < 𝑃)
63	16, 62	eqbrtrid 4123	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑅 < 𝑃)
64		modqid 10610	. . . . . . . . 9 ⊢ (((𝑅 ∈ ℚ ∧ 𝑃 ∈ ℚ) ∧ (0 ≤ 𝑅 ∧ 𝑅 < 𝑃)) → (𝑅 mod 𝑃) = 𝑅)
65	54, 56, 57, 63, 64	syl22anc 1274	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (𝑅 mod 𝑃) = 𝑅)
66	65	adantr 276	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) ∧ (𝑅 / 2) ∈ ℤ) → (𝑅 mod 𝑃) = 𝑅)
67	52, 66	eqtrd 2264	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) ∧ (𝑅 / 2) ∈ ℤ) → (((-1↑𝑅) · 𝑅) mod 𝑃) = 𝑅)
68	67	oveq1d 6032	. . . . 5 ⊢ (((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) ∧ (𝑅 / 2) ∈ ℤ) → ((((-1↑𝑅) · 𝑅) mod 𝑃) / 2) = (𝑅 / 2))
69	68, 13	eqeltrd 2308	. . . 4 ⊢ (((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) ∧ (𝑅 / 2) ∈ ℤ) → ((((-1↑𝑅) · 𝑅) mod 𝑃) / 2) ∈ ℤ)
70	29	nncnd 9156	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑃 ∈ ℂ)
71	70	mullidd 8196	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (1 · 𝑃) = 𝑃)
72	71	oveq2d 6033	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (-𝑅 + (1 · 𝑃)) = (-𝑅 + 𝑃))
73	34	nn0red 9455	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑅 ∈ ℝ)
74	73	renegcld 8558	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → -𝑅 ∈ ℝ)
75	74	recnd 8207	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → -𝑅 ∈ ℂ)
76	70, 75	addcomd 8329	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (𝑃 + -𝑅) = (-𝑅 + 𝑃))
77	70, 36	negsubd 8495	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (𝑃 + -𝑅) = (𝑃 − 𝑅))
78	72, 76, 77	3eqtr2d 2270	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (-𝑅 + (1 · 𝑃)) = (𝑃 − 𝑅))
79	78	oveq1d 6032	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → ((-𝑅 + (1 · 𝑃)) mod 𝑃) = ((𝑃 − 𝑅) mod 𝑃))
80		qnegcl 9869	. . . . . . . . . . . 12 ⊢ (𝑅 ∈ ℚ → -𝑅 ∈ ℚ)
81	54, 80	syl 14	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → -𝑅 ∈ ℚ)
82		modqcyc 10620	. . . . . . . . . . 11 ⊢ (((-𝑅 ∈ ℚ ∧ 1 ∈ ℤ) ∧ (𝑃 ∈ ℚ ∧ 0 < 𝑃)) → ((-𝑅 + (1 · 𝑃)) mod 𝑃) = (-𝑅 mod 𝑃))
83	81, 1, 56, 60, 82	syl22anc 1274	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → ((-𝑅 + (1 · 𝑃)) mod 𝑃) = (-𝑅 mod 𝑃))
84		qsubcl 9871	. . . . . . . . . . . 12 ⊢ ((𝑃 ∈ ℚ ∧ 𝑅 ∈ ℚ) → (𝑃 − 𝑅) ∈ ℚ)
85	56, 54, 84	syl2anc 411	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (𝑃 − 𝑅) ∈ ℚ)
86	29	nnred 9155	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑃 ∈ ℝ)
87	73, 86, 63	ltled 8297	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑅 ≤ 𝑃)
88	86, 73	subge0d 8714	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (0 ≤ (𝑃 − 𝑅) ↔ 𝑅 ≤ 𝑃))
89	87, 88	mpbird 167	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → 0 ≤ (𝑃 − 𝑅))
90		2nn 9304	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 2 ∈ ℕ
91		elfznn 10288	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑥 ∈ (1...((𝑃 − 1) / 2)) → 𝑥 ∈ ℕ)
92	91	adantl 277	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑥 ∈ ℕ)
93		nnmulcl 9163	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((2 ∈ ℕ ∧ 𝑥 ∈ ℕ) → (2 · 𝑥) ∈ ℕ)
94	90, 92, 93	sylancr 414	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (2 · 𝑥) ∈ ℕ)
95		elfzle2 10262	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑥 ∈ (1...((𝑃 − 1) / 2)) → 𝑥 ≤ ((𝑃 − 1) / 2))
96	95	adantl 277	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑥 ≤ ((𝑃 − 1) / 2))
97	92	nnred 9155	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑥 ∈ ℝ)
98		prmuz2 12702	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑃 ∈ ℙ → 𝑃 ∈ (ℤ_≥‘2))
99		uz2m1nn 9838	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑃 ∈ (ℤ_≥‘2) → (𝑃 − 1) ∈ ℕ)
100	27, 98, 99	3syl 17	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (𝑃 − 1) ∈ ℕ)
101	100	nnred 9155	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (𝑃 − 1) ∈ ℝ)
102		2re 9212	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ 2 ∈ ℝ
103	102	a1i 9	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → 2 ∈ ℝ)
104		2pos 9233	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ 0 < 2
105	104	a1i 9	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → 0 < 2)
106		lemuldiv2 9061	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑥 ∈ ℝ ∧ (𝑃 − 1) ∈ ℝ ∧ (2 ∈ ℝ ∧ 0 < 2)) → ((2 · 𝑥) ≤ (𝑃 − 1) ↔ 𝑥 ≤ ((𝑃 − 1) / 2)))
107	97, 101, 103, 105, 106	syl112anc 1277	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → ((2 · 𝑥) ≤ (𝑃 − 1) ↔ 𝑥 ≤ ((𝑃 − 1) / 2)))
108	96, 107	mpbird 167	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (2 · 𝑥) ≤ (𝑃 − 1))
109		prmz 12682	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑃 ∈ ℙ → 𝑃 ∈ ℤ)
110	27, 109	syl 14	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑃 ∈ ℤ)
111		peano2zm 9516	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑃 ∈ ℤ → (𝑃 − 1) ∈ ℤ)
112		fznn 10323	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑃 − 1) ∈ ℤ → ((2 · 𝑥) ∈ (1...(𝑃 − 1)) ↔ ((2 · 𝑥) ∈ ℕ ∧ (2 · 𝑥) ≤ (𝑃 − 1))))
113	110, 111, 112	3syl 17	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → ((2 · 𝑥) ∈ (1...(𝑃 − 1)) ↔ ((2 · 𝑥) ∈ ℕ ∧ (2 · 𝑥) ≤ (𝑃 − 1))))
114	94, 108, 113	mpbir2and 952	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (2 · 𝑥) ∈ (1...(𝑃 − 1)))
115		fzm1ndvds 12416	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑃 ∈ ℕ ∧ (2 · 𝑥) ∈ (1...(𝑃 − 1))) → ¬ 𝑃 ∥ (2 · 𝑥))
116	29, 114, 115	syl2anc 411	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → ¬ 𝑃 ∥ (2 · 𝑥))
117		lgseisen.3	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → 𝑃 ≠ 𝑄)
118	117	adantr 276	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑃 ≠ 𝑄)
119		prmrp 12716	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑃 ∈ ℙ ∧ 𝑄 ∈ ℙ) → ((𝑃 gcd 𝑄) = 1 ↔ 𝑃 ≠ 𝑄))
120	27, 19, 119	syl2anc 411	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → ((𝑃 gcd 𝑄) = 1 ↔ 𝑃 ≠ 𝑄))
121	118, 120	mpbird 167	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (𝑃 gcd 𝑄) = 1)
122		coprmdvds 12663	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑃 ∈ ℤ ∧ 𝑄 ∈ ℤ ∧ (2 · 𝑥) ∈ ℤ) → ((𝑃 ∥ (𝑄 · (2 · 𝑥)) ∧ (𝑃 gcd 𝑄) = 1) → 𝑃 ∥ (2 · 𝑥)))
123	110, 21, 25, 122	syl3anc 1273	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → ((𝑃 ∥ (𝑄 · (2 · 𝑥)) ∧ (𝑃 gcd 𝑄) = 1) → 𝑃 ∥ (2 · 𝑥)))
124	121, 123	mpan2d 428	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (𝑃 ∥ (𝑄 · (2 · 𝑥)) → 𝑃 ∥ (2 · 𝑥)))
125	116, 124	mtod 669	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → ¬ 𝑃 ∥ (𝑄 · (2 · 𝑥)))
126		dvdsval3 12351	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑃 ∈ ℕ ∧ (𝑄 · (2 · 𝑥)) ∈ ℤ) → (𝑃 ∥ (𝑄 · (2 · 𝑥)) ↔ ((𝑄 · (2 · 𝑥)) mod 𝑃) = 0))
127	29, 26, 126	syl2anc 411	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (𝑃 ∥ (𝑄 · (2 · 𝑥)) ↔ ((𝑄 · (2 · 𝑥)) mod 𝑃) = 0))
128	125, 127	mtbid 678	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → ¬ ((𝑄 · (2 · 𝑥)) mod 𝑃) = 0)
129	16	eqeq1i 2239	. . . . . . . . . . . . . . . . 17 ⊢ (𝑅 = 0 ↔ ((𝑄 · (2 · 𝑥)) mod 𝑃) = 0)
130	128, 129	sylnibr 683	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → ¬ 𝑅 = 0)
131	100	nnnn0d 9454	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (𝑃 − 1) ∈ ℕ₀)
132		nn0uz 9790	. . . . . . . . . . . . . . . . . . . 20 ⊢ ℕ₀ = (ℤ_≥‘0)
133	131, 132	eleqtrdi 2324	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (𝑃 − 1) ∈ (ℤ_≥‘0))
134		elfzp12 10333	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑃 − 1) ∈ (ℤ_≥‘0) → (𝑅 ∈ (0...(𝑃 − 1)) ↔ (𝑅 = 0 ∨ 𝑅 ∈ ((0 + 1)...(𝑃 − 1)))))
135	133, 134	syl 14	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (𝑅 ∈ (0...(𝑃 − 1)) ↔ (𝑅 = 0 ∨ 𝑅 ∈ ((0 + 1)...(𝑃 − 1)))))
136	32, 135	mpbid 147	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (𝑅 = 0 ∨ 𝑅 ∈ ((0 + 1)...(𝑃 − 1))))
137	136	ord 731	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (¬ 𝑅 = 0 → 𝑅 ∈ ((0 + 1)...(𝑃 − 1))))
138	130, 137	mpd 13	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑅 ∈ ((0 + 1)...(𝑃 − 1)))
139		1e0p1 9651	. . . . . . . . . . . . . . . 16 ⊢ 1 = (0 + 1)
140	139	oveq1i 6027	. . . . . . . . . . . . . . 15 ⊢ (1...(𝑃 − 1)) = ((0 + 1)...(𝑃 − 1))
141	138, 140	eleqtrrdi 2325	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑅 ∈ (1...(𝑃 − 1)))
142		elfznn 10288	. . . . . . . . . . . . . 14 ⊢ (𝑅 ∈ (1...(𝑃 − 1)) → 𝑅 ∈ ℕ)
143	141, 142	syl 14	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑅 ∈ ℕ)
144	143	nnrpd 9928	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑅 ∈ ℝ⁺)
145	86, 144	ltsubrpd 9963	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (𝑃 − 𝑅) < 𝑃)
146		modqid 10610	. . . . . . . . . . 11 ⊢ ((((𝑃 − 𝑅) ∈ ℚ ∧ 𝑃 ∈ ℚ) ∧ (0 ≤ (𝑃 − 𝑅) ∧ (𝑃 − 𝑅) < 𝑃)) → ((𝑃 − 𝑅) mod 𝑃) = (𝑃 − 𝑅))
147	85, 56, 89, 145, 146	syl22anc 1274	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → ((𝑃 − 𝑅) mod 𝑃) = (𝑃 − 𝑅))
148	79, 83, 147	3eqtr3d 2272	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (-𝑅 mod 𝑃) = (𝑃 − 𝑅))
149	148	adantr 276	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) ∧ ((𝑅 + 1) / 2) ∈ ℤ) → (-𝑅 mod 𝑃) = (𝑃 − 𝑅))
150		ax-1cn 8124	. . . . . . . . . . . . . 14 ⊢ 1 ∈ ℂ
151	150	a1i 9	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) ∧ ((𝑅 + 1) / 2) ∈ ℤ) → 1 ∈ ℂ)
152	143	adantr 276	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) ∧ ((𝑅 + 1) / 2) ∈ ℤ) → 𝑅 ∈ ℕ)
153		2ne0 9234	. . . . . . . . . . . . . . . 16 ⊢ 2 ≠ 0
154	35	peano2zd 9604	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (𝑅 + 1) ∈ ℤ)
155		dvdsval2 12350	. . . . . . . . . . . . . . . 16 ⊢ ((2 ∈ ℤ ∧ 2 ≠ 0 ∧ (𝑅 + 1) ∈ ℤ) → (2 ∥ (𝑅 + 1) ↔ ((𝑅 + 1) / 2) ∈ ℤ))
156	11, 153, 154, 155	mp3an12i 1377	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (2 ∥ (𝑅 + 1) ↔ ((𝑅 + 1) / 2) ∈ ℤ))
157	156	biimpar 297	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) ∧ ((𝑅 + 1) / 2) ∈ ℤ) → 2 ∥ (𝑅 + 1))
158	35	adantr 276	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) ∧ ((𝑅 + 1) / 2) ∈ ℤ) → 𝑅 ∈ ℤ)
159	90	a1i 9	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) ∧ ((𝑅 + 1) / 2) ∈ ℤ) → 2 ∈ ℕ)
160		1lt2 9312	. . . . . . . . . . . . . . . 16 ⊢ 1 < 2
161	160	a1i 9	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) ∧ ((𝑅 + 1) / 2) ∈ ℤ) → 1 < 2)
162		ndvdsp1 12492	. . . . . . . . . . . . . . 15 ⊢ ((𝑅 ∈ ℤ ∧ 2 ∈ ℕ ∧ 1 < 2) → (2 ∥ 𝑅 → ¬ 2 ∥ (𝑅 + 1)))
163	158, 159, 161, 162	syl3anc 1273	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) ∧ ((𝑅 + 1) / 2) ∈ ℤ) → (2 ∥ 𝑅 → ¬ 2 ∥ (𝑅 + 1)))
164	157, 163	mt2d 630	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) ∧ ((𝑅 + 1) / 2) ∈ ℤ) → ¬ 2 ∥ 𝑅)
165		oexpneg 12437	. . . . . . . . . . . . 13 ⊢ ((1 ∈ ℂ ∧ 𝑅 ∈ ℕ ∧ ¬ 2 ∥ 𝑅) → (-1↑𝑅) = -(1↑𝑅))
166	151, 152, 164, 165	syl3anc 1273	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) ∧ ((𝑅 + 1) / 2) ∈ ℤ) → (-1↑𝑅) = -(1↑𝑅))
167		1exp 10829	. . . . . . . . . . . . . 14 ⊢ (𝑅 ∈ ℤ → (1↑𝑅) = 1)
168	158, 167	syl 14	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) ∧ ((𝑅 + 1) / 2) ∈ ℤ) → (1↑𝑅) = 1)
169	168	negeqd 8373	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) ∧ ((𝑅 + 1) / 2) ∈ ℤ) → -(1↑𝑅) = -1)
170	166, 169	eqtrd 2264	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) ∧ ((𝑅 + 1) / 2) ∈ ℤ) → (-1↑𝑅) = -1)
171	170	oveq1d 6032	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) ∧ ((𝑅 + 1) / 2) ∈ ℤ) → ((-1↑𝑅) · 𝑅) = (-1 · 𝑅))
172	36	adantr 276	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) ∧ ((𝑅 + 1) / 2) ∈ ℤ) → 𝑅 ∈ ℂ)
173	172	mulm1d 8588	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) ∧ ((𝑅 + 1) / 2) ∈ ℤ) → (-1 · 𝑅) = -𝑅)
174	171, 173	eqtrd 2264	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) ∧ ((𝑅 + 1) / 2) ∈ ℤ) → ((-1↑𝑅) · 𝑅) = -𝑅)
175	174	oveq1d 6032	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) ∧ ((𝑅 + 1) / 2) ∈ ℤ) → (((-1↑𝑅) · 𝑅) mod 𝑃) = (-𝑅 mod 𝑃))
176	70	adantr 276	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) ∧ ((𝑅 + 1) / 2) ∈ ℤ) → 𝑃 ∈ ℂ)
177	176, 172, 151	pnpcan2d 8527	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) ∧ ((𝑅 + 1) / 2) ∈ ℤ) → ((𝑃 + 1) − (𝑅 + 1)) = (𝑃 − 𝑅))
178	149, 175, 177	3eqtr4d 2274	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) ∧ ((𝑅 + 1) / 2) ∈ ℤ) → (((-1↑𝑅) · 𝑅) mod 𝑃) = ((𝑃 + 1) − (𝑅 + 1)))
179	178	oveq1d 6032	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) ∧ ((𝑅 + 1) / 2) ∈ ℤ) → ((((-1↑𝑅) · 𝑅) mod 𝑃) / 2) = (((𝑃 + 1) − (𝑅 + 1)) / 2))
180		peano2cn 8313	. . . . . . . 8 ⊢ (𝑃 ∈ ℂ → (𝑃 + 1) ∈ ℂ)
181	176, 180	syl 14	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) ∧ ((𝑅 + 1) / 2) ∈ ℤ) → (𝑃 + 1) ∈ ℂ)
182		peano2cn 8313	. . . . . . . 8 ⊢ (𝑅 ∈ ℂ → (𝑅 + 1) ∈ ℂ)
183	172, 182	syl 14	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) ∧ ((𝑅 + 1) / 2) ∈ ℤ) → (𝑅 + 1) ∈ ℂ)
184		2cnd 9215	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) ∧ ((𝑅 + 1) / 2) ∈ ℤ) → 2 ∈ ℂ)
185	39	a1i 9	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) ∧ ((𝑅 + 1) / 2) ∈ ℤ) → 2 # 0)
186	181, 183, 184, 185	divsubdirapd 9009	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) ∧ ((𝑅 + 1) / 2) ∈ ℤ) → (((𝑃 + 1) − (𝑅 + 1)) / 2) = (((𝑃 + 1) / 2) − ((𝑅 + 1) / 2)))
187	179, 186	eqtrd 2264	. . . . 5 ⊢ (((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) ∧ ((𝑅 + 1) / 2) ∈ ℤ) → ((((-1↑𝑅) · 𝑅) mod 𝑃) / 2) = (((𝑃 + 1) / 2) − ((𝑅 + 1) / 2)))
188	176, 151, 184	subadd23d 8511	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) ∧ ((𝑅 + 1) / 2) ∈ ℤ) → ((𝑃 − 1) + 2) = (𝑃 + (2 − 1)))
189		2m1e1 9260	. . . . . . . . . . 11 ⊢ (2 − 1) = 1
190	189	oveq2i 6028	. . . . . . . . . 10 ⊢ (𝑃 + (2 − 1)) = (𝑃 + 1)
191	188, 190	eqtr2di 2281	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) ∧ ((𝑅 + 1) / 2) ∈ ℤ) → (𝑃 + 1) = ((𝑃 − 1) + 2))
192	191	oveq1d 6032	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) ∧ ((𝑅 + 1) / 2) ∈ ℤ) → ((𝑃 + 1) / 2) = (((𝑃 − 1) + 2) / 2))
193	100	nncnd 9156	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (𝑃 − 1) ∈ ℂ)
194	193	adantr 276	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) ∧ ((𝑅 + 1) / 2) ∈ ℤ) → (𝑃 − 1) ∈ ℂ)
195	194, 184, 184, 185	divdirapd 9008	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) ∧ ((𝑅 + 1) / 2) ∈ ℤ) → (((𝑃 − 1) + 2) / 2) = (((𝑃 − 1) / 2) + (2 / 2)))
196		2div2e1 9275	. . . . . . . . . 10 ⊢ (2 / 2) = 1
197	196	oveq2i 6028	. . . . . . . . 9 ⊢ (((𝑃 − 1) / 2) + (2 / 2)) = (((𝑃 − 1) / 2) + 1)
198	195, 197	eqtrdi 2280	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) ∧ ((𝑅 + 1) / 2) ∈ ℤ) → (((𝑃 − 1) + 2) / 2) = (((𝑃 − 1) / 2) + 1))
199	192, 198	eqtrd 2264	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) ∧ ((𝑅 + 1) / 2) ∈ ℤ) → ((𝑃 + 1) / 2) = (((𝑃 − 1) / 2) + 1))
200	6	adantr 276	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) ∧ ((𝑅 + 1) / 2) ∈ ℤ) → ((𝑃 − 1) / 2) ∈ ℤ)
201	200	peano2zd 9604	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) ∧ ((𝑅 + 1) / 2) ∈ ℤ) → (((𝑃 − 1) / 2) + 1) ∈ ℤ)
202	199, 201	eqeltrd 2308	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) ∧ ((𝑅 + 1) / 2) ∈ ℤ) → ((𝑃 + 1) / 2) ∈ ℤ)
203		simpr 110	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) ∧ ((𝑅 + 1) / 2) ∈ ℤ) → ((𝑅 + 1) / 2) ∈ ℤ)
204	202, 203	zsubcld 9606	. . . . 5 ⊢ (((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) ∧ ((𝑅 + 1) / 2) ∈ ℤ) → (((𝑃 + 1) / 2) − ((𝑅 + 1) / 2)) ∈ ℤ)
205	187, 204	eqeltrd 2308	. . . 4 ⊢ (((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) ∧ ((𝑅 + 1) / 2) ∈ ℤ) → ((((-1↑𝑅) · 𝑅) mod 𝑃) / 2) ∈ ℤ)
206		zeo 9584	. . . . 5 ⊢ (𝑅 ∈ ℤ → ((𝑅 / 2) ∈ ℤ ∨ ((𝑅 + 1) / 2) ∈ ℤ))
207	35, 206	syl 14	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → ((𝑅 / 2) ∈ ℤ ∨ ((𝑅 + 1) / 2) ∈ ℤ))
208	69, 205, 207	mpjaodan 805	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → ((((-1↑𝑅) · 𝑅) mod 𝑃) / 2) ∈ ℤ)
209		m1expcl 10823	. . . . . . . . . 10 ⊢ (𝑅 ∈ ℤ → (-1↑𝑅) ∈ ℤ)
210	35, 209	syl 14	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (-1↑𝑅) ∈ ℤ)
211	210, 35	zmulcld 9607	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → ((-1↑𝑅) · 𝑅) ∈ ℤ)
212	211, 29	zmodcld 10606	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (((-1↑𝑅) · 𝑅) mod 𝑃) ∈ ℕ₀)
213	212	nn0red 9455	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (((-1↑𝑅) · 𝑅) mod 𝑃) ∈ ℝ)
214		fzm1ndvds 12416	. . . . . . . . . . . 12 ⊢ ((𝑃 ∈ ℕ ∧ 𝑅 ∈ (1...(𝑃 − 1))) → ¬ 𝑃 ∥ 𝑅)
215	29, 141, 214	syl2anc 411	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → ¬ 𝑃 ∥ 𝑅)
216		1ap0 8769	. . . . . . . . . . . . . . . . . . . 20 ⊢ 1 # 0
217		divneg2ap 8915	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((1 ∈ ℂ ∧ 1 ∈ ℂ ∧ 1 # 0) → -(1 / 1) = (1 / -1))
218	150, 150, 216, 217	mp3an 1373	. . . . . . . . . . . . . . . . . . 19 ⊢ -(1 / 1) = (1 / -1)
219		1div1e1 8883	. . . . . . . . . . . . . . . . . . . 20 ⊢ (1 / 1) = 1
220	219	negeqi 8372	. . . . . . . . . . . . . . . . . . 19 ⊢ -(1 / 1) = -1
221	218, 220	eqtr3i 2254	. . . . . . . . . . . . . . . . . 18 ⊢ (1 / -1) = -1
222	221	oveq1i 6027	. . . . . . . . . . . . . . . . 17 ⊢ ((1 / -1)↑𝑅) = (-1↑𝑅)
223	7	a1i 9	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → -1 ∈ ℂ)
224	9	a1i 9	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → -1 # 0)
225	223, 224, 35	exprecapd 10942	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → ((1 / -1)↑𝑅) = (1 / (-1↑𝑅)))
226	222, 225	eqtr3id 2278	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (-1↑𝑅) = (1 / (-1↑𝑅)))
227	226	oveq2d 6033	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → ((-1↑𝑅) · (-1↑𝑅)) = ((-1↑𝑅) · (1 / (-1↑𝑅))))
228	210	zcnd 9602	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (-1↑𝑅) ∈ ℂ)
229	223, 224, 35	expap0d 10940	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (-1↑𝑅) # 0)
230	228, 229	recidapd 8962	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → ((-1↑𝑅) · (1 / (-1↑𝑅))) = 1)
231	227, 230	eqtrd 2264	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → ((-1↑𝑅) · (-1↑𝑅)) = 1)
232	231	oveq1d 6032	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (((-1↑𝑅) · (-1↑𝑅)) · 𝑅) = (1 · 𝑅))
233	228, 228, 36	mulassd 8202	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (((-1↑𝑅) · (-1↑𝑅)) · 𝑅) = ((-1↑𝑅) · ((-1↑𝑅) · 𝑅)))
234	36	mullidd 8196	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (1 · 𝑅) = 𝑅)
235	232, 233, 234	3eqtr3d 2272	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → ((-1↑𝑅) · ((-1↑𝑅) · 𝑅)) = 𝑅)
236	235	breq2d 4100	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (𝑃 ∥ ((-1↑𝑅) · ((-1↑𝑅) · 𝑅)) ↔ 𝑃 ∥ 𝑅))
237	215, 236	mtbird 679	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → ¬ 𝑃 ∥ ((-1↑𝑅) · ((-1↑𝑅) · 𝑅)))
238		dvdsmultr2 12393	. . . . . . . . . . 11 ⊢ ((𝑃 ∈ ℤ ∧ (-1↑𝑅) ∈ ℤ ∧ ((-1↑𝑅) · 𝑅) ∈ ℤ) → (𝑃 ∥ ((-1↑𝑅) · 𝑅) → 𝑃 ∥ ((-1↑𝑅) · ((-1↑𝑅) · 𝑅))))
239	110, 210, 211, 238	syl3anc 1273	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (𝑃 ∥ ((-1↑𝑅) · 𝑅) → 𝑃 ∥ ((-1↑𝑅) · ((-1↑𝑅) · 𝑅))))
240	237, 239	mtod 669	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → ¬ 𝑃 ∥ ((-1↑𝑅) · 𝑅))
241		dvdsval3 12351	. . . . . . . . . 10 ⊢ ((𝑃 ∈ ℕ ∧ ((-1↑𝑅) · 𝑅) ∈ ℤ) → (𝑃 ∥ ((-1↑𝑅) · 𝑅) ↔ (((-1↑𝑅) · 𝑅) mod 𝑃) = 0))
242	29, 211, 241	syl2anc 411	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (𝑃 ∥ ((-1↑𝑅) · 𝑅) ↔ (((-1↑𝑅) · 𝑅) mod 𝑃) = 0))
243	240, 242	mtbid 678	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → ¬ (((-1↑𝑅) · 𝑅) mod 𝑃) = 0)
244		elnn0 9403	. . . . . . . . 9 ⊢ ((((-1↑𝑅) · 𝑅) mod 𝑃) ∈ ℕ₀ ↔ ((((-1↑𝑅) · 𝑅) mod 𝑃) ∈ ℕ ∨ (((-1↑𝑅) · 𝑅) mod 𝑃) = 0))
245	212, 244	sylib 122	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → ((((-1↑𝑅) · 𝑅) mod 𝑃) ∈ ℕ ∨ (((-1↑𝑅) · 𝑅) mod 𝑃) = 0))
246	243, 245	ecased 1385	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (((-1↑𝑅) · 𝑅) mod 𝑃) ∈ ℕ)
247	246	nngt0d 9186	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → 0 < (((-1↑𝑅) · 𝑅) mod 𝑃))
248	213, 103, 247, 105	divgt0d 9114	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → 0 < ((((-1↑𝑅) · 𝑅) mod 𝑃) / 2))
249		elnnz 9488	. . . . 5 ⊢ (((((-1↑𝑅) · 𝑅) mod 𝑃) / 2) ∈ ℕ ↔ (((((-1↑𝑅) · 𝑅) mod 𝑃) / 2) ∈ ℤ ∧ 0 < ((((-1↑𝑅) · 𝑅) mod 𝑃) / 2)))
250	208, 248, 249	sylanbrc 417	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → ((((-1↑𝑅) · 𝑅) mod 𝑃) / 2) ∈ ℕ)
251	250	nnge1d 9185	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → 1 ≤ ((((-1↑𝑅) · 𝑅) mod 𝑃) / 2))
252		zmodfz 10607	. . . . . 6 ⊢ ((((-1↑𝑅) · 𝑅) ∈ ℤ ∧ 𝑃 ∈ ℕ) → (((-1↑𝑅) · 𝑅) mod 𝑃) ∈ (0...(𝑃 − 1)))
253	211, 29, 252	syl2anc 411	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (((-1↑𝑅) · 𝑅) mod 𝑃) ∈ (0...(𝑃 − 1)))
254		elfzle2 10262	. . . . 5 ⊢ ((((-1↑𝑅) · 𝑅) mod 𝑃) ∈ (0...(𝑃 − 1)) → (((-1↑𝑅) · 𝑅) mod 𝑃) ≤ (𝑃 − 1))
255	253, 254	syl 14	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (((-1↑𝑅) · 𝑅) mod 𝑃) ≤ (𝑃 − 1))
256		lediv1 9048	. . . . 5 ⊢ (((((-1↑𝑅) · 𝑅) mod 𝑃) ∈ ℝ ∧ (𝑃 − 1) ∈ ℝ ∧ (2 ∈ ℝ ∧ 0 < 2)) → ((((-1↑𝑅) · 𝑅) mod 𝑃) ≤ (𝑃 − 1) ↔ ((((-1↑𝑅) · 𝑅) mod 𝑃) / 2) ≤ ((𝑃 − 1) / 2)))
257	213, 101, 103, 105, 256	syl112anc 1277	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → ((((-1↑𝑅) · 𝑅) mod 𝑃) ≤ (𝑃 − 1) ↔ ((((-1↑𝑅) · 𝑅) mod 𝑃) / 2) ≤ ((𝑃 − 1) / 2)))
258	255, 257	mpbid 147	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → ((((-1↑𝑅) · 𝑅) mod 𝑃) / 2) ≤ ((𝑃 − 1) / 2))
259	1, 6, 208, 251, 258	elfzd 10250	. 2 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → ((((-1↑𝑅) · 𝑅) mod 𝑃) / 2) ∈ (1...((𝑃 − 1) / 2)))
260		lgseisen.5	. 2 ⊢ 𝑀 = (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ ((((-1↑𝑅) · 𝑅) mod 𝑃) / 2))
261	259, 260	fmptd 5801	1 ⊢ (𝜑 → 𝑀:(1...((𝑃 − 1) / 2))⟶(1...((𝑃 − 1) / 2)))

Colors of variables: wff set class

Syntax hints: ¬ wn 3 → wi 4 ∧ wa 104 ↔ wb 105 ∨ wo 715 = wceq 1397 ∈ wcel 2202 ≠ wne 2402 ∖ cdif 3197 {csn 3669 class class class wbr 4088 ↦ cmpt 4150 ⟶wf 5322 ‘cfv 5326 (class class class)co 6017 ℂcc 8029 ℝcr 8030 0cc0 8031 1c1 8032 + caddc 8034 · cmul 8036 < clt 8213 ≤ cle 8214 − cmin 8349 -cneg 8350 # cap 8760 / cdiv 8851 ℕcn 9142 2c2 9193 ℕ₀cn0 9401 ℤcz 9478 ℤ_≥cuz 9754 ℚcq 9852 ...cfz 10242 mod cmo 10583 ↑cexp 10799 ∥ cdvds 12347 gcd cgcd 12523 ℙcprime 12678

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-in1 619 ax-in2 620 ax-io 716 ax-5 1495 ax-7 1496 ax-gen 1497 ax-ie1 1541 ax-ie2 1542 ax-8 1552 ax-10 1553 ax-11 1554 ax-i12 1555 ax-bndl 1557 ax-4 1558 ax-17 1574 ax-i9 1578 ax-ial 1582 ax-i5r 1583 ax-13 2204 ax-14 2205 ax-ext 2213 ax-coll 4204 ax-sep 4207 ax-nul 4215 ax-pow 4264 ax-pr 4299 ax-un 4530 ax-setind 4635 ax-iinf 4686 ax-cnex 8122 ax-resscn 8123 ax-1cn 8124 ax-1re 8125 ax-icn 8126 ax-addcl 8127 ax-addrcl 8128 ax-mulcl 8129 ax-mulrcl 8130 ax-addcom 8131 ax-mulcom 8132 ax-addass 8133 ax-mulass 8134 ax-distr 8135 ax-i2m1 8136 ax-0lt1 8137 ax-1rid 8138 ax-0id 8139 ax-rnegex 8140 ax-precex 8141 ax-cnre 8142 ax-pre-ltirr 8143 ax-pre-ltwlin 8144 ax-pre-lttrn 8145 ax-pre-apti 8146 ax-pre-ltadd 8147 ax-pre-mulgt0 8148 ax-pre-mulext 8149 ax-arch 8150 ax-caucvg 8151

This theorem depends on definitions: df-bi 117 df-dc 842 df-3or 1005 df-3an 1006 df-tru 1400 df-fal 1403 df-xor 1420 df-nf 1509 df-sb 1811 df-eu 2082 df-mo 2083 df-clab 2218 df-cleq 2224 df-clel 2227 df-nfc 2363 df-ne 2403 df-nel 2498 df-ral 2515 df-rex 2516 df-reu 2517 df-rmo 2518 df-rab 2519 df-v 2804 df-sbc 3032 df-csb 3128 df-dif 3202 df-un 3204 df-in 3206 df-ss 3213 df-nul 3495 df-if 3606 df-pw 3654 df-sn 3675 df-pr 3676 df-op 3678 df-uni 3894 df-int 3929 df-iun 3972 df-br 4089 df-opab 4151 df-mpt 4152 df-tr 4188 df-id 4390 df-po 4393 df-iso 4394 df-iord 4463 df-on 4465 df-ilim 4466 df-suc 4468 df-iom 4689 df-xp 4731 df-rel 4732 df-cnv 4733 df-co 4734 df-dm 4735 df-rn 4736 df-res 4737 df-ima 4738 df-iota 5286 df-fun 5328 df-fn 5329 df-f 5330 df-f1 5331 df-fo 5332 df-f1o 5333 df-fv 5334 df-riota 5970 df-ov 6020 df-oprab 6021 df-mpo 6022 df-1st 6302 df-2nd 6303 df-recs 6470 df-frec 6556 df-1o 6581 df-2o 6582 df-er 6701 df-en 6909 df-sup 7182 df-pnf 8215 df-mnf 8216 df-xr 8217 df-ltxr 8218 df-le 8219 df-sub 8351 df-neg 8352 df-reap 8754 df-ap 8761 df-div 8852 df-inn 9143 df-2 9201 df-3 9202 df-4 9203 df-n0 9402 df-z 9479 df-uz 9755 df-q 9853 df-rp 9888 df-fz 10243 df-fzo 10377 df-fl 10529 df-mod 10584 df-seqfrec 10709 df-exp 10800 df-cj 11402 df-re 11403 df-im 11404 df-rsqrt 11558 df-abs 11559 df-dvds 12348 df-gcd 12524 df-prm 12679

This theorem is referenced by: lgseisenlem2 15799 lgseisenlem3 15800

W3C validator