Metamath Proof Explorer

Theorem lgseisenlem1

Description: Lemma for lgseisen . If R ( u ) = ( Q x. u ) mod P and M ( u ) = ( -u 1 ^ R ( u ) ) x. R ( u ) , then for any even 1 <_ u <_ P - 1 , M ( u ) is also an even integer 1 <_ M ( u ) <_ P - 1 . To simplify these statements, we divide all the even numbers by 2 , so that it becomes the statement that M ( x / 2 ) = ( -u 1 ^ R ( x / 2 ) ) x. R ( x / 2 ) / 2 is an integer between 1 and ( P - 1 ) / 2 . (Contributed by Mario Carneiro, 17-Jun-2015)

Ref Expression
Hypotheses lgseisen.1 ⊢ ( 𝜑 → 𝑃 ∈ ( ℙ ∖ { 2 } ) )
lgseisen.2 ⊢ ( 𝜑 → 𝑄 ∈ ( ℙ ∖ { 2 } ) )
lgseisen.3 ⊢ ( 𝜑 → 𝑃 ≠ 𝑄 )
lgseisen.4 ⊢ 𝑅 = ( ( 𝑄 · ( 2 · 𝑥 ) ) mod 𝑃 )
lgseisen.5 ⊢ 𝑀 = ( 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ↦ ( ( ( ( - 1 ↑ 𝑅 ) · 𝑅 ) mod 𝑃 ) / 2 ) )
Assertion lgseisenlem1 ( 𝜑 → 𝑀 : ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ⟶ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) )

Proof

Step Hyp Ref Expression
1 lgseisen.1 ⊢ ( 𝜑 → 𝑃 ∈ ( ℙ ∖ { 2 } ) )
2 lgseisen.2 ⊢ ( 𝜑 → 𝑄 ∈ ( ℙ ∖ { 2 } ) )
3 lgseisen.3 ⊢ ( 𝜑 → 𝑃 ≠ 𝑄 )
4 lgseisen.4 ⊢ 𝑅 = ( ( 𝑄 · ( 2 · 𝑥 ) ) mod 𝑃 )
5 lgseisen.5 ⊢ 𝑀 = ( 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ↦ ( ( ( ( - 1 ↑ 𝑅 ) · 𝑅 ) mod 𝑃 ) / 2 ) )
6 neg1cn ⊢ - 1 ∈ ℂ
7 6 a1i ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ∧ ( 𝑅 / 2 ) ∈ ℤ ) → - 1 ∈ ℂ )
8 neg1ne0 ⊢ - 1 ≠ 0
9 8 a1i ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ∧ ( 𝑅 / 2 ) ∈ ℤ ) → - 1 ≠ 0 )
10 2z ⊢ 2 ∈ ℤ
11 10 a1i ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ∧ ( 𝑅 / 2 ) ∈ ℤ ) → 2 ∈ ℤ )
12 simpr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ∧ ( 𝑅 / 2 ) ∈ ℤ ) → ( 𝑅 / 2 ) ∈ ℤ )
13 expmulz ⊢ ( ( ( - 1 ∈ ℂ ∧ - 1 ≠ 0 ) ∧ ( 2 ∈ ℤ ∧ ( 𝑅 / 2 ) ∈ ℤ ) ) → ( - 1 ↑ ( 2 · ( 𝑅 / 2 ) ) ) = ( ( - 1 ↑ 2 ) ↑ ( 𝑅 / 2 ) ) )
14 7 9 11 12 13 syl22anc ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ∧ ( 𝑅 / 2 ) ∈ ℤ ) → ( - 1 ↑ ( 2 · ( 𝑅 / 2 ) ) ) = ( ( - 1 ↑ 2 ) ↑ ( 𝑅 / 2 ) ) )
15 2 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) → 𝑄 ∈ ( ℙ ∖ { 2 } ) )
16 15 eldifad ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) → 𝑄 ∈ ℙ )
17 prmz ⊢ ( 𝑄 ∈ ℙ → 𝑄 ∈ ℤ )
18 16 17 syl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) → 𝑄 ∈ ℤ )
19 elfzelz ⊢ ( 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) → 𝑥 ∈ ℤ )
20 19 adantl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) → 𝑥 ∈ ℤ )
21 zmulcl ⊢ ( ( 2 ∈ ℤ ∧ 𝑥 ∈ ℤ ) → ( 2 · 𝑥 ) ∈ ℤ )
22 10 20 21 sylancr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) → ( 2 · 𝑥 ) ∈ ℤ )
23 18 22 zmulcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) → ( 𝑄 · ( 2 · 𝑥 ) ) ∈ ℤ )
24 1 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) → 𝑃 ∈ ( ℙ ∖ { 2 } ) )
25 24 eldifad ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) → 𝑃 ∈ ℙ )
26 prmnn ⊢ ( 𝑃 ∈ ℙ → 𝑃 ∈ ℕ )
27 25 26 syl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) → 𝑃 ∈ ℕ )
28 zmodfz ⊢ ( ( ( 𝑄 · ( 2 · 𝑥 ) ) ∈ ℤ ∧ 𝑃 ∈ ℕ ) → ( ( 𝑄 · ( 2 · 𝑥 ) ) mod 𝑃 ) ∈ ( 0 ... ( 𝑃 − 1 ) ) )
29 23 27 28 syl2anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) → ( ( 𝑄 · ( 2 · 𝑥 ) ) mod 𝑃 ) ∈ ( 0 ... ( 𝑃 − 1 ) ) )
30 4 29 eqeltrid ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) → 𝑅 ∈ ( 0 ... ( 𝑃 − 1 ) ) )
31 elfznn0 ⊢ ( 𝑅 ∈ ( 0 ... ( 𝑃 − 1 ) ) → 𝑅 ∈ ℕ0 )
32 30 31 syl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) → 𝑅 ∈ ℕ0 )
33 32 nn0zd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) → 𝑅 ∈ ℤ )
34 33 zcnd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) → 𝑅 ∈ ℂ )
35 34 adantr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ∧ ( 𝑅 / 2 ) ∈ ℤ ) → 𝑅 ∈ ℂ )
36 2cnd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ∧ ( 𝑅 / 2 ) ∈ ℤ ) → 2 ∈ ℂ )
37 2ne0 ⊢ 2 ≠ 0
38 37 a1i ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ∧ ( 𝑅 / 2 ) ∈ ℤ ) → 2 ≠ 0 )
39 35 36 38 divcan2d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ∧ ( 𝑅 / 2 ) ∈ ℤ ) → ( 2 · ( 𝑅 / 2 ) ) = 𝑅 )
40 39 oveq2d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ∧ ( 𝑅 / 2 ) ∈ ℤ ) → ( - 1 ↑ ( 2 · ( 𝑅 / 2 ) ) ) = ( - 1 ↑ 𝑅 ) )
41 neg1sqe1 ⊢ ( - 1 ↑ 2 ) = 1
42 41 oveq1i ⊢ ( ( - 1 ↑ 2 ) ↑ ( 𝑅 / 2 ) ) = ( 1 ↑ ( 𝑅 / 2 ) )
43 1exp ⊢ ( ( 𝑅 / 2 ) ∈ ℤ → ( 1 ↑ ( 𝑅 / 2 ) ) = 1 )
44 43 adantl ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ∧ ( 𝑅 / 2 ) ∈ ℤ ) → ( 1 ↑ ( 𝑅 / 2 ) ) = 1 )
45 42 44 syl5eq ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ∧ ( 𝑅 / 2 ) ∈ ℤ ) → ( ( - 1 ↑ 2 ) ↑ ( 𝑅 / 2 ) ) = 1 )
46 14 40 45 3eqtr3d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ∧ ( 𝑅 / 2 ) ∈ ℤ ) → ( - 1 ↑ 𝑅 ) = 1 )
47 46 oveq1d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ∧ ( 𝑅 / 2 ) ∈ ℤ ) → ( ( - 1 ↑ 𝑅 ) · 𝑅 ) = ( 1 · 𝑅 ) )
48 35 mulid2d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ∧ ( 𝑅 / 2 ) ∈ ℤ ) → ( 1 · 𝑅 ) = 𝑅 )
49 47 48 eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ∧ ( 𝑅 / 2 ) ∈ ℤ ) → ( ( - 1 ↑ 𝑅 ) · 𝑅 ) = 𝑅 )
50 49 oveq1d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ∧ ( 𝑅 / 2 ) ∈ ℤ ) → ( ( ( - 1 ↑ 𝑅 ) · 𝑅 ) mod 𝑃 ) = ( 𝑅 mod 𝑃 ) )
51 32 nn0red ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) → 𝑅 ∈ ℝ )
52 27 nnrpd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) → 𝑃 ∈ ℝ+ )
53 32 nn0ge0d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) → 0 ≤ 𝑅 )
54 23 zred ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) → ( 𝑄 · ( 2 · 𝑥 ) ) ∈ ℝ )
55 modlt ⊢ ( ( ( 𝑄 · ( 2 · 𝑥 ) ) ∈ ℝ ∧ 𝑃 ∈ ℝ+ ) → ( ( 𝑄 · ( 2 · 𝑥 ) ) mod 𝑃 ) < 𝑃 )
56 54 52 55 syl2anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) → ( ( 𝑄 · ( 2 · 𝑥 ) ) mod 𝑃 ) < 𝑃 )
57 4 56 eqbrtrid ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) → 𝑅 < 𝑃 )
58 modid ⊢ ( ( ( 𝑅 ∈ ℝ ∧ 𝑃 ∈ ℝ+ ) ∧ ( 0 ≤ 𝑅 ∧ 𝑅 < 𝑃 ) ) → ( 𝑅 mod 𝑃 ) = 𝑅 )
59 51 52 53 57 58 syl22anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) → ( 𝑅 mod 𝑃 ) = 𝑅 )
60 59 adantr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ∧ ( 𝑅 / 2 ) ∈ ℤ ) → ( 𝑅 mod 𝑃 ) = 𝑅 )
61 50 60 eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ∧ ( 𝑅 / 2 ) ∈ ℤ ) → ( ( ( - 1 ↑ 𝑅 ) · 𝑅 ) mod 𝑃 ) = 𝑅 )
62 61 oveq1d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ∧ ( 𝑅 / 2 ) ∈ ℤ ) → ( ( ( ( - 1 ↑ 𝑅 ) · 𝑅 ) mod 𝑃 ) / 2 ) = ( 𝑅 / 2 ) )
63 62 12 eqeltrd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ∧ ( 𝑅 / 2 ) ∈ ℤ ) → ( ( ( ( - 1 ↑ 𝑅 ) · 𝑅 ) mod 𝑃 ) / 2 ) ∈ ℤ )
64 27 nncnd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) → 𝑃 ∈ ℂ )
65 64 mulid2d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) → ( 1 · 𝑃 ) = 𝑃 )
66 65 oveq2d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) → ( - 𝑅 + ( 1 · 𝑃 ) ) = ( - 𝑅 + 𝑃 ) )
67 51 renegcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) → - 𝑅 ∈ ℝ )
68 67 recnd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) → - 𝑅 ∈ ℂ )
69 64 68 addcomd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) → ( 𝑃 + - 𝑅 ) = ( - 𝑅 + 𝑃 ) )
70 64 34 negsubd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) → ( 𝑃 + - 𝑅 ) = ( 𝑃 − 𝑅 ) )
71 66 69 70 3eqtr2d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) → ( - 𝑅 + ( 1 · 𝑃 ) ) = ( 𝑃 − 𝑅 ) )
72 71 oveq1d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) → ( ( - 𝑅 + ( 1 · 𝑃 ) ) mod 𝑃 ) = ( ( 𝑃 − 𝑅 ) mod 𝑃 ) )
73 1zzd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) → 1 ∈ ℤ )
74 modcyc ⊢ ( ( - 𝑅 ∈ ℝ ∧ 𝑃 ∈ ℝ+ ∧ 1 ∈ ℤ ) → ( ( - 𝑅 + ( 1 · 𝑃 ) ) mod 𝑃 ) = ( - 𝑅 mod 𝑃 ) )
75 67 52 73 74 syl3anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) → ( ( - 𝑅 + ( 1 · 𝑃 ) ) mod 𝑃 ) = ( - 𝑅 mod 𝑃 ) )
76 27 nnred ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) → 𝑃 ∈ ℝ )
77 76 51 resubcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) → ( 𝑃 − 𝑅 ) ∈ ℝ )
78 51 76 57 ltled ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) → 𝑅 ≤ 𝑃 )
79 76 51 subge0d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) → ( 0 ≤ ( 𝑃 − 𝑅 ) ↔ 𝑅 ≤ 𝑃 ) )
80 78 79 mpbird ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) → 0 ≤ ( 𝑃 − 𝑅 ) )
81 2nn ⊢ 2 ∈ ℕ
82 elfznn ⊢ ( 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) → 𝑥 ∈ ℕ )
83 82 adantl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) → 𝑥 ∈ ℕ )
84 nnmulcl ⊢ ( ( 2 ∈ ℕ ∧ 𝑥 ∈ ℕ ) → ( 2 · 𝑥 ) ∈ ℕ )
85 81 83 84 sylancr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) → ( 2 · 𝑥 ) ∈ ℕ )
86 elfzle2 ⊢ ( 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) → 𝑥 ≤ ( ( 𝑃 − 1 ) / 2 ) )
87 86 adantl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) → 𝑥 ≤ ( ( 𝑃 − 1 ) / 2 ) )
88 83 nnred ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) → 𝑥 ∈ ℝ )
89 prmuz2 ⊢ ( 𝑃 ∈ ℙ → 𝑃 ∈ ( ℤ≥ ‘ 2 ) )
90 uz2m1nn ⊢ ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) → ( 𝑃 − 1 ) ∈ ℕ )
91 25 89 90 3syl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) → ( 𝑃 − 1 ) ∈ ℕ )
92 91 nnred ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) → ( 𝑃 − 1 ) ∈ ℝ )
93 2re ⊢ 2 ∈ ℝ
94 93 a1i ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) → 2 ∈ ℝ )
95 2pos ⊢ 0 < 2
96 95 a1i ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) → 0 < 2 )
97 lemuldiv2 ⊢ ( ( 𝑥 ∈ ℝ ∧ ( 𝑃 − 1 ) ∈ ℝ ∧ ( 2 ∈ ℝ ∧ 0 < 2 ) ) → ( ( 2 · 𝑥 ) ≤ ( 𝑃 − 1 ) ↔ 𝑥 ≤ ( ( 𝑃 − 1 ) / 2 ) ) )
98 88 92 94 96 97 syl112anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) → ( ( 2 · 𝑥 ) ≤ ( 𝑃 − 1 ) ↔ 𝑥 ≤ ( ( 𝑃 − 1 ) / 2 ) ) )
99 87 98 mpbird ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) → ( 2 · 𝑥 ) ≤ ( 𝑃 − 1 ) )
100 prmz ⊢ ( 𝑃 ∈ ℙ → 𝑃 ∈ ℤ )
101 25 100 syl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) → 𝑃 ∈ ℤ )
102 peano2zm ⊢ ( 𝑃 ∈ ℤ → ( 𝑃 − 1 ) ∈ ℤ )
103 fznn ⊢ ( ( 𝑃 − 1 ) ∈ ℤ → ( ( 2 · 𝑥 ) ∈ ( 1 ... ( 𝑃 − 1 ) ) ↔ ( ( 2 · 𝑥 ) ∈ ℕ ∧ ( 2 · 𝑥 ) ≤ ( 𝑃 − 1 ) ) ) )
104 101 102 103 3syl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) → ( ( 2 · 𝑥 ) ∈ ( 1 ... ( 𝑃 − 1 ) ) ↔ ( ( 2 · 𝑥 ) ∈ ℕ ∧ ( 2 · 𝑥 ) ≤ ( 𝑃 − 1 ) ) ) )
105 85 99 104 mpbir2and ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) → ( 2 · 𝑥 ) ∈ ( 1 ... ( 𝑃 − 1 ) ) )
106 fzm1ndvds ⊢ ( ( 𝑃 ∈ ℕ ∧ ( 2 · 𝑥 ) ∈ ( 1 ... ( 𝑃 − 1 ) ) ) → ¬ 𝑃 ∥ ( 2 · 𝑥 ) )
107 27 105 106 syl2anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) → ¬ 𝑃 ∥ ( 2 · 𝑥 ) )
108 3 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) → 𝑃 ≠ 𝑄 )
109 prmrp ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑄 ∈ ℙ ) → ( ( 𝑃 gcd 𝑄 ) = 1 ↔ 𝑃 ≠ 𝑄 ) )
110 25 16 109 syl2anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) → ( ( 𝑃 gcd 𝑄 ) = 1 ↔ 𝑃 ≠ 𝑄 ) )
111 108 110 mpbird ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) → ( 𝑃 gcd 𝑄 ) = 1 )
112 coprmdvds ⊢ ( ( 𝑃 ∈ ℤ ∧ 𝑄 ∈ ℤ ∧ ( 2 · 𝑥 ) ∈ ℤ ) → ( ( 𝑃 ∥ ( 𝑄 · ( 2 · 𝑥 ) ) ∧ ( 𝑃 gcd 𝑄 ) = 1 ) → 𝑃 ∥ ( 2 · 𝑥 ) ) )
113 101 18 22 112 syl3anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) → ( ( 𝑃 ∥ ( 𝑄 · ( 2 · 𝑥 ) ) ∧ ( 𝑃 gcd 𝑄 ) = 1 ) → 𝑃 ∥ ( 2 · 𝑥 ) ) )
114 111 113 mpan2d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) → ( 𝑃 ∥ ( 𝑄 · ( 2 · 𝑥 ) ) → 𝑃 ∥ ( 2 · 𝑥 ) ) )
115 107 114 mtod ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) → ¬ 𝑃 ∥ ( 𝑄 · ( 2 · 𝑥 ) ) )
116 dvdsval3 ⊢ ( ( 𝑃 ∈ ℕ ∧ ( 𝑄 · ( 2 · 𝑥 ) ) ∈ ℤ ) → ( 𝑃 ∥ ( 𝑄 · ( 2 · 𝑥 ) ) ↔ ( ( 𝑄 · ( 2 · 𝑥 ) ) mod 𝑃 ) = 0 ) )
117 27 23 116 syl2anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) → ( 𝑃 ∥ ( 𝑄 · ( 2 · 𝑥 ) ) ↔ ( ( 𝑄 · ( 2 · 𝑥 ) ) mod 𝑃 ) = 0 ) )
118 115 117 mtbid ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) → ¬ ( ( 𝑄 · ( 2 · 𝑥 ) ) mod 𝑃 ) = 0 )
119 4 eqeq1i ⊢ ( 𝑅 = 0 ↔ ( ( 𝑄 · ( 2 · 𝑥 ) ) mod 𝑃 ) = 0 )
120 118 119 sylnibr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) → ¬ 𝑅 = 0 )
121 91 nnnn0d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) → ( 𝑃 − 1 ) ∈ ℕ0 )
122 nn0uz ⊢ ℕ0 = ( ℤ≥ ‘ 0 )
123 121 122 eleqtrdi ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) → ( 𝑃 − 1 ) ∈ ( ℤ≥ ‘ 0 ) )
124 elfzp12 ⊢ ( ( 𝑃 − 1 ) ∈ ( ℤ≥ ‘ 0 ) → ( 𝑅 ∈ ( 0 ... ( 𝑃 − 1 ) ) ↔ ( 𝑅 = 0 ∨ 𝑅 ∈ ( ( 0 + 1 ) ... ( 𝑃 − 1 ) ) ) ) )
125 123 124 syl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) → ( 𝑅 ∈ ( 0 ... ( 𝑃 − 1 ) ) ↔ ( 𝑅 = 0 ∨ 𝑅 ∈ ( ( 0 + 1 ) ... ( 𝑃 − 1 ) ) ) ) )
126 30 125 mpbid ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) → ( 𝑅 = 0 ∨ 𝑅 ∈ ( ( 0 + 1 ) ... ( 𝑃 − 1 ) ) ) )
127 126 ord ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) → ( ¬ 𝑅 = 0 → 𝑅 ∈ ( ( 0 + 1 ) ... ( 𝑃 − 1 ) ) ) )
128 120 127 mpd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) → 𝑅 ∈ ( ( 0 + 1 ) ... ( 𝑃 − 1 ) ) )
129 1e0p1 ⊢ 1 = ( 0 + 1 )
130 129 oveq1i ⊢ ( 1 ... ( 𝑃 − 1 ) ) = ( ( 0 + 1 ) ... ( 𝑃 − 1 ) )
131 128 130 eleqtrrdi ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) → 𝑅 ∈ ( 1 ... ( 𝑃 − 1 ) ) )
132 elfznn ⊢ ( 𝑅 ∈ ( 1 ... ( 𝑃 − 1 ) ) → 𝑅 ∈ ℕ )
133 131 132 syl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) → 𝑅 ∈ ℕ )
134 133 nnrpd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) → 𝑅 ∈ ℝ+ )
135 76 134 ltsubrpd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) → ( 𝑃 − 𝑅 ) < 𝑃 )
136 modid ⊢ ( ( ( ( 𝑃 − 𝑅 ) ∈ ℝ ∧ 𝑃 ∈ ℝ+ ) ∧ ( 0 ≤ ( 𝑃 − 𝑅 ) ∧ ( 𝑃 − 𝑅 ) < 𝑃 ) ) → ( ( 𝑃 − 𝑅 ) mod 𝑃 ) = ( 𝑃 − 𝑅 ) )
137 77 52 80 135 136 syl22anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) → ( ( 𝑃 − 𝑅 ) mod 𝑃 ) = ( 𝑃 − 𝑅 ) )
138 72 75 137 3eqtr3d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) → ( - 𝑅 mod 𝑃 ) = ( 𝑃 − 𝑅 ) )
139 138 adantr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ∧ ( ( 𝑅 + 1 ) / 2 ) ∈ ℤ ) → ( - 𝑅 mod 𝑃 ) = ( 𝑃 − 𝑅 ) )
140 ax-1cn ⊢ 1 ∈ ℂ
141 140 a1i ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ∧ ( ( 𝑅 + 1 ) / 2 ) ∈ ℤ ) → 1 ∈ ℂ )
142 133 adantr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ∧ ( ( 𝑅 + 1 ) / 2 ) ∈ ℤ ) → 𝑅 ∈ ℕ )
143 33 peano2zd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) → ( 𝑅 + 1 ) ∈ ℤ )
144 dvdsval2 ⊢ ( ( 2 ∈ ℤ ∧ 2 ≠ 0 ∧ ( 𝑅 + 1 ) ∈ ℤ ) → ( 2 ∥ ( 𝑅 + 1 ) ↔ ( ( 𝑅 + 1 ) / 2 ) ∈ ℤ ) )
145 10 37 143 144 mp3an12i ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) → ( 2 ∥ ( 𝑅 + 1 ) ↔ ( ( 𝑅 + 1 ) / 2 ) ∈ ℤ ) )
146 145 biimpar ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ∧ ( ( 𝑅 + 1 ) / 2 ) ∈ ℤ ) → 2 ∥ ( 𝑅 + 1 ) )
147 33 adantr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ∧ ( ( 𝑅 + 1 ) / 2 ) ∈ ℤ ) → 𝑅 ∈ ℤ )
148 81 a1i ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ∧ ( ( 𝑅 + 1 ) / 2 ) ∈ ℤ ) → 2 ∈ ℕ )
149 1lt2 ⊢ 1 < 2
150 149 a1i ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ∧ ( ( 𝑅 + 1 ) / 2 ) ∈ ℤ ) → 1 < 2 )
151 ndvdsp1 ⊢ ( ( 𝑅 ∈ ℤ ∧ 2 ∈ ℕ ∧ 1 < 2 ) → ( 2 ∥ 𝑅 → ¬ 2 ∥ ( 𝑅 + 1 ) ) )
152 147 148 150 151 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ∧ ( ( 𝑅 + 1 ) / 2 ) ∈ ℤ ) → ( 2 ∥ 𝑅 → ¬ 2 ∥ ( 𝑅 + 1 ) ) )
153 146 152 mt2d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ∧ ( ( 𝑅 + 1 ) / 2 ) ∈ ℤ ) → ¬ 2 ∥ 𝑅 )
154 oexpneg ⊢ ( ( 1 ∈ ℂ ∧ 𝑅 ∈ ℕ ∧ ¬ 2 ∥ 𝑅 ) → ( - 1 ↑ 𝑅 ) = - ( 1 ↑ 𝑅 ) )
155 141 142 153 154 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ∧ ( ( 𝑅 + 1 ) / 2 ) ∈ ℤ ) → ( - 1 ↑ 𝑅 ) = - ( 1 ↑ 𝑅 ) )
156 1exp ⊢ ( 𝑅 ∈ ℤ → ( 1 ↑ 𝑅 ) = 1 )
157 147 156 syl ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ∧ ( ( 𝑅 + 1 ) / 2 ) ∈ ℤ ) → ( 1 ↑ 𝑅 ) = 1 )
158 157 negeqd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ∧ ( ( 𝑅 + 1 ) / 2 ) ∈ ℤ ) → - ( 1 ↑ 𝑅 ) = - 1 )
159 155 158 eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ∧ ( ( 𝑅 + 1 ) / 2 ) ∈ ℤ ) → ( - 1 ↑ 𝑅 ) = - 1 )
160 159 oveq1d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ∧ ( ( 𝑅 + 1 ) / 2 ) ∈ ℤ ) → ( ( - 1 ↑ 𝑅 ) · 𝑅 ) = ( - 1 · 𝑅 ) )
161 34 adantr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ∧ ( ( 𝑅 + 1 ) / 2 ) ∈ ℤ ) → 𝑅 ∈ ℂ )
162 161 mulm1d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ∧ ( ( 𝑅 + 1 ) / 2 ) ∈ ℤ ) → ( - 1 · 𝑅 ) = - 𝑅 )
163 160 162 eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ∧ ( ( 𝑅 + 1 ) / 2 ) ∈ ℤ ) → ( ( - 1 ↑ 𝑅 ) · 𝑅 ) = - 𝑅 )
164 163 oveq1d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ∧ ( ( 𝑅 + 1 ) / 2 ) ∈ ℤ ) → ( ( ( - 1 ↑ 𝑅 ) · 𝑅 ) mod 𝑃 ) = ( - 𝑅 mod 𝑃 ) )
165 64 adantr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ∧ ( ( 𝑅 + 1 ) / 2 ) ∈ ℤ ) → 𝑃 ∈ ℂ )
166 165 161 141 pnpcan2d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ∧ ( ( 𝑅 + 1 ) / 2 ) ∈ ℤ ) → ( ( 𝑃 + 1 ) − ( 𝑅 + 1 ) ) = ( 𝑃 − 𝑅 ) )
167 139 164 166 3eqtr4d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ∧ ( ( 𝑅 + 1 ) / 2 ) ∈ ℤ ) → ( ( ( - 1 ↑ 𝑅 ) · 𝑅 ) mod 𝑃 ) = ( ( 𝑃 + 1 ) − ( 𝑅 + 1 ) ) )
168 167 oveq1d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ∧ ( ( 𝑅 + 1 ) / 2 ) ∈ ℤ ) → ( ( ( ( - 1 ↑ 𝑅 ) · 𝑅 ) mod 𝑃 ) / 2 ) = ( ( ( 𝑃 + 1 ) − ( 𝑅 + 1 ) ) / 2 ) )
169 peano2cn ⊢ ( 𝑃 ∈ ℂ → ( 𝑃 + 1 ) ∈ ℂ )
170 165 169 syl ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ∧ ( ( 𝑅 + 1 ) / 2 ) ∈ ℤ ) → ( 𝑃 + 1 ) ∈ ℂ )
171 peano2cn ⊢ ( 𝑅 ∈ ℂ → ( 𝑅 + 1 ) ∈ ℂ )
172 161 171 syl ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ∧ ( ( 𝑅 + 1 ) / 2 ) ∈ ℤ ) → ( 𝑅 + 1 ) ∈ ℂ )
173 2cnd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ∧ ( ( 𝑅 + 1 ) / 2 ) ∈ ℤ ) → 2 ∈ ℂ )
174 37 a1i ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ∧ ( ( 𝑅 + 1 ) / 2 ) ∈ ℤ ) → 2 ≠ 0 )
175 170 172 173 174 divsubdird ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ∧ ( ( 𝑅 + 1 ) / 2 ) ∈ ℤ ) → ( ( ( 𝑃 + 1 ) − ( 𝑅 + 1 ) ) / 2 ) = ( ( ( 𝑃 + 1 ) / 2 ) − ( ( 𝑅 + 1 ) / 2 ) ) )
176 168 175 eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ∧ ( ( 𝑅 + 1 ) / 2 ) ∈ ℤ ) → ( ( ( ( - 1 ↑ 𝑅 ) · 𝑅 ) mod 𝑃 ) / 2 ) = ( ( ( 𝑃 + 1 ) / 2 ) − ( ( 𝑅 + 1 ) / 2 ) ) )
177 165 141 173 subadd23d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ∧ ( ( 𝑅 + 1 ) / 2 ) ∈ ℤ ) → ( ( 𝑃 − 1 ) + 2 ) = ( 𝑃 + ( 2 − 1 ) ) )
178 2m1e1 ⊢ ( 2 − 1 ) = 1
179 178 oveq2i ⊢ ( 𝑃 + ( 2 − 1 ) ) = ( 𝑃 + 1 )
180 177 179 syl6req ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ∧ ( ( 𝑅 + 1 ) / 2 ) ∈ ℤ ) → ( 𝑃 + 1 ) = ( ( 𝑃 − 1 ) + 2 ) )
181 180 oveq1d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ∧ ( ( 𝑅 + 1 ) / 2 ) ∈ ℤ ) → ( ( 𝑃 + 1 ) / 2 ) = ( ( ( 𝑃 − 1 ) + 2 ) / 2 ) )
182 91 nncnd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) → ( 𝑃 − 1 ) ∈ ℂ )
183 182 adantr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ∧ ( ( 𝑅 + 1 ) / 2 ) ∈ ℤ ) → ( 𝑃 − 1 ) ∈ ℂ )
184 183 173 173 174 divdird ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ∧ ( ( 𝑅 + 1 ) / 2 ) ∈ ℤ ) → ( ( ( 𝑃 − 1 ) + 2 ) / 2 ) = ( ( ( 𝑃 − 1 ) / 2 ) + ( 2 / 2 ) ) )
185 2div2e1 ⊢ ( 2 / 2 ) = 1
186 185 oveq2i ⊢ ( ( ( 𝑃 − 1 ) / 2 ) + ( 2 / 2 ) ) = ( ( ( 𝑃 − 1 ) / 2 ) + 1 )
187 184 186 syl6eq ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ∧ ( ( 𝑅 + 1 ) / 2 ) ∈ ℤ ) → ( ( ( 𝑃 − 1 ) + 2 ) / 2 ) = ( ( ( 𝑃 − 1 ) / 2 ) + 1 ) )
188 181 187 eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ∧ ( ( 𝑅 + 1 ) / 2 ) ∈ ℤ ) → ( ( 𝑃 + 1 ) / 2 ) = ( ( ( 𝑃 − 1 ) / 2 ) + 1 ) )
189 oddprm ⊢ ( 𝑃 ∈ ( ℙ ∖ { 2 } ) → ( ( 𝑃 − 1 ) / 2 ) ∈ ℕ )
190 24 189 syl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) → ( ( 𝑃 − 1 ) / 2 ) ∈ ℕ )
191 190 nnzd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) → ( ( 𝑃 − 1 ) / 2 ) ∈ ℤ )
192 191 adantr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ∧ ( ( 𝑅 + 1 ) / 2 ) ∈ ℤ ) → ( ( 𝑃 − 1 ) / 2 ) ∈ ℤ )
193 192 peano2zd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ∧ ( ( 𝑅 + 1 ) / 2 ) ∈ ℤ ) → ( ( ( 𝑃 − 1 ) / 2 ) + 1 ) ∈ ℤ )
194 188 193 eqeltrd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ∧ ( ( 𝑅 + 1 ) / 2 ) ∈ ℤ ) → ( ( 𝑃 + 1 ) / 2 ) ∈ ℤ )
195 simpr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ∧ ( ( 𝑅 + 1 ) / 2 ) ∈ ℤ ) → ( ( 𝑅 + 1 ) / 2 ) ∈ ℤ )
196 194 195 zsubcld ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ∧ ( ( 𝑅 + 1 ) / 2 ) ∈ ℤ ) → ( ( ( 𝑃 + 1 ) / 2 ) − ( ( 𝑅 + 1 ) / 2 ) ) ∈ ℤ )
197 176 196 eqeltrd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ∧ ( ( 𝑅 + 1 ) / 2 ) ∈ ℤ ) → ( ( ( ( - 1 ↑ 𝑅 ) · 𝑅 ) mod 𝑃 ) / 2 ) ∈ ℤ )
198 zeo ⊢ ( 𝑅 ∈ ℤ → ( ( 𝑅 / 2 ) ∈ ℤ ∨ ( ( 𝑅 + 1 ) / 2 ) ∈ ℤ ) )
199 33 198 syl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) → ( ( 𝑅 / 2 ) ∈ ℤ ∨ ( ( 𝑅 + 1 ) / 2 ) ∈ ℤ ) )
200 63 197 199 mpjaodan ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) → ( ( ( ( - 1 ↑ 𝑅 ) · 𝑅 ) mod 𝑃 ) / 2 ) ∈ ℤ )
201 m1expcl ⊢ ( 𝑅 ∈ ℤ → ( - 1 ↑ 𝑅 ) ∈ ℤ )
202 33 201 syl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) → ( - 1 ↑ 𝑅 ) ∈ ℤ )
203 202 33 zmulcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) → ( ( - 1 ↑ 𝑅 ) · 𝑅 ) ∈ ℤ )
204 203 27 zmodcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) → ( ( ( - 1 ↑ 𝑅 ) · 𝑅 ) mod 𝑃 ) ∈ ℕ0 )
205 204 nn0red ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) → ( ( ( - 1 ↑ 𝑅 ) · 𝑅 ) mod 𝑃 ) ∈ ℝ )
206 fzm1ndvds ⊢ ( ( 𝑃 ∈ ℕ ∧ 𝑅 ∈ ( 1 ... ( 𝑃 − 1 ) ) ) → ¬ 𝑃 ∥ 𝑅 )
207 27 131 206 syl2anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) → ¬ 𝑃 ∥ 𝑅 )
208 ax-1ne0 ⊢ 1 ≠ 0
209 divneg2 ⊢ ( ( 1 ∈ ℂ ∧ 1 ∈ ℂ ∧ 1 ≠ 0 ) → - ( 1 / 1 ) = ( 1 / - 1 ) )
210 140 140 208 209 mp3an ⊢ - ( 1 / 1 ) = ( 1 / - 1 )
211 1div1e1 ⊢ ( 1 / 1 ) = 1
212 211 negeqi ⊢ - ( 1 / 1 ) = - 1
213 210 212 eqtr3i ⊢ ( 1 / - 1 ) = - 1
214 213 oveq1i ⊢ ( ( 1 / - 1 ) ↑ 𝑅 ) = ( - 1 ↑ 𝑅 )
215 6 a1i ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) → - 1 ∈ ℂ )
216 8 a1i ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) → - 1 ≠ 0 )
217 215 216 33 exprecd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) → ( ( 1 / - 1 ) ↑ 𝑅 ) = ( 1 / ( - 1 ↑ 𝑅 ) ) )
218 214 217 syl5eqr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) → ( - 1 ↑ 𝑅 ) = ( 1 / ( - 1 ↑ 𝑅 ) ) )
219 218 oveq2d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) → ( ( - 1 ↑ 𝑅 ) · ( - 1 ↑ 𝑅 ) ) = ( ( - 1 ↑ 𝑅 ) · ( 1 / ( - 1 ↑ 𝑅 ) ) ) )
220 202 zcnd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) → ( - 1 ↑ 𝑅 ) ∈ ℂ )
221 215 216 33 expne0d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) → ( - 1 ↑ 𝑅 ) ≠ 0 )
222 220 221 recidd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) → ( ( - 1 ↑ 𝑅 ) · ( 1 / ( - 1 ↑ 𝑅 ) ) ) = 1 )
223 219 222 eqtrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) → ( ( - 1 ↑ 𝑅 ) · ( - 1 ↑ 𝑅 ) ) = 1 )
224 223 oveq1d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) → ( ( ( - 1 ↑ 𝑅 ) · ( - 1 ↑ 𝑅 ) ) · 𝑅 ) = ( 1 · 𝑅 ) )
225 220 220 34 mulassd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) → ( ( ( - 1 ↑ 𝑅 ) · ( - 1 ↑ 𝑅 ) ) · 𝑅 ) = ( ( - 1 ↑ 𝑅 ) · ( ( - 1 ↑ 𝑅 ) · 𝑅 ) ) )
226 34 mulid2d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) → ( 1 · 𝑅 ) = 𝑅 )
227 224 225 226 3eqtr3d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) → ( ( - 1 ↑ 𝑅 ) · ( ( - 1 ↑ 𝑅 ) · 𝑅 ) ) = 𝑅 )
228 227 breq2d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) → ( 𝑃 ∥ ( ( - 1 ↑ 𝑅 ) · ( ( - 1 ↑ 𝑅 ) · 𝑅 ) ) ↔ 𝑃 ∥ 𝑅 ) )
229 207 228 mtbird ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) → ¬ 𝑃 ∥ ( ( - 1 ↑ 𝑅 ) · ( ( - 1 ↑ 𝑅 ) · 𝑅 ) ) )
230 dvdsmultr2 ⊢ ( ( 𝑃 ∈ ℤ ∧ ( - 1 ↑ 𝑅 ) ∈ ℤ ∧ ( ( - 1 ↑ 𝑅 ) · 𝑅 ) ∈ ℤ ) → ( 𝑃 ∥ ( ( - 1 ↑ 𝑅 ) · 𝑅 ) → 𝑃 ∥ ( ( - 1 ↑ 𝑅 ) · ( ( - 1 ↑ 𝑅 ) · 𝑅 ) ) ) )
231 101 202 203 230 syl3anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) → ( 𝑃 ∥ ( ( - 1 ↑ 𝑅 ) · 𝑅 ) → 𝑃 ∥ ( ( - 1 ↑ 𝑅 ) · ( ( - 1 ↑ 𝑅 ) · 𝑅 ) ) ) )
232 229 231 mtod ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) → ¬ 𝑃 ∥ ( ( - 1 ↑ 𝑅 ) · 𝑅 ) )
233 dvdsval3 ⊢ ( ( 𝑃 ∈ ℕ ∧ ( ( - 1 ↑ 𝑅 ) · 𝑅 ) ∈ ℤ ) → ( 𝑃 ∥ ( ( - 1 ↑ 𝑅 ) · 𝑅 ) ↔ ( ( ( - 1 ↑ 𝑅 ) · 𝑅 ) mod 𝑃 ) = 0 ) )
234 27 203 233 syl2anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) → ( 𝑃 ∥ ( ( - 1 ↑ 𝑅 ) · 𝑅 ) ↔ ( ( ( - 1 ↑ 𝑅 ) · 𝑅 ) mod 𝑃 ) = 0 ) )
235 232 234 mtbid ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) → ¬ ( ( ( - 1 ↑ 𝑅 ) · 𝑅 ) mod 𝑃 ) = 0 )
236 elnn0 ⊢ ( ( ( ( - 1 ↑ 𝑅 ) · 𝑅 ) mod 𝑃 ) ∈ ℕ0 ↔ ( ( ( ( - 1 ↑ 𝑅 ) · 𝑅 ) mod 𝑃 ) ∈ ℕ ∨ ( ( ( - 1 ↑ 𝑅 ) · 𝑅 ) mod 𝑃 ) = 0 ) )
237 204 236 sylib ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) → ( ( ( ( - 1 ↑ 𝑅 ) · 𝑅 ) mod 𝑃 ) ∈ ℕ ∨ ( ( ( - 1 ↑ 𝑅 ) · 𝑅 ) mod 𝑃 ) = 0 ) )
238 237 ord ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) → ( ¬ ( ( ( - 1 ↑ 𝑅 ) · 𝑅 ) mod 𝑃 ) ∈ ℕ → ( ( ( - 1 ↑ 𝑅 ) · 𝑅 ) mod 𝑃 ) = 0 ) )
239 235 238 mt3d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) → ( ( ( - 1 ↑ 𝑅 ) · 𝑅 ) mod 𝑃 ) ∈ ℕ )
240 239 nngt0d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) → 0 < ( ( ( - 1 ↑ 𝑅 ) · 𝑅 ) mod 𝑃 ) )
241 205 94 240 96 divgt0d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) → 0 < ( ( ( ( - 1 ↑ 𝑅 ) · 𝑅 ) mod 𝑃 ) / 2 ) )
242 elnnz ⊢ ( ( ( ( ( - 1 ↑ 𝑅 ) · 𝑅 ) mod 𝑃 ) / 2 ) ∈ ℕ ↔ ( ( ( ( ( - 1 ↑ 𝑅 ) · 𝑅 ) mod 𝑃 ) / 2 ) ∈ ℤ ∧ 0 < ( ( ( ( - 1 ↑ 𝑅 ) · 𝑅 ) mod 𝑃 ) / 2 ) ) )
243 200 241 242 sylanbrc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) → ( ( ( ( - 1 ↑ 𝑅 ) · 𝑅 ) mod 𝑃 ) / 2 ) ∈ ℕ )
244 243 nnge1d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) → 1 ≤ ( ( ( ( - 1 ↑ 𝑅 ) · 𝑅 ) mod 𝑃 ) / 2 ) )
245 zmodfz ⊢ ( ( ( ( - 1 ↑ 𝑅 ) · 𝑅 ) ∈ ℤ ∧ 𝑃 ∈ ℕ ) → ( ( ( - 1 ↑ 𝑅 ) · 𝑅 ) mod 𝑃 ) ∈ ( 0 ... ( 𝑃 − 1 ) ) )
246 203 27 245 syl2anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) → ( ( ( - 1 ↑ 𝑅 ) · 𝑅 ) mod 𝑃 ) ∈ ( 0 ... ( 𝑃 − 1 ) ) )
247 elfzle2 ⊢ ( ( ( ( - 1 ↑ 𝑅 ) · 𝑅 ) mod 𝑃 ) ∈ ( 0 ... ( 𝑃 − 1 ) ) → ( ( ( - 1 ↑ 𝑅 ) · 𝑅 ) mod 𝑃 ) ≤ ( 𝑃 − 1 ) )
248 246 247 syl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) → ( ( ( - 1 ↑ 𝑅 ) · 𝑅 ) mod 𝑃 ) ≤ ( 𝑃 − 1 ) )
249 lediv1 ⊢ ( ( ( ( ( - 1 ↑ 𝑅 ) · 𝑅 ) mod 𝑃 ) ∈ ℝ ∧ ( 𝑃 − 1 ) ∈ ℝ ∧ ( 2 ∈ ℝ ∧ 0 < 2 ) ) → ( ( ( ( - 1 ↑ 𝑅 ) · 𝑅 ) mod 𝑃 ) ≤ ( 𝑃 − 1 ) ↔ ( ( ( ( - 1 ↑ 𝑅 ) · 𝑅 ) mod 𝑃 ) / 2 ) ≤ ( ( 𝑃 − 1 ) / 2 ) ) )
250 205 92 94 96 249 syl112anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) → ( ( ( ( - 1 ↑ 𝑅 ) · 𝑅 ) mod 𝑃 ) ≤ ( 𝑃 − 1 ) ↔ ( ( ( ( - 1 ↑ 𝑅 ) · 𝑅 ) mod 𝑃 ) / 2 ) ≤ ( ( 𝑃 − 1 ) / 2 ) ) )
251 248 250 mpbid ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) → ( ( ( ( - 1 ↑ 𝑅 ) · 𝑅 ) mod 𝑃 ) / 2 ) ≤ ( ( 𝑃 − 1 ) / 2 ) )
252 elfz ⊢ ( ( ( ( ( ( - 1 ↑ 𝑅 ) · 𝑅 ) mod 𝑃 ) / 2 ) ∈ ℤ ∧ 1 ∈ ℤ ∧ ( ( 𝑃 − 1 ) / 2 ) ∈ ℤ ) → ( ( ( ( ( - 1 ↑ 𝑅 ) · 𝑅 ) mod 𝑃 ) / 2 ) ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ↔ ( 1 ≤ ( ( ( ( - 1 ↑ 𝑅 ) · 𝑅 ) mod 𝑃 ) / 2 ) ∧ ( ( ( ( - 1 ↑ 𝑅 ) · 𝑅 ) mod 𝑃 ) / 2 ) ≤ ( ( 𝑃 − 1 ) / 2 ) ) ) )
253 200 73 191 252 syl3anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) → ( ( ( ( ( - 1 ↑ 𝑅 ) · 𝑅 ) mod 𝑃 ) / 2 ) ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ↔ ( 1 ≤ ( ( ( ( - 1 ↑ 𝑅 ) · 𝑅 ) mod 𝑃 ) / 2 ) ∧ ( ( ( ( - 1 ↑ 𝑅 ) · 𝑅 ) mod 𝑃 ) / 2 ) ≤ ( ( 𝑃 − 1 ) / 2 ) ) ) )
254 244 251 253 mpbir2and ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) → ( ( ( ( - 1 ↑ 𝑅 ) · 𝑅 ) mod 𝑃 ) / 2 ) ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) )
255 254 5 fmptd ⊢ ( 𝜑 → 𝑀 : ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ⟶ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) )