Metamath Proof Explorer

Theorem elfznelfzo

Description: A value in a finite set of sequential integers is a border value if it is not contained in the half-open integer range contained in the finite set of sequential integers. (Contributed by Alexander van der Vekens, 31-Oct-2017) (Revised by Thierry Arnoux, 22-Dec-2021)

Ref Expression
Assertion elfznelfzo 
|- ( ( M e. ( 0 ... K ) /\ -. M e. ( 1 ..^ K ) ) -> ( M = 0 \/ M = K ) )

Proof

Step Hyp Ref Expression
1 elfz2nn0 
 |-  ( M e. ( 0 ... K ) <-> ( M e. NN0 /\ K e. NN0 /\ M <_ K ) )
2 nn0z 
 |-  ( M e. NN0 -> M e. ZZ )
3 nn0z 
 |-  ( K e. NN0 -> K e. ZZ )
4 2 3 anim12i 
 |-  ( ( M e. NN0 /\ K e. NN0 ) -> ( M e. ZZ /\ K e. ZZ ) )
5 4 3adant3 
 |-  ( ( M e. NN0 /\ K e. NN0 /\ M <_ K ) -> ( M e. ZZ /\ K e. ZZ ) )
6 elfzom1b 
 |-  ( ( M e. ZZ /\ K e. ZZ ) -> ( M e. ( 1 ..^ K ) <-> ( M - 1 ) e. ( 0 ..^ ( K - 1 ) ) ) )
7 5 6 syl 
 |-  ( ( M e. NN0 /\ K e. NN0 /\ M <_ K ) -> ( M e. ( 1 ..^ K ) <-> ( M - 1 ) e. ( 0 ..^ ( K - 1 ) ) ) )
8 7 notbid 
 |-  ( ( M e. NN0 /\ K e. NN0 /\ M <_ K ) -> ( -. M e. ( 1 ..^ K ) <-> -. ( M - 1 ) e. ( 0 ..^ ( K - 1 ) ) ) )
9 elfzo0 
 |-  ( ( M - 1 ) e. ( 0 ..^ ( K - 1 ) ) <-> ( ( M - 1 ) e. NN0 /\ ( K - 1 ) e. NN /\ ( M - 1 ) < ( K - 1 ) ) )
10 9 a1i 
 |-  ( ( M e. NN0 /\ K e. NN0 /\ M <_ K ) -> ( ( M - 1 ) e. ( 0 ..^ ( K - 1 ) ) <-> ( ( M - 1 ) e. NN0 /\ ( K - 1 ) e. NN /\ ( M - 1 ) < ( K - 1 ) ) ) )
11 10 notbid 
 |-  ( ( M e. NN0 /\ K e. NN0 /\ M <_ K ) -> ( -. ( M - 1 ) e. ( 0 ..^ ( K - 1 ) ) <-> -. ( ( M - 1 ) e. NN0 /\ ( K - 1 ) e. NN /\ ( M - 1 ) < ( K - 1 ) ) ) )
12 3ianor 
 |-  ( -. ( ( M - 1 ) e. NN0 /\ ( K - 1 ) e. NN /\ ( M - 1 ) < ( K - 1 ) ) <-> ( -. ( M - 1 ) e. NN0 \/ -. ( K - 1 ) e. NN \/ -. ( M - 1 ) < ( K - 1 ) ) )
13 elnnne0 
 |-  ( M e. NN <-> ( M e. NN0 /\ M =/= 0 ) )
14 df-ne 
 |-  ( M =/= 0 <-> -. M = 0 )
15 14 anbi2i 
 |-  ( ( M e. NN0 /\ M =/= 0 ) <-> ( M e. NN0 /\ -. M = 0 ) )
16 13 15 bitr2i 
 |-  ( ( M e. NN0 /\ -. M = 0 ) <-> M e. NN )
17 nnm1nn0 
 |-  ( M e. NN -> ( M - 1 ) e. NN0 )
18 16 17 sylbi 
 |-  ( ( M e. NN0 /\ -. M = 0 ) -> ( M - 1 ) e. NN0 )
19 18 ex 
 |-  ( M e. NN0 -> ( -. M = 0 -> ( M - 1 ) e. NN0 ) )
20 19 con1d 
 |-  ( M e. NN0 -> ( -. ( M - 1 ) e. NN0 -> M = 0 ) )
