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 ⟼ if x < P − 2 E -1 ⁡ P ⁡ x P ⁡ x + 1 E -1 ⁡ P ⁡ x P ⁡ 0
Assertion clwlkclwwlklem2fv2 ⊢ P ∈ ℕ 0 ∧ 2 ≤ P → F ⁡ P − 2 = E -1 ⁡ P ⁡ P − 2 P ⁡ 0

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 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 → if x < P − 2 E -1 ⁡ P ⁡ x P ⁡ x + 1 E -1 ⁡ P ⁡ x P ⁡ 0 = E -1 ⁡ P ⁡ x P ⁡ 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 ⁡ x P ⁡ 0 = P ⁡ P − 2 P ⁡ 0
31 30 fveq2d ⊢ P ∈ ℕ 0 ∧ 2 ≤ P ∧ x = P − 2 → E -1 ⁡ P ⁡ x P ⁡ 0 = E -1 ⁡ P ⁡ P − 2 P ⁡ 0
32 27 31 eqtrd ⊢ P ∈ ℕ 0 ∧ 2 ≤ P ∧ x = P − 2 → if x < P − 2 E -1 ⁡ P ⁡ x P ⁡ x + 1 E -1 ⁡ P ⁡ x P ⁡ 0 = E -1 ⁡ P ⁡ P − 2 P ⁡ 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 − 2 P ⁡ 0 ∈ V
49 1 32 47 48 fvmptd2 ⊢ P ∈ ℕ 0 ∧ 2 ≤ P → F ⁡ P − 2 = E -1 ⁡ P ⁡ P − 2 P ⁡ 0