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⟼ifx<P−2E-1⁡P⁡xP⁡x+1E-1⁡P⁡xP⁡0
Assertion clwlkclwwlklem2fv1 ⊢P∈ℕ0∧I∈0..^P−2→F⁡I=E-1⁡P⁡IP⁡I+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 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⁡xP⁡x+1=P⁡IP⁡I+1
6 5 fveq2d ⊢x=I→E-1⁡P⁡xP⁡x+1=E-1⁡P⁡IP⁡I+1
7 3 preq1d ⊢x=I→P⁡xP⁡0=P⁡IP⁡0
8 7 fveq2d ⊢x=I→E-1⁡P⁡xP⁡0=E-1⁡P⁡IP⁡0
9 2 6 8 ifbieq12d ⊢x=I→ifx<P−2E-1⁡P⁡xP⁡x+1E-1⁡P⁡xP⁡0=ifI<P−2E-1⁡P⁡IP⁡I+1E-1⁡P⁡IP⁡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→ifI<P−2E-1⁡P⁡IP⁡I+1E-1⁡P⁡IP⁡0=E-1⁡P⁡IP⁡I+1
13 9 12 sylan9eqr ⊢P∈ℕ0∧I∈0..^P−2∧x=I→ifx<P−2E-1⁡P⁡xP⁡x+1E-1⁡P⁡xP⁡0=E-1⁡P⁡IP⁡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⁡IP⁡I+1∈V
33 1 13 31 32 fvmptd2 ⊢P∈ℕ0∧I∈0..^P−2→F⁡I=E-1⁡P⁡IP⁡I+1