Metamath Proof Explorer

Theorem chnerlem3

Description: Lemma for chner - trichotomy of integers within the word's domain. (Contributed by Ender Ting, 29-Jan-2026)

Ref Expression
Hypotheses chner.1 ⊢ φ → ∼ ˙ Er A
chner.2 ⊢ φ → C ∈ Chain A ∼ ˙
chner.3 ⊢ φ → J ∈ 0 ..^ C
chner.4 ⊢ φ → I ∈ 0 ..^ C
Assertion chnerlem3 ⊢ φ → I ∈ 0 ..^ J ∨ J ∈ 0 ..^ I ∨ I = J

Proof

Step Hyp Ref Expression
1 chner.1 ⊢ φ → ∼ ˙ Er A
2 chner.2 ⊢ φ → C ∈ Chain A ∼ ˙
3 chner.3 ⊢ φ → J ∈ 0 ..^ C
4 chner.4 ⊢ φ → I ∈ 0 ..^ C
5 elfzoelz ⊢ I ∈ 0 ..^ C → I ∈ ℤ
6 4 5 syl ⊢ φ → I ∈ ℤ
7 6 zred ⊢ φ → I ∈ ℝ
8 elfzoelz ⊢ J ∈ 0 ..^ C → J ∈ ℤ
9 3 8 syl ⊢ φ → J ∈ ℤ
10 9 zred ⊢ φ → J ∈ ℝ
11 lttri4 ⊢ I ∈ ℝ ∧ J ∈ ℝ → I < J ∨ I = J ∨ J < I
12 7 10 11 syl2anc ⊢ φ → I < J ∨ I = J ∨ J < I
13 3orcomb ⊢ I < J ∨ I = J ∨ J < I ↔ I < J ∨ J < I ∨ I = J
14 12 13 sylib ⊢ φ → I < J ∨ J < I ∨ I = J
15 elfzonn0 ⊢ I ∈ 0 ..^ C → I ∈ ℕ 0
16 4 15 syl ⊢ φ → I ∈ ℕ 0
17 16 adantr ⊢ φ ∧ I < J → I ∈ ℕ 0
18 9 adantr ⊢ φ ∧ I < J → J ∈ ℤ
19 simpr ⊢ φ ∧ I < J → I < J
20 17 18 19 3jca ⊢ φ ∧ I < J → I ∈ ℕ 0 ∧ J ∈ ℤ ∧ I < J
21 elfzo0z ⊢ I ∈ 0 ..^ J ↔ I ∈ ℕ 0 ∧ J ∈ ℤ ∧ I < J
22 20 21 sylibr ⊢ φ ∧ I < J → I ∈ 0 ..^ J
23 22 ex ⊢ φ → I < J → I ∈ 0 ..^ J
24 elfzonn0 ⊢ J ∈ 0 ..^ C → J ∈ ℕ 0
25 3 24 syl ⊢ φ → J ∈ ℕ 0
26 25 adantr ⊢ φ ∧ J < I → J ∈ ℕ 0
27 6 adantr ⊢ φ ∧ J < I → I ∈ ℤ
28 simpr ⊢ φ ∧ J < I → J < I
29 26 27 28 3jca ⊢ φ ∧ J < I → J ∈ ℕ 0 ∧ I ∈ ℤ ∧ J < I
30 elfzo0z ⊢ J ∈ 0 ..^ I ↔ J ∈ ℕ 0 ∧ I ∈ ℤ ∧ J < I
31 29 30 sylibr ⊢ φ ∧ J < I → J ∈ 0 ..^ I
32 31 ex ⊢ φ → J < I → J ∈ 0 ..^ I
33 idd ⊢ φ → I = J → I = J
34 23 32 33 3orim123d ⊢ φ → I < J ∨ J < I ∨ I = J → I ∈ 0 ..^ J ∨ J ∈ 0 ..^ I ∨ I = J
35 14 34 mpd ⊢ φ → I ∈ 0 ..^ J ∨ J ∈ 0 ..^ I ∨ I = J