Metamath Proof Explorer

Theorem swrd2lsw

Description: Extract the last two symbols from a word. (Contributed by Alexander van der Vekens, 23-Sep-2018)

Ref Expression
Assertion swrd2lsw ⊢ W ∈ Word V ∧ 1 < W → W substr W − 2 W = ⟨“ W ⁡ W − 2 lastS ⁡ W ”⟩

Proof

Step Hyp Ref Expression
1 simpl ⊢ W ∈ Word V ∧ 1 < W → W ∈ Word V
2 lencl ⊢ W ∈ Word V → W ∈ ℕ 0
3 1z ⊢ 1 ∈ ℤ
4 nn0z ⊢ W ∈ ℕ 0 → W ∈ ℤ
5 zltp1le ⊢ 1 ∈ ℤ ∧ W ∈ ℤ → 1 < W ↔ 1 + 1 ≤ W
6 3 4 5 sylancr ⊢ W ∈ ℕ 0 → 1 < W ↔ 1 + 1 ≤ W
7 1p1e2 ⊢ 1 + 1 = 2
8 7 a1i ⊢ W ∈ ℕ 0 → 1 + 1 = 2
9 8 breq1d ⊢ W ∈ ℕ 0 → 1 + 1 ≤ W ↔ 2 ≤ W
10 9 biimpd ⊢ W ∈ ℕ 0 → 1 + 1 ≤ W → 2 ≤ W
11 6 10 sylbid ⊢ W ∈ ℕ 0 → 1 < W → 2 ≤ W
12 11 imp ⊢ W ∈ ℕ 0 ∧ 1 < W → 2 ≤ W
13 2nn0 ⊢ 2 ∈ ℕ 0
14 13 jctl ⊢ W ∈ ℕ 0 → 2 ∈ ℕ 0 ∧ W ∈ ℕ 0
15 14 adantr ⊢ W ∈ ℕ 0 ∧ 1 < W → 2 ∈ ℕ 0 ∧ W ∈ ℕ 0
16 nn0sub ⊢ 2 ∈ ℕ 0 ∧ W ∈ ℕ 0 → 2 ≤ W ↔ W − 2 ∈ ℕ 0
17 15 16 syl ⊢ W ∈ ℕ 0 ∧ 1 < W → 2 ≤ W ↔ W − 2 ∈ ℕ 0
18 12 17 mpbid ⊢ W ∈ ℕ 0 ∧ 1 < W → W − 2 ∈ ℕ 0
19 2 18 sylan ⊢ W ∈ Word V ∧ 1 < W → W − 2 ∈ ℕ 0
20 0red ⊢ W ∈ ℤ → 0 ∈ ℝ
21 1red ⊢ W ∈ ℤ → 1 ∈ ℝ
22 zre ⊢ W ∈ ℤ → W ∈ ℝ
23 20 21 22 3jca ⊢ W ∈ ℤ → 0 ∈ ℝ ∧ 1 ∈ ℝ ∧ W ∈ ℝ
24 0lt1 ⊢ 0 < 1
25 lttr ⊢ 0 ∈ ℝ ∧ 1 ∈ ℝ ∧ W ∈ ℝ → 0 < 1 ∧ 1 < W → 0 < W
26 25 expd ⊢ 0 ∈ ℝ ∧ 1 ∈ ℝ ∧ W ∈ ℝ → 0 < 1 → 1 < W → 0 < W
27 23 24 26 mpisyl ⊢ W ∈ ℤ → 1 < W → 0 < W
28 elnnz ⊢ W ∈ ℕ ↔ W ∈ ℤ ∧ 0 < W
29 28 simplbi2 ⊢ W ∈ ℤ → 0 < W → W ∈ ℕ
30 27 29 syld ⊢ W ∈ ℤ → 1 < W → W ∈ ℕ
31 4 30 syl ⊢ W ∈ ℕ 0 → 1 < W → W ∈ ℕ
32 31 imp ⊢ W ∈ ℕ 0 ∧ 1 < W → W ∈ ℕ
33 fzo0end ⊢ W ∈ ℕ → W − 1 ∈ 0 ..^ W
34 32 33 syl ⊢ W ∈ ℕ 0 ∧ 1 < W → W − 1 ∈ 0 ..^ W
35 nn0cn ⊢ W ∈ ℕ 0 → W ∈ ℂ
36 2cn ⊢ 2 ∈ ℂ
37 36 a1i ⊢ W ∈ ℕ 0 → 2 ∈ ℂ
38 1cnd ⊢ W ∈ ℕ 0 → 1 ∈ ℂ
39 35 37 38 3jca ⊢ W ∈ ℕ 0 → W ∈ ℂ ∧ 2 ∈ ℂ ∧ 1 ∈ ℂ
40 1e2m1 ⊢ 1 = 2 − 1
41 40 a1i ⊢ W ∈ ℂ ∧ 2 ∈ ℂ ∧ 1 ∈ ℂ → 1 = 2 − 1
42 41 oveq2d ⊢ W ∈ ℂ ∧ 2 ∈ ℂ ∧ 1 ∈ ℂ → W − 1 = W − 2 − 1
43 subsub ⊢ W ∈ ℂ ∧ 2 ∈ ℂ ∧ 1 ∈ ℂ → W − 2 − 1 = W - 2 + 1
44 42 43 eqtrd ⊢ W ∈ ℂ ∧ 2 ∈ ℂ ∧ 1 ∈ ℂ → W − 1 = W - 2 + 1
45 39 44 syl ⊢ W ∈ ℕ 0 → W − 1 = W - 2 + 1
46 45 eqcomd ⊢ W ∈ ℕ 0 → W - 2 + 1 = W − 1
47 46 eleq1d ⊢ W ∈ ℕ 0 → W - 2 + 1 ∈ 0 ..^ W ↔ W − 1 ∈ 0 ..^ W
48 47 adantr ⊢ W ∈ ℕ 0 ∧ 1 < W → W - 2 + 1 ∈ 0 ..^ W ↔ W − 1 ∈ 0 ..^ W
49 34 48 mpbird ⊢ W ∈ ℕ 0 ∧ 1 < W → W - 2 + 1 ∈ 0 ..^ W
50 2 49 sylan ⊢ W ∈ Word V ∧ 1 < W → W - 2 + 1 ∈ 0 ..^ W
51 1 19 50 3jca ⊢ W ∈ Word V ∧ 1 < W → W ∈ Word V ∧ W − 2 ∈ ℕ 0 ∧ W - 2 + 1 ∈ 0 ..^ W
52 swrds2 ⊢ W ∈ Word V ∧ W − 2 ∈ ℕ 0 ∧ W - 2 + 1 ∈ 0 ..^ W → W substr W − 2 W - 2 + 2 = ⟨“ W ⁡ W − 2 W ⁡ W - 2 + 1 ”⟩
53 51 52 syl ⊢ W ∈ Word V ∧ 1 < W → W substr W − 2 W - 2 + 2 = ⟨“ W ⁡ W − 2 W ⁡ W - 2 + 1 ”⟩
54 35 36 jctir ⊢ W ∈ ℕ 0 → W ∈ ℂ ∧ 2 ∈ ℂ
55 npcan ⊢ W ∈ ℂ ∧ 2 ∈ ℂ → W - 2 + 2 = W
56 55 eqcomd ⊢ W ∈ ℂ ∧ 2 ∈ ℂ → W = W - 2 + 2
57 2 54 56 3syl ⊢ W ∈ Word V → W = W - 2 + 2
58 57 adantr ⊢ W ∈ Word V ∧ 1 < W → W = W - 2 + 2
59 58 opeq2d ⊢ W ∈ Word V ∧ 1 < W → W − 2 W = W − 2 W - 2 + 2
60 59 oveq2d ⊢ W ∈ Word V ∧ 1 < W → W substr W − 2 W = W substr W − 2 W - 2 + 2
61 eqidd ⊢ W ∈ Word V ∧ 1 < W → W ⁡ W − 2 = W ⁡ W − 2
62 lsw ⊢ W ∈ Word V → lastS ⁡ W = W ⁡ W − 1
63 39 43 syl ⊢ W ∈ ℕ 0 → W − 2 − 1 = W - 2 + 1
64 63 eqcomd ⊢ W ∈ ℕ 0 → W - 2 + 1 = W − 2 − 1
65 2m1e1 ⊢ 2 − 1 = 1
66 65 a1i ⊢ W ∈ ℕ 0 → 2 − 1 = 1
67 66 oveq2d ⊢ W ∈ ℕ 0 → W − 2 − 1 = W − 1
68 64 67 eqtrd ⊢ W ∈ ℕ 0 → W - 2 + 1 = W − 1
69 2 68 syl ⊢ W ∈ Word V → W - 2 + 1 = W − 1
70 69 eqcomd ⊢ W ∈ Word V → W − 1 = W - 2 + 1
71 70 fveq2d ⊢ W ∈ Word V → W ⁡ W − 1 = W ⁡ W - 2 + 1
72 62 71 eqtrd ⊢ W ∈ Word V → lastS ⁡ W = W ⁡ W - 2 + 1
73 72 adantr ⊢ W ∈ Word V ∧ 1 < W → lastS ⁡ W = W ⁡ W - 2 + 1
74 61 73 s2eqd ⊢ W ∈ Word V ∧ 1 < W → ⟨“ W ⁡ W − 2 lastS ⁡ W ”⟩ = ⟨“ W ⁡ W − 2 W ⁡ W - 2 + 1 ”⟩
75 53 60 74 3eqtr4d ⊢ W ∈ Word V ∧ 1 < W → W substr W − 2 W = ⟨“ W ⁡ W − 2 lastS ⁡ W ”⟩