Metamath Proof Explorer

Theorem wlkiswwlks2lem1

Description: Lemma 1 for wlkiswwlks2 . (Contributed by Alexander van der Vekens, 20-Jul-2018)

Ref Expression
Hypothesis wlkiswwlks2lem.f ⊢ F = x ∈ 0 ..^ P − 1 ⟼ E -1 ⁡ P ⁡ x P ⁡ x + 1
Assertion wlkiswwlks2lem1 ⊢ P ∈ Word V ∧ 1 ≤ P → F = P − 1

Proof

Step Hyp Ref Expression
1 wlkiswwlks2lem.f ⊢ F = x ∈ 0 ..^ P − 1 ⟼ E -1 ⁡ P ⁡ x P ⁡ x + 1
2 lencl ⊢ P ∈ Word V → P ∈ ℕ 0
3 elnnnn0c ⊢ P ∈ ℕ ↔ P ∈ ℕ 0 ∧ 1 ≤ P
4 3 biimpri ⊢ P ∈ ℕ 0 ∧ 1 ≤ P → P ∈ ℕ
5 2 4 sylan ⊢ P ∈ Word V ∧ 1 ≤ P → P ∈ ℕ
6 nnm1nn0 ⊢ P ∈ ℕ → P − 1 ∈ ℕ 0
7 5 6 syl ⊢ P ∈ Word V ∧ 1 ≤ P → P − 1 ∈ ℕ 0
8 fvex ⊢ E -1 ⁡ P ⁡ x P ⁡ x + 1 ∈ V
9 8 1 fnmpti ⊢ F Fn 0 ..^ P − 1
10 ffzo0hash ⊢ P − 1 ∈ ℕ 0 ∧ F Fn 0 ..^ P − 1 → F = P − 1
11 7 9 10 sylancl ⊢ P ∈ Word V ∧ 1 ≤ P → F = P − 1