Metamath Proof Explorer

Theorem lgseisenlem2

Description: Lemma for lgseisen . The function M is an injection (and hence a bijection by the pigeonhole principle). (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 ) )
lgseisen.6 ⊢ 𝑆 = ( ( 𝑄 · ( 2 · 𝑦 ) ) mod 𝑃 )
Assertion lgseisenlem2 ( 𝜑 → 𝑀 : ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) –1-1-onto→ ( 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 lgseisen.6 ⊢ 𝑆 = ( ( 𝑄 · ( 2 · 𝑦 ) ) mod 𝑃 )
7 1 2 3 4 5 lgseisenlem1 ⊢ ( 𝜑 → 𝑀 : ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ⟶ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) )
8 oveq2 ⊢ ( 𝑥 = 𝑦 → ( 2 · 𝑥 ) = ( 2 · 𝑦 ) )
9 8 oveq2d ⊢ ( 𝑥 = 𝑦 → ( 𝑄 · ( 2 · 𝑥 ) ) = ( 𝑄 · ( 2 · 𝑦 ) ) )
10 9 oveq1d ⊢ ( 𝑥 = 𝑦 → ( ( 𝑄 · ( 2 · 𝑥 ) ) mod 𝑃 ) = ( ( 𝑄 · ( 2 · 𝑦 ) ) mod 𝑃 ) )
11 10 4 6 3eqtr4g ⊢ ( 𝑥 = 𝑦 → 𝑅 = 𝑆 )
12 11 oveq2d ⊢ ( 𝑥 = 𝑦 → ( - 1 ↑ 𝑅 ) = ( - 1 ↑ 𝑆 ) )
13 12 11 oveq12d ⊢ ( 𝑥 = 𝑦 → ( ( - 1 ↑ 𝑅 ) · 𝑅 ) = ( ( - 1 ↑ 𝑆 ) · 𝑆 ) )
14 13 oveq1d ⊢ ( 𝑥 = 𝑦 → ( ( ( - 1 ↑ 𝑅 ) · 𝑅 ) mod 𝑃 ) = ( ( ( - 1 ↑ 𝑆 ) · 𝑆 ) mod 𝑃 ) )
15 14 oveq1d ⊢ ( 𝑥 = 𝑦 → ( ( ( ( - 1 ↑ 𝑅 ) · 𝑅 ) mod 𝑃 ) / 2 ) = ( ( ( ( - 1 ↑ 𝑆 ) · 𝑆 ) mod 𝑃 ) / 2 ) )
16 ovex ⊢ ( ( ( ( - 1 ↑ 𝑆 ) · 𝑆 ) mod 𝑃 ) / 2 ) ∈ V
17 15 5 16 fvmpt ⊢ ( 𝑦 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) → ( 𝑀 ‘ 𝑦 ) = ( ( ( ( - 1 ↑ 𝑆 ) · 𝑆 ) mod 𝑃 ) / 2 ) )
18 17 ad2antrl ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ) → ( 𝑀 ‘ 𝑦 ) = ( ( ( ( - 1 ↑ 𝑆 ) · 𝑆 ) mod 𝑃 ) / 2 ) )
19 ovex ⊢ ( ( ( ( - 1 ↑ 𝑅 ) · 𝑅 ) mod 𝑃 ) / 2 ) ∈ V
20 5 fvmpt2 ⊢ ( ( 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ∧ ( ( ( ( - 1 ↑ 𝑅 ) · 𝑅 ) mod 𝑃 ) / 2 ) ∈ V ) → ( 𝑀 ‘ 𝑥 ) = ( ( ( ( - 1 ↑ 𝑅 ) · 𝑅 ) mod 𝑃 ) / 2 ) )
21 19 20 mpan2 ⊢ ( 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) → ( 𝑀 ‘ 𝑥 ) = ( ( ( ( - 1 ↑ 𝑅 ) · 𝑅 ) mod 𝑃 ) / 2 ) )
22 21 ad2antll ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ) → ( 𝑀 ‘ 𝑥 ) = ( ( ( ( - 1 ↑ 𝑅 ) · 𝑅 ) mod 𝑃 ) / 2 ) )
23 18 22 eqeq12d ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ) → ( ( 𝑀 ‘ 𝑦 ) = ( 𝑀 ‘ 𝑥 ) ↔ ( ( ( ( - 1 ↑ 𝑆 ) · 𝑆 ) mod 𝑃 ) / 2 ) = ( ( ( ( - 1 ↑ 𝑅 ) · 𝑅 ) mod 𝑃 ) / 2 ) ) )
24 2 adantr ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ) → 𝑄 ∈ ( ℙ ∖ { 2 } ) )
25 24 eldifad ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ) → 𝑄 ∈ ℙ )
26 prmz ⊢ ( 𝑄 ∈ ℙ → 𝑄 ∈ ℤ )
27 25 26 syl ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ) → 𝑄 ∈ ℤ )
28 2z ⊢ 2 ∈ ℤ
29 elfzelz ⊢ ( 𝑦 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) → 𝑦 ∈ ℤ )
30 29 ad2antrl ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ) → 𝑦 ∈ ℤ )
31 zmulcl ⊢ ( ( 2 ∈ ℤ ∧ 𝑦 ∈ ℤ ) → ( 2 · 𝑦 ) ∈ ℤ )
32 28 30 31 sylancr ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ) → ( 2 · 𝑦 ) ∈ ℤ )
33 27 32 zmulcld ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ) → ( 𝑄 · ( 2 · 𝑦 ) ) ∈ ℤ )
34 1 adantr ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ) → 𝑃 ∈ ( ℙ ∖ { 2 } ) )
35 34 eldifad ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ) → 𝑃 ∈ ℙ )
36 prmnn ⊢ ( 𝑃 ∈ ℙ → 𝑃 ∈ ℕ )
37 35 36 syl ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ) → 𝑃 ∈ ℕ )
38 33 37 zmodcld ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ) → ( ( 𝑄 · ( 2 · 𝑦 ) ) mod 𝑃 ) ∈ ℕ0 )
39 6 38 eqeltrid ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ) → 𝑆 ∈ ℕ0 )
40 39 nn0zd ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ) → 𝑆 ∈ ℤ )
41 m1expcl ⊢ ( 𝑆 ∈ ℤ → ( - 1 ↑ 𝑆 ) ∈ ℤ )
42 40 41 syl ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ) → ( - 1 ↑ 𝑆 ) ∈ ℤ )
43 42 40 zmulcld ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ) → ( ( - 1 ↑ 𝑆 ) · 𝑆 ) ∈ ℤ )
44 43 37 zmodcld ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ) → ( ( ( - 1 ↑ 𝑆 ) · 𝑆 ) mod 𝑃 ) ∈ ℕ0 )
45 44 nn0cnd ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ) → ( ( ( - 1 ↑ 𝑆 ) · 𝑆 ) mod 𝑃 ) ∈ ℂ )
46 elfzelz ⊢ ( 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) → 𝑥 ∈ ℤ )
47 46 ad2antll ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ) → 𝑥 ∈ ℤ )
48 zmulcl ⊢ ( ( 2 ∈ ℤ ∧ 𝑥 ∈ ℤ ) → ( 2 · 𝑥 ) ∈ ℤ )
49 28 47 48 sylancr ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ) → ( 2 · 𝑥 ) ∈ ℤ )
50 27 49 zmulcld ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ) → ( 𝑄 · ( 2 · 𝑥 ) ) ∈ ℤ )
51 50 37 zmodcld ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ) → ( ( 𝑄 · ( 2 · 𝑥 ) ) mod 𝑃 ) ∈ ℕ0 )
52 4 51 eqeltrid ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ) → 𝑅 ∈ ℕ0 )
53 52 nn0zd ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ) → 𝑅 ∈ ℤ )
54 m1expcl ⊢ ( 𝑅 ∈ ℤ → ( - 1 ↑ 𝑅 ) ∈ ℤ )
55 53 54 syl ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ) → ( - 1 ↑ 𝑅 ) ∈ ℤ )
56 55 53 zmulcld ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ) → ( ( - 1 ↑ 𝑅 ) · 𝑅 ) ∈ ℤ )
57 56 37 zmodcld ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ) → ( ( ( - 1 ↑ 𝑅 ) · 𝑅 ) mod 𝑃 ) ∈ ℕ0 )
58 57 nn0cnd ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ) → ( ( ( - 1 ↑ 𝑅 ) · 𝑅 ) mod 𝑃 ) ∈ ℂ )
59 2cnd ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ) → 2 ∈ ℂ )
60 2ne0 ⊢ 2 ≠ 0
61 60 a1i ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ) → 2 ≠ 0 )
62 div11 ⊢ ( ( ( ( ( - 1 ↑ 𝑆 ) · 𝑆 ) mod 𝑃 ) ∈ ℂ ∧ ( ( ( - 1 ↑ 𝑅 ) · 𝑅 ) mod 𝑃 ) ∈ ℂ ∧ ( 2 ∈ ℂ ∧ 2 ≠ 0 ) ) → ( ( ( ( ( - 1 ↑ 𝑆 ) · 𝑆 ) mod 𝑃 ) / 2 ) = ( ( ( ( - 1 ↑ 𝑅 ) · 𝑅 ) mod 𝑃 ) / 2 ) ↔ ( ( ( - 1 ↑ 𝑆 ) · 𝑆 ) mod 𝑃 ) = ( ( ( - 1 ↑ 𝑅 ) · 𝑅 ) mod 𝑃 ) ) )
63 45 58 59 61 62 syl112anc ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ) → ( ( ( ( ( - 1 ↑ 𝑆 ) · 𝑆 ) mod 𝑃 ) / 2 ) = ( ( ( ( - 1 ↑ 𝑅 ) · 𝑅 ) mod 𝑃 ) / 2 ) ↔ ( ( ( - 1 ↑ 𝑆 ) · 𝑆 ) mod 𝑃 ) = ( ( ( - 1 ↑ 𝑅 ) · 𝑅 ) mod 𝑃 ) ) )
64 37 nnrpd ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ) → 𝑃 ∈ ℝ+ )
65 eqidd ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ) → ( ( - 1 ↑ 𝑆 ) mod 𝑃 ) = ( ( - 1 ↑ 𝑆 ) mod 𝑃 ) )
66 6 oveq1i ⊢ ( 𝑆 mod 𝑃 ) = ( ( ( 𝑄 · ( 2 · 𝑦 ) ) mod 𝑃 ) mod 𝑃 )
67 33 zred ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ) → ( 𝑄 · ( 2 · 𝑦 ) ) ∈ ℝ )
68 modabs2 ⊢ ( ( ( 𝑄 · ( 2 · 𝑦 ) ) ∈ ℝ ∧ 𝑃 ∈ ℝ+ ) → ( ( ( 𝑄 · ( 2 · 𝑦 ) ) mod 𝑃 ) mod 𝑃 ) = ( ( 𝑄 · ( 2 · 𝑦 ) ) mod 𝑃 ) )
69 67 64 68 syl2anc ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ) → ( ( ( 𝑄 · ( 2 · 𝑦 ) ) mod 𝑃 ) mod 𝑃 ) = ( ( 𝑄 · ( 2 · 𝑦 ) ) mod 𝑃 ) )
70 66 69 eqtrid ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ) → ( 𝑆 mod 𝑃 ) = ( ( 𝑄 · ( 2 · 𝑦 ) ) mod 𝑃 ) )
71 42 42 40 33 64 65 70 modmul12d ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ) → ( ( ( - 1 ↑ 𝑆 ) · 𝑆 ) mod 𝑃 ) = ( ( ( - 1 ↑ 𝑆 ) · ( 𝑄 · ( 2 · 𝑦 ) ) ) mod 𝑃 ) )
72 eqidd ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ) → ( ( - 1 ↑ 𝑅 ) mod 𝑃 ) = ( ( - 1 ↑ 𝑅 ) mod 𝑃 ) )
73 4 oveq1i ⊢ ( 𝑅 mod 𝑃 ) = ( ( ( 𝑄 · ( 2 · 𝑥 ) ) mod 𝑃 ) mod 𝑃 )
74 50 zred ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ) → ( 𝑄 · ( 2 · 𝑥 ) ) ∈ ℝ )
75 modabs2 ⊢ ( ( ( 𝑄 · ( 2 · 𝑥 ) ) ∈ ℝ ∧ 𝑃 ∈ ℝ+ ) → ( ( ( 𝑄 · ( 2 · 𝑥 ) ) mod 𝑃 ) mod 𝑃 ) = ( ( 𝑄 · ( 2 · 𝑥 ) ) mod 𝑃 ) )
76 74 64 75 syl2anc ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ) → ( ( ( 𝑄 · ( 2 · 𝑥 ) ) mod 𝑃 ) mod 𝑃 ) = ( ( 𝑄 · ( 2 · 𝑥 ) ) mod 𝑃 ) )
77 73 76 eqtrid ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ) → ( 𝑅 mod 𝑃 ) = ( ( 𝑄 · ( 2 · 𝑥 ) ) mod 𝑃 ) )
78 55 55 53 50 64 72 77 modmul12d ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ) → ( ( ( - 1 ↑ 𝑅 ) · 𝑅 ) mod 𝑃 ) = ( ( ( - 1 ↑ 𝑅 ) · ( 𝑄 · ( 2 · 𝑥 ) ) ) mod 𝑃 ) )
79 71 78 eqeq12d ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ) → ( ( ( ( - 1 ↑ 𝑆 ) · 𝑆 ) mod 𝑃 ) = ( ( ( - 1 ↑ 𝑅 ) · 𝑅 ) mod 𝑃 ) ↔ ( ( ( - 1 ↑ 𝑆 ) · ( 𝑄 · ( 2 · 𝑦 ) ) ) mod 𝑃 ) = ( ( ( - 1 ↑ 𝑅 ) · ( 𝑄 · ( 2 · 𝑥 ) ) ) mod 𝑃 ) ) )
80 42 33 zmulcld ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ) → ( ( - 1 ↑ 𝑆 ) · ( 𝑄 · ( 2 · 𝑦 ) ) ) ∈ ℤ )
81 55 50 zmulcld ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ) → ( ( - 1 ↑ 𝑅 ) · ( 𝑄 · ( 2 · 𝑥 ) ) ) ∈ ℤ )
82 moddvds ⊢ ( ( 𝑃 ∈ ℕ ∧ ( ( - 1 ↑ 𝑆 ) · ( 𝑄 · ( 2 · 𝑦 ) ) ) ∈ ℤ ∧ ( ( - 1 ↑ 𝑅 ) · ( 𝑄 · ( 2 · 𝑥 ) ) ) ∈ ℤ ) → ( ( ( ( - 1 ↑ 𝑆 ) · ( 𝑄 · ( 2 · 𝑦 ) ) ) mod 𝑃 ) = ( ( ( - 1 ↑ 𝑅 ) · ( 𝑄 · ( 2 · 𝑥 ) ) ) mod 𝑃 ) ↔ 𝑃 ∥ ( ( ( - 1 ↑ 𝑆 ) · ( 𝑄 · ( 2 · 𝑦 ) ) ) − ( ( - 1 ↑ 𝑅 ) · ( 𝑄 · ( 2 · 𝑥 ) ) ) ) ) )
83 37 80 81 82 syl3anc ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ) → ( ( ( ( - 1 ↑ 𝑆 ) · ( 𝑄 · ( 2 · 𝑦 ) ) ) mod 𝑃 ) = ( ( ( - 1 ↑ 𝑅 ) · ( 𝑄 · ( 2 · 𝑥 ) ) ) mod 𝑃 ) ↔ 𝑃 ∥ ( ( ( - 1 ↑ 𝑆 ) · ( 𝑄 · ( 2 · 𝑦 ) ) ) − ( ( - 1 ↑ 𝑅 ) · ( 𝑄 · ( 2 · 𝑥 ) ) ) ) ) )
84 27 zcnd ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ) → 𝑄 ∈ ℂ )
85 42 32 zmulcld ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ) → ( ( - 1 ↑ 𝑆 ) · ( 2 · 𝑦 ) ) ∈ ℤ )
86 85 zcnd ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ) → ( ( - 1 ↑ 𝑆 ) · ( 2 · 𝑦 ) ) ∈ ℂ )
87 55 49 zmulcld ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ) → ( ( - 1 ↑ 𝑅 ) · ( 2 · 𝑥 ) ) ∈ ℤ )
88 87 zcnd ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ) → ( ( - 1 ↑ 𝑅 ) · ( 2 · 𝑥 ) ) ∈ ℂ )
89 84 86 88 subdid ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ) → ( 𝑄 · ( ( ( - 1 ↑ 𝑆 ) · ( 2 · 𝑦 ) ) − ( ( - 1 ↑ 𝑅 ) · ( 2 · 𝑥 ) ) ) ) = ( ( 𝑄 · ( ( - 1 ↑ 𝑆 ) · ( 2 · 𝑦 ) ) ) − ( 𝑄 · ( ( - 1 ↑ 𝑅 ) · ( 2 · 𝑥 ) ) ) ) )
90 42 zcnd ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ) → ( - 1 ↑ 𝑆 ) ∈ ℂ )
91 32 zcnd ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ) → ( 2 · 𝑦 ) ∈ ℂ )
92 84 90 91 mul12d ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ) → ( 𝑄 · ( ( - 1 ↑ 𝑆 ) · ( 2 · 𝑦 ) ) ) = ( ( - 1 ↑ 𝑆 ) · ( 𝑄 · ( 2 · 𝑦 ) ) ) )
93 55 zcnd ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ) → ( - 1 ↑ 𝑅 ) ∈ ℂ )
94 49 zcnd ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ) → ( 2 · 𝑥 ) ∈ ℂ )
95 84 93 94 mul12d ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ) → ( 𝑄 · ( ( - 1 ↑ 𝑅 ) · ( 2 · 𝑥 ) ) ) = ( ( - 1 ↑ 𝑅 ) · ( 𝑄 · ( 2 · 𝑥 ) ) ) )
96 92 95 oveq12d ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ) → ( ( 𝑄 · ( ( - 1 ↑ 𝑆 ) · ( 2 · 𝑦 ) ) ) − ( 𝑄 · ( ( - 1 ↑ 𝑅 ) · ( 2 · 𝑥 ) ) ) ) = ( ( ( - 1 ↑ 𝑆 ) · ( 𝑄 · ( 2 · 𝑦 ) ) ) − ( ( - 1 ↑ 𝑅 ) · ( 𝑄 · ( 2 · 𝑥 ) ) ) ) )
97 89 96 eqtrd ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ) → ( 𝑄 · ( ( ( - 1 ↑ 𝑆 ) · ( 2 · 𝑦 ) ) − ( ( - 1 ↑ 𝑅 ) · ( 2 · 𝑥 ) ) ) ) = ( ( ( - 1 ↑ 𝑆 ) · ( 𝑄 · ( 2 · 𝑦 ) ) ) − ( ( - 1 ↑ 𝑅 ) · ( 𝑄 · ( 2 · 𝑥 ) ) ) ) )
98 97 breq2d ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ) → ( 𝑃 ∥ ( 𝑄 · ( ( ( - 1 ↑ 𝑆 ) · ( 2 · 𝑦 ) ) − ( ( - 1 ↑ 𝑅 ) · ( 2 · 𝑥 ) ) ) ) ↔ 𝑃 ∥ ( ( ( - 1 ↑ 𝑆 ) · ( 𝑄 · ( 2 · 𝑦 ) ) ) − ( ( - 1 ↑ 𝑅 ) · ( 𝑄 · ( 2 · 𝑥 ) ) ) ) ) )
99 3 adantr ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ) → 𝑃 ≠ 𝑄 )
100 prmrp ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑄 ∈ ℙ ) → ( ( 𝑃 gcd 𝑄 ) = 1 ↔ 𝑃 ≠ 𝑄 ) )
101 35 25 100 syl2anc ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ) → ( ( 𝑃 gcd 𝑄 ) = 1 ↔ 𝑃 ≠ 𝑄 ) )
102 99 101 mpbird ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ) → ( 𝑃 gcd 𝑄 ) = 1 )
103 prmz ⊢ ( 𝑃 ∈ ℙ → 𝑃 ∈ ℤ )
104 35 103 syl ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ) → 𝑃 ∈ ℤ )
105 85 87 zsubcld ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ) → ( ( ( - 1 ↑ 𝑆 ) · ( 2 · 𝑦 ) ) − ( ( - 1 ↑ 𝑅 ) · ( 2 · 𝑥 ) ) ) ∈ ℤ )
106 coprmdvds ⊢ ( ( 𝑃 ∈ ℤ ∧ 𝑄 ∈ ℤ ∧ ( ( ( - 1 ↑ 𝑆 ) · ( 2 · 𝑦 ) ) − ( ( - 1 ↑ 𝑅 ) · ( 2 · 𝑥 ) ) ) ∈ ℤ ) → ( ( 𝑃 ∥ ( 𝑄 · ( ( ( - 1 ↑ 𝑆 ) · ( 2 · 𝑦 ) ) − ( ( - 1 ↑ 𝑅 ) · ( 2 · 𝑥 ) ) ) ) ∧ ( 𝑃 gcd 𝑄 ) = 1 ) → 𝑃 ∥ ( ( ( - 1 ↑ 𝑆 ) · ( 2 · 𝑦 ) ) − ( ( - 1 ↑ 𝑅 ) · ( 2 · 𝑥 ) ) ) ) )
107 104 27 105 106 syl3anc ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ) → ( ( 𝑃 ∥ ( 𝑄 · ( ( ( - 1 ↑ 𝑆 ) · ( 2 · 𝑦 ) ) − ( ( - 1 ↑ 𝑅 ) · ( 2 · 𝑥 ) ) ) ) ∧ ( 𝑃 gcd 𝑄 ) = 1 ) → 𝑃 ∥ ( ( ( - 1 ↑ 𝑆 ) · ( 2 · 𝑦 ) ) − ( ( - 1 ↑ 𝑅 ) · ( 2 · 𝑥 ) ) ) ) )
108 102 107 mpan2d ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ) → ( 𝑃 ∥ ( 𝑄 · ( ( ( - 1 ↑ 𝑆 ) · ( 2 · 𝑦 ) ) − ( ( - 1 ↑ 𝑅 ) · ( 2 · 𝑥 ) ) ) ) → 𝑃 ∥ ( ( ( - 1 ↑ 𝑆 ) · ( 2 · 𝑦 ) ) − ( ( - 1 ↑ 𝑅 ) · ( 2 · 𝑥 ) ) ) ) )
109 dvdsmultr2 ⊢ ( ( 𝑃 ∈ ℤ ∧ ( - 1 ↑ 𝑅 ) ∈ ℤ ∧ ( ( ( - 1 ↑ 𝑆 ) · ( 2 · 𝑦 ) ) − ( ( - 1 ↑ 𝑅 ) · ( 2 · 𝑥 ) ) ) ∈ ℤ ) → ( 𝑃 ∥ ( ( ( - 1 ↑ 𝑆 ) · ( 2 · 𝑦 ) ) − ( ( - 1 ↑ 𝑅 ) · ( 2 · 𝑥 ) ) ) → 𝑃 ∥ ( ( - 1 ↑ 𝑅 ) · ( ( ( - 1 ↑ 𝑆 ) · ( 2 · 𝑦 ) ) − ( ( - 1 ↑ 𝑅 ) · ( 2 · 𝑥 ) ) ) ) ) )
110 104 55 105 109 syl3anc ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ) → ( 𝑃 ∥ ( ( ( - 1 ↑ 𝑆 ) · ( 2 · 𝑦 ) ) − ( ( - 1 ↑ 𝑅 ) · ( 2 · 𝑥 ) ) ) → 𝑃 ∥ ( ( - 1 ↑ 𝑅 ) · ( ( ( - 1 ↑ 𝑆 ) · ( 2 · 𝑦 ) ) − ( ( - 1 ↑ 𝑅 ) · ( 2 · 𝑥 ) ) ) ) ) )
111 93 86 88 subdid ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ) → ( ( - 1 ↑ 𝑅 ) · ( ( ( - 1 ↑ 𝑆 ) · ( 2 · 𝑦 ) ) − ( ( - 1 ↑ 𝑅 ) · ( 2 · 𝑥 ) ) ) ) = ( ( ( - 1 ↑ 𝑅 ) · ( ( - 1 ↑ 𝑆 ) · ( 2 · 𝑦 ) ) ) − ( ( - 1 ↑ 𝑅 ) · ( ( - 1 ↑ 𝑅 ) · ( 2 · 𝑥 ) ) ) ) )
112 neg1cn ⊢ - 1 ∈ ℂ
113 112 a1i ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ) → - 1 ∈ ℂ )
114 113 39 52 expaddd ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ) → ( - 1 ↑ ( 𝑅 + 𝑆 ) ) = ( ( - 1 ↑ 𝑅 ) · ( - 1 ↑ 𝑆 ) ) )
115 114 oveq1d ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ) → ( ( - 1 ↑ ( 𝑅 + 𝑆 ) ) · ( 2 · 𝑦 ) ) = ( ( ( - 1 ↑ 𝑅 ) · ( - 1 ↑ 𝑆 ) ) · ( 2 · 𝑦 ) ) )
116 93 90 91 mulassd ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ) → ( ( ( - 1 ↑ 𝑅 ) · ( - 1 ↑ 𝑆 ) ) · ( 2 · 𝑦 ) ) = ( ( - 1 ↑ 𝑅 ) · ( ( - 1 ↑ 𝑆 ) · ( 2 · 𝑦 ) ) ) )
117 115 116 eqtr2d ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ) → ( ( - 1 ↑ 𝑅 ) · ( ( - 1 ↑ 𝑆 ) · ( 2 · 𝑦 ) ) ) = ( ( - 1 ↑ ( 𝑅 + 𝑆 ) ) · ( 2 · 𝑦 ) ) )
118 ax-1cn ⊢ 1 ∈ ℂ
119 ax-1ne0 ⊢ 1 ≠ 0
120 divneg2 ⊢ ( ( 1 ∈ ℂ ∧ 1 ∈ ℂ ∧ 1 ≠ 0 ) → - ( 1 / 1 ) = ( 1 / - 1 ) )
121 118 118 119 120 mp3an ⊢ - ( 1 / 1 ) = ( 1 / - 1 )
122 1div1e1 ⊢ ( 1 / 1 ) = 1
123 122 negeqi ⊢ - ( 1 / 1 ) = - 1
124 121 123 eqtr3i ⊢ ( 1 / - 1 ) = - 1
125 124 oveq1i ⊢ ( ( 1 / - 1 ) ↑ 𝑅 ) = ( - 1 ↑ 𝑅 )
126 neg1ne0 ⊢ - 1 ≠ 0
127 126 a1i ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ) → - 1 ≠ 0 )
128 113 127 53 exprecd ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ) → ( ( 1 / - 1 ) ↑ 𝑅 ) = ( 1 / ( - 1 ↑ 𝑅 ) ) )
129 125 128 eqtr3id ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ) → ( - 1 ↑ 𝑅 ) = ( 1 / ( - 1 ↑ 𝑅 ) ) )
130 129 oveq2d ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ) → ( ( - 1 ↑ 𝑅 ) · ( - 1 ↑ 𝑅 ) ) = ( ( - 1 ↑ 𝑅 ) · ( 1 / ( - 1 ↑ 𝑅 ) ) ) )
131 113 127 53 expne0d ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ) → ( - 1 ↑ 𝑅 ) ≠ 0 )
132 93 131 recidd ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ) → ( ( - 1 ↑ 𝑅 ) · ( 1 / ( - 1 ↑ 𝑅 ) ) ) = 1 )
133 130 132 eqtrd ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ) → ( ( - 1 ↑ 𝑅 ) · ( - 1 ↑ 𝑅 ) ) = 1 )
134 133 oveq1d ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ) → ( ( ( - 1 ↑ 𝑅 ) · ( - 1 ↑ 𝑅 ) ) · ( 2 · 𝑥 ) ) = ( 1 · ( 2 · 𝑥 ) ) )
135 93 93 94 mulassd ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ) → ( ( ( - 1 ↑ 𝑅 ) · ( - 1 ↑ 𝑅 ) ) · ( 2 · 𝑥 ) ) = ( ( - 1 ↑ 𝑅 ) · ( ( - 1 ↑ 𝑅 ) · ( 2 · 𝑥 ) ) ) )
136 94 mullidd ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ) → ( 1 · ( 2 · 𝑥 ) ) = ( 2 · 𝑥 ) )
137 134 135 136 3eqtr3d ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ) → ( ( - 1 ↑ 𝑅 ) · ( ( - 1 ↑ 𝑅 ) · ( 2 · 𝑥 ) ) ) = ( 2 · 𝑥 ) )
138 117 137 oveq12d ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ) → ( ( ( - 1 ↑ 𝑅 ) · ( ( - 1 ↑ 𝑆 ) · ( 2 · 𝑦 ) ) ) − ( ( - 1 ↑ 𝑅 ) · ( ( - 1 ↑ 𝑅 ) · ( 2 · 𝑥 ) ) ) ) = ( ( ( - 1 ↑ ( 𝑅 + 𝑆 ) ) · ( 2 · 𝑦 ) ) − ( 2 · 𝑥 ) ) )
139 111 138 eqtrd ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ) → ( ( - 1 ↑ 𝑅 ) · ( ( ( - 1 ↑ 𝑆 ) · ( 2 · 𝑦 ) ) − ( ( - 1 ↑ 𝑅 ) · ( 2 · 𝑥 ) ) ) ) = ( ( ( - 1 ↑ ( 𝑅 + 𝑆 ) ) · ( 2 · 𝑦 ) ) − ( 2 · 𝑥 ) ) )
140 139 breq2d ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ) → ( 𝑃 ∥ ( ( - 1 ↑ 𝑅 ) · ( ( ( - 1 ↑ 𝑆 ) · ( 2 · 𝑦 ) ) − ( ( - 1 ↑ 𝑅 ) · ( 2 · 𝑥 ) ) ) ) ↔ 𝑃 ∥ ( ( ( - 1 ↑ ( 𝑅 + 𝑆 ) ) · ( 2 · 𝑦 ) ) − ( 2 · 𝑥 ) ) ) )
141 eqcom ⊢ ( ( ( - 1 · ( 2 · 𝑦 ) ) mod 𝑃 ) = ( ( 2 · 𝑥 ) mod 𝑃 ) ↔ ( ( 2 · 𝑥 ) mod 𝑃 ) = ( ( - 1 · ( 2 · 𝑦 ) ) mod 𝑃 ) )
142 91 mulm1d ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ) → ( - 1 · ( 2 · 𝑦 ) ) = - ( 2 · 𝑦 ) )
143 142 oveq1d ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ) → ( ( - 1 · ( 2 · 𝑦 ) ) mod 𝑃 ) = ( - ( 2 · 𝑦 ) mod 𝑃 ) )
144 143 eqeq2d ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ) → ( ( ( 2 · 𝑥 ) mod 𝑃 ) = ( ( - 1 · ( 2 · 𝑦 ) ) mod 𝑃 ) ↔ ( ( 2 · 𝑥 ) mod 𝑃 ) = ( - ( 2 · 𝑦 ) mod 𝑃 ) ) )
145 141 144 bitrid ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ) → ( ( ( - 1 · ( 2 · 𝑦 ) ) mod 𝑃 ) = ( ( 2 · 𝑥 ) mod 𝑃 ) ↔ ( ( 2 · 𝑥 ) mod 𝑃 ) = ( - ( 2 · 𝑦 ) mod 𝑃 ) ) )
146 32 znegcld ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ) → - ( 2 · 𝑦 ) ∈ ℤ )
147 moddvds ⊢ ( ( 𝑃 ∈ ℕ ∧ ( 2 · 𝑥 ) ∈ ℤ ∧ - ( 2 · 𝑦 ) ∈ ℤ ) → ( ( ( 2 · 𝑥 ) mod 𝑃 ) = ( - ( 2 · 𝑦 ) mod 𝑃 ) ↔ 𝑃 ∥ ( ( 2 · 𝑥 ) − - ( 2 · 𝑦 ) ) ) )
148 37 49 146 147 syl3anc ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ) → ( ( ( 2 · 𝑥 ) mod 𝑃 ) = ( - ( 2 · 𝑦 ) mod 𝑃 ) ↔ 𝑃 ∥ ( ( 2 · 𝑥 ) − - ( 2 · 𝑦 ) ) ) )
149 elfznn ⊢ ( 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) → 𝑥 ∈ ℕ )
150 149 ad2antll ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ) → 𝑥 ∈ ℕ )
151 elfznn ⊢ ( 𝑦 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) → 𝑦 ∈ ℕ )
152 151 ad2antrl ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ) → 𝑦 ∈ ℕ )
153 150 152 nnaddcld ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ) → ( 𝑥 + 𝑦 ) ∈ ℕ )
154 150 nnred ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ) → 𝑥 ∈ ℝ )
155 30 zred ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ) → 𝑦 ∈ ℝ )
156 oddprm ⊢ ( 𝑃 ∈ ( ℙ ∖ { 2 } ) → ( ( 𝑃 − 1 ) / 2 ) ∈ ℕ )
157 34 156 syl ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ) → ( ( 𝑃 − 1 ) / 2 ) ∈ ℕ )
158 157 nnred ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ) → ( ( 𝑃 − 1 ) / 2 ) ∈ ℝ )
159 elfzle2 ⊢ ( 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) → 𝑥 ≤ ( ( 𝑃 − 1 ) / 2 ) )
160 159 ad2antll ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ) → 𝑥 ≤ ( ( 𝑃 − 1 ) / 2 ) )
161 elfzle2 ⊢ ( 𝑦 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) → 𝑦 ≤ ( ( 𝑃 − 1 ) / 2 ) )
162 161 ad2antrl ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ) → 𝑦 ≤ ( ( 𝑃 − 1 ) / 2 ) )
163 154 155 158 158 160 162 le2addd ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ) → ( 𝑥 + 𝑦 ) ≤ ( ( ( 𝑃 − 1 ) / 2 ) + ( ( 𝑃 − 1 ) / 2 ) ) )
164 37 nnred ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ) → 𝑃 ∈ ℝ )
165 peano2rem ⊢ ( 𝑃 ∈ ℝ → ( 𝑃 − 1 ) ∈ ℝ )
166 164 165 syl ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ) → ( 𝑃 − 1 ) ∈ ℝ )
167 166 recnd ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ) → ( 𝑃 − 1 ) ∈ ℂ )
168 167 2halvesd ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ) → ( ( ( 𝑃 − 1 ) / 2 ) + ( ( 𝑃 − 1 ) / 2 ) ) = ( 𝑃 − 1 ) )
169 163 168 breqtrd ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ) → ( 𝑥 + 𝑦 ) ≤ ( 𝑃 − 1 ) )
170 peano2zm ⊢ ( 𝑃 ∈ ℤ → ( 𝑃 − 1 ) ∈ ℤ )
171 fznn ⊢ ( ( 𝑃 − 1 ) ∈ ℤ → ( ( 𝑥 + 𝑦 ) ∈ ( 1 ... ( 𝑃 − 1 ) ) ↔ ( ( 𝑥 + 𝑦 ) ∈ ℕ ∧ ( 𝑥 + 𝑦 ) ≤ ( 𝑃 − 1 ) ) ) )
172 104 170 171 3syl ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ) → ( ( 𝑥 + 𝑦 ) ∈ ( 1 ... ( 𝑃 − 1 ) ) ↔ ( ( 𝑥 + 𝑦 ) ∈ ℕ ∧ ( 𝑥 + 𝑦 ) ≤ ( 𝑃 − 1 ) ) ) )
173 153 169 172 mpbir2and ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ) → ( 𝑥 + 𝑦 ) ∈ ( 1 ... ( 𝑃 − 1 ) ) )
174 fzm1ndvds ⊢ ( ( 𝑃 ∈ ℕ ∧ ( 𝑥 + 𝑦 ) ∈ ( 1 ... ( 𝑃 − 1 ) ) ) → ¬ 𝑃 ∥ ( 𝑥 + 𝑦 ) )
175 37 173 174 syl2anc ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ) → ¬ 𝑃 ∥ ( 𝑥 + 𝑦 ) )
176 eldifsni ⊢ ( 𝑃 ∈ ( ℙ ∖ { 2 } ) → 𝑃 ≠ 2 )
177 34 176 syl ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ) → 𝑃 ≠ 2 )
178 2prm ⊢ 2 ∈ ℙ
179 prmrp ⊢ ( ( 𝑃 ∈ ℙ ∧ 2 ∈ ℙ ) → ( ( 𝑃 gcd 2 ) = 1 ↔ 𝑃 ≠ 2 ) )
180 35 178 179 sylancl ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ) → ( ( 𝑃 gcd 2 ) = 1 ↔ 𝑃 ≠ 2 ) )
181 177 180 mpbird ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ) → ( 𝑃 gcd 2 ) = 1 )
182 28 a1i ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ) → 2 ∈ ℤ )
183 153 nnzd ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ) → ( 𝑥 + 𝑦 ) ∈ ℤ )
184 coprmdvds ⊢ ( ( 𝑃 ∈ ℤ ∧ 2 ∈ ℤ ∧ ( 𝑥 + 𝑦 ) ∈ ℤ ) → ( ( 𝑃 ∥ ( 2 · ( 𝑥 + 𝑦 ) ) ∧ ( 𝑃 gcd 2 ) = 1 ) → 𝑃 ∥ ( 𝑥 + 𝑦 ) ) )
185 104 182 183 184 syl3anc ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ) → ( ( 𝑃 ∥ ( 2 · ( 𝑥 + 𝑦 ) ) ∧ ( 𝑃 gcd 2 ) = 1 ) → 𝑃 ∥ ( 𝑥 + 𝑦 ) ) )
186 181 185 mpan2d ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ) → ( 𝑃 ∥ ( 2 · ( 𝑥 + 𝑦 ) ) → 𝑃 ∥ ( 𝑥 + 𝑦 ) ) )
187 175 186 mtod ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ) → ¬ 𝑃 ∥ ( 2 · ( 𝑥 + 𝑦 ) ) )
188 94 91 subnegd ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ) → ( ( 2 · 𝑥 ) − - ( 2 · 𝑦 ) ) = ( ( 2 · 𝑥 ) + ( 2 · 𝑦 ) ) )
189 47 zcnd ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ) → 𝑥 ∈ ℂ )
190 30 zcnd ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ) → 𝑦 ∈ ℂ )
191 59 189 190 adddid ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ) → ( 2 · ( 𝑥 + 𝑦 ) ) = ( ( 2 · 𝑥 ) + ( 2 · 𝑦 ) ) )
192 188 191 eqtr4d ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ) → ( ( 2 · 𝑥 ) − - ( 2 · 𝑦 ) ) = ( 2 · ( 𝑥 + 𝑦 ) ) )
193 192 breq2d ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ) → ( 𝑃 ∥ ( ( 2 · 𝑥 ) − - ( 2 · 𝑦 ) ) ↔ 𝑃 ∥ ( 2 · ( 𝑥 + 𝑦 ) ) ) )
194 187 193 mtbird ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ) → ¬ 𝑃 ∥ ( ( 2 · 𝑥 ) − - ( 2 · 𝑦 ) ) )
195 194 pm2.21d ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ) → ( 𝑃 ∥ ( ( 2 · 𝑥 ) − - ( 2 · 𝑦 ) ) → ( 2 · 𝑦 ) = ( 2 · 𝑥 ) ) )
196 148 195 sylbid ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ) → ( ( ( 2 · 𝑥 ) mod 𝑃 ) = ( - ( 2 · 𝑦 ) mod 𝑃 ) → ( 2 · 𝑦 ) = ( 2 · 𝑥 ) ) )
197 145 196 sylbid ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ) → ( ( ( - 1 · ( 2 · 𝑦 ) ) mod 𝑃 ) = ( ( 2 · 𝑥 ) mod 𝑃 ) → ( 2 · 𝑦 ) = ( 2 · 𝑥 ) ) )
198 oveq1 ⊢ ( ( - 1 ↑ ( 𝑅 + 𝑆 ) ) = - 1 → ( ( - 1 ↑ ( 𝑅 + 𝑆 ) ) · ( 2 · 𝑦 ) ) = ( - 1 · ( 2 · 𝑦 ) ) )
199 198 oveq1d ⊢ ( ( - 1 ↑ ( 𝑅 + 𝑆 ) ) = - 1 → ( ( ( - 1 ↑ ( 𝑅 + 𝑆 ) ) · ( 2 · 𝑦 ) ) mod 𝑃 ) = ( ( - 1 · ( 2 · 𝑦 ) ) mod 𝑃 ) )
200 199 eqeq1d ⊢ ( ( - 1 ↑ ( 𝑅 + 𝑆 ) ) = - 1 → ( ( ( ( - 1 ↑ ( 𝑅 + 𝑆 ) ) · ( 2 · 𝑦 ) ) mod 𝑃 ) = ( ( 2 · 𝑥 ) mod 𝑃 ) ↔ ( ( - 1 · ( 2 · 𝑦 ) ) mod 𝑃 ) = ( ( 2 · 𝑥 ) mod 𝑃 ) ) )
201 200 imbi1d ⊢ ( ( - 1 ↑ ( 𝑅 + 𝑆 ) ) = - 1 → ( ( ( ( ( - 1 ↑ ( 𝑅 + 𝑆 ) ) · ( 2 · 𝑦 ) ) mod 𝑃 ) = ( ( 2 · 𝑥 ) mod 𝑃 ) → ( 2 · 𝑦 ) = ( 2 · 𝑥 ) ) ↔ ( ( ( - 1 · ( 2 · 𝑦 ) ) mod 𝑃 ) = ( ( 2 · 𝑥 ) mod 𝑃 ) → ( 2 · 𝑦 ) = ( 2 · 𝑥 ) ) ) )
202 197 201 syl5ibrcom ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ) → ( ( - 1 ↑ ( 𝑅 + 𝑆 ) ) = - 1 → ( ( ( ( - 1 ↑ ( 𝑅 + 𝑆 ) ) · ( 2 · 𝑦 ) ) mod 𝑃 ) = ( ( 2 · 𝑥 ) mod 𝑃 ) → ( 2 · 𝑦 ) = ( 2 · 𝑥 ) ) ) )
203 91 mullidd ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ) → ( 1 · ( 2 · 𝑦 ) ) = ( 2 · 𝑦 ) )
204 203 oveq1d ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ) → ( ( 1 · ( 2 · 𝑦 ) ) mod 𝑃 ) = ( ( 2 · 𝑦 ) mod 𝑃 ) )
205 32 zred ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ) → ( 2 · 𝑦 ) ∈ ℝ )
206 2nn ⊢ 2 ∈ ℕ
207 nnmulcl ⊢ ( ( 2 ∈ ℕ ∧ 𝑦 ∈ ℕ ) → ( 2 · 𝑦 ) ∈ ℕ )
208 206 152 207 sylancr ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ) → ( 2 · 𝑦 ) ∈ ℕ )
209 208 nnnn0d ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ) → ( 2 · 𝑦 ) ∈ ℕ0 )
210 209 nn0ge0d ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ) → 0 ≤ ( 2 · 𝑦 ) )
211 2re ⊢ 2 ∈ ℝ
212 211 a1i ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ) → 2 ∈ ℝ )
213 2pos ⊢ 0 < 2
214 213 a1i ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ) → 0 < 2 )
215 lemuldiv2 ⊢ ( ( 𝑦 ∈ ℝ ∧ ( 𝑃 − 1 ) ∈ ℝ ∧ ( 2 ∈ ℝ ∧ 0 < 2 ) ) → ( ( 2 · 𝑦 ) ≤ ( 𝑃 − 1 ) ↔ 𝑦 ≤ ( ( 𝑃 − 1 ) / 2 ) ) )
216 155 166 212 214 215 syl112anc ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ) → ( ( 2 · 𝑦 ) ≤ ( 𝑃 − 1 ) ↔ 𝑦 ≤ ( ( 𝑃 − 1 ) / 2 ) ) )
217 162 216 mpbird ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ) → ( 2 · 𝑦 ) ≤ ( 𝑃 − 1 ) )
218 zltlem1 ⊢ ( ( ( 2 · 𝑦 ) ∈ ℤ ∧ 𝑃 ∈ ℤ ) → ( ( 2 · 𝑦 ) < 𝑃 ↔ ( 2 · 𝑦 ) ≤ ( 𝑃 − 1 ) ) )
219 32 104 218 syl2anc ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ) → ( ( 2 · 𝑦 ) < 𝑃 ↔ ( 2 · 𝑦 ) ≤ ( 𝑃 − 1 ) ) )
220 217 219 mpbird ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ) → ( 2 · 𝑦 ) < 𝑃 )
221 modid ⊢ ( ( ( ( 2 · 𝑦 ) ∈ ℝ ∧ 𝑃 ∈ ℝ+ ) ∧ ( 0 ≤ ( 2 · 𝑦 ) ∧ ( 2 · 𝑦 ) < 𝑃 ) ) → ( ( 2 · 𝑦 ) mod 𝑃 ) = ( 2 · 𝑦 ) )
222 205 64 210 220 221 syl22anc ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ) → ( ( 2 · 𝑦 ) mod 𝑃 ) = ( 2 · 𝑦 ) )
223 204 222 eqtrd ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ) → ( ( 1 · ( 2 · 𝑦 ) ) mod 𝑃 ) = ( 2 · 𝑦 ) )
224 49 zred ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ) → ( 2 · 𝑥 ) ∈ ℝ )
225 nnmulcl ⊢ ( ( 2 ∈ ℕ ∧ 𝑥 ∈ ℕ ) → ( 2 · 𝑥 ) ∈ ℕ )
226 206 150 225 sylancr ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ) → ( 2 · 𝑥 ) ∈ ℕ )
227 226 nnnn0d ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ) → ( 2 · 𝑥 ) ∈ ℕ0 )
228 227 nn0ge0d ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ) → 0 ≤ ( 2 · 𝑥 ) )
229 lemuldiv2 ⊢ ( ( 𝑥 ∈ ℝ ∧ ( 𝑃 − 1 ) ∈ ℝ ∧ ( 2 ∈ ℝ ∧ 0 < 2 ) ) → ( ( 2 · 𝑥 ) ≤ ( 𝑃 − 1 ) ↔ 𝑥 ≤ ( ( 𝑃 − 1 ) / 2 ) ) )
230 154 166 212 214 229 syl112anc ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ) → ( ( 2 · 𝑥 ) ≤ ( 𝑃 − 1 ) ↔ 𝑥 ≤ ( ( 𝑃 − 1 ) / 2 ) ) )
231 160 230 mpbird ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ) → ( 2 · 𝑥 ) ≤ ( 𝑃 − 1 ) )
232 zltlem1 ⊢ ( ( ( 2 · 𝑥 ) ∈ ℤ ∧ 𝑃 ∈ ℤ ) → ( ( 2 · 𝑥 ) < 𝑃 ↔ ( 2 · 𝑥 ) ≤ ( 𝑃 − 1 ) ) )
233 49 104 232 syl2anc ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ) → ( ( 2 · 𝑥 ) < 𝑃 ↔ ( 2 · 𝑥 ) ≤ ( 𝑃 − 1 ) ) )
234 231 233 mpbird ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ) → ( 2 · 𝑥 ) < 𝑃 )
235 modid ⊢ ( ( ( ( 2 · 𝑥 ) ∈ ℝ ∧ 𝑃 ∈ ℝ+ ) ∧ ( 0 ≤ ( 2 · 𝑥 ) ∧ ( 2 · 𝑥 ) < 𝑃 ) ) → ( ( 2 · 𝑥 ) mod 𝑃 ) = ( 2 · 𝑥 ) )
236 224 64 228 234 235 syl22anc ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ) → ( ( 2 · 𝑥 ) mod 𝑃 ) = ( 2 · 𝑥 ) )
237 223 236 eqeq12d ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ) → ( ( ( 1 · ( 2 · 𝑦 ) ) mod 𝑃 ) = ( ( 2 · 𝑥 ) mod 𝑃 ) ↔ ( 2 · 𝑦 ) = ( 2 · 𝑥 ) ) )
238 237 biimpd ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ) → ( ( ( 1 · ( 2 · 𝑦 ) ) mod 𝑃 ) = ( ( 2 · 𝑥 ) mod 𝑃 ) → ( 2 · 𝑦 ) = ( 2 · 𝑥 ) ) )
239 oveq1 ⊢ ( ( - 1 ↑ ( 𝑅 + 𝑆 ) ) = 1 → ( ( - 1 ↑ ( 𝑅 + 𝑆 ) ) · ( 2 · 𝑦 ) ) = ( 1 · ( 2 · 𝑦 ) ) )
240 239 oveq1d ⊢ ( ( - 1 ↑ ( 𝑅 + 𝑆 ) ) = 1 → ( ( ( - 1 ↑ ( 𝑅 + 𝑆 ) ) · ( 2 · 𝑦 ) ) mod 𝑃 ) = ( ( 1 · ( 2 · 𝑦 ) ) mod 𝑃 ) )
241 240 eqeq1d ⊢ ( ( - 1 ↑ ( 𝑅 + 𝑆 ) ) = 1 → ( ( ( ( - 1 ↑ ( 𝑅 + 𝑆 ) ) · ( 2 · 𝑦 ) ) mod 𝑃 ) = ( ( 2 · 𝑥 ) mod 𝑃 ) ↔ ( ( 1 · ( 2 · 𝑦 ) ) mod 𝑃 ) = ( ( 2 · 𝑥 ) mod 𝑃 ) ) )
242 241 imbi1d ⊢ ( ( - 1 ↑ ( 𝑅 + 𝑆 ) ) = 1 → ( ( ( ( ( - 1 ↑ ( 𝑅 + 𝑆 ) ) · ( 2 · 𝑦 ) ) mod 𝑃 ) = ( ( 2 · 𝑥 ) mod 𝑃 ) → ( 2 · 𝑦 ) = ( 2 · 𝑥 ) ) ↔ ( ( ( 1 · ( 2 · 𝑦 ) ) mod 𝑃 ) = ( ( 2 · 𝑥 ) mod 𝑃 ) → ( 2 · 𝑦 ) = ( 2 · 𝑥 ) ) ) )
243 238 242 syl5ibrcom ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ) → ( ( - 1 ↑ ( 𝑅 + 𝑆 ) ) = 1 → ( ( ( ( - 1 ↑ ( 𝑅 + 𝑆 ) ) · ( 2 · 𝑦 ) ) mod 𝑃 ) = ( ( 2 · 𝑥 ) mod 𝑃 ) → ( 2 · 𝑦 ) = ( 2 · 𝑥 ) ) ) )
244 52 39 nn0addcld ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ) → ( 𝑅 + 𝑆 ) ∈ ℕ0 )
245 244 nn0zd ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ) → ( 𝑅 + 𝑆 ) ∈ ℤ )
246 m1expcl2 ⊢ ( ( 𝑅 + 𝑆 ) ∈ ℤ → ( - 1 ↑ ( 𝑅 + 𝑆 ) ) ∈ { - 1 , 1 } )
247 elpri ⊢ ( ( - 1 ↑ ( 𝑅 + 𝑆 ) ) ∈ { - 1 , 1 } → ( ( - 1 ↑ ( 𝑅 + 𝑆 ) ) = - 1 ∨ ( - 1 ↑ ( 𝑅 + 𝑆 ) ) = 1 ) )
248 245 246 247 3syl ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ) → ( ( - 1 ↑ ( 𝑅 + 𝑆 ) ) = - 1 ∨ ( - 1 ↑ ( 𝑅 + 𝑆 ) ) = 1 ) )
249 202 243 248 mpjaod ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ) → ( ( ( ( - 1 ↑ ( 𝑅 + 𝑆 ) ) · ( 2 · 𝑦 ) ) mod 𝑃 ) = ( ( 2 · 𝑥 ) mod 𝑃 ) → ( 2 · 𝑦 ) = ( 2 · 𝑥 ) ) )
250 neg1z ⊢ - 1 ∈ ℤ
251 zexpcl ⊢ ( ( - 1 ∈ ℤ ∧ ( 𝑅 + 𝑆 ) ∈ ℕ0 ) → ( - 1 ↑ ( 𝑅 + 𝑆 ) ) ∈ ℤ )
252 250 244 251 sylancr ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ) → ( - 1 ↑ ( 𝑅 + 𝑆 ) ) ∈ ℤ )
253 252 32 zmulcld ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ) → ( ( - 1 ↑ ( 𝑅 + 𝑆 ) ) · ( 2 · 𝑦 ) ) ∈ ℤ )
254 moddvds ⊢ ( ( 𝑃 ∈ ℕ ∧ ( ( - 1 ↑ ( 𝑅 + 𝑆 ) ) · ( 2 · 𝑦 ) ) ∈ ℤ ∧ ( 2 · 𝑥 ) ∈ ℤ ) → ( ( ( ( - 1 ↑ ( 𝑅 + 𝑆 ) ) · ( 2 · 𝑦 ) ) mod 𝑃 ) = ( ( 2 · 𝑥 ) mod 𝑃 ) ↔ 𝑃 ∥ ( ( ( - 1 ↑ ( 𝑅 + 𝑆 ) ) · ( 2 · 𝑦 ) ) − ( 2 · 𝑥 ) ) ) )
255 37 253 49 254 syl3anc ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ) → ( ( ( ( - 1 ↑ ( 𝑅 + 𝑆 ) ) · ( 2 · 𝑦 ) ) mod 𝑃 ) = ( ( 2 · 𝑥 ) mod 𝑃 ) ↔ 𝑃 ∥ ( ( ( - 1 ↑ ( 𝑅 + 𝑆 ) ) · ( 2 · 𝑦 ) ) − ( 2 · 𝑥 ) ) ) )
256 190 189 59 61 mulcand ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ) → ( ( 2 · 𝑦 ) = ( 2 · 𝑥 ) ↔ 𝑦 = 𝑥 ) )
257 249 255 256 3imtr3d ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ) → ( 𝑃 ∥ ( ( ( - 1 ↑ ( 𝑅 + 𝑆 ) ) · ( 2 · 𝑦 ) ) − ( 2 · 𝑥 ) ) → 𝑦 = 𝑥 ) )
258 140 257 sylbid ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ) → ( 𝑃 ∥ ( ( - 1 ↑ 𝑅 ) · ( ( ( - 1 ↑ 𝑆 ) · ( 2 · 𝑦 ) ) − ( ( - 1 ↑ 𝑅 ) · ( 2 · 𝑥 ) ) ) ) → 𝑦 = 𝑥 ) )
259 108 110 258 3syld ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ) → ( 𝑃 ∥ ( 𝑄 · ( ( ( - 1 ↑ 𝑆 ) · ( 2 · 𝑦 ) ) − ( ( - 1 ↑ 𝑅 ) · ( 2 · 𝑥 ) ) ) ) → 𝑦 = 𝑥 ) )
260 98 259 sylbird ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ) → ( 𝑃 ∥ ( ( ( - 1 ↑ 𝑆 ) · ( 𝑄 · ( 2 · 𝑦 ) ) ) − ( ( - 1 ↑ 𝑅 ) · ( 𝑄 · ( 2 · 𝑥 ) ) ) ) → 𝑦 = 𝑥 ) )
261 83 260 sylbid ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ) → ( ( ( ( - 1 ↑ 𝑆 ) · ( 𝑄 · ( 2 · 𝑦 ) ) ) mod 𝑃 ) = ( ( ( - 1 ↑ 𝑅 ) · ( 𝑄 · ( 2 · 𝑥 ) ) ) mod 𝑃 ) → 𝑦 = 𝑥 ) )
262 79 261 sylbid ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ) → ( ( ( ( - 1 ↑ 𝑆 ) · 𝑆 ) mod 𝑃 ) = ( ( ( - 1 ↑ 𝑅 ) · 𝑅 ) mod 𝑃 ) → 𝑦 = 𝑥 ) )
263 63 262 sylbid ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ) → ( ( ( ( ( - 1 ↑ 𝑆 ) · 𝑆 ) mod 𝑃 ) / 2 ) = ( ( ( ( - 1 ↑ 𝑅 ) · 𝑅 ) mod 𝑃 ) / 2 ) → 𝑦 = 𝑥 ) )
264 23 263 sylbid ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ) → ( ( 𝑀 ‘ 𝑦 ) = ( 𝑀 ‘ 𝑥 ) → 𝑦 = 𝑥 ) )
265 264 ralrimivva ⊢ ( 𝜑 → ∀ 𝑦 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ∀ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ( ( 𝑀 ‘ 𝑦 ) = ( 𝑀 ‘ 𝑥 ) → 𝑦 = 𝑥 ) )
266 nfmpt1 ⊢ Ⅎ 𝑥 ( 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ↦ ( ( ( ( - 1 ↑ 𝑅 ) · 𝑅 ) mod 𝑃 ) / 2 ) )
267 5 266 nfcxfr ⊢ Ⅎ 𝑥 𝑀
268 nfcv ⊢ Ⅎ 𝑥 𝑦
269 267 268 nffv ⊢ Ⅎ 𝑥 ( 𝑀 ‘ 𝑦 )
270 nfcv ⊢ Ⅎ 𝑥 𝑧
271 267 270 nffv ⊢ Ⅎ 𝑥 ( 𝑀 ‘ 𝑧 )
272 269 271 nfeq ⊢ Ⅎ 𝑥 ( 𝑀 ‘ 𝑦 ) = ( 𝑀 ‘ 𝑧 )
273 nfv ⊢ Ⅎ 𝑥 𝑦 = 𝑧
274 272 273 nfim ⊢ Ⅎ 𝑥 ( ( 𝑀 ‘ 𝑦 ) = ( 𝑀 ‘ 𝑧 ) → 𝑦 = 𝑧 )
275 nfv ⊢ Ⅎ 𝑧 ( ( 𝑀 ‘ 𝑦 ) = ( 𝑀 ‘ 𝑥 ) → 𝑦 = 𝑥 )
276 fveq2 ⊢ ( 𝑧 = 𝑥 → ( 𝑀 ‘ 𝑧 ) = ( 𝑀 ‘ 𝑥 ) )
277 276 eqeq2d ⊢ ( 𝑧 = 𝑥 → ( ( 𝑀 ‘ 𝑦 ) = ( 𝑀 ‘ 𝑧 ) ↔ ( 𝑀 ‘ 𝑦 ) = ( 𝑀 ‘ 𝑥 ) ) )
278 equequ2 ⊢ ( 𝑧 = 𝑥 → ( 𝑦 = 𝑧 ↔ 𝑦 = 𝑥 ) )
279 277 278 imbi12d ⊢ ( 𝑧 = 𝑥 → ( ( ( 𝑀 ‘ 𝑦 ) = ( 𝑀 ‘ 𝑧 ) → 𝑦 = 𝑧 ) ↔ ( ( 𝑀 ‘ 𝑦 ) = ( 𝑀 ‘ 𝑥 ) → 𝑦 = 𝑥 ) ) )
280 274 275 279 cbvralw ⊢ ( ∀ 𝑧 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ( ( 𝑀 ‘ 𝑦 ) = ( 𝑀 ‘ 𝑧 ) → 𝑦 = 𝑧 ) ↔ ∀ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ( ( 𝑀 ‘ 𝑦 ) = ( 𝑀 ‘ 𝑥 ) → 𝑦 = 𝑥 ) )
281 280 ralbii ⊢ ( ∀ 𝑦 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ∀ 𝑧 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ( ( 𝑀 ‘ 𝑦 ) = ( 𝑀 ‘ 𝑧 ) → 𝑦 = 𝑧 ) ↔ ∀ 𝑦 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ∀ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ( ( 𝑀 ‘ 𝑦 ) = ( 𝑀 ‘ 𝑥 ) → 𝑦 = 𝑥 ) )
282 265 281 sylibr ⊢ ( 𝜑 → ∀ 𝑦 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ∀ 𝑧 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ( ( 𝑀 ‘ 𝑦 ) = ( 𝑀 ‘ 𝑧 ) → 𝑦 = 𝑧 ) )
283 dff13 ⊢ ( 𝑀 : ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) –1-1→ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ↔ ( 𝑀 : ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ⟶ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ∧ ∀ 𝑦 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ∀ 𝑧 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ( ( 𝑀 ‘ 𝑦 ) = ( 𝑀 ‘ 𝑧 ) → 𝑦 = 𝑧 ) ) )
284 7 282 283 sylanbrc ⊢ ( 𝜑 → 𝑀 : ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) –1-1→ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) )
285 ovex ⊢ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ∈ V
286 285 enref ⊢ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ≈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) )
287 fzfi ⊢ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ∈ Fin
288 f1finf1o ⊢ ( ( ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ≈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ∧ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ∈ Fin ) → ( 𝑀 : ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) –1-1→ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ↔ 𝑀 : ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) –1-1-onto→ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) )
289 286 287 288 mp2an ⊢ ( 𝑀 : ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) –1-1→ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ↔ 𝑀 : ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) –1-1-onto→ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) )
290 284 289 sylib ⊢ ( 𝜑 → 𝑀 : ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) –1-1-onto→ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) )