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 
|- ( ph -> .~ Er A )
chner.2 
|- ( ph -> C e. ( .~ Chain A ) )
chner.3 
|- ( ph -> J e. ( 0 ..^ ( # ` C ) ) )
chner.4 
|- ( ph -> I e. ( 0 ..^ ( # ` C ) ) )
Assertion chnerlem3 
|- ( ph -> ( I e. ( 0 ..^ J ) \/ J e. ( 0 ..^ I ) \/ I = J ) )

Proof

Step Hyp Ref Expression
1 chner.1 
 |-  ( ph -> .~ Er A )
2 chner.2 
 |-  ( ph -> C e. ( .~ Chain A ) )
3 chner.3 
 |-  ( ph -> J e. ( 0 ..^ ( # ` C ) ) )
4 chner.4 
 |-  ( ph -> I e. ( 0 ..^ ( # ` C ) ) )
5 elfzoelz 
 |-  ( I e. ( 0 ..^ ( # ` C ) ) -> I e. ZZ )
6 4 5 syl 
 |-  ( ph -> I e. ZZ )
7 6 zred 
 |-  ( ph -> I e. RR )
8 elfzoelz 
 |-  ( J e. ( 0 ..^ ( # ` C ) ) -> J e. ZZ )
9 3 8 syl 
 |-  ( ph -> J e. ZZ )
10 9 zred 
 |-  ( ph -> J e. RR )
11 lttri4 
 |-  ( ( I e. RR /\ J e. RR ) -> ( I < J \/ I = J \/ J < I ) )
12 7 10 11 syl2anc 
 |-  ( ph -> ( I < J \/ I = J \/ J < I ) )
13 3orcomb 
 |-  ( ( I < J \/ I = J \/ J < I ) <-> ( I < J \/ J < I \/ I = J ) )
14 12 13 sylib 
 |-  ( ph -> ( I < J \/ J < I \/ I = J ) )
15 elfzonn0 
 |-  ( I e. ( 0 ..^ ( # ` C ) ) -> I e. NN0 )
16 4 15 syl 
 |-  ( ph -> I e. NN0 )
17 16 adantr 
 |-  ( ( ph /\ I < J ) -> I e. NN0 )
18 9 adantr 
 |-  ( ( ph /\ I < J ) -> J e. ZZ )
19 simpr 
 |-  ( ( ph /\ I < J ) -> I < J )
20 17 18 19 3jca 
 |-  ( ( ph /\ I < J ) -> ( I e. NN0 /\ J e. ZZ /\ I < J ) )
21 elfzo0z 
 |-  ( I e. ( 0 ..^ J ) <-> ( I e. NN0 /\ J e. ZZ /\ I < J ) )
22 20 21 sylibr 
 |-  ( ( ph /\ I < J ) -> I e. ( 0 ..^ J ) )
23 22 ex 
 |-  ( ph -> ( I < J -> I e. ( 0 ..^ J ) ) )
24 elfzonn0 
 |-  ( J e. ( 0 ..^ ( # ` C ) ) -> J e. NN0 )
25 3 24 syl 
 |-  ( ph -> J e. NN0 )
26 25 adantr 
 |-  ( ( ph /\ J < I ) -> J e. NN0 )
27 6 adantr 
 |-  ( ( ph /\ J < I ) -> I e. ZZ )
28 simpr 
 |-  ( ( ph /\ J < I ) -> J < I )
29 26 27 28 3jca 
 |-  ( ( ph /\ J < I ) -> ( J e. NN0 /\ I e. ZZ /\ J < I ) )
30 elfzo0z 
 |-  ( J e. ( 0 ..^ I ) <-> ( J e. NN0 /\ I e. ZZ /\ J < I ) )
31 29 30 sylibr 
 |-  ( ( ph /\ J < I ) -> J e. ( 0 ..^ I ) )
32 31 ex 
 |-  ( ph -> ( J < I -> J e. ( 0 ..^ I ) ) )
33 idd 
 |-  ( ph -> ( I = J -> I = J ) )
34 23 32 33 3orim123d 
 |-  ( ph -> ( ( I < J \/ J < I \/ I = J ) -> ( I e. ( 0 ..^ J ) \/ J e. ( 0 ..^ I ) \/ I = J ) ) )
35 14 34 mpd 
 |-  ( ph -> ( I e. ( 0 ..^ J ) \/ J e. ( 0 ..^ I ) \/ I = J ) )