Metamath Proof Explorer

Theorem 2lgslem1

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

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

Proof

Step Hyp Ref Expression
1 2lgslem1a ⊢ ( ( 𝑃 ∈ ℙ ∧ ¬ 2 ∥ 𝑃 ) → { 𝑥 ∈ ℤ ∣ ∃ 𝑖 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ( 𝑥 = ( 𝑖 · 2 ) ∧ ( 𝑃 / 2 ) < ( 𝑥 mod 𝑃 ) ) } = { 𝑥 ∈ ℤ ∣ ∃ 𝑖 ∈ ( ( ( ⌊ ‘ ( 𝑃 / 4 ) ) + 1 ) ... ( ( 𝑃 − 1 ) / 2 ) ) 𝑥 = ( 𝑖 · 2 ) } )
2 1 fveq2d ⊢ ( ( 𝑃 ∈ ℙ ∧ ¬ 2 ∥ 𝑃 ) → ( ♯ ‘ { 𝑥 ∈ ℤ ∣ ∃ 𝑖 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ( 𝑥 = ( 𝑖 · 2 ) ∧ ( 𝑃 / 2 ) < ( 𝑥 mod 𝑃 ) ) } ) = ( ♯ ‘ { 𝑥 ∈ ℤ ∣ ∃ 𝑖 ∈ ( ( ( ⌊ ‘ ( 𝑃 / 4 ) ) + 1 ) ... ( ( 𝑃 − 1 ) / 2 ) ) 𝑥 = ( 𝑖 · 2 ) } ) )
3 ovex ⊢ ( ( ( ⌊ ‘ ( 𝑃 / 4 ) ) + 1 ) ... ( ( 𝑃 − 1 ) / 2 ) ) ∈ V
4 3 mptex ⊢ ( 𝑦 ∈ ( ( ( ⌊ ‘ ( 𝑃 / 4 ) ) + 1 ) ... ( ( 𝑃 − 1 ) / 2 ) ) ↦ ( 𝑦 · 2 ) ) ∈ V
5 f1oeq1 ⊢ ( 𝑓 = ( 𝑦 ∈ ( ( ( ⌊ ‘ ( 𝑃 / 4 ) ) + 1 ) ... ( ( 𝑃 − 1 ) / 2 ) ) ↦ ( 𝑦 · 2 ) ) → ( 𝑓 : ( ( ( ⌊ ‘ ( 𝑃 / 4 ) ) + 1 ) ... ( ( 𝑃 − 1 ) / 2 ) ) –1-1-onto→ { 𝑥 ∈ ℤ ∣ ∃ 𝑖 ∈ ( ( ( ⌊ ‘ ( 𝑃 / 4 ) ) + 1 ) ... ( ( 𝑃 − 1 ) / 2 ) ) 𝑥 = ( 𝑖 · 2 ) } ↔ ( 𝑦 ∈ ( ( ( ⌊ ‘ ( 𝑃 / 4 ) ) + 1 ) ... ( ( 𝑃 − 1 ) / 2 ) ) ↦ ( 𝑦 · 2 ) ) : ( ( ( ⌊ ‘ ( 𝑃 / 4 ) ) + 1 ) ... ( ( 𝑃 − 1 ) / 2 ) ) –1-1-onto→ { 𝑥 ∈ ℤ ∣ ∃ 𝑖 ∈ ( ( ( ⌊ ‘ ( 𝑃 / 4 ) ) + 1 ) ... ( ( 𝑃 − 1 ) / 2 ) ) 𝑥 = ( 𝑖 · 2 ) } ) )
6 eqid ⊢ ( ( ( ⌊ ‘ ( 𝑃 / 4 ) ) + 1 ) ... ( ( 𝑃 − 1 ) / 2 ) ) = ( ( ( ⌊ ‘ ( 𝑃 / 4 ) ) + 1 ) ... ( ( 𝑃 − 1 ) / 2 ) )
7 eqid ⊢ ( 𝑦 ∈ ( ( ( ⌊ ‘ ( 𝑃 / 4 ) ) + 1 ) ... ( ( 𝑃 − 1 ) / 2 ) ) ↦ ( 𝑦 · 2 ) ) = ( 𝑦 ∈ ( ( ( ⌊ ‘ ( 𝑃 / 4 ) ) + 1 ) ... ( ( 𝑃 − 1 ) / 2 ) ) ↦ ( 𝑦 · 2 ) )
8 6 7 2lgslem1b ⊢ ( 𝑦 ∈ ( ( ( ⌊ ‘ ( 𝑃 / 4 ) ) + 1 ) ... ( ( 𝑃 − 1 ) / 2 ) ) ↦ ( 𝑦 · 2 ) ) : ( ( ( ⌊ ‘ ( 𝑃 / 4 ) ) + 1 ) ... ( ( 𝑃 − 1 ) / 2 ) ) –1-1-onto→ { 𝑥 ∈ ℤ ∣ ∃ 𝑖 ∈ ( ( ( ⌊ ‘ ( 𝑃 / 4 ) ) + 1 ) ... ( ( 𝑃 − 1 ) / 2 ) ) 𝑥 = ( 𝑖 · 2 ) }
9 4 5 8 ceqsexv2d ⊢ ∃ 𝑓 𝑓 : ( ( ( ⌊ ‘ ( 𝑃 / 4 ) ) + 1 ) ... ( ( 𝑃 − 1 ) / 2 ) ) –1-1-onto→ { 𝑥 ∈ ℤ ∣ ∃ 𝑖 ∈ ( ( ( ⌊ ‘ ( 𝑃 / 4 ) ) + 1 ) ... ( ( 𝑃 − 1 ) / 2 ) ) 𝑥 = ( 𝑖 · 2 ) }
10 9 a1i ⊢ ( ( 𝑃 ∈ ℙ ∧ ¬ 2 ∥ 𝑃 ) → ∃ 𝑓 𝑓 : ( ( ( ⌊ ‘ ( 𝑃 / 4 ) ) + 1 ) ... ( ( 𝑃 − 1 ) / 2 ) ) –1-1-onto→ { 𝑥 ∈ ℤ ∣ ∃ 𝑖 ∈ ( ( ( ⌊ ‘ ( 𝑃 / 4 ) ) + 1 ) ... ( ( 𝑃 − 1 ) / 2 ) ) 𝑥 = ( 𝑖 · 2 ) } )
11 hasheqf1oi ⊢ ( ( ( ( ⌊ ‘ ( 𝑃 / 4 ) ) + 1 ) ... ( ( 𝑃 − 1 ) / 2 ) ) ∈ V → ( ∃ 𝑓 𝑓 : ( ( ( ⌊ ‘ ( 𝑃 / 4 ) ) + 1 ) ... ( ( 𝑃 − 1 ) / 2 ) ) –1-1-onto→ { 𝑥 ∈ ℤ ∣ ∃ 𝑖 ∈ ( ( ( ⌊ ‘ ( 𝑃 / 4 ) ) + 1 ) ... ( ( 𝑃 − 1 ) / 2 ) ) 𝑥 = ( 𝑖 · 2 ) } → ( ♯ ‘ ( ( ( ⌊ ‘ ( 𝑃 / 4 ) ) + 1 ) ... ( ( 𝑃 − 1 ) / 2 ) ) ) = ( ♯ ‘ { 𝑥 ∈ ℤ ∣ ∃ 𝑖 ∈ ( ( ( ⌊ ‘ ( 𝑃 / 4 ) ) + 1 ) ... ( ( 𝑃 − 1 ) / 2 ) ) 𝑥 = ( 𝑖 · 2 ) } ) ) )
12 3 10 11 mpsyl ⊢ ( ( 𝑃 ∈ ℙ ∧ ¬ 2 ∥ 𝑃 ) → ( ♯ ‘ ( ( ( ⌊ ‘ ( 𝑃 / 4 ) ) + 1 ) ... ( ( 𝑃 − 1 ) / 2 ) ) ) = ( ♯ ‘ { 𝑥 ∈ ℤ ∣ ∃ 𝑖 ∈ ( ( ( ⌊ ‘ ( 𝑃 / 4 ) ) + 1 ) ... ( ( 𝑃 − 1 ) / 2 ) ) 𝑥 = ( 𝑖 · 2 ) } ) )
13 prmz ⊢ ( 𝑃 ∈ ℙ → 𝑃 ∈ ℤ )
14 13 zred ⊢ ( 𝑃 ∈ ℙ → 𝑃 ∈ ℝ )
15 4re ⊢ 4 ∈ ℝ
16 15 a1i ⊢ ( 𝑃 ∈ ℙ → 4 ∈ ℝ )
17 4ne0 ⊢ 4 ≠ 0
18 17 a1i ⊢ ( 𝑃 ∈ ℙ → 4 ≠ 0 )
19 14 16 18 redivcld ⊢ ( 𝑃 ∈ ℙ → ( 𝑃 / 4 ) ∈ ℝ )
20 19 flcld ⊢ ( 𝑃 ∈ ℙ → ( ⌊ ‘ ( 𝑃 / 4 ) ) ∈ ℤ )
21 20 adantr ⊢ ( ( 𝑃 ∈ ℙ ∧ ¬ 2 ∥ 𝑃 ) → ( ⌊ ‘ ( 𝑃 / 4 ) ) ∈ ℤ )
22 oddm1d2 ⊢ ( 𝑃 ∈ ℤ → ( ¬ 2 ∥ 𝑃 ↔ ( ( 𝑃 − 1 ) / 2 ) ∈ ℤ ) )
23 13 22 syl ⊢ ( 𝑃 ∈ ℙ → ( ¬ 2 ∥ 𝑃 ↔ ( ( 𝑃 − 1 ) / 2 ) ∈ ℤ ) )
24 23 biimpa ⊢ ( ( 𝑃 ∈ ℙ ∧ ¬ 2 ∥ 𝑃 ) → ( ( 𝑃 − 1 ) / 2 ) ∈ ℤ )
25 2lgslem1c ⊢ ( ( 𝑃 ∈ ℙ ∧ ¬ 2 ∥ 𝑃 ) → ( ⌊ ‘ ( 𝑃 / 4 ) ) ≤ ( ( 𝑃 − 1 ) / 2 ) )
26 eluz2 ⊢ ( ( ( 𝑃 − 1 ) / 2 ) ∈ ( ℤ≥ ‘ ( ⌊ ‘ ( 𝑃 / 4 ) ) ) ↔ ( ( ⌊ ‘ ( 𝑃 / 4 ) ) ∈ ℤ ∧ ( ( 𝑃 − 1 ) / 2 ) ∈ ℤ ∧ ( ⌊ ‘ ( 𝑃 / 4 ) ) ≤ ( ( 𝑃 − 1 ) / 2 ) ) )
27 21 24 25 26 syl3anbrc ⊢ ( ( 𝑃 ∈ ℙ ∧ ¬ 2 ∥ 𝑃 ) → ( ( 𝑃 − 1 ) / 2 ) ∈ ( ℤ≥ ‘ ( ⌊ ‘ ( 𝑃 / 4 ) ) ) )
28 hashfzp1 ⊢ ( ( ( 𝑃 − 1 ) / 2 ) ∈ ( ℤ≥ ‘ ( ⌊ ‘ ( 𝑃 / 4 ) ) ) → ( ♯ ‘ ( ( ( ⌊ ‘ ( 𝑃 / 4 ) ) + 1 ) ... ( ( 𝑃 − 1 ) / 2 ) ) ) = ( ( ( 𝑃 − 1 ) / 2 ) − ( ⌊ ‘ ( 𝑃 / 4 ) ) ) )
29 27 28 syl ⊢ ( ( 𝑃 ∈ ℙ ∧ ¬ 2 ∥ 𝑃 ) → ( ♯ ‘ ( ( ( ⌊ ‘ ( 𝑃 / 4 ) ) + 1 ) ... ( ( 𝑃 − 1 ) / 2 ) ) ) = ( ( ( 𝑃 − 1 ) / 2 ) − ( ⌊ ‘ ( 𝑃 / 4 ) ) ) )
30 2 12 29 3eqtr2d ⊢ ( ( 𝑃 ∈ ℙ ∧ ¬ 2 ∥ 𝑃 ) → ( ♯ ‘ { 𝑥 ∈ ℤ ∣ ∃ 𝑖 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ( 𝑥 = ( 𝑖 · 2 ) ∧ ( 𝑃 / 2 ) < ( 𝑥 mod 𝑃 ) ) } ) = ( ( ( 𝑃 − 1 ) / 2 ) − ( ⌊ ‘ ( 𝑃 / 4 ) ) ) )