Metamath Proof Explorer

Theorem clwlkclwwlklem2a1

Description: Lemma 1 for clwlkclwwlklem2a . (Contributed by Alexander van der Vekens, 21-Jun-2018) (Revised by AV, 11-Apr-2021)

Ref Expression
Assertion clwlkclwwlklem2a1 ⊢ P ∈ Word V ∧ 2 ≤ P → lastS ⁡ P = P ⁡ 0 ∧ ∀ i ∈ 0 ..^ P − 1 - 0 - 1 P ⁡ i P ⁡ i + 1 ∈ ran ⁡ E ∧ P ⁡ P − 2 P ⁡ 0 ∈ ran ⁡ E → ∀ i ∈ 0 ..^ P − 1 P ⁡ i P ⁡ i + 1 ∈ ran ⁡ E

Proof

Step Hyp Ref Expression
1 lencl ⊢ P ∈ Word V → P ∈ ℕ 0
2 nn0cn ⊢ P ∈ ℕ 0 → P ∈ ℂ
3 peano2cnm ⊢ P ∈ ℂ → P − 1 ∈ ℂ
4 3 subid1d ⊢ P ∈ ℂ → P - 1 - 0 = P − 1
5 4 oveq1d ⊢ P ∈ ℂ → P − 1 - 0 - 1 = P - 1 - 1
6 sub1m1 ⊢ P ∈ ℂ → P - 1 - 1 = P − 2
7 5 6 eqtrd ⊢ P ∈ ℂ → P − 1 - 0 - 1 = P − 2
8 1 2 7 3syl ⊢ P ∈ Word V → P − 1 - 0 - 1 = P − 2
9 8 adantr ⊢ P ∈ Word V ∧ 2 ≤ P → P − 1 - 0 - 1 = P − 2
10 9 oveq2d ⊢ P ∈ Word V ∧ 2 ≤ P → 0 ..^ P − 1 - 0 - 1 = 0 ..^ P − 2
11 10 raleqdv ⊢ P ∈ Word V ∧ 2 ≤ P → ∀ i ∈ 0 ..^ P − 1 - 0 - 1 P ⁡ i P ⁡ i + 1 ∈ ran ⁡ E ↔ ∀ i ∈ 0 ..^ P − 2 P ⁡ i P ⁡ i + 1 ∈ ran ⁡ E
12 11 biimpcd ⊢ ∀ i ∈ 0 ..^ P − 1 - 0 - 1 P ⁡ i P ⁡ i + 1 ∈ ran ⁡ E → P ∈ Word V ∧ 2 ≤ P → ∀ i ∈ 0 ..^ P − 2 P ⁡ i P ⁡ i + 1 ∈ ran ⁡ E
13 12 adantr ⊢ ∀ i ∈ 0 ..^ P − 1 - 0 - 1 P ⁡ i P ⁡ i + 1 ∈ ran ⁡ E ∧ P ⁡ P − 2 P ⁡ 0 ∈ ran ⁡ E → P ∈ Word V ∧ 2 ≤ P → ∀ i ∈ 0 ..^ P − 2 P ⁡ i P ⁡ i + 1 ∈ ran ⁡ E
14 13 adantl ⊢ lastS ⁡ P = P ⁡ 0 ∧ ∀ i ∈ 0 ..^ P − 1 - 0 - 1 P ⁡ i P ⁡ i + 1 ∈ ran ⁡ E ∧ P ⁡ P − 2 P ⁡ 0 ∈ ran ⁡ E → P ∈ Word V ∧ 2 ≤ P → ∀ i ∈ 0 ..^ P − 2 P ⁡ i P ⁡ i + 1 ∈ ran ⁡ E
15 14 impcom ⊢ P ∈ Word V ∧ 2 ≤ P ∧ lastS ⁡ P = P ⁡ 0 ∧ ∀ i ∈ 0 ..^ P − 1 - 0 - 1 P ⁡ i P ⁡ i + 1 ∈ ran ⁡ E ∧ P ⁡ P − 2 P ⁡ 0 ∈ ran ⁡ E → ∀ i ∈ 0 ..^ P − 2 P ⁡ i P ⁡ i + 1 ∈ ran ⁡ E
16 lsw ⊢ P ∈ Word V → lastS ⁡ P = P ⁡ P − 1
17 2m1e1 ⊢ 2 − 1 = 1
18 17 a1i ⊢ P ∈ Word V → 2 − 1 = 1
19 18 eqcomd ⊢ P ∈ Word V → 1 = 2 − 1
20 19 oveq2d ⊢ P ∈ Word V → P − 1 = P − 2 − 1
21 1 2 syl ⊢ P ∈ Word V → P ∈ ℂ
22 2cnd ⊢ P ∈ Word V → 2 ∈ ℂ
23 1cnd ⊢ P ∈ Word V → 1 ∈ ℂ
24 21 22 23 subsubd ⊢ P ∈ Word V → P − 2 − 1 = P - 2 + 1
25 20 24 eqtrd ⊢ P ∈ Word V → P − 1 = P - 2 + 1
26 25 fveq2d ⊢ P ∈ Word V → P ⁡ P − 1 = P ⁡ P - 2 + 1
27 16 26 eqtrd ⊢ P ∈ Word V → lastS ⁡ P = P ⁡ P - 2 + 1
28 27 adantr ⊢ P ∈ Word V ∧ 2 ≤ P → lastS ⁡ P = P ⁡ P - 2 + 1
29 28 adantr ⊢ P ∈ Word V ∧ 2 ≤ P ∧ lastS ⁡ P = P ⁡ 0 → lastS ⁡ P = P ⁡ P - 2 + 1
30 eqeq1 ⊢ lastS ⁡ P = P ⁡ 0 → lastS ⁡ P = P ⁡ P - 2 + 1 ↔ P ⁡ 0 = P ⁡ P - 2 + 1
31 30 adantl ⊢ P ∈ Word V ∧ 2 ≤ P ∧ lastS ⁡ P = P ⁡ 0 → lastS ⁡ P = P ⁡ P - 2 + 1 ↔ P ⁡ 0 = P ⁡ P - 2 + 1
32 29 31 mpbid ⊢ P ∈ Word V ∧ 2 ≤ P ∧ lastS ⁡ P = P ⁡ 0 → P ⁡ 0 = P ⁡ P - 2 + 1
33 32 preq2d ⊢ P ∈ Word V ∧ 2 ≤ P ∧ lastS ⁡ P = P ⁡ 0 → P ⁡ P − 2 P ⁡ 0 = P ⁡ P − 2 P ⁡ P - 2 + 1
34 33 eleq1d ⊢ P ∈ Word V ∧ 2 ≤ P ∧ lastS ⁡ P = P ⁡ 0 → P ⁡ P − 2 P ⁡ 0 ∈ ran ⁡ E ↔ P ⁡ P − 2 P ⁡ P - 2 + 1 ∈ ran ⁡ E
35 34 biimpd ⊢ P ∈ Word V ∧ 2 ≤ P ∧ lastS ⁡ P = P ⁡ 0 → P ⁡ P − 2 P ⁡ 0 ∈ ran ⁡ E → P ⁡ P − 2 P ⁡ P - 2 + 1 ∈ ran ⁡ E
36 35 ex ⊢ P ∈ Word V ∧ 2 ≤ P → lastS ⁡ P = P ⁡ 0 → P ⁡ P − 2 P ⁡ 0 ∈ ran ⁡ E → P ⁡ P − 2 P ⁡ P - 2 + 1 ∈ ran ⁡ E
37 36 com13 ⊢ P ⁡ P − 2 P ⁡ 0 ∈ ran ⁡ E → lastS ⁡ P = P ⁡ 0 → P ∈ Word V ∧ 2 ≤ P → P ⁡ P − 2 P ⁡ P - 2 + 1 ∈ ran ⁡ E
38 37 adantl ⊢ ∀ i ∈ 0 ..^ P − 1 - 0 - 1 P ⁡ i P ⁡ i + 1 ∈ ran ⁡ E ∧ P ⁡ P − 2 P ⁡ 0 ∈ ran ⁡ E → lastS ⁡ P = P ⁡ 0 → P ∈ Word V ∧ 2 ≤ P → P ⁡ P − 2 P ⁡ P - 2 + 1 ∈ ran ⁡ E
39 38 impcom ⊢ lastS ⁡ P = P ⁡ 0 ∧ ∀ i ∈ 0 ..^ P − 1 - 0 - 1 P ⁡ i P ⁡ i + 1 ∈ ran ⁡ E ∧ P ⁡ P − 2 P ⁡ 0 ∈ ran ⁡ E → P ∈ Word V ∧ 2 ≤ P → P ⁡ P − 2 P ⁡ P - 2 + 1 ∈ ran ⁡ E
40 39 impcom ⊢ P ∈ Word V ∧ 2 ≤ P ∧ lastS ⁡ P = P ⁡ 0 ∧ ∀ i ∈ 0 ..^ P − 1 - 0 - 1 P ⁡ i P ⁡ i + 1 ∈ ran ⁡ E ∧ P ⁡ P − 2 P ⁡ 0 ∈ ran ⁡ E → P ⁡ P − 2 P ⁡ P - 2 + 1 ∈ ran ⁡ E
41 ovexd ⊢ P ∈ Word V ∧ 2 ≤ P ∧ lastS ⁡ P = P ⁡ 0 ∧ ∀ i ∈ 0 ..^ P − 1 - 0 - 1 P ⁡ i P ⁡ i + 1 ∈ ran ⁡ E ∧ P ⁡ P − 2 P ⁡ 0 ∈ ran ⁡ E → P − 2 ∈ V
42 fveq2 ⊢ i = P − 2 → P ⁡ i = P ⁡ P − 2
43 fvoveq1 ⊢ i = P − 2 → P ⁡ i + 1 = P ⁡ P - 2 + 1
44 42 43 preq12d ⊢ i = P − 2 → P ⁡ i P ⁡ i + 1 = P ⁡ P − 2 P ⁡ P - 2 + 1
45 44 eleq1d ⊢ i = P − 2 → P ⁡ i P ⁡ i + 1 ∈ ran ⁡ E ↔ P ⁡ P − 2 P ⁡ P - 2 + 1 ∈ ran ⁡ E
46 45 ralunsn ⊢ P − 2 ∈ V → ∀ i ∈ 0 ..^ P − 2 ∪ P − 2 P ⁡ i P ⁡ i + 1 ∈ ran ⁡ E ↔ ∀ i ∈ 0 ..^ P − 2 P ⁡ i P ⁡ i + 1 ∈ ran ⁡ E ∧ P ⁡ P − 2 P ⁡ P - 2 + 1 ∈ ran ⁡ E
47 41 46 syl ⊢ P ∈ Word V ∧ 2 ≤ P ∧ lastS ⁡ P = P ⁡ 0 ∧ ∀ i ∈ 0 ..^ P − 1 - 0 - 1 P ⁡ i P ⁡ i + 1 ∈ ran ⁡ E ∧ P ⁡ P − 2 P ⁡ 0 ∈ ran ⁡ E → ∀ i ∈ 0 ..^ P − 2 ∪ P − 2 P ⁡ i P ⁡ i + 1 ∈ ran ⁡ E ↔ ∀ i ∈ 0 ..^ P − 2 P ⁡ i P ⁡ i + 1 ∈ ran ⁡ E ∧ P ⁡ P − 2 P ⁡ P - 2 + 1 ∈ ran ⁡ E
48 15 40 47 mpbir2and ⊢ P ∈ Word V ∧ 2 ≤ P ∧ lastS ⁡ P = P ⁡ 0 ∧ ∀ i ∈ 0 ..^ P − 1 - 0 - 1 P ⁡ i P ⁡ i + 1 ∈ ran ⁡ E ∧ P ⁡ P − 2 P ⁡ 0 ∈ ran ⁡ E → ∀ i ∈ 0 ..^ P − 2 ∪ P − 2 P ⁡ i P ⁡ i + 1 ∈ ran ⁡ E
49 1e2m1 ⊢ 1 = 2 − 1
50 49 a1i ⊢ P ∈ Word V → 1 = 2 − 1
51 50 oveq2d ⊢ P ∈ Word V → P − 1 = P − 2 − 1
52 51 24 eqtrd ⊢ P ∈ Word V → P − 1 = P - 2 + 1
53 52 oveq2d ⊢ P ∈ Word V → 0 ..^ P − 1 = 0 ..^ P - 2 + 1
54 53 adantr ⊢ P ∈ Word V ∧ 2 ≤ P → 0 ..^ P − 1 = 0 ..^ P - 2 + 1
55 nn0re ⊢ P ∈ ℕ 0 → P ∈ ℝ
56 2re ⊢ 2 ∈ ℝ
57 56 a1i ⊢ P ∈ ℕ 0 → 2 ∈ ℝ
58 55 57 subge0d ⊢ P ∈ ℕ 0 → 0 ≤ P − 2 ↔ 2 ≤ P
59 58 biimprd ⊢ P ∈ ℕ 0 → 2 ≤ P → 0 ≤ P − 2
60 nn0z ⊢ P ∈ ℕ 0 → P ∈ ℤ
61 2z ⊢ 2 ∈ ℤ
62 61 a1i ⊢ P ∈ ℕ 0 → 2 ∈ ℤ
63 60 62 zsubcld ⊢ P ∈ ℕ 0 → P − 2 ∈ ℤ
64 59 63 jctild ⊢ P ∈ ℕ 0 → 2 ≤ P → P − 2 ∈ ℤ ∧ 0 ≤ P − 2
65 1 64 syl ⊢ P ∈ Word V → 2 ≤ P → P − 2 ∈ ℤ ∧ 0 ≤ P − 2
66 65 imp ⊢ P ∈ Word V ∧ 2 ≤ P → P − 2 ∈ ℤ ∧ 0 ≤ P − 2
67 elnn0z ⊢ P − 2 ∈ ℕ 0 ↔ P − 2 ∈ ℤ ∧ 0 ≤ P − 2
68 66 67 sylibr ⊢ P ∈ Word V ∧ 2 ≤ P → P − 2 ∈ ℕ 0
69 elnn0uz ⊢ P − 2 ∈ ℕ 0 ↔ P − 2 ∈ ℤ ≥ 0
70 68 69 sylib ⊢ P ∈ Word V ∧ 2 ≤ P → P − 2 ∈ ℤ ≥ 0
71 fzosplitsn ⊢ P − 2 ∈ ℤ ≥ 0 → 0 ..^ P - 2 + 1 = 0 ..^ P − 2 ∪ P − 2
72 70 71 syl ⊢ P ∈ Word V ∧ 2 ≤ P → 0 ..^ P - 2 + 1 = 0 ..^ P − 2 ∪ P − 2
73 54 72 eqtrd ⊢ P ∈ Word V ∧ 2 ≤ P → 0 ..^ P − 1 = 0 ..^ P − 2 ∪ P − 2
74 73 adantr ⊢ P ∈ Word V ∧ 2 ≤ P ∧ lastS ⁡ P = P ⁡ 0 ∧ ∀ i ∈ 0 ..^ P − 1 - 0 - 1 P ⁡ i P ⁡ i + 1 ∈ ran ⁡ E ∧ P ⁡ P − 2 P ⁡ 0 ∈ ran ⁡ E → 0 ..^ P − 1 = 0 ..^ P − 2 ∪ P − 2
75 74 raleqdv ⊢ P ∈ Word V ∧ 2 ≤ P ∧ lastS ⁡ P = P ⁡ 0 ∧ ∀ i ∈ 0 ..^ P − 1 - 0 - 1 P ⁡ i P ⁡ i + 1 ∈ ran ⁡ E ∧ P ⁡ P − 2 P ⁡ 0 ∈ ran ⁡ E → ∀ i ∈ 0 ..^ P − 1 P ⁡ i P ⁡ i + 1 ∈ ran ⁡ E ↔ ∀ i ∈ 0 ..^ P − 2 ∪ P − 2 P ⁡ i P ⁡ i + 1 ∈ ran ⁡ E
76 48 75 mpbird ⊢ P ∈ Word V ∧ 2 ≤ P ∧ lastS ⁡ P = P ⁡ 0 ∧ ∀ i ∈ 0 ..^ P − 1 - 0 - 1 P ⁡ i P ⁡ i + 1 ∈ ran ⁡ E ∧ P ⁡ P − 2 P ⁡ 0 ∈ ran ⁡ E → ∀ i ∈ 0 ..^ P − 1 P ⁡ i P ⁡ i + 1 ∈ ran ⁡ E
77 76 ex ⊢ P ∈ Word V ∧ 2 ≤ P → lastS ⁡ P = P ⁡ 0 ∧ ∀ i ∈ 0 ..^ P − 1 - 0 - 1 P ⁡ i P ⁡ i + 1 ∈ ran ⁡ E ∧ P ⁡ P − 2 P ⁡ 0 ∈ ran ⁡ E → ∀ i ∈ 0 ..^ P − 1 P ⁡ i P ⁡ i + 1 ∈ ran ⁡ E