Metamath Proof Explorer

Theorem 2lgslem1

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

Ref Expression
Assertion 2lgslem1 ⊢ P ∈ ℙ ∧ ¬ 2 ∥ P → x ∈ ℤ | ∃ i ∈ 1 … P − 1 2 x = i ⋅ 2 ∧ P 2 < x mod P = P − 1 2 − P 4

Proof

Step Hyp Ref Expression
1 2lgslem1a ⊢ P ∈ ℙ ∧ ¬ 2 ∥ P → x ∈ ℤ | ∃ i ∈ 1 … P − 1 2 x = i ⋅ 2 ∧ P 2 < x mod P = x ∈ ℤ | ∃ i ∈ P 4 + 1 … P − 1 2 x = i ⋅ 2
2 1 fveq2d ⊢ P ∈ ℙ ∧ ¬ 2 ∥ P → x ∈ ℤ | ∃ i ∈ 1 … P − 1 2 x = i ⋅ 2 ∧ P 2 < x mod P = x ∈ ℤ | ∃ i ∈ P 4 + 1 … P − 1 2 x = i ⋅ 2
3 ovex ⊢ P 4 + 1 … P − 1 2 ∈ V
4 3 mptex ⊢ y ∈ P 4 + 1 … P − 1 2 ⟼ y ⋅ 2 ∈ V
5 f1oeq1 ⊢ f = y ∈ P 4 + 1 … P − 1 2 ⟼ y ⋅ 2 → f : P 4 + 1 … P − 1 2 ⟶ 1-1 onto x ∈ ℤ | ∃ i ∈ P 4 + 1 … P − 1 2 x = i ⋅ 2 ↔ y ∈ P 4 + 1 … P − 1 2 ⟼ y ⋅ 2 : P 4 + 1 … P − 1 2 ⟶ 1-1 onto x ∈ ℤ | ∃ i ∈ P 4 + 1 … P − 1 2 x = i ⋅ 2
6 eqid ⊢ P 4 + 1 … P − 1 2 = P 4 + 1 … P − 1 2
7 eqid ⊢ y ∈ P 4 + 1 … P − 1 2 ⟼ y ⋅ 2 = y ∈ P 4 + 1 … P − 1 2 ⟼ y ⋅ 2
8 6 7 2lgslem1b ⊢ y ∈ P 4 + 1 … P − 1 2 ⟼ y ⋅ 2 : P 4 + 1 … P − 1 2 ⟶ 1-1 onto x ∈ ℤ | ∃ i ∈ P 4 + 1 … P − 1 2 x = i ⋅ 2
9 4 5 8 ceqsexv2d ⊢ ∃ f f : P 4 + 1 … P − 1 2 ⟶ 1-1 onto x ∈ ℤ | ∃ i ∈ P 4 + 1 … P − 1 2 x = i ⋅ 2
10 9 a1i ⊢ P ∈ ℙ ∧ ¬ 2 ∥ P → ∃ f f : P 4 + 1 … P − 1 2 ⟶ 1-1 onto x ∈ ℤ | ∃ i ∈ P 4 + 1 … P − 1 2 x = i ⋅ 2
11 hasheqf1oi ⊢ P 4 + 1 … P − 1 2 ∈ V → ∃ f f : P 4 + 1 … P − 1 2 ⟶ 1-1 onto x ∈ ℤ | ∃ i ∈ P 4 + 1 … P − 1 2 x = i ⋅ 2 → P 4 + 1 … P − 1 2 = x ∈ ℤ | ∃ i ∈ P 4 + 1 … P − 1 2 x = i ⋅ 2
12 3 10 11 mpsyl ⊢ P ∈ ℙ ∧ ¬ 2 ∥ P → P 4 + 1 … P − 1 2 = x ∈ ℤ | ∃ i ∈ P 4 + 1 … P − 1 2 x = i ⋅ 2
13 prmz ⊢ P ∈ ℙ → P ∈ ℤ
14 13 zred ⊢ P ∈ ℙ → P ∈ ℝ
15 4re ⊢ 4 ∈ ℝ
16 15 a1i ⊢ P ∈ ℙ → 4 ∈ ℝ
17 4ne0 ⊢ 4 ≠ 0
18 17 a1i ⊢ P ∈ ℙ → 4 ≠ 0
19 14 16 18 redivcld ⊢ P ∈ ℙ → P 4 ∈ ℝ
20 19 flcld ⊢ P ∈ ℙ → P 4 ∈ ℤ
21 20 adantr ⊢ P ∈ ℙ ∧ ¬ 2 ∥ P → P 4 ∈ ℤ
22 oddm1d2 ⊢ P ∈ ℤ → ¬ 2 ∥ P ↔ P − 1 2 ∈ ℤ
23 13 22 syl ⊢ P ∈ ℙ → ¬ 2 ∥ P ↔ P − 1 2 ∈ ℤ
24 23 biimpa ⊢ P ∈ ℙ ∧ ¬ 2 ∥ P → P − 1 2 ∈ ℤ
25 2lgslem1c ⊢ P ∈ ℙ ∧ ¬ 2 ∥ P → P 4 ≤ P − 1 2
26 eluz2 ⊢ P − 1 2 ∈ ℤ ≥ P 4 ↔ P 4 ∈ ℤ ∧ P − 1 2 ∈ ℤ ∧ P 4 ≤ P − 1 2
27 21 24 25 26 syl3anbrc ⊢ P ∈ ℙ ∧ ¬ 2 ∥ P → P − 1 2 ∈ ℤ ≥ P 4
28 hashfzp1 ⊢ P − 1 2 ∈ ℤ ≥ P 4 → P 4 + 1 … P − 1 2 = P − 1 2 − P 4
29 27 28 syl ⊢ P ∈ ℙ ∧ ¬ 2 ∥ P → P 4 + 1 … P − 1 2 = P − 1 2 − P 4
30 2 12 29 3eqtr2d ⊢ P ∈ ℙ ∧ ¬ 2 ∥ P → x ∈ ℤ | ∃ i ∈ 1 … P − 1 2 x = i ⋅ 2 ∧ P 2 < x mod P = P − 1 2 − P 4