Metamath Proof Explorer

Theorem chnlt

Description: Compare any two elements in a chain. (Contributed by Thierry Arnoux, 19-Jun-2025)

Ref Expression
Hypotheses chnlt.1 ⊢ φ → < ˙ Po A
chnlt.2 ⊢ φ → C ∈ Chain A < ˙
chnlt.3 ⊢ φ → J ∈ 0 ..^ C
chnlt.4 ⊢ φ → I ∈ 0 ..^ J
Assertion chnlt ⊢ φ → C ⁡ I < ˙ C ⁡ J

Proof

Step Hyp Ref Expression
1 chnlt.1 ⊢ φ → < ˙ Po A
2 chnlt.2 ⊢ φ → C ∈ Chain A < ˙
3 chnlt.3 ⊢ φ → J ∈ 0 ..^ C
4 chnlt.4 ⊢ φ → I ∈ 0 ..^ J
5 fzofzp1 ⊢ J ∈ 0 ..^ C → J + 1 ∈ 0 … C
6 3 5 syl ⊢ φ → J + 1 ∈ 0 … C
7 2 6 pfxchn ⊢ φ → C prefix J + 1 ∈ Chain A < ˙
8 fzossz ⊢ 0 ..^ C ⊆ ℤ
9 8 3 sselid ⊢ φ → J ∈ ℤ
10 9 zcnd ⊢ φ → J ∈ ℂ
11 1cnd ⊢ φ → 1 ∈ ℂ
12 2 chnwrd ⊢ φ → C ∈ Word A
13 pfxlen ⊢ C ∈ Word A ∧ J + 1 ∈ 0 … C → C prefix J + 1 = J + 1
14 12 6 13 syl2anc ⊢ φ → C prefix J + 1 = J + 1
15 10 11 14 mvrraddd ⊢ φ → C prefix J + 1 − 1 = J
16 15 oveq2d ⊢ φ → 0 ..^ C prefix J + 1 − 1 = 0 ..^ J
17 4 16 eleqtrrd ⊢ φ → I ∈ 0 ..^ C prefix J + 1 − 1
18 1 7 17 chnub ⊢ φ → C prefix J + 1 ⁡ I < ˙ lastS ⁡ C prefix J + 1
19 fzo0ssnn0 ⊢ 0 ..^ C ⊆ ℕ 0
20 19 3 sselid ⊢ φ → J ∈ ℕ 0
21 fzossfzop1 ⊢ J ∈ ℕ 0 → 0 ..^ J ⊆ 0 ..^ J + 1
22 20 21 syl ⊢ φ → 0 ..^ J ⊆ 0 ..^ J + 1
23 22 4 sseldd ⊢ φ → I ∈ 0 ..^ J + 1
24 pfxfv ⊢ C ∈ Word A ∧ J + 1 ∈ 0 … C ∧ I ∈ 0 ..^ J + 1 → C prefix J + 1 ⁡ I = C ⁡ I
25 12 6 23 24 syl3anc ⊢ φ → C prefix J + 1 ⁡ I = C ⁡ I
26 lencl ⊢ C ∈ Word A → C ∈ ℕ 0
27 12 26 syl ⊢ φ → C ∈ ℕ 0
28 fz0add1fz1 ⊢ C ∈ ℕ 0 ∧ J ∈ 0 ..^ C → J + 1 ∈ 1 … C
29 27 3 28 syl2anc ⊢ φ → J + 1 ∈ 1 … C
30 pfxfvlsw ⊢ C ∈ Word A ∧ J + 1 ∈ 1 … C → lastS ⁡ C prefix J + 1 = C ⁡ J + 1 - 1
31 12 29 30 syl2anc ⊢ φ → lastS ⁡ C prefix J + 1 = C ⁡ J + 1 - 1
32 10 11 pncand ⊢ φ → J + 1 - 1 = J
33 32 fveq2d ⊢ φ → C ⁡ J + 1 - 1 = C ⁡ J
34 31 33 eqtrd ⊢ φ → lastS ⁡ C prefix J + 1 = C ⁡ J
35 18 25 34 3brtr3d ⊢ φ → C ⁡ I < ˙ C ⁡ J