Metamath Proof Explorer

Theorem clwlkclwwlklem2a1

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

Ref Expression
Assertion clwlkclwwlklem2a1 ( ( 𝑃 ∈ Word 𝑉 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) → ( ( ( lastS ‘ 𝑃 ) = ( 𝑃 ‘ 0 ) ∧ ( ∀ 𝑖 ∈ ( 0 ..^ ( ( ( ( ♯ ‘ 𝑃 ) − 1 ) − 0 ) − 1 ) ) { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∈ ran 𝐸 ∧ { ( 𝑃 ‘ ( ( ♯ ‘ 𝑃 ) − 2 ) ) , ( 𝑃 ‘ 0 ) } ∈ ran 𝐸 ) ) → ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∈ ran 𝐸 ) )

Proof

Step Hyp Ref Expression
1 lencl ⊢ ( 𝑃 ∈ Word 𝑉 → ( ♯ ‘ 𝑃 ) ∈ ℕ0 )
2 nn0cn ⊢ ( ( ♯ ‘ 𝑃 ) ∈ ℕ0 → ( ♯ ‘ 𝑃 ) ∈ ℂ )
3 peano2cnm ⊢ ( ( ♯ ‘ 𝑃 ) ∈ ℂ → ( ( ♯ ‘ 𝑃 ) − 1 ) ∈ ℂ )
4 3 subid1d ⊢ ( ( ♯ ‘ 𝑃 ) ∈ ℂ → ( ( ( ♯ ‘ 𝑃 ) − 1 ) − 0 ) = ( ( ♯ ‘ 𝑃 ) − 1 ) )
5 4 oveq1d ⊢ ( ( ♯ ‘ 𝑃 ) ∈ ℂ → ( ( ( ( ♯ ‘ 𝑃 ) − 1 ) − 0 ) − 1 ) = ( ( ( ♯ ‘ 𝑃 ) − 1 ) − 1 ) )
6 sub1m1 ⊢ ( ( ♯ ‘ 𝑃 ) ∈ ℂ → ( ( ( ♯ ‘ 𝑃 ) − 1 ) − 1 ) = ( ( ♯ ‘ 𝑃 ) − 2 ) )
7 5 6 eqtrd ⊢ ( ( ♯ ‘ 𝑃 ) ∈ ℂ → ( ( ( ( ♯ ‘ 𝑃 ) − 1 ) − 0 ) − 1 ) = ( ( ♯ ‘ 𝑃 ) − 2 ) )
8 1 2 7 3syl ⊢ ( 𝑃 ∈ Word 𝑉 → ( ( ( ( ♯ ‘ 𝑃 ) − 1 ) − 0 ) − 1 ) = ( ( ♯ ‘ 𝑃 ) − 2 ) )
9 8 adantr ⊢ ( ( 𝑃 ∈ Word 𝑉 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) → ( ( ( ( ♯ ‘ 𝑃 ) − 1 ) − 0 ) − 1 ) = ( ( ♯ ‘ 𝑃 ) − 2 ) )
10 9 oveq2d ⊢ ( ( 𝑃 ∈ Word 𝑉 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) → ( 0 ..^ ( ( ( ( ♯ ‘ 𝑃 ) − 1 ) − 0 ) − 1 ) ) = ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 2 ) ) )
11 10 raleqdv ⊢ ( ( 𝑃 ∈ Word 𝑉 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) → ( ∀ 𝑖 ∈ ( 0 ..^ ( ( ( ( ♯ ‘ 𝑃 ) − 1 ) − 0 ) − 1 ) ) { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∈ ran 𝐸 ↔ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 2 ) ) { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∈ ran 𝐸 ) )
12 11 biimpcd ⊢ ( ∀ 𝑖 ∈ ( 0 ..^ ( ( ( ( ♯ ‘ 𝑃 ) − 1 ) − 0 ) − 1 ) ) { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∈ ran 𝐸 → ( ( 𝑃 ∈ Word 𝑉 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) → ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 2 ) ) { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∈ ran 𝐸 ) )
13 12 adantr ⊢ ( ( ∀ 𝑖 ∈ ( 0 ..^ ( ( ( ( ♯ ‘ 𝑃 ) − 1 ) − 0 ) − 1 ) ) { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∈ ran 𝐸 ∧ { ( 𝑃 ‘ ( ( ♯ ‘ 𝑃 ) − 2 ) ) , ( 𝑃 ‘ 0 ) } ∈ ran 𝐸 ) → ( ( 𝑃 ∈ Word 𝑉 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) → ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 2 ) ) { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∈ ran 𝐸 ) )
14 13 adantl ⊢ ( ( ( lastS ‘ 𝑃 ) = ( 𝑃 ‘ 0 ) ∧ ( ∀ 𝑖 ∈ ( 0 ..^ ( ( ( ( ♯ ‘ 𝑃 ) − 1 ) − 0 ) − 1 ) ) { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∈ ran 𝐸 ∧ { ( 𝑃 ‘ ( ( ♯ ‘ 𝑃 ) − 2 ) ) , ( 𝑃 ‘ 0 ) } ∈ ran 𝐸 ) ) → ( ( 𝑃 ∈ Word 𝑉 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) → ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 2 ) ) { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∈ ran 𝐸 ) )
15 14 impcom ⊢ ( ( ( 𝑃 ∈ Word 𝑉 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) ∧ ( ( lastS ‘ 𝑃 ) = ( 𝑃 ‘ 0 ) ∧ ( ∀ 𝑖 ∈ ( 0 ..^ ( ( ( ( ♯ ‘ 𝑃 ) − 1 ) − 0 ) − 1 ) ) { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∈ ran 𝐸 ∧ { ( 𝑃 ‘ ( ( ♯ ‘ 𝑃 ) − 2 ) ) , ( 𝑃 ‘ 0 ) } ∈ ran 𝐸 ) ) ) → ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 2 ) ) { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∈ ran 𝐸 )
16 lsw ⊢ ( 𝑃 ∈ Word 𝑉 → ( lastS ‘ 𝑃 ) = ( 𝑃 ‘ ( ( ♯ ‘ 𝑃 ) − 1 ) ) )
17 2m1e1 ⊢ ( 2 − 1 ) = 1
18 17 a1i ⊢ ( 𝑃 ∈ Word 𝑉 → ( 2 − 1 ) = 1 )
19 18 eqcomd ⊢ ( 𝑃 ∈ Word 𝑉 → 1 = ( 2 − 1 ) )
20 19 oveq2d ⊢ ( 𝑃 ∈ Word 𝑉 → ( ( ♯ ‘ 𝑃 ) − 1 ) = ( ( ♯ ‘ 𝑃 ) − ( 2 − 1 ) ) )
21 1 2 syl ⊢ ( 𝑃 ∈ Word 𝑉 → ( ♯ ‘ 𝑃 ) ∈ ℂ )
22 2cnd ⊢ ( 𝑃 ∈ Word 𝑉 → 2 ∈ ℂ )
23 1cnd ⊢ ( 𝑃 ∈ Word 𝑉 → 1 ∈ ℂ )
24 21 22 23 subsubd ⊢ ( 𝑃 ∈ Word 𝑉 → ( ( ♯ ‘ 𝑃 ) − ( 2 − 1 ) ) = ( ( ( ♯ ‘ 𝑃 ) − 2 ) + 1 ) )
25 20 24 eqtrd ⊢ ( 𝑃 ∈ Word 𝑉 → ( ( ♯ ‘ 𝑃 ) − 1 ) = ( ( ( ♯ ‘ 𝑃 ) − 2 ) + 1 ) )
26 25 fveq2d ⊢ ( 𝑃 ∈ Word 𝑉 → ( 𝑃 ‘ ( ( ♯ ‘ 𝑃 ) − 1 ) ) = ( 𝑃 ‘ ( ( ( ♯ ‘ 𝑃 ) − 2 ) + 1 ) ) )
27 16 26 eqtrd ⊢ ( 𝑃 ∈ Word 𝑉 → ( lastS ‘ 𝑃 ) = ( 𝑃 ‘ ( ( ( ♯ ‘ 𝑃 ) − 2 ) + 1 ) ) )
28 27 adantr ⊢ ( ( 𝑃 ∈ Word 𝑉 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) → ( lastS ‘ 𝑃 ) = ( 𝑃 ‘ ( ( ( ♯ ‘ 𝑃 ) − 2 ) + 1 ) ) )
29 28 adantr ⊢ ( ( ( 𝑃 ∈ Word 𝑉 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) ∧ ( lastS ‘ 𝑃 ) = ( 𝑃 ‘ 0 ) ) → ( lastS ‘ 𝑃 ) = ( 𝑃 ‘ ( ( ( ♯ ‘ 𝑃 ) − 2 ) + 1 ) ) )
30 eqeq1 ⊢ ( ( lastS ‘ 𝑃 ) = ( 𝑃 ‘ 0 ) → ( ( lastS ‘ 𝑃 ) = ( 𝑃 ‘ ( ( ( ♯ ‘ 𝑃 ) − 2 ) + 1 ) ) ↔ ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ ( ( ( ♯ ‘ 𝑃 ) − 2 ) + 1 ) ) ) )
31 30 adantl ⊢ ( ( ( 𝑃 ∈ Word 𝑉 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) ∧ ( lastS ‘ 𝑃 ) = ( 𝑃 ‘ 0 ) ) → ( ( lastS ‘ 𝑃 ) = ( 𝑃 ‘ ( ( ( ♯ ‘ 𝑃 ) − 2 ) + 1 ) ) ↔ ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ ( ( ( ♯ ‘ 𝑃 ) − 2 ) + 1 ) ) ) )
32 29 31 mpbid ⊢ ( ( ( 𝑃 ∈ Word 𝑉 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) ∧ ( lastS ‘ 𝑃 ) = ( 𝑃 ‘ 0 ) ) → ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ ( ( ( ♯ ‘ 𝑃 ) − 2 ) + 1 ) ) )
33 32 preq2d ⊢ ( ( ( 𝑃 ∈ Word 𝑉 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) ∧ ( lastS ‘ 𝑃 ) = ( 𝑃 ‘ 0 ) ) → { ( 𝑃 ‘ ( ( ♯ ‘ 𝑃 ) − 2 ) ) , ( 𝑃 ‘ 0 ) } = { ( 𝑃 ‘ ( ( ♯ ‘ 𝑃 ) − 2 ) ) , ( 𝑃 ‘ ( ( ( ♯ ‘ 𝑃 ) − 2 ) + 1 ) ) } )
34 33 eleq1d ⊢ ( ( ( 𝑃 ∈ Word 𝑉 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) ∧ ( lastS ‘ 𝑃 ) = ( 𝑃 ‘ 0 ) ) → ( { ( 𝑃 ‘ ( ( ♯ ‘ 𝑃 ) − 2 ) ) , ( 𝑃 ‘ 0 ) } ∈ ran 𝐸 ↔ { ( 𝑃 ‘ ( ( ♯ ‘ 𝑃 ) − 2 ) ) , ( 𝑃 ‘ ( ( ( ♯ ‘ 𝑃 ) − 2 ) + 1 ) ) } ∈ ran 𝐸 ) )
35 34 biimpd ⊢ ( ( ( 𝑃 ∈ Word 𝑉 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) ∧ ( lastS ‘ 𝑃 ) = ( 𝑃 ‘ 0 ) ) → ( { ( 𝑃 ‘ ( ( ♯ ‘ 𝑃 ) − 2 ) ) , ( 𝑃 ‘ 0 ) } ∈ ran 𝐸 → { ( 𝑃 ‘ ( ( ♯ ‘ 𝑃 ) − 2 ) ) , ( 𝑃 ‘ ( ( ( ♯ ‘ 𝑃 ) − 2 ) + 1 ) ) } ∈ ran 𝐸 ) )
36 35 ex ⊢ ( ( 𝑃 ∈ Word 𝑉 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) → ( ( lastS ‘ 𝑃 ) = ( 𝑃 ‘ 0 ) → ( { ( 𝑃 ‘ ( ( ♯ ‘ 𝑃 ) − 2 ) ) , ( 𝑃 ‘ 0 ) } ∈ ran 𝐸 → { ( 𝑃 ‘ ( ( ♯ ‘ 𝑃 ) − 2 ) ) , ( 𝑃 ‘ ( ( ( ♯ ‘ 𝑃 ) − 2 ) + 1 ) ) } ∈ ran 𝐸 ) ) )
37 36 com13 ⊢ ( { ( 𝑃 ‘ ( ( ♯ ‘ 𝑃 ) − 2 ) ) , ( 𝑃 ‘ 0 ) } ∈ ran 𝐸 → ( ( lastS ‘ 𝑃 ) = ( 𝑃 ‘ 0 ) → ( ( 𝑃 ∈ Word 𝑉 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) → { ( 𝑃 ‘ ( ( ♯ ‘ 𝑃 ) − 2 ) ) , ( 𝑃 ‘ ( ( ( ♯ ‘ 𝑃 ) − 2 ) + 1 ) ) } ∈ ran 𝐸 ) ) )
38 37 adantl ⊢ ( ( ∀ 𝑖 ∈ ( 0 ..^ ( ( ( ( ♯ ‘ 𝑃 ) − 1 ) − 0 ) − 1 ) ) { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∈ ran 𝐸 ∧ { ( 𝑃 ‘ ( ( ♯ ‘ 𝑃 ) − 2 ) ) , ( 𝑃 ‘ 0 ) } ∈ ran 𝐸 ) → ( ( lastS ‘ 𝑃 ) = ( 𝑃 ‘ 0 ) → ( ( 𝑃 ∈ Word 𝑉 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) → { ( 𝑃 ‘ ( ( ♯ ‘ 𝑃 ) − 2 ) ) , ( 𝑃 ‘ ( ( ( ♯ ‘ 𝑃 ) − 2 ) + 1 ) ) } ∈ ran 𝐸 ) ) )
39 38 impcom ⊢ ( ( ( lastS ‘ 𝑃 ) = ( 𝑃 ‘ 0 ) ∧ ( ∀ 𝑖 ∈ ( 0 ..^ ( ( ( ( ♯ ‘ 𝑃 ) − 1 ) − 0 ) − 1 ) ) { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∈ ran 𝐸 ∧ { ( 𝑃 ‘ ( ( ♯ ‘ 𝑃 ) − 2 ) ) , ( 𝑃 ‘ 0 ) } ∈ ran 𝐸 ) ) → ( ( 𝑃 ∈ Word 𝑉 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) → { ( 𝑃 ‘ ( ( ♯ ‘ 𝑃 ) − 2 ) ) , ( 𝑃 ‘ ( ( ( ♯ ‘ 𝑃 ) − 2 ) + 1 ) ) } ∈ ran 𝐸 ) )
40 39 impcom ⊢ ( ( ( 𝑃 ∈ Word 𝑉 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) ∧ ( ( lastS ‘ 𝑃 ) = ( 𝑃 ‘ 0 ) ∧ ( ∀ 𝑖 ∈ ( 0 ..^ ( ( ( ( ♯ ‘ 𝑃 ) − 1 ) − 0 ) − 1 ) ) { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∈ ran 𝐸 ∧ { ( 𝑃 ‘ ( ( ♯ ‘ 𝑃 ) − 2 ) ) , ( 𝑃 ‘ 0 ) } ∈ ran 𝐸 ) ) ) → { ( 𝑃 ‘ ( ( ♯ ‘ 𝑃 ) − 2 ) ) , ( 𝑃 ‘ ( ( ( ♯ ‘ 𝑃 ) − 2 ) + 1 ) ) } ∈ ran 𝐸 )
41 ovexd ⊢ ( ( ( 𝑃 ∈ Word 𝑉 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) ∧ ( ( lastS ‘ 𝑃 ) = ( 𝑃 ‘ 0 ) ∧ ( ∀ 𝑖 ∈ ( 0 ..^ ( ( ( ( ♯ ‘ 𝑃 ) − 1 ) − 0 ) − 1 ) ) { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∈ ran 𝐸 ∧ { ( 𝑃 ‘ ( ( ♯ ‘ 𝑃 ) − 2 ) ) , ( 𝑃 ‘ 0 ) } ∈ ran 𝐸 ) ) ) → ( ( ♯ ‘ 𝑃 ) − 2 ) ∈ V )
42 fveq2 ⊢ ( 𝑖 = ( ( ♯ ‘ 𝑃 ) − 2 ) → ( 𝑃 ‘ 𝑖 ) = ( 𝑃 ‘ ( ( ♯ ‘ 𝑃 ) − 2 ) ) )
43 fvoveq1 ⊢ ( 𝑖 = ( ( ♯ ‘ 𝑃 ) − 2 ) → ( 𝑃 ‘ ( 𝑖 + 1 ) ) = ( 𝑃 ‘ ( ( ( ♯ ‘ 𝑃 ) − 2 ) + 1 ) ) )
44 42 43 preq12d ⊢ ( 𝑖 = ( ( ♯ ‘ 𝑃 ) − 2 ) → { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } = { ( 𝑃 ‘ ( ( ♯ ‘ 𝑃 ) − 2 ) ) , ( 𝑃 ‘ ( ( ( ♯ ‘ 𝑃 ) − 2 ) + 1 ) ) } )
45 44 eleq1d ⊢ ( 𝑖 = ( ( ♯ ‘ 𝑃 ) − 2 ) → ( { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∈ ran 𝐸 ↔ { ( 𝑃 ‘ ( ( ♯ ‘ 𝑃 ) − 2 ) ) , ( 𝑃 ‘ ( ( ( ♯ ‘ 𝑃 ) − 2 ) + 1 ) ) } ∈ ran 𝐸 ) )
46 45 ralunsn ⊢ ( ( ( ♯ ‘ 𝑃 ) − 2 ) ∈ V → ( ∀ 𝑖 ∈ ( ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 2 ) ) ∪ { ( ( ♯ ‘ 𝑃 ) − 2 ) } ) { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∈ ran 𝐸 ↔ ( ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 2 ) ) { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∈ ran 𝐸 ∧ { ( 𝑃 ‘ ( ( ♯ ‘ 𝑃 ) − 2 ) ) , ( 𝑃 ‘ ( ( ( ♯ ‘ 𝑃 ) − 2 ) + 1 ) ) } ∈ ran 𝐸 ) ) )
47 41 46 syl ⊢ ( ( ( 𝑃 ∈ Word 𝑉 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) ∧ ( ( lastS ‘ 𝑃 ) = ( 𝑃 ‘ 0 ) ∧ ( ∀ 𝑖 ∈ ( 0 ..^ ( ( ( ( ♯ ‘ 𝑃 ) − 1 ) − 0 ) − 1 ) ) { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∈ ran 𝐸 ∧ { ( 𝑃 ‘ ( ( ♯ ‘ 𝑃 ) − 2 ) ) , ( 𝑃 ‘ 0 ) } ∈ ran 𝐸 ) ) ) → ( ∀ 𝑖 ∈ ( ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 2 ) ) ∪ { ( ( ♯ ‘ 𝑃 ) − 2 ) } ) { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∈ ran 𝐸 ↔ ( ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 2 ) ) { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∈ ran 𝐸 ∧ { ( 𝑃 ‘ ( ( ♯ ‘ 𝑃 ) − 2 ) ) , ( 𝑃 ‘ ( ( ( ♯ ‘ 𝑃 ) − 2 ) + 1 ) ) } ∈ ran 𝐸 ) ) )
48 15 40 47 mpbir2and ⊢ ( ( ( 𝑃 ∈ Word 𝑉 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) ∧ ( ( lastS ‘ 𝑃 ) = ( 𝑃 ‘ 0 ) ∧ ( ∀ 𝑖 ∈ ( 0 ..^ ( ( ( ( ♯ ‘ 𝑃 ) − 1 ) − 0 ) − 1 ) ) { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∈ ran 𝐸 ∧ { ( 𝑃 ‘ ( ( ♯ ‘ 𝑃 ) − 2 ) ) , ( 𝑃 ‘ 0 ) } ∈ ran 𝐸 ) ) ) → ∀ 𝑖 ∈ ( ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 2 ) ) ∪ { ( ( ♯ ‘ 𝑃 ) − 2 ) } ) { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∈ ran 𝐸 )
49 1e2m1 ⊢ 1 = ( 2 − 1 )
50 49 a1i ⊢ ( 𝑃 ∈ Word 𝑉 → 1 = ( 2 − 1 ) )
51 50 oveq2d ⊢ ( 𝑃 ∈ Word 𝑉 → ( ( ♯ ‘ 𝑃 ) − 1 ) = ( ( ♯ ‘ 𝑃 ) − ( 2 − 1 ) ) )
52 51 24 eqtrd ⊢ ( 𝑃 ∈ Word 𝑉 → ( ( ♯ ‘ 𝑃 ) − 1 ) = ( ( ( ♯ ‘ 𝑃 ) − 2 ) + 1 ) )
53 52 oveq2d ⊢ ( 𝑃 ∈ Word 𝑉 → ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) = ( 0 ..^ ( ( ( ♯ ‘ 𝑃 ) − 2 ) + 1 ) ) )
54 53 adantr ⊢ ( ( 𝑃 ∈ Word 𝑉 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) → ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) = ( 0 ..^ ( ( ( ♯ ‘ 𝑃 ) − 2 ) + 1 ) ) )
55 nn0re ⊢ ( ( ♯ ‘ 𝑃 ) ∈ ℕ0 → ( ♯ ‘ 𝑃 ) ∈ ℝ )
56 2re ⊢ 2 ∈ ℝ
57 56 a1i ⊢ ( ( ♯ ‘ 𝑃 ) ∈ ℕ0 → 2 ∈ ℝ )
58 55 57 subge0d ⊢ ( ( ♯ ‘ 𝑃 ) ∈ ℕ0 → ( 0 ≤ ( ( ♯ ‘ 𝑃 ) − 2 ) ↔ 2 ≤ ( ♯ ‘ 𝑃 ) ) )
59 58 biimprd ⊢ ( ( ♯ ‘ 𝑃 ) ∈ ℕ0 → ( 2 ≤ ( ♯ ‘ 𝑃 ) → 0 ≤ ( ( ♯ ‘ 𝑃 ) − 2 ) ) )
60 nn0z ⊢ ( ( ♯ ‘ 𝑃 ) ∈ ℕ0 → ( ♯ ‘ 𝑃 ) ∈ ℤ )
61 2z ⊢ 2 ∈ ℤ
62 61 a1i ⊢ ( ( ♯ ‘ 𝑃 ) ∈ ℕ0 → 2 ∈ ℤ )
63 60 62 zsubcld ⊢ ( ( ♯ ‘ 𝑃 ) ∈ ℕ0 → ( ( ♯ ‘ 𝑃 ) − 2 ) ∈ ℤ )
64 59 63 jctild ⊢ ( ( ♯ ‘ 𝑃 ) ∈ ℕ0 → ( 2 ≤ ( ♯ ‘ 𝑃 ) → ( ( ( ♯ ‘ 𝑃 ) − 2 ) ∈ ℤ ∧ 0 ≤ ( ( ♯ ‘ 𝑃 ) − 2 ) ) ) )
65 1 64 syl ⊢ ( 𝑃 ∈ Word 𝑉 → ( 2 ≤ ( ♯ ‘ 𝑃 ) → ( ( ( ♯ ‘ 𝑃 ) − 2 ) ∈ ℤ ∧ 0 ≤ ( ( ♯ ‘ 𝑃 ) − 2 ) ) ) )
66 65 imp ⊢ ( ( 𝑃 ∈ Word 𝑉 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) → ( ( ( ♯ ‘ 𝑃 ) − 2 ) ∈ ℤ ∧ 0 ≤ ( ( ♯ ‘ 𝑃 ) − 2 ) ) )
67 elnn0z ⊢ ( ( ( ♯ ‘ 𝑃 ) − 2 ) ∈ ℕ0 ↔ ( ( ( ♯ ‘ 𝑃 ) − 2 ) ∈ ℤ ∧ 0 ≤ ( ( ♯ ‘ 𝑃 ) − 2 ) ) )
68 66 67 sylibr ⊢ ( ( 𝑃 ∈ Word 𝑉 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) → ( ( ♯ ‘ 𝑃 ) − 2 ) ∈ ℕ0 )
69 elnn0uz ⊢ ( ( ( ♯ ‘ 𝑃 ) − 2 ) ∈ ℕ0 ↔ ( ( ♯ ‘ 𝑃 ) − 2 ) ∈ ( ℤ≥ ‘ 0 ) )
70 68 69 sylib ⊢ ( ( 𝑃 ∈ Word 𝑉 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) → ( ( ♯ ‘ 𝑃 ) − 2 ) ∈ ( ℤ≥ ‘ 0 ) )
71 fzosplitsn ⊢ ( ( ( ♯ ‘ 𝑃 ) − 2 ) ∈ ( ℤ≥ ‘ 0 ) → ( 0 ..^ ( ( ( ♯ ‘ 𝑃 ) − 2 ) + 1 ) ) = ( ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 2 ) ) ∪ { ( ( ♯ ‘ 𝑃 ) − 2 ) } ) )
72 70 71 syl ⊢ ( ( 𝑃 ∈ Word 𝑉 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) → ( 0 ..^ ( ( ( ♯ ‘ 𝑃 ) − 2 ) + 1 ) ) = ( ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 2 ) ) ∪ { ( ( ♯ ‘ 𝑃 ) − 2 ) } ) )
73 54 72 eqtrd ⊢ ( ( 𝑃 ∈ Word 𝑉 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) → ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) = ( ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 2 ) ) ∪ { ( ( ♯ ‘ 𝑃 ) − 2 ) } ) )
74 73 adantr ⊢ ( ( ( 𝑃 ∈ Word 𝑉 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) ∧ ( ( lastS ‘ 𝑃 ) = ( 𝑃 ‘ 0 ) ∧ ( ∀ 𝑖 ∈ ( 0 ..^ ( ( ( ( ♯ ‘ 𝑃 ) − 1 ) − 0 ) − 1 ) ) { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∈ ran 𝐸 ∧ { ( 𝑃 ‘ ( ( ♯ ‘ 𝑃 ) − 2 ) ) , ( 𝑃 ‘ 0 ) } ∈ ran 𝐸 ) ) ) → ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) = ( ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 2 ) ) ∪ { ( ( ♯ ‘ 𝑃 ) − 2 ) } ) )
75 74 raleqdv ⊢ ( ( ( 𝑃 ∈ Word 𝑉 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) ∧ ( ( lastS ‘ 𝑃 ) = ( 𝑃 ‘ 0 ) ∧ ( ∀ 𝑖 ∈ ( 0 ..^ ( ( ( ( ♯ ‘ 𝑃 ) − 1 ) − 0 ) − 1 ) ) { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∈ ran 𝐸 ∧ { ( 𝑃 ‘ ( ( ♯ ‘ 𝑃 ) − 2 ) ) , ( 𝑃 ‘ 0 ) } ∈ ran 𝐸 ) ) ) → ( ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∈ ran 𝐸 ↔ ∀ 𝑖 ∈ ( ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 2 ) ) ∪ { ( ( ♯ ‘ 𝑃 ) − 2 ) } ) { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∈ ran 𝐸 ) )
76 48 75 mpbird ⊢ ( ( ( 𝑃 ∈ Word 𝑉 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) ∧ ( ( lastS ‘ 𝑃 ) = ( 𝑃 ‘ 0 ) ∧ ( ∀ 𝑖 ∈ ( 0 ..^ ( ( ( ( ♯ ‘ 𝑃 ) − 1 ) − 0 ) − 1 ) ) { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∈ ran 𝐸 ∧ { ( 𝑃 ‘ ( ( ♯ ‘ 𝑃 ) − 2 ) ) , ( 𝑃 ‘ 0 ) } ∈ ran 𝐸 ) ) ) → ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∈ ran 𝐸 )
77 76 ex ⊢ ( ( 𝑃 ∈ Word 𝑉 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) → ( ( ( lastS ‘ 𝑃 ) = ( 𝑃 ‘ 0 ) ∧ ( ∀ 𝑖 ∈ ( 0 ..^ ( ( ( ( ♯ ‘ 𝑃 ) − 1 ) − 0 ) − 1 ) ) { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∈ ran 𝐸 ∧ { ( 𝑃 ‘ ( ( ♯ ‘ 𝑃 ) − 2 ) ) , ( 𝑃 ‘ 0 ) } ∈ ran 𝐸 ) ) → ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∈ ran 𝐸 ) )