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

Theorem lgseisenlem1 25878
Description: Lemma for lgseisen 25882. 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 11739 . . . . . . . . . . . . . . 15 -1 ∈ ℂ
21a1i 11 . . . . . . . . . . . . . 14 (((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) ∧ (𝑅 / 2) ∈ ℤ) → -1 ∈ ℂ)
3 neg1ne0 11741 . . . . . . . . . . . . . . 15 -1 ≠ 0
43a1i 11 . . . . . . . . . . . . . 14 (((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) ∧ (𝑅 / 2) ∈ ℤ) → -1 ≠ 0)
5 2z 12002 . . . . . . . . . . . . . . 15 2 ∈ ℤ
65a1i 11 . . . . . . . . . . . . . 14 (((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) ∧ (𝑅 / 2) ∈ ℤ) → 2 ∈ ℤ)
7 simpr 485 . . . . . . . . . . . . . 14 (((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) ∧ (𝑅 / 2) ∈ ℤ) → (𝑅 / 2) ∈ ℤ)
8 expmulz 13463 . . . . . . . . . . . . . 14 (((-1 ∈ ℂ ∧ -1 ≠ 0) ∧ (2 ∈ ℤ ∧ (𝑅 / 2) ∈ ℤ)) → (-1↑(2 · (𝑅 / 2))) = ((-1↑2)↑(𝑅 / 2)))
92, 4, 6, 7, 8syl22anc 834 . . . . . . . . . . . . 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 3945 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑄 ∈ ℙ)
14 prmz 16007 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑄 ∈ ℙ → 𝑄 ∈ ℤ)
1513, 14syl 17 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑄 ∈ ℤ)
16 elfzelz 12896 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑥 ∈ (1...((𝑃 − 1) / 2)) → 𝑥 ∈ ℤ)
1716adantl 482 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑥 ∈ ℤ)
18 zmulcl 12019 . . . . . . . . . . . . . . . . . . . . . . 23 ((2 ∈ ℤ ∧ 𝑥 ∈ ℤ) → (2 · 𝑥) ∈ ℤ)
195, 17, 18sylancr 587 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → (2 · 𝑥) ∈ ℤ)
2015, 19zmulcld 12081 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → (𝑄 · (2 · 𝑥)) ∈ ℤ)
21 lgseisen.1 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑𝑃 ∈ (ℙ ∖ {2}))
2221adantr 481 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑃 ∈ (ℙ ∖ {2}))
2322eldifad 3945 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑃 ∈ ℙ)
24 prmnn 16006 . . . . . . . . . . . . . . . . . . . . . 22 (𝑃 ∈ ℙ → 𝑃 ∈ ℕ)
2523, 24syl 17 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑃 ∈ ℕ)
26 zmodfz 13249 . . . . . . . . . . . . . . . . . . . . 21 (((𝑄 · (2 · 𝑥)) ∈ ℤ ∧ 𝑃 ∈ ℕ) → ((𝑄 · (2 · 𝑥)) mod 𝑃) ∈ (0...(𝑃 − 1)))
2720, 25, 26syl2anc 584 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → ((𝑄 · (2 · 𝑥)) mod 𝑃) ∈ (0...(𝑃 − 1)))
2810, 27eqeltrid 2914 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑅 ∈ (0...(𝑃 − 1)))
29 elfznn0 12988 . . . . . . . . . . . . . . . . . . 19 (𝑅 ∈ (0...(𝑃 − 1)) → 𝑅 ∈ ℕ0)
3028, 29syl 17 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑅 ∈ ℕ0)
3130nn0zd 12073 . . . . . . . . . . . . . . . . 17 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑅 ∈ ℤ)
3231zcnd 12076 . . . . . . . . . . . . . . . 16 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑅 ∈ ℂ)
3332adantr 481 . . . . . . . . . . . . . . 15 (((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) ∧ (𝑅 / 2) ∈ ℤ) → 𝑅 ∈ ℂ)
34 2cnd 11703 . . . . . . . . . . . . . . 15 (((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) ∧ (𝑅 / 2) ∈ ℤ) → 2 ∈ ℂ)
35 2ne0 11729 . . . . . . . . . . . . . . . 16 2 ≠ 0
3635a1i 11 . . . . . . . . . . . . . . 15 (((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) ∧ (𝑅 / 2) ∈ ℤ) → 2 ≠ 0)
3733, 34, 36divcan2d 11406 . . . . . . . . . . . . . 14 (((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) ∧ (𝑅 / 2) ∈ ℤ) → (2 · (𝑅 / 2)) = 𝑅)
3837oveq2d 7161 . . . . . . . . . . . . 13 (((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) ∧ (𝑅 / 2) ∈ ℤ) → (-1↑(2 · (𝑅 / 2))) = (-1↑𝑅))
39 neg1sqe1 13547 . . . . . . . . . . . . . . 15 (-1↑2) = 1
4039oveq1i 7155 . . . . . . . . . . . . . 14 ((-1↑2)↑(𝑅 / 2)) = (1↑(𝑅 / 2))
41 1exp 13446 . . . . . . . . . . . . . . 15 ((𝑅 / 2) ∈ ℤ → (1↑(𝑅 / 2)) = 1)
4241adantl 482 . . . . . . . . . . . . . 14 (((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) ∧ (𝑅 / 2) ∈ ℤ) → (1↑(𝑅 / 2)) = 1)
4340, 42syl5eq 2865 . . . . . . . . . . . . 13 (((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) ∧ (𝑅 / 2) ∈ ℤ) → ((-1↑2)↑(𝑅 / 2)) = 1)
449, 38, 433eqtr3d 2861 . . . . . . . . . . . 12 (((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) ∧ (𝑅 / 2) ∈ ℤ) → (-1↑𝑅) = 1)
4544oveq1d 7160 . . . . . . . . . . 11 (((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) ∧ (𝑅 / 2) ∈ ℤ) → ((-1↑𝑅) · 𝑅) = (1 · 𝑅))
4633mulid2d 10647 . . . . . . . . . . 11 (((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) ∧ (𝑅 / 2) ∈ ℤ) → (1 · 𝑅) = 𝑅)
4745, 46eqtrd 2853 . . . . . . . . . 10 (((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) ∧ (𝑅 / 2) ∈ ℤ) → ((-1↑𝑅) · 𝑅) = 𝑅)
4847oveq1d 7160 . . . . . . . . 9 (((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) ∧ (𝑅 / 2) ∈ ℤ) → (((-1↑𝑅) · 𝑅) mod 𝑃) = (𝑅 mod 𝑃))
4930nn0red 11944 . . . . . . . . . . 11 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑅 ∈ ℝ)
5025nnrpd 12417 . . . . . . . . . . 11 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑃 ∈ ℝ+)
5130nn0ge0d 11946 . . . . . . . . . . 11 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → 0 ≤ 𝑅)
5220zred 12075 . . . . . . . . . . . . 13 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → (𝑄 · (2 · 𝑥)) ∈ ℝ)
53 modlt 13236 . . . . . . . . . . . . 13 (((𝑄 · (2 · 𝑥)) ∈ ℝ ∧ 𝑃 ∈ ℝ+) → ((𝑄 · (2 · 𝑥)) mod 𝑃) < 𝑃)
5452, 50, 53syl2anc 584 . . . . . . . . . . . 12 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → ((𝑄 · (2 · 𝑥)) mod 𝑃) < 𝑃)
5510, 54eqbrtrid 5092 . . . . . . . . . . 11 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑅 < 𝑃)
56 modid 13252 . . . . . . . . . . 11 (((𝑅 ∈ ℝ ∧ 𝑃 ∈ ℝ+) ∧ (0 ≤ 𝑅𝑅 < 𝑃)) → (𝑅 mod 𝑃) = 𝑅)
5749, 50, 51, 55, 56syl22anc 834 . . . . . . . . . 10 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → (𝑅 mod 𝑃) = 𝑅)
5857adantr 481 . . . . . . . . 9 (((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) ∧ (𝑅 / 2) ∈ ℤ) → (𝑅 mod 𝑃) = 𝑅)
5948, 58eqtrd 2853 . . . . . . . 8 (((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) ∧ (𝑅 / 2) ∈ ℤ) → (((-1↑𝑅) · 𝑅) mod 𝑃) = 𝑅)
6059oveq1d 7160 . . . . . . 7 (((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) ∧ (𝑅 / 2) ∈ ℤ) → ((((-1↑𝑅) · 𝑅) mod 𝑃) / 2) = (𝑅 / 2))
6160, 7eqeltrd 2910 . . . . . 6 (((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) ∧ (𝑅 / 2) ∈ ℤ) → ((((-1↑𝑅) · 𝑅) mod 𝑃) / 2) ∈ ℤ)
6225nncnd 11642 . . . . . . . . . . . . . . . 16 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑃 ∈ ℂ)
6362mulid2d 10647 . . . . . . . . . . . . . . 15 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → (1 · 𝑃) = 𝑃)
6463oveq2d 7161 . . . . . . . . . . . . . 14 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → (-𝑅 + (1 · 𝑃)) = (-𝑅 + 𝑃))
6549renegcld 11055 . . . . . . . . . . . . . . . 16 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → -𝑅 ∈ ℝ)
6665recnd 10657 . . . . . . . . . . . . . . 15 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → -𝑅 ∈ ℂ)
6762, 66addcomd 10830 . . . . . . . . . . . . . 14 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → (𝑃 + -𝑅) = (-𝑅 + 𝑃))
6862, 32negsubd 10991 . . . . . . . . . . . . . 14 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → (𝑃 + -𝑅) = (𝑃𝑅))
6964, 67, 683eqtr2d 2859 . . . . . . . . . . . . 13 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → (-𝑅 + (1 · 𝑃)) = (𝑃𝑅))
7069oveq1d 7160 . . . . . . . . . . . 12 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → ((-𝑅 + (1 · 𝑃)) mod 𝑃) = ((𝑃𝑅) mod 𝑃))
71 1zzd 12001 . . . . . . . . . . . . 13 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → 1 ∈ ℤ)
72 modcyc 13262 . . . . . . . . . . . . 13 ((-𝑅 ∈ ℝ ∧ 𝑃 ∈ ℝ+ ∧ 1 ∈ ℤ) → ((-𝑅 + (1 · 𝑃)) mod 𝑃) = (-𝑅 mod 𝑃))
7365, 50, 71, 72syl3anc 1363 . . . . . . . . . . . 12 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → ((-𝑅 + (1 · 𝑃)) mod 𝑃) = (-𝑅 mod 𝑃))
7425nnred 11641 . . . . . . . . . . . . . 14 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑃 ∈ ℝ)
7574, 49resubcld 11056 . . . . . . . . . . . . 13 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → (𝑃𝑅) ∈ ℝ)
7649, 74, 55ltled 10776 . . . . . . . . . . . . . 14 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑅𝑃)
7774, 49subge0d 11218 . . . . . . . . . . . . . 14 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → (0 ≤ (𝑃𝑅) ↔ 𝑅𝑃))
7876, 77mpbird 258 . . . . . . . . . . . . 13 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → 0 ≤ (𝑃𝑅))
79 2nn 11698 . . . . . . . . . . . . . . . . . . . . . . . 24 2 ∈ ℕ
80 elfznn 12924 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑥 ∈ (1...((𝑃 − 1) / 2)) → 𝑥 ∈ ℕ)
8180adantl 482 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑥 ∈ ℕ)
82 nnmulcl 11649 . . . . . . . . . . . . . . . . . . . . . . . 24 ((2 ∈ ℕ ∧ 𝑥 ∈ ℕ) → (2 · 𝑥) ∈ ℕ)
8379, 81, 82sylancr 587 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → (2 · 𝑥) ∈ ℕ)
84 elfzle2 12899 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑥 ∈ (1...((𝑃 − 1) / 2)) → 𝑥 ≤ ((𝑃 − 1) / 2))
8584adantl 482 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑥 ≤ ((𝑃 − 1) / 2))
8681nnred 11641 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑥 ∈ ℝ)
87 prmuz2 16028 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑃 ∈ ℙ → 𝑃 ∈ (ℤ‘2))
88 uz2m1nn 12311 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑃 ∈ (ℤ‘2) → (𝑃 − 1) ∈ ℕ)
8923, 87, 883syl 18 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → (𝑃 − 1) ∈ ℕ)
9089nnred 11641 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → (𝑃 − 1) ∈ ℝ)
91 2re 11699 . . . . . . . . . . . . . . . . . . . . . . . . . 26 2 ∈ ℝ
9291a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → 2 ∈ ℝ)
93 2pos 11728 . . . . . . . . . . . . . . . . . . . . . . . . . 26 0 < 2
9493a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → 0 < 2)
95 lemuldiv2 11509 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑥 ∈ ℝ ∧ (𝑃 − 1) ∈ ℝ ∧ (2 ∈ ℝ ∧ 0 < 2)) → ((2 · 𝑥) ≤ (𝑃 − 1) ↔ 𝑥 ≤ ((𝑃 − 1) / 2)))
9686, 90, 92, 94, 95syl112anc 1366 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → ((2 · 𝑥) ≤ (𝑃 − 1) ↔ 𝑥 ≤ ((𝑃 − 1) / 2)))
9785, 96mpbird 258 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → (2 · 𝑥) ≤ (𝑃 − 1))
98 prmz 16007 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑃 ∈ ℙ → 𝑃 ∈ ℤ)
9923, 98syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑃 ∈ ℤ)
100 peano2zm 12013 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑃 ∈ ℤ → (𝑃 − 1) ∈ ℤ)
101 fznn 12963 . . . . . . . . . . . . . . . . . . . . . . . 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 709 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → (2 · 𝑥) ∈ (1...(𝑃 − 1)))
104 fzm1ndvds 15660 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑃 ∈ ℕ ∧ (2 · 𝑥) ∈ (1...(𝑃 − 1))) → ¬ 𝑃 ∥ (2 · 𝑥))
10525, 103, 104syl2anc 584 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → ¬ 𝑃 ∥ (2 · 𝑥))
106 lgseisen.3 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑𝑃𝑄)
107106adantr 481 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑃𝑄)
108 prmrp 16044 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑃 ∈ ℙ ∧ 𝑄 ∈ ℙ) → ((𝑃 gcd 𝑄) = 1 ↔ 𝑃𝑄))
10923, 13, 108syl2anc 584 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → ((𝑃 gcd 𝑄) = 1 ↔ 𝑃𝑄))
110107, 109mpbird 258 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → (𝑃 gcd 𝑄) = 1)
111 coprmdvds 15985 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑃 ∈ ℤ ∧ 𝑄 ∈ ℤ ∧ (2 · 𝑥) ∈ ℤ) → ((𝑃 ∥ (𝑄 · (2 · 𝑥)) ∧ (𝑃 gcd 𝑄) = 1) → 𝑃 ∥ (2 · 𝑥)))
11299, 15, 19, 111syl3anc 1363 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → ((𝑃 ∥ (𝑄 · (2 · 𝑥)) ∧ (𝑃 gcd 𝑄) = 1) → 𝑃 ∥ (2 · 𝑥)))
113110, 112mpan2d 690 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → (𝑃 ∥ (𝑄 · (2 · 𝑥)) → 𝑃 ∥ (2 · 𝑥)))
114105, 113mtod 199 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → ¬ 𝑃 ∥ (𝑄 · (2 · 𝑥)))
115 dvdsval3 15599 . . . . . . . . . . . . . . . . . . . . 21 ((𝑃 ∈ ℕ ∧ (𝑄 · (2 · 𝑥)) ∈ ℤ) → (𝑃 ∥ (𝑄 · (2 · 𝑥)) ↔ ((𝑄 · (2 · 𝑥)) mod 𝑃) = 0))
11625, 20, 115syl2anc 584 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → (𝑃 ∥ (𝑄 · (2 · 𝑥)) ↔ ((𝑄 · (2 · 𝑥)) mod 𝑃) = 0))
117114, 116mtbid 325 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → ¬ ((𝑄 · (2 · 𝑥)) mod 𝑃) = 0)
11810eqeq1i 2823 . . . . . . . . . . . . . . . . . . 19 (𝑅 = 0 ↔ ((𝑄 · (2 · 𝑥)) mod 𝑃) = 0)
119117, 118sylnibr 330 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → ¬ 𝑅 = 0)
12089nnnn0d 11943 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → (𝑃 − 1) ∈ ℕ0)
121 nn0uz 12268 . . . . . . . . . . . . . . . . . . . . . 22 0 = (ℤ‘0)
122120, 121eleqtrdi 2920 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → (𝑃 − 1) ∈ (ℤ‘0))
123 elfzp12 12974 . . . . . . . . . . . . . . . . . . . . 21 ((𝑃 − 1) ∈ (ℤ‘0) → (𝑅 ∈ (0...(𝑃 − 1)) ↔ (𝑅 = 0 ∨ 𝑅 ∈ ((0 + 1)...(𝑃 − 1)))))
124122, 123syl 17 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → (𝑅 ∈ (0...(𝑃 − 1)) ↔ (𝑅 = 0 ∨ 𝑅 ∈ ((0 + 1)...(𝑃 − 1)))))
12528, 124mpbid 233 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → (𝑅 = 0 ∨ 𝑅 ∈ ((0 + 1)...(𝑃 − 1))))
126125ord 858 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → (¬ 𝑅 = 0 → 𝑅 ∈ ((0 + 1)...(𝑃 − 1))))
127119, 126mpd 15 . . . . . . . . . . . . . . . . 17 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑅 ∈ ((0 + 1)...(𝑃 − 1)))
128 1e0p1 12128 . . . . . . . . . . . . . . . . . 18 1 = (0 + 1)
129128oveq1i 7155 . . . . . . . . . . . . . . . . 17 (1...(𝑃 − 1)) = ((0 + 1)...(𝑃 − 1))
130127, 129eleqtrrdi 2921 . . . . . . . . . . . . . . . 16 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑅 ∈ (1...(𝑃 − 1)))
131 elfznn 12924 . . . . . . . . . . . . . . . 16 (𝑅 ∈ (1...(𝑃 − 1)) → 𝑅 ∈ ℕ)
132130, 131syl 17 . . . . . . . . . . . . . . 15 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑅 ∈ ℕ)
133132nnrpd 12417 . . . . . . . . . . . . . 14 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑅 ∈ ℝ+)
13474, 133ltsubrpd 12451 . . . . . . . . . . . . 13 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → (𝑃𝑅) < 𝑃)
135 modid 13252 . . . . . . . . . . . . 13 ((((𝑃𝑅) ∈ ℝ ∧ 𝑃 ∈ ℝ+) ∧ (0 ≤ (𝑃𝑅) ∧ (𝑃𝑅) < 𝑃)) → ((𝑃𝑅) mod 𝑃) = (𝑃𝑅))
13675, 50, 78, 134, 135syl22anc 834 . . . . . . . . . . . 12 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → ((𝑃𝑅) mod 𝑃) = (𝑃𝑅))
13770, 73, 1363eqtr3d 2861 . . . . . . . . . . 11 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → (-𝑅 mod 𝑃) = (𝑃𝑅))
138137adantr 481 . . . . . . . . . 10 (((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) ∧ ((𝑅 + 1) / 2) ∈ ℤ) → (-𝑅 mod 𝑃) = (𝑃𝑅))
139 ax-1cn 10583 . . . . . . . . . . . . . . . 16 1 ∈ ℂ
140139a1i 11 . . . . . . . . . . . . . . 15 (((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) ∧ ((𝑅 + 1) / 2) ∈ ℤ) → 1 ∈ ℂ)
141132adantr 481 . . . . . . . . . . . . . . 15 (((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) ∧ ((𝑅 + 1) / 2) ∈ ℤ) → 𝑅 ∈ ℕ)
14231peano2zd 12078 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → (𝑅 + 1) ∈ ℤ)
143 dvdsval2 15598 . . . . . . . . . . . . . . . . . 18 ((2 ∈ ℤ ∧ 2 ≠ 0 ∧ (𝑅 + 1) ∈ ℤ) → (2 ∥ (𝑅 + 1) ↔ ((𝑅 + 1) / 2) ∈ ℤ))
1445, 35, 142, 143mp3an12i 1456 . . . . . . . . . . . . . . . . 17 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → (2 ∥ (𝑅 + 1) ↔ ((𝑅 + 1) / 2) ∈ ℤ))
145144biimpar 478 . . . . . . . . . . . . . . . 16 (((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) ∧ ((𝑅 + 1) / 2) ∈ ℤ) → 2 ∥ (𝑅 + 1))
14631adantr 481 . . . . . . . . . . . . . . . . 17 (((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) ∧ ((𝑅 + 1) / 2) ∈ ℤ) → 𝑅 ∈ ℤ)
14779a1i 11 . . . . . . . . . . . . . . . . 17 (((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) ∧ ((𝑅 + 1) / 2) ∈ ℤ) → 2 ∈ ℕ)
148 1lt2 11796 . . . . . . . . . . . . . . . . . 18 1 < 2
149148a1i 11 . . . . . . . . . . . . . . . . 17 (((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) ∧ ((𝑅 + 1) / 2) ∈ ℤ) → 1 < 2)
150 ndvdsp1 15750 . . . . . . . . . . . . . . . . 17 ((𝑅 ∈ ℤ ∧ 2 ∈ ℕ ∧ 1 < 2) → (2 ∥ 𝑅 → ¬ 2 ∥ (𝑅 + 1)))
151146, 147, 149, 150syl3anc 1363 . . . . . . . . . . . . . . . 16 (((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) ∧ ((𝑅 + 1) / 2) ∈ ℤ) → (2 ∥ 𝑅 → ¬ 2 ∥ (𝑅 + 1)))
152145, 151mt2d 138 . . . . . . . . . . . . . . 15 (((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) ∧ ((𝑅 + 1) / 2) ∈ ℤ) → ¬ 2 ∥ 𝑅)
153 oexpneg 15682 . . . . . . . . . . . . . . 15 ((1 ∈ ℂ ∧ 𝑅 ∈ ℕ ∧ ¬ 2 ∥ 𝑅) → (-1↑𝑅) = -(1↑𝑅))
154140, 141, 152, 153syl3anc 1363 . . . . . . . . . . . . . 14 (((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) ∧ ((𝑅 + 1) / 2) ∈ ℤ) → (-1↑𝑅) = -(1↑𝑅))
155 1exp 13446 . . . . . . . . . . . . . . . 16 (𝑅 ∈ ℤ → (1↑𝑅) = 1)
156146, 155syl 17 . . . . . . . . . . . . . . 15 (((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) ∧ ((𝑅 + 1) / 2) ∈ ℤ) → (1↑𝑅) = 1)
157156negeqd 10868 . . . . . . . . . . . . . 14 (((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) ∧ ((𝑅 + 1) / 2) ∈ ℤ) → -(1↑𝑅) = -1)
158154, 157eqtrd 2853 . . . . . . . . . . . . 13 (((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) ∧ ((𝑅 + 1) / 2) ∈ ℤ) → (-1↑𝑅) = -1)
159158oveq1d 7160 . . . . . . . . . . . 12 (((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) ∧ ((𝑅 + 1) / 2) ∈ ℤ) → ((-1↑𝑅) · 𝑅) = (-1 · 𝑅))
16032adantr 481 . . . . . . . . . . . . 13 (((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) ∧ ((𝑅 + 1) / 2) ∈ ℤ) → 𝑅 ∈ ℂ)
161160mulm1d 11080 . . . . . . . . . . . 12 (((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) ∧ ((𝑅 + 1) / 2) ∈ ℤ) → (-1 · 𝑅) = -𝑅)
162159, 161eqtrd 2853 . . . . . . . . . . 11 (((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) ∧ ((𝑅 + 1) / 2) ∈ ℤ) → ((-1↑𝑅) · 𝑅) = -𝑅)
163162oveq1d 7160 . . . . . . . . . 10 (((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) ∧ ((𝑅 + 1) / 2) ∈ ℤ) → (((-1↑𝑅) · 𝑅) mod 𝑃) = (-𝑅 mod 𝑃))
16462adantr 481 . . . . . . . . . . 11 (((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) ∧ ((𝑅 + 1) / 2) ∈ ℤ) → 𝑃 ∈ ℂ)
165164, 160, 140pnpcan2d 11023 . . . . . . . . . 10 (((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) ∧ ((𝑅 + 1) / 2) ∈ ℤ) → ((𝑃 + 1) − (𝑅 + 1)) = (𝑃𝑅))
166138, 163, 1653eqtr4d 2863 . . . . . . . . 9 (((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) ∧ ((𝑅 + 1) / 2) ∈ ℤ) → (((-1↑𝑅) · 𝑅) mod 𝑃) = ((𝑃 + 1) − (𝑅 + 1)))
167166oveq1d 7160 . . . . . . . 8 (((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) ∧ ((𝑅 + 1) / 2) ∈ ℤ) → ((((-1↑𝑅) · 𝑅) mod 𝑃) / 2) = (((𝑃 + 1) − (𝑅 + 1)) / 2))
168 peano2cn 10800 . . . . . . . . . 10 (𝑃 ∈ ℂ → (𝑃 + 1) ∈ ℂ)
169164, 168syl 17 . . . . . . . . 9 (((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) ∧ ((𝑅 + 1) / 2) ∈ ℤ) → (𝑃 + 1) ∈ ℂ)
170 peano2cn 10800 . . . . . . . . . 10 (𝑅 ∈ ℂ → (𝑅 + 1) ∈ ℂ)
171160, 170syl 17 . . . . . . . . 9 (((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) ∧ ((𝑅 + 1) / 2) ∈ ℤ) → (𝑅 + 1) ∈ ℂ)
172 2cnd 11703 . . . . . . . . 9 (((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) ∧ ((𝑅 + 1) / 2) ∈ ℤ) → 2 ∈ ℂ)
17335a1i 11 . . . . . . . . 9 (((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) ∧ ((𝑅 + 1) / 2) ∈ ℤ) → 2 ≠ 0)
174169, 171, 172, 173divsubdird 11443 . . . . . . . 8 (((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) ∧ ((𝑅 + 1) / 2) ∈ ℤ) → (((𝑃 + 1) − (𝑅 + 1)) / 2) = (((𝑃 + 1) / 2) − ((𝑅 + 1) / 2)))
175167, 174eqtrd 2853 . . . . . . 7 (((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) ∧ ((𝑅 + 1) / 2) ∈ ℤ) → ((((-1↑𝑅) · 𝑅) mod 𝑃) / 2) = (((𝑃 + 1) / 2) − ((𝑅 + 1) / 2)))
176164, 140, 172subadd23d 11007 . . . . . . . . . . . 12 (((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) ∧ ((𝑅 + 1) / 2) ∈ ℤ) → ((𝑃 − 1) + 2) = (𝑃 + (2 − 1)))
177 2m1e1 11751 . . . . . . . . . . . . 13 (2 − 1) = 1
178177oveq2i 7156 . . . . . . . . . . . 12 (𝑃 + (2 − 1)) = (𝑃 + 1)
179176, 178syl6req 2870 . . . . . . . . . . 11 (((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) ∧ ((𝑅 + 1) / 2) ∈ ℤ) → (𝑃 + 1) = ((𝑃 − 1) + 2))
180179oveq1d 7160 . . . . . . . . . 10 (((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) ∧ ((𝑅 + 1) / 2) ∈ ℤ) → ((𝑃 + 1) / 2) = (((𝑃 − 1) + 2) / 2))
18189nncnd 11642 . . . . . . . . . . . . 13 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → (𝑃 − 1) ∈ ℂ)
182181adantr 481 . . . . . . . . . . . 12 (((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) ∧ ((𝑅 + 1) / 2) ∈ ℤ) → (𝑃 − 1) ∈ ℂ)
183182, 172, 172, 173divdird 11442 . . . . . . . . . . 11 (((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) ∧ ((𝑅 + 1) / 2) ∈ ℤ) → (((𝑃 − 1) + 2) / 2) = (((𝑃 − 1) / 2) + (2 / 2)))
184 2div2e1 11766 . . . . . . . . . . . 12 (2 / 2) = 1
185184oveq2i 7156 . . . . . . . . . . 11 (((𝑃 − 1) / 2) + (2 / 2)) = (((𝑃 − 1) / 2) + 1)
186183, 185syl6eq 2869 . . . . . . . . . 10 (((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) ∧ ((𝑅 + 1) / 2) ∈ ℤ) → (((𝑃 − 1) + 2) / 2) = (((𝑃 − 1) / 2) + 1))
187180, 186eqtrd 2853 . . . . . . . . 9 (((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) ∧ ((𝑅 + 1) / 2) ∈ ℤ) → ((𝑃 + 1) / 2) = (((𝑃 − 1) / 2) + 1))
188 oddprm 16135 . . . . . . . . . . . . 13 (𝑃 ∈ (ℙ ∖ {2}) → ((𝑃 − 1) / 2) ∈ ℕ)
18922, 188syl 17 . . . . . . . . . . . 12 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → ((𝑃 − 1) / 2) ∈ ℕ)
190189nnzd 12074 . . . . . . . . . . 11 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → ((𝑃 − 1) / 2) ∈ ℤ)
191190adantr 481 . . . . . . . . . 10 (((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) ∧ ((𝑅 + 1) / 2) ∈ ℤ) → ((𝑃 − 1) / 2) ∈ ℤ)
192191peano2zd 12078 . . . . . . . . 9 (((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) ∧ ((𝑅 + 1) / 2) ∈ ℤ) → (((𝑃 − 1) / 2) + 1) ∈ ℤ)
193187, 192eqeltrd 2910 . . . . . . . 8 (((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) ∧ ((𝑅 + 1) / 2) ∈ ℤ) → ((𝑃 + 1) / 2) ∈ ℤ)
194 simpr 485 . . . . . . . 8 (((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) ∧ ((𝑅 + 1) / 2) ∈ ℤ) → ((𝑅 + 1) / 2) ∈ ℤ)
195193, 194zsubcld 12080 . . . . . . 7 (((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) ∧ ((𝑅 + 1) / 2) ∈ ℤ) → (((𝑃 + 1) / 2) − ((𝑅 + 1) / 2)) ∈ ℤ)
196175, 195eqeltrd 2910 . . . . . 6 (((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) ∧ ((𝑅 + 1) / 2) ∈ ℤ) → ((((-1↑𝑅) · 𝑅) mod 𝑃) / 2) ∈ ℤ)
197 zeo 12056 . . . . . . 7 (𝑅 ∈ ℤ → ((𝑅 / 2) ∈ ℤ ∨ ((𝑅 + 1) / 2) ∈ ℤ))
19831, 197syl 17 . . . . . 6 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → ((𝑅 / 2) ∈ ℤ ∨ ((𝑅 + 1) / 2) ∈ ℤ))
19961, 196, 198mpjaodan 952 . . . . 5 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → ((((-1↑𝑅) · 𝑅) mod 𝑃) / 2) ∈ ℤ)
200 m1expcl 13440 . . . . . . . . . 10 (𝑅 ∈ ℤ → (-1↑𝑅) ∈ ℤ)
20131, 200syl 17 . . . . . . . . 9 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → (-1↑𝑅) ∈ ℤ)
202201, 31zmulcld 12081 . . . . . . . 8 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → ((-1↑𝑅) · 𝑅) ∈ ℤ)
203202, 25zmodcld 13248 . . . . . . 7 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → (((-1↑𝑅) · 𝑅) mod 𝑃) ∈ ℕ0)
204203nn0red 11944 . . . . . 6 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → (((-1↑𝑅) · 𝑅) mod 𝑃) ∈ ℝ)
205 fzm1ndvds 15660 . . . . . . . . . . . 12 ((𝑃 ∈ ℕ ∧ 𝑅 ∈ (1...(𝑃 − 1))) → ¬ 𝑃𝑅)
20625, 130, 205syl2anc 584 . . . . . . . . . . 11 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → ¬ 𝑃𝑅)
207 ax-1ne0 10594 . . . . . . . . . . . . . . . . . . . 20 1 ≠ 0
208 divneg2 11352 . . . . . . . . . . . . . . . . . . . 20 ((1 ∈ ℂ ∧ 1 ∈ ℂ ∧ 1 ≠ 0) → -(1 / 1) = (1 / -1))
209139, 139, 207, 208mp3an 1452 . . . . . . . . . . . . . . . . . . 19 -(1 / 1) = (1 / -1)
210 1div1e1 11318 . . . . . . . . . . . . . . . . . . . 20 (1 / 1) = 1
211210negeqi 10867 . . . . . . . . . . . . . . . . . . 19 -(1 / 1) = -1
212209, 211eqtr3i 2843 . . . . . . . . . . . . . . . . . 18 (1 / -1) = -1
213212oveq1i 7155 . . . . . . . . . . . . . . . . 17 ((1 / -1)↑𝑅) = (-1↑𝑅)
2141a1i 11 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → -1 ∈ ℂ)
2153a1i 11 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → -1 ≠ 0)
216214, 215, 31exprecd 13506 . . . . . . . . . . . . . . . . 17 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → ((1 / -1)↑𝑅) = (1 / (-1↑𝑅)))
217213, 216syl5eqr 2867 . . . . . . . . . . . . . . . 16 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → (-1↑𝑅) = (1 / (-1↑𝑅)))
218217oveq2d 7161 . . . . . . . . . . . . . . 15 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → ((-1↑𝑅) · (-1↑𝑅)) = ((-1↑𝑅) · (1 / (-1↑𝑅))))
219201zcnd 12076 . . . . . . . . . . . . . . . 16 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → (-1↑𝑅) ∈ ℂ)
220214, 215, 31expne0d 13504 . . . . . . . . . . . . . . . 16 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → (-1↑𝑅) ≠ 0)
221219, 220recidd 11399 . . . . . . . . . . . . . . 15 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → ((-1↑𝑅) · (1 / (-1↑𝑅))) = 1)
222218, 221eqtrd 2853 . . . . . . . . . . . . . 14 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → ((-1↑𝑅) · (-1↑𝑅)) = 1)
223222oveq1d 7160 . . . . . . . . . . . . 13 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → (((-1↑𝑅) · (-1↑𝑅)) · 𝑅) = (1 · 𝑅))
224219, 219, 32mulassd 10652 . . . . . . . . . . . . 13 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → (((-1↑𝑅) · (-1↑𝑅)) · 𝑅) = ((-1↑𝑅) · ((-1↑𝑅) · 𝑅)))
22532mulid2d 10647 . . . . . . . . . . . . 13 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → (1 · 𝑅) = 𝑅)
226223, 224, 2253eqtr3d 2861 . . . . . . . . . . . 12 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → ((-1↑𝑅) · ((-1↑𝑅) · 𝑅)) = 𝑅)
227226breq2d 5069 . . . . . . . . . . 11 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → (𝑃 ∥ ((-1↑𝑅) · ((-1↑𝑅) · 𝑅)) ↔ 𝑃𝑅))
228206, 227mtbird 326 . . . . . . . . . 10 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → ¬ 𝑃 ∥ ((-1↑𝑅) · ((-1↑𝑅) · 𝑅)))
229 dvdsmultr2 15637 . . . . . . . . . . 11 ((𝑃 ∈ ℤ ∧ (-1↑𝑅) ∈ ℤ ∧ ((-1↑𝑅) · 𝑅) ∈ ℤ) → (𝑃 ∥ ((-1↑𝑅) · 𝑅) → 𝑃 ∥ ((-1↑𝑅) · ((-1↑𝑅) · 𝑅))))
23099, 201, 202, 229syl3anc 1363 . . . . . . . . . 10 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → (𝑃 ∥ ((-1↑𝑅) · 𝑅) → 𝑃 ∥ ((-1↑𝑅) · ((-1↑𝑅) · 𝑅))))
231228, 230mtod 199 . . . . . . . . 9 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → ¬ 𝑃 ∥ ((-1↑𝑅) · 𝑅))
232 dvdsval3 15599 . . . . . . . . . 10 ((𝑃 ∈ ℕ ∧ ((-1↑𝑅) · 𝑅) ∈ ℤ) → (𝑃 ∥ ((-1↑𝑅) · 𝑅) ↔ (((-1↑𝑅) · 𝑅) mod 𝑃) = 0))
23325, 202, 232syl2anc 584 . . . . . . . . 9 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → (𝑃 ∥ ((-1↑𝑅) · 𝑅) ↔ (((-1↑𝑅) · 𝑅) mod 𝑃) = 0))
234231, 233mtbid 325 . . . . . . . 8 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → ¬ (((-1↑𝑅) · 𝑅) mod 𝑃) = 0)
235 elnn0 11887 . . . . . . . . . 10 ((((-1↑𝑅) · 𝑅) mod 𝑃) ∈ ℕ0 ↔ ((((-1↑𝑅) · 𝑅) mod 𝑃) ∈ ℕ ∨ (((-1↑𝑅) · 𝑅) mod 𝑃) = 0))
236203, 235sylib 219 . . . . . . . . 9 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → ((((-1↑𝑅) · 𝑅) mod 𝑃) ∈ ℕ ∨ (((-1↑𝑅) · 𝑅) mod 𝑃) = 0))
237236ord 858 . . . . . . . 8 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → (¬ (((-1↑𝑅) · 𝑅) mod 𝑃) ∈ ℕ → (((-1↑𝑅) · 𝑅) mod 𝑃) = 0))
238234, 237mt3d 150 . . . . . . 7 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → (((-1↑𝑅) · 𝑅) mod 𝑃) ∈ ℕ)
239238nngt0d 11674 . . . . . 6 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → 0 < (((-1↑𝑅) · 𝑅) mod 𝑃))
240204, 92, 239, 94divgt0d 11563 . . . . 5 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → 0 < ((((-1↑𝑅) · 𝑅) mod 𝑃) / 2))
241 elnnz 11979 . . . . 5 (((((-1↑𝑅) · 𝑅) mod 𝑃) / 2) ∈ ℕ ↔ (((((-1↑𝑅) · 𝑅) mod 𝑃) / 2) ∈ ℤ ∧ 0 < ((((-1↑𝑅) · 𝑅) mod 𝑃) / 2)))
242199, 240, 241sylanbrc 583 . . . 4 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → ((((-1↑𝑅) · 𝑅) mod 𝑃) / 2) ∈ ℕ)
243242nnge1d 11673 . . 3 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → 1 ≤ ((((-1↑𝑅) · 𝑅) mod 𝑃) / 2))
244 zmodfz 13249 . . . . . 6 ((((-1↑𝑅) · 𝑅) ∈ ℤ ∧ 𝑃 ∈ ℕ) → (((-1↑𝑅) · 𝑅) mod 𝑃) ∈ (0...(𝑃 − 1)))
245202, 25, 244syl2anc 584 . . . . 5 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → (((-1↑𝑅) · 𝑅) mod 𝑃) ∈ (0...(𝑃 − 1)))
246 elfzle2 12899 . . . . 5 ((((-1↑𝑅) · 𝑅) mod 𝑃) ∈ (0...(𝑃 − 1)) → (((-1↑𝑅) · 𝑅) mod 𝑃) ≤ (𝑃 − 1))
247245, 246syl 17 . . . 4 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → (((-1↑𝑅) · 𝑅) mod 𝑃) ≤ (𝑃 − 1))
248 lediv1 11493 . . . . 5 (((((-1↑𝑅) · 𝑅) mod 𝑃) ∈ ℝ ∧ (𝑃 − 1) ∈ ℝ ∧ (2 ∈ ℝ ∧ 0 < 2)) → ((((-1↑𝑅) · 𝑅) mod 𝑃) ≤ (𝑃 − 1) ↔ ((((-1↑𝑅) · 𝑅) mod 𝑃) / 2) ≤ ((𝑃 − 1) / 2)))
249204, 90, 92, 94, 248syl112anc 1366 . . . 4 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → ((((-1↑𝑅) · 𝑅) mod 𝑃) ≤ (𝑃 − 1) ↔ ((((-1↑𝑅) · 𝑅) mod 𝑃) / 2) ≤ ((𝑃 − 1) / 2)))
250247, 249mpbid 233 . . 3 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → ((((-1↑𝑅) · 𝑅) mod 𝑃) / 2) ≤ ((𝑃 − 1) / 2))
251 elfz 12886 . . . 4 ((((((-1↑𝑅) · 𝑅) mod 𝑃) / 2) ∈ ℤ ∧ 1 ∈ ℤ ∧ ((𝑃 − 1) / 2) ∈ ℤ) → (((((-1↑𝑅) · 𝑅) mod 𝑃) / 2) ∈ (1...((𝑃 − 1) / 2)) ↔ (1 ≤ ((((-1↑𝑅) · 𝑅) mod 𝑃) / 2) ∧ ((((-1↑𝑅) · 𝑅) mod 𝑃) / 2) ≤ ((𝑃 − 1) / 2))))
252199, 71, 190, 251syl3anc 1363 . . 3 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → (((((-1↑𝑅) · 𝑅) mod 𝑃) / 2) ∈ (1...((𝑃 − 1) / 2)) ↔ (1 ≤ ((((-1↑𝑅) · 𝑅) mod 𝑃) / 2) ∧ ((((-1↑𝑅) · 𝑅) mod 𝑃) / 2) ≤ ((𝑃 − 1) / 2))))
253243, 250, 252mpbir2and 709 . 2 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → ((((-1↑𝑅) · 𝑅) mod 𝑃) / 2) ∈ (1...((𝑃 − 1) / 2)))
254 lgseisen.5 . 2 𝑀 = (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ ((((-1↑𝑅) · 𝑅) mod 𝑃) / 2))
255253, 254fmptd 6870 1 (𝜑𝑀:(1...((𝑃 − 1) / 2))⟶(1...((𝑃 − 1) / 2)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 207  wa 396  wo 841   = wceq 1528  wcel 2105  wne 3013  cdif 3930  {csn 4557   class class class wbr 5057  cmpt 5137  wf 6344  cfv 6348  (class class class)co 7145  cc 10523  cr 10524  0cc0 10525  1c1 10526   + caddc 10528   · cmul 10530   < clt 10663  cle 10664  cmin 10858  -cneg 10859   / cdiv 11285  cn 11626  2c2 11680  0cn0 11885  cz 11969  cuz 12231  +crp 12377  ...cfz 12880   mod cmo 13225  cexp 13417  cdvds 15595   gcd cgcd 15831  cprime 16003
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2790  ax-sep 5194  ax-nul 5201  ax-pow 5257  ax-pr 5320  ax-un 7450  ax-cnex 10581  ax-resscn 10582  ax-1cn 10583  ax-icn 10584  ax-addcl 10585  ax-addrcl 10586  ax-mulcl 10587  ax-mulrcl 10588  ax-mulcom 10589  ax-addass 10590  ax-mulass 10591  ax-distr 10592  ax-i2m1 10593  ax-1ne0 10594  ax-1rid 10595  ax-rnegex 10596  ax-rrecex 10597  ax-cnre 10598  ax-pre-lttri 10599  ax-pre-lttrn 10600  ax-pre-ltadd 10601  ax-pre-mulgt0 10602  ax-pre-sup 10603
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-3or 1080  df-3an 1081  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-mo 2615  df-eu 2647  df-clab 2797  df-cleq 2811  df-clel 2890  df-nfc 2960  df-ne 3014  df-nel 3121  df-ral 3140  df-rex 3141  df-reu 3142  df-rmo 3143  df-rab 3144  df-v 3494  df-sbc 3770  df-csb 3881  df-dif 3936  df-un 3938  df-in 3940  df-ss 3949  df-pss 3951  df-nul 4289  df-if 4464  df-pw 4537  df-sn 4558  df-pr 4560  df-tp 4562  df-op 4564  df-uni 4831  df-iun 4912  df-br 5058  df-opab 5120  df-mpt 5138  df-tr 5164  df-id 5453  df-eprel 5458  df-po 5467  df-so 5468  df-fr 5507  df-we 5509  df-xp 5554  df-rel 5555  df-cnv 5556  df-co 5557  df-dm 5558  df-rn 5559  df-res 5560  df-ima 5561  df-pred 6141  df-ord 6187  df-on 6188  df-lim 6189  df-suc 6190  df-iota 6307  df-fun 6350  df-fn 6351  df-f 6352  df-f1 6353  df-fo 6354  df-f1o 6355  df-fv 6356  df-riota 7103  df-ov 7148  df-oprab 7149  df-mpo 7150  df-om 7570  df-1st 7678  df-2nd 7679  df-wrecs 7936  df-recs 7997  df-rdg 8035  df-1o 8091  df-2o 8092  df-er 8278  df-en 8498  df-dom 8499  df-sdom 8500  df-fin 8501  df-sup 8894  df-inf 8895  df-pnf 10665  df-mnf 10666  df-xr 10667  df-ltxr 10668  df-le 10669  df-sub 10860  df-neg 10861  df-div 11286  df-nn 11627  df-2 11688  df-3 11689  df-n0 11886  df-z 11970  df-uz 12232  df-rp 12378  df-fz 12881  df-fl 13150  df-mod 13226  df-seq 13358  df-exp 13418  df-cj 14446  df-re 14447  df-im 14448  df-sqrt 14582  df-abs 14583  df-dvds 15596  df-gcd 15832  df-prm 16004
This theorem is referenced by:  lgseisenlem2  25879  lgseisenlem3  25880
  Copyright terms: Public domain W3C validator