21 20 imp 
 |-  ( ( M e. NN0 /\ -. ( M - 1 ) e. NN0 ) -> M = 0 )
22 21 orcd 
 |-  ( ( M e. NN0 /\ -. ( M - 1 ) e. NN0 ) -> ( M = 0 \/ M = K ) )
23 22 ex 
 |-  ( M e. NN0 -> ( -. ( M - 1 ) e. NN0 -> ( M = 0 \/ M = K ) ) )
24 23 3ad2ant1 
 |-  ( ( M e. NN0 /\ K e. NN0 /\ M <_ K ) -> ( -. ( M - 1 ) e. NN0 -> ( M = 0 \/ M = K ) ) )
25 24 com12 
 |-  ( -. ( M - 1 ) e. NN0 -> ( ( M e. NN0 /\ K e. NN0 /\ M <_ K ) -> ( M = 0 \/ M = K ) ) )
26 ioran 
 |-  ( -. ( M = 0 \/ M = K ) <-> ( -. M = 0 /\ -. M = K ) )
27 nn1m1nn 
 |-  ( M e. NN -> ( M = 1 \/ ( M - 1 ) e. NN ) )
28 df-ne 
 |-  ( M =/= K <-> -. M = K )
29 necom 
 |-  ( M =/= K <-> K =/= M )
30 nn0re 
 |-  ( M e. NN0 -> M e. RR )
31 30 ad2antlr 
 |-  ( ( ( K e. NN0 /\ M e. NN0 ) /\ M <_ K ) -> M e. RR )
32 nn0re 
 |-  ( K e. NN0 -> K e. RR )
33 32 adantr 
 |-  ( ( K e. NN0 /\ M e. NN0 ) -> K e. RR )
34 33 adantr 
 |-  ( ( ( K e. NN0 /\ M e. NN0 ) /\ M <_ K ) -> K e. RR )
35 simpr 
 |-  ( ( ( K e. NN0 /\ M e. NN0 ) /\ M <_ K ) -> M <_ K )
36 31 34 35 leltned 
 |-  ( ( ( K e. NN0 /\ M e. NN0 ) /\ M <_ K ) -> ( M < K <-> K =/= M ) )
37 29 36 bitr4id 
 |-  ( ( ( K e. NN0 /\ M e. NN0 ) /\ M <_ K ) -> ( M =/= K <-> M < K ) )
38 37 adantr 
 |-  ( ( ( ( K e. NN0 /\ M e. NN0 ) /\ M <_ K ) /\ M = 1 ) -> ( M =/= K <-> M < K ) )
39 breq1 
 |-  ( M = 1 -> ( M < K <-> 1 < K ) )
40 39 biimpa 
 |-  ( ( M = 1 /\ M < K ) -> 1 < K )
41 1red 
 |-  ( ( K e. NN0 /\ M e. NN0 ) -> 1 e. RR )
42 41 33 41 ltsub1d 
 |-  ( ( K e. NN0 /\ M e. NN0 ) -> ( 1 < K <-> ( 1 - 1 ) < ( K - 1 ) ) )
43 1m1e0 
 |-  ( 1 - 1 ) = 0
44 43 breq1i 
 |-  ( ( 1 - 1 ) < ( K - 1 ) <-> 0 < ( K - 1 ) )
45 1zzd 
 |-  ( K e. NN0 -> 1 e. ZZ )
46 3 45 zsubcld 
 |-  ( K e. NN0 -> ( K - 1 ) e. ZZ )
47 46 adantr 
 |-  ( ( K e. NN0 /\ M e. NN0 ) -> ( K - 1 ) e. ZZ )
48 47 adantr 
 |-  ( ( ( K e. NN0 /\ M e. NN0 ) /\ 0 < ( K - 1 ) ) -> ( K - 1 ) e. ZZ )
49 simpr 
 |-  ( ( ( K e. NN0 /\ M e. NN0 ) /\ 0 < ( K - 1 ) ) -> 0 < ( K - 1 ) )
50 elnnz 
 |-  ( ( K - 1 ) e. NN <-> ( ( K - 1 ) e. ZZ /\ 0 < ( K - 1 ) ) )
51 48 49 50 sylanbrc 
 |-  ( ( ( K e. NN0 /\ M e. NN0 ) /\ 0 < ( K - 1 ) ) -> ( K - 1 ) e. NN )
