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∈WordV∧1<W→WsubstrW−2W=⟨“W⁡W−2lastS⁡W”⟩

Proof

Step Hyp Ref Expression
1 simpl ⊢W∈WordV∧1<W→W∈WordV
2 lencl ⊢W∈WordV→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∈WordV∧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∈WordV∧1<W→W-2+1∈0..^W
51 1 19 50 3jca ⊢W∈WordV∧1<W→W∈WordV∧W−2∈ℕ0∧W-2+1∈0..^W
52 swrds2 ⊢W∈WordV∧W−2∈ℕ0∧W-2+1∈0..^W→WsubstrW−2W-2+2=⟨“W⁡W−2W⁡W-2+1”⟩
53 51 52 syl ⊢W∈WordV∧1<W→WsubstrW−2W-2+2=⟨“W⁡W−2W⁡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∈WordV→W=W-2+2
58 57 adantr ⊢W∈WordV∧1<W→W=W-2+2
59 58 opeq2d ⊢W∈WordV∧1<W→W−2W=W−2W-2+2
60 59 oveq2d ⊢W∈WordV∧1<W→WsubstrW−2W=WsubstrW−2W-2+2
61 eqidd ⊢W∈WordV∧1<W→W⁡W−2=W⁡W−2
62 lsw ⊢W∈WordV→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∈WordV→W-2+1=W−1
70 69 eqcomd ⊢W∈WordV→W−1=W-2+1
71 70 fveq2d ⊢W∈WordV→W⁡W−1=W⁡W-2+1
72 62 71 eqtrd ⊢W∈WordV→lastS⁡W=W⁡W-2+1
73 72 adantr ⊢W∈WordV∧1<W→lastS⁡W=W⁡W-2+1
74 61 73 s2eqd ⊢W∈WordV∧1<W→⟨“W⁡W−2lastS⁡W”⟩=⟨“W⁡W−2W⁡W-2+1”⟩
75 53 60 74 3eqtr4d ⊢W∈WordV∧1<W→WsubstrW−2W=⟨“W⁡W−2lastS⁡W”⟩