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∈0…K∧¬M∈1..^K→M=0∨M=K

Proof

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