52 51 ex 
 |-  ( ( K e. NN0 /\ M e. NN0 ) -> ( 0 < ( K - 1 ) -> ( K - 1 ) e. NN ) )
53 44 52 syl5bi 
 |-  ( ( K e. NN0 /\ M e. NN0 ) -> ( ( 1 - 1 ) < ( K - 1 ) -> ( K - 1 ) e. NN ) )
54 42 53 sylbid 
 |-  ( ( K e. NN0 /\ M e. NN0 ) -> ( 1 < K -> ( K - 1 ) e. NN ) )
55 40 54 syl5 
 |-  ( ( K e. NN0 /\ M e. NN0 ) -> ( ( M = 1 /\ M < K ) -> ( K - 1 ) e. NN ) )
56 55 expd 
 |-  ( ( K e. NN0 /\ M e. NN0 ) -> ( M = 1 -> ( M < K -> ( K - 1 ) e. NN ) ) )
57 56 adantr 
 |-  ( ( ( K e. NN0 /\ M e. NN0 ) /\ M <_ K ) -> ( M = 1 -> ( M < K -> ( K - 1 ) e. NN ) ) )
58 57 imp 
 |-  ( ( ( ( K e. NN0 /\ M e. NN0 ) /\ M <_ K ) /\ M = 1 ) -> ( M < K -> ( K - 1 ) e. NN ) )
59 38 58 sylbid 
 |-  ( ( ( ( K e. NN0 /\ M e. NN0 ) /\ M <_ K ) /\ M = 1 ) -> ( M =/= K -> ( K - 1 ) e. NN ) )
60 59 exp31 
 |-  ( ( K e. NN0 /\ M e. NN0 ) -> ( M <_ K -> ( M = 1 -> ( M =/= K -> ( K - 1 ) e. NN ) ) ) )
61 60 com14 
 |-  ( M =/= K -> ( M <_ K -> ( M = 1 -> ( ( K e. NN0 /\ M e. NN0 ) -> ( K - 1 ) e. NN ) ) ) )
62 28 61 sylbir 
 |-  ( -. M = K -> ( M <_ K -> ( M = 1 -> ( ( K e. NN0 /\ M e. NN0 ) -> ( K - 1 ) e. NN ) ) ) )
63 62 com23 
 |-  ( -. M = K -> ( M = 1 -> ( M <_ K -> ( ( K e. NN0 /\ M e. NN0 ) -> ( K - 1 ) e. NN ) ) ) )
64 63 com14 
 |-  ( ( K e. NN0 /\ M e. NN0 ) -> ( M = 1 -> ( M <_ K -> ( -. M = K -> ( K - 1 ) e. NN ) ) ) )
65 64 ex 
 |-  ( K e. NN0 -> ( M e. NN0 -> ( M = 1 -> ( M <_ K -> ( -. M = K -> ( K - 1 ) e. NN ) ) ) ) )
66 65 com14 
 |-  ( M <_ K -> ( M e. NN0 -> ( M = 1 -> ( K e. NN0 -> ( -. M = K -> ( K - 1 ) e. NN ) ) ) ) )
67 66 com13 
 |-  ( M = 1 -> ( M e. NN0 -> ( M <_ K -> ( K e. NN0 -> ( -. M = K -> ( K - 1 ) e. NN ) ) ) ) )
68 30 ad2antlr 
 |-  ( ( ( ( M - 1 ) e. NN /\ M e. NN0 ) /\ K e. NN0 ) -> M e. RR )
69 32 adantl 
 |-  ( ( ( ( M - 1 ) e. NN /\ M e. NN0 ) /\ K e. NN0 ) -> K e. RR )
70 1red 
 |-  ( ( ( ( M - 1 ) e. NN /\ M e. NN0 ) /\ K e. NN0 ) -> 1 e. RR )
71 68 69 70 lesub1d 
 |-  ( ( ( ( M - 1 ) e. NN /\ M e. NN0 ) /\ K e. NN0 ) -> ( M <_ K <-> ( M - 1 ) <_ ( K - 1 ) ) )
72 3 ad2antlr 
 |-  ( ( ( ( ( M - 1 ) e. NN /\ M e. NN0 ) /\ K e. NN0 ) /\ ( M - 1 ) <_ ( K - 1 ) ) -> K e. ZZ )
73 1zzd 
 |-  ( ( ( ( ( M - 1 ) e. NN /\ M e. NN0 ) /\ K e. NN0 ) /\ ( M - 1 ) <_ ( K - 1 ) ) -> 1 e. ZZ )
