Metamath Proof Explorer

Theorem clwlkclwwlklem2fv2

Description: Lemma 4b 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 clwlkclwwlklem2fv2 ⊢P∈ℕ0∧2≤P→F⁡P−2=E-1⁡P⁡P−2P⁡0

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 simpr ⊢P∈ℕ0∧2≤P∧x=P−2→x=P−2
3 nn0z ⊢P∈ℕ0→P∈ℤ
4 2z ⊢2∈ℤ
5 3 4 jctir ⊢P∈ℕ0→P∈ℤ∧2∈ℤ
6 zsubcl ⊢P∈ℤ∧2∈ℤ→P−2∈ℤ
7 5 6 syl ⊢P∈ℕ0→P−2∈ℤ
8 7 adantr ⊢P∈ℕ0∧2≤P→P−2∈ℤ
9 8 adantr ⊢P∈ℕ0∧2≤P∧x=P−2→P−2∈ℤ
10 2 9 eqeltrd ⊢P∈ℕ0∧2≤P∧x=P−2→x∈ℤ
11 10 ex ⊢P∈ℕ0∧2≤P→x=P−2→x∈ℤ
12 zre ⊢x∈ℤ→x∈ℝ
13 nn0re ⊢P∈ℕ0→P∈ℝ
14 2re ⊢2∈ℝ
15 14 a1i ⊢P∈ℕ0→2∈ℝ
16 13 15 resubcld ⊢P∈ℕ0→P−2∈ℝ
17 16 adantr ⊢P∈ℕ0∧2≤P→P−2∈ℝ
18 lttri3 ⊢x∈ℝ∧P−2∈ℝ→x=P−2↔¬x<P−2∧¬P−2<x
19 12 17 18 syl2anr ⊢P∈ℕ0∧2≤P∧x∈ℤ→x=P−2↔¬x<P−2∧¬P−2<x
20 simpl ⊢¬x<P−2∧¬P−2<x→¬x<P−2
21 19 20 syl6bi ⊢P∈ℕ0∧2≤P∧x∈ℤ→x=P−2→¬x<P−2
22 21 ex ⊢P∈ℕ0∧2≤P→x∈ℤ→x=P−2→¬x<P−2
23 11 22 syld ⊢P∈ℕ0∧2≤P→x=P−2→x=P−2→¬x<P−2
24 23 com13 ⊢x=P−2→x=P−2→P∈ℕ0∧2≤P→¬x<P−2
25 24 pm2.43i ⊢x=P−2→P∈ℕ0∧2≤P→¬x<P−2
26 25 impcom ⊢P∈ℕ0∧2≤P∧x=P−2→¬x<P−2
27 26 iffalsed ⊢P∈ℕ0∧2≤P∧x=P−2→ifx<P−2E-1⁡P⁡xP⁡x+1E-1⁡P⁡xP⁡0=E-1⁡P⁡xP⁡0
28 fveq2 ⊢x=P−2→P⁡x=P⁡P−2
29 28 adantl ⊢P∈ℕ0∧2≤P∧x=P−2→P⁡x=P⁡P−2
30 29 preq1d ⊢P∈ℕ0∧2≤P∧x=P−2→P⁡xP⁡0=P⁡P−2P⁡0
31 30 fveq2d ⊢P∈ℕ0∧2≤P∧x=P−2→E-1⁡P⁡xP⁡0=E-1⁡P⁡P−2P⁡0
32 27 31 eqtrd ⊢P∈ℕ0∧2≤P∧x=P−2→ifx<P−2E-1⁡P⁡xP⁡x+1E-1⁡P⁡xP⁡0=E-1⁡P⁡P−2P⁡0
33 5 adantr ⊢P∈ℕ0∧2≤P→P∈ℤ∧2∈ℤ
34 33 6 syl ⊢P∈ℕ0∧2≤P→P−2∈ℤ
35 13 15 subge0d ⊢P∈ℕ0→0≤P−2↔2≤P
36 35 biimpar ⊢P∈ℕ0∧2≤P→0≤P−2
37 elnn0z ⊢P−2∈ℕ0↔P−2∈ℤ∧0≤P−2
38 34 36 37 sylanbrc ⊢P∈ℕ0∧2≤P→P−2∈ℕ0
39 nn0ge2m1nn ⊢P∈ℕ0∧2≤P→P−1∈ℕ
40 1red ⊢P∈ℕ0∧2≤P→1∈ℝ
41 14 a1i ⊢P∈ℕ0∧2≤P→2∈ℝ
42 13 adantr ⊢P∈ℕ0∧2≤P→P∈ℝ
43 1lt2 ⊢1<2
44 43 a1i ⊢P∈ℕ0∧2≤P→1<2
45 40 41 42 44 ltsub2dd ⊢P∈ℕ0∧2≤P→P−2<P−1
46 elfzo0 ⊢P−2∈0..^P−1↔P−2∈ℕ0∧P−1∈ℕ∧P−2<P−1
47 38 39 45 46 syl3anbrc ⊢P∈ℕ0∧2≤P→P−2∈0..^P−1
48 fvexd ⊢P∈ℕ0∧2≤P→E-1⁡P⁡P−2P⁡0∈V
49 1 32 47 48 fvmptd2 ⊢P∈ℕ0∧2≤P→F⁡P−2=E-1⁡P⁡P−2P⁡0