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

Theorem lgseisenlem1 25094
Description: Lemma for lgseisen 25098. 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 neg1cn 11121 . . . . . . . . . . . . . . 15 -1 ∈ ℂ
21a1i 11 . . . . . . . . . . . . . 14 (((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) ∧ (𝑅 / 2) ∈ ℤ) → -1 ∈ ℂ)
3 neg1ne0 11123 . . . . . . . . . . . . . . 15 -1 ≠ 0
43a1i 11 . . . . . . . . . . . . . 14 (((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) ∧ (𝑅 / 2) ∈ ℤ) → -1 ≠ 0)
5 2z 11406 . . . . . . . . . . . . . . 15 2 ∈ ℤ
65a1i 11 . . . . . . . . . . . . . 14 (((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) ∧ (𝑅 / 2) ∈ ℤ) → 2 ∈ ℤ)
7 simpr 477 . . . . . . . . . . . . . 14 (((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) ∧ (𝑅 / 2) ∈ ℤ) → (𝑅 / 2) ∈ ℤ)
8 expmulz 12901 . . . . . . . . . . . . . 14 (((-1 ∈ ℂ ∧ -1 ≠ 0) ∧ (2 ∈ ℤ ∧ (𝑅 / 2) ∈ ℤ)) → (-1↑(2 · (𝑅 / 2))) = ((-1↑2)↑(𝑅 / 2)))
92, 4, 6, 7, 8syl22anc 1326 . . . . . . . . . . . . 13 (((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) ∧ (𝑅 / 2) ∈ ℤ) → (-1↑(2 · (𝑅 / 2))) = ((-1↑2)↑(𝑅 / 2)))
10 lgseisen.4 . . . . . . . . . . . . . . . . . . . 20 𝑅 = ((𝑄 · (2 · 𝑥)) mod 𝑃)
11 lgseisen.2 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑𝑄 ∈ (ℙ ∖ {2}))
1211adantr 481 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑄 ∈ (ℙ ∖ {2}))
1312eldifad 3584 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑄 ∈ ℙ)
14 prmz 15383 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑄 ∈ ℙ → 𝑄 ∈ ℤ)
1513, 14syl 17 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑄 ∈ ℤ)
16 elfzelz 12339 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑥 ∈ (1...((𝑃 − 1) / 2)) → 𝑥 ∈ ℤ)
1716adantl 482 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑥 ∈ ℤ)
18 zmulcl 11423 . . . . . . . . . . . . . . . . . . . . . . 23 ((2 ∈ ℤ ∧ 𝑥 ∈ ℤ) → (2 · 𝑥) ∈ ℤ)
195, 17, 18sylancr 695 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → (2 · 𝑥) ∈ ℤ)
2015, 19zmulcld 11485 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → (𝑄 · (2 · 𝑥)) ∈ ℤ)
21 lgseisen.1 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑𝑃 ∈ (ℙ ∖ {2}))
2221adantr 481 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑃 ∈ (ℙ ∖ {2}))
2322eldifad 3584 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑃 ∈ ℙ)
24 prmnn 15382 . . . . . . . . . . . . . . . . . . . . . 22 (𝑃 ∈ ℙ → 𝑃 ∈ ℕ)
2523, 24syl 17 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑃 ∈ ℕ)
26 zmodfz 12687 . . . . . . . . . . . . . . . . . . . . 21 (((𝑄 · (2 · 𝑥)) ∈ ℤ ∧ 𝑃 ∈ ℕ) → ((𝑄 · (2 · 𝑥)) mod 𝑃) ∈ (0...(𝑃 − 1)))
2720, 25, 26syl2anc 693 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → ((𝑄 · (2 · 𝑥)) mod 𝑃) ∈ (0...(𝑃 − 1)))
2810, 27syl5eqel 2704 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑅 ∈ (0...(𝑃 − 1)))
29 elfznn0 12429 . . . . . . . . . . . . . . . . . . 19 (𝑅 ∈ (0...(𝑃 − 1)) → 𝑅 ∈ ℕ0)
3028, 29syl 17 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑅 ∈ ℕ0)
3130nn0zd 11477 . . . . . . . . . . . . . . . . 17 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑅 ∈ ℤ)
3231zcnd 11480 . . . . . . . . . . . . . . . 16 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑅 ∈ ℂ)
3332adantr 481 . . . . . . . . . . . . . . 15 (((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) ∧ (𝑅 / 2) ∈ ℤ) → 𝑅 ∈ ℂ)
34 2cnd 11090 . . . . . . . . . . . . . . 15 (((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) ∧ (𝑅 / 2) ∈ ℤ) → 2 ∈ ℂ)
35 2ne0 11110 . . . . . . . . . . . . . . . 16 2 ≠ 0
3635a1i 11 . . . . . . . . . . . . . . 15 (((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) ∧ (𝑅 / 2) ∈ ℤ) → 2 ≠ 0)
3733, 34, 36divcan2d 10800 . . . . . . . . . . . . . 14 (((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) ∧ (𝑅 / 2) ∈ ℤ) → (2 · (𝑅 / 2)) = 𝑅)
3837oveq2d 6663 . . . . . . . . . . . . 13 (((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) ∧ (𝑅 / 2) ∈ ℤ) → (-1↑(2 · (𝑅 / 2))) = (-1↑𝑅))
39 neg1sqe1 12954 . . . . . . . . . . . . . . 15 (-1↑2) = 1
4039oveq1i 6657 . . . . . . . . . . . . . 14 ((-1↑2)↑(𝑅 / 2)) = (1↑(𝑅 / 2))
41 1exp 12884 . . . . . . . . . . . . . . 15 ((𝑅 / 2) ∈ ℤ → (1↑(𝑅 / 2)) = 1)
4241adantl 482 . . . . . . . . . . . . . 14 (((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) ∧ (𝑅 / 2) ∈ ℤ) → (1↑(𝑅 / 2)) = 1)
4340, 42syl5eq 2667 . . . . . . . . . . . . 13 (((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) ∧ (𝑅 / 2) ∈ ℤ) → ((-1↑2)↑(𝑅 / 2)) = 1)
449, 38, 433eqtr3d 2663 . . . . . . . . . . . 12 (((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) ∧ (𝑅 / 2) ∈ ℤ) → (-1↑𝑅) = 1)
4544oveq1d 6662 . . . . . . . . . . 11 (((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) ∧ (𝑅 / 2) ∈ ℤ) → ((-1↑𝑅) · 𝑅) = (1 · 𝑅))
4633mulid2d 10055 . . . . . . . . . . 11 (((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) ∧ (𝑅 / 2) ∈ ℤ) → (1 · 𝑅) = 𝑅)
4745, 46eqtrd 2655 . . . . . . . . . 10 (((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) ∧ (𝑅 / 2) ∈ ℤ) → ((-1↑𝑅) · 𝑅) = 𝑅)
4847oveq1d 6662 . . . . . . . . 9 (((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) ∧ (𝑅 / 2) ∈ ℤ) → (((-1↑𝑅) · 𝑅) mod 𝑃) = (𝑅 mod 𝑃))
4930nn0red 11349 . . . . . . . . . . 11 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑅 ∈ ℝ)
5025nnrpd 11867 . . . . . . . . . . 11 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑃 ∈ ℝ+)
5130nn0ge0d 11351 . . . . . . . . . . 11 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → 0 ≤ 𝑅)
5220zred 11479 . . . . . . . . . . . . 13 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → (𝑄 · (2 · 𝑥)) ∈ ℝ)
53 modlt 12674 . . . . . . . . . . . . 13 (((𝑄 · (2 · 𝑥)) ∈ ℝ ∧ 𝑃 ∈ ℝ+) → ((𝑄 · (2 · 𝑥)) mod 𝑃) < 𝑃)
5452, 50, 53syl2anc 693 . . . . . . . . . . . 12 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → ((𝑄 · (2 · 𝑥)) mod 𝑃) < 𝑃)
5510, 54syl5eqbr 4686 . . . . . . . . . . 11 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑅 < 𝑃)
56 modid 12690 . . . . . . . . . . 11 (((𝑅 ∈ ℝ ∧ 𝑃 ∈ ℝ+) ∧ (0 ≤ 𝑅𝑅 < 𝑃)) → (𝑅 mod 𝑃) = 𝑅)
5749, 50, 51, 55, 56syl22anc 1326 . . . . . . . . . 10 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → (𝑅 mod 𝑃) = 𝑅)
5857adantr 481 . . . . . . . . 9 (((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) ∧ (𝑅 / 2) ∈ ℤ) → (𝑅 mod 𝑃) = 𝑅)
5948, 58eqtrd 2655 . . . . . . . 8 (((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) ∧ (𝑅 / 2) ∈ ℤ) → (((-1↑𝑅) · 𝑅) mod 𝑃) = 𝑅)
6059oveq1d 6662 . . . . . . 7 (((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) ∧ (𝑅 / 2) ∈ ℤ) → ((((-1↑𝑅) · 𝑅) mod 𝑃) / 2) = (𝑅 / 2))
6160, 7eqeltrd 2700 . . . . . 6 (((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) ∧ (𝑅 / 2) ∈ ℤ) → ((((-1↑𝑅) · 𝑅) mod 𝑃) / 2) ∈ ℤ)
6225nncnd 11033 . . . . . . . . . . . . . . . 16 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑃 ∈ ℂ)
6362mulid2d 10055 . . . . . . . . . . . . . . 15 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → (1 · 𝑃) = 𝑃)
6463oveq2d 6663 . . . . . . . . . . . . . 14 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → (-𝑅 + (1 · 𝑃)) = (-𝑅 + 𝑃))
6549renegcld 10454 . . . . . . . . . . . . . . . 16 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → -𝑅 ∈ ℝ)
6665recnd 10065 . . . . . . . . . . . . . . 15 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → -𝑅 ∈ ℂ)
6762, 66addcomd 10235 . . . . . . . . . . . . . 14 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → (𝑃 + -𝑅) = (-𝑅 + 𝑃))
6862, 32negsubd 10395 . . . . . . . . . . . . . 14 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → (𝑃 + -𝑅) = (𝑃𝑅))
6964, 67, 683eqtr2d 2661 . . . . . . . . . . . . 13 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → (-𝑅 + (1 · 𝑃)) = (𝑃𝑅))
7069oveq1d 6662 . . . . . . . . . . . 12 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → ((-𝑅 + (1 · 𝑃)) mod 𝑃) = ((𝑃𝑅) mod 𝑃))
71 1zzd 11405 . . . . . . . . . . . . 13 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → 1 ∈ ℤ)
72 modcyc 12700 . . . . . . . . . . . . 13 ((-𝑅 ∈ ℝ ∧ 𝑃 ∈ ℝ+ ∧ 1 ∈ ℤ) → ((-𝑅 + (1 · 𝑃)) mod 𝑃) = (-𝑅 mod 𝑃))
7365, 50, 71, 72syl3anc 1325 . . . . . . . . . . . 12 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → ((-𝑅 + (1 · 𝑃)) mod 𝑃) = (-𝑅 mod 𝑃))
7425nnred 11032 . . . . . . . . . . . . . 14 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑃 ∈ ℝ)
7574, 49resubcld 10455 . . . . . . . . . . . . 13 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → (𝑃𝑅) ∈ ℝ)
7649, 74, 55ltled 10182 . . . . . . . . . . . . . 14 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑅𝑃)
7774, 49subge0d 10614 . . . . . . . . . . . . . 14 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → (0 ≤ (𝑃𝑅) ↔ 𝑅𝑃))
7876, 77mpbird 247 . . . . . . . . . . . . 13 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → 0 ≤ (𝑃𝑅))
79 2nn 11182 . . . . . . . . . . . . . . . . . . . . . . . 24 2 ∈ ℕ
80 elfznn 12367 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑥 ∈ (1...((𝑃 − 1) / 2)) → 𝑥 ∈ ℕ)
8180adantl 482 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑥 ∈ ℕ)
82 nnmulcl 11040 . . . . . . . . . . . . . . . . . . . . . . . 24 ((2 ∈ ℕ ∧ 𝑥 ∈ ℕ) → (2 · 𝑥) ∈ ℕ)
8379, 81, 82sylancr 695 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → (2 · 𝑥) ∈ ℕ)
84 elfzle2 12342 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑥 ∈ (1...((𝑃 − 1) / 2)) → 𝑥 ≤ ((𝑃 − 1) / 2))
8584adantl 482 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑥 ≤ ((𝑃 − 1) / 2))
8681nnred 11032 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑥 ∈ ℝ)
87 prmuz2 15402 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑃 ∈ ℙ → 𝑃 ∈ (ℤ‘2))
88 uz2m1nn 11760 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑃 ∈ (ℤ‘2) → (𝑃 − 1) ∈ ℕ)
8923, 87, 883syl 18 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → (𝑃 − 1) ∈ ℕ)
9089nnred 11032 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → (𝑃 − 1) ∈ ℝ)
91 2re 11087 . . . . . . . . . . . . . . . . . . . . . . . . . 26 2 ∈ ℝ
9291a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → 2 ∈ ℝ)
93 2pos 11109 . . . . . . . . . . . . . . . . . . . . . . . . . 26 0 < 2
9493a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → 0 < 2)
95 lemuldiv2 10901 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑥 ∈ ℝ ∧ (𝑃 − 1) ∈ ℝ ∧ (2 ∈ ℝ ∧ 0 < 2)) → ((2 · 𝑥) ≤ (𝑃 − 1) ↔ 𝑥 ≤ ((𝑃 − 1) / 2)))
9686, 90, 92, 94, 95syl112anc 1329 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → ((2 · 𝑥) ≤ (𝑃 − 1) ↔ 𝑥 ≤ ((𝑃 − 1) / 2)))
9785, 96mpbird 247 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → (2 · 𝑥) ≤ (𝑃 − 1))
98 prmz 15383 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑃 ∈ ℙ → 𝑃 ∈ ℤ)
9923, 98syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑃 ∈ ℤ)
100 peano2zm 11417 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑃 ∈ ℤ → (𝑃 − 1) ∈ ℤ)
101 fznn 12405 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑃 − 1) ∈ ℤ → ((2 · 𝑥) ∈ (1...(𝑃 − 1)) ↔ ((2 · 𝑥) ∈ ℕ ∧ (2 · 𝑥) ≤ (𝑃 − 1))))
10299, 100, 1013syl 18 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → ((2 · 𝑥) ∈ (1...(𝑃 − 1)) ↔ ((2 · 𝑥) ∈ ℕ ∧ (2 · 𝑥) ≤ (𝑃 − 1))))
10383, 97, 102mpbir2and 957 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → (2 · 𝑥) ∈ (1...(𝑃 − 1)))
104 fzm1ndvds 15038 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑃 ∈ ℕ ∧ (2 · 𝑥) ∈ (1...(𝑃 − 1))) → ¬ 𝑃 ∥ (2 · 𝑥))
10525, 103, 104syl2anc 693 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → ¬ 𝑃 ∥ (2 · 𝑥))
106 lgseisen.3 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑𝑃𝑄)
107106adantr 481 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑃𝑄)
108 prmrp 15418 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑃 ∈ ℙ ∧ 𝑄 ∈ ℙ) → ((𝑃 gcd 𝑄) = 1 ↔ 𝑃𝑄))
10923, 13, 108syl2anc 693 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → ((𝑃 gcd 𝑄) = 1 ↔ 𝑃𝑄))
110107, 109mpbird 247 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → (𝑃 gcd 𝑄) = 1)
111 coprmdvds 15360 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑃 ∈ ℤ ∧ 𝑄 ∈ ℤ ∧ (2 · 𝑥) ∈ ℤ) → ((𝑃 ∥ (𝑄 · (2 · 𝑥)) ∧ (𝑃 gcd 𝑄) = 1) → 𝑃 ∥ (2 · 𝑥)))
11299, 15, 19, 111syl3anc 1325 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → ((𝑃 ∥ (𝑄 · (2 · 𝑥)) ∧ (𝑃 gcd 𝑄) = 1) → 𝑃 ∥ (2 · 𝑥)))
113110, 112mpan2d 710 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → (𝑃 ∥ (𝑄 · (2 · 𝑥)) → 𝑃 ∥ (2 · 𝑥)))
114105, 113mtod 189 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → ¬ 𝑃 ∥ (𝑄 · (2 · 𝑥)))
115 dvdsval3 14981 . . . . . . . . . . . . . . . . . . . . 21 ((𝑃 ∈ ℕ ∧ (𝑄 · (2 · 𝑥)) ∈ ℤ) → (𝑃 ∥ (𝑄 · (2 · 𝑥)) ↔ ((𝑄 · (2 · 𝑥)) mod 𝑃) = 0))
11625, 20, 115syl2anc 693 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → (𝑃 ∥ (𝑄 · (2 · 𝑥)) ↔ ((𝑄 · (2 · 𝑥)) mod 𝑃) = 0))
117114, 116mtbid 314 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → ¬ ((𝑄 · (2 · 𝑥)) mod 𝑃) = 0)
11810eqeq1i 2626 . . . . . . . . . . . . . . . . . . 19 (𝑅 = 0 ↔ ((𝑄 · (2 · 𝑥)) mod 𝑃) = 0)
119117, 118sylnibr 319 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → ¬ 𝑅 = 0)
12089nnnn0d 11348 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → (𝑃 − 1) ∈ ℕ0)
121 nn0uz 11719 . . . . . . . . . . . . . . . . . . . . . 22 0 = (ℤ‘0)
122120, 121syl6eleq 2710 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → (𝑃 − 1) ∈ (ℤ‘0))
123 elfzp12 12415 . . . . . . . . . . . . . . . . . . . . 21 ((𝑃 − 1) ∈ (ℤ‘0) → (𝑅 ∈ (0...(𝑃 − 1)) ↔ (𝑅 = 0 ∨ 𝑅 ∈ ((0 + 1)...(𝑃 − 1)))))
124122, 123syl 17 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → (𝑅 ∈ (0...(𝑃 − 1)) ↔ (𝑅 = 0 ∨ 𝑅 ∈ ((0 + 1)...(𝑃 − 1)))))
12528, 124mpbid 222 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → (𝑅 = 0 ∨ 𝑅 ∈ ((0 + 1)...(𝑃 − 1))))
126125ord 392 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → (¬ 𝑅 = 0 → 𝑅 ∈ ((0 + 1)...(𝑃 − 1))))
127119, 126mpd 15 . . . . . . . . . . . . . . . . 17 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑅 ∈ ((0 + 1)...(𝑃 − 1)))
128 1e0p1 11549 . . . . . . . . . . . . . . . . . 18 1 = (0 + 1)
129128oveq1i 6657 . . . . . . . . . . . . . . . . 17 (1...(𝑃 − 1)) = ((0 + 1)...(𝑃 − 1))
130127, 129syl6eleqr 2711 . . . . . . . . . . . . . . . 16 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑅 ∈ (1...(𝑃 − 1)))
131 elfznn 12367 . . . . . . . . . . . . . . . 16 (𝑅 ∈ (1...(𝑃 − 1)) → 𝑅 ∈ ℕ)
132130, 131syl 17 . . . . . . . . . . . . . . 15 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑅 ∈ ℕ)
133132nnrpd 11867 . . . . . . . . . . . . . 14 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑅 ∈ ℝ+)
13474, 133ltsubrpd 11901 . . . . . . . . . . . . 13 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → (𝑃𝑅) < 𝑃)
135 modid 12690 . . . . . . . . . . . . 13 ((((𝑃𝑅) ∈ ℝ ∧ 𝑃 ∈ ℝ+) ∧ (0 ≤ (𝑃𝑅) ∧ (𝑃𝑅) < 𝑃)) → ((𝑃𝑅) mod 𝑃) = (𝑃𝑅))
13675, 50, 78, 134, 135syl22anc 1326 . . . . . . . . . . . 12 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → ((𝑃𝑅) mod 𝑃) = (𝑃𝑅))
13770, 73, 1363eqtr3d 2663 . . . . . . . . . . 11 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → (-𝑅 mod 𝑃) = (𝑃𝑅))
138137adantr 481 . . . . . . . . . 10 (((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) ∧ ((𝑅 + 1) / 2) ∈ ℤ) → (-𝑅 mod 𝑃) = (𝑃𝑅))
139 ax-1cn 9991 . . . . . . . . . . . . . . . 16 1 ∈ ℂ
140139a1i 11 . . . . . . . . . . . . . . 15 (((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) ∧ ((𝑅 + 1) / 2) ∈ ℤ) → 1 ∈ ℂ)
141132adantr 481 . . . . . . . . . . . . . . 15 (((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) ∧ ((𝑅 + 1) / 2) ∈ ℤ) → 𝑅 ∈ ℕ)
1425a1i 11 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → 2 ∈ ℤ)
14335a1i 11 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → 2 ≠ 0)
14431peano2zd 11482 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → (𝑅 + 1) ∈ ℤ)
145 dvdsval2 14980 . . . . . . . . . . . . . . . . . 18 ((2 ∈ ℤ ∧ 2 ≠ 0 ∧ (𝑅 + 1) ∈ ℤ) → (2 ∥ (𝑅 + 1) ↔ ((𝑅 + 1) / 2) ∈ ℤ))
146142, 143, 144, 145syl3anc 1325 . . . . . . . . . . . . . . . . 17 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → (2 ∥ (𝑅 + 1) ↔ ((𝑅 + 1) / 2) ∈ ℤ))
147146biimpar 502 . . . . . . . . . . . . . . . 16 (((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) ∧ ((𝑅 + 1) / 2) ∈ ℤ) → 2 ∥ (𝑅 + 1))
14831adantr 481 . . . . . . . . . . . . . . . . 17 (((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) ∧ ((𝑅 + 1) / 2) ∈ ℤ) → 𝑅 ∈ ℤ)
14979a1i 11 . . . . . . . . . . . . . . . . 17 (((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) ∧ ((𝑅 + 1) / 2) ∈ ℤ) → 2 ∈ ℕ)
150 1lt2 11191 . . . . . . . . . . . . . . . . . 18 1 < 2
151150a1i 11 . . . . . . . . . . . . . . . . 17 (((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) ∧ ((𝑅 + 1) / 2) ∈ ℤ) → 1 < 2)
152 ndvdsp1 15129 . . . . . . . . . . . . . . . . 17 ((𝑅 ∈ ℤ ∧ 2 ∈ ℕ ∧ 1 < 2) → (2 ∥ 𝑅 → ¬ 2 ∥ (𝑅 + 1)))
153148, 149, 151, 152syl3anc 1325 . . . . . . . . . . . . . . . 16 (((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) ∧ ((𝑅 + 1) / 2) ∈ ℤ) → (2 ∥ 𝑅 → ¬ 2 ∥ (𝑅 + 1)))
154147, 153mt2d 131 . . . . . . . . . . . . . . 15 (((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) ∧ ((𝑅 + 1) / 2) ∈ ℤ) → ¬ 2 ∥ 𝑅)
155 oexpneg 15063 . . . . . . . . . . . . . . 15 ((1 ∈ ℂ ∧ 𝑅 ∈ ℕ ∧ ¬ 2 ∥ 𝑅) → (-1↑𝑅) = -(1↑𝑅))
156140, 141, 154, 155syl3anc 1325 . . . . . . . . . . . . . 14 (((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) ∧ ((𝑅 + 1) / 2) ∈ ℤ) → (-1↑𝑅) = -(1↑𝑅))
157 1exp 12884 . . . . . . . . . . . . . . . 16 (𝑅 ∈ ℤ → (1↑𝑅) = 1)
158148, 157syl 17 . . . . . . . . . . . . . . 15 (((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) ∧ ((𝑅 + 1) / 2) ∈ ℤ) → (1↑𝑅) = 1)
159158negeqd 10272 . . . . . . . . . . . . . 14 (((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) ∧ ((𝑅 + 1) / 2) ∈ ℤ) → -(1↑𝑅) = -1)
160156, 159eqtrd 2655 . . . . . . . . . . . . 13 (((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) ∧ ((𝑅 + 1) / 2) ∈ ℤ) → (-1↑𝑅) = -1)
161160oveq1d 6662 . . . . . . . . . . . 12 (((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) ∧ ((𝑅 + 1) / 2) ∈ ℤ) → ((-1↑𝑅) · 𝑅) = (-1 · 𝑅))
16232adantr 481 . . . . . . . . . . . . 13 (((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) ∧ ((𝑅 + 1) / 2) ∈ ℤ) → 𝑅 ∈ ℂ)
163162mulm1d 10479 . . . . . . . . . . . 12 (((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) ∧ ((𝑅 + 1) / 2) ∈ ℤ) → (-1 · 𝑅) = -𝑅)
164161, 163eqtrd 2655 . . . . . . . . . . 11 (((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) ∧ ((𝑅 + 1) / 2) ∈ ℤ) → ((-1↑𝑅) · 𝑅) = -𝑅)
165164oveq1d 6662 . . . . . . . . . 10 (((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) ∧ ((𝑅 + 1) / 2) ∈ ℤ) → (((-1↑𝑅) · 𝑅) mod 𝑃) = (-𝑅 mod 𝑃))
16662adantr 481 . . . . . . . . . . 11 (((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) ∧ ((𝑅 + 1) / 2) ∈ ℤ) → 𝑃 ∈ ℂ)
167166, 162, 140pnpcan2d 10427 . . . . . . . . . 10 (((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) ∧ ((𝑅 + 1) / 2) ∈ ℤ) → ((𝑃 + 1) − (𝑅 + 1)) = (𝑃𝑅))
168138, 165, 1673eqtr4d 2665 . . . . . . . . 9 (((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) ∧ ((𝑅 + 1) / 2) ∈ ℤ) → (((-1↑𝑅) · 𝑅) mod 𝑃) = ((𝑃 + 1) − (𝑅 + 1)))
169168oveq1d 6662 . . . . . . . 8 (((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) ∧ ((𝑅 + 1) / 2) ∈ ℤ) → ((((-1↑𝑅) · 𝑅) mod 𝑃) / 2) = (((𝑃 + 1) − (𝑅 + 1)) / 2))
170 peano2cn 10205 . . . . . . . . . 10 (𝑃 ∈ ℂ → (𝑃 + 1) ∈ ℂ)
171166, 170syl 17 . . . . . . . . 9 (((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) ∧ ((𝑅 + 1) / 2) ∈ ℤ) → (𝑃 + 1) ∈ ℂ)
172 peano2cn 10205 . . . . . . . . . 10 (𝑅 ∈ ℂ → (𝑅 + 1) ∈ ℂ)
173162, 172syl 17 . . . . . . . . 9 (((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) ∧ ((𝑅 + 1) / 2) ∈ ℤ) → (𝑅 + 1) ∈ ℂ)
174 2cnd 11090 . . . . . . . . 9 (((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) ∧ ((𝑅 + 1) / 2) ∈ ℤ) → 2 ∈ ℂ)
17535a1i 11 . . . . . . . . 9 (((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) ∧ ((𝑅 + 1) / 2) ∈ ℤ) → 2 ≠ 0)
176171, 173, 174, 175divsubdird 10837 . . . . . . . 8 (((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) ∧ ((𝑅 + 1) / 2) ∈ ℤ) → (((𝑃 + 1) − (𝑅 + 1)) / 2) = (((𝑃 + 1) / 2) − ((𝑅 + 1) / 2)))
177169, 176eqtrd 2655 . . . . . . 7 (((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) ∧ ((𝑅 + 1) / 2) ∈ ℤ) → ((((-1↑𝑅) · 𝑅) mod 𝑃) / 2) = (((𝑃 + 1) / 2) − ((𝑅 + 1) / 2)))
178166, 140, 174subadd23d 10411 . . . . . . . . . . . 12 (((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) ∧ ((𝑅 + 1) / 2) ∈ ℤ) → ((𝑃 − 1) + 2) = (𝑃 + (2 − 1)))
179 2m1e1 11132 . . . . . . . . . . . . 13 (2 − 1) = 1
180179oveq2i 6658 . . . . . . . . . . . 12 (𝑃 + (2 − 1)) = (𝑃 + 1)
181178, 180syl6req 2672 . . . . . . . . . . 11 (((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) ∧ ((𝑅 + 1) / 2) ∈ ℤ) → (𝑃 + 1) = ((𝑃 − 1) + 2))
182181oveq1d 6662 . . . . . . . . . 10 (((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) ∧ ((𝑅 + 1) / 2) ∈ ℤ) → ((𝑃 + 1) / 2) = (((𝑃 − 1) + 2) / 2))
18389nncnd 11033 . . . . . . . . . . . . 13 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → (𝑃 − 1) ∈ ℂ)
184183adantr 481 . . . . . . . . . . . 12 (((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) ∧ ((𝑅 + 1) / 2) ∈ ℤ) → (𝑃 − 1) ∈ ℂ)
185184, 174, 174, 175divdird 10836 . . . . . . . . . . 11 (((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) ∧ ((𝑅 + 1) / 2) ∈ ℤ) → (((𝑃 − 1) + 2) / 2) = (((𝑃 − 1) / 2) + (2 / 2)))
186 2div2e1 11147 . . . . . . . . . . . 12 (2 / 2) = 1
187186oveq2i 6658 . . . . . . . . . . 11 (((𝑃 − 1) / 2) + (2 / 2)) = (((𝑃 − 1) / 2) + 1)
188185, 187syl6eq 2671 . . . . . . . . . 10 (((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) ∧ ((𝑅 + 1) / 2) ∈ ℤ) → (((𝑃 − 1) + 2) / 2) = (((𝑃 − 1) / 2) + 1))
189182, 188eqtrd 2655 . . . . . . . . 9 (((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) ∧ ((𝑅 + 1) / 2) ∈ ℤ) → ((𝑃 + 1) / 2) = (((𝑃 − 1) / 2) + 1))
190 oddprm 15509 . . . . . . . . . . . . 13 (𝑃 ∈ (ℙ ∖ {2}) → ((𝑃 − 1) / 2) ∈ ℕ)
19122, 190syl 17 . . . . . . . . . . . 12 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → ((𝑃 − 1) / 2) ∈ ℕ)
192191nnzd 11478 . . . . . . . . . . 11 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → ((𝑃 − 1) / 2) ∈ ℤ)
193192adantr 481 . . . . . . . . . 10 (((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) ∧ ((𝑅 + 1) / 2) ∈ ℤ) → ((𝑃 − 1) / 2) ∈ ℤ)
194193peano2zd 11482 . . . . . . . . 9 (((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) ∧ ((𝑅 + 1) / 2) ∈ ℤ) → (((𝑃 − 1) / 2) + 1) ∈ ℤ)
195189, 194eqeltrd 2700 . . . . . . . 8 (((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) ∧ ((𝑅 + 1) / 2) ∈ ℤ) → ((𝑃 + 1) / 2) ∈ ℤ)
196 simpr 477 . . . . . . . 8 (((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) ∧ ((𝑅 + 1) / 2) ∈ ℤ) → ((𝑅 + 1) / 2) ∈ ℤ)
197195, 196zsubcld 11484 . . . . . . 7 (((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) ∧ ((𝑅 + 1) / 2) ∈ ℤ) → (((𝑃 + 1) / 2) − ((𝑅 + 1) / 2)) ∈ ℤ)
198177, 197eqeltrd 2700 . . . . . 6 (((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) ∧ ((𝑅 + 1) / 2) ∈ ℤ) → ((((-1↑𝑅) · 𝑅) mod 𝑃) / 2) ∈ ℤ)
199 zeo 11460 . . . . . . 7 (𝑅 ∈ ℤ → ((𝑅 / 2) ∈ ℤ ∨ ((𝑅 + 1) / 2) ∈ ℤ))
20031, 199syl 17 . . . . . 6 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → ((𝑅 / 2) ∈ ℤ ∨ ((𝑅 + 1) / 2) ∈ ℤ))
20161, 198, 200mpjaodan 827 . . . . 5 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → ((((-1↑𝑅) · 𝑅) mod 𝑃) / 2) ∈ ℤ)
202 m1expcl 12878 . . . . . . . . . 10 (𝑅 ∈ ℤ → (-1↑𝑅) ∈ ℤ)
20331, 202syl 17 . . . . . . . . 9 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → (-1↑𝑅) ∈ ℤ)
204203, 31zmulcld 11485 . . . . . . . 8 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → ((-1↑𝑅) · 𝑅) ∈ ℤ)
205204, 25zmodcld 12686 . . . . . . 7 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → (((-1↑𝑅) · 𝑅) mod 𝑃) ∈ ℕ0)
206205nn0red 11349 . . . . . 6 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → (((-1↑𝑅) · 𝑅) mod 𝑃) ∈ ℝ)
207 fzm1ndvds 15038 . . . . . . . . . . . 12 ((𝑃 ∈ ℕ ∧ 𝑅 ∈ (1...(𝑃 − 1))) → ¬ 𝑃𝑅)
20825, 130, 207syl2anc 693 . . . . . . . . . . 11 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → ¬ 𝑃𝑅)
209 ax-1ne0 10002 . . . . . . . . . . . . . . . . . . . 20 1 ≠ 0
210 divneg2 10746 . . . . . . . . . . . . . . . . . . . 20 ((1 ∈ ℂ ∧ 1 ∈ ℂ ∧ 1 ≠ 0) → -(1 / 1) = (1 / -1))
211139, 139, 209, 210mp3an 1423 . . . . . . . . . . . . . . . . . . 19 -(1 / 1) = (1 / -1)
212 1div1e1 10714 . . . . . . . . . . . . . . . . . . . 20 (1 / 1) = 1
213212negeqi 10271 . . . . . . . . . . . . . . . . . . 19 -(1 / 1) = -1
214211, 213eqtr3i 2645 . . . . . . . . . . . . . . . . . 18 (1 / -1) = -1
215214oveq1i 6657 . . . . . . . . . . . . . . . . 17 ((1 / -1)↑𝑅) = (-1↑𝑅)
2161a1i 11 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → -1 ∈ ℂ)
2173a1i 11 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → -1 ≠ 0)
218216, 217, 31exprecd 13011 . . . . . . . . . . . . . . . . 17 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → ((1 / -1)↑𝑅) = (1 / (-1↑𝑅)))
219215, 218syl5eqr 2669 . . . . . . . . . . . . . . . 16 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → (-1↑𝑅) = (1 / (-1↑𝑅)))
220219oveq2d 6663 . . . . . . . . . . . . . . 15 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → ((-1↑𝑅) · (-1↑𝑅)) = ((-1↑𝑅) · (1 / (-1↑𝑅))))
221203zcnd 11480 . . . . . . . . . . . . . . . 16 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → (-1↑𝑅) ∈ ℂ)
222216, 217, 31expne0d 13009 . . . . . . . . . . . . . . . 16 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → (-1↑𝑅) ≠ 0)
223221, 222recidd 10793 . . . . . . . . . . . . . . 15 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → ((-1↑𝑅) · (1 / (-1↑𝑅))) = 1)
224220, 223eqtrd 2655 . . . . . . . . . . . . . 14 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → ((-1↑𝑅) · (-1↑𝑅)) = 1)
225224oveq1d 6662 . . . . . . . . . . . . 13 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → (((-1↑𝑅) · (-1↑𝑅)) · 𝑅) = (1 · 𝑅))
226221, 221, 32mulassd 10060 . . . . . . . . . . . . 13 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → (((-1↑𝑅) · (-1↑𝑅)) · 𝑅) = ((-1↑𝑅) · ((-1↑𝑅) · 𝑅)))
22732mulid2d 10055 . . . . . . . . . . . . 13 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → (1 · 𝑅) = 𝑅)
228225, 226, 2273eqtr3d 2663 . . . . . . . . . . . 12 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → ((-1↑𝑅) · ((-1↑𝑅) · 𝑅)) = 𝑅)
229228breq2d 4663 . . . . . . . . . . 11 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → (𝑃 ∥ ((-1↑𝑅) · ((-1↑𝑅) · 𝑅)) ↔ 𝑃𝑅))
230208, 229mtbird 315 . . . . . . . . . 10 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → ¬ 𝑃 ∥ ((-1↑𝑅) · ((-1↑𝑅) · 𝑅)))
231 dvdsmultr2 15015 . . . . . . . . . . 11 ((𝑃 ∈ ℤ ∧ (-1↑𝑅) ∈ ℤ ∧ ((-1↑𝑅) · 𝑅) ∈ ℤ) → (𝑃 ∥ ((-1↑𝑅) · 𝑅) → 𝑃 ∥ ((-1↑𝑅) · ((-1↑𝑅) · 𝑅))))
23299, 203, 204, 231syl3anc 1325 . . . . . . . . . 10 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → (𝑃 ∥ ((-1↑𝑅) · 𝑅) → 𝑃 ∥ ((-1↑𝑅) · ((-1↑𝑅) · 𝑅))))
233230, 232mtod 189 . . . . . . . . 9 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → ¬ 𝑃 ∥ ((-1↑𝑅) · 𝑅))
234 dvdsval3 14981 . . . . . . . . . 10 ((𝑃 ∈ ℕ ∧ ((-1↑𝑅) · 𝑅) ∈ ℤ) → (𝑃 ∥ ((-1↑𝑅) · 𝑅) ↔ (((-1↑𝑅) · 𝑅) mod 𝑃) = 0))
23525, 204, 234syl2anc 693 . . . . . . . . 9 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → (𝑃 ∥ ((-1↑𝑅) · 𝑅) ↔ (((-1↑𝑅) · 𝑅) mod 𝑃) = 0))
236233, 235mtbid 314 . . . . . . . 8 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → ¬ (((-1↑𝑅) · 𝑅) mod 𝑃) = 0)
237 elnn0 11291 . . . . . . . . . 10 ((((-1↑𝑅) · 𝑅) mod 𝑃) ∈ ℕ0 ↔ ((((-1↑𝑅) · 𝑅) mod 𝑃) ∈ ℕ ∨ (((-1↑𝑅) · 𝑅) mod 𝑃) = 0))
238205, 237sylib 208 . . . . . . . . 9 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → ((((-1↑𝑅) · 𝑅) mod 𝑃) ∈ ℕ ∨ (((-1↑𝑅) · 𝑅) mod 𝑃) = 0))
239238ord 392 . . . . . . . 8 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → (¬ (((-1↑𝑅) · 𝑅) mod 𝑃) ∈ ℕ → (((-1↑𝑅) · 𝑅) mod 𝑃) = 0))
240236, 239mt3d 140 . . . . . . 7 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → (((-1↑𝑅) · 𝑅) mod 𝑃) ∈ ℕ)
241240nngt0d 11061 . . . . . 6 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → 0 < (((-1↑𝑅) · 𝑅) mod 𝑃))
242206, 92, 241, 94divgt0d 10956 . . . . 5 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → 0 < ((((-1↑𝑅) · 𝑅) mod 𝑃) / 2))
243 elnnz 11384 . . . . 5 (((((-1↑𝑅) · 𝑅) mod 𝑃) / 2) ∈ ℕ ↔ (((((-1↑𝑅) · 𝑅) mod 𝑃) / 2) ∈ ℤ ∧ 0 < ((((-1↑𝑅) · 𝑅) mod 𝑃) / 2)))
244201, 242, 243sylanbrc 698 . . . 4 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → ((((-1↑𝑅) · 𝑅) mod 𝑃) / 2) ∈ ℕ)
245244nnge1d 11060 . . 3 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → 1 ≤ ((((-1↑𝑅) · 𝑅) mod 𝑃) / 2))
246 zmodfz 12687 . . . . . 6 ((((-1↑𝑅) · 𝑅) ∈ ℤ ∧ 𝑃 ∈ ℕ) → (((-1↑𝑅) · 𝑅) mod 𝑃) ∈ (0...(𝑃 − 1)))
247204, 25, 246syl2anc 693 . . . . 5 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → (((-1↑𝑅) · 𝑅) mod 𝑃) ∈ (0...(𝑃 − 1)))
248 elfzle2 12342 . . . . 5 ((((-1↑𝑅) · 𝑅) mod 𝑃) ∈ (0...(𝑃 − 1)) → (((-1↑𝑅) · 𝑅) mod 𝑃) ≤ (𝑃 − 1))
249247, 248syl 17 . . . 4 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → (((-1↑𝑅) · 𝑅) mod 𝑃) ≤ (𝑃 − 1))
250 lediv1 10885 . . . . 5 (((((-1↑𝑅) · 𝑅) mod 𝑃) ∈ ℝ ∧ (𝑃 − 1) ∈ ℝ ∧ (2 ∈ ℝ ∧ 0 < 2)) → ((((-1↑𝑅) · 𝑅) mod 𝑃) ≤ (𝑃 − 1) ↔ ((((-1↑𝑅) · 𝑅) mod 𝑃) / 2) ≤ ((𝑃 − 1) / 2)))
251206, 90, 92, 94, 250syl112anc 1329 . . . 4 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → ((((-1↑𝑅) · 𝑅) mod 𝑃) ≤ (𝑃 − 1) ↔ ((((-1↑𝑅) · 𝑅) mod 𝑃) / 2) ≤ ((𝑃 − 1) / 2)))
252249, 251mpbid 222 . . 3 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → ((((-1↑𝑅) · 𝑅) mod 𝑃) / 2) ≤ ((𝑃 − 1) / 2))
253 elfz 12329 . . . 4 ((((((-1↑𝑅) · 𝑅) mod 𝑃) / 2) ∈ ℤ ∧ 1 ∈ ℤ ∧ ((𝑃 − 1) / 2) ∈ ℤ) → (((((-1↑𝑅) · 𝑅) mod 𝑃) / 2) ∈ (1...((𝑃 − 1) / 2)) ↔ (1 ≤ ((((-1↑𝑅) · 𝑅) mod 𝑃) / 2) ∧ ((((-1↑𝑅) · 𝑅) mod 𝑃) / 2) ≤ ((𝑃 − 1) / 2))))
254201, 71, 192, 253syl3anc 1325 . . 3 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → (((((-1↑𝑅) · 𝑅) mod 𝑃) / 2) ∈ (1...((𝑃 − 1) / 2)) ↔ (1 ≤ ((((-1↑𝑅) · 𝑅) mod 𝑃) / 2) ∧ ((((-1↑𝑅) · 𝑅) mod 𝑃) / 2) ≤ ((𝑃 − 1) / 2))))
255245, 252, 254mpbir2and 957 . 2 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → ((((-1↑𝑅) · 𝑅) mod 𝑃) / 2) ∈ (1...((𝑃 − 1) / 2)))
256 lgseisen.5 . 2 𝑀 = (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ ((((-1↑𝑅) · 𝑅) mod 𝑃) / 2))
257255, 256fmptd 6383 1 (𝜑𝑀:(1...((𝑃 − 1) / 2))⟶(1...((𝑃 − 1) / 2)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wo 383  wa 384   = wceq 1482  wcel 1989  wne 2793  cdif 3569  {csn 4175   class class class wbr 4651  cmpt 4727  wf 5882  cfv 5886  (class class class)co 6647  cc 9931  cr 9932  0cc0 9933  1c1 9934   + caddc 9936   · cmul 9938   < clt 10071  cle 10072  cmin 10263  -cneg 10264   / cdiv 10681  cn 11017  2c2 11067  0cn0 11289  cz 11374  cuz 11684  +crp 11829  ...cfz 12323   mod cmo 12663  cexp 12855  cdvds 14977   gcd cgcd 15210  cprime 15379
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1721  ax-4 1736  ax-5 1838  ax-6 1887  ax-7 1934  ax-8 1991  ax-9 1998  ax-10 2018  ax-11 2033  ax-12 2046  ax-13 2245  ax-ext 2601  ax-sep 4779  ax-nul 4787  ax-pow 4841  ax-pr 4904  ax-un 6946  ax-cnex 9989  ax-resscn 9990  ax-1cn 9991  ax-icn 9992  ax-addcl 9993  ax-addrcl 9994  ax-mulcl 9995  ax-mulrcl 9996  ax-mulcom 9997  ax-addass 9998  ax-mulass 9999  ax-distr 10000  ax-i2m1 10001  ax-1ne0 10002  ax-1rid 10003  ax-rnegex 10004  ax-rrecex 10005  ax-cnre 10006  ax-pre-lttri 10007  ax-pre-lttrn 10008  ax-pre-ltadd 10009  ax-pre-mulgt0 10010  ax-pre-sup 10011
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1038  df-3an 1039  df-tru 1485  df-ex 1704  df-nf 1709  df-sb 1880  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2752  df-ne 2794  df-nel 2897  df-ral 2916  df-rex 2917  df-reu 2918  df-rmo 2919  df-rab 2920  df-v 3200  df-sbc 3434  df-csb 3532  df-dif 3575  df-un 3577  df-in 3579  df-ss 3586  df-pss 3588  df-nul 3914  df-if 4085  df-pw 4158  df-sn 4176  df-pr 4178  df-tp 4180  df-op 4182  df-uni 4435  df-int 4474  df-iun 4520  df-br 4652  df-opab 4711  df-mpt 4728  df-tr 4751  df-id 5022  df-eprel 5027  df-po 5033  df-so 5034  df-fr 5071  df-we 5073  df-xp 5118  df-rel 5119  df-cnv 5120  df-co 5121  df-dm 5122  df-rn 5123  df-res 5124  df-ima 5125  df-pred 5678  df-ord 5724  df-on 5725  df-lim 5726  df-suc 5727  df-iota 5849  df-fun 5888  df-fn 5889  df-f 5890  df-f1 5891  df-fo 5892  df-f1o 5893  df-fv 5894  df-riota 6608  df-ov 6650  df-oprab 6651  df-mpt2 6652  df-om 7063  df-1st 7165  df-2nd 7166  df-wrecs 7404  df-recs 7465  df-rdg 7503  df-1o 7557  df-2o 7558  df-oadd 7561  df-er 7739  df-en 7953  df-dom 7954  df-sdom 7955  df-fin 7956  df-sup 8345  df-inf 8346  df-pnf 10073  df-mnf 10074  df-xr 10075  df-ltxr 10076  df-le 10077  df-sub 10265  df-neg 10266  df-div 10682  df-nn 11018  df-2 11076  df-3 11077  df-n0 11290  df-z 11375  df-uz 11685  df-rp 11830  df-fz 12324  df-fl 12588  df-mod 12664  df-seq 12797  df-exp 12856  df-cj 13833  df-re 13834  df-im 13835  df-sqrt 13969  df-abs 13970  df-dvds 14978  df-gcd 15211  df-prm 15380
This theorem is referenced by:  lgseisenlem2  25095  lgseisenlem3  25096
  Copyright terms: Public domain W3C validator