This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ 𝐹 = ( 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) ↦ if ( 𝑥 < ( ( ♯ ‘ 𝑃 ) − 2 ) , ( ◡ 𝐸 ‘ { ( 𝑃 ‘ 𝑥 ) , ( 𝑃 ‘ ( 𝑥 + 1 ) ) } ) , ( ◡ 𝐸 ‘ { ( 𝑃 ‘ 𝑥 ) , ( 𝑃 ‘ 0 ) } ) ) )
Assertion clwlkclwwlklem2a4 ( ( 𝐸 : dom 𝐸 –1-1→ 𝑅 ∧ 𝑃 ∈ Word 𝑉 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) → ( ( ( lastS ‘ 𝑃 ) = ( 𝑃 ‘ 0 ) ∧ 𝐼 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) ) → ( { ( 𝑃 ‘ 𝐼 ) , ( 𝑃 ‘ ( 𝐼 + 1 ) ) } ∈ ran 𝐸 → ( 𝐸 ‘ ( 𝐹 ‘ 𝐼 ) ) = { ( 𝑃 ‘ 𝐼 ) , ( 𝑃 ‘ ( 𝐼 + 1 ) ) } ) ) )

Proof

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