Metamath Proof Explorer

Theorem 2lgslem1a

Description: Lemma 1 for 2lgslem1 . (Contributed by AV, 18-Jun-2021)

Ref Expression
Assertion 2lgslem1a ( ( 𝑃 ∈ ℙ ∧ ¬ 2 ∥ 𝑃 ) → { 𝑥 ∈ ℤ ∣ ∃ 𝑖 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ( 𝑥 = ( 𝑖 · 2 ) ∧ ( 𝑃 / 2 ) < ( 𝑥 mod 𝑃 ) ) } = { 𝑥 ∈ ℤ ∣ ∃ 𝑖 ∈ ( ( ( ⌊ ‘ ( 𝑃 / 4 ) ) + 1 ) ... ( ( 𝑃 − 1 ) / 2 ) ) 𝑥 = ( 𝑖 · 2 ) } )

Proof

Step Hyp Ref Expression
1 prmnn ⊢ ( 𝑃 ∈ ℙ → 𝑃 ∈ ℕ )
2 1 nnnn0d ⊢ ( 𝑃 ∈ ℙ → 𝑃 ∈ ℕ0 )
3 2 ad2antrr ⊢ ( ( ( 𝑃 ∈ ℙ ∧ ¬ 2 ∥ 𝑃 ) ∧ 𝑥 ∈ ℤ ) → 𝑃 ∈ ℕ0 )
4 4nn ⊢ 4 ∈ ℕ
5 3 4 jctir ⊢ ( ( ( 𝑃 ∈ ℙ ∧ ¬ 2 ∥ 𝑃 ) ∧ 𝑥 ∈ ℤ ) → ( 𝑃 ∈ ℕ0 ∧ 4 ∈ ℕ ) )
6 fldivnn0 ⊢ ( ( 𝑃 ∈ ℕ0 ∧ 4 ∈ ℕ ) → ( ⌊ ‘ ( 𝑃 / 4 ) ) ∈ ℕ0 )
7 nn0p1nn ⊢ ( ( ⌊ ‘ ( 𝑃 / 4 ) ) ∈ ℕ0 → ( ( ⌊ ‘ ( 𝑃 / 4 ) ) + 1 ) ∈ ℕ )
8 5 6 7 3syl ⊢ ( ( ( 𝑃 ∈ ℙ ∧ ¬ 2 ∥ 𝑃 ) ∧ 𝑥 ∈ ℤ ) → ( ( ⌊ ‘ ( 𝑃 / 4 ) ) + 1 ) ∈ ℕ )
9 elnnuz ⊢ ( ( ( ⌊ ‘ ( 𝑃 / 4 ) ) + 1 ) ∈ ℕ ↔ ( ( ⌊ ‘ ( 𝑃 / 4 ) ) + 1 ) ∈ ( ℤ≥ ‘ 1 ) )
10 8 9 sylib ⊢ ( ( ( 𝑃 ∈ ℙ ∧ ¬ 2 ∥ 𝑃 ) ∧ 𝑥 ∈ ℤ ) → ( ( ⌊ ‘ ( 𝑃 / 4 ) ) + 1 ) ∈ ( ℤ≥ ‘ 1 ) )
11 fzss1 ⊢ ( ( ( ⌊ ‘ ( 𝑃 / 4 ) ) + 1 ) ∈ ( ℤ≥ ‘ 1 ) → ( ( ( ⌊ ‘ ( 𝑃 / 4 ) ) + 1 ) ... ( ( 𝑃 − 1 ) / 2 ) ) ⊆ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) )
12 rexss ⊢ ( ( ( ( ⌊ ‘ ( 𝑃 / 4 ) ) + 1 ) ... ( ( 𝑃 − 1 ) / 2 ) ) ⊆ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) → ( ∃ 𝑖 ∈ ( ( ( ⌊ ‘ ( 𝑃 / 4 ) ) + 1 ) ... ( ( 𝑃 − 1 ) / 2 ) ) 𝑥 = ( 𝑖 · 2 ) ↔ ∃ 𝑖 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ( 𝑖 ∈ ( ( ( ⌊ ‘ ( 𝑃 / 4 ) ) + 1 ) ... ( ( 𝑃 − 1 ) / 2 ) ) ∧ 𝑥 = ( 𝑖 · 2 ) ) ) )
13 10 11 12 3syl ⊢ ( ( ( 𝑃 ∈ ℙ ∧ ¬ 2 ∥ 𝑃 ) ∧ 𝑥 ∈ ℤ ) → ( ∃ 𝑖 ∈ ( ( ( ⌊ ‘ ( 𝑃 / 4 ) ) + 1 ) ... ( ( 𝑃 − 1 ) / 2 ) ) 𝑥 = ( 𝑖 · 2 ) ↔ ∃ 𝑖 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ( 𝑖 ∈ ( ( ( ⌊ ‘ ( 𝑃 / 4 ) ) + 1 ) ... ( ( 𝑃 − 1 ) / 2 ) ) ∧ 𝑥 = ( 𝑖 · 2 ) ) ) )
14 ancom ⊢ ( ( 𝑖 ∈ ( ( ( ⌊ ‘ ( 𝑃 / 4 ) ) + 1 ) ... ( ( 𝑃 − 1 ) / 2 ) ) ∧ 𝑥 = ( 𝑖 · 2 ) ) ↔ ( 𝑥 = ( 𝑖 · 2 ) ∧ 𝑖 ∈ ( ( ( ⌊ ‘ ( 𝑃 / 4 ) ) + 1 ) ... ( ( 𝑃 − 1 ) / 2 ) ) ) )
15 2 4 jctir ⊢ ( 𝑃 ∈ ℙ → ( 𝑃 ∈ ℕ0 ∧ 4 ∈ ℕ ) )
16 15 6 syl ⊢ ( 𝑃 ∈ ℙ → ( ⌊ ‘ ( 𝑃 / 4 ) ) ∈ ℕ0 )
17 16 nn0zd ⊢ ( 𝑃 ∈ ℙ → ( ⌊ ‘ ( 𝑃 / 4 ) ) ∈ ℤ )
18 17 ad2antrr ⊢ ( ( ( 𝑃 ∈ ℙ ∧ ¬ 2 ∥ 𝑃 ) ∧ 𝑥 ∈ ℤ ) → ( ⌊ ‘ ( 𝑃 / 4 ) ) ∈ ℤ )
19 elfzelz ⊢ ( 𝑖 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) → 𝑖 ∈ ℤ )
20 zltp1le ⊢ ( ( ( ⌊ ‘ ( 𝑃 / 4 ) ) ∈ ℤ ∧ 𝑖 ∈ ℤ ) → ( ( ⌊ ‘ ( 𝑃 / 4 ) ) < 𝑖 ↔ ( ( ⌊ ‘ ( 𝑃 / 4 ) ) + 1 ) ≤ 𝑖 ) )
21 18 19 20 syl2an ⊢ ( ( ( ( 𝑃 ∈ ℙ ∧ ¬ 2 ∥ 𝑃 ) ∧ 𝑥 ∈ ℤ ) ∧ 𝑖 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) → ( ( ⌊ ‘ ( 𝑃 / 4 ) ) < 𝑖 ↔ ( ( ⌊ ‘ ( 𝑃 / 4 ) ) + 1 ) ≤ 𝑖 ) )
22 21 bicomd ⊢ ( ( ( ( 𝑃 ∈ ℙ ∧ ¬ 2 ∥ 𝑃 ) ∧ 𝑥 ∈ ℤ ) ∧ 𝑖 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) → ( ( ( ⌊ ‘ ( 𝑃 / 4 ) ) + 1 ) ≤ 𝑖 ↔ ( ⌊ ‘ ( 𝑃 / 4 ) ) < 𝑖 ) )
23 22 anbi1d ⊢ ( ( ( ( 𝑃 ∈ ℙ ∧ ¬ 2 ∥ 𝑃 ) ∧ 𝑥 ∈ ℤ ) ∧ 𝑖 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) → ( ( ( ( ⌊ ‘ ( 𝑃 / 4 ) ) + 1 ) ≤ 𝑖 ∧ 𝑖 ≤ ( ( 𝑃 − 1 ) / 2 ) ) ↔ ( ( ⌊ ‘ ( 𝑃 / 4 ) ) < 𝑖 ∧ 𝑖 ≤ ( ( 𝑃 − 1 ) / 2 ) ) ) )
24 19 adantl ⊢ ( ( ( ( 𝑃 ∈ ℙ ∧ ¬ 2 ∥ 𝑃 ) ∧ 𝑥 ∈ ℤ ) ∧ 𝑖 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) → 𝑖 ∈ ℤ )
25 17 peano2zd ⊢ ( 𝑃 ∈ ℙ → ( ( ⌊ ‘ ( 𝑃 / 4 ) ) + 1 ) ∈ ℤ )
26 25 adantr ⊢ ( ( 𝑃 ∈ ℙ ∧ ¬ 2 ∥ 𝑃 ) → ( ( ⌊ ‘ ( 𝑃 / 4 ) ) + 1 ) ∈ ℤ )
27 26 ad2antrr ⊢ ( ( ( ( 𝑃 ∈ ℙ ∧ ¬ 2 ∥ 𝑃 ) ∧ 𝑥 ∈ ℤ ) ∧ 𝑖 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) → ( ( ⌊ ‘ ( 𝑃 / 4 ) ) + 1 ) ∈ ℤ )
28 prmz ⊢ ( 𝑃 ∈ ℙ → 𝑃 ∈ ℤ )
29 oddm1d2 ⊢ ( 𝑃 ∈ ℤ → ( ¬ 2 ∥ 𝑃 ↔ ( ( 𝑃 − 1 ) / 2 ) ∈ ℤ ) )
30 28 29 syl ⊢ ( 𝑃 ∈ ℙ → ( ¬ 2 ∥ 𝑃 ↔ ( ( 𝑃 − 1 ) / 2 ) ∈ ℤ ) )
31 30 biimpa ⊢ ( ( 𝑃 ∈ ℙ ∧ ¬ 2 ∥ 𝑃 ) → ( ( 𝑃 − 1 ) / 2 ) ∈ ℤ )
32 31 ad2antrr ⊢ ( ( ( ( 𝑃 ∈ ℙ ∧ ¬ 2 ∥ 𝑃 ) ∧ 𝑥 ∈ ℤ ) ∧ 𝑖 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) → ( ( 𝑃 − 1 ) / 2 ) ∈ ℤ )
33 elfz ⊢ ( ( 𝑖 ∈ ℤ ∧ ( ( ⌊ ‘ ( 𝑃 / 4 ) ) + 1 ) ∈ ℤ ∧ ( ( 𝑃 − 1 ) / 2 ) ∈ ℤ ) → ( 𝑖 ∈ ( ( ( ⌊ ‘ ( 𝑃 / 4 ) ) + 1 ) ... ( ( 𝑃 − 1 ) / 2 ) ) ↔ ( ( ( ⌊ ‘ ( 𝑃 / 4 ) ) + 1 ) ≤ 𝑖 ∧ 𝑖 ≤ ( ( 𝑃 − 1 ) / 2 ) ) ) )
34 24 27 32 33 syl3anc ⊢ ( ( ( ( 𝑃 ∈ ℙ ∧ ¬ 2 ∥ 𝑃 ) ∧ 𝑥 ∈ ℤ ) ∧ 𝑖 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) → ( 𝑖 ∈ ( ( ( ⌊ ‘ ( 𝑃 / 4 ) ) + 1 ) ... ( ( 𝑃 − 1 ) / 2 ) ) ↔ ( ( ( ⌊ ‘ ( 𝑃 / 4 ) ) + 1 ) ≤ 𝑖 ∧ 𝑖 ≤ ( ( 𝑃 − 1 ) / 2 ) ) ) )
35 elfzle2 ⊢ ( 𝑖 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) → 𝑖 ≤ ( ( 𝑃 − 1 ) / 2 ) )
36 35 adantl ⊢ ( ( ( ( 𝑃 ∈ ℙ ∧ ¬ 2 ∥ 𝑃 ) ∧ 𝑥 ∈ ℤ ) ∧ 𝑖 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) → 𝑖 ≤ ( ( 𝑃 − 1 ) / 2 ) )
37 36 biantrud ⊢ ( ( ( ( 𝑃 ∈ ℙ ∧ ¬ 2 ∥ 𝑃 ) ∧ 𝑥 ∈ ℤ ) ∧ 𝑖 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) → ( ( ⌊ ‘ ( 𝑃 / 4 ) ) < 𝑖 ↔ ( ( ⌊ ‘ ( 𝑃 / 4 ) ) < 𝑖 ∧ 𝑖 ≤ ( ( 𝑃 − 1 ) / 2 ) ) ) )
38 23 34 37 3bitr4d ⊢ ( ( ( ( 𝑃 ∈ ℙ ∧ ¬ 2 ∥ 𝑃 ) ∧ 𝑥 ∈ ℤ ) ∧ 𝑖 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) → ( 𝑖 ∈ ( ( ( ⌊ ‘ ( 𝑃 / 4 ) ) + 1 ) ... ( ( 𝑃 − 1 ) / 2 ) ) ↔ ( ⌊ ‘ ( 𝑃 / 4 ) ) < 𝑖 ) )
39 28 ad2antrr ⊢ ( ( ( 𝑃 ∈ ℙ ∧ ¬ 2 ∥ 𝑃 ) ∧ 𝑥 ∈ ℤ ) → 𝑃 ∈ ℤ )
40 2lgslem1a2 ⊢ ( ( 𝑃 ∈ ℤ ∧ 𝑖 ∈ ℤ ) → ( ( ⌊ ‘ ( 𝑃 / 4 ) ) < 𝑖 ↔ ( 𝑃 / 2 ) < ( 𝑖 · 2 ) ) )
41 39 19 40 syl2an ⊢ ( ( ( ( 𝑃 ∈ ℙ ∧ ¬ 2 ∥ 𝑃 ) ∧ 𝑥 ∈ ℤ ) ∧ 𝑖 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) → ( ( ⌊ ‘ ( 𝑃 / 4 ) ) < 𝑖 ↔ ( 𝑃 / 2 ) < ( 𝑖 · 2 ) ) )
42 38 41 bitrd ⊢ ( ( ( ( 𝑃 ∈ ℙ ∧ ¬ 2 ∥ 𝑃 ) ∧ 𝑥 ∈ ℤ ) ∧ 𝑖 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) → ( 𝑖 ∈ ( ( ( ⌊ ‘ ( 𝑃 / 4 ) ) + 1 ) ... ( ( 𝑃 − 1 ) / 2 ) ) ↔ ( 𝑃 / 2 ) < ( 𝑖 · 2 ) ) )
43 2lgslem1a1 ⊢ ( ( 𝑃 ∈ ℕ ∧ ¬ 2 ∥ 𝑃 ) → ∀ 𝑘 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ( 𝑘 · 2 ) = ( ( 𝑘 · 2 ) mod 𝑃 ) )
44 1 43 sylan ⊢ ( ( 𝑃 ∈ ℙ ∧ ¬ 2 ∥ 𝑃 ) → ∀ 𝑘 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ( 𝑘 · 2 ) = ( ( 𝑘 · 2 ) mod 𝑃 ) )
45 44 adantr ⊢ ( ( ( 𝑃 ∈ ℙ ∧ ¬ 2 ∥ 𝑃 ) ∧ 𝑥 ∈ ℤ ) → ∀ 𝑘 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ( 𝑘 · 2 ) = ( ( 𝑘 · 2 ) mod 𝑃 ) )
46 oveq1 ⊢ ( 𝑘 = 𝑖 → ( 𝑘 · 2 ) = ( 𝑖 · 2 ) )
47 46 oveq1d ⊢ ( 𝑘 = 𝑖 → ( ( 𝑘 · 2 ) mod 𝑃 ) = ( ( 𝑖 · 2 ) mod 𝑃 ) )
48 46 47 eqeq12d ⊢ ( 𝑘 = 𝑖 → ( ( 𝑘 · 2 ) = ( ( 𝑘 · 2 ) mod 𝑃 ) ↔ ( 𝑖 · 2 ) = ( ( 𝑖 · 2 ) mod 𝑃 ) ) )
49 48 rspccva ⊢ ( ( ∀ 𝑘 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ( 𝑘 · 2 ) = ( ( 𝑘 · 2 ) mod 𝑃 ) ∧ 𝑖 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) → ( 𝑖 · 2 ) = ( ( 𝑖 · 2 ) mod 𝑃 ) )
50 45 49 sylan ⊢ ( ( ( ( 𝑃 ∈ ℙ ∧ ¬ 2 ∥ 𝑃 ) ∧ 𝑥 ∈ ℤ ) ∧ 𝑖 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) → ( 𝑖 · 2 ) = ( ( 𝑖 · 2 ) mod 𝑃 ) )
51 50 breq2d ⊢ ( ( ( ( 𝑃 ∈ ℙ ∧ ¬ 2 ∥ 𝑃 ) ∧ 𝑥 ∈ ℤ ) ∧ 𝑖 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) → ( ( 𝑃 / 2 ) < ( 𝑖 · 2 ) ↔ ( 𝑃 / 2 ) < ( ( 𝑖 · 2 ) mod 𝑃 ) ) )
52 42 51 bitrd ⊢ ( ( ( ( 𝑃 ∈ ℙ ∧ ¬ 2 ∥ 𝑃 ) ∧ 𝑥 ∈ ℤ ) ∧ 𝑖 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) → ( 𝑖 ∈ ( ( ( ⌊ ‘ ( 𝑃 / 4 ) ) + 1 ) ... ( ( 𝑃 − 1 ) / 2 ) ) ↔ ( 𝑃 / 2 ) < ( ( 𝑖 · 2 ) mod 𝑃 ) ) )
53 oveq1 ⊢ ( 𝑥 = ( 𝑖 · 2 ) → ( 𝑥 mod 𝑃 ) = ( ( 𝑖 · 2 ) mod 𝑃 ) )
54 53 eqcomd ⊢ ( 𝑥 = ( 𝑖 · 2 ) → ( ( 𝑖 · 2 ) mod 𝑃 ) = ( 𝑥 mod 𝑃 ) )
55 54 breq2d ⊢ ( 𝑥 = ( 𝑖 · 2 ) → ( ( 𝑃 / 2 ) < ( ( 𝑖 · 2 ) mod 𝑃 ) ↔ ( 𝑃 / 2 ) < ( 𝑥 mod 𝑃 ) ) )
56 52 55 sylan9bb ⊢ ( ( ( ( ( 𝑃 ∈ ℙ ∧ ¬ 2 ∥ 𝑃 ) ∧ 𝑥 ∈ ℤ ) ∧ 𝑖 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ∧ 𝑥 = ( 𝑖 · 2 ) ) → ( 𝑖 ∈ ( ( ( ⌊ ‘ ( 𝑃 / 4 ) ) + 1 ) ... ( ( 𝑃 − 1 ) / 2 ) ) ↔ ( 𝑃 / 2 ) < ( 𝑥 mod 𝑃 ) ) )
57 56 pm5.32da ⊢ ( ( ( ( 𝑃 ∈ ℙ ∧ ¬ 2 ∥ 𝑃 ) ∧ 𝑥 ∈ ℤ ) ∧ 𝑖 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) → ( ( 𝑥 = ( 𝑖 · 2 ) ∧ 𝑖 ∈ ( ( ( ⌊ ‘ ( 𝑃 / 4 ) ) + 1 ) ... ( ( 𝑃 − 1 ) / 2 ) ) ) ↔ ( 𝑥 = ( 𝑖 · 2 ) ∧ ( 𝑃 / 2 ) < ( 𝑥 mod 𝑃 ) ) ) )
58 14 57 syl5bb ⊢ ( ( ( ( 𝑃 ∈ ℙ ∧ ¬ 2 ∥ 𝑃 ) ∧ 𝑥 ∈ ℤ ) ∧ 𝑖 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) → ( ( 𝑖 ∈ ( ( ( ⌊ ‘ ( 𝑃 / 4 ) ) + 1 ) ... ( ( 𝑃 − 1 ) / 2 ) ) ∧ 𝑥 = ( 𝑖 · 2 ) ) ↔ ( 𝑥 = ( 𝑖 · 2 ) ∧ ( 𝑃 / 2 ) < ( 𝑥 mod 𝑃 ) ) ) )
59 58 rexbidva ⊢ ( ( ( 𝑃 ∈ ℙ ∧ ¬ 2 ∥ 𝑃 ) ∧ 𝑥 ∈ ℤ ) → ( ∃ 𝑖 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ( 𝑖 ∈ ( ( ( ⌊ ‘ ( 𝑃 / 4 ) ) + 1 ) ... ( ( 𝑃 − 1 ) / 2 ) ) ∧ 𝑥 = ( 𝑖 · 2 ) ) ↔ ∃ 𝑖 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ( 𝑥 = ( 𝑖 · 2 ) ∧ ( 𝑃 / 2 ) < ( 𝑥 mod 𝑃 ) ) ) )
60 13 59 bitrd ⊢ ( ( ( 𝑃 ∈ ℙ ∧ ¬ 2 ∥ 𝑃 ) ∧ 𝑥 ∈ ℤ ) → ( ∃ 𝑖 ∈ ( ( ( ⌊ ‘ ( 𝑃 / 4 ) ) + 1 ) ... ( ( 𝑃 − 1 ) / 2 ) ) 𝑥 = ( 𝑖 · 2 ) ↔ ∃ 𝑖 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ( 𝑥 = ( 𝑖 · 2 ) ∧ ( 𝑃 / 2 ) < ( 𝑥 mod 𝑃 ) ) ) )
61 60 bicomd ⊢ ( ( ( 𝑃 ∈ ℙ ∧ ¬ 2 ∥ 𝑃 ) ∧ 𝑥 ∈ ℤ ) → ( ∃ 𝑖 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ( 𝑥 = ( 𝑖 · 2 ) ∧ ( 𝑃 / 2 ) < ( 𝑥 mod 𝑃 ) ) ↔ ∃ 𝑖 ∈ ( ( ( ⌊ ‘ ( 𝑃 / 4 ) ) + 1 ) ... ( ( 𝑃 − 1 ) / 2 ) ) 𝑥 = ( 𝑖 · 2 ) ) )
62 61 rabbidva ⊢ ( ( 𝑃 ∈ ℙ ∧ ¬ 2 ∥ 𝑃 ) → { 𝑥 ∈ ℤ ∣ ∃ 𝑖 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ( 𝑥 = ( 𝑖 · 2 ) ∧ ( 𝑃 / 2 ) < ( 𝑥 mod 𝑃 ) ) } = { 𝑥 ∈ ℤ ∣ ∃ 𝑖 ∈ ( ( ( ⌊ ‘ ( 𝑃 / 4 ) ) + 1 ) ... ( ( 𝑃 − 1 ) / 2 ) ) 𝑥 = ( 𝑖 · 2 ) } )