74 72 73 zsubcld 
 |-  ( ( ( ( ( M - 1 ) e. NN /\ M e. NN0 ) /\ K e. NN0 ) /\ ( M - 1 ) <_ ( K - 1 ) ) -> ( K - 1 ) e. ZZ )
75 nngt0 
 |-  ( ( M - 1 ) e. NN -> 0 < ( M - 1 ) )
76 0red 
 |-  ( ( M e. NN0 /\ K e. NN0 ) -> 0 e. RR )
77 peano2rem 
 |-  ( M e. RR -> ( M - 1 ) e. RR )
78 30 77 syl 
 |-  ( M e. NN0 -> ( M - 1 ) e. RR )
79 78 adantr 
 |-  ( ( M e. NN0 /\ K e. NN0 ) -> ( M - 1 ) e. RR )
80 peano2rem 
 |-  ( K e. RR -> ( K - 1 ) e. RR )
81 32 80 syl 
 |-  ( K e. NN0 -> ( K - 1 ) e. RR )
82 81 adantl 
 |-  ( ( M e. NN0 /\ K e. NN0 ) -> ( K - 1 ) e. RR )
83 ltletr 
 |-  ( ( 0 e. RR /\ ( M - 1 ) e. RR /\ ( K - 1 ) e. RR ) -> ( ( 0 < ( M - 1 ) /\ ( M - 1 ) <_ ( K - 1 ) ) -> 0 < ( K - 1 ) ) )
84 76 79 82 83 syl3anc 
 |-  ( ( M e. NN0 /\ K e. NN0 ) -> ( ( 0 < ( M - 1 ) /\ ( M - 1 ) <_ ( K - 1 ) ) -> 0 < ( K - 1 ) ) )
85 84 ex 
 |-  ( M e. NN0 -> ( K e. NN0 -> ( ( 0 < ( M - 1 ) /\ ( M - 1 ) <_ ( K - 1 ) ) -> 0 < ( K - 1 ) ) ) )
86 85 com13 
 |-  ( ( 0 < ( M - 1 ) /\ ( M - 1 ) <_ ( K - 1 ) ) -> ( K e. NN0 -> ( M e. NN0 -> 0 < ( K - 1 ) ) ) )
87 86 ex 
 |-  ( 0 < ( M - 1 ) -> ( ( M - 1 ) <_ ( K - 1 ) -> ( K e. NN0 -> ( M e. NN0 -> 0 < ( K - 1 ) ) ) ) )
88 87 com24 
 |-  ( 0 < ( M - 1 ) -> ( M e. NN0 -> ( K e. NN0 -> ( ( M - 1 ) <_ ( K - 1 ) -> 0 < ( K - 1 ) ) ) ) )
89 75 88 syl 
 |-  ( ( M - 1 ) e. NN -> ( M e. NN0 -> ( K e. NN0 -> ( ( M - 1 ) <_ ( K - 1 ) -> 0 < ( K - 1 ) ) ) ) )
90 89 imp41 
 |-  ( ( ( ( ( M - 1 ) e. NN /\ M e. NN0 ) /\ K e. NN0 ) /\ ( M - 1 ) <_ ( K - 1 ) ) -> 0 < ( K - 1 ) )
91 74 90 50 sylanbrc 
 |-  ( ( ( ( ( M - 1 ) e. NN /\ M e. NN0 ) /\ K e. NN0 ) /\ ( M - 1 ) <_ ( K - 1 ) ) -> ( K - 1 ) e. NN )
92 91 a1d 
 |-  ( ( ( ( ( M - 1 ) e. NN /\ M e. NN0 ) /\ K e. NN0 ) /\ ( M - 1 ) <_ ( K - 1 ) ) -> ( -. M = K -> ( K - 1 ) e. NN ) )
93 92 ex 
 |-  ( ( ( ( M - 1 ) e. NN /\ M e. NN0 ) /\ K e. NN0 ) -> ( ( M - 1 ) <_ ( K - 1 ) -> ( -. M = K -> ( K - 1 ) e. NN ) ) )
94 71 93 sylbid 
 |-  ( ( ( ( M - 1 ) e. NN /\ M e. NN0 ) /\ K e. NN0 ) -> ( M <_ K -> ( -. M = K -> ( K - 1 ) e. NN ) ) )
