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 ( ( 𝑊 ∈ Word 𝑉 ∧ 1 < ( ♯ ‘ 𝑊 ) ) → ( 𝑊 substr ⟨ ( ( ♯ ‘ 𝑊 ) − 2 ) , ( ♯ ‘ 𝑊 ) ⟩ ) = ⟨“ ( 𝑊 ‘ ( ( ♯ ‘ 𝑊 ) − 2 ) ) ( lastS ‘ 𝑊 ) ”⟩ )

Proof

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