Metamath Proof Explorer

Theorem clwlkclwwlklem2a

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

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 clwlkclwwlklem2a ⊢ E : dom ⁡ E ⟶ 1-1 R ∧ 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 → F ∈ Word dom ⁡ E ∧ P : 0 … F ⟶ V ∧ ∀ i ∈ 0 ..^ F E ⁡ F ⁡ i = P ⁡ i P ⁡ i + 1 ∧ P ⁡ 0 = P ⁡ F

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 simpl ⊢ x < P − 2 ∧ E : dom ⁡ E ⟶ 1-1 R ∧ 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 ∧ x ∈ 0 ..^ P − 1 → x < P − 2
3 f1f1orn ⊢ E : dom ⁡ E ⟶ 1-1 R → E : dom ⁡ E ⟶ 1-1 onto ran ⁡ E
4 3 3ad2ant1 ⊢ E : dom ⁡ E ⟶ 1-1 R ∧ P ∈ Word V ∧ 2 ≤ P → E : dom ⁡ E ⟶ 1-1 onto ran ⁡ E
5 4 adantr ⊢ E : dom ⁡ E ⟶ 1-1 R ∧ 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 → E : dom ⁡ E ⟶ 1-1 onto ran ⁡ E
6 5 ad2antrl ⊢ x < P − 2 ∧ E : dom ⁡ E ⟶ 1-1 R ∧ 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 ∧ x ∈ 0 ..^ P − 1 → E : dom ⁡ E ⟶ 1-1 onto ran ⁡ E
7 elfzo0 ⊢ x ∈ 0 ..^ P − 1 ↔ x ∈ ℕ 0 ∧ P − 1 ∈ ℕ ∧ x < P − 1
8 lencl ⊢ P ∈ Word V → P ∈ ℕ 0
9 simpl ⊢ x ∈ ℕ 0 ∧ P ∈ ℕ 0 → x ∈ ℕ 0
10 9 adantr ⊢ x ∈ ℕ 0 ∧ P ∈ ℕ 0 ∧ x < P − 2 ∧ 2 ≤ P → x ∈ ℕ 0
11 elnn0z ⊢ x ∈ ℕ 0 ↔ x ∈ ℤ ∧ 0 ≤ x
12 0red ⊢ x ∈ ℤ ∧ P ∈ ℕ 0 → 0 ∈ ℝ
13 zre ⊢ x ∈ ℤ → x ∈ ℝ
14 13 adantr ⊢ x ∈ ℤ ∧ P ∈ ℕ 0 → x ∈ ℝ
15 nn0re ⊢ P ∈ ℕ 0 → P ∈ ℝ
16 2re ⊢ 2 ∈ ℝ
17 16 a1i ⊢ P ∈ ℕ 0 → 2 ∈ ℝ
18 15 17 resubcld ⊢ P ∈ ℕ 0 → P − 2 ∈ ℝ
19 18 adantl ⊢ x ∈ ℤ ∧ P ∈ ℕ 0 → P − 2 ∈ ℝ
20 lelttr ⊢ 0 ∈ ℝ ∧ x ∈ ℝ ∧ P − 2 ∈ ℝ → 0 ≤ x ∧ x < P − 2 → 0 < P − 2
21 12 14 19 20 syl3anc ⊢ x ∈ ℤ ∧ P ∈ ℕ 0 → 0 ≤ x ∧ x < P − 2 → 0 < P − 2
22 nn0z ⊢ P ∈ ℕ 0 → P ∈ ℤ
23 2z ⊢ 2 ∈ ℤ
24 23 a1i ⊢ P ∈ ℕ 0 → 2 ∈ ℤ
25 22 24 zsubcld ⊢ P ∈ ℕ 0 → P − 2 ∈ ℤ
26 25 anim1i ⊢ P ∈ ℕ 0 ∧ 0 < P − 2 → P − 2 ∈ ℤ ∧ 0 < P − 2
27 elnnz ⊢ P − 2 ∈ ℕ ↔ P − 2 ∈ ℤ ∧ 0 < P − 2
28 26 27 sylibr ⊢ P ∈ ℕ 0 ∧ 0 < P − 2 → P − 2 ∈ ℕ
29 nn0cn ⊢ P ∈ ℕ 0 → P ∈ ℂ
30 peano2cnm ⊢ P ∈ ℂ → P − 1 ∈ ℂ
31 29 30 syl ⊢ P ∈ ℕ 0 → P − 1 ∈ ℂ
32 31 subid1d ⊢ P ∈ ℕ 0 → P - 1 - 0 = P − 1
33 32 oveq1d ⊢ P ∈ ℕ 0 → P − 1 - 0 - 1 = P - 1 - 1
34 1cnd ⊢ P ∈ ℕ 0 → 1 ∈ ℂ
35 29 34 34 subsub4d ⊢ P ∈ ℕ 0 → P - 1 - 1 = P − 1 + 1
36 1p1e2 ⊢ 1 + 1 = 2
37 36 a1i ⊢ P ∈ ℕ 0 → 1 + 1 = 2
38 37 oveq2d ⊢ P ∈ ℕ 0 → P − 1 + 1 = P − 2
39 35 38 eqtrd ⊢ P ∈ ℕ 0 → P - 1 - 1 = P − 2
40 33 39 eqtrd ⊢ P ∈ ℕ 0 → P − 1 - 0 - 1 = P − 2
41 40 eleq1d ⊢ P ∈ ℕ 0 → P − 1 - 0 - 1 ∈ ℕ ↔ P − 2 ∈ ℕ
42 41 adantr ⊢ P ∈ ℕ 0 ∧ 0 < P − 2 → P − 1 - 0 - 1 ∈ ℕ ↔ P − 2 ∈ ℕ
43 28 42 mpbird ⊢ P ∈ ℕ 0 ∧ 0 < P − 2 → P − 1 - 0 - 1 ∈ ℕ
44 43 ex ⊢ P ∈ ℕ 0 → 0 < P − 2 → P − 1 - 0 - 1 ∈ ℕ
45 44 adantl ⊢ x ∈ ℤ ∧ P ∈ ℕ 0 → 0 < P − 2 → P − 1 - 0 - 1 ∈ ℕ
46 21 45 syld ⊢ x ∈ ℤ ∧ P ∈ ℕ 0 → 0 ≤ x ∧ x < P − 2 → P − 1 - 0 - 1 ∈ ℕ
47 46 exp4b ⊢ x ∈ ℤ → P ∈ ℕ 0 → 0 ≤ x → x < P − 2 → P − 1 - 0 - 1 ∈ ℕ
48 47 com23 ⊢ x ∈ ℤ → 0 ≤ x → P ∈ ℕ 0 → x < P − 2 → P − 1 - 0 - 1 ∈ ℕ
49 48 imp ⊢ x ∈ ℤ ∧ 0 ≤ x → P ∈ ℕ 0 → x < P − 2 → P − 1 - 0 - 1 ∈ ℕ
50 11 49 sylbi ⊢ x ∈ ℕ 0 → P ∈ ℕ 0 → x < P − 2 → P − 1 - 0 - 1 ∈ ℕ
51 50 imp ⊢ x ∈ ℕ 0 ∧ P ∈ ℕ 0 → x < P − 2 → P − 1 - 0 - 1 ∈ ℕ
52 51 com12 ⊢ x < P − 2 → x ∈ ℕ 0 ∧ P ∈ ℕ 0 → P − 1 - 0 - 1 ∈ ℕ
53 52 adantr ⊢ x < P − 2 ∧ 2 ≤ P → x ∈ ℕ 0 ∧ P ∈ ℕ 0 → P − 1 - 0 - 1 ∈ ℕ
54 53 impcom ⊢ x ∈ ℕ 0 ∧ P ∈ ℕ 0 ∧ x < P − 2 ∧ 2 ≤ P → P − 1 - 0 - 1 ∈ ℕ
55 df-2 ⊢ 2 = 1 + 1
56 55 a1i ⊢ P ∈ ℕ 0 → 2 = 1 + 1
57 56 oveq2d ⊢ P ∈ ℕ 0 → P − 2 = P − 1 + 1
58 32 eqcomd ⊢ P ∈ ℕ 0 → P − 1 = P - 1 - 0
59 58 oveq1d ⊢ P ∈ ℕ 0 → P - 1 - 1 = P − 1 - 0 - 1
60 57 35 59 3eqtr2d ⊢ P ∈ ℕ 0 → P − 2 = P − 1 - 0 - 1
61 60 adantl ⊢ x ∈ ℕ 0 ∧ P ∈ ℕ 0 → P − 2 = P − 1 - 0 - 1
62 61 breq2d ⊢ x ∈ ℕ 0 ∧ P ∈ ℕ 0 → x < P − 2 ↔ x < P − 1 - 0 - 1
63 62 biimpcd ⊢ x < P − 2 → x ∈ ℕ 0 ∧ P ∈ ℕ 0 → x < P − 1 - 0 - 1
64 63 adantr ⊢ x < P − 2 ∧ 2 ≤ P → x ∈ ℕ 0 ∧ P ∈ ℕ 0 → x < P − 1 - 0 - 1
65 64 impcom ⊢ x ∈ ℕ 0 ∧ P ∈ ℕ 0 ∧ x < P − 2 ∧ 2 ≤ P → x < P − 1 - 0 - 1
66 elfzo0 ⊢ x ∈ 0 ..^ P − 1 - 0 - 1 ↔ x ∈ ℕ 0 ∧ P − 1 - 0 - 1 ∈ ℕ ∧ x < P − 1 - 0 - 1
67 10 54 65 66 syl3anbrc ⊢ x ∈ ℕ 0 ∧ P ∈ ℕ 0 ∧ x < P − 2 ∧ 2 ≤ P → x ∈ 0 ..^ P − 1 - 0 - 1
68 67 exp32 ⊢ x ∈ ℕ 0 ∧ P ∈ ℕ 0 → x < P − 2 → 2 ≤ P → x ∈ 0 ..^ P − 1 - 0 - 1
69 68 a1d ⊢ x ∈ ℕ 0 ∧ P ∈ ℕ 0 → x < P − 1 → x < P − 2 → 2 ≤ P → x ∈ 0 ..^ P − 1 - 0 - 1
70 69 com24 ⊢ x ∈ ℕ 0 ∧ P ∈ ℕ 0 → 2 ≤ P → x < P − 2 → x < P − 1 → x ∈ 0 ..^ P − 1 - 0 - 1
71 70 ex ⊢ x ∈ ℕ 0 → P ∈ ℕ 0 → 2 ≤ P → x < P − 2 → x < P − 1 → x ∈ 0 ..^ P − 1 - 0 - 1
72 71 com25 ⊢ x ∈ ℕ 0 → x < P − 1 → 2 ≤ P → x < P − 2 → P ∈ ℕ 0 → x ∈ 0 ..^ P − 1 - 0 - 1
73 72 imp ⊢ x ∈ ℕ 0 ∧ x < P − 1 → 2 ≤ P → x < P − 2 → P ∈ ℕ 0 → x ∈ 0 ..^ P − 1 - 0 - 1
74 73 3adant2 ⊢ x ∈ ℕ 0 ∧ P − 1 ∈ ℕ ∧ x < P − 1 → 2 ≤ P → x < P − 2 → P ∈ ℕ 0 → x ∈ 0 ..^ P − 1 - 0 - 1
75 74 com14 ⊢ P ∈ ℕ 0 → 2 ≤ P → x < P − 2 → x ∈ ℕ 0 ∧ P − 1 ∈ ℕ ∧ x < P − 1 → x ∈ 0 ..^ P − 1 - 0 - 1
76 8 75 syl ⊢ P ∈ Word V → 2 ≤ P → x < P − 2 → x ∈ ℕ 0 ∧ P − 1 ∈ ℕ ∧ x < P − 1 → x ∈ 0 ..^ P − 1 - 0 - 1
77 76 imp ⊢ P ∈ Word V ∧ 2 ≤ P → x < P − 2 → x ∈ ℕ 0 ∧ P − 1 ∈ ℕ ∧ x < P − 1 → x ∈ 0 ..^ P − 1 - 0 - 1
78 77 3adant1 ⊢ E : dom ⁡ E ⟶ 1-1 R ∧ P ∈ Word V ∧ 2 ≤ P → x < P − 2 → x ∈ ℕ 0 ∧ P − 1 ∈ ℕ ∧ x < P − 1 → x ∈ 0 ..^ P − 1 - 0 - 1
79 7 78 syl7bi ⊢ E : dom ⁡ E ⟶ 1-1 R ∧ P ∈ Word V ∧ 2 ≤ P → x < P − 2 → x ∈ 0 ..^ P − 1 → x ∈ 0 ..^ P − 1 - 0 - 1
80 79 com13 ⊢ x ∈ 0 ..^ P − 1 → x < P − 2 → E : dom ⁡ E ⟶ 1-1 R ∧ P ∈ Word V ∧ 2 ≤ P → x ∈ 0 ..^ P − 1 - 0 - 1
81 80 imp31 ⊢ x ∈ 0 ..^ P − 1 ∧ x < P − 2 ∧ E : dom ⁡ E ⟶ 1-1 R ∧ P ∈ Word V ∧ 2 ≤ P → x ∈ 0 ..^ P − 1 - 0 - 1
82 fveq2 ⊢ i = x → P ⁡ i = P ⁡ x
83 fvoveq1 ⊢ i = x → P ⁡ i + 1 = P ⁡ x + 1
84 82 83 preq12d ⊢ i = x → P ⁡ i P ⁡ i + 1 = P ⁡ x P ⁡ x + 1
85 84 eleq1d ⊢ i = x → P ⁡ i P ⁡ i + 1 ∈ ran ⁡ E ↔ P ⁡ x P ⁡ x + 1 ∈ ran ⁡ E
86 85 adantl ⊢ x ∈ 0 ..^ P − 1 ∧ x < P − 2 ∧ E : dom ⁡ E ⟶ 1-1 R ∧ P ∈ Word V ∧ 2 ≤ P ∧ i = x → P ⁡ i P ⁡ i + 1 ∈ ran ⁡ E ↔ P ⁡ x P ⁡ x + 1 ∈ ran ⁡ E
87 81 86 rspcdv ⊢ x ∈ 0 ..^ P − 1 ∧ x < P − 2 ∧ E : dom ⁡ E ⟶ 1-1 R ∧ P ∈ Word V ∧ 2 ≤ P → ∀ i ∈ 0 ..^ P − 1 - 0 - 1 P ⁡ i P ⁡ i + 1 ∈ ran ⁡ E → P ⁡ x P ⁡ x + 1 ∈ ran ⁡ E
88 87 ex ⊢ x ∈ 0 ..^ P − 1 ∧ x < P − 2 → E : dom ⁡ E ⟶ 1-1 R ∧ P ∈ Word V ∧ 2 ≤ P → ∀ i ∈ 0 ..^ P − 1 - 0 - 1 P ⁡ i P ⁡ i + 1 ∈ ran ⁡ E → P ⁡ x P ⁡ x + 1 ∈ ran ⁡ E
89 88 com13 ⊢ ∀ i ∈ 0 ..^ P − 1 - 0 - 1 P ⁡ i P ⁡ i + 1 ∈ ran ⁡ E → E : dom ⁡ E ⟶ 1-1 R ∧ P ∈ Word V ∧ 2 ≤ P → x ∈ 0 ..^ P − 1 ∧ x < P − 2 → P ⁡ x P ⁡ x + 1 ∈ ran ⁡ E
90 89 ad2antrl ⊢ lastS ⁡ P = P ⁡ 0 ∧ ∀ i ∈ 0 ..^ P − 1 - 0 - 1 P ⁡ i P ⁡ i + 1 ∈ ran ⁡ E ∧ P ⁡ P − 2 P ⁡ 0 ∈ ran ⁡ E → E : dom ⁡ E ⟶ 1-1 R ∧ P ∈ Word V ∧ 2 ≤ P → x ∈ 0 ..^ P − 1 ∧ x < P − 2 → P ⁡ x P ⁡ x + 1 ∈ ran ⁡ E
91 90 impcom ⊢ E : dom ⁡ E ⟶ 1-1 R ∧ 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 → x ∈ 0 ..^ P − 1 ∧ x < P − 2 → P ⁡ x P ⁡ x + 1 ∈ ran ⁡ E
92 91 expdimp ⊢ E : dom ⁡ E ⟶ 1-1 R ∧ 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 ∧ x ∈ 0 ..^ P − 1 → x < P − 2 → P ⁡ x P ⁡ x + 1 ∈ ran ⁡ E
93 92 impcom ⊢ x < P − 2 ∧ E : dom ⁡ E ⟶ 1-1 R ∧ 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 ∧ x ∈ 0 ..^ P − 1 → P ⁡ x P ⁡ x + 1 ∈ ran ⁡ E
94 f1ocnvdm ⊢ E : dom ⁡ E ⟶ 1-1 onto ran ⁡ E ∧ P ⁡ x P ⁡ x + 1 ∈ ran ⁡ E → E -1 ⁡ P ⁡ x P ⁡ x + 1 ∈ dom ⁡ E
95 6 93 94 syl2anc ⊢ x < P − 2 ∧ E : dom ⁡ E ⟶ 1-1 R ∧ 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 ∧ x ∈ 0 ..^ P − 1 → E -1 ⁡ P ⁡ x P ⁡ x + 1 ∈ dom ⁡ E
96 2 95 jca ⊢ x < P − 2 ∧ E : dom ⁡ E ⟶ 1-1 R ∧ 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 ∧ x ∈ 0 ..^ P − 1 → x < P − 2 ∧ E -1 ⁡ P ⁡ x P ⁡ x + 1 ∈ dom ⁡ E
97 96 orcd ⊢ x < P − 2 ∧ E : dom ⁡ E ⟶ 1-1 R ∧ 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 ∧ x ∈ 0 ..^ P − 1 → x < P − 2 ∧ E -1 ⁡ P ⁡ x P ⁡ x + 1 ∈ dom ⁡ E ∨ ¬ x < P − 2 ∧ E -1 ⁡ P ⁡ x P ⁡ 0 ∈ dom ⁡ E
98 simpl ⊢ ¬ x < P − 2 ∧ E : dom ⁡ E ⟶ 1-1 R ∧ 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 ∧ x ∈ 0 ..^ P − 1 → ¬ x < P − 2
99 5 ad2antrl ⊢ ¬ x < P − 2 ∧ E : dom ⁡ E ⟶ 1-1 R ∧ 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 ∧ x ∈ 0 ..^ P − 1 → E : dom ⁡ E ⟶ 1-1 onto ran ⁡ E
100 nn0z ⊢ x ∈ ℕ 0 → x ∈ ℤ
101 peano2zm ⊢ P ∈ ℤ → P − 1 ∈ ℤ
102 22 101 syl ⊢ P ∈ ℕ 0 → P − 1 ∈ ℤ
103 100 102 anim12i ⊢ x ∈ ℕ 0 ∧ P ∈ ℕ 0 → x ∈ ℤ ∧ P − 1 ∈ ℤ
104 zltlem1 ⊢ x ∈ ℤ ∧ P − 1 ∈ ℤ → x < P − 1 ↔ x ≤ P - 1 - 1
105 103 104 syl ⊢ x ∈ ℕ 0 ∧ P ∈ ℕ 0 → x < P − 1 ↔ x ≤ P - 1 - 1
106 39 adantl ⊢ x ∈ ℕ 0 ∧ P ∈ ℕ 0 → P - 1 - 1 = P − 2
107 106 breq2d ⊢ x ∈ ℕ 0 ∧ P ∈ ℕ 0 → x ≤ P - 1 - 1 ↔ x ≤ P − 2
108 107 biimpd ⊢ x ∈ ℕ 0 ∧ P ∈ ℕ 0 → x ≤ P - 1 - 1 → x ≤ P − 2
109 105 108 sylbid ⊢ x ∈ ℕ 0 ∧ P ∈ ℕ 0 → x < P − 1 → x ≤ P − 2
110 109 impancom ⊢ x ∈ ℕ 0 ∧ x < P − 1 → P ∈ ℕ 0 → x ≤ P − 2
111 110 imp ⊢ x ∈ ℕ 0 ∧ x < P − 1 ∧ P ∈ ℕ 0 → x ≤ P − 2
112 nn0re ⊢ x ∈ ℕ 0 → x ∈ ℝ
113 112 adantr ⊢ x ∈ ℕ 0 ∧ x < P − 1 → x ∈ ℝ
114 113 18 anim12i ⊢ x ∈ ℕ 0 ∧ x < P − 1 ∧ P ∈ ℕ 0 → x ∈ ℝ ∧ P − 2 ∈ ℝ
115 lenlt ⊢ x ∈ ℝ ∧ P − 2 ∈ ℝ → x ≤ P − 2 ↔ ¬ P − 2 < x
116 114 115 syl ⊢ x ∈ ℕ 0 ∧ x < P − 1 ∧ P ∈ ℕ 0 → x ≤ P − 2 ↔ ¬ P − 2 < x
117 111 116 mpbid ⊢ x ∈ ℕ 0 ∧ x < P − 1 ∧ P ∈ ℕ 0 → ¬ P − 2 < x
118 117 anim1i ⊢ x ∈ ℕ 0 ∧ x < P − 1 ∧ P ∈ ℕ 0 ∧ ¬ x < P − 2 → ¬ P − 2 < x ∧ ¬ x < P − 2
119 114 ancomd ⊢ x ∈ ℕ 0 ∧ x < P − 1 ∧ P ∈ ℕ 0 → P − 2 ∈ ℝ ∧ x ∈ ℝ
120 119 adantr ⊢ x ∈ ℕ 0 ∧ x < P − 1 ∧ P ∈ ℕ 0 ∧ ¬ x < P − 2 → P − 2 ∈ ℝ ∧ x ∈ ℝ
121 lttri3 ⊢ P − 2 ∈ ℝ ∧ x ∈ ℝ → P − 2 = x ↔ ¬ P − 2 < x ∧ ¬ x < P − 2
122 120 121 syl ⊢ x ∈ ℕ 0 ∧ x < P − 1 ∧ P ∈ ℕ 0 ∧ ¬ x < P − 2 → P − 2 = x ↔ ¬ P − 2 < x ∧ ¬ x < P − 2
123 118 122 mpbird ⊢ x ∈ ℕ 0 ∧ x < P − 1 ∧ P ∈ ℕ 0 ∧ ¬ x < P − 2 → P − 2 = x
124 123 exp31 ⊢ x ∈ ℕ 0 ∧ x < P − 1 → P ∈ ℕ 0 → ¬ x < P − 2 → P − 2 = x
125 124 com23 ⊢ x ∈ ℕ 0 ∧ x < P − 1 → ¬ x < P − 2 → P ∈ ℕ 0 → P − 2 = x
126 125 3adant2 ⊢ x ∈ ℕ 0 ∧ P − 1 ∈ ℕ ∧ x < P − 1 → ¬ x < P − 2 → P ∈ ℕ 0 → P − 2 = x
127 7 126 sylbi ⊢ x ∈ 0 ..^ P − 1 → ¬ x < P − 2 → P ∈ ℕ 0 → P − 2 = x
128 127 impcom ⊢ ¬ x < P − 2 ∧ x ∈ 0 ..^ P − 1 → P ∈ ℕ 0 → P − 2 = x
129 8 128 syl5com ⊢ P ∈ Word V → ¬ x < P − 2 ∧ x ∈ 0 ..^ P − 1 → P − 2 = x
130 129 3ad2ant2 ⊢ E : dom ⁡ E ⟶ 1-1 R ∧ P ∈ Word V ∧ 2 ≤ P → ¬ x < P − 2 ∧ x ∈ 0 ..^ P − 1 → P − 2 = x
131 130 imp ⊢ E : dom ⁡ E ⟶ 1-1 R ∧ P ∈ Word V ∧ 2 ≤ P ∧ ¬ x < P − 2 ∧ x ∈ 0 ..^ P − 1 → P − 2 = x
132 131 fveq2d ⊢ E : dom ⁡ E ⟶ 1-1 R ∧ P ∈ Word V ∧ 2 ≤ P ∧ ¬ x < P − 2 ∧ x ∈ 0 ..^ P − 1 → P ⁡ P − 2 = P ⁡ x
133 132 preq1d ⊢ E : dom ⁡ E ⟶ 1-1 R ∧ P ∈ Word V ∧ 2 ≤ P ∧ ¬ x < P − 2 ∧ x ∈ 0 ..^ P − 1 → P ⁡ P − 2 P ⁡ 0 = P ⁡ x P ⁡ 0
134 133 eleq1d ⊢ E : dom ⁡ E ⟶ 1-1 R ∧ P ∈ Word V ∧ 2 ≤ P ∧ ¬ x < P − 2 ∧ x ∈ 0 ..^ P − 1 → P ⁡ P − 2 P ⁡ 0 ∈ ran ⁡ E ↔ P ⁡ x P ⁡ 0 ∈ ran ⁡ E
135 134 biimpd ⊢ E : dom ⁡ E ⟶ 1-1 R ∧ P ∈ Word V ∧ 2 ≤ P ∧ ¬ x < P − 2 ∧ x ∈ 0 ..^ P − 1 → P ⁡ P − 2 P ⁡ 0 ∈ ran ⁡ E → P ⁡ x P ⁡ 0 ∈ ran ⁡ E
136 135 exp32 ⊢ E : dom ⁡ E ⟶ 1-1 R ∧ P ∈ Word V ∧ 2 ≤ P → ¬ x < P − 2 → x ∈ 0 ..^ P − 1 → P ⁡ P − 2 P ⁡ 0 ∈ ran ⁡ E → P ⁡ x P ⁡ 0 ∈ ran ⁡ E
137 136 com12 ⊢ ¬ x < P − 2 → E : dom ⁡ E ⟶ 1-1 R ∧ P ∈ Word V ∧ 2 ≤ P → x ∈ 0 ..^ P − 1 → P ⁡ P − 2 P ⁡ 0 ∈ ran ⁡ E → P ⁡ x P ⁡ 0 ∈ ran ⁡ E
138 137 com14 ⊢ P ⁡ P − 2 P ⁡ 0 ∈ ran ⁡ E → E : dom ⁡ E ⟶ 1-1 R ∧ P ∈ Word V ∧ 2 ≤ P → x ∈ 0 ..^ P − 1 → ¬ x < P − 2 → P ⁡ x P ⁡ 0 ∈ ran ⁡ E
139 138 adantl ⊢ ∀ i ∈ 0 ..^ P − 1 - 0 - 1 P ⁡ i P ⁡ i + 1 ∈ ran ⁡ E ∧ P ⁡ P − 2 P ⁡ 0 ∈ ran ⁡ E → E : dom ⁡ E ⟶ 1-1 R ∧ P ∈ Word V ∧ 2 ≤ P → x ∈ 0 ..^ P − 1 → ¬ x < P − 2 → P ⁡ x P ⁡ 0 ∈ ran ⁡ E
140 139 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 → E : dom ⁡ E ⟶ 1-1 R ∧ P ∈ Word V ∧ 2 ≤ P → x ∈ 0 ..^ P − 1 → ¬ x < P − 2 → P ⁡ x P ⁡ 0 ∈ ran ⁡ E
141 140 com12 ⊢ E : dom ⁡ E ⟶ 1-1 R ∧ 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 → x ∈ 0 ..^ P − 1 → ¬ x < P − 2 → P ⁡ x P ⁡ 0 ∈ ran ⁡ E
142 141 imp31 ⊢ E : dom ⁡ E ⟶ 1-1 R ∧ 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 ∧ x ∈ 0 ..^ P − 1 → ¬ x < P − 2 → P ⁡ x P ⁡ 0 ∈ ran ⁡ E
143 142 impcom ⊢ ¬ x < P − 2 ∧ E : dom ⁡ E ⟶ 1-1 R ∧ 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 ∧ x ∈ 0 ..^ P − 1 → P ⁡ x P ⁡ 0 ∈ ran ⁡ E
144 f1ocnvdm ⊢ E : dom ⁡ E ⟶ 1-1 onto ran ⁡ E ∧ P ⁡ x P ⁡ 0 ∈ ran ⁡ E → E -1 ⁡ P ⁡ x P ⁡ 0 ∈ dom ⁡ E
145 99 143 144 syl2anc ⊢ ¬ x < P − 2 ∧ E : dom ⁡ E ⟶ 1-1 R ∧ 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 ∧ x ∈ 0 ..^ P − 1 → E -1 ⁡ P ⁡ x P ⁡ 0 ∈ dom ⁡ E
146 98 145 jca ⊢ ¬ x < P − 2 ∧ E : dom ⁡ E ⟶ 1-1 R ∧ 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 ∧ x ∈ 0 ..^ P − 1 → ¬ x < P − 2 ∧ E -1 ⁡ P ⁡ x P ⁡ 0 ∈ dom ⁡ E
147 146 olcd ⊢ ¬ x < P − 2 ∧ E : dom ⁡ E ⟶ 1-1 R ∧ 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 ∧ x ∈ 0 ..^ P − 1 → x < P − 2 ∧ E -1 ⁡ P ⁡ x P ⁡ x + 1 ∈ dom ⁡ E ∨ ¬ x < P − 2 ∧ E -1 ⁡ P ⁡ x P ⁡ 0 ∈ dom ⁡ E
148 97 147 pm2.61ian ⊢ E : dom ⁡ E ⟶ 1-1 R ∧ 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 ∧ x ∈ 0 ..^ P − 1 → x < P − 2 ∧ E -1 ⁡ P ⁡ x P ⁡ x + 1 ∈ dom ⁡ E ∨ ¬ x < P − 2 ∧ E -1 ⁡ P ⁡ x P ⁡ 0 ∈ dom ⁡ E
149 ifel ⊢ if x < P − 2 E -1 ⁡ P ⁡ x P ⁡ x + 1 E -1 ⁡ P ⁡ x P ⁡ 0 ∈ dom ⁡ E ↔ x < P − 2 ∧ E -1 ⁡ P ⁡ x P ⁡ x + 1 ∈ dom ⁡ E ∨ ¬ x < P − 2 ∧ E -1 ⁡ P ⁡ x P ⁡ 0 ∈ dom ⁡ E
150 148 149 sylibr ⊢ E : dom ⁡ E ⟶ 1-1 R ∧ 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 ∧ x ∈ 0 ..^ P − 1 → if x < P − 2 E -1 ⁡ P ⁡ x P ⁡ x + 1 E -1 ⁡ P ⁡ x P ⁡ 0 ∈ dom ⁡ E
151 150 1 fmptd ⊢ E : dom ⁡ E ⟶ 1-1 R ∧ 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 → F : 0 ..^ P − 1 ⟶ dom ⁡ E
152 iswrdi ⊢ F : 0 ..^ P − 1 ⟶ dom ⁡ E → F ∈ Word dom ⁡ E
153 151 152 syl ⊢ E : dom ⁡ E ⟶ 1-1 R ∧ 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 → F ∈ Word dom ⁡ E
154 wrdf ⊢ P ∈ Word V → P : 0 ..^ P ⟶ V
155 154 adantr ⊢ P ∈ Word V ∧ 2 ≤ P → P : 0 ..^ P ⟶ V
156 1 clwlkclwwlklem2a2 ⊢ P ∈ Word V ∧ 2 ≤ P → F = P − 1
157 fzoval ⊢ P ∈ ℤ → 0 ..^ P = 0 … P − 1
158 8 22 157 3syl ⊢ P ∈ Word V → 0 ..^ P = 0 … P − 1
159 oveq2 ⊢ P − 1 = F → 0 … P − 1 = 0 … F
160 159 eqcoms ⊢ F = P − 1 → 0 … P − 1 = 0 … F
161 158 160 sylan9eq ⊢ P ∈ Word V ∧ F = P − 1 → 0 ..^ P = 0 … F
162 156 161 syldan ⊢ P ∈ Word V ∧ 2 ≤ P → 0 ..^ P = 0 … F
163 162 feq2d ⊢ P ∈ Word V ∧ 2 ≤ P → P : 0 ..^ P ⟶ V ↔ P : 0 … F ⟶ V
164 155 163 mpbid ⊢ P ∈ Word V ∧ 2 ≤ P → P : 0 … F ⟶ V
165 164 3adant1 ⊢ E : dom ⁡ E ⟶ 1-1 R ∧ P ∈ Word V ∧ 2 ≤ P → P : 0 … F ⟶ V
166 165 adantr ⊢ E : dom ⁡ E ⟶ 1-1 R ∧ 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 : 0 … F ⟶ V
167 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
168 167 3adant1 ⊢ E : dom ⁡ E ⟶ 1-1 R ∧ 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
169 168 imp ⊢ E : dom ⁡ E ⟶ 1-1 R ∧ 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
170 156 3adant1 ⊢ E : dom ⁡ E ⟶ 1-1 R ∧ P ∈ Word V ∧ 2 ≤ P → F = P − 1
171 170 adantr ⊢ E : dom ⁡ E ⟶ 1-1 R ∧ P ∈ Word V ∧ 2 ≤ P ∧ lastS ⁡ P = P ⁡ 0 → F = P − 1
172 1 clwlkclwwlklem2a4 ⊢ E : dom ⁡ E ⟶ 1-1 R ∧ P ∈ Word V ∧ 2 ≤ P → lastS ⁡ P = P ⁡ 0 ∧ i ∈ 0 ..^ P − 1 → P ⁡ i P ⁡ i + 1 ∈ ran ⁡ E → E ⁡ F ⁡ i = P ⁡ i P ⁡ i + 1
173 172 impl ⊢ E : dom ⁡ E ⟶ 1-1 R ∧ P ∈ Word V ∧ 2 ≤ P ∧ lastS ⁡ P = P ⁡ 0 ∧ i ∈ 0 ..^ P − 1 → P ⁡ i P ⁡ i + 1 ∈ ran ⁡ E → E ⁡ F ⁡ i = P ⁡ i P ⁡ i + 1
174 173 ralimdva ⊢ E : dom ⁡ E ⟶ 1-1 R ∧ P ∈ Word V ∧ 2 ≤ P ∧ lastS ⁡ P = P ⁡ 0 → ∀ i ∈ 0 ..^ P − 1 P ⁡ i P ⁡ i + 1 ∈ ran ⁡ E → ∀ i ∈ 0 ..^ P − 1 E ⁡ F ⁡ i = P ⁡ i P ⁡ i + 1
175 oveq2 ⊢ F = P − 1 → 0 ..^ F = 0 ..^ P − 1
176 175 raleqdv ⊢ F = P − 1 → ∀ i ∈ 0 ..^ F E ⁡ F ⁡ i = P ⁡ i P ⁡ i + 1 ↔ ∀ i ∈ 0 ..^ P − 1 E ⁡ F ⁡ i = P ⁡ i P ⁡ i + 1
177 176 imbi2d ⊢ F = P − 1 → ∀ i ∈ 0 ..^ P − 1 P ⁡ i P ⁡ i + 1 ∈ ran ⁡ E → ∀ i ∈ 0 ..^ F E ⁡ F ⁡ i = P ⁡ i P ⁡ i + 1 ↔ ∀ i ∈ 0 ..^ P − 1 P ⁡ i P ⁡ i + 1 ∈ ran ⁡ E → ∀ i ∈ 0 ..^ P − 1 E ⁡ F ⁡ i = P ⁡ i P ⁡ i + 1
178 174 177 imbitrrid ⊢ F = P − 1 → E : dom ⁡ E ⟶ 1-1 R ∧ P ∈ Word V ∧ 2 ≤ P ∧ lastS ⁡ P = P ⁡ 0 → ∀ i ∈ 0 ..^ P − 1 P ⁡ i P ⁡ i + 1 ∈ ran ⁡ E → ∀ i ∈ 0 ..^ F E ⁡ F ⁡ i = P ⁡ i P ⁡ i + 1
179 171 178 mpcom ⊢ E : dom ⁡ E ⟶ 1-1 R ∧ P ∈ Word V ∧ 2 ≤ P ∧ lastS ⁡ P = P ⁡ 0 → ∀ i ∈ 0 ..^ P − 1 P ⁡ i P ⁡ i + 1 ∈ ran ⁡ E → ∀ i ∈ 0 ..^ F E ⁡ F ⁡ i = P ⁡ i P ⁡ i + 1
180 179 adantrr ⊢ E : dom ⁡ E ⟶ 1-1 R ∧ 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 ..^ F E ⁡ F ⁡ i = P ⁡ i P ⁡ i + 1
181 169 180 mpd ⊢ E : dom ⁡ E ⟶ 1-1 R ∧ 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 ..^ F E ⁡ F ⁡ i = P ⁡ i P ⁡ i + 1
182 153 166 181 3jca ⊢ E : dom ⁡ E ⟶ 1-1 R ∧ 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 → F ∈ Word dom ⁡ E ∧ P : 0 … F ⟶ V ∧ ∀ i ∈ 0 ..^ F E ⁡ F ⁡ i = P ⁡ i P ⁡ i + 1
183 1 clwlkclwwlklem2a3 ⊢ P ∈ Word V ∧ 2 ≤ P → P ⁡ F = lastS ⁡ P
184 183 3adant1 ⊢ E : dom ⁡ E ⟶ 1-1 R ∧ P ∈ Word V ∧ 2 ≤ P → P ⁡ F = lastS ⁡ P
185 184 eqcomd ⊢ E : dom ⁡ E ⟶ 1-1 R ∧ P ∈ Word V ∧ 2 ≤ P → lastS ⁡ P = P ⁡ F
186 185 eqeq2d ⊢ E : dom ⁡ E ⟶ 1-1 R ∧ P ∈ Word V ∧ 2 ≤ P → P ⁡ 0 = lastS ⁡ P ↔ P ⁡ 0 = P ⁡ F
187 186 biimpcd ⊢ P ⁡ 0 = lastS ⁡ P → E : dom ⁡ E ⟶ 1-1 R ∧ P ∈ Word V ∧ 2 ≤ P → P ⁡ 0 = P ⁡ F
188 187 eqcoms ⊢ lastS ⁡ P = P ⁡ 0 → E : dom ⁡ E ⟶ 1-1 R ∧ P ∈ Word V ∧ 2 ≤ P → P ⁡ 0 = P ⁡ F
189 188 adantr ⊢ lastS ⁡ P = P ⁡ 0 ∧ ∀ i ∈ 0 ..^ P − 1 - 0 - 1 P ⁡ i P ⁡ i + 1 ∈ ran ⁡ E ∧ P ⁡ P − 2 P ⁡ 0 ∈ ran ⁡ E → E : dom ⁡ E ⟶ 1-1 R ∧ P ∈ Word V ∧ 2 ≤ P → P ⁡ 0 = P ⁡ F
190 189 impcom ⊢ E : dom ⁡ E ⟶ 1-1 R ∧ 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 ⁡ 0 = P ⁡ F
191 182 190 jca ⊢ E : dom ⁡ E ⟶ 1-1 R ∧ 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 → F ∈ Word dom ⁡ E ∧ P : 0 … F ⟶ V ∧ ∀ i ∈ 0 ..^ F E ⁡ F ⁡ i = P ⁡ i P ⁡ i + 1 ∧ P ⁡ 0 = P ⁡ F
192 191 ex ⊢ E : dom ⁡ E ⟶ 1-1 R ∧ 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 → F ∈ Word dom ⁡ E ∧ P : 0 … F ⟶ V ∧ ∀ i ∈ 0 ..^ F E ⁡ F ⁡ i = P ⁡ i P ⁡ i + 1 ∧ P ⁡ 0 = P ⁡ F