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⟼ifx<P−2E-1⁡P⁡xP⁡x+1E-1⁡P⁡xP⁡0
Assertion clwlkclwwlklem2a2 ⊢P∈WordV∧2≤P→F=P−1

Proof

Step Hyp Ref Expression
1 clwlkclwwlklem2.f ⊢F=x∈0..^P−1⟼ifx<P−2E-1⁡P⁡xP⁡x+1E-1⁡P⁡xP⁡0
2 lencl ⊢P∈WordV→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∈WordV∧2≤P→P∈ℕ
17 nnm1nn0 ⊢P∈ℕ→P−1∈ℕ0
18 16 17 syl ⊢P∈WordV∧2≤P→P−1∈ℕ0
19 fvex ⊢E-1⁡P⁡xP⁡x+1∈V
20 fvex ⊢E-1⁡P⁡xP⁡0∈V
21 19 20 ifex ⊢ifx<P−2E-1⁡P⁡xP⁡x+1E-1⁡P⁡xP⁡0∈V
22 21 1 fnmpti ⊢FFn0..^P−1
23 ffzo0hash ⊢P−1∈ℕ0∧FFn0..^P−1→F=P−1
24 18 22 23 sylancl ⊢P∈WordV∧2≤P→F=P−1