Metamath Proof Explorer

Theorem clwlkclwwlklem2a4

Description: Lemma 4 for clwlkclwwlklem2a . (Contributed by Alexander van der Vekens, 21-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 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

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 fveq2 ⊢ I = P − 2 → F ⁡ I = F ⁡ P − 2
3 lencl ⊢ P ∈ Word V → P ∈ ℕ 0
4 1 clwlkclwwlklem2fv2 ⊢ P ∈ ℕ 0 ∧ 2 ≤ P → F ⁡ P − 2 = E -1 ⁡ P ⁡ P − 2 P ⁡ 0
5 3 4 sylan ⊢ P ∈ Word V ∧ 2 ≤ P → F ⁡ P − 2 = E -1 ⁡ P ⁡ P − 2 P ⁡ 0
6 2 5 sylan9eqr ⊢ P ∈ Word V ∧ 2 ≤ P ∧ I = P − 2 → F ⁡ I = E -1 ⁡ P ⁡ P − 2 P ⁡ 0
7 6 ex ⊢ P ∈ Word V ∧ 2 ≤ P → I = P − 2 → F ⁡ I = E -1 ⁡ P ⁡ P − 2 P ⁡ 0
8 7 3adant1 ⊢ E : dom ⁡ E ⟶ 1-1 R ∧ P ∈ Word V ∧ 2 ≤ P → I = P − 2 → F ⁡ I = E -1 ⁡ P ⁡ P − 2 P ⁡ 0
9 8 ad2antrr ⊢ 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 = P − 2 → F ⁡ I = E -1 ⁡ P ⁡ P − 2 P ⁡ 0
10 9 impcom ⊢ I = P − 2 ∧ 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 → F ⁡ I = E -1 ⁡ P ⁡ P − 2 P ⁡ 0
11 10 fveq2d ⊢ I = P − 2 ∧ 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 = E ⁡ E -1 ⁡ P ⁡ P − 2 P ⁡ 0
12 f1f1orn ⊢ E : dom ⁡ E ⟶ 1-1 R → E : dom ⁡ E ⟶ 1-1 onto ran ⁡ E
13 12 3ad2ant1 ⊢ E : dom ⁡ E ⟶ 1-1 R ∧ P ∈ Word V ∧ 2 ≤ P → E : dom ⁡ E ⟶ 1-1 onto ran ⁡ E
14 13 ad2antrr ⊢ 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 : dom ⁡ E ⟶ 1-1 onto ran ⁡ E
15 lsw ⊢ P ∈ Word V → lastS ⁡ P = P ⁡ P − 1
16 15 eqeq1d ⊢ P ∈ Word V → lastS ⁡ P = P ⁡ 0 ↔ P ⁡ P − 1 = P ⁡ 0
17 nn0cn ⊢ P ∈ ℕ 0 → P ∈ ℂ
18 id ⊢ P ∈ ℂ → P ∈ ℂ
19 2cnd ⊢ P ∈ ℂ → 2 ∈ ℂ
20 1cnd ⊢ P ∈ ℂ → 1 ∈ ℂ
21 18 19 20 subsubd ⊢ P ∈ ℂ → P − 2 − 1 = P - 2 + 1
22 2m1e1 ⊢ 2 − 1 = 1
23 22 a1i ⊢ P ∈ ℂ → 2 − 1 = 1
24 23 oveq2d ⊢ P ∈ ℂ → P − 2 − 1 = P − 1
25 21 24 eqtr3d ⊢ P ∈ ℂ → P - 2 + 1 = P − 1
26 3 17 25 3syl ⊢ P ∈ Word V → P - 2 + 1 = P − 1
27 26 adantr ⊢ P ∈ Word V ∧ P ⁡ P − 1 = P ⁡ 0 → P - 2 + 1 = P − 1
28 27 fveq2d ⊢ P ∈ Word V ∧ P ⁡ P − 1 = P ⁡ 0 → P ⁡ P - 2 + 1 = P ⁡ P − 1
29 eqeq2 ⊢ P ⁡ 0 = P ⁡ P − 1 → P ⁡ P - 2 + 1 = P ⁡ 0 ↔ P ⁡ P - 2 + 1 = P ⁡ P − 1
30 29 eqcoms ⊢ P ⁡ P − 1 = P ⁡ 0 → P ⁡ P - 2 + 1 = P ⁡ 0 ↔ P ⁡ P - 2 + 1 = P ⁡ P − 1
31 30 adantl ⊢ P ∈ Word V ∧ P ⁡ P − 1 = P ⁡ 0 → P ⁡ P - 2 + 1 = P ⁡ 0 ↔ P ⁡ P - 2 + 1 = P ⁡ P − 1
32 28 31 mpbird ⊢ P ∈ Word V ∧ P ⁡ P − 1 = P ⁡ 0 → P ⁡ P - 2 + 1 = P ⁡ 0
33 32 ex ⊢ P ∈ Word V → P ⁡ P − 1 = P ⁡ 0 → P ⁡ P - 2 + 1 = P ⁡ 0
34 16 33 sylbid ⊢ P ∈ Word V → lastS ⁡ P = P ⁡ 0 → P ⁡ P - 2 + 1 = P ⁡ 0
35 34 3ad2ant2 ⊢ E : dom ⁡ E ⟶ 1-1 R ∧ P ∈ Word V ∧ 2 ≤ P → lastS ⁡ P = P ⁡ 0 → P ⁡ P - 2 + 1 = P ⁡ 0
36 35 com12 ⊢ lastS ⁡ P = P ⁡ 0 → E : dom ⁡ E ⟶ 1-1 R ∧ P ∈ Word V ∧ 2 ≤ P → P ⁡ P - 2 + 1 = P ⁡ 0
37 36 adantr ⊢ lastS ⁡ P = P ⁡ 0 ∧ I ∈ 0 ..^ P − 1 → E : dom ⁡ E ⟶ 1-1 R ∧ P ∈ Word V ∧ 2 ≤ P → P ⁡ P - 2 + 1 = P ⁡ 0
38 37 impcom ⊢ E : dom ⁡ E ⟶ 1-1 R ∧ P ∈ Word V ∧ 2 ≤ P ∧ lastS ⁡ P = P ⁡ 0 ∧ I ∈ 0 ..^ P − 1 → P ⁡ P - 2 + 1 = P ⁡ 0
39 38 adantr ⊢ E : dom ⁡ E ⟶ 1-1 R ∧ P ∈ Word V ∧ 2 ≤ P ∧ lastS ⁡ P = P ⁡ 0 ∧ I ∈ 0 ..^ P − 1 ∧ I = P − 2 → P ⁡ P - 2 + 1 = P ⁡ 0
40 39 preq2d ⊢ E : dom ⁡ E ⟶ 1-1 R ∧ P ∈ Word V ∧ 2 ≤ P ∧ lastS ⁡ P = P ⁡ 0 ∧ I ∈ 0 ..^ P − 1 ∧ I = P − 2 → P ⁡ P − 2 P ⁡ P - 2 + 1 = P ⁡ P − 2 P ⁡ 0
41 fveq2 ⊢ I = P − 2 → P ⁡ I = P ⁡ P − 2
42 fvoveq1 ⊢ I = P − 2 → P ⁡ I + 1 = P ⁡ P - 2 + 1
43 41 42 preq12d ⊢ I = P − 2 → P ⁡ I P ⁡ I + 1 = P ⁡ P − 2 P ⁡ P - 2 + 1
44 43 eqeq1d ⊢ I = P − 2 → P ⁡ I P ⁡ I + 1 = P ⁡ P − 2 P ⁡ 0 ↔ P ⁡ P − 2 P ⁡ P - 2 + 1 = P ⁡ P − 2 P ⁡ 0
45 44 adantl ⊢ E : dom ⁡ E ⟶ 1-1 R ∧ P ∈ Word V ∧ 2 ≤ P ∧ lastS ⁡ P = P ⁡ 0 ∧ I ∈ 0 ..^ P − 1 ∧ I = P − 2 → P ⁡ I P ⁡ I + 1 = P ⁡ P − 2 P ⁡ 0 ↔ P ⁡ P − 2 P ⁡ P - 2 + 1 = P ⁡ P − 2 P ⁡ 0
46 40 45 mpbird ⊢ E : dom ⁡ E ⟶ 1-1 R ∧ P ∈ Word V ∧ 2 ≤ P ∧ lastS ⁡ P = P ⁡ 0 ∧ I ∈ 0 ..^ P − 1 ∧ I = P − 2 → P ⁡ I P ⁡ I + 1 = P ⁡ P − 2 P ⁡ 0
47 46 eleq1d ⊢ E : dom ⁡ E ⟶ 1-1 R ∧ P ∈ Word V ∧ 2 ≤ P ∧ lastS ⁡ P = P ⁡ 0 ∧ I ∈ 0 ..^ P − 1 ∧ I = P − 2 → P ⁡ I P ⁡ I + 1 ∈ ran ⁡ E ↔ P ⁡ P − 2 P ⁡ 0 ∈ ran ⁡ E
48 47 biimpd ⊢ E : dom ⁡ E ⟶ 1-1 R ∧ P ∈ Word V ∧ 2 ≤ P ∧ lastS ⁡ P = P ⁡ 0 ∧ I ∈ 0 ..^ P − 1 ∧ I = P − 2 → P ⁡ I P ⁡ I + 1 ∈ ran ⁡ E → P ⁡ P − 2 P ⁡ 0 ∈ ran ⁡ E
49 48 impancom ⊢ 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 = P − 2 → P ⁡ P − 2 P ⁡ 0 ∈ ran ⁡ E
50 49 impcom ⊢ I = P − 2 ∧ 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 → P ⁡ P − 2 P ⁡ 0 ∈ ran ⁡ E
51 f1ocnvfv2 ⊢ E : dom ⁡ E ⟶ 1-1 onto ran ⁡ E ∧ P ⁡ P − 2 P ⁡ 0 ∈ ran ⁡ E → E ⁡ E -1 ⁡ P ⁡ P − 2 P ⁡ 0 = P ⁡ P − 2 P ⁡ 0
52 14 50 51 syl2an2 ⊢ I = P − 2 ∧ 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 ⁡ E -1 ⁡ P ⁡ P − 2 P ⁡ 0 = P ⁡ P − 2 P ⁡ 0
53 eqcom ⊢ P ⁡ P − 1 = P ⁡ 0 ↔ P ⁡ 0 = P ⁡ P − 1
54 53 biimpi ⊢ P ⁡ P − 1 = P ⁡ 0 → P ⁡ 0 = P ⁡ P − 1
55 1e2m1 ⊢ 1 = 2 − 1
56 55 a1i ⊢ P ∈ Word V → 1 = 2 − 1
57 56 oveq2d ⊢ P ∈ Word V → P − 1 = P − 2 − 1
58 3 17 syl ⊢ P ∈ Word V → P ∈ ℂ
59 2cnd ⊢ P ∈ Word V → 2 ∈ ℂ
60 1cnd ⊢ P ∈ Word V → 1 ∈ ℂ
61 58 59 60 subsubd ⊢ P ∈ Word V → P − 2 − 1 = P - 2 + 1
62 57 61 eqtrd ⊢ P ∈ Word V → P − 1 = P - 2 + 1
63 62 fveq2d ⊢ P ∈ Word V → P ⁡ P − 1 = P ⁡ P - 2 + 1
64 54 63 sylan9eqr ⊢ P ∈ Word V ∧ P ⁡ P − 1 = P ⁡ 0 → P ⁡ 0 = P ⁡ P - 2 + 1
65 64 ex ⊢ P ∈ Word V → P ⁡ P − 1 = P ⁡ 0 → P ⁡ 0 = P ⁡ P - 2 + 1
66 16 65 sylbid ⊢ P ∈ Word V → lastS ⁡ P = P ⁡ 0 → P ⁡ 0 = P ⁡ P - 2 + 1
67 66 imp ⊢ P ∈ Word V ∧ lastS ⁡ P = P ⁡ 0 → P ⁡ 0 = P ⁡ P - 2 + 1
68 67 preq2d ⊢ P ∈ Word V ∧ lastS ⁡ P = P ⁡ 0 → P ⁡ P − 2 P ⁡ 0 = P ⁡ P − 2 P ⁡ P - 2 + 1
69 68 adantr ⊢ P ∈ Word V ∧ lastS ⁡ P = P ⁡ 0 ∧ I = P − 2 → P ⁡ P − 2 P ⁡ 0 = P ⁡ P − 2 P ⁡ P - 2 + 1
70 43 adantl ⊢ P ∈ Word V ∧ lastS ⁡ P = P ⁡ 0 ∧ I = P − 2 → P ⁡ I P ⁡ I + 1 = P ⁡ P − 2 P ⁡ P - 2 + 1
71 69 70 eqtr4d ⊢ P ∈ Word V ∧ lastS ⁡ P = P ⁡ 0 ∧ I = P − 2 → P ⁡ P − 2 P ⁡ 0 = P ⁡ I P ⁡ I + 1
72 71 exp31 ⊢ P ∈ Word V → lastS ⁡ P = P ⁡ 0 → I = P − 2 → P ⁡ P − 2 P ⁡ 0 = P ⁡ I P ⁡ I + 1
73 72 3ad2ant2 ⊢ E : dom ⁡ E ⟶ 1-1 R ∧ P ∈ Word V ∧ 2 ≤ P → lastS ⁡ P = P ⁡ 0 → I = P − 2 → P ⁡ P − 2 P ⁡ 0 = P ⁡ I P ⁡ I + 1
74 73 com12 ⊢ lastS ⁡ P = P ⁡ 0 → E : dom ⁡ E ⟶ 1-1 R ∧ P ∈ Word V ∧ 2 ≤ P → I = P − 2 → P ⁡ P − 2 P ⁡ 0 = P ⁡ I P ⁡ I + 1
75 74 adantr ⊢ lastS ⁡ P = P ⁡ 0 ∧ I ∈ 0 ..^ P − 1 → E : dom ⁡ E ⟶ 1-1 R ∧ P ∈ Word V ∧ 2 ≤ P → I = P − 2 → P ⁡ P − 2 P ⁡ 0 = P ⁡ I P ⁡ I + 1
76 75 impcom ⊢ E : dom ⁡ E ⟶ 1-1 R ∧ P ∈ Word V ∧ 2 ≤ P ∧ lastS ⁡ P = P ⁡ 0 ∧ I ∈ 0 ..^ P − 1 → I = P − 2 → P ⁡ P − 2 P ⁡ 0 = P ⁡ I P ⁡ I + 1
77 76 adantr ⊢ 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 = P − 2 → P ⁡ P − 2 P ⁡ 0 = P ⁡ I P ⁡ I + 1
78 77 impcom ⊢ I = P − 2 ∧ 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 → P ⁡ P − 2 P ⁡ 0 = P ⁡ I P ⁡ I + 1
79 11 52 78 3eqtrd ⊢ I = P − 2 ∧ 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
80 simpll ⊢ P ∈ ℕ 0 ∧ 2 ≤ P ∧ I ∈ 0 ..^ P − 1 ∧ ¬ I = P − 2 → P ∈ ℕ 0
81 oveq1 ⊢ P = 2 → P − 1 = 2 − 1
82 81 22 eqtrdi ⊢ P = 2 → P − 1 = 1
83 82 oveq2d ⊢ P = 2 → 0 ..^ P − 1 = 0 ..^ 1
84 83 eleq2d ⊢ P = 2 → I ∈ 0 ..^ P − 1 ↔ I ∈ 0 ..^ 1
85 oveq1 ⊢ P = 2 → P − 2 = 2 − 2
86 2cn ⊢ 2 ∈ ℂ
87 86 subidi ⊢ 2 − 2 = 0
88 85 87 eqtrdi ⊢ P = 2 → P − 2 = 0
89 88 eqeq2d ⊢ P = 2 → I = P − 2 ↔ I = 0
90 89 notbid ⊢ P = 2 → ¬ I = P − 2 ↔ ¬ I = 0
91 84 90 anbi12d ⊢ P = 2 → I ∈ 0 ..^ P − 1 ∧ ¬ I = P − 2 ↔ I ∈ 0 ..^ 1 ∧ ¬ I = 0
92 elsni ⊢ I ∈ 0 → I = 0
93 92 pm2.24d ⊢ I ∈ 0 → ¬ I = 0 → I ∈ ℕ 0 ∧ P − 2 ∈ ℕ ∧ I < P − 2
94 fzo01 ⊢ 0 ..^ 1 = 0
95 93 94 eleq2s ⊢ I ∈ 0 ..^ 1 → ¬ I = 0 → I ∈ ℕ 0 ∧ P − 2 ∈ ℕ ∧ I < P − 2
96 95 imp ⊢ I ∈ 0 ..^ 1 ∧ ¬ I = 0 → I ∈ ℕ 0 ∧ P − 2 ∈ ℕ ∧ I < P − 2
97 91 96 syl6bi ⊢ P = 2 → I ∈ 0 ..^ P − 1 ∧ ¬ I = P − 2 → I ∈ ℕ 0 ∧ P − 2 ∈ ℕ ∧ I < P − 2
98 97 adantld ⊢ P = 2 → P ∈ ℕ 0 ∧ 2 ≤ P ∧ I ∈ 0 ..^ P − 1 ∧ ¬ I = P − 2 → I ∈ ℕ 0 ∧ P − 2 ∈ ℕ ∧ I < P − 2
99 df-ne ⊢ P ≠ 2 ↔ ¬ P = 2
100 2re ⊢ 2 ∈ ℝ
101 100 a1i ⊢ P ∈ ℕ 0 ∧ 2 ≤ P → 2 ∈ ℝ
102 nn0re ⊢ P ∈ ℕ 0 → P ∈ ℝ
103 102 adantr ⊢ P ∈ ℕ 0 ∧ 2 ≤ P → P ∈ ℝ
104 simpr ⊢ P ∈ ℕ 0 ∧ 2 ≤ P → 2 ≤ P
105 101 103 104 leltned ⊢ P ∈ ℕ 0 ∧ 2 ≤ P → 2 < P ↔ P ≠ 2
106 elfzo0 ⊢ I ∈ 0 ..^ P − 1 ↔ I ∈ ℕ 0 ∧ P − 1 ∈ ℕ ∧ I < P − 1
107 simp-4l ⊢ I ∈ ℕ 0 ∧ P ∈ ℕ 0 ∧ ¬ I = P − 2 ∧ 2 < P ∧ I < P − 1 → I ∈ ℕ 0
108 nn0z ⊢ P ∈ ℕ 0 → P ∈ ℤ
109 2z ⊢ 2 ∈ ℤ
110 109 a1i ⊢ P ∈ ℕ 0 → 2 ∈ ℤ
111 108 110 zsubcld ⊢ P ∈ ℕ 0 → P − 2 ∈ ℤ
112 111 adantr ⊢ P ∈ ℕ 0 ∧ 2 < P → P − 2 ∈ ℤ
113 100 a1i ⊢ P ∈ ℕ 0 → 2 ∈ ℝ
114 113 102 posdifd ⊢ P ∈ ℕ 0 → 2 < P ↔ 0 < P − 2
115 114 biimpa ⊢ P ∈ ℕ 0 ∧ 2 < P → 0 < P − 2
116 elnnz ⊢ P − 2 ∈ ℕ ↔ P − 2 ∈ ℤ ∧ 0 < P − 2
117 112 115 116 sylanbrc ⊢ P ∈ ℕ 0 ∧ 2 < P → P − 2 ∈ ℕ
118 117 ad5ant24 ⊢ I ∈ ℕ 0 ∧ P ∈ ℕ 0 ∧ ¬ I = P − 2 ∧ 2 < P ∧ I < P − 1 → P − 2 ∈ ℕ
119 nn0z ⊢ I ∈ ℕ 0 → I ∈ ℤ
120 peano2zm ⊢ P ∈ ℤ → P − 1 ∈ ℤ
121 108 120 syl ⊢ P ∈ ℕ 0 → P − 1 ∈ ℤ
122 zltlem1 ⊢ I ∈ ℤ ∧ P − 1 ∈ ℤ → I < P − 1 ↔ I ≤ P - 1 - 1
123 119 121 122 syl2an ⊢ I ∈ ℕ 0 ∧ P ∈ ℕ 0 → I < P − 1 ↔ I ≤ P - 1 - 1
124 17 adantl ⊢ I ∈ ℕ 0 ∧ P ∈ ℕ 0 → P ∈ ℂ
125 1cnd ⊢ I ∈ ℕ 0 ∧ P ∈ ℕ 0 → 1 ∈ ℂ
126 124 125 125 subsub4d ⊢ I ∈ ℕ 0 ∧ P ∈ ℕ 0 → P - 1 - 1 = P − 1 + 1
127 1p1e2 ⊢ 1 + 1 = 2
128 127 a1i ⊢ I ∈ ℕ 0 ∧ P ∈ ℕ 0 → 1 + 1 = 2
129 128 oveq2d ⊢ I ∈ ℕ 0 ∧ P ∈ ℕ 0 → P − 1 + 1 = P − 2
130 126 129 eqtrd ⊢ I ∈ ℕ 0 ∧ P ∈ ℕ 0 → P - 1 - 1 = P − 2
131 130 breq2d ⊢ I ∈ ℕ 0 ∧ P ∈ ℕ 0 → I ≤ P - 1 - 1 ↔ I ≤ P − 2
132 123 131 bitrd ⊢ I ∈ ℕ 0 ∧ P ∈ ℕ 0 → I < P − 1 ↔ I ≤ P − 2
133 necom ⊢ P − 2 ≠ I ↔ I ≠ P − 2
134 df-ne ⊢ I ≠ P − 2 ↔ ¬ I = P − 2
135 133 134 bitr2i ⊢ ¬ I = P − 2 ↔ P − 2 ≠ I
136 nn0re ⊢ I ∈ ℕ 0 → I ∈ ℝ
137 136 ad2antrr ⊢ I ∈ ℕ 0 ∧ P ∈ ℕ 0 ∧ I ≤ P − 2 → I ∈ ℝ
138 102 113 resubcld ⊢ P ∈ ℕ 0 → P − 2 ∈ ℝ
139 138 ad2antlr ⊢ I ∈ ℕ 0 ∧ P ∈ ℕ 0 ∧ I ≤ P − 2 → P − 2 ∈ ℝ
140 simpr ⊢ I ∈ ℕ 0 ∧ P ∈ ℕ 0 ∧ I ≤ P − 2 → I ≤ P − 2
141 leltne ⊢ I ∈ ℝ ∧ P − 2 ∈ ℝ ∧ I ≤ P − 2 → I < P − 2 ↔ P − 2 ≠ I
142 141 bicomd ⊢ I ∈ ℝ ∧ P − 2 ∈ ℝ ∧ I ≤ P − 2 → P − 2 ≠ I ↔ I < P − 2
143 137 139 140 142 syl3anc ⊢ I ∈ ℕ 0 ∧ P ∈ ℕ 0 ∧ I ≤ P − 2 → P − 2 ≠ I ↔ I < P − 2
144 143 biimpd ⊢ I ∈ ℕ 0 ∧ P ∈ ℕ 0 ∧ I ≤ P − 2 → P − 2 ≠ I → I < P − 2
145 135 144 syl5bi ⊢ I ∈ ℕ 0 ∧ P ∈ ℕ 0 ∧ I ≤ P − 2 → ¬ I = P − 2 → I < P − 2
146 145 ex ⊢ I ∈ ℕ 0 ∧ P ∈ ℕ 0 → I ≤ P − 2 → ¬ I = P − 2 → I < P − 2
147 132 146 sylbid ⊢ I ∈ ℕ 0 ∧ P ∈ ℕ 0 → I < P − 1 → ¬ I = P − 2 → I < P − 2
148 147 com23 ⊢ I ∈ ℕ 0 ∧ P ∈ ℕ 0 → ¬ I = P − 2 → I < P − 1 → I < P − 2
149 148 imp ⊢ I ∈ ℕ 0 ∧ P ∈ ℕ 0 ∧ ¬ I = P − 2 → I < P − 1 → I < P − 2
150 149 adantr ⊢ I ∈ ℕ 0 ∧ P ∈ ℕ 0 ∧ ¬ I = P − 2 ∧ 2 < P → I < P − 1 → I < P − 2
151 150 imp ⊢ I ∈ ℕ 0 ∧ P ∈ ℕ 0 ∧ ¬ I = P − 2 ∧ 2 < P ∧ I < P − 1 → I < P − 2
152 107 118 151 3jca ⊢ I ∈ ℕ 0 ∧ P ∈ ℕ 0 ∧ ¬ I = P − 2 ∧ 2 < P ∧ I < P − 1 → I ∈ ℕ 0 ∧ P − 2 ∈ ℕ ∧ I < P − 2
153 152 ex ⊢ I ∈ ℕ 0 ∧ P ∈ ℕ 0 ∧ ¬ I = P − 2 ∧ 2 < P → I < P − 1 → I ∈ ℕ 0 ∧ P − 2 ∈ ℕ ∧ I < P − 2
154 153 exp41 ⊢ I ∈ ℕ 0 → P ∈ ℕ 0 → ¬ I = P − 2 → 2 < P → I < P − 1 → I ∈ ℕ 0 ∧ P − 2 ∈ ℕ ∧ I < P − 2
155 154 com25 ⊢ I ∈ ℕ 0 → I < P − 1 → ¬ I = P − 2 → 2 < P → P ∈ ℕ 0 → I ∈ ℕ 0 ∧ P − 2 ∈ ℕ ∧ I < P − 2
156 155 imp ⊢ I ∈ ℕ 0 ∧ I < P − 1 → ¬ I = P − 2 → 2 < P → P ∈ ℕ 0 → I ∈ ℕ 0 ∧ P − 2 ∈ ℕ ∧ I < P − 2
157 156 3adant2 ⊢ I ∈ ℕ 0 ∧ P − 1 ∈ ℕ ∧ I < P − 1 → ¬ I = P − 2 → 2 < P → P ∈ ℕ 0 → I ∈ ℕ 0 ∧ P − 2 ∈ ℕ ∧ I < P − 2
158 106 157 sylbi ⊢ I ∈ 0 ..^ P − 1 → ¬ I = P − 2 → 2 < P → P ∈ ℕ 0 → I ∈ ℕ 0 ∧ P − 2 ∈ ℕ ∧ I < P − 2
159 158 imp ⊢ I ∈ 0 ..^ P − 1 ∧ ¬ I = P − 2 → 2 < P → P ∈ ℕ 0 → I ∈ ℕ 0 ∧ P − 2 ∈ ℕ ∧ I < P − 2
160 159 com13 ⊢ P ∈ ℕ 0 → 2 < P → I ∈ 0 ..^ P − 1 ∧ ¬ I = P − 2 → I ∈ ℕ 0 ∧ P − 2 ∈ ℕ ∧ I < P − 2
161 160 adantr ⊢ P ∈ ℕ 0 ∧ 2 ≤ P → 2 < P → I ∈ 0 ..^ P − 1 ∧ ¬ I = P − 2 → I ∈ ℕ 0 ∧ P − 2 ∈ ℕ ∧ I < P − 2
162 105 161 sylbird ⊢ P ∈ ℕ 0 ∧ 2 ≤ P → P ≠ 2 → I ∈ 0 ..^ P − 1 ∧ ¬ I = P − 2 → I ∈ ℕ 0 ∧ P − 2 ∈ ℕ ∧ I < P − 2
163 99 162 syl5bir ⊢ P ∈ ℕ 0 ∧ 2 ≤ P → ¬ P = 2 → I ∈ 0 ..^ P − 1 ∧ ¬ I = P − 2 → I ∈ ℕ 0 ∧ P − 2 ∈ ℕ ∧ I < P − 2
164 163 com23 ⊢ P ∈ ℕ 0 ∧ 2 ≤ P → I ∈ 0 ..^ P − 1 ∧ ¬ I = P − 2 → ¬ P = 2 → I ∈ ℕ 0 ∧ P − 2 ∈ ℕ ∧ I < P − 2
165 164 imp ⊢ P ∈ ℕ 0 ∧ 2 ≤ P ∧ I ∈ 0 ..^ P − 1 ∧ ¬ I = P − 2 → ¬ P = 2 → I ∈ ℕ 0 ∧ P − 2 ∈ ℕ ∧ I < P − 2
166 165 com12 ⊢ ¬ P = 2 → P ∈ ℕ 0 ∧ 2 ≤ P ∧ I ∈ 0 ..^ P − 1 ∧ ¬ I = P − 2 → I ∈ ℕ 0 ∧ P − 2 ∈ ℕ ∧ I < P − 2
167 98 166 pm2.61i ⊢ P ∈ ℕ 0 ∧ 2 ≤ P ∧ I ∈ 0 ..^ P − 1 ∧ ¬ I = P − 2 → I ∈ ℕ 0 ∧ P − 2 ∈ ℕ ∧ I < P − 2
168 elfzo0 ⊢ I ∈ 0 ..^ P − 2 ↔ I ∈ ℕ 0 ∧ P − 2 ∈ ℕ ∧ I < P − 2
169 167 168 sylibr ⊢ P ∈ ℕ 0 ∧ 2 ≤ P ∧ I ∈ 0 ..^ P − 1 ∧ ¬ I = P − 2 → I ∈ 0 ..^ P − 2
170 80 169 jca ⊢ P ∈ ℕ 0 ∧ 2 ≤ P ∧ I ∈ 0 ..^ P − 1 ∧ ¬ I = P − 2 → P ∈ ℕ 0 ∧ I ∈ 0 ..^ P − 2
171 170 exp31 ⊢ P ∈ ℕ 0 → 2 ≤ P → I ∈ 0 ..^ P − 1 ∧ ¬ I = P − 2 → P ∈ ℕ 0 ∧ I ∈ 0 ..^ P − 2
172 3 171 syl ⊢ P ∈ Word V → 2 ≤ P → I ∈ 0 ..^ P − 1 ∧ ¬ I = P − 2 → P ∈ ℕ 0 ∧ I ∈ 0 ..^ P − 2
173 172 imp ⊢ P ∈ Word V ∧ 2 ≤ P → I ∈ 0 ..^ P − 1 ∧ ¬ I = P − 2 → P ∈ ℕ 0 ∧ I ∈ 0 ..^ P − 2
174 173 3adant1 ⊢ E : dom ⁡ E ⟶ 1-1 R ∧ P ∈ Word V ∧ 2 ≤ P → I ∈ 0 ..^ P − 1 ∧ ¬ I = P − 2 → P ∈ ℕ 0 ∧ I ∈ 0 ..^ P − 2
175 174 expd ⊢ E : dom ⁡ E ⟶ 1-1 R ∧ P ∈ Word V ∧ 2 ≤ P → I ∈ 0 ..^ P − 1 → ¬ I = P − 2 → P ∈ ℕ 0 ∧ I ∈ 0 ..^ P − 2
176 175 com12 ⊢ I ∈ 0 ..^ P − 1 → E : dom ⁡ E ⟶ 1-1 R ∧ P ∈ Word V ∧ 2 ≤ P → ¬ I = P − 2 → P ∈ ℕ 0 ∧ I ∈ 0 ..^ P − 2
177 176 adantl ⊢ lastS ⁡ P = P ⁡ 0 ∧ I ∈ 0 ..^ P − 1 → E : dom ⁡ E ⟶ 1-1 R ∧ P ∈ Word V ∧ 2 ≤ P → ¬ I = P − 2 → P ∈ ℕ 0 ∧ I ∈ 0 ..^ P − 2
178 177 impcom ⊢ E : dom ⁡ E ⟶ 1-1 R ∧ P ∈ Word V ∧ 2 ≤ P ∧ lastS ⁡ P = P ⁡ 0 ∧ I ∈ 0 ..^ P − 1 → ¬ I = P − 2 → P ∈ ℕ 0 ∧ I ∈ 0 ..^ P − 2
179 178 adantr ⊢ 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 = P − 2 → P ∈ ℕ 0 ∧ I ∈ 0 ..^ P − 2
180 179 impcom ⊢ ¬ I = P − 2 ∧ 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 → P ∈ ℕ 0 ∧ I ∈ 0 ..^ P − 2
181 1 clwlkclwwlklem2fv1 ⊢ P ∈ ℕ 0 ∧ I ∈ 0 ..^ P − 2 → F ⁡ I = E -1 ⁡ P ⁡ I P ⁡ I + 1
182 180 181 syl ⊢ ¬ I = P − 2 ∧ 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 → F ⁡ I = E -1 ⁡ P ⁡ I P ⁡ I + 1
183 182 fveq2d ⊢ ¬ I = P − 2 ∧ 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 = E ⁡ E -1 ⁡ P ⁡ I P ⁡ I + 1
184 simprr ⊢ ¬ I = P − 2 ∧ 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 → P ⁡ I P ⁡ I + 1 ∈ ran ⁡ E
185 f1ocnvfv2 ⊢ E : dom ⁡ E ⟶ 1-1 onto ran ⁡ E ∧ P ⁡ I P ⁡ I + 1 ∈ ran ⁡ E → E ⁡ E -1 ⁡ P ⁡ I P ⁡ I + 1 = P ⁡ I P ⁡ I + 1
186 14 184 185 syl2an2 ⊢ ¬ I = P − 2 ∧ 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 ⁡ E -1 ⁡ P ⁡ I P ⁡ I + 1 = P ⁡ I P ⁡ I + 1
187 183 186 eqtrd ⊢ ¬ I = P − 2 ∧ 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
188 79 187 pm2.61ian ⊢ 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
189 188 exp31 ⊢ 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