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

Theorem lgseisenlem1 26280
Description: Lemma for lgseisen 26284. 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
StepHypRef Expression
1 1zzd 12232 . . 3 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → 1 ∈ ℤ)
2 lgseisen.1 . . . . . 6 (𝜑𝑃 ∈ (ℙ ∖ {2}))
32adantr 484 . . . . 5 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑃 ∈ (ℙ ∖ {2}))
4 oddprm 16387 . . . . 5 (𝑃 ∈ (ℙ ∖ {2}) → ((𝑃 − 1) / 2) ∈ ℕ)
53, 4syl 17 . . . 4 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → ((𝑃 − 1) / 2) ∈ ℕ)
65nnzd 12305 . . 3 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → ((𝑃 − 1) / 2) ∈ ℤ)
7 neg1cn 11968 . . . . . . . . . . . . 13 -1 ∈ ℂ
87a1i 11 . . . . . . . . . . . 12 (((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) ∧ (𝑅 / 2) ∈ ℤ) → -1 ∈ ℂ)
9 neg1ne0 11970 . . . . . . . . . . . . 13 -1 ≠ 0
109a1i 11 . . . . . . . . . . . 12 (((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) ∧ (𝑅 / 2) ∈ ℤ) → -1 ≠ 0)
11 2z 12233 . . . . . . . . . . . . 13 2 ∈ ℤ
1211a1i 11 . . . . . . . . . . . 12 (((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) ∧ (𝑅 / 2) ∈ ℤ) → 2 ∈ ℤ)
13 simpr 488 . . . . . . . . . . . 12 (((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) ∧ (𝑅 / 2) ∈ ℤ) → (𝑅 / 2) ∈ ℤ)
14 expmulz 13705 . . . . . . . . . . . 12 (((-1 ∈ ℂ ∧ -1 ≠ 0) ∧ (2 ∈ ℤ ∧ (𝑅 / 2) ∈ ℤ)) → (-1↑(2 · (𝑅 / 2))) = ((-1↑2)↑(𝑅 / 2)))
158, 10, 12, 13, 14syl22anc 839 . . . . . . . . . . 11 (((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) ∧ (𝑅 / 2) ∈ ℤ) → (-1↑(2 · (𝑅 / 2))) = ((-1↑2)↑(𝑅 / 2)))
16 lgseisen.4 . . . . . . . . . . . . . . . . . 18 𝑅 = ((𝑄 · (2 · 𝑥)) mod 𝑃)
17 lgseisen.2 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑𝑄 ∈ (ℙ ∖ {2}))
1817adantr 484 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑄 ∈ (ℙ ∖ {2}))
1918eldifad 3892 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑄 ∈ ℙ)
20 prmz 16256 . . . . . . . . . . . . . . . . . . . . 21 (𝑄 ∈ ℙ → 𝑄 ∈ ℤ)
2119, 20syl 17 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑄 ∈ ℤ)
22 elfzelz 13136 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 ∈ (1...((𝑃 − 1) / 2)) → 𝑥 ∈ ℤ)
2322adantl 485 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑥 ∈ ℤ)
24 zmulcl 12250 . . . . . . . . . . . . . . . . . . . . 21 ((2 ∈ ℤ ∧ 𝑥 ∈ ℤ) → (2 · 𝑥) ∈ ℤ)
2511, 23, 24sylancr 590 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → (2 · 𝑥) ∈ ℤ)
2621, 25zmulcld 12312 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → (𝑄 · (2 · 𝑥)) ∈ ℤ)
273eldifad 3892 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑃 ∈ ℙ)
28 prmnn 16255 . . . . . . . . . . . . . . . . . . . 20 (𝑃 ∈ ℙ → 𝑃 ∈ ℕ)
2927, 28syl 17 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑃 ∈ ℕ)
30 zmodfz 13490 . . . . . . . . . . . . . . . . . . 19 (((𝑄 · (2 · 𝑥)) ∈ ℤ ∧ 𝑃 ∈ ℕ) → ((𝑄 · (2 · 𝑥)) mod 𝑃) ∈ (0...(𝑃 − 1)))
3126, 29, 30syl2anc 587 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → ((𝑄 · (2 · 𝑥)) mod 𝑃) ∈ (0...(𝑃 − 1)))
3216, 31eqeltrid 2843 . . . . . . . . . . . . . . . . 17 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑅 ∈ (0...(𝑃 − 1)))
33 elfznn0 13229 . . . . . . . . . . . . . . . . 17 (𝑅 ∈ (0...(𝑃 − 1)) → 𝑅 ∈ ℕ0)
3432, 33syl 17 . . . . . . . . . . . . . . . 16 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑅 ∈ ℕ0)
3534nn0zd 12304 . . . . . . . . . . . . . . 15 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑅 ∈ ℤ)
3635zcnd 12307 . . . . . . . . . . . . . 14 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑅 ∈ ℂ)
3736adantr 484 . . . . . . . . . . . . 13 (((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) ∧ (𝑅 / 2) ∈ ℤ) → 𝑅 ∈ ℂ)
38 2cnd 11932 . . . . . . . . . . . . 13 (((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) ∧ (𝑅 / 2) ∈ ℤ) → 2 ∈ ℂ)
39 2ne0 11958 . . . . . . . . . . . . . 14 2 ≠ 0
4039a1i 11 . . . . . . . . . . . . 13 (((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) ∧ (𝑅 / 2) ∈ ℤ) → 2 ≠ 0)
4137, 38, 40divcan2d 11634 . . . . . . . . . . . 12 (((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) ∧ (𝑅 / 2) ∈ ℤ) → (2 · (𝑅 / 2)) = 𝑅)
4241oveq2d 7247 . . . . . . . . . . 11 (((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) ∧ (𝑅 / 2) ∈ ℤ) → (-1↑(2 · (𝑅 / 2))) = (-1↑𝑅))
43 neg1sqe1 13789 . . . . . . . . . . . . 13 (-1↑2) = 1
4443oveq1i 7241 . . . . . . . . . . . 12 ((-1↑2)↑(𝑅 / 2)) = (1↑(𝑅 / 2))
45 1exp 13688 . . . . . . . . . . . . 13 ((𝑅 / 2) ∈ ℤ → (1↑(𝑅 / 2)) = 1)
4645adantl 485 . . . . . . . . . . . 12 (((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) ∧ (𝑅 / 2) ∈ ℤ) → (1↑(𝑅 / 2)) = 1)
4744, 46syl5eq 2791 . . . . . . . . . . 11 (((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) ∧ (𝑅 / 2) ∈ ℤ) → ((-1↑2)↑(𝑅 / 2)) = 1)
4815, 42, 473eqtr3d 2786 . . . . . . . . . 10 (((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) ∧ (𝑅 / 2) ∈ ℤ) → (-1↑𝑅) = 1)
4948oveq1d 7246 . . . . . . . . 9 (((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) ∧ (𝑅 / 2) ∈ ℤ) → ((-1↑𝑅) · 𝑅) = (1 · 𝑅))
5037mulid2d 10875 . . . . . . . . 9 (((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) ∧ (𝑅 / 2) ∈ ℤ) → (1 · 𝑅) = 𝑅)
5149, 50eqtrd 2778 . . . . . . . 8 (((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) ∧ (𝑅 / 2) ∈ ℤ) → ((-1↑𝑅) · 𝑅) = 𝑅)
5251oveq1d 7246 . . . . . . 7 (((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) ∧ (𝑅 / 2) ∈ ℤ) → (((-1↑𝑅) · 𝑅) mod 𝑃) = (𝑅 mod 𝑃))
5334nn0red 12175 . . . . . . . . 9 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑅 ∈ ℝ)
5429nnrpd 12650 . . . . . . . . 9 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑃 ∈ ℝ+)
5534nn0ge0d 12177 . . . . . . . . 9 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → 0 ≤ 𝑅)
5626zred 12306 . . . . . . . . . . 11 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → (𝑄 · (2 · 𝑥)) ∈ ℝ)
57 modlt 13477 . . . . . . . . . . 11 (((𝑄 · (2 · 𝑥)) ∈ ℝ ∧ 𝑃 ∈ ℝ+) → ((𝑄 · (2 · 𝑥)) mod 𝑃) < 𝑃)
5856, 54, 57syl2anc 587 . . . . . . . . . 10 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → ((𝑄 · (2 · 𝑥)) mod 𝑃) < 𝑃)
5916, 58eqbrtrid 5102 . . . . . . . . 9 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑅 < 𝑃)
60 modid 13493 . . . . . . . . 9 (((𝑅 ∈ ℝ ∧ 𝑃 ∈ ℝ+) ∧ (0 ≤ 𝑅𝑅 < 𝑃)) → (𝑅 mod 𝑃) = 𝑅)
6153, 54, 55, 59, 60syl22anc 839 . . . . . . . 8 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → (𝑅 mod 𝑃) = 𝑅)
6261adantr 484 . . . . . . 7 (((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) ∧ (𝑅 / 2) ∈ ℤ) → (𝑅 mod 𝑃) = 𝑅)
6352, 62eqtrd 2778 . . . . . 6 (((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) ∧ (𝑅 / 2) ∈ ℤ) → (((-1↑𝑅) · 𝑅) mod 𝑃) = 𝑅)
6463oveq1d 7246 . . . . 5 (((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) ∧ (𝑅 / 2) ∈ ℤ) → ((((-1↑𝑅) · 𝑅) mod 𝑃) / 2) = (𝑅 / 2))
6564, 13eqeltrd 2839 . . . 4 (((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) ∧ (𝑅 / 2) ∈ ℤ) → ((((-1↑𝑅) · 𝑅) mod 𝑃) / 2) ∈ ℤ)
6629nncnd 11870 . . . . . . . . . . . . . 14 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑃 ∈ ℂ)
6766mulid2d 10875 . . . . . . . . . . . . 13 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → (1 · 𝑃) = 𝑃)
6867oveq2d 7247 . . . . . . . . . . . 12 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → (-𝑅 + (1 · 𝑃)) = (-𝑅 + 𝑃))
6953renegcld 11283 . . . . . . . . . . . . . 14 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → -𝑅 ∈ ℝ)
7069recnd 10885 . . . . . . . . . . . . 13 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → -𝑅 ∈ ℂ)
7166, 70addcomd 11058 . . . . . . . . . . . 12 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → (𝑃 + -𝑅) = (-𝑅 + 𝑃))
7266, 36negsubd 11219 . . . . . . . . . . . 12 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → (𝑃 + -𝑅) = (𝑃𝑅))
7368, 71, 723eqtr2d 2784 . . . . . . . . . . 11 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → (-𝑅 + (1 · 𝑃)) = (𝑃𝑅))
7473oveq1d 7246 . . . . . . . . . 10 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → ((-𝑅 + (1 · 𝑃)) mod 𝑃) = ((𝑃𝑅) mod 𝑃))
75 modcyc 13503 . . . . . . . . . . 11 ((-𝑅 ∈ ℝ ∧ 𝑃 ∈ ℝ+ ∧ 1 ∈ ℤ) → ((-𝑅 + (1 · 𝑃)) mod 𝑃) = (-𝑅 mod 𝑃))
7669, 54, 1, 75syl3anc 1373 . . . . . . . . . 10 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → ((-𝑅 + (1 · 𝑃)) mod 𝑃) = (-𝑅 mod 𝑃))
7729nnred 11869 . . . . . . . . . . . 12 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑃 ∈ ℝ)
7877, 53resubcld 11284 . . . . . . . . . . 11 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → (𝑃𝑅) ∈ ℝ)
7953, 77, 59ltled 11004 . . . . . . . . . . . 12 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑅𝑃)
8077, 53subge0d 11446 . . . . . . . . . . . 12 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → (0 ≤ (𝑃𝑅) ↔ 𝑅𝑃))
8179, 80mpbird 260 . . . . . . . . . . 11 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → 0 ≤ (𝑃𝑅))
82 2nn 11927 . . . . . . . . . . . . . . . . . . . . . 22 2 ∈ ℕ
83 elfznn 13165 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥 ∈ (1...((𝑃 − 1) / 2)) → 𝑥 ∈ ℕ)
8483adantl 485 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑥 ∈ ℕ)
85 nnmulcl 11878 . . . . . . . . . . . . . . . . . . . . . 22 ((2 ∈ ℕ ∧ 𝑥 ∈ ℕ) → (2 · 𝑥) ∈ ℕ)
8682, 84, 85sylancr 590 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → (2 · 𝑥) ∈ ℕ)
87 elfzle2 13140 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥 ∈ (1...((𝑃 − 1) / 2)) → 𝑥 ≤ ((𝑃 − 1) / 2))
8887adantl 485 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑥 ≤ ((𝑃 − 1) / 2))
8984nnred 11869 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑥 ∈ ℝ)
90 prmuz2 16277 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑃 ∈ ℙ → 𝑃 ∈ (ℤ‘2))
91 uz2m1nn 12543 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑃 ∈ (ℤ‘2) → (𝑃 − 1) ∈ ℕ)
9227, 90, 913syl 18 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → (𝑃 − 1) ∈ ℕ)
9392nnred 11869 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → (𝑃 − 1) ∈ ℝ)
94 2re 11928 . . . . . . . . . . . . . . . . . . . . . . . 24 2 ∈ ℝ
9594a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → 2 ∈ ℝ)
96 2pos 11957 . . . . . . . . . . . . . . . . . . . . . . . 24 0 < 2
9796a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → 0 < 2)
98 lemuldiv2 11737 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑥 ∈ ℝ ∧ (𝑃 − 1) ∈ ℝ ∧ (2 ∈ ℝ ∧ 0 < 2)) → ((2 · 𝑥) ≤ (𝑃 − 1) ↔ 𝑥 ≤ ((𝑃 − 1) / 2)))
9989, 93, 95, 97, 98syl112anc 1376 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → ((2 · 𝑥) ≤ (𝑃 − 1) ↔ 𝑥 ≤ ((𝑃 − 1) / 2)))
10088, 99mpbird 260 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → (2 · 𝑥) ≤ (𝑃 − 1))
101 prmz 16256 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑃 ∈ ℙ → 𝑃 ∈ ℤ)
10227, 101syl 17 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑃 ∈ ℤ)
103 peano2zm 12244 . . . . . . . . . . . . . . . . . . . . . 22 (𝑃 ∈ ℤ → (𝑃 − 1) ∈ ℤ)
104 fznn 13204 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑃 − 1) ∈ ℤ → ((2 · 𝑥) ∈ (1...(𝑃 − 1)) ↔ ((2 · 𝑥) ∈ ℕ ∧ (2 · 𝑥) ≤ (𝑃 − 1))))
105102, 103, 1043syl 18 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → ((2 · 𝑥) ∈ (1...(𝑃 − 1)) ↔ ((2 · 𝑥) ∈ ℕ ∧ (2 · 𝑥) ≤ (𝑃 − 1))))
10686, 100, 105mpbir2and 713 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → (2 · 𝑥) ∈ (1...(𝑃 − 1)))
107 fzm1ndvds 15907 . . . . . . . . . . . . . . . . . . . 20 ((𝑃 ∈ ℕ ∧ (2 · 𝑥) ∈ (1...(𝑃 − 1))) → ¬ 𝑃 ∥ (2 · 𝑥))
10829, 106, 107syl2anc 587 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → ¬ 𝑃 ∥ (2 · 𝑥))
109 lgseisen.3 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑𝑃𝑄)
110109adantr 484 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑃𝑄)
111 prmrp 16293 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑃 ∈ ℙ ∧ 𝑄 ∈ ℙ) → ((𝑃 gcd 𝑄) = 1 ↔ 𝑃𝑄))
11227, 19, 111syl2anc 587 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → ((𝑃 gcd 𝑄) = 1 ↔ 𝑃𝑄))
113110, 112mpbird 260 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → (𝑃 gcd 𝑄) = 1)
114 coprmdvds 16234 . . . . . . . . . . . . . . . . . . . . 21 ((𝑃 ∈ ℤ ∧ 𝑄 ∈ ℤ ∧ (2 · 𝑥) ∈ ℤ) → ((𝑃 ∥ (𝑄 · (2 · 𝑥)) ∧ (𝑃 gcd 𝑄) = 1) → 𝑃 ∥ (2 · 𝑥)))
115102, 21, 25, 114syl3anc 1373 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → ((𝑃 ∥ (𝑄 · (2 · 𝑥)) ∧ (𝑃 gcd 𝑄) = 1) → 𝑃 ∥ (2 · 𝑥)))
116113, 115mpan2d 694 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → (𝑃 ∥ (𝑄 · (2 · 𝑥)) → 𝑃 ∥ (2 · 𝑥)))
117108, 116mtod 201 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → ¬ 𝑃 ∥ (𝑄 · (2 · 𝑥)))
118 dvdsval3 15843 . . . . . . . . . . . . . . . . . . 19 ((𝑃 ∈ ℕ ∧ (𝑄 · (2 · 𝑥)) ∈ ℤ) → (𝑃 ∥ (𝑄 · (2 · 𝑥)) ↔ ((𝑄 · (2 · 𝑥)) mod 𝑃) = 0))
11929, 26, 118syl2anc 587 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → (𝑃 ∥ (𝑄 · (2 · 𝑥)) ↔ ((𝑄 · (2 · 𝑥)) mod 𝑃) = 0))
120117, 119mtbid 327 . . . . . . . . . . . . . . . . 17 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → ¬ ((𝑄 · (2 · 𝑥)) mod 𝑃) = 0)
12116eqeq1i 2743 . . . . . . . . . . . . . . . . 17 (𝑅 = 0 ↔ ((𝑄 · (2 · 𝑥)) mod 𝑃) = 0)
122120, 121sylnibr 332 . . . . . . . . . . . . . . . 16 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → ¬ 𝑅 = 0)
12392nnnn0d 12174 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → (𝑃 − 1) ∈ ℕ0)
124 nn0uz 12500 . . . . . . . . . . . . . . . . . . . 20 0 = (ℤ‘0)
125123, 124eleqtrdi 2849 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → (𝑃 − 1) ∈ (ℤ‘0))
126 elfzp12 13215 . . . . . . . . . . . . . . . . . . 19 ((𝑃 − 1) ∈ (ℤ‘0) → (𝑅 ∈ (0...(𝑃 − 1)) ↔ (𝑅 = 0 ∨ 𝑅 ∈ ((0 + 1)...(𝑃 − 1)))))
127125, 126syl 17 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → (𝑅 ∈ (0...(𝑃 − 1)) ↔ (𝑅 = 0 ∨ 𝑅 ∈ ((0 + 1)...(𝑃 − 1)))))
12832, 127mpbid 235 . . . . . . . . . . . . . . . . 17 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → (𝑅 = 0 ∨ 𝑅 ∈ ((0 + 1)...(𝑃 − 1))))
129128ord 864 . . . . . . . . . . . . . . . 16 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → (¬ 𝑅 = 0 → 𝑅 ∈ ((0 + 1)...(𝑃 − 1))))
130122, 129mpd 15 . . . . . . . . . . . . . . 15 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑅 ∈ ((0 + 1)...(𝑃 − 1)))
131 1e0p1 12359 . . . . . . . . . . . . . . . 16 1 = (0 + 1)
132131oveq1i 7241 . . . . . . . . . . . . . . 15 (1...(𝑃 − 1)) = ((0 + 1)...(𝑃 − 1))
133130, 132eleqtrrdi 2850 . . . . . . . . . . . . . 14 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑅 ∈ (1...(𝑃 − 1)))
134 elfznn 13165 . . . . . . . . . . . . . 14 (𝑅 ∈ (1...(𝑃 − 1)) → 𝑅 ∈ ℕ)
135133, 134syl 17 . . . . . . . . . . . . 13 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑅 ∈ ℕ)
136135nnrpd 12650 . . . . . . . . . . . 12 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑅 ∈ ℝ+)
13777, 136ltsubrpd 12684 . . . . . . . . . . 11 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → (𝑃𝑅) < 𝑃)
138 modid 13493 . . . . . . . . . . 11 ((((𝑃𝑅) ∈ ℝ ∧ 𝑃 ∈ ℝ+) ∧ (0 ≤ (𝑃𝑅) ∧ (𝑃𝑅) < 𝑃)) → ((𝑃𝑅) mod 𝑃) = (𝑃𝑅))
13978, 54, 81, 137, 138syl22anc 839 . . . . . . . . . 10 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → ((𝑃𝑅) mod 𝑃) = (𝑃𝑅))
14074, 76, 1393eqtr3d 2786 . . . . . . . . 9 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → (-𝑅 mod 𝑃) = (𝑃𝑅))
141140adantr 484 . . . . . . . 8 (((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) ∧ ((𝑅 + 1) / 2) ∈ ℤ) → (-𝑅 mod 𝑃) = (𝑃𝑅))
142 ax-1cn 10811 . . . . . . . . . . . . . 14 1 ∈ ℂ
143142a1i 11 . . . . . . . . . . . . 13 (((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) ∧ ((𝑅 + 1) / 2) ∈ ℤ) → 1 ∈ ℂ)
144135adantr 484 . . . . . . . . . . . . 13 (((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) ∧ ((𝑅 + 1) / 2) ∈ ℤ) → 𝑅 ∈ ℕ)
14535peano2zd 12309 . . . . . . . . . . . . . . . 16 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → (𝑅 + 1) ∈ ℤ)
146 dvdsval2 15842 . . . . . . . . . . . . . . . 16 ((2 ∈ ℤ ∧ 2 ≠ 0 ∧ (𝑅 + 1) ∈ ℤ) → (2 ∥ (𝑅 + 1) ↔ ((𝑅 + 1) / 2) ∈ ℤ))
14711, 39, 145, 146mp3an12i 1467 . . . . . . . . . . . . . . 15 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → (2 ∥ (𝑅 + 1) ↔ ((𝑅 + 1) / 2) ∈ ℤ))
148147biimpar 481 . . . . . . . . . . . . . 14 (((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) ∧ ((𝑅 + 1) / 2) ∈ ℤ) → 2 ∥ (𝑅 + 1))
14935adantr 484 . . . . . . . . . . . . . . 15 (((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) ∧ ((𝑅 + 1) / 2) ∈ ℤ) → 𝑅 ∈ ℤ)
15082a1i 11 . . . . . . . . . . . . . . 15 (((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) ∧ ((𝑅 + 1) / 2) ∈ ℤ) → 2 ∈ ℕ)
151 1lt2 12025 . . . . . . . . . . . . . . . 16 1 < 2
152151a1i 11 . . . . . . . . . . . . . . 15 (((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) ∧ ((𝑅 + 1) / 2) ∈ ℤ) → 1 < 2)
153 ndvdsp1 15996 . . . . . . . . . . . . . . 15 ((𝑅 ∈ ℤ ∧ 2 ∈ ℕ ∧ 1 < 2) → (2 ∥ 𝑅 → ¬ 2 ∥ (𝑅 + 1)))
154149, 150, 152, 153syl3anc 1373 . . . . . . . . . . . . . 14 (((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) ∧ ((𝑅 + 1) / 2) ∈ ℤ) → (2 ∥ 𝑅 → ¬ 2 ∥ (𝑅 + 1)))
155148, 154mt2d 138 . . . . . . . . . . . . 13 (((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) ∧ ((𝑅 + 1) / 2) ∈ ℤ) → ¬ 2 ∥ 𝑅)
156 oexpneg 15930 . . . . . . . . . . . . 13 ((1 ∈ ℂ ∧ 𝑅 ∈ ℕ ∧ ¬ 2 ∥ 𝑅) → (-1↑𝑅) = -(1↑𝑅))
157143, 144, 155, 156syl3anc 1373 . . . . . . . . . . . 12 (((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) ∧ ((𝑅 + 1) / 2) ∈ ℤ) → (-1↑𝑅) = -(1↑𝑅))
158 1exp 13688 . . . . . . . . . . . . . 14 (𝑅 ∈ ℤ → (1↑𝑅) = 1)
159149, 158syl 17 . . . . . . . . . . . . 13 (((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) ∧ ((𝑅 + 1) / 2) ∈ ℤ) → (1↑𝑅) = 1)
160159negeqd 11096 . . . . . . . . . . . 12 (((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) ∧ ((𝑅 + 1) / 2) ∈ ℤ) → -(1↑𝑅) = -1)
161157, 160eqtrd 2778 . . . . . . . . . . 11 (((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) ∧ ((𝑅 + 1) / 2) ∈ ℤ) → (-1↑𝑅) = -1)
162161oveq1d 7246 . . . . . . . . . 10 (((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) ∧ ((𝑅 + 1) / 2) ∈ ℤ) → ((-1↑𝑅) · 𝑅) = (-1 · 𝑅))
16336adantr 484 . . . . . . . . . . 11 (((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) ∧ ((𝑅 + 1) / 2) ∈ ℤ) → 𝑅 ∈ ℂ)
164163mulm1d 11308 . . . . . . . . . 10 (((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) ∧ ((𝑅 + 1) / 2) ∈ ℤ) → (-1 · 𝑅) = -𝑅)
165162, 164eqtrd 2778 . . . . . . . . 9 (((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) ∧ ((𝑅 + 1) / 2) ∈ ℤ) → ((-1↑𝑅) · 𝑅) = -𝑅)
166165oveq1d 7246 . . . . . . . 8 (((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) ∧ ((𝑅 + 1) / 2) ∈ ℤ) → (((-1↑𝑅) · 𝑅) mod 𝑃) = (-𝑅 mod 𝑃))
16766adantr 484 . . . . . . . . 9 (((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) ∧ ((𝑅 + 1) / 2) ∈ ℤ) → 𝑃 ∈ ℂ)
168167, 163, 143pnpcan2d 11251 . . . . . . . 8 (((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) ∧ ((𝑅 + 1) / 2) ∈ ℤ) → ((𝑃 + 1) − (𝑅 + 1)) = (𝑃𝑅))
169141, 166, 1683eqtr4d 2788 . . . . . . 7 (((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) ∧ ((𝑅 + 1) / 2) ∈ ℤ) → (((-1↑𝑅) · 𝑅) mod 𝑃) = ((𝑃 + 1) − (𝑅 + 1)))
170169oveq1d 7246 . . . . . 6 (((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) ∧ ((𝑅 + 1) / 2) ∈ ℤ) → ((((-1↑𝑅) · 𝑅) mod 𝑃) / 2) = (((𝑃 + 1) − (𝑅 + 1)) / 2))
171 peano2cn 11028 . . . . . . . 8 (𝑃 ∈ ℂ → (𝑃 + 1) ∈ ℂ)
172167, 171syl 17 . . . . . . 7 (((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) ∧ ((𝑅 + 1) / 2) ∈ ℤ) → (𝑃 + 1) ∈ ℂ)
173 peano2cn 11028 . . . . . . . 8 (𝑅 ∈ ℂ → (𝑅 + 1) ∈ ℂ)
174163, 173syl 17 . . . . . . 7 (((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) ∧ ((𝑅 + 1) / 2) ∈ ℤ) → (𝑅 + 1) ∈ ℂ)
175 2cnd 11932 . . . . . . 7 (((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) ∧ ((𝑅 + 1) / 2) ∈ ℤ) → 2 ∈ ℂ)
17639a1i 11 . . . . . . 7 (((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) ∧ ((𝑅 + 1) / 2) ∈ ℤ) → 2 ≠ 0)
177172, 174, 175, 176divsubdird 11671 . . . . . 6 (((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) ∧ ((𝑅 + 1) / 2) ∈ ℤ) → (((𝑃 + 1) − (𝑅 + 1)) / 2) = (((𝑃 + 1) / 2) − ((𝑅 + 1) / 2)))
178170, 177eqtrd 2778 . . . . 5 (((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) ∧ ((𝑅 + 1) / 2) ∈ ℤ) → ((((-1↑𝑅) · 𝑅) mod 𝑃) / 2) = (((𝑃 + 1) / 2) − ((𝑅 + 1) / 2)))
179167, 143, 175subadd23d 11235 . . . . . . . . . 10 (((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) ∧ ((𝑅 + 1) / 2) ∈ ℤ) → ((𝑃 − 1) + 2) = (𝑃 + (2 − 1)))
180 2m1e1 11980 . . . . . . . . . . 11 (2 − 1) = 1
181180oveq2i 7242 . . . . . . . . . 10 (𝑃 + (2 − 1)) = (𝑃 + 1)
182179, 181eqtr2di 2796 . . . . . . . . 9 (((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) ∧ ((𝑅 + 1) / 2) ∈ ℤ) → (𝑃 + 1) = ((𝑃 − 1) + 2))
183182oveq1d 7246 . . . . . . . 8 (((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) ∧ ((𝑅 + 1) / 2) ∈ ℤ) → ((𝑃 + 1) / 2) = (((𝑃 − 1) + 2) / 2))
18492nncnd 11870 . . . . . . . . . . 11 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → (𝑃 − 1) ∈ ℂ)
185184adantr 484 . . . . . . . . . 10 (((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) ∧ ((𝑅 + 1) / 2) ∈ ℤ) → (𝑃 − 1) ∈ ℂ)
186185, 175, 175, 176divdird 11670 . . . . . . . . 9 (((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) ∧ ((𝑅 + 1) / 2) ∈ ℤ) → (((𝑃 − 1) + 2) / 2) = (((𝑃 − 1) / 2) + (2 / 2)))
187 2div2e1 11995 . . . . . . . . . 10 (2 / 2) = 1
188187oveq2i 7242 . . . . . . . . 9 (((𝑃 − 1) / 2) + (2 / 2)) = (((𝑃 − 1) / 2) + 1)
189186, 188eqtrdi 2795 . . . . . . . 8 (((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) ∧ ((𝑅 + 1) / 2) ∈ ℤ) → (((𝑃 − 1) + 2) / 2) = (((𝑃 − 1) / 2) + 1))
190183, 189eqtrd 2778 . . . . . . 7 (((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) ∧ ((𝑅 + 1) / 2) ∈ ℤ) → ((𝑃 + 1) / 2) = (((𝑃 − 1) / 2) + 1))
1916adantr 484 . . . . . . . 8 (((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) ∧ ((𝑅 + 1) / 2) ∈ ℤ) → ((𝑃 − 1) / 2) ∈ ℤ)
192191peano2zd 12309 . . . . . . 7 (((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) ∧ ((𝑅 + 1) / 2) ∈ ℤ) → (((𝑃 − 1) / 2) + 1) ∈ ℤ)
193190, 192eqeltrd 2839 . . . . . 6 (((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) ∧ ((𝑅 + 1) / 2) ∈ ℤ) → ((𝑃 + 1) / 2) ∈ ℤ)
194 simpr 488 . . . . . 6 (((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) ∧ ((𝑅 + 1) / 2) ∈ ℤ) → ((𝑅 + 1) / 2) ∈ ℤ)
195193, 194zsubcld 12311 . . . . 5 (((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) ∧ ((𝑅 + 1) / 2) ∈ ℤ) → (((𝑃 + 1) / 2) − ((𝑅 + 1) / 2)) ∈ ℤ)
196178, 195eqeltrd 2839 . . . 4 (((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) ∧ ((𝑅 + 1) / 2) ∈ ℤ) → ((((-1↑𝑅) · 𝑅) mod 𝑃) / 2) ∈ ℤ)
197 zeo 12287 . . . . 5 (𝑅 ∈ ℤ → ((𝑅 / 2) ∈ ℤ ∨ ((𝑅 + 1) / 2) ∈ ℤ))
19835, 197syl 17 . . . 4 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → ((𝑅 / 2) ∈ ℤ ∨ ((𝑅 + 1) / 2) ∈ ℤ))
19965, 196, 198mpjaodan 959 . . 3 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → ((((-1↑𝑅) · 𝑅) mod 𝑃) / 2) ∈ ℤ)
200 m1expcl 13682 . . . . . . . . . 10 (𝑅 ∈ ℤ → (-1↑𝑅) ∈ ℤ)
20135, 200syl 17 . . . . . . . . 9 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → (-1↑𝑅) ∈ ℤ)
202201, 35zmulcld 12312 . . . . . . . 8 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → ((-1↑𝑅) · 𝑅) ∈ ℤ)
203202, 29zmodcld 13489 . . . . . . 7 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → (((-1↑𝑅) · 𝑅) mod 𝑃) ∈ ℕ0)
204203nn0red 12175 . . . . . 6 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → (((-1↑𝑅) · 𝑅) mod 𝑃) ∈ ℝ)
205 fzm1ndvds 15907 . . . . . . . . . . . 12 ((𝑃 ∈ ℕ ∧ 𝑅 ∈ (1...(𝑃 − 1))) → ¬ 𝑃𝑅)
20629, 133, 205syl2anc 587 . . . . . . . . . . 11 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → ¬ 𝑃𝑅)
207 ax-1ne0 10822 . . . . . . . . . . . . . . . . . . . 20 1 ≠ 0
208 divneg2 11580 . . . . . . . . . . . . . . . . . . . 20 ((1 ∈ ℂ ∧ 1 ∈ ℂ ∧ 1 ≠ 0) → -(1 / 1) = (1 / -1))
209142, 142, 207, 208mp3an 1463 . . . . . . . . . . . . . . . . . . 19 -(1 / 1) = (1 / -1)
210 1div1e1 11546 . . . . . . . . . . . . . . . . . . . 20 (1 / 1) = 1
211210negeqi 11095 . . . . . . . . . . . . . . . . . . 19 -(1 / 1) = -1
212209, 211eqtr3i 2768 . . . . . . . . . . . . . . . . . 18 (1 / -1) = -1
213212oveq1i 7241 . . . . . . . . . . . . . . . . 17 ((1 / -1)↑𝑅) = (-1↑𝑅)
2147a1i 11 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → -1 ∈ ℂ)
2159a1i 11 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → -1 ≠ 0)
216214, 215, 35exprecd 13748 . . . . . . . . . . . . . . . . 17 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → ((1 / -1)↑𝑅) = (1 / (-1↑𝑅)))
217213, 216eqtr3id 2793 . . . . . . . . . . . . . . . 16 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → (-1↑𝑅) = (1 / (-1↑𝑅)))
218217oveq2d 7247 . . . . . . . . . . . . . . 15 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → ((-1↑𝑅) · (-1↑𝑅)) = ((-1↑𝑅) · (1 / (-1↑𝑅))))
219201zcnd 12307 . . . . . . . . . . . . . . . 16 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → (-1↑𝑅) ∈ ℂ)
220214, 215, 35expne0d 13746 . . . . . . . . . . . . . . . 16 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → (-1↑𝑅) ≠ 0)
221219, 220recidd 11627 . . . . . . . . . . . . . . 15 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → ((-1↑𝑅) · (1 / (-1↑𝑅))) = 1)
222218, 221eqtrd 2778 . . . . . . . . . . . . . 14 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → ((-1↑𝑅) · (-1↑𝑅)) = 1)
223222oveq1d 7246 . . . . . . . . . . . . 13 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → (((-1↑𝑅) · (-1↑𝑅)) · 𝑅) = (1 · 𝑅))
224219, 219, 36mulassd 10880 . . . . . . . . . . . . 13 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → (((-1↑𝑅) · (-1↑𝑅)) · 𝑅) = ((-1↑𝑅) · ((-1↑𝑅) · 𝑅)))
22536mulid2d 10875 . . . . . . . . . . . . 13 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → (1 · 𝑅) = 𝑅)
226223, 224, 2253eqtr3d 2786 . . . . . . . . . . . 12 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → ((-1↑𝑅) · ((-1↑𝑅) · 𝑅)) = 𝑅)
227226breq2d 5079 . . . . . . . . . . 11 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → (𝑃 ∥ ((-1↑𝑅) · ((-1↑𝑅) · 𝑅)) ↔ 𝑃𝑅))
228206, 227mtbird 328 . . . . . . . . . 10 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → ¬ 𝑃 ∥ ((-1↑𝑅) · ((-1↑𝑅) · 𝑅)))
229 dvdsmultr2 15883 . . . . . . . . . . 11 ((𝑃 ∈ ℤ ∧ (-1↑𝑅) ∈ ℤ ∧ ((-1↑𝑅) · 𝑅) ∈ ℤ) → (𝑃 ∥ ((-1↑𝑅) · 𝑅) → 𝑃 ∥ ((-1↑𝑅) · ((-1↑𝑅) · 𝑅))))
230102, 201, 202, 229syl3anc 1373 . . . . . . . . . 10 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → (𝑃 ∥ ((-1↑𝑅) · 𝑅) → 𝑃 ∥ ((-1↑𝑅) · ((-1↑𝑅) · 𝑅))))
231228, 230mtod 201 . . . . . . . . 9 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → ¬ 𝑃 ∥ ((-1↑𝑅) · 𝑅))
232 dvdsval3 15843 . . . . . . . . . 10 ((𝑃 ∈ ℕ ∧ ((-1↑𝑅) · 𝑅) ∈ ℤ) → (𝑃 ∥ ((-1↑𝑅) · 𝑅) ↔ (((-1↑𝑅) · 𝑅) mod 𝑃) = 0))
23329, 202, 232syl2anc 587 . . . . . . . . 9 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → (𝑃 ∥ ((-1↑𝑅) · 𝑅) ↔ (((-1↑𝑅) · 𝑅) mod 𝑃) = 0))
234231, 233mtbid 327 . . . . . . . 8 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → ¬ (((-1↑𝑅) · 𝑅) mod 𝑃) = 0)
235 elnn0 12116 . . . . . . . . . 10 ((((-1↑𝑅) · 𝑅) mod 𝑃) ∈ ℕ0 ↔ ((((-1↑𝑅) · 𝑅) mod 𝑃) ∈ ℕ ∨ (((-1↑𝑅) · 𝑅) mod 𝑃) = 0))
236203, 235sylib 221 . . . . . . . . 9 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → ((((-1↑𝑅) · 𝑅) mod 𝑃) ∈ ℕ ∨ (((-1↑𝑅) · 𝑅) mod 𝑃) = 0))
237236ord 864 . . . . . . . 8 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → (¬ (((-1↑𝑅) · 𝑅) mod 𝑃) ∈ ℕ → (((-1↑𝑅) · 𝑅) mod 𝑃) = 0))
238234, 237mt3d 150 . . . . . . 7 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → (((-1↑𝑅) · 𝑅) mod 𝑃) ∈ ℕ)
239238nngt0d 11903 . . . . . 6 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → 0 < (((-1↑𝑅) · 𝑅) mod 𝑃))
240204, 95, 239, 97divgt0d 11791 . . . . 5 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → 0 < ((((-1↑𝑅) · 𝑅) mod 𝑃) / 2))
241 elnnz 12210 . . . . 5 (((((-1↑𝑅) · 𝑅) mod 𝑃) / 2) ∈ ℕ ↔ (((((-1↑𝑅) · 𝑅) mod 𝑃) / 2) ∈ ℤ ∧ 0 < ((((-1↑𝑅) · 𝑅) mod 𝑃) / 2)))
242199, 240, 241sylanbrc 586 . . . 4 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → ((((-1↑𝑅) · 𝑅) mod 𝑃) / 2) ∈ ℕ)
243242nnge1d 11902 . . 3 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → 1 ≤ ((((-1↑𝑅) · 𝑅) mod 𝑃) / 2))
244 zmodfz 13490 . . . . . 6 ((((-1↑𝑅) · 𝑅) ∈ ℤ ∧ 𝑃 ∈ ℕ) → (((-1↑𝑅) · 𝑅) mod 𝑃) ∈ (0...(𝑃 − 1)))
245202, 29, 244syl2anc 587 . . . . 5 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → (((-1↑𝑅) · 𝑅) mod 𝑃) ∈ (0...(𝑃 − 1)))
246 elfzle2 13140 . . . . 5 ((((-1↑𝑅) · 𝑅) mod 𝑃) ∈ (0...(𝑃 − 1)) → (((-1↑𝑅) · 𝑅) mod 𝑃) ≤ (𝑃 − 1))
247245, 246syl 17 . . . 4 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → (((-1↑𝑅) · 𝑅) mod 𝑃) ≤ (𝑃 − 1))
248 lediv1 11721 . . . . 5 (((((-1↑𝑅) · 𝑅) mod 𝑃) ∈ ℝ ∧ (𝑃 − 1) ∈ ℝ ∧ (2 ∈ ℝ ∧ 0 < 2)) → ((((-1↑𝑅) · 𝑅) mod 𝑃) ≤ (𝑃 − 1) ↔ ((((-1↑𝑅) · 𝑅) mod 𝑃) / 2) ≤ ((𝑃 − 1) / 2)))
249204, 93, 95, 97, 248syl112anc 1376 . . . 4 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → ((((-1↑𝑅) · 𝑅) mod 𝑃) ≤ (𝑃 − 1) ↔ ((((-1↑𝑅) · 𝑅) mod 𝑃) / 2) ≤ ((𝑃 − 1) / 2)))
250247, 249mpbid 235 . . 3 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → ((((-1↑𝑅) · 𝑅) mod 𝑃) / 2) ≤ ((𝑃 − 1) / 2))
2511, 6, 199, 243, 250elfzd 13127 . 2 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → ((((-1↑𝑅) · 𝑅) mod 𝑃) / 2) ∈ (1...((𝑃 − 1) / 2)))
252 lgseisen.5 . 2 𝑀 = (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ ((((-1↑𝑅) · 𝑅) mod 𝑃) / 2))
253251, 252fmptd 6949 1 (𝜑𝑀:(1...((𝑃 − 1) / 2))⟶(1...((𝑃 − 1) / 2)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 209  wa 399  wo 847   = wceq 1543  wcel 2111  wne 2941  cdif 3877  {csn 4555   class class class wbr 5067  cmpt 5149  wf 6393  cfv 6397  (class class class)co 7231  cc 10751  cr 10752  0cc0 10753  1c1 10754   + caddc 10756   · cmul 10758   < clt 10891  cle 10892  cmin 11086  -cneg 11087   / cdiv 11513  cn 11854  2c2 11909  0cn0 12114  cz 12200  cuz 12462  +crp 12610  ...cfz 13119   mod cmo 13466  cexp 13659  cdvds 15839   gcd cgcd 16077  cprime 16252
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2159  ax-12 2176  ax-ext 2709  ax-sep 5206  ax-nul 5213  ax-pow 5272  ax-pr 5336  ax-un 7541  ax-cnex 10809  ax-resscn 10810  ax-1cn 10811  ax-icn 10812  ax-addcl 10813  ax-addrcl 10814  ax-mulcl 10815  ax-mulrcl 10816  ax-mulcom 10817  ax-addass 10818  ax-mulass 10819  ax-distr 10820  ax-i2m1 10821  ax-1ne0 10822  ax-1rid 10823  ax-rnegex 10824  ax-rrecex 10825  ax-cnre 10826  ax-pre-lttri 10827  ax-pre-lttrn 10828  ax-pre-ltadd 10829  ax-pre-mulgt0 10830  ax-pre-sup 10831
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3or 1090  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-nf 1792  df-sb 2072  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2817  df-nfc 2887  df-ne 2942  df-nel 3048  df-ral 3067  df-rex 3068  df-reu 3069  df-rmo 3070  df-rab 3071  df-v 3422  df-sbc 3709  df-csb 3826  df-dif 3883  df-un 3885  df-in 3887  df-ss 3897  df-pss 3899  df-nul 4252  df-if 4454  df-pw 4529  df-sn 4556  df-pr 4558  df-tp 4560  df-op 4562  df-uni 4834  df-iun 4920  df-br 5068  df-opab 5130  df-mpt 5150  df-tr 5176  df-id 5469  df-eprel 5474  df-po 5482  df-so 5483  df-fr 5523  df-we 5525  df-xp 5571  df-rel 5572  df-cnv 5573  df-co 5574  df-dm 5575  df-rn 5576  df-res 5577  df-ima 5578  df-pred 6175  df-ord 6233  df-on 6234  df-lim 6235  df-suc 6236  df-iota 6355  df-fun 6399  df-fn 6400  df-f 6401  df-f1 6402  df-fo 6403  df-f1o 6404  df-fv 6405  df-riota 7188  df-ov 7234  df-oprab 7235  df-mpo 7236  df-om 7663  df-1st 7779  df-2nd 7780  df-wrecs 8067  df-recs 8128  df-rdg 8166  df-1o 8222  df-2o 8223  df-er 8411  df-en 8647  df-dom 8648  df-sdom 8649  df-fin 8650  df-sup 9082  df-inf 9083  df-pnf 10893  df-mnf 10894  df-xr 10895  df-ltxr 10896  df-le 10897  df-sub 11088  df-neg 11089  df-div 11514  df-nn 11855  df-2 11917  df-3 11918  df-n0 12115  df-z 12201  df-uz 12463  df-rp 12611  df-fz 13120  df-fl 13391  df-mod 13467  df-seq 13599  df-exp 13660  df-cj 14686  df-re 14687  df-im 14688  df-sqrt 14822  df-abs 14823  df-dvds 15840  df-gcd 16078  df-prm 16253
This theorem is referenced by:  lgseisenlem2  26281  lgseisenlem3  26282
  Copyright terms: Public domain W3C validator