Metamath Proof Explorer

Theorem clwlkclwwlklem2fv1

Description: Lemma 4a for clwlkclwwlklem2a . (Contributed by Alexander van der Vekens, 22-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 clwlkclwwlklem2fv1 ⊢ P ∈ ℕ 0 ∧ I ∈ 0 ..^ P − 2 → F ⁡ I = E -1 ⁡ P ⁡ I P ⁡ I + 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 breq1 ⊢ x = I → x < P − 2 ↔ I < P − 2
3 fveq2 ⊢ x = I → P ⁡ x = P ⁡ I
4 fvoveq1 ⊢ x = I → P ⁡ x + 1 = P ⁡ I + 1
5 3 4 preq12d ⊢ x = I → P ⁡ x P ⁡ x + 1 = P ⁡ I P ⁡ I + 1
6 5 fveq2d ⊢ x = I → E -1 ⁡ P ⁡ x P ⁡ x + 1 = E -1 ⁡ P ⁡ I P ⁡ I + 1
7 3 preq1d ⊢ x = I → P ⁡ x P ⁡ 0 = P ⁡ I P ⁡ 0
8 7 fveq2d ⊢ x = I → E -1 ⁡ P ⁡ x P ⁡ 0 = E -1 ⁡ P ⁡ I P ⁡ 0
9 2 6 8 ifbieq12d ⊢ x = I → if x < P − 2 E -1 ⁡ P ⁡ x P ⁡ x + 1 E -1 ⁡ P ⁡ x P ⁡ 0 = if I < P − 2 E -1 ⁡ P ⁡ I P ⁡ I + 1 E -1 ⁡ P ⁡ I P ⁡ 0
10 elfzolt2 ⊢ I ∈ 0 ..^ P − 2 → I < P − 2
11 10 adantl ⊢ P ∈ ℕ 0 ∧ I ∈ 0 ..^ P − 2 → I < P − 2
12 11 iftrued ⊢ P ∈ ℕ 0 ∧ I ∈ 0 ..^ P − 2 → if I < P − 2 E -1 ⁡ P ⁡ I P ⁡ I + 1 E -1 ⁡ P ⁡ I P ⁡ 0 = E -1 ⁡ P ⁡ I P ⁡ I + 1
13 9 12 sylan9eqr ⊢ P ∈ ℕ 0 ∧ I ∈ 0 ..^ P − 2 ∧ x = I → if x < P − 2 E -1 ⁡ P ⁡ x P ⁡ x + 1 E -1 ⁡ P ⁡ x P ⁡ 0 = E -1 ⁡ P ⁡ I P ⁡ I + 1
14 nn0z ⊢ P ∈ ℕ 0 → P ∈ ℤ
15 2z ⊢ 2 ∈ ℤ
16 15 a1i ⊢ P ∈ ℕ 0 → 2 ∈ ℤ
17 14 16 zsubcld ⊢ P ∈ ℕ 0 → P − 2 ∈ ℤ
18 peano2zm ⊢ P ∈ ℤ → P − 1 ∈ ℤ
19 14 18 syl ⊢ P ∈ ℕ 0 → P − 1 ∈ ℤ
20 1red ⊢ P ∈ ℕ 0 → 1 ∈ ℝ
21 2re ⊢ 2 ∈ ℝ
22 21 a1i ⊢ P ∈ ℕ 0 → 2 ∈ ℝ
23 nn0re ⊢ P ∈ ℕ 0 → P ∈ ℝ
24 1le2 ⊢ 1 ≤ 2
25 24 a1i ⊢ P ∈ ℕ 0 → 1 ≤ 2
26 20 22 23 25 lesub2dd ⊢ P ∈ ℕ 0 → P − 2 ≤ P − 1
27 eluz2 ⊢ P − 1 ∈ ℤ ≥ P − 2 ↔ P − 2 ∈ ℤ ∧ P − 1 ∈ ℤ ∧ P − 2 ≤ P − 1
28 17 19 26 27 syl3anbrc ⊢ P ∈ ℕ 0 → P − 1 ∈ ℤ ≥ P − 2
29 fzoss2 ⊢ P − 1 ∈ ℤ ≥ P − 2 → 0 ..^ P − 2 ⊆ 0 ..^ P − 1
30 28 29 syl ⊢ P ∈ ℕ 0 → 0 ..^ P − 2 ⊆ 0 ..^ P − 1
31 30 sselda ⊢ P ∈ ℕ 0 ∧ I ∈ 0 ..^ P − 2 → I ∈ 0 ..^ P − 1
32 fvexd ⊢ P ∈ ℕ 0 ∧ I ∈ 0 ..^ P − 2 → E -1 ⁡ P ⁡ I P ⁡ I + 1 ∈ V
33 1 13 31 32 fvmptd2 ⊢ P ∈ ℕ 0 ∧ I ∈ 0 ..^ P − 2 → F ⁡ I = E -1 ⁡ P ⁡ I P ⁡ I + 1