95 94 ex 
 |-  ( ( ( M - 1 ) e. NN /\ M e. NN0 ) -> ( K e. NN0 -> ( M <_ K -> ( -. M = K -> ( K - 1 ) e. NN ) ) ) )
96 95 com23 
 |-  ( ( ( M - 1 ) e. NN /\ M e. NN0 ) -> ( M <_ K -> ( K e. NN0 -> ( -. M = K -> ( K - 1 ) e. NN ) ) ) )
97 96 ex 
 |-  ( ( M - 1 ) e. NN -> ( M e. NN0 -> ( M <_ K -> ( K e. NN0 -> ( -. M = K -> ( K - 1 ) e. NN ) ) ) ) )
98 67 97 jaoi 
 |-  ( ( M = 1 \/ ( M - 1 ) e. NN ) -> ( M e. NN0 -> ( M <_ K -> ( K e. NN0 -> ( -. M = K -> ( K - 1 ) e. NN ) ) ) ) )
99 27 98 syl 
 |-  ( M e. NN -> ( M e. NN0 -> ( M <_ K -> ( K e. NN0 -> ( -. M = K -> ( K - 1 ) e. NN ) ) ) ) )
100 13 99 sylbir 
 |-  ( ( M e. NN0 /\ M =/= 0 ) -> ( M e. NN0 -> ( M <_ K -> ( K e. NN0 -> ( -. M = K -> ( K - 1 ) e. NN ) ) ) ) )
101 100 ex 
 |-  ( M e. NN0 -> ( M =/= 0 -> ( M e. NN0 -> ( M <_ K -> ( K e. NN0 -> ( -. M = K -> ( K - 1 ) e. NN ) ) ) ) ) )
102 101 pm2.43a 
 |-  ( M e. NN0 -> ( M =/= 0 -> ( M <_ K -> ( K e. NN0 -> ( -. M = K -> ( K - 1 ) e. NN ) ) ) ) )
103 102 com24 
 |-  ( M e. NN0 -> ( K e. NN0 -> ( M <_ K -> ( M =/= 0 -> ( -. M = K -> ( K - 1 ) e. NN ) ) ) ) )
104 103 3imp 
 |-  ( ( M e. NN0 /\ K e. NN0 /\ M <_ K ) -> ( M =/= 0 -> ( -. M = K -> ( K - 1 ) e. NN ) ) )
105 104 com3l 
 |-  ( M =/= 0 -> ( -. M = K -> ( ( M e. NN0 /\ K e. NN0 /\ M <_ K ) -> ( K - 1 ) e. NN ) ) )
106 14 105 sylbir 
 |-  ( -. M = 0 -> ( -. M = K -> ( ( M e. NN0 /\ K e. NN0 /\ M <_ K ) -> ( K - 1 ) e. NN ) ) )
107 106 imp 
 |-  ( ( -. M = 0 /\ -. M = K ) -> ( ( M e. NN0 /\ K e. NN0 /\ M <_ K ) -> ( K - 1 ) e. NN ) )
108 26 107 sylbi 
 |-  ( -. ( M = 0 \/ M = K ) -> ( ( M e. NN0 /\ K e. NN0 /\ M <_ K ) -> ( K - 1 ) e. NN ) )
109 108 com12 
 |-  ( ( M e. NN0 /\ K e. NN0 /\ M <_ K ) -> ( -. ( M = 0 \/ M = K ) -> ( K - 1 ) e. NN ) )
110 109 con1d 
 |-  ( ( M e. NN0 /\ K e. NN0 /\ M <_ K ) -> ( -. ( K - 1 ) e. NN -> ( M = 0 \/ M = K ) ) )
111 110 com12 
 |-  ( -. ( K - 1 ) e. NN -> ( ( M e. NN0 /\ K e. NN0 /\ M <_ K ) -> ( M = 0 \/ M = K ) ) )
112 30 adantr 
 |-  ( ( M e. NN0 /\ K e. NN0 ) -> M e. RR )
113 32 adantl 
 |-  ( ( M e. NN0 /\ K e. NN0 ) -> K e. RR )
114 1red 
 |-  ( ( M e. NN0 /\ K e. NN0 ) -> 1 e. RR )
115 112 113 114 3jca 
 |-  ( ( M e. NN0 /\ K e. NN0 ) -> ( M e. RR /\ K e. RR /\ 1 e. RR ) )
