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