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−12x=i⋅2∧P2<xmodP=P−12−P4

Proof

Step Hyp Ref Expression
1 2lgslem1a ⊢P∈ℙ∧¬2∥P→x∈ℤ|∃i∈1…P−12x=i⋅2∧P2<xmodP=x∈ℤ|∃i∈P4+1…P−12x=i⋅2
2 1 fveq2d ⊢P∈ℙ∧¬2∥P→x∈ℤ|∃i∈1…P−12x=i⋅2∧P2<xmodP=x∈ℤ|∃i∈P4+1…P−12x=i⋅2
3 ovex ⊢P4+1…P−12∈V
4 3 mptex ⊢y∈P4+1…P−12⟼y⋅2∈V
5 f1oeq1 ⊢f=y∈P4+1…P−12⟼y⋅2→f:P4+1…P−12⟶1-1 ontox∈ℤ|∃i∈P4+1…P−12x=i⋅2↔y∈P4+1…P−12⟼y⋅2:P4+1…P−12⟶1-1 ontox∈ℤ|∃i∈P4+1…P−12x=i⋅2
6 eqid ⊢P4+1…P−12=P4+1…P−12
7 eqid ⊢y∈P4+1…P−12⟼y⋅2=y∈P4+1…P−12⟼y⋅2
8 6 7 2lgslem1b ⊢y∈P4+1…P−12⟼y⋅2:P4+1…P−12⟶1-1 ontox∈ℤ|∃i∈P4+1…P−12x=i⋅2
9 4 5 8 ceqsexv2d ⊢∃ff:P4+1…P−12⟶1-1 ontox∈ℤ|∃i∈P4+1…P−12x=i⋅2
10 9 a1i ⊢P∈ℙ∧¬2∥P→∃ff:P4+1…P−12⟶1-1 ontox∈ℤ|∃i∈P4+1…P−12x=i⋅2
11 hasheqf1oi ⊢P4+1…P−12∈V→∃ff:P4+1…P−12⟶1-1 ontox∈ℤ|∃i∈P4+1…P−12x=i⋅2→P4+1…P−12=x∈ℤ|∃i∈P4+1…P−12x=i⋅2
12 3 10 11 mpsyl ⊢P∈ℙ∧¬2∥P→P4+1…P−12=x∈ℤ|∃i∈P4+1…P−12x=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∈ℙ→P4∈ℝ
20 19 flcld ⊢P∈ℙ→P4∈ℤ
21 20 adantr ⊢P∈ℙ∧¬2∥P→P4∈ℤ
22 oddm1d2 ⊢P∈ℤ→¬2∥P↔P−12∈ℤ
23 13 22 syl ⊢P∈ℙ→¬2∥P↔P−12∈ℤ
24 23 biimpa ⊢P∈ℙ∧¬2∥P→P−12∈ℤ
25 2lgslem1c ⊢P∈ℙ∧¬2∥P→P4≤P−12
26 eluz2 ⊢P−12∈ℤ≥P4↔P4∈ℤ∧P−12∈ℤ∧P4≤P−12
27 21 24 25 26 syl3anbrc ⊢P∈ℙ∧¬2∥P→P−12∈ℤ≥P4
28 hashfzp1 ⊢P−12∈ℤ≥P4→P4+1…P−12=P−12−P4
29 27 28 syl ⊢P∈ℙ∧¬2∥P→P4+1…P−12=P−12−P4
30 2 12 29 3eqtr2d ⊢P∈ℙ∧¬2∥P→x∈ℤ|∃i∈1…P−12x=i⋅2∧P2<xmodP=P−12−P4