116 115 3adant3 
 |-  ( ( M e. NN0 /\ K e. NN0 /\ M <_ K ) -> ( M e. RR /\ K e. RR /\ 1 e. RR ) )
117 ltsub1 
 |-  ( ( M e. RR /\ K e. RR /\ 1 e. RR ) -> ( M < K <-> ( M - 1 ) < ( K - 1 ) ) )
118 116 117 syl 
 |-  ( ( M e. NN0 /\ K e. NN0 /\ M <_ K ) -> ( M < K <-> ( M - 1 ) < ( K - 1 ) ) )
119 118 bicomd 
 |-  ( ( M e. NN0 /\ K e. NN0 /\ M <_ K ) -> ( ( M - 1 ) < ( K - 1 ) <-> M < K ) )
120 119 notbid 
 |-  ( ( M e. NN0 /\ K e. NN0 /\ M <_ K ) -> ( -. ( M - 1 ) < ( K - 1 ) <-> -. M < K ) )
121 eqlelt 
 |-  ( ( M e. RR /\ K e. RR ) -> ( M = K <-> ( M <_ K /\ -. M < K ) ) )
122 30 32 121 syl2an 
 |-  ( ( M e. NN0 /\ K e. NN0 ) -> ( M = K <-> ( M <_ K /\ -. M < K ) ) )
123 122 biimpar 
 |-  ( ( ( M e. NN0 /\ K e. NN0 ) /\ ( M <_ K /\ -. M < K ) ) -> M = K )
124 123 olcd 
 |-  ( ( ( M e. NN0 /\ K e. NN0 ) /\ ( M <_ K /\ -. M < K ) ) -> ( M = 0 \/ M = K ) )
125 124 exp43 
 |-  ( M e. NN0 -> ( K e. NN0 -> ( M <_ K -> ( -. M < K -> ( M = 0 \/ M = K ) ) ) ) )
126 125 3imp 
 |-  ( ( M e. NN0 /\ K e. NN0 /\ M <_ K ) -> ( -. M < K -> ( M = 0 \/ M = K ) ) )
127 120 126 sylbid 
 |-  ( ( M e. NN0 /\ K e. NN0 /\ M <_ K ) -> ( -. ( M - 1 ) < ( K - 1 ) -> ( M = 0 \/ M = K ) ) )
128 127 com12 
 |-  ( -. ( M - 1 ) < ( K - 1 ) -> ( ( M e. NN0 /\ K e. NN0 /\ M <_ K ) -> ( M = 0 \/ M = K ) ) )
129 25 111 128 3jaoi 
 |-  ( ( -. ( M - 1 ) e. NN0 \/ -. ( K - 1 ) e. NN \/ -. ( M - 1 ) < ( K - 1 ) ) -> ( ( M e. NN0 /\ K e. NN0 /\ M <_ K ) -> ( M = 0 \/ M = K ) ) )
130 12 129 sylbi 
 |-  ( -. ( ( M - 1 ) e. NN0 /\ ( K - 1 ) e. NN /\ ( M - 1 ) < ( K - 1 ) ) -> ( ( M e. NN0 /\ K e. NN0 /\ M <_ K ) -> ( M = 0 \/ M = K ) ) )
131 130 com12 
 |-  ( ( M e. NN0 /\ K e. NN0 /\ M <_ K ) -> ( -. ( ( M - 1 ) e. NN0 /\ ( K - 1 ) e. NN /\ ( M - 1 ) < ( K - 1 ) ) -> ( M = 0 \/ M = K ) ) )
132 11 131 sylbid 
 |-  ( ( M e. NN0 /\ K e. NN0 /\ M <_ K ) -> ( -. ( M - 1 ) e. ( 0 ..^ ( K - 1 ) ) -> ( M = 0 \/ M = K ) ) )
133 8 132 sylbid 
 |-  ( ( M e. NN0 /\ K e. NN0 /\ M <_ K ) -> ( -. M e. ( 1 ..^ K ) -> ( M = 0 \/ M = K ) ) )
134 1 133 sylbi 
 |-  ( M e. ( 0 ... K ) -> ( -. M e. ( 1 ..^ K ) -> ( M = 0 \/ M = K ) ) )
135 134 imp 
 |-  ( ( M e. ( 0 ... K ) /\ -. M e. ( 1 ..^ K ) ) -> ( M = 0 \/ M = K ) )