Metamath Proof Explorer

Theorem clwlkclwwlklem2a2

Description: Lemma 2 for clwlkclwwlklem2a . (Contributed by Alexander van der Vekens, 21-Jun-2018)

Ref Expression
Hypothesis clwlkclwwlklem2.f ⊢ F = x ∈ 0 ..^ P − 1 ⟼ if x < P − 2 E -1 ⁡ P ⁡ x P ⁡ x + 1 E -1 ⁡ P ⁡ x P ⁡ 0
Assertion clwlkclwwlklem2a2 ⊢ P ∈ Word V ∧ 2 ≤ P → F = P − 1

Proof

Step Hyp Ref Expression
1 clwlkclwwlklem2.f ⊢ F = x ∈ 0 ..^ P − 1 ⟼ if x < P − 2 E -1 ⁡ P ⁡ x P ⁡ x + 1 E -1 ⁡ P ⁡ x P ⁡ 0
2 lencl ⊢ P ∈ Word V → P ∈ ℕ 0
3 nn0z ⊢ P ∈ ℕ 0 → P ∈ ℤ
4 3 adantr ⊢ P ∈ ℕ 0 ∧ 2 ≤ P → P ∈ ℤ
5 0red ⊢ P ∈ ℕ 0 ∧ 2 ≤ P → 0 ∈ ℝ
6 2re ⊢ 2 ∈ ℝ
7 6 a1i ⊢ P ∈ ℕ 0 ∧ 2 ≤ P → 2 ∈ ℝ
8 nn0re ⊢ P ∈ ℕ 0 → P ∈ ℝ
9 8 adantr ⊢ P ∈ ℕ 0 ∧ 2 ≤ P → P ∈ ℝ
10 2pos ⊢ 0 < 2
11 10 a1i ⊢ P ∈ ℕ 0 ∧ 2 ≤ P → 0 < 2
12 simpr ⊢ P ∈ ℕ 0 ∧ 2 ≤ P → 2 ≤ P
13 5 7 9 11 12 ltletrd ⊢ P ∈ ℕ 0 ∧ 2 ≤ P → 0 < P
14 elnnz ⊢ P ∈ ℕ ↔ P ∈ ℤ ∧ 0 < P
15 4 13 14 sylanbrc ⊢ P ∈ ℕ 0 ∧ 2 ≤ P → P ∈ ℕ
16 2 15 sylan ⊢ P ∈ Word V ∧ 2 ≤ P → P ∈ ℕ
17 nnm1nn0 ⊢ P ∈ ℕ → P − 1 ∈ ℕ 0
18 16 17 syl ⊢ P ∈ Word V ∧ 2 ≤ P → P − 1 ∈ ℕ 0
19 fvex ⊢ E -1 ⁡ P ⁡ x P ⁡ x + 1 ∈ V
20 fvex ⊢ E -1 ⁡ P ⁡ x P ⁡ 0 ∈ V
21 19 20 ifex ⊢ if x < P − 2 E -1 ⁡ P ⁡ x P ⁡ x + 1 E -1 ⁡ P ⁡ x P ⁡ 0 ∈ V
22 21 1 fnmpti ⊢ F Fn 0 ..^ P − 1
23 ffzo0hash ⊢ P − 1 ∈ ℕ 0 ∧ F Fn 0 ..^ P − 1 → F = P − 1
24 18 22 23 sylancl ⊢ P ∈ Word V ∧ 2 ≤ P → F